Added proper source grouping for properties directory. Fixed one performance tests. Started on SCC-based reachability model checker.

Former-commit-id: e48c163783

CMakeLists.txt

@@ -240,11 +240,11 @@ file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm.cpp)
 set(STORM_SOURCES "${STORM_SOURCES_WITHOUT_MAIN};${STORM_MAIN_FILE}")
 file(GLOB_RECURSE STORM_ADAPTERS_FILES ${PROJECT_SOURCE_DIR}/src/adapters/*.h ${PROJECT_SOURCE_DIR}/src/adapters/*.cpp)
 file(GLOB_RECURSE STORM_EXCEPTIONS_FILES ${PROJECT_SOURCE_DIR}/src/exceptions/*.h ${PROJECT_SOURCE_DIR}/src/exceptions/*.cpp)
-file(GLOB STORM_FORMULA_FILES ${PROJECT_SOURCE_DIR}/src/formula/*.h ${PROJECT_SOURCE_DIR}/src/formula/*.cpp)
-file(GLOB_RECURSE STORM_FORMULA_ABSTRACT_FILES ${PROJECT_SOURCE_DIR}/src/formula/abstract/*.h ${PROJECT_SOURCE_DIR}/src/formula/abstract/*.cpp)
-file(GLOB_RECURSE STORM_FORMULA_CSL_FILES ${PROJECT_SOURCE_DIR}/src/formula/Csl/*.h ${PROJECT_SOURCE_DIR}/src/formula/Csl/*.cpp)
-file(GLOB_RECURSE STORM_FORMULA_LTL_FILES ${PROJECT_SOURCE_DIR}/src/formula/Ltl/*.h ${PROJECT_SOURCE_DIR}/src/formula/Ltl/*.cpp)
-file(GLOB_RECURSE STORM_FORMULA_PRCTL_FILES ${PROJECT_SOURCE_DIR}/src/formula/Prctl/*.h ${PROJECT_SOURCE_DIR}/src/formula/Prctl/*.cpp)
+file(GLOB STORM_PROPERTIES_FILES ${PROJECT_SOURCE_DIR}/src/properties/*.h ${PROJECT_SOURCE_DIR}/src/properties/*.cpp)
+file(GLOB_RECURSE STORM_PROPERTIES_CSL_FILES ${PROJECT_SOURCE_DIR}/src/properties/csl/*.h ${PROJECT_SOURCE_DIR}/src/properties/csl/*.cpp)
+file(GLOB_RECURSE STORM_PROPERTIES_LTL_FILES ${PROJECT_SOURCE_DIR}/src/properties/ltl/*.h ${PROJECT_SOURCE_DIR}/src/properties/ltl/*.cpp)
+file(GLOB_RECURSE STORM_PROPERTIES_PRCTL_FILES ${PROJECT_SOURCE_DIR}/src/properties/prctl/*.h ${PROJECT_SOURCE_DIR}/src/properties/prctl/*.cpp)
+file(GLOB_RECURSE STORM_PROPERTIES_ACTIONS_FILES ${PROJECT_SOURCE_DIR}/src/properties/actions/*.h ${PROJECT_SOURCE_DIR}/src/properties/actions/*.cpp)
 file(GLOB_RECURSE STORM_MODELCHECKER_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/*.cpp)
 file(GLOB_RECURSE STORM_COUNTEREXAMPLES_FILES ${PROJECT_SOURCE_DIR}/src/counterexamples/*.h ${PROJECT_SOURCE_DIR}/src/counterexamples/*.cpp)
 file(GLOB_RECURSE STORM_MODELS_FILES ${PROJECT_SOURCE_DIR}/src/models/*.h ${PROJECT_SOURCE_DIR}/src/models/*.cpp)
@@ -269,11 +269,11 @@ file(GLOB_RECURSE STORM_BUILD_HEADERS ${PROJECT_BINARY_DIR}/include/*.h)
 source_group(main FILES ${STORM_MAIN_FILE})
 source_group(adapters FILES ${STORM_ADAPTERS_FILES})
 source_group(exceptions FILES ${STORM_EXCEPTIONS_FILES})
-source_group(formula FILES ${STORM_FORMULA_FILES})
-source_group(formula\\abstract FILES ${STORM_FORMULA_ABSTRACT_FILES})
-source_group(formula\\csl FILES ${STORM_FORMULA_CSL_FILES})
-source_group(formula\\ltl FILES ${STORM_FORMULA_LTL_FILES})
-source_group(formula\\prctl FILES ${STORM_FORMULA_PRCTL_FILES})
+source_group(properties FILES ${STORM_PROPERTIES_FILES})
+source_group(properties\\csl FILES ${STORM_PROPERTIES_CSL_FILES})
+source_group(properties\\ltl FILES ${STORM_PROPERTIES_LTL_FILES})
+source_group(properties\\prctl FILES ${STORM_PROPERTIES_PRCTL_FILES})
+source_group(properties\\actions FILES ${STORM_PROPERTIES_ACTIONS_FILES})
 source_group(generated FILES ${STORM_BUILD_HEADERS})
 source_group(modelchecker FILES ${STORM_MODELCHECKER_FILES})
 source_group(counterexamples FILES ${STORM_COUNTEREXAMPLES_FILES})

examples/dtmc/die/die.pm

@@ -22,3 +22,10 @@ endmodule
 rewards "coin_flips"
 	[] s<7 : 1;
 endrewards
+
+label "one" = s=7&d=1;
+label "two" = s=7&d=2;
+label "three" = s=7&d=3;
+label "four" = s=7&d=4;
+label "five" = s=7&d=5;
+label "six" = s=7&d=6;

src/modelchecker/reachability/SparseSccModelChecker.cpp

@@ -0,0 +1,30 @@
+#include "src/modelchecker/reachability/SparseSccModelChecker.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace reachability {
+            
+            template<typename ValueType>
+            ValueType SparseSccModelChecker<ValueType>::computeReachabilityProbability(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+                
+                
+                
+                return 0;
+            }
+            
+            template<typename ValueType>
+            typename SparseSccModelChecker<ValueType>::FlexibleSparseMatrix SparseSccModelChecker<ValueType>::getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix) {
+                FlexibleSparseMatrix flexibleMatrix(matrix.getRowCount());
+                
+                for (SparseSccModelChecker<ValueType>::FlexibleMatrix::index_type row = 0; row < matrix.getRowCount(); ++row) {
+                    
+                }
+                
+                return flexibleMatrix;
+            }
+            
+            template class SparseSccModelChecker<double>;
+            
+        } // namespace reachability
+    } // namespace modelchecker
+} // namespace storm

src/modelchecker/reachability/SparseSccModelChecker.h

@@ -0,0 +1,36 @@
+#include "src/models/Dtmc.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace reachability {
+            
+            template<typename ValueType>
+            class SparseSccModelChecker {
+            private:
+                class FlexibleSparseMatrix {
+                public:
+                    typedef uint_fast64_t index_type;
+                    typedef ValueType value_type;
+                    typedef std::vector<storm::storage::MatrixEntry<index_type, value_type>> row_type;
+                    
+                    FlexibleSparseMatrix(index_type rows);
+                    
+                    void reserveInRow(index_type row, index_type numberOfElements);
+                    
+                    row_type& getRow(index_type);
+                    
+                private:
+                    std::vector<row_type> data;
+                };
+                
+            public:
+                static ValueType computeReachabilityProbability(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+                
+            private:
+                void treatScc(storm::storage::SparseMatrix<ValueType>& matrix, storm::storage::BitVector const& scc, uint_fast64_t level) const;
+                
+                FlexibleSparseMatrix getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix);
+            };
+        }
+    }
+}

src/storm.cpp

@@ -37,6 +37,7 @@
 #include "src/modelchecker/prctl/CreatePrctlModelChecker.h"
 #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
 #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
+#include "src/modelchecker/reachability/SparseSccModelChecker.h"
 #include "src/solver/GmmxxLinearEquationSolver.h"
 #include "src/solver/NativeLinearEquationSolver.h"
 #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
@@ -227,6 +228,12 @@ int main(const int argc, const char* argv[]) {
 			std::chrono::high_resolution_clock::time_point programTranslationEnd = std::chrono::high_resolution_clock::now();
 			std::cout << "Parsing and translating the Symbolic Input took " << std::chrono::duration_cast<std::chrono::milliseconds>(programTranslationEnd - programTranslationStart).count() << " milliseconds." << std::endl;
 
+            storm::modelchecker::reachability::SparseSccModelChecker<double> modelChecker;
+            
+            storm::storage::BitVector trueStates(model->getNumberOfStates(), true);
+            storm::storage::BitVector oneStates = model->getLabeledStates("one");
+            modelChecker.computeReachabilityProbability(*model->as<storm::models::Dtmc<double>>(), trueStates, oneStates);
+            
             if (s->isSet("mincmd")) {
                 if (model->getType() != storm::models::MDP) {
                     LOG4CPLUS_ERROR(logger, "Minimal command counterexample generation is only supported for models of type MDP.");
@@ -258,44 +265,44 @@ int main(const int argc, const char* argv[]) {
 				std::chrono::high_resolution_clock::time_point minCmdEnd = std::chrono::high_resolution_clock::now();
 				std::cout << "Minimal command Counterexample generation took " << std::chrono::duration_cast<std::chrono::milliseconds>(minCmdEnd - minCmdStart).count() << " milliseconds." << std::endl;
             } else if (s->isSet("prctl")) {
-				// Depending on the model type, the appropriate model checking procedure is chosen.
-				storm::modelchecker::prctl::AbstractModelChecker<double>* modelchecker = nullptr;
-                
+//				// Depending on the model type, the appropriate model checking procedure is chosen.
+//				storm::modelchecker::prctl::AbstractModelChecker<double>* modelchecker = nullptr;
+//                
 				// Modelchecking Time Measurement, Start
 				std::chrono::high_resolution_clock::time_point modelcheckingStart = std::chrono::high_resolution_clock::now();
-
-				switch (model->getType()) {
-                    case storm::models::DTMC:
-                        LOG4CPLUS_INFO(logger, "Model is a DTMC.");
-                        modelchecker = createPrctlModelChecker(*model->as<storm::models::Dtmc<double>>());
-                        checkPrctlFormulae(*modelchecker);
-                        break;
-                    case storm::models::MDP:
-                        LOG4CPLUS_INFO(logger, "Model is an MDP.");
-                        modelchecker = createPrctlModelChecker(*model->as<storm::models::Mdp<double>>());
-                        checkPrctlFormulae(*modelchecker);
-                        break;
-                    case storm::models::CTMC:
-                        LOG4CPLUS_INFO(logger, "Model is a CTMC.");
-                        LOG4CPLUS_ERROR(logger, "The selected model type is not supported.");
-                        break;
-                    case storm::models::CTMDP:
-                        LOG4CPLUS_INFO(logger, "Model is a CTMDP.");
-                        LOG4CPLUS_ERROR(logger, "The selected model type is not supported.");
-                        break;
-                    case storm::models::MA:
-                        LOG4CPLUS_INFO(logger, "Model is a Markov automaton.");
-                        break;
-                    case storm::models::Unknown:
-                    default:
-                        LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly.");
-                        break;
-				}
+//
+//				switch (model->getType()) {
+//                    case storm::models::DTMC:
+//                        LOG4CPLUS_INFO(logger, "Model is a DTMC.");
+//                        modelchecker = createPrctlModelChecker(*model->as<storm::models::Dtmc<double>>());
+//                        checkPrctlFormulae(*modelchecker);
+//                        break;
+//                    case storm::models::MDP:
+//                        LOG4CPLUS_INFO(logger, "Model is an MDP.");
+//                        modelchecker = createPrctlModelChecker(*model->as<storm::models::Mdp<double>>());
+//                        checkPrctlFormulae(*modelchecker);
+//                        break;
+//                    case storm::models::CTMC:
+//                        LOG4CPLUS_INFO(logger, "Model is a CTMC.");
+//                        LOG4CPLUS_ERROR(logger, "The selected model type is not supported.");
+//                        break;
+//                    case storm::models::CTMDP:
+//                        LOG4CPLUS_INFO(logger, "Model is a CTMDP.");
+//                        LOG4CPLUS_ERROR(logger, "The selected model type is not supported.");
+//                        break;
+//                    case storm::models::MA:
+//                        LOG4CPLUS_INFO(logger, "Model is a Markov automaton.");
+//                        break;
+//                    case storm::models::Unknown:
+//                    default:
+//                        LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly.");
+//                        break;
+//				}
+//                
+//				if (modelchecker != nullptr) {
+//					delete modelchecker;
+//				}
                 
-				if (modelchecker != nullptr) {
-					delete modelchecker;
-				}
-
 				// Modelchecking Time Measurement, End
 				std::chrono::high_resolution_clock::time_point modelcheckingEnd = std::chrono::high_resolution_clock::now();
 				std::cout << "Running the PRCTL ModelChecker took " << std::chrono::duration_cast<std::chrono::milliseconds>(modelcheckingEnd - modelcheckingStart).count() << " milliseconds." << std::endl;

test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp

@@ -53,8 +53,8 @@ TEST(StronglyConnectedComponentDecomposition, AsynchronousLeader) {
     ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp, true));
     ASSERT_EQ(127, sccDecomposition.size());
 
-    ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp, true));
-    ASSERT_EQ(127, sccDecomposition.size());
+    ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp, true, true));
+    ASSERT_EQ(7, sccDecomposition.size());
 
     mdp = nullptr;
 }