Fixed SCC decomposition. Added functional tests for SCC decomposition.

Former-commit-id: 25a7805fcb

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<StateBlock>::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());

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.

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<double> parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.lab", "", "");
 
     std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = parser.getModel<storm::models::MarkovAutomaton<double>>();
@@ -71,6 +71,35 @@ TEST(MaximalEndComponentDecomposition, FullSystem) {
     }
 }
 
+TEST(MaximalEndComponentDecomposition, FullSystem2) {
+    storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.lab", "", "");
+    
+    std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = parser.getModel<storm::models::MarkovAutomaton<double>>();
+    
+    storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition;
+    ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition<double>(*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<double> 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));

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<double> parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.lab", "", "");
+	std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = parser.getModel<storm::models::MarkovAutomaton<double>>();
+    
+    storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
+
+    ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*markovAutomaton));
+    ASSERT_EQ(5, sccDecomposition.size());
+    
+    ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*markovAutomaton, true));
+    ASSERT_EQ(2, sccDecomposition.size());
+
+    ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*markovAutomaton, true, true));
+    ASSERT_EQ(2, sccDecomposition.size());
+    
+    markovAutomaton = nullptr;
+}
+
+TEST(StronglyConnectedComponentDecomposition, FullSystem2) {
+    storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.lab", "", "");
+	std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = parser.getModel<storm::models::MarkovAutomaton<double>>();
+    
+    storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
+    ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*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<uint_fast64_t> correctScc1 = {1, 3, 8, 9, 10};
+    std::vector<uint_fast64_t> 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<double>(*markovAutomaton, true, true));
+    ASSERT_EQ(1, sccDecomposition.size());
+
+    markovAutomaton = nullptr;
+}

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<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
-	std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
-    
-    LOG4CPLUS_WARN(logger, "Computing SCC decomposition of crowds/crowds20_5...");
-    storm::storage::StronglyConnectedComponentDecomposition<double> 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<double> sccDependencyGraph(std::move(dtmc->extractPartitionDependencyGraph(sccDecomposition)));
-    LOG4CPLUS_WARN(logger, "Done.");
-    
-    ASSERT_EQ(sccDependencyGraph.getEntryCount(), 1371253ull);
-    
-    dtmc = nullptr;
-    
-    storm::parser::AutoParser<double> 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<storm::models::Dtmc<double>> dtmc2 = parser2.getModel<storm::models::Dtmc<double>>();
-
-    LOG4CPLUS_WARN(logger, "Computing SCC decomposition of synchronous_leader/leader6_8...");
-    sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*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<double> parser3(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader6.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader6.lab", "", "");
-	std::shared_ptr<storm::models::Mdp<double>> mdp = parser3.getModel<storm::models::Mdp<double>>();
-    
-    LOG4CPLUS_WARN(logger, "Computing SCC decomposition of asynchronous_leader/leader6...");
-    sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*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<double> parser4(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", "", "");
-	std::shared_ptr<storm::models::Mdp<double>> mdp2 = parser4.getModel<storm::models::Mdp<double>>();
-
-    LOG4CPLUS_WARN(logger, "Computing SCC decomposition of consensus/coin4_6...");
-    sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*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;
-}
+}

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<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
+	std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
+    
+    storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
+    ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc));
+    
+    ASSERT_EQ(sccDecomposition.size(), 1290297ull);
+    dtmc = nullptr;
+}
+
+TEST(StronglyConnectedComponentDecomposition, SynchronousLeader) {
+    storm::parser::AutoParser<double> 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<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
+    
+    storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
+    ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc));
+
+    ASSERT_EQ(sccDecomposition.size(), 1279673ull);
+    dtmc = nullptr;
+}
+
+TEST(StronglyConnectedComponentDecomposition, AsynchronousLeader) {
+    storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader6.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader6.lab", "", "");
+	std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
+    
+    storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
+    ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp));
+    
+    ASSERT_EQ(sccDecomposition.size(), 146844ull);
+    mdp = nullptr;
+}
+
+TEST(StronglyConnectedComponentDecomposition, Consensus) {
+    storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", "", "");
+	std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
+    
+    storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
+    ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp));
+    
+    ASSERT_EQ(sccDecomposition.size(), 2611ull);
+    mdp = nullptr;
+}