Added correct detection of states that possess infinite exptected time to reach a given goal set.

Former-commit-id: 4bc605d89d

src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h

@@ -6,7 +6,9 @@
 #include "src/modelchecker/csl/AbstractModelChecker.h"
 #include "src/models/MarkovAutomaton.h"
 #include "src/storage/BitVector.h"
+#include "src/storage/MaximalEndComponentDecomposition.h"
 #include "src/solver/AbstractNondeterministicLinearEquationSolver.h"
+#include "src/utility/graph.h"
 #include "src/exceptions/NotImplementedException.h"
 
 namespace storm {
@@ -69,8 +71,55 @@ namespace storm {
                     // TODO: check whether the Markov automaton is closed once again? Or should that rather be done when constructing the model checker?
                     // For now we just assume that it is closed already.
 
-                    // Start by identifying the states for which values need to be computed.
-                    storm::storage::BitVector maybeStates = ~goalStates;
+                    // First, we need to check which states have infinite expected time (by definition).
+                    storm::storage::BitVector infinityStates;
+                    if (min) {
+                        // If we need to compute the minimum expected times, we have to set the values of those states to infinity that, under all schedulers,
+                        // reach a bottom SCC without a goal state.
+                        
+                        // So we start by computing all bottom SCCs without goal states.
+                        storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition(this->getModel(), ~goalStates, true, true);
+                        
+                        // Now form the union of all these SCCs.
+                        storm::storage::BitVector unionOfNonGoalBSccs(this->getModel().getNumberOfStates());
+                        for (auto const& scc : sccDecomposition) {
+                            for (auto state : scc) {
+                                unionOfNonGoalBSccs.set(state);
+                            }
+                        }
+                        
+                        // Finally, if this union is non-empty, compute the states such that all schedulers reach some state of the union.
+                        if (!unionOfNonGoalBSccs.empty()) {
+                            infinityStates = storm::utility::graph::performProbGreater0A(this->getModel(), this->getModel().getBackwardTransitions(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), unionOfNonGoalBSccs);
+                        } else {
+                            // Otherwise, we have no infinity states.
+                            infinityStates = storm::storage::BitVector(this->getModel().getNumberOfStates());
+                        }
+                    } else {
+                        // If we maximize the property, the expected time of a state is infinite, if an end-component without any goal state is reachable.
+                        
+                        // So we start by computing all MECs that have no goal state.
+                        storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition(this->getModel(), ~goalStates);
+                        
+                        // Now we form the union of all states in these end components.
+                        storm::storage::BitVector unionOfNonGoalMaximalEndComponents(this->getModel().getNumberOfStates());
+                        for (auto const& mec : mecDecomposition) {
+                            for (auto const& stateActionPair : mec) {
+                                unionOfNonGoalMaximalEndComponents.set(stateActionPair.first);
+                            }
+                        }
+                        
+                        if (!unionOfNonGoalMaximalEndComponents.empty()) {
+                            // Now we need to check for which states there exists a scheduler that reaches one of the previously computed states.
+                            infinityStates = storm::utility::graph::performProbGreater0E(this->getModel(), this->getModel().getBackwardTransitions(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), unionOfNonGoalMaximalEndComponents);
+                        } else {
+                            // Otherwise, we have no infinity states.
+                            infinityStates = storm::storage::BitVector(this->getModel().getNumberOfStates());
+                        }
+                    }
+
+                    // Now we identify the states for which values need to be computed.
+                    storm::storage::BitVector maybeStates = ~(goalStates | infinityStates);
                     
                     // Then, we can eliminate the rows and columns for all states whose values are already known to be 0.
                     std::vector<ValueType> x(maybeStates.getNumberOfSetBits());
@@ -97,8 +146,11 @@ namespace storm {
                     // Create resulting vector.
                     std::vector<ValueType> result(this->getModel().getNumberOfStates());
 
-                    // Set values of resulting vector according to previous result (goal states will have a value of 0) and return the result.
+                    // Set values of resulting vector according to previous result and return the result.
                     storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, x);
+                    storm::utility::vector::setVectorValues(result, goalStates, storm::utility::constGetZero<ValueType>());
+                    storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::constGetInfinity<ValueType>());
+
                     return result;
                 }
                 

src/models/MarkovAutomaton.h

@@ -263,15 +263,12 @@ namespace storm {
              * the rates into the corresponding probabilities by dividing each entry by the exit rate of the state.
              */
             void turnRatesToProbabilities() {
-                std::cout << this->transitionMatrix.toString() << std::endl;
                 for (auto state : this->markovianStates) {
                     for (typename storm::storage::SparseMatrix<T>::ValueIterator valIt = this->transitionMatrix.valueIteratorBegin(this->getNondeterministicChoiceIndices()[state]), valIte = this->transitionMatrix.valueIteratorEnd(this->getNondeterministicChoiceIndices()[state]); valIt != valIte; ++valIt) {
                         *valIt = *valIt / this->exitRates[state];
                     }
                 }
-                std::cout << this->transitionMatrix.toString() << std::endl;
             }
-
                     
             storm::storage::BitVector markovianStates;
 			std::vector<T> exitRates;

src/storage/MaximalEndComponent.cpp

@@ -102,6 +102,22 @@ namespace storm {
             out << "}";
             
             return out;
-        }        
+        }
+        
+        MaximalEndComponent::iterator MaximalEndComponent::begin() {
+            return stateToChoicesMapping.begin();
+        }
+        
+        MaximalEndComponent::iterator MaximalEndComponent::end() {
+            return stateToChoicesMapping.end();
+        }
+        
+        MaximalEndComponent::const_iterator MaximalEndComponent::begin() const {
+            return stateToChoicesMapping.begin();
+        }
+        
+        MaximalEndComponent::const_iterator MaximalEndComponent::end() const {
+            return stateToChoicesMapping.end();
+        }
     }
 }

src/storage/MaximalEndComponent.h

@@ -12,6 +12,9 @@ namespace storm {
          */
         class MaximalEndComponent {
         public:
+            typedef std::unordered_map<uint_fast64_t, storm::storage::VectorSet<uint_fast64_t>>::iterator iterator;
+            typedef std::unordered_map<uint_fast64_t, storm::storage::VectorSet<uint_fast64_t>>::const_iterator const_iterator;
+            
             /*!
              * Creates an empty MEC.
              */
@@ -89,6 +92,14 @@ namespace storm {
              */
             storm::storage::VectorSet<uint_fast64_t> getStateSet() const;
             
+            iterator begin();
+            
+            iterator end();
+            
+            const_iterator begin() const;
+            
+            const_iterator end() const;
+            
             friend std::ostream& operator<<(std::ostream& out, MaximalEndComponent const& component);
             
         private:

src/storage/MaximalEndComponentDecomposition.cpp

@@ -13,7 +13,12 @@ namespace storm {
         
         template<typename ValueType>
         MaximalEndComponentDecomposition<ValueType>::MaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel<ValueType> const& model) {
-            performMaximalEndComponentDecomposition(model);
+            performMaximalEndComponentDecomposition(model, storm::storage::BitVector(model.getNumberOfStates(), true));
+        }
+        
+        template<typename ValueType>
+        MaximalEndComponentDecomposition<ValueType>::MaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel<ValueType> const& model, storm::storage::BitVector const& subsystem) {
+            performMaximalEndComponentDecomposition(model, subsystem);
         }
         
         template<typename ValueType>
@@ -39,7 +44,7 @@ namespace storm {
         }
         
         template <typename ValueType>
-        void MaximalEndComponentDecomposition<ValueType>::performMaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel<ValueType> const& model) {
+        void MaximalEndComponentDecomposition<ValueType>::performMaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel<ValueType> const& model, storm::storage::BitVector const& subsystem) {
             // Get some references for convenient access.
             storm::storage::SparseMatrix<bool> backwardTransitions = model.getBackwardTransitions();
             std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
@@ -47,12 +52,12 @@ namespace storm {
             
             // Initialize the maximal end component list to be the full state space.
             std::list<StateBlock> endComponentStateSets;
-            endComponentStateSets.emplace_back(0, model.getNumberOfStates());
+            endComponentStateSets.emplace_back(subsystem);
             storm::storage::BitVector statesToCheck(model.getNumberOfStates());
             
             for (std::list<StateBlock>::const_iterator mecIterator = endComponentStateSets.begin(); mecIterator != endComponentStateSets.end();) {
                 StateBlock const& mec = *mecIterator;
-                
+
                 // Keep track of whether the MEC changed during this iteration.
                 bool mecChanged = false;
                 
@@ -110,13 +115,14 @@ namespace storm {
                 
                 // If the MEC changed, we delete it from the list of MECs and append the possible new MEC candidates to the list instead.
                 if (mecChanged) {
-                    std::list<StateBlock>::const_iterator eraseIterator(mecIterator);
                     for (StateBlock& scc : sccs) {
                         if (!scc.empty()) {
                             endComponentStateSets.push_back(std::move(scc));
-                            ++mecIterator;
                         }
                     }
+
+                    std::list<StateBlock>::const_iterator eraseIterator(mecIterator);
+                    ++mecIterator;
                     endComponentStateSets.erase(eraseIterator);
                 } else {
                     // Otherwise, we proceed with the next MEC candidate.

src/storage/MaximalEndComponentDecomposition.h

@@ -24,6 +24,8 @@ namespace storm  {
              */
             MaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel<ValueType> const& model);
             
+            MaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel<ValueType> const& model, storm::storage::BitVector const& subsystem);
+            
             MaximalEndComponentDecomposition(MaximalEndComponentDecomposition const& other);
             
             MaximalEndComponentDecomposition& operator=(MaximalEndComponentDecomposition const& other);
@@ -39,7 +41,7 @@ namespace storm  {
              *
              * @param model The model to decompose.
              */
-            void performMaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel<ValueType> const& model);
+            void performMaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel<ValueType> const& model, storm::storage::BitVector const& subsystem);
         };
     }
 }

src/storage/StronglyConnectedComponentDecomposition.cpp

@@ -9,14 +9,19 @@ namespace storm {
         }
 
         template <typename ValueType>
-        StronglyConnectedComponentDecomposition<ValueType>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, bool dropNaiveSccs) : Decomposition() {
-            performSccDecomposition(model, dropNaiveSccs);
+        StronglyConnectedComponentDecomposition<ValueType>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, bool dropNaiveSccs, bool onlyBottomSccs) : Decomposition() {
+            performSccDecomposition(model, dropNaiveSccs, onlyBottomSccs);
         }
         
         template <typename ValueType>
-        StronglyConnectedComponentDecomposition<ValueType>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, StateBlock const& block, bool dropNaiveSccs) {
+        StronglyConnectedComponentDecomposition<ValueType>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs) {
             storm::storage::BitVector subsystem(model.getNumberOfStates(), block);
-            performSccDecomposition(model, subsystem, dropNaiveSccs);
+            performSccDecomposition(model, subsystem, dropNaiveSccs, onlyBottomSccs);
+        }
+        
+        template <typename ValueType>
+        StronglyConnectedComponentDecomposition<ValueType>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) {
+            performSccDecomposition(model, subsystem, dropNaiveSccs, onlyBottomSccs);
         }
         
         template <typename ValueType>
@@ -42,7 +47,7 @@ namespace storm {
         }
         
         template <typename ValueType>
-        void StronglyConnectedComponentDecomposition<ValueType>::performSccDecomposition(storm::models::AbstractModel<ValueType> const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs) {
+        void StronglyConnectedComponentDecomposition<ValueType>::performSccDecomposition(storm::models::AbstractModel<ValueType> const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) {
             LOG4CPLUS_INFO(logger, "Computing SCC decomposition.");
             
             uint_fast64_t numberOfStates = model.getNumberOfStates();
@@ -59,7 +64,7 @@ namespace storm {
             uint_fast64_t currentIndex = 0;
             for (auto state : subsystem) {
                 if (!visitedStates.get(state)) {
-                    performSccDecompositionHelper(model, state, subsystem, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, dropNaiveSccs);
+                    performSccDecompositionHelper(model, state, subsystem, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, dropNaiveSccs, onlyBottomSccs);
                 }
             }
             
@@ -68,18 +73,18 @@ namespace storm {
 
         
         template <typename ValueType>
-        void StronglyConnectedComponentDecomposition<ValueType>::performSccDecomposition(storm::models::AbstractModel<ValueType> const& model, bool dropNaiveSccs) {
+        void StronglyConnectedComponentDecomposition<ValueType>::performSccDecomposition(storm::models::AbstractModel<ValueType> const& model, bool dropNaiveSccs, bool onlyBottomSccs) {
             uint_fast64_t numberOfStates = model.getNumberOfStates();
 
             // Prepare a block that contains all states for a call to the other overload of this function.
             storm::storage::BitVector fullSystem(numberOfStates, true);
             
             // Call the overloaded function.
-            performSccDecomposition(model, fullSystem, dropNaiveSccs);
+            performSccDecomposition(model, fullSystem, dropNaiveSccs, onlyBottomSccs);
         }
         
         template <typename ValueType>
-        void StronglyConnectedComponentDecomposition<ValueType>::performSccDecompositionHelper(storm::models::AbstractModel<ValueType> const& model, uint_fast64_t startState, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, std::vector<uint_fast64_t>& stateIndices, std::vector<uint_fast64_t>& lowlinks, std::vector<uint_fast64_t>& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, bool dropNaiveSccs) {
+        void StronglyConnectedComponentDecomposition<ValueType>::performSccDecompositionHelper(storm::models::AbstractModel<ValueType> const& model, uint_fast64_t startState, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, std::vector<uint_fast64_t>& stateIndices, std::vector<uint_fast64_t>& lowlinks, std::vector<uint_fast64_t>& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, bool dropNaiveSccs, bool onlyBottomSccs) {
             // Create the stacks needed for turning the recursive formulation of Tarjan's algorithm
             // into an iterative version. In particular, we keep one stack for states and one stack
             // for the iterators. The last one is not strictly needed, but reduces iteration work when
@@ -91,7 +96,16 @@ namespace storm {
             std::vector<bool> statesInStack(lowlinks.size());
             
             // Store a bit vector of all states with a self-loop to be able to detect non-trivial SCCs with only one state.
-            storm::storage::BitVector statesWithSelfloop(lowlinks.size());
+            storm::storage::BitVector statesWithSelfloop;
+            if (dropNaiveSccs) {
+                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);
@@ -112,33 +126,45 @@ namespace storm {
                 
                 // Now, traverse all successors of the current state.
                 for(; successorIt != model.getRows(currentState).end(); ++successorIt) {
-                    // Record if the current state has a self-loop.
-                    if (currentState == successorIt.column()) {
+                    // Record if the current state has a self-loop if we are to drop naive SCCs later.
+                    if (dropNaiveSccs && currentState == successorIt.column()) {
                         statesWithSelfloop.set(currentState, true);
                     }
                     
                     // If we have not visited the successor already, we need to perform the procedure
-                    // recursively on the newly found state.
-                    if (!visitedStates.get(successorIt.column()) && subsystem.get(successorIt.column())) {
-                        // Save current iterator position so we can continue where we left off later.
-                        recursionIteratorStack.pop_back();
-                        recursionIteratorStack.push_back(successorIt);
-                        
-                        // Put unvisited successor on top of our recursion stack and remember that.
-                        recursionStateStack.push_back(successorIt.column());
-                        statesInStack[successorIt.column()] = true;
-                        
-                        // Also, put initial value for iterator on corresponding recursion stack.
-                        recursionIteratorStack.push_back(model.getRows(successorIt.column()).begin());
-                        
-                        // Perform the actual recursion step in an iterative way.
-                        goto recursionStepForward;
-                        
-                    recursionStepBackward:
-                        lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[successorIt.column()]);
-                    } else if (tarjanStackStates.get(successorIt.column())) {
-                        // Update the lowlink of the current state.
-                        lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[successorIt.column()]);
+                    // recursively on the newly found state, but only if it belongs to the subsystem in
+                    // which we are interested.
+                    if (subsystem.get(successorIt.column())) {
+                        if (!visitedStates.get(successorIt.column())) {
+                            // Save current iterator position so we can continue where we left off later.
+                            recursionIteratorStack.pop_back();
+                            recursionIteratorStack.push_back(successorIt);
+                            
+                            // Put unvisited successor on top of our recursion stack and remember that.
+                            recursionStateStack.push_back(successorIt.column());
+                            statesInStack[successorIt.column()] = true;
+                            
+                            // Also, put initial value for iterator on corresponding recursion stack.
+                            recursionIteratorStack.push_back(model.getRows(successorIt.column()).begin());
+                            
+                            // Perform the actual recursion step in an iterative way.
+                            goto recursionStepForward;
+                            
+                        recursionStepBackward:
+                            lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[successorIt.column()]);
+                            
+                            // 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.column()]) {
+                                statesThatCanLeaveTheirScc.set(currentState);
+                            }
+                        } else if (tarjanStackStates.get(successorIt.column())) {
+                            // Update the lowlink of the current state.
+                            lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[successorIt.column()]);
+                            
+                            // 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.
+                        }
                     }
                 }
                 
@@ -148,6 +174,7 @@ namespace storm {
                     Block scc;
                     
                     uint_fast64_t lastState = 0;
+                    bool isBottomScc = true;
                     do {
                         // Pop topmost state from the algorithm's stack.
                         lastState = tarjanStack.back();
@@ -156,10 +183,20 @@ namespace storm {
                         
                         // Add the state to the current SCC.
                         scc.insert(lastState);
+                        
+                        if (onlyBottomSccs && isBottomScc && statesThatCanLeaveTheirScc.get(lastState)) {
+                            isBottomScc = false;
+                        }
                     } while (lastState != currentState);
                     
-                    // Only add the SCC if it is non-trivial if the corresponding flag was set.
-                    if (!dropNaiveSccs || scc.size() > 1 || statesWithSelfloop.get(*scc.begin())) {
+                    // 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.
+                    bool keepScc = !dropNaiveSccs || (scc.size() > 1 || statesWithSelfloop.get(*scc.begin()));
+                    // Then, we also need to make sure that it is a bottom SCC if we were required to.
+                    keepScc &= !onlyBottomSccs || isBottomScc;
+                    
+                    // Only add the SCC if we determined to keep it, based on the given parameters.
+                    if (keepScc) {
                         this->blocks.emplace_back(std::move(scc));
                     }
                 }

src/storage/StronglyConnectedComponentDecomposition.h

@@ -32,7 +32,7 @@ namespace storm {
              * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state
              * are to be kept in the decomposition.
              */
-            StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, bool dropNaiveSccs = false);
+            StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, bool dropNaiveSccs = false, bool onlyBottomSccs = false);
 
             /*
              * Creates an SCC decomposition of given block in the given model.
@@ -42,7 +42,9 @@ namespace storm {
              * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state
              * are to be kept in the decomposition.
              */
-            StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, StateBlock const& block, bool dropNaiveSccs = false);
+            StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, StateBlock const& block, bool dropNaiveSccs = false, bool onlyBottomSccs = false);
+            
+            StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs = false, bool onlyBottomSccs = false);
             
             StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition const& other);
             
@@ -53,11 +55,11 @@ namespace storm {
             StronglyConnectedComponentDecomposition& operator=(StronglyConnectedComponentDecomposition&& other);
             
         private:
-            void performSccDecomposition(storm::models::AbstractModel<ValueType> const& model, bool dropNaiveSccs);
+            void performSccDecomposition(storm::models::AbstractModel<ValueType> const& model, bool dropNaiveSccs, bool onlyBottomSccs);
             
-            void performSccDecomposition(storm::models::AbstractModel<ValueType> const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs);
+            void performSccDecomposition(storm::models::AbstractModel<ValueType> const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs);
             
-            void performSccDecompositionHelper(storm::models::AbstractModel<ValueType> const& model, uint_fast64_t startState, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, std::vector<uint_fast64_t>& stateIndices, std::vector<uint_fast64_t>& lowlinks, std::vector<uint_fast64_t>& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, bool dropNaiveSccs);
+            void performSccDecompositionHelper(storm::models::AbstractModel<ValueType> const& model, uint_fast64_t startState, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, std::vector<uint_fast64_t>& stateIndices, std::vector<uint_fast64_t>& lowlinks, std::vector<uint_fast64_t>& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, bool dropNaiveSccs, bool onlyBottomSccs);
         };
     }
 }

src/storage/VectorSet.cpp

@@ -1,4 +1,5 @@
 #include "src/storage/VectorSet.h"
+#include "src/storage/BitVector.h"
 
 namespace storm {
     namespace storage {
@@ -25,6 +26,14 @@ namespace storm {
             }
         }
         
+        template<typename ValueType>
+        VectorSet<ValueType>::VectorSet(storm::storage::BitVector const& data) : dirty(false) {
+            this->data.reserve(data.getNumberOfSetBits());
+            for (auto element : data) {
+                this->data.push_back(element);
+            }
+        }
+        
         template<typename ValueType>
         VectorSet<ValueType>::VectorSet(uint_fast64_t from, uint_fast64_t to) : dirty(false) {
             data.reserve(to - from);

src/storage/VectorSet.h

@@ -19,6 +19,9 @@
 namespace storm  {
     namespace storage {
         
+        // Forward declare bit vector class.
+        class BitVector;
+        
         template<typename ValueType>
         class VectorSet {
         public:
@@ -37,6 +40,8 @@ namespace storm  {
             
             VectorSet(std::set<ValueType> const& data);
             
+            VectorSet(BitVector const& data);
+            
             VectorSet(uint_fast64_t from, uint_fast64_t to);
                         
             VectorSet(VectorSet const& other);

src/storm.cpp

@@ -24,6 +24,7 @@
 #include "src/models/Dtmc.h"
 #include "src/models/MarkovAutomaton.h"
 #include "src/storage/SparseMatrix.h"
+#include "src/storage/MaximalEndComponentDecomposition.h"
 #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"
 #include "src/models/AtomicPropositionsLabeling.h"
 #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
@@ -471,9 +472,9 @@ int main(const int argc, const char* argv[]) {
                     LOG4CPLUS_INFO(logger, "Model is a Markov automaton.");
                     std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = parser.getModel<storm::models::MarkovAutomaton<double>>();
                     markovAutomaton->close();
-                    
                     storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker<double> mc(*markovAutomaton, new storm::solver::AbstractNondeterministicLinearEquationSolver<double>());
-                    mc.checkExpectedTime(true, markovAutomaton->getLabeledStates("goal"));
+                    std::cout << mc.checkExpectedTime(true, markovAutomaton->getLabeledStates("goal")) << std::endl;
+                    std::cout << mc.checkExpectedTime(false, markovAutomaton->getLabeledStates("goal")) << std::endl;
                     
                     break;
                 }