From 00e7121bc4c576f93c69dc42d3e39821688ea4be Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 16 Mar 2015 20:20:15 +0100 Subject: [PATCH] some work towards BDD-based mc. Former-commit-id: cae0c4421eb495fa69ae9d659c0b8a057530db56 --- src/models/symbolic/Model.cpp | 2 +- src/utility/graph.h | 98 +++++++++++++-------------- test/functional/utility/GraphTest.cpp | 53 ++++++++++++++- 3 files changed, 102 insertions(+), 51 deletions(-) diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index 178391f25..6778d8eb0 100644 --- a/src/models/symbolic/Model.cpp +++ b/src/models/symbolic/Model.cpp @@ -54,7 +54,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; + return rowExpressionAdapter->translateExpression(labelToExpressionMap.at(label)).toBdd() && this->reachableStates; } template diff --git a/src/utility/graph.h b/src/utility/graph.h index 4fe9469af..8eff8179d 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -258,20 +258,19 @@ namespace storm { * through phi states before. * * @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 transitionMatrixBdd The transition matrix of the model as a BDD. + * @param phiStatesBdd The BDD containing all phi states of the model. + * @param psiStatesBdd The BDD containing all psi states of the model. * @return All states with positive probability. */ template - storm::dd::Dd performProbGreater0(storm::models::symbolic::DeterministicModel const& model, storm::dd::Dd const& phiStates, storm::dd::Dd const& psiStates) { + storm::dd::Dd performProbGreater0(storm::models::symbolic::DeterministicModel const& model, storm::dd::Dd const& transitionMatrixBdd, storm::dd::Dd const& phiStatesBdd, storm::dd::Dd const& psiStatesBdd) { // Initialize environment for backward search. storm::dd::DdManager const& manager = model.getManager(); storm::dd::Dd lastIterationStates = manager.getZero(); - storm::dd::Dd statesWithProbabilityGreater0 = psiStates.toBdd(); - storm::dd::Dd phiStatesBdd = phiStates.toBdd(); + storm::dd::Dd statesWithProbabilityGreater0 = psiStatesBdd; uint_fast64_t iterations = 0; - storm::dd::Dd transitionMatrixBdd = model.getTransitionMatrix().notZero(); while (lastIterationStates != statesWithProbabilityGreater0) { lastIterationStates = statesWithProbabilityGreater0; statesWithProbabilityGreater0 = statesWithProbabilityGreater0.swapVariables(model.getRowColumnMetaVariablePairs()); @@ -290,15 +289,17 @@ namespace storm { * deterministic model. * * @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 transitionMatrixBdd The transition matrix of the model as a BDD. + * @param phiStatesBdd The BDD containing all phi states of the model. + * @param psiStatesBdd The BDD containing all psi states of the model. * @return A pair of DDs that represent all states with probability 0 and 1, respectively. */ template - static std::pair, storm::dd::Dd> performProb01(storm::models::symbolic::DeterministicModel const& model, storm::dd::Dd const& phiStates, storm::dd::Dd const& psiStates) { + static std::pair, storm::dd::Dd> performProb01(storm::models::symbolic::DeterministicModel const& model, storm::dd::Dd const& phiStatesBdd, storm::dd::Dd const& psiStatesBdd) { std::pair, storm::dd::Dd> result; - result.first = performProbGreater0(model, phiStates, psiStates); - result.second = !performProbGreater0(model, !psiStates && model.getReachableStates(), !result.first && model.getReachableStates()) && model.getReachableStates(); + storm::dd::Dd transitionMatrixBdd = model.getTransitionMatrix().notZero(); + result.first = performProbGreater0(model, transitionMatrixBdd, phiStatesBdd, psiStatesBdd); + result.second = !performProbGreater0(model, transitionMatrixBdd, !psiStatesBdd && model.getReachableStates(), !result.first && model.getReachableStates()) && model.getReachableStates(); result.first = !result.first && model.getReachableStates(); return result; } @@ -705,24 +706,24 @@ namespace storm { * 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. + * @param transitionMatrixBdd The transition matrix of the model as a BDD. + * @param phiStatesBdd The BDD containing all phi states of the model. + * @param psiStatesBdd The BDD containing all 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) { + storm::dd::Dd performProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& transitionMatrixBdd, storm::dd::Dd const& phiStatesBdd, storm::dd::Dd const& psiStatesBdd) { // 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(); + storm::dd::Dd statesWithProbabilityGreater0E = psiStatesBdd; uint_fast64_t iterations = 0; - storm::dd::Dd transitionMatrixBdd = model.getTransitionMatrix().notZero().existsAbstract(model.getNondeterminismVariables()); + storm::dd::Dd abstractedTransitionMatrixBdd = transitionMatrixBdd.existsAbstract(model.getNondeterminismVariables()); while (lastIterationStates != statesWithProbabilityGreater0E) { lastIterationStates = statesWithProbabilityGreater0E; statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.swapVariables(model.getRowColumnMetaVariablePairs()); - statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.andExists(transitionMatrixBdd, model.getColumnVariables()); + statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.andExists(abstractedTransitionMatrixBdd, model.getColumnVariables()); statesWithProbabilityGreater0E &= phiStatesBdd; statesWithProbabilityGreater0E |= lastIterationStates; ++iterations; @@ -736,13 +737,14 @@ namespace storm { * than zero of satisfying phi until psi. * * @param model The (symbolic) model for which to compute the set of states. + * @param transitionMatrixBdd The transition matrix of the model as a BDD. * @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(); + storm::dd::Dd performProb0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& transitionMatrixBdd, storm::dd::Dd const& phiStatesBdd, storm::dd::Dd const& psiStatesBdd) { + return !performProbGreater0E(model, transitionMatrixBdd, phiStatesBdd, psiStatesBdd) && model.getReachableStates(); } /*! @@ -750,21 +752,19 @@ namespace storm { * 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 transitionMatrixBdd The transition matrix of the model as a BDD. + * @param phiStatesBdd The BDD containing all phi states of the model. + * @param psiStatesBdd The BDD containing all 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) { + storm::dd::Dd performProbGreater0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& transitionMatrixBdd, storm::dd::Dd const& phiStatesBdd, storm::dd::Dd const& psiStatesBdd) { // 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; + storm::dd::Dd statesWithProbabilityGreater0A = psiStatesBdd; uint_fast64_t iterations = 0; - storm::dd::Dd transitionMatrixBdd = model.getTransitionMatrix().notZero(); while (lastIterationStates != statesWithProbabilityGreater0A) { lastIterationStates = statesWithProbabilityGreater0A; statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.swapVariables(model.getRowColumnMetaVariablePairs()); @@ -784,35 +784,35 @@ namespace storm { * 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 transitionMatrixBdd The transition matrix of the model as a BDD. + * @param phiStatesBdd The BDD containing all phi states of the model. + * @param psiStatesBdd The BDD containing all 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(); + storm::dd::Dd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& transitionMatrixBdd, storm::dd::Dd const& phiStatesBdd, storm::dd::Dd const& psiStatesBdd) { + return !performProbGreater0A(model, transitionMatrixBdd, phiStatesBdd, psiStatesBdd) && 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 transitionMatrixBdd The transition matrix of the model as a BDD. + * @param phiStatesBdd The BDD containing all phi states of the model. + * @param psiStatesBdd The BDD containing all 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) { + storm::dd::Dd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& transitionMatrixBdd, storm::dd::Dd const& phiStatesBdd, storm::dd::Dd const& psiStatesBdd, 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(); + storm::dd::Dd statesWithProbability1A = psiStatesBdd || statesWithProbabilityGreater0A; uint_fast64_t iterations = 0; - storm::dd::Dd transitionMatrixBdd = model.getTransitionMatrix().notZero(); while (lastIterationStates != statesWithProbability1A) { lastIterationStates = statesWithProbability1A; statesWithProbability1A = statesWithProbability1A.swapVariables(model.getRowColumnMetaVariablePairs()); @@ -832,22 +832,20 @@ namespace storm { * 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 transitionMatrixBdd The transition matrix of the model as a BDD. + * @param phiStatesBdd The BDD containing all phi states of the model. + * @param psiStatesBdd The BDD containing all psi states of the model. * @param statesWithProbabilityGreater0E The states of the model that have a scheduler that achieves a value * greater than zero. * @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) { + storm::dd::Dd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& transitionMatrixBdd, storm::dd::Dd const& phiStatesBdd, storm::dd::Dd const& psiStatesBdd, storm::dd::Dd const& statesWithProbabilityGreater0E) { // Initialize environment for backward search. storm::dd::DdManager const& manager = model.getManager(); 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(); bool outerLoopDone = false; while (!outerLoopDone) { storm::dd::Dd innerStates = manager.getZero(); @@ -883,18 +881,20 @@ namespace storm { } 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> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& phiStatesBdd, storm::dd::Dd const& psiStatesBdd) { std::pair, storm::dd::Dd> result; - result.first = performProb0A(model, phiStates, psiStates); - result.second = performProb1E(model, phiStates, psiStates, !result.first && model.getReachableStates()); + storm::dd::Dd transitionMatrixBdd = model.getTransitionMatrix().notZero(); + result.first = performProb0A(model, transitionMatrixBdd, phiStatesBdd, psiStatesBdd); + result.second = performProb1E(model, transitionMatrixBdd, phiStatesBdd, psiStatesBdd, !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> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& phiStatesBdd, storm::dd::Dd const& psiStatesBdd) { std::pair, storm::dd::Dd> result; - result.first = performProb0E(model, phiStates, psiStates); - result.second = performProb1A(model, phiStates, psiStates, !result.first && model.getReachableStates()); + storm::dd::Dd transitionMatrixBdd = model.getTransitionMatrix().notZero(); + result.first = performProb0E(model, transitionMatrixBdd, phiStatesBdd, psiStatesBdd); + result.second = performProb1A(model, transitionMatrixBdd, phiStatesBdd, psiStatesBdd, !result.first && model.getReachableStates()); return result; } diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 9a17e4207..68c62182a 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -6,6 +6,7 @@ #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/Mdp.h" #include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/Mdp.h" #include "src/builder/DdPrismModelBuilder.h" #include "src/builder/ExplicitPrismModelBuilder.h" #include "src/utility/graph.h" @@ -73,7 +74,6 @@ TEST(GraphTest, SymbolicProb01MinMax) { ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); - statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("collision_max_backoff")); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("collision_max_backoff"))); EXPECT_EQ(993, statesWithProbability01.first.getNonZeroCount()); EXPECT_EQ(16, statesWithProbability01.second.getNonZeroCount()); @@ -102,4 +102,55 @@ TEST(GraphTest, ExplicitProb01) { ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("observeOnlyTrueSender"))); EXPECT_EQ(5829, statesWithProbability01.first.getNumberOfSetBits()); EXPECT_EQ(1032, statesWithProbability01.second.getNumberOfSetBits()); +} + +TEST(GraphTest, ExplicitProb01MinMax) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + + ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); + + std::pair statesWithProbability01; + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("elected"))); + EXPECT_EQ(0, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(364, statesWithProbability01.second.getNumberOfSetBits()); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("elected"))); + EXPECT_EQ(0, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(364, statesWithProbability01.second.getNumberOfSetBits()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + + ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("all_coins_equal_0"))); + EXPECT_EQ(77, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(149, statesWithProbability01.second.getNumberOfSetBits()); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("all_coins_equal_0"))); + EXPECT_EQ(74, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(198, statesWithProbability01.second.getNumberOfSetBits()); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("all_coins_equal_1"))); + EXPECT_EQ(94, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(33, statesWithProbability01.second.getNumberOfSetBits()); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("all_coins_equal_1"))); + EXPECT_EQ(83, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(35, statesWithProbability01.second.getNumberOfSetBits()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + + ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("collision_max_backoff"))); + EXPECT_EQ(993, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(16, statesWithProbability01.second.getNumberOfSetBits()); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("collision_max_backoff"))); + EXPECT_EQ(993, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(16, statesWithProbability01.second.getNumberOfSetBits()); } \ No newline at end of file