From 1cc930f0e4c70a06d07eb99b02b667427ce33983 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 12 Sep 2014 16:51:24 +0200 Subject: [PATCH] Added proper source grouping for properties directory. Fixed one performance tests. Started on SCC-based reachability model checker. Former-commit-id: e48c1637830f09e3714f7fc1d10eddc9e1b4a2fb --- CMakeLists.txt | 20 ++--- examples/dtmc/die/die.pm | 7 ++ .../reachability/SparseSccModelChecker.cpp | 30 ++++++++ .../reachability/SparseSccModelChecker.h | 36 +++++++++ src/storm.cpp | 77 ++++++++++--------- ...glyConnectedComponentDecompositionTest.cpp | 4 +- 6 files changed, 127 insertions(+), 47 deletions(-) create mode 100644 src/modelchecker/reachability/SparseSccModelChecker.cpp create mode 100644 src/modelchecker/reachability/SparseSccModelChecker.h diff --git a/CMakeLists.txt b/CMakeLists.txt index c6d62bdde..2f7d1cc25 100644 --- a/CMakeLists.txt +++ b/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}) diff --git a/examples/dtmc/die/die.pm b/examples/dtmc/die/die.pm index 700951a05..dacde8a79 100644 --- a/examples/dtmc/die/die.pm +++ b/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; diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp new file mode 100644 index 000000000..3592983e6 --- /dev/null +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -0,0 +1,30 @@ +#include "src/modelchecker/reachability/SparseSccModelChecker.h" + +namespace storm { + namespace modelchecker { + namespace reachability { + + template + ValueType SparseSccModelChecker::computeReachabilityProbability(storm::models::Dtmc const& dtmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + + + + return 0; + } + + template + typename SparseSccModelChecker::FlexibleSparseMatrix SparseSccModelChecker::getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix) { + FlexibleSparseMatrix flexibleMatrix(matrix.getRowCount()); + + for (SparseSccModelChecker::FlexibleMatrix::index_type row = 0; row < matrix.getRowCount(); ++row) { + + } + + return flexibleMatrix; + } + + template class SparseSccModelChecker; + + } // namespace reachability + } // namespace modelchecker +} // namespace storm \ No newline at end of file diff --git a/src/modelchecker/reachability/SparseSccModelChecker.h b/src/modelchecker/reachability/SparseSccModelChecker.h new file mode 100644 index 000000000..7e6d89ead --- /dev/null +++ b/src/modelchecker/reachability/SparseSccModelChecker.h @@ -0,0 +1,36 @@ +#include "src/models/Dtmc.h" + +namespace storm { + namespace modelchecker { + namespace reachability { + + template + class SparseSccModelChecker { + private: + class FlexibleSparseMatrix { + public: + typedef uint_fast64_t index_type; + typedef ValueType value_type; + typedef std::vector> row_type; + + FlexibleSparseMatrix(index_type rows); + + void reserveInRow(index_type row, index_type numberOfElements); + + row_type& getRow(index_type); + + private: + std::vector data; + }; + + public: + static ValueType computeReachabilityProbability(storm::models::Dtmc const& dtmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + private: + void treatScc(storm::storage::SparseMatrix& matrix, storm::storage::BitVector const& scc, uint_fast64_t level) const; + + FlexibleSparseMatrix getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix); + }; + } + } +} \ No newline at end of file diff --git a/src/storm.cpp b/src/storm.cpp index 940e75ed8..e708d6c70 100644 --- a/src/storm.cpp +++ b/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(programTranslationEnd - programTranslationStart).count() << " milliseconds." << std::endl; + storm::modelchecker::reachability::SparseSccModelChecker modelChecker; + + storm::storage::BitVector trueStates(model->getNumberOfStates(), true); + storm::storage::BitVector oneStates = model->getLabeledStates("one"); + modelChecker.computeReachabilityProbability(*model->as>(), 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(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* modelchecker = nullptr; - +// // Depending on the model type, the appropriate model checking procedure is chosen. +// storm::modelchecker::prctl::AbstractModelChecker* 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>()); - checkPrctlFormulae(*modelchecker); - break; - case storm::models::MDP: - LOG4CPLUS_INFO(logger, "Model is an MDP."); - modelchecker = createPrctlModelChecker(*model->as>()); - 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>()); +// checkPrctlFormulae(*modelchecker); +// break; +// case storm::models::MDP: +// LOG4CPLUS_INFO(logger, "Model is an MDP."); +// modelchecker = createPrctlModelChecker(*model->as>()); +// 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(modelcheckingEnd - modelcheckingStart).count() << " milliseconds." << std::endl; diff --git a/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp b/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp index 24c173265..e2ecbd5b6 100644 --- a/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp +++ b/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp @@ -53,8 +53,8 @@ TEST(StronglyConnectedComponentDecomposition, AsynchronousLeader) { ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*mdp, true)); ASSERT_EQ(127, sccDecomposition.size()); - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*mdp, true)); - ASSERT_EQ(127, sccDecomposition.size()); + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*mdp, true, true)); + ASSERT_EQ(7, sccDecomposition.size()); mdp = nullptr; }