From 81100c7afd238404aaf0a74dc3ba3e9d8cb5008e Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 26 Feb 2015 18:41:33 +0100 Subject: [PATCH] debugged and added more tests for prob0/1 for MDPs using BDDs Former-commit-id: f47fb3631ad16b3131339f025153bd9d7a496fe5 --- src/builder/DdPrismModelBuilder.cpp | 2 +- src/utility/graph.h | 36 +++++++++++++++++---------- test/functional/utility/GraphTest.cpp | 34 +++++++++++++++++-------- 3 files changed, 48 insertions(+), 24 deletions(-) diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 03b225768..74508e763 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -668,7 +668,7 @@ namespace storm { // Build the labels that can be accessed as a shortcut. std::map labelToExpressionMapping; - for (auto const& label : program.getLabels()) { + for (auto const& label : preparedProgram.getLabels()) { labelToExpressionMapping.emplace(label.getName(), label.getStatePredicateExpression()); } diff --git a/src/utility/graph.h b/src/utility/graph.h index f2389d3e9..4fe9469af 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -724,9 +724,10 @@ namespace storm { statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.swapVariables(model.getRowColumnMetaVariablePairs()); statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.andExists(transitionMatrixBdd, model.getColumnVariables()); statesWithProbabilityGreater0E &= phiStatesBdd; + statesWithProbabilityGreater0E |= lastIterationStates; ++iterations; } - + return statesWithProbabilityGreater0E; } @@ -833,37 +834,47 @@ namespace storm { * @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. + * @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) { // 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(); + bool outerLoopDone = false; + while (!outerLoopDone) { + storm::dd::Dd innerStates = manager.getZero(); - while (innerStates != temporary) { - innerStates = temporary; - temporary = statesWithProbability1E; - temporary = temporary.swapVariables(model.getRowColumnMetaVariablePairs()); + bool innerLoopDone = false; + while (!innerLoopDone) { + storm::dd::Dd temporary = statesWithProbability1E.swapVariables(model.getRowColumnMetaVariablePairs()); temporary = transitionMatrixBdd.implies(temporary).universalAbstract(model.getColumnVariables()); - storm::dd::Dd temporary2 = innerStates; - temporary2 = temporary2.swapVariables(model.getRowColumnMetaVariablePairs()); + storm::dd::Dd temporary2 = innerStates.swapVariables(model.getRowColumnMetaVariablePairs()); temporary2 = transitionMatrixBdd.andExists(temporary2, model.getColumnVariables()); temporary = temporary.andExists(temporary2, model.getNondeterminismVariables()); temporary &= phiStatesBdd; temporary |= psiStatesBdd; + + if (innerStates == temporary) { + innerLoopDone = true; + } else { + innerStates = temporary; + } + } + + if (statesWithProbability1E == innerStates) { + outerLoopDone = true; + } else { + statesWithProbability1E = innerStates; } ++iterations; } @@ -875,7 +886,6 @@ namespace storm { 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; } diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index af1ae47db..9a17e4207 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -56,17 +56,31 @@ TEST(GraphTest, SymbolicProb01MinMax) { 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::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()); + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_1"))); + EXPECT_EQ(94, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(33, statesWithProbability01.second.getNonZeroCount()); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_1"))); + EXPECT_EQ(83, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(35, statesWithProbability01.second.getNonZeroCount()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + model = storm::builder::DdPrismModelBuilder::translateProgram(program); + + 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()); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), model->getReachableStates(), model->getStates("collision_max_backoff"))); + EXPECT_EQ(993, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(16, statesWithProbability01.second.getNonZeroCount()); } TEST(GraphTest, ExplicitProb01) {