diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 6c9a31a15..03b225768 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -709,7 +709,7 @@ namespace storm { STORM_LOG_TRACE("Iteration " << iteration << " of computing reachable states."); changed = false; storm::dd::Dd tmp = reachableStatesBdd.andExists(transitionBdd, generationInfo.rowMetaVariables); - tmp.swapVariables(generationInfo.rowColumnMetaVariablePairs); + tmp = tmp.swapVariables(generationInfo.rowColumnMetaVariablePairs); storm::dd::Dd newReachableStates = tmp && (!reachableStatesBdd); diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index 569f1eb55..178391f25 100644 --- a/src/models/symbolic/Model.cpp +++ b/src/models/symbolic/Model.cpp @@ -53,6 +53,7 @@ namespace storm { template storm::dd::Dd Model::getStates(std::string const& label) const { + STORM_LOG_THROW(labelToExpressionMap.find(label) != labelToExpressionMap.end(), storm::exceptions::InvalidArgumentException, "The label " << label << " is invalid for the labeling of the model."); return rowExpressionAdapter->translateExpression(labelToExpressionMap.at(label)) && this->reachableStates; } diff --git a/src/models/symbolic/NondeterministicModel.cpp b/src/models/symbolic/NondeterministicModel.cpp index 0dcd8ad25..59a8381e5 100644 --- a/src/models/symbolic/NondeterministicModel.cpp +++ b/src/models/symbolic/NondeterministicModel.cpp @@ -20,7 +20,10 @@ namespace storm { boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix) : Model(modelType, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, optionalStateRewardVector, optionalTransitionRewardMatrix), nondeterminismVariables(nondeterminismVariables) { - // Intentionally left empty. + + // Prepare the mask of illegal nondeterministic choices. + illegalMask = transitionMatrix.notZero().existsAbstract(this->getColumnVariables()); + illegalMask = !illegalMask && reachableStates; } template @@ -37,6 +40,11 @@ namespace storm { return nondeterminismVariables; } + template + storm::dd::Dd const& NondeterministicModel::getIllegalMask() const { + return illegalMask; + } + template void NondeterministicModel::printModelInformationToStream(std::ostream& out) const { out << "-------------------------------------------------------------- " << std::endl; diff --git a/src/models/symbolic/NondeterministicModel.h b/src/models/symbolic/NondeterministicModel.h index 7b0470ead..1e6d36cd6 100644 --- a/src/models/symbolic/NondeterministicModel.h +++ b/src/models/symbolic/NondeterministicModel.h @@ -71,12 +71,22 @@ namespace storm { */ std::set const& getNondeterminismVariables() const; + /*! + * Retrieves a BDD characterizing all illegal nondeterminism encodings in the model. + * + * @return A BDD characterizing all illegal nondeterminism encodings in the model. + */ + storm::dd::Dd const& getIllegalMask() const; + virtual void printModelInformationToStream(std::ostream& out) const override; private: // The meta variables encoding the nondeterminism in the model. std::set nondeterminismVariables; + + // A mask that characterizes all legal nondeterministic choices. + storm::dd::Dd illegalMask; }; } // namespace symbolic diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index effea029f..a169403d0 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -252,7 +252,6 @@ namespace storm { STORM_LOG_WARN_COND(false, "Performing logical iff on two DDs of different type."); return Dd(this->getDdManager(), this->getCuddBdd().Xnor(other.getCuddBdd()), metaVariables); } - return *this; } Dd Dd::exclusiveOr(Dd const& other) const { @@ -263,12 +262,18 @@ namespace storm { } else if (this->isMtbdd() && other.isMtbdd()) { // We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that // the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise. - return Dd(this->getDdManager(), this->getCuddMtbdd().Xnor(other.getCuddMtbdd()), metaVariables); + return Dd(this->getDdManager(), this->getCuddMtbdd().Xor(other.getCuddMtbdd()), metaVariables); } else { STORM_LOG_WARN_COND(false, "Performing logical iff on two DDs of different type."); return Dd(this->getDdManager(), this->getCuddBdd().Xor(other.getCuddBdd()), metaVariables); } - return *this; + } + + Dd Dd::implies(Dd const& other) const { + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + STORM_LOG_WARN_COND(this->isBdd() && other.isBdd(), "Performing logical operatiorn on MTBDDs."); + return Dd(this->getDdManager(), this->getCuddBdd().Ite(other.getCuddBdd(), this->getDdManager()->getOne().getCuddBdd()), metaVariables); } Dd Dd::equals(Dd const& other) const { @@ -422,7 +427,8 @@ namespace storm { } } - void Dd::swapVariables(std::vector> const& metaVariablePairs) { + Dd Dd::swapVariables(std::vector> const& metaVariablePairs) { + std::set newContainedMetaVariables; if (this->isBdd()) { std::vector from; std::vector to; @@ -431,19 +437,14 @@ namespace storm { DdMetaVariable const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second); // Check if it's legal so swap the meta variables. - if (variable1.getNumberOfDdVariables() != variable2.getNumberOfDdVariables()) { - throw storm::exceptions::InvalidArgumentException() << "Unable to swap meta variables with different size."; - } + STORM_LOG_THROW(variable1.getNumberOfDdVariables() == variable2.getNumberOfDdVariables(), storm::exceptions::InvalidArgumentException, "Unable to swap meta variables with different size."); // Keep track of the contained meta variables in the DD. - bool containsVariable1 = this->containsMetaVariable(metaVariablePair.first); - bool containsVariable2 = this->containsMetaVariable(metaVariablePair.second); - if (containsVariable1 && !containsVariable2) { - this->removeContainedMetaVariable(metaVariablePair.first); - this->addContainedMetaVariable(metaVariablePair.second); - } else if (!containsVariable1 && containsVariable2) { - this->removeContainedMetaVariable(metaVariablePair.second); - this->addContainedMetaVariable(metaVariablePair.first); + if (this->containsMetaVariable(metaVariablePair.first)) { + newContainedMetaVariables.insert(metaVariablePair.second); + } + if (this->containsMetaVariable(metaVariablePair.second)) { + newContainedMetaVariables.insert(metaVariablePair.first); } // Add the variables to swap to the corresponding vectors. @@ -456,7 +457,7 @@ namespace storm { } // Finally, call CUDD to swap the variables. - this->cuddDd = this->getCuddBdd().SwapVariables(from, to); + return Dd(this->getDdManager(), this->getCuddBdd().SwapVariables(from, to), newContainedMetaVariables); } else { std::vector from; std::vector to; @@ -470,14 +471,11 @@ namespace storm { } // Keep track of the contained meta variables in the DD. - bool containsVariable1 = this->containsMetaVariable(metaVariablePair.first); - bool containsVariable2 = this->containsMetaVariable(metaVariablePair.second); - if (containsVariable1 && !containsVariable2) { - this->removeContainedMetaVariable(metaVariablePair.first); - this->addContainedMetaVariable(metaVariablePair.second); - } else if (!containsVariable1 && containsVariable2) { - this->removeContainedMetaVariable(metaVariablePair.second); - this->addContainedMetaVariable(metaVariablePair.first); + if (this->containsMetaVariable(metaVariablePair.first)) { + newContainedMetaVariables.insert(metaVariablePair.second); + } + if (this->containsMetaVariable(metaVariablePair.second)) { + newContainedMetaVariables.insert(metaVariablePair.first); } // Add the variables to swap to the corresponding vectors. @@ -490,7 +488,7 @@ namespace storm { } // Finally, call CUDD to swap the variables. - this->cuddDd = this->getCuddMtbdd().SwapVariables(from, to); + return Dd(this->getDdManager(), this->getCuddMtbdd().SwapVariables(from, to), newContainedMetaVariables); } } diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 21038643a..fadbe06a9 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -111,6 +111,14 @@ namespace storm { */ Dd exclusiveOr(Dd const& other) const; + /*! + * Performs a logical implication of the current and the given DD. + * + * @param other The second DD used for the operation. + * @return The logical implication of the operands. + */ + Dd implies(Dd const& other) const; + /*! * Adds the two DDs. * @@ -317,8 +325,9 @@ namespace storm { * the same number of underlying DD variables. * * @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another. + * @return The resulting DD. */ - void swapVariables(std::vector> const& metaVariablePairs); + Dd swapVariables(std::vector> const& metaVariablePairs); /*! * Multiplies the current DD (representing a matrix) with the given matrix by summing over the given meta diff --git a/src/utility/graph.h b/src/utility/graph.h index ace5a9f64..f2389d3e9 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -274,7 +274,7 @@ namespace storm { storm::dd::Dd transitionMatrixBdd = model.getTransitionMatrix().notZero(); while (lastIterationStates != statesWithProbabilityGreater0) { lastIterationStates = statesWithProbabilityGreater0; - statesWithProbabilityGreater0.swapVariables(model.getRowColumnMetaVariablePairs()); + statesWithProbabilityGreater0 = statesWithProbabilityGreater0.swapVariables(model.getRowColumnMetaVariablePairs()); statesWithProbabilityGreater0 &= transitionMatrixBdd; statesWithProbabilityGreater0 = statesWithProbabilityGreater0.existsAbstract(model.getColumnVariables()); statesWithProbabilityGreater0 &= phiStatesBdd; @@ -700,6 +700,194 @@ namespace storm { return performProb01Min(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), phiStates, psiStates); } + /*! + * Computes the set of states for which there exists a scheduler that achieves a probability greater than + * zero of satisfying phi until psi. + * + * @param model The (symbolic) model for which to compute the set of states. + * @param phiStates The phi states of the model. + * @param psiStates The psi states of the model. + * @return A DD representing all such states. + */ + template + storm::dd::Dd performProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& phiStates, storm::dd::Dd const& psiStates) { + // Initialize environment for backward search. + storm::dd::DdManager const& manager = model.getManager(); + storm::dd::Dd lastIterationStates = manager.getZero(); + storm::dd::Dd statesWithProbabilityGreater0E = psiStates.toBdd(); + storm::dd::Dd phiStatesBdd = phiStates.toBdd(); + + uint_fast64_t iterations = 0; + storm::dd::Dd transitionMatrixBdd = model.getTransitionMatrix().notZero().existsAbstract(model.getNondeterminismVariables()); + while (lastIterationStates != statesWithProbabilityGreater0E) { + lastIterationStates = statesWithProbabilityGreater0E; + statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.swapVariables(model.getRowColumnMetaVariablePairs()); + statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.andExists(transitionMatrixBdd, model.getColumnVariables()); + statesWithProbabilityGreater0E &= phiStatesBdd; + ++iterations; + } + + return statesWithProbabilityGreater0E; + } + + /*! + * Computes the set of states for which there does not exist a scheduler that achieves a probability greater + * than zero of satisfying phi until psi. + * + * @param model The (symbolic) model for which to compute the set of states. + * @param phiStates The phi states of the model. + * @param psiStates The psi states of the model. + * @return A DD representing all such states. + */ + template + storm::dd::Dd performProb0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& phiStates, storm::dd::Dd const& psiStates) { + return !performProbGreater0E(model, phiStates, psiStates) && model.getReachableStates(); + } + + /*! + * Computes the set of states for which all schedulers achieve a probability greater than zero of satisfying + * phi until psi. + * + * @param model The (symbolic) model for which to compute the set of states. + * @param phiStates The phi states of the model. + * @param psiStates The psi states of the model. + * @return A DD representing all such states. + */ + template + storm::dd::Dd performProbGreater0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& phiStates, storm::dd::Dd const& psiStates) { + // Initialize environment for backward search. + storm::dd::DdManager const& manager = model.getManager(); + storm::dd::Dd lastIterationStates = manager.getZero(); + storm::dd::Dd statesWithProbabilityGreater0A = psiStates.toBdd(); + storm::dd::Dd phiStatesBdd = phiStates.toBdd(); + storm::dd::Dd psiStatesBdd = statesWithProbabilityGreater0A; + + uint_fast64_t iterations = 0; + storm::dd::Dd transitionMatrixBdd = model.getTransitionMatrix().notZero(); + while (lastIterationStates != statesWithProbabilityGreater0A) { + lastIterationStates = statesWithProbabilityGreater0A; + statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.swapVariables(model.getRowColumnMetaVariablePairs()); + statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.andExists(transitionMatrixBdd, model.getColumnVariables()); + statesWithProbabilityGreater0A |= model.getIllegalMask(); + statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.universalAbstract(model.getNondeterminismVariables()); + statesWithProbabilityGreater0A &= phiStatesBdd; + statesWithProbabilityGreater0A |= psiStatesBdd; + ++iterations; + } + + return statesWithProbabilityGreater0A; + } + + /*! + * Computes the set of states for which there exists a scheduler that achieves probability zero of satisfying + * phi until psi. + * + * @param model The (symbolic) model for which to compute the set of states. + * @param phiStates The phi states of the model. + * @param psiStates The psi states of the model. + * @return A DD representing all such states. + */ + template + storm::dd::Dd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& phiStates, storm::dd::Dd const& psiStates) { + return !performProbGreater0A(model, phiStates, psiStates) && model.getReachableStates(); + } + + /*! + * Computes the set of states for which all schedulers achieve probability one of satisfying phi until psi. + * + * @param model The (symbolic) model for which to compute the set of states. + * @param phiStates The phi states of the model. + * @param psiStates The psi states of the model. + * @param statesWithProbabilityGreater0A The states of the model that have a probability greater zero under + * all schedulers. + * @return A DD representing all such states. + */ + template + storm::dd::Dd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& phiStates, storm::dd::Dd const& psiStates, storm::dd::Dd const& statesWithProbabilityGreater0A) { + // Initialize environment for backward search. + storm::dd::DdManager const& manager = model.getManager(); + storm::dd::Dd lastIterationStates = manager.getZero(); + storm::dd::Dd statesWithProbability1A = psiStates.toBdd() || statesWithProbabilityGreater0A; + storm::dd::Dd psiStatesBdd = psiStates.toBdd(); + + uint_fast64_t iterations = 0; + storm::dd::Dd transitionMatrixBdd = model.getTransitionMatrix().notZero(); + while (lastIterationStates != statesWithProbability1A) { + lastIterationStates = statesWithProbability1A; + statesWithProbability1A = statesWithProbability1A.swapVariables(model.getRowColumnMetaVariablePairs()); + statesWithProbability1A = transitionMatrixBdd.implies(statesWithProbability1A).universalAbstract(model.getColumnVariables()); + statesWithProbability1A |= model.getIllegalMask(); + statesWithProbability1A = statesWithProbability1A.universalAbstract(model.getNondeterminismVariables()); + statesWithProbability1A &= statesWithProbabilityGreater0A; + statesWithProbability1A |= psiStatesBdd; + ++iterations; + } + + return statesWithProbability1A; + } + + /*! + * Computes the set of states for which there exists a scheduler that achieves probability one of satisfying + * phi until psi. + * + * @param model The (symbolic) model for which to compute the set of states. + * @param phiStates The phi states of the model. + * @param psiStates The psi states of the model. + * @param statesWithProbability0A The states of the model that have a probability zero under all schedulers. + * @return A DD representing all such states. + */ + template + storm::dd::Dd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& phiStates, storm::dd::Dd const& psiStates, storm::dd::Dd const& statesWithProbabilityGreater0E) { + // Initialize environment for backward search. + storm::dd::DdManager const& manager = model.getManager(); + storm::dd::Dd innerStates = manager.getZero(); + storm::dd::Dd statesWithProbability1E = statesWithProbabilityGreater0E; + storm::dd::Dd phiStatesBdd = phiStates.toBdd(); + storm::dd::Dd psiStatesBdd = psiStates.toBdd(); + + uint_fast64_t iterations = 0; + storm::dd::Dd transitionMatrixBdd = model.getTransitionMatrix().notZero(); + while (statesWithProbability1E != innerStates) { + innerStates = manager.getZero(); + storm::dd::Dd temporary = manager.getOne(); + + while (innerStates != temporary) { + innerStates = temporary; + temporary = statesWithProbability1E; + temporary = temporary.swapVariables(model.getRowColumnMetaVariablePairs()); + temporary = transitionMatrixBdd.implies(temporary).universalAbstract(model.getColumnVariables()); + + storm::dd::Dd temporary2 = innerStates; + temporary2 = temporary2.swapVariables(model.getRowColumnMetaVariablePairs()); + temporary2 = transitionMatrixBdd.andExists(temporary2, model.getColumnVariables()); + + temporary = temporary.andExists(temporary2, model.getNondeterminismVariables()); + temporary &= phiStatesBdd; + temporary |= psiStatesBdd; + } + ++iterations; + } + + return statesWithProbability1E; + } + + template + std::pair, storm::dd::Dd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& phiStates, storm::dd::Dd const& psiStates) { + std::pair, storm::dd::Dd> result; + result.first = performProb0A(model, phiStates, psiStates); + std::cout << "first: " << result.first.getNonZeroCount() << std::endl; + result.second = performProb1E(model, phiStates, psiStates, !result.first && model.getReachableStates()); + return result; + } + + template + std::pair, storm::dd::Dd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& phiStates, storm::dd::Dd const& psiStates) { + std::pair, storm::dd::Dd> result; + result.first = performProb0E(model, phiStates, psiStates); + result.second = performProb1A(model, phiStates, psiStates, !result.first && model.getReachableStates()); + return result; + } + /*! * Performs a topological sort of the states of the system according to the given transitions. * diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index fdc283f5e..773334797 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -234,8 +234,8 @@ TEST(CuddDd, SwapTest) { storm::dd::Dd dd2; dd1 = manager->getIdentity(x.first); - ASSERT_THROW(dd1.swapVariables({std::make_pair(x.first, z.first)}), storm::exceptions::InvalidArgumentException); - ASSERT_NO_THROW(dd1.swapVariables({std::make_pair(x.first, x.second)})); + ASSERT_THROW(dd1 = dd1.swapVariables({std::make_pair(x.first, z.first)}), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(dd1 = dd1.swapVariables({std::make_pair(x.first, x.second)})); EXPECT_TRUE(dd1 == manager->getIdentity(x.second)); } @@ -249,7 +249,7 @@ TEST(CuddDd, MultiplyMatrixTest) { dd1 *= manager->getConstant(2); ASSERT_NO_THROW(dd3 = dd1.multiplyMatrix(dd2, {x.second})); - ASSERT_NO_THROW(dd3.swapVariables({std::make_pair(x.first, x.second)})); + ASSERT_NO_THROW(dd3 = dd3.swapVariables({std::make_pair(x.first, x.second)})); EXPECT_TRUE(dd3 == dd2 * manager->getConstant(2)); } diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 071466846..af1ae47db 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -4,6 +4,7 @@ #include "src/storage/dd/CuddDd.h" #include "src/parser/PrismParser.h" #include "src/models/symbolic/Dtmc.h" +#include "src/models/symbolic/Mdp.h" #include "src/models/sparse/Dtmc.h" #include "src/builder/DdPrismModelBuilder.h" #include "src/builder/ExplicitPrismModelBuilder.h" @@ -30,6 +31,44 @@ TEST(GraphTest, SymbolicProb01) { EXPECT_EQ(1032, statesWithProbability01.second.getNonZeroCount()); } +TEST(GraphTest, SymbolicProb01MinMax) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); + + ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); + + std::pair, storm::dd::Dd> statesWithProbability01; + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("elected"))); + EXPECT_EQ(0, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(364, statesWithProbability01.second.getNonZeroCount()); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), model->getReachableStates(), model->getStates("elected"))); + EXPECT_EQ(0, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(364, statesWithProbability01.second.getNonZeroCount()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + model = storm::builder::DdPrismModelBuilder::translateProgram(program); + + ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_0"))); + EXPECT_EQ(77, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(149, statesWithProbability01.second.getNonZeroCount()); + +// ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_0"))); +// EXPECT_EQ(74, statesWithProbability01.first.getNonZeroCount()); +// EXPECT_EQ(198, statesWithProbability01.second.getNonZeroCount()); + +// ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_1"))); +// EXPECT_EQ(0, statesWithProbability01.first.getNonZeroCount()); +// EXPECT_EQ(364, statesWithProbability01.second.getNonZeroCount()); +// +// ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_1"))); +// EXPECT_EQ(0, statesWithProbability01.first.getNonZeroCount()); +// EXPECT_EQ(364, statesWithProbability01.second.getNonZeroCount()); +} + TEST(GraphTest, ExplicitProb01) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program);