From 89fc5be1ab523affd78d8fe796a135cec6070be5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 27 Jan 2015 08:50:32 +0100 Subject: [PATCH] Fixed some things and wrote tests for elimination-based DTMC modelchecker. They fail: apparently rewards are not correctly computed in some cases. Former-commit-id: 000ad6b049464a8f6e3e42608c18273923094522 --- src/modelchecker/CheckResult.h | 1 - .../SparseMarkovAutomatonCslModelChecker.cpp | 90 ++++++------- .../SparseMarkovAutomatonCslModelChecker.h | 1 - .../SparseDtmcEliminationModelChecker.cpp | 71 ++++++++--- .../SparseDtmcEliminationModelChecker.h | 1 + .../SparseDtmcEliminationModelCheckerTest.cpp | 120 ++++++++++++++++++ 6 files changed, 216 insertions(+), 68 deletions(-) create mode 100644 test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp diff --git a/src/modelchecker/CheckResult.h b/src/modelchecker/CheckResult.h index 4e0754652..9e7c061e7 100644 --- a/src/modelchecker/CheckResult.h +++ b/src/modelchecker/CheckResult.h @@ -31,7 +31,6 @@ namespace storm { virtual bool isExplicitQualitativeCheckResult() const; virtual bool isExplicitQuantitativeCheckResult() const; - virtual bool isExplicitSingleStateQuantitativeCheckResult() const; ExplicitQualitativeCheckResult& asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& asExplicitQualitativeCheckResult() const; diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 508157d94..123be8cbc 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -235,56 +235,6 @@ namespace storm { template std::vector SparseMarkovAutomatonCslModelChecker::computeLongRunAverageHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const { - // FIXME - } - - template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - STORM_LOG_THROW(model.isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute long-run average in non-closed Markov automaton."); - std::unique_ptr subResultPointer = this->check(stateFormula); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeLongRunAverageHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector(), qualitative))); - } - - template - std::vector SparseMarkovAutomatonCslModelChecker::computeExpectedTimesHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const { - std::vector rewardValues(model.getNumberOfStates(), storm::utility::zero()); - storm::utility::vector::setVectorValues(rewardValues, model.getMarkovianStates(), storm::utility::one()); - return this->computeExpectedRewards(minimize, psiStates, rewardValues); - } - - template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - STORM_LOG_THROW(model.isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute expected times in non-closed Markov automaton."); - std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); - ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeExpectedTimesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector(), qualitative))); - } - - template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) { - if (stateFormula.isTrueFormula()) { - return std::unique_ptr(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates(), true))); - } else { - return std::unique_ptr(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates()))); - } - } - - template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) { - STORM_LOG_THROW(model.hasAtomicProposition(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'."); - return std::unique_ptr(new ExplicitQualitativeCheckResult(model.getLabeledStates(stateFormula.getLabel()))); - } - - template - std::vector SparseMarkovAutomatonCslModelChecker::computeLongRunAverage(bool minimize, storm::storage::BitVector const& psiStates) const { - // Check whether the automaton is closed. - if (!model.isClosed()) { - throw storm::exceptions::InvalidArgumentException() << "Unable to compute long-run average on non-closed Markov automaton."; - } - // If there are no goal states, we avoid the computation and directly return zero. if (psiStates.empty()) { return std::vector(model.getNumberOfStates(), storm::utility::zero()); @@ -443,6 +393,46 @@ namespace storm { return result; } + template + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + STORM_LOG_THROW(model.isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute long-run average in non-closed Markov automaton."); + std::unique_ptr subResultPointer = this->check(stateFormula); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeLongRunAverageHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector(), qualitative))); + } + + template + std::vector SparseMarkovAutomatonCslModelChecker::computeExpectedTimesHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const { + std::vector rewardValues(model.getNumberOfStates(), storm::utility::zero()); + storm::utility::vector::setVectorValues(rewardValues, model.getMarkovianStates(), storm::utility::one()); + return this->computeExpectedRewards(minimize, psiStates, rewardValues); + } + + template + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + STORM_LOG_THROW(model.isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute expected times in non-closed Markov automaton."); + std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); + ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeExpectedTimesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector(), qualitative))); + } + + template + std::unique_ptr SparseMarkovAutomatonCslModelChecker::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) { + if (stateFormula.isTrueFormula()) { + return std::unique_ptr(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates(), true))); + } else { + return std::unique_ptr(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates()))); + } + } + + template + std::unique_ptr SparseMarkovAutomatonCslModelChecker::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) { + STORM_LOG_THROW(model.hasAtomicProposition(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'."); + return std::unique_ptr(new ExplicitQualitativeCheckResult(model.getLabeledStates(stateFormula.getLabel()))); + } + template ValueType SparseMarkovAutomatonCslModelChecker::computeLraForMaximalEndComponent(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::BitVector const& markovianStates, std::vector const& exitRates, storm::storage::BitVector const& psiStates, storm::storage::MaximalEndComponent const& mec, uint_fast64_t mecIndex) { std::shared_ptr solver = storm::utility::solver::getLpSolver("LRA for MEC"); diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 0b47e3cf6..86eb07bdc 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -36,7 +36,6 @@ namespace storm { std::vector computeReachabilityRewardsHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const; std::vector computeLongRunAverageHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const; std::vector computeExpectedTimesHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const; - std::vector computeLongRunAverage(bool minimize, storm::storage::BitVector const& psiStates) const; /*! * Computes the long-run average value for the given maximal end component of a Markov automaton. diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 0a531ff8d..8f3659eab 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -14,7 +14,6 @@ #include "src/utility/graph.h" #include "src/utility/vector.h" #include "src/utility/macros.h" -#include "src/utility/ConstantsComparator.h" #include "src/exceptions/InvalidPropertyException.h" #include "src/exceptions/InvalidStateException.h" @@ -63,6 +62,8 @@ namespace storm { if (conditionalPathFormula.getLeftSubformula().isEventuallyFormula() && conditionalPathFormula.getRightSubformula().isEventuallyFormula()) { return this->canHandle(conditionalPathFormula.getLeftSubformula()) && this->canHandle(conditionalPathFormula.getRightSubformula()); } + } else if (formula.isPropositionalFormula()) { + return true; } return false; } @@ -77,6 +78,7 @@ namespace storm { // Do some sanity checks to establish some required properties. STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); + storm::storage::sparse::state_type initialState = *model.getInitialStates().begin(); // Then, compute the subset of states that has a probability of 0 or 1, respectively. std::pair statesWithProbability01 = storm::utility::graph::performProb01(model, phiStates, psiStates); @@ -87,7 +89,7 @@ namespace storm { // If the initial state is known to have either probability 0 or 1, we can directly return the result. if (model.getInitialStates().isDisjointFrom(maybeStates)) { STORM_LOG_DEBUG("The probability of all initial states was found in a preprocessing step."); - return statesWithProbability0.get(*model.getInitialStates().begin()) ? storm::utility::zero() : storm::utility::one(); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, statesWithProbability0.get(*model.getInitialStates().begin()) ? storm::utility::zero() : storm::utility::one())); } // Determine the set of states that is reachable from the initial state without jumping over a target state. @@ -111,7 +113,7 @@ namespace storm { std::vector statePriorities = getStatePriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities); boost::optional> missingStateRewards; - return computeReachabilityValue(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, missingStateRewards, statePriorities); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, computeReachabilityValue(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, missingStateRewards, statePriorities))); } template @@ -122,10 +124,10 @@ namespace storm { storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); // Do some sanity checks to establish some required properties. - STORM_LOG_THROW(!model.hasTransitionRewards(), storm::exceptions::IllegalArgumentException, "Input model does have transition-based rewards, which are currently unsupported."); - STORM_LOG_THROW(model.hasStateRewards(), storm::exceptions::IllegalArgumentException, "Input model does not have a state-based reward model."); + STORM_LOG_THROW(model.hasStateRewards() || model.hasTransitionRewards(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model."); STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); - + storm::storage::sparse::state_type initialState = *model.getInitialStates().begin(); + // Then, compute the subset of states that has a reachability reward less than infinity. storm::storage::BitVector trueStates(model.getNumberOfStates(), true); storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(model.getBackwardTransitions(), trueStates, psiStates); @@ -136,7 +138,7 @@ namespace storm { STORM_LOG_THROW(model.getInitialStates().isDisjointFrom(infinityStates), storm::exceptions::IllegalArgumentException, "Initial state has infinite reward."); if (!model.getInitialStates().isDisjointFrom(psiStates)) { STORM_LOG_DEBUG("The reward of all initial states was found in a preprocessing step."); - return storm::utility::zero(); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, storm::utility::zero())); } // Determine the set of states that is reachable from the initial state without jumping over a target state. @@ -148,10 +150,6 @@ namespace storm { // Create a vector for the probabilities to go to a state with probability 1 in one step. std::vector oneStepProbabilities = model.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, psiStates); - // Project the state reward vector to all maybe-states. - boost::optional> stateRewards(maybeStates.getNumberOfSetBits()); - storm::utility::vector::selectVectorValues(stateRewards.get(), maybeStates, model.getStateRewardVector()); - // Determine the set of initial states of the sub-model. storm::storage::BitVector newInitialStates = model.getInitialStates() % maybeStates; @@ -162,8 +160,35 @@ namespace storm { // Before starting the model checking process, we assign priorities to states so we can use them to // impose ordering constraints later. std::vector statePriorities = getStatePriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities); + + // Project the state reward vector to all maybe-states. + boost::optional> optionalStateRewards(maybeStates.getNumberOfSetBits()); + std::vector& stateRewards = optionalStateRewards.get(); + if (model.hasTransitionRewards()) { + // If a transition-based reward model is available, we initialize the right-hand + // side to the vector resulting from summing the rows of the pointwise product + // of the transition probability matrix and the transition reward matrix. + std::vector pointwiseProductRowSumVector = model.getTransitionMatrix().getPointwiseProductRowSumVector(model.getTransitionRewardMatrix()); + storm::utility::vector::selectVectorValues(stateRewards, maybeStates, pointwiseProductRowSumVector); + + if (model.hasStateRewards()) { + // If a state-based reward model is also available, we need to add this vector + // as well. As the state reward vector contains entries not just for the states + // that we still consider (i.e. maybeStates), we need to extract these values + // first. + std::vector subStateRewards(stateRewards.size()); + storm::utility::vector::selectVectorValues(subStateRewards, maybeStates, model.getStateRewardVector()); + storm::utility::vector::addVectorsInPlace(stateRewards, subStateRewards); + } + } else { + // If only a state-based reward model is available, we take this vector as the + // right-hand side. As the state reward vector contains entries not just for the + // states that we still consider (i.e. maybeStates), we need to extract these values + // first. + storm::utility::vector::selectVectorValues(stateRewards, maybeStates, model.getStateRewardVector()); + } - return computeReachabilityValue(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, stateRewards, statePriorities); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, computeReachabilityValue(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, optionalStateRewards, statePriorities))); } template @@ -179,8 +204,9 @@ namespace storm { storm::storage::BitVector trueStates(model.getNumberOfStates(), true); // Do some sanity checks to establish some required properties. - STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); STORM_LOG_THROW(storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() != storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State, storm::exceptions::InvalidArgumentException, "Unsupported elimination method for conditional probabilities."); + STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); + storm::storage::sparse::state_type initialState = *model.getInitialStates().begin(); storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); @@ -194,7 +220,7 @@ namespace storm { if (model.getInitialStates().isSubsetOf(statesWithProbability1)) { std::shared_ptr trueFormula = std::make_shared(true); std::shared_ptr untilFormula = std::make_shared(trueFormula, pathFormula.getLeftSubformula().asSharedPointer()); - return this->computeUntilProbabilities(untilFormula); + return this->computeUntilProbabilities(*untilFormula); } // From now on, we know the condition does not have a trivial probability in the initial state. @@ -306,7 +332,7 @@ namespace storm { } } - return numerator / denominator; + return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, numerator / denominator)); } template @@ -337,6 +363,8 @@ namespace storm { FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(backwardTransitions, true); auto conversionEnd = std::chrono::high_resolution_clock::now(); + flexibleMatrix.print(); + std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now(); uint_fast64_t maximalDepth = 0; if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State) { @@ -387,6 +415,7 @@ namespace storm { // of the initial state, this amounts to checking whether the outgoing transitions of the initial // state are non-empty. if (!flexibleMatrix.getRow(*initialStates.begin()).empty()) { + flexibleMatrix.print(); STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).size() == 1, "At most one outgoing transition expected at this point, but found more."); STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).front().getColumn() == *initialStates.begin(), "Remaining entry should be a self-loop, but it is not."); ValueType loopProbability = flexibleMatrix.getRow(*initialStates.begin()).front().getValue(); @@ -394,10 +423,12 @@ namespace storm { loopProbability = storm::utility::pow(loopProbability, 2); STORM_PRINT_AND_LOG("Scaling the transition reward of the initial state."); stateRewards.get()[(*initialStates.begin())] *= loopProbability; + flexibleMatrix.getRow(*initialStates.begin()).clear(); } } // Make sure that we have eliminated all transitions from the initial state. + flexibleMatrix.print(); STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).empty(), "The transitions of the initial states are non-empty."); std::chrono::high_resolution_clock::time_point modelCheckingEnd = std::chrono::high_resolution_clock::now(); @@ -595,7 +626,7 @@ namespace storm { } bool hasSelfLoop = false; - ValueType loopProbability = storm::utility:: (); + ValueType loopProbability = storm::utility::zero(); // Start by finding loop probability. typename FlexibleSparseMatrix::row_type& currentStateSuccessors = matrix.getRow(state); @@ -838,11 +869,19 @@ namespace storm { typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix SparseDtmcEliminationModelChecker::getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne) { FlexibleSparseMatrix flexibleMatrix(matrix.getRowCount()); + // A comparator used for comparing probabilities. + storm::utility::ConstantsComparator comparator; + for (typename FlexibleSparseMatrix::index_type rowIndex = 0; rowIndex < matrix.getRowCount(); ++rowIndex) { typename storm::storage::SparseMatrix::const_rows row = matrix.getRow(rowIndex); flexibleMatrix.reserveInRow(rowIndex, row.getNumberOfEntries()); for (auto const& element : row) { + // If the probability is zero, we skip this entry. + if (comparator.isZero(element.getValue())) { + continue; + } + if (setAllValuesToOne) { flexibleMatrix.getRow(rowIndex).emplace_back(element.getColumn(), storm::utility::one()); } else { diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index d3ab0bdd0..0aed17aff 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -4,6 +4,7 @@ #include "src/storage/sparse/StateType.h" #include "src/models/Dtmc.h" #include "src/modelchecker/AbstractModelChecker.h" +#include "src/utility/ConstantsComparator.h" namespace storm { namespace modelchecker { diff --git a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp new file mode 100644 index 000000000..04e944f8c --- /dev/null +++ b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp @@ -0,0 +1,120 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/logic/Formulas.h" +#include "src/solver/GmmxxLinearEquationSolver.h" +#include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" +#include "src/modelchecker/ExplicitQuantitativeCheckResult.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/SettingMemento.h" +#include "src/parser/AutoParser.h" + +TEST(SparseDtmcEliminationModelCheckerTest, Die) { + std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew"); + + ASSERT_EQ(abstractModel->getType(), storm::models::DTMC); + + std::shared_ptr> dtmc = abstractModel->as>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); + + storm::modelchecker::SparseDtmcEliminationModelChecker checker(*dtmc); + + auto labelFormula = std::make_shared("one"); + auto eventuallyFormula = std::make_shared(labelFormula); + + std::unique_ptr result = checker.check(*eventuallyFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("two"); + eventuallyFormula = std::make_shared(labelFormula); + + result = checker.check(*eventuallyFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("three"); + eventuallyFormula = std::make_shared(labelFormula); + + result = checker.check(*eventuallyFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + + auto done = std::make_shared("done"); + auto reachabilityRewardFormula = std::make_shared(done); + + result = checker.check(*reachabilityRewardFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(11.0/3.0, quantitativeResult4[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); +} + +TEST(SparseDtmcEliminationModelCheckerTest, Crowds) { + std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", ""); + + ASSERT_EQ(abstractModel->getType(), storm::models::DTMC); + + std::shared_ptr> dtmc = abstractModel->as>(); + + ASSERT_EQ(8607ull, dtmc->getNumberOfStates()); + ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions()); + + storm::modelchecker::SparseDtmcEliminationModelChecker checker(*dtmc); + + auto labelFormula = std::make_shared("observe0Greater1"); + auto eventuallyFormula = std::make_shared(labelFormula); + + std::unique_ptr result = checker.check(*eventuallyFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.3328800375801578281, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("observeIGreater1"); + eventuallyFormula = std::make_shared(labelFormula); + + result = checker.check(*eventuallyFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.1522194965, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("observeOnlyTrueSender"); + eventuallyFormula = std::make_shared(labelFormula); + + result = checker.check(*eventuallyFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.32153724292835045, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); +} + +TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) { + std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.pick.trans.rew"); + + ASSERT_EQ(abstractModel->getType(), storm::models::DTMC); + std::shared_ptr> dtmc = abstractModel->as>(); + + ASSERT_EQ(12400ull, dtmc->getNumberOfStates()); + ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions()); + + storm::modelchecker::SparseDtmcEliminationModelChecker checker(*dtmc); + + auto labelFormula = std::make_shared("elected"); + auto eventuallyFormula = std::make_shared(labelFormula); + + std::unique_ptr result = checker.check(*eventuallyFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("elected"); + auto reachabilityRewardFormula = std::make_shared(labelFormula); + + result = checker.check(*reachabilityRewardFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.044879046, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); +}