diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp index 5955a58d3..a0d14de9d 100644 --- a/src/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storage/MaximalEndComponentDecomposition.cpp @@ -70,7 +70,10 @@ namespace storm { // Get an SCC decomposition of the current MEC candidate. StronglyConnectedComponentDecomposition sccs(model, mec, true); - mecChanged |= sccs.size() > 1; + + // 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. + mecChanged |= sccs.size() > 1 || sccs[0].size() < mec.size(); // Check for each of the SCCs whether there is at least one action for each state that does not leave the SCC. for (auto& scc : sccs) { diff --git a/src/storage/PartialScheduler.cpp b/src/storage/PartialScheduler.cpp index a3a0a20d9..6f004c315 100644 --- a/src/storage/PartialScheduler.cpp +++ b/src/storage/PartialScheduler.cpp @@ -9,7 +9,7 @@ namespace storm { } bool PartialScheduler::isChoiceDefined(uint_fast64_t state) const { - return stateToChoiceMapping.find(state) != choices.end(); + return stateToChoiceMapping.find(state) != stateToChoiceMapping.end(); } uint_fast64_t PartialScheduler::getChoice(uint_fast64_t state) const { diff --git a/test/functional/storage/MaximalEndComponentDecompositionTest.cpp b/test/functional/storage/MaximalEndComponentDecompositionTest.cpp new file mode 100644 index 000000000..189a2ab26 --- /dev/null +++ b/test/functional/storage/MaximalEndComponentDecompositionTest.cpp @@ -0,0 +1,106 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/parser/AutoParser.h" +#include "src/storage/MaximalEndComponentDecomposition.h" + +TEST(MaximalEndComponentDecomposition, FullSystem) { + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.lab", "", ""); + + std::shared_ptr> markovAutomaton = parser.getModel>(); + + storm::storage::MaximalEndComponentDecomposition mecDecomposition; + ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition(*markovAutomaton)); + + ASSERT_EQ(2, mecDecomposition.size()); + + // Now, because there is no ordering we have to check the contents of the MECs in a symmetrical way. + storm::storage::MaximalEndComponent const& mec1 = mecDecomposition[0]; + if (mec1.containsState(3)) { + ASSERT_TRUE(mec1.containsState(8)); + ASSERT_TRUE(mec1.containsState(9)); + ASSERT_TRUE(mec1.containsState(10)); + ASSERT_FALSE(mec1.containsState(0)); + ASSERT_FALSE(mec1.containsState(1)); + ASSERT_FALSE(mec1.containsState(2)); + ASSERT_FALSE(mec1.containsState(4)); + ASSERT_FALSE(mec1.containsState(5)); + ASSERT_FALSE(mec1.containsState(6)); + ASSERT_FALSE(mec1.containsState(7)); + } else if (mec1.containsState(4)) { + ASSERT_TRUE(mec1.containsState(5)); + ASSERT_TRUE(mec1.containsState(6)); + ASSERT_TRUE(mec1.containsState(7)); + ASSERT_FALSE(mec1.containsState(0)); + ASSERT_FALSE(mec1.containsState(1)); + ASSERT_FALSE(mec1.containsState(2)); + ASSERT_FALSE(mec1.containsState(3)); + ASSERT_FALSE(mec1.containsState(8)); + ASSERT_FALSE(mec1.containsState(9)); + ASSERT_FALSE(mec1.containsState(10)); + } else { + // This case must never happen as the only two existing MECs contain either 3 or 4. + ASSERT_TRUE(false); + } + + storm::storage::MaximalEndComponent const& mec2 = mecDecomposition[1]; + if (mec2.containsState(3)) { + ASSERT_TRUE(mec2.containsState(8)); + ASSERT_TRUE(mec2.containsState(9)); + ASSERT_TRUE(mec2.containsState(10)); + ASSERT_FALSE(mec2.containsState(0)); + ASSERT_FALSE(mec2.containsState(1)); + ASSERT_FALSE(mec2.containsState(2)); + ASSERT_FALSE(mec2.containsState(4)); + ASSERT_FALSE(mec2.containsState(5)); + ASSERT_FALSE(mec2.containsState(6)); + ASSERT_FALSE(mec2.containsState(7)); + } else if (mec2.containsState(4)) { + ASSERT_TRUE(mec2.containsState(5)); + ASSERT_TRUE(mec2.containsState(6)); + ASSERT_TRUE(mec2.containsState(7)); + ASSERT_FALSE(mec2.containsState(0)); + ASSERT_FALSE(mec2.containsState(1)); + ASSERT_FALSE(mec2.containsState(2)); + ASSERT_FALSE(mec2.containsState(3)); + ASSERT_FALSE(mec2.containsState(8)); + ASSERT_FALSE(mec2.containsState(9)); + ASSERT_FALSE(mec2.containsState(10)); + } else { + // This case must never happen as the only two existing MECs contain either 3 or 4. + ASSERT_TRUE(false); + } +} + +TEST(MaximalEndComponentDecomposition, Subsystem) { + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.lab", "", ""); + + std::shared_ptr> markovAutomaton = parser.getModel>(); + + storm::storage::BitVector subsystem(markovAutomaton->getNumberOfStates(), true); + subsystem.set(7, false); + + storm::storage::MaximalEndComponentDecomposition mecDecomposition; + ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition(*markovAutomaton, subsystem)); + + ASSERT_EQ(1, mecDecomposition.size()); + + storm::storage::MaximalEndComponent const& mec1 = mecDecomposition[0]; + + std::cout << mec1 << std::endl; + + if (mec1.containsState(3)) { + ASSERT_TRUE(mec1.containsState(8)); + ASSERT_TRUE(mec1.containsState(9)); + ASSERT_TRUE(mec1.containsState(10)); + ASSERT_FALSE(mec1.containsState(0)); + ASSERT_FALSE(mec1.containsState(1)); + ASSERT_FALSE(mec1.containsState(2)); + ASSERT_FALSE(mec1.containsState(4)); + ASSERT_FALSE(mec1.containsState(5)); + ASSERT_FALSE(mec1.containsState(6)); + ASSERT_FALSE(mec1.containsState(7)); + } else { + // This case must never happen as the only two existing MEC contains 3. + ASSERT_TRUE(false); + } +} \ No newline at end of file