diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp index a0d14de9d..56ebbd34c 100644 --- a/src/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storage/MaximalEndComponentDecomposition.cpp @@ -64,7 +64,7 @@ namespace storm { // FIXME: As soon as gcc provides an erase(const_iterator) method, change this iterator back to a const_iterator. for (std::list::iterator mecIterator = endComponentStateSets.begin(); mecIterator != endComponentStateSets.end();) { StateBlock const& mec = *mecIterator; - + // Keep track of whether the MEC changed during this iteration. bool mecChanged = false; @@ -73,7 +73,7 @@ namespace storm { // 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(); + mecChanged |= sccs.size() > 1 || (sccs.size() > 0 && 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) { @@ -115,7 +115,7 @@ namespace storm { // Now check which states should be reconsidered, because successors of them were removed. statesToCheck.clear(); for (auto state : statesToRemove) { - for (auto const& entry : transitionMatrix.getRow(state)) { + for (auto const& entry : backwardTransitions.getRow(state)) { if (scc.find(entry.first) != scc.end()) { statesToCheck.set(entry.first); } @@ -142,7 +142,7 @@ namespace storm { } } // End of loop over all MEC candidates. - + // Now that we computed the underlying state sets of the MECs, we need to properly identify the choices // contained in the MEC and store them as actual MECs. this->blocks.reserve(endComponentStateSets.size()); diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index b7bd88dd2..6e9f08386 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -94,12 +94,6 @@ namespace storm { statesWithSelfloop = storm::storage::BitVector(lowlinks.size()); } - // Store a bit vector of all states that can leave their SCC to be able to detect bottom SCCs. - storm::storage::BitVector statesThatCanLeaveTheirScc; - if (onlyBottomSccs) { - statesThatCanLeaveTheirScc = storm::storage::BitVector(lowlinks.size()); - } - // Initialize the recursion stacks with the given initial state (and its successor iterator). recursionStateStack.push_back(startState); recursionIteratorStack.push_back(model.getRows(startState).begin()); @@ -144,18 +138,9 @@ namespace storm { recursionStepBackward: lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[successorIt->first]); - - // If we are interested in bottom SCCs only, we need to check whether the current state - // can leave the SCC. - if (onlyBottomSccs && lowlinks[currentState] != lowlinks[successorIt->first]) { - statesThatCanLeaveTheirScc.set(currentState); - } } else if (tarjanStackStates.get(successorIt->first)) { // Update the lowlink of the current state. lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[successorIt->first]); - - // Since it is known that in this case, the successor state is in the same SCC as the - // current state we don't need to update the bit vector of states that can leave their SCC. } } } @@ -166,7 +151,6 @@ namespace storm { Block scc; uint_fast64_t lastState = 0; - bool isBottomScc = true; do { // Pop topmost state from the algorithm's stack. lastState = tarjanStack.back(); @@ -175,12 +159,20 @@ namespace storm { // Add the state to the current SCC. scc.insert(lastState); - - if (onlyBottomSccs && isBottomScc && statesThatCanLeaveTheirScc.get(lastState)) { - isBottomScc = false; - } } while (lastState != currentState); - + + bool isBottomScc = true; + if (onlyBottomSccs) { + for (auto const& state : scc) { + for (auto const& successor : model.getRows(state)) { + if (scc.find(successor.first) == scc.end()) { + isBottomScc = false; + break; + } + } + } + } + // Now determine whether we want to keep this SCC in the decomposition. // First, we need to check whether we should drop the SCC because of the requirement to not include // naive SCCs. diff --git a/test/functional/storage/MaximalEndComponentDecompositionTest.cpp b/test/functional/storage/MaximalEndComponentDecompositionTest.cpp index 189a2ab26..cacb33843 100644 --- a/test/functional/storage/MaximalEndComponentDecompositionTest.cpp +++ b/test/functional/storage/MaximalEndComponentDecompositionTest.cpp @@ -3,7 +3,7 @@ #include "src/parser/AutoParser.h" #include "src/storage/MaximalEndComponentDecomposition.h" -TEST(MaximalEndComponentDecomposition, FullSystem) { +TEST(MaximalEndComponentDecomposition, FullSystem1) { 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>(); @@ -71,6 +71,35 @@ TEST(MaximalEndComponentDecomposition, FullSystem) { } } +TEST(MaximalEndComponentDecomposition, FullSystem2) { + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.lab", "", ""); + + std::shared_ptr> markovAutomaton = parser.getModel>(); + + storm::storage::MaximalEndComponentDecomposition mecDecomposition; + ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition(*markovAutomaton)); + + ASSERT_EQ(1, 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(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 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", "", ""); @@ -85,8 +114,6 @@ TEST(MaximalEndComponentDecomposition, 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)); diff --git a/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp b/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp new file mode 100644 index 000000000..22f04d0d1 --- /dev/null +++ b/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp @@ -0,0 +1,46 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/parser/AutoParser.h" +#include "src/storage/StronglyConnectedComponentDecomposition.h" + +TEST(StronglyConnectedComponentDecomposition, FullSystem1) { + 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::StronglyConnectedComponentDecomposition sccDecomposition; + + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*markovAutomaton)); + ASSERT_EQ(5, sccDecomposition.size()); + + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*markovAutomaton, true)); + ASSERT_EQ(2, sccDecomposition.size()); + + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*markovAutomaton, true, true)); + ASSERT_EQ(2, sccDecomposition.size()); + + markovAutomaton = nullptr; +} + +TEST(StronglyConnectedComponentDecomposition, FullSystem2) { + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.lab", "", ""); + std::shared_ptr> markovAutomaton = parser.getModel>(); + + storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*markovAutomaton, true, false)); + + ASSERT_EQ(sccDecomposition.size(), 2); + + // Now, because there is no ordering we have to check the contents of the MECs in a symmetrical way. + storm::storage::StateBlock const& scc1 = sccDecomposition[0]; + storm::storage::StateBlock const& scc2 = sccDecomposition[1]; + + std::vector correctScc1 = {1, 3, 8, 9, 10}; + std::vector correctScc2 = {4, 5, 6, 7}; + ASSERT_TRUE(scc1 == storm::storage::StateBlock(correctScc1.begin(), correctScc1.end()) || scc1 == storm::storage::StateBlock(correctScc2.begin(), correctScc2.end())); + ASSERT_TRUE(scc2 == storm::storage::StateBlock(correctScc1.begin(), correctScc1.end()) || scc2 == storm::storage::StateBlock(correctScc2.begin(), correctScc2.end())); + + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*markovAutomaton, true, true)); + ASSERT_EQ(1, sccDecomposition.size()); + + markovAutomaton = nullptr; +} diff --git a/test/performance/graph/GraphTest.cpp b/test/performance/graph/GraphTest.cpp index 6bc0042b5..b3355c398 100644 --- a/test/performance/graph/GraphTest.cpp +++ b/test/performance/graph/GraphTest.cpp @@ -86,74 +86,4 @@ TEST(GraphTest, PerformProb01MinMax) { ASSERT_EQ(prob01.second.getNumberOfSetBits(), 63616ull); mdp2 = nullptr; -} - -TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) { - storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); - std::shared_ptr> dtmc = parser.getModel>(); - - LOG4CPLUS_WARN(logger, "Computing SCC decomposition of crowds/crowds20_5..."); - storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(*dtmc); - LOG4CPLUS_WARN(logger, "Done."); - - ASSERT_EQ(sccDecomposition.size(), 1290297ull); - - LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of crowds/crowds20_5..."); - storm::storage::SparseMatrix sccDependencyGraph(std::move(dtmc->extractPartitionDependencyGraph(sccDecomposition))); - LOG4CPLUS_WARN(logger, "Done."); - - ASSERT_EQ(sccDependencyGraph.getEntryCount(), 1371253ull); - - dtmc = nullptr; - - storm::parser::AutoParser parser2(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", ""); - std::shared_ptr> dtmc2 = parser2.getModel>(); - - LOG4CPLUS_WARN(logger, "Computing SCC decomposition of synchronous_leader/leader6_8..."); - sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*dtmc2); - LOG4CPLUS_WARN(logger, "Done."); - - ASSERT_EQ(sccDecomposition.size(), 1279673ull); - - LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of synchronous_leader/leader6_8..."); - sccDependencyGraph = std::move(dtmc2->extractPartitionDependencyGraph(sccDecomposition)); - LOG4CPLUS_WARN(logger, "Done."); - - ASSERT_EQ(sccDependencyGraph.getEntryCount(), 1535367ull); - - dtmc2 = nullptr; - - storm::parser::AutoParser parser3(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader6.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader6.lab", "", ""); - std::shared_ptr> mdp = parser3.getModel>(); - - LOG4CPLUS_WARN(logger, "Computing SCC decomposition of asynchronous_leader/leader6..."); - sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*mdp); - LOG4CPLUS_WARN(logger, "Done."); - - ASSERT_EQ(sccDecomposition.size(), 146844ull); - - LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of asynchronous_leader/leader6..."); - sccDependencyGraph = std::move(mdp->extractPartitionDependencyGraph(sccDecomposition)); - LOG4CPLUS_WARN(logger, "Done."); - - ASSERT_EQ(sccDependencyGraph.getEntryCount(), 489918ull); - - mdp = nullptr; - - storm::parser::AutoParser parser4(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", "", ""); - std::shared_ptr> mdp2 = parser4.getModel>(); - - LOG4CPLUS_WARN(logger, "Computing SCC decomposition of consensus/coin4_6..."); - sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*mdp2); - LOG4CPLUS_WARN(logger, "Done."); - - ASSERT_EQ(sccDecomposition.size(), 2611ull); - - LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of consensus/coin4_6..."); - sccDependencyGraph = std::move(mdp2->extractPartitionDependencyGraph(sccDecomposition)); - LOG4CPLUS_WARN(logger, "Done."); - - ASSERT_EQ(sccDependencyGraph.getEntryCount(), 7888ull); - - mdp2 = nullptr; -} +} \ No newline at end of file diff --git a/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp b/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp new file mode 100644 index 000000000..30bfd5734 --- /dev/null +++ b/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp @@ -0,0 +1,48 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/parser/AutoParser.h" +#include "src/storage/StronglyConnectedComponentDecomposition.h" + +TEST(StronglyConnectedComponentDecomposition, Crowds) { + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); + std::shared_ptr> dtmc = parser.getModel>(); + + storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*dtmc)); + + ASSERT_EQ(sccDecomposition.size(), 1290297ull); + dtmc = nullptr; +} + +TEST(StronglyConnectedComponentDecomposition, SynchronousLeader) { + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", ""); + std::shared_ptr> dtmc = parser.getModel>(); + + storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*dtmc)); + + ASSERT_EQ(sccDecomposition.size(), 1279673ull); + dtmc = nullptr; +} + +TEST(StronglyConnectedComponentDecomposition, AsynchronousLeader) { + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader6.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader6.lab", "", ""); + std::shared_ptr> mdp = parser.getModel>(); + + storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*mdp)); + + ASSERT_EQ(sccDecomposition.size(), 146844ull); + mdp = nullptr; +} + +TEST(StronglyConnectedComponentDecomposition, Consensus) { + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", "", ""); + std::shared_ptr> mdp = parser.getModel>(); + + storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*mdp)); + + ASSERT_EQ(sccDecomposition.size(), 2611ull); + mdp = nullptr; +} \ No newline at end of file