From ca651ec61cc91cc1ebcacc8812879f01b8940009 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 23 May 2018 13:03:14 +0200 Subject: [PATCH] fixes github issue #24 related to MEC decomposition --- .../testfiles/mdp/prism-mec-example1.nm | 12 ++++++ .../testfiles/mdp/prism-mec-example2.nm | 13 ++++++ .../MaximalEndComponentDecomposition.cpp | 35 +++++++++------ ...tronglyConnectedComponentDecomposition.cpp | 5 +++ .../StronglyConnectedComponentDecomposition.h | 16 ++++++- .../MaximalEndComponentDecompositionTest.cpp | 43 +++++++++++++++++++ 6 files changed, 111 insertions(+), 13 deletions(-) create mode 100644 resources/examples/testfiles/mdp/prism-mec-example1.nm create mode 100644 resources/examples/testfiles/mdp/prism-mec-example2.nm diff --git a/resources/examples/testfiles/mdp/prism-mec-example1.nm b/resources/examples/testfiles/mdp/prism-mec-example1.nm new file mode 100644 index 000000000..bb8ec7d17 --- /dev/null +++ b/resources/examples/testfiles/mdp/prism-mec-example1.nm @@ -0,0 +1,12 @@ +mdp + +module test + + x : [0..2]; + + [] x=0 -> true; + [] x=0 -> 0.5 : (x'=1) + 0.5: (x'=2); + [] x=1 -> (x'=0); + [] x=2 -> true; + +endmodule diff --git a/resources/examples/testfiles/mdp/prism-mec-example2.nm b/resources/examples/testfiles/mdp/prism-mec-example2.nm new file mode 100644 index 000000000..7ef54d4b2 --- /dev/null +++ b/resources/examples/testfiles/mdp/prism-mec-example2.nm @@ -0,0 +1,13 @@ +mdp + +module test + + x : [0..2]; + + [] x=0 -> true; + [] x=0 -> 0.5 : (x'=1) + 0.5: (x'=1); + [] x=0 -> (x'=2); + [] x=1 -> (x'=0); + [] x=2 -> true; + +endmodule diff --git a/src/storm/storage/MaximalEndComponentDecomposition.cpp b/src/storm/storage/MaximalEndComponentDecomposition.cpp index cd8b637e3..7cbf36fd7 100644 --- a/src/storm/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storm/storage/MaximalEndComponentDecomposition.cpp @@ -80,7 +80,20 @@ namespace storm { endComponentStateSets.emplace_back(states.begin(), states.end(), true); } storm::storage::BitVector statesToCheck(numberOfStates); - + storm::storage::BitVector includedChoices; + if (choices) { + includedChoices = *choices; + } else if (states) { + includedChoices = storm::storage::BitVector(transitionMatrix.getRowCount()); + for (auto state : *states) { + for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { + includedChoices.set(choice, true); + } + } + } else { + includedChoices = storm::storage::BitVector(transitionMatrix.getRowCount(), true); + } + for (std::list::const_iterator mecIterator = endComponentStateSets.begin(); mecIterator != endComponentStateSets.end();) { StateBlock const& mec = *mecIterator; @@ -88,7 +101,7 @@ namespace storm { bool mecChanged = false; // Get an SCC decomposition of the current MEC candidate. - StronglyConnectedComponentDecomposition sccs(transitionMatrix, mec, true); + StronglyConnectedComponentDecomposition sccs(transitionMatrix, mec, includedChoices, true); // We need to do another iteration in case we have either more than once SCC or the SCC is smaller than // the MEC canditate itself. @@ -105,10 +118,16 @@ namespace storm { bool keepStateInMEC = false; for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { + // If the choice is not part of our subsystem, skip it. if (choices && !choices->get(choice)) { continue; } + + // If the choice is not included any more, skip it. + if (!includedChoices.get(choice)) { + continue; + } bool choiceContainedInMEC = true; for (auto const& entry : transitionMatrix.getRow(choice)) { @@ -117,6 +136,7 @@ namespace storm { } if (!scc.containsState(entry.getColumn())) { + includedChoices.set(choice, false); choiceContainedInMEC = false; break; } @@ -125,7 +145,6 @@ namespace storm { // If there is at least one choice whose successor states are fully contained in the MEC, we can leave the state in the MEC. if (choiceContainedInMEC) { keepStateInMEC = true; - break; } } @@ -185,15 +204,7 @@ namespace storm { continue; } - bool choiceContained = true; - for (auto const& entry : transitionMatrix.getRow(choice)) { - if (!mecStateSet.containsState(entry.getColumn())) { - choiceContained = false; - break; - } - } - - if (choiceContained) { + if (includedChoices.get(choice)) { containedChoices.insert(choice); } } diff --git a/src/storm/storage/StronglyConnectedComponentDecomposition.cpp b/src/storm/storage/StronglyConnectedComponentDecomposition.cpp index 9eae9d05a..6ab3e31f6 100644 --- a/src/storm/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storm/storage/StronglyConnectedComponentDecomposition.cpp @@ -38,6 +38,11 @@ namespace storm { performSccDecomposition(transitionMatrix, &subsystem, nullptr, dropNaiveSccs, onlyBottomSccs); } + template + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StateBlock const& block, storm::storage::BitVector const& choices, bool dropNaiveSccs, bool onlyBottomSccs) { + storm::storage::BitVector subsystem(transitionMatrix.getRowGroupCount(), block.begin(), block.end()); + performSccDecomposition(transitionMatrix, &subsystem, &choices, dropNaiveSccs, onlyBottomSccs); + } template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, bool dropNaiveSccs, bool onlyBottomSccs) { diff --git a/src/storm/storage/StronglyConnectedComponentDecomposition.h b/src/storm/storage/StronglyConnectedComponentDecomposition.h index 5a9fa2cf4..7d244b914 100644 --- a/src/storm/storage/StronglyConnectedComponentDecomposition.h +++ b/src/storm/storage/StronglyConnectedComponentDecomposition.h @@ -78,7 +78,21 @@ namespace storm { * leaving the SCC), are kept. */ StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StateBlock const& block, bool dropNaiveSccs = false, bool onlyBottomSccs = false); - + + /* + * Creates an SCC decomposition of the given subsystem in the given system (whose transition relation is + * given by a sparse matrix). + * + * @param transitionMatrix The transition matrix of the system to decompose. + * @param block The block to decompose into SCCs. + * @param choices A bit vector indicating which choices of the states are contained in the subsystem. + * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state + * without a self-loop) are to be kept in the decomposition. + * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of + * leaving the SCC), are kept. + */ + StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StateBlock const& block, storm::storage::BitVector const& choices, bool dropNaiveSccs = false, bool onlyBottomSccs = false); + /* * Creates an SCC decomposition of the given system (whose transition relation is given by a sparse matrix). * diff --git a/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp b/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp index a7c23edf3..6e9718e6b 100644 --- a/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp +++ b/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp @@ -3,7 +3,11 @@ #include "storm/parser/AutoParser.h" #include "storm/storage/MaximalEndComponentDecomposition.h" #include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" +#include "storm/builder/ExplicitModelBuilder.h" +#include "storm/storage/SymbolicModelDescription.h" +#include "storm/parser/PrismParser.h" TEST(MaximalEndComponentDecomposition, FullSystem1) { std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/tiny1.tra", STORM_TEST_RESOURCES_DIR "/lab/tiny1.lab", "", ""); @@ -133,3 +137,42 @@ TEST(MaximalEndComponentDecomposition, Subsystem) { ASSERT_TRUE(false); } } + +TEST(MaximalEndComponentDecomposition, Example1) { + std::string prismModelPath = STORM_TEST_RESOURCES_DIR "/mdp/prism-mec-example1.nm"; + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(prismModelPath); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); + std::shared_ptr> mdp = model->as>(); + + storm::storage::MaximalEndComponentDecomposition mecDecomposition(*mdp); + + EXPECT_EQ(mecDecomposition.size(), 2); + + ASSERT_TRUE(mecDecomposition[0].getStateSet() == storm::storage::MaximalEndComponent::set_type{2}); + EXPECT_TRUE(mecDecomposition[0].getChoicesForState(2) == storm::storage::MaximalEndComponent::set_type{3}); + + ASSERT_TRUE(mecDecomposition[1].getStateSet() == storm::storage::MaximalEndComponent::set_type{0}); + EXPECT_TRUE(mecDecomposition[1].getChoicesForState(0) == storm::storage::MaximalEndComponent::set_type{0}); +} + +TEST(MaximalEndComponentDecomposition, Example2) { + std::string prismModelPath = STORM_TEST_RESOURCES_DIR "/mdp/prism-mec-example2.nm"; + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(prismModelPath); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); + std::shared_ptr> mdp = model->as>(); + + storm::storage::MaximalEndComponentDecomposition mecDecomposition(*mdp); + + EXPECT_EQ(mecDecomposition.size(), 2); + + ASSERT_TRUE(mecDecomposition[0].getStateSet() == storm::storage::MaximalEndComponent::set_type{2}); + EXPECT_TRUE(mecDecomposition[0].getChoicesForState(2) == storm::storage::MaximalEndComponent::set_type{4}); + + ASSERT_TRUE((mecDecomposition[1].getStateSet() == storm::storage::MaximalEndComponent::set_type{0, 1})); + EXPECT_TRUE((mecDecomposition[1].getChoicesForState(0) == storm::storage::MaximalEndComponent::set_type{0, 1})); + EXPECT_TRUE((mecDecomposition[1].getChoicesForState(1) == storm::storage::MaximalEndComponent::set_type{3})); +}