From 5f27a932a9746e60e7d21f2e34d4face5ceac7ef Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 13 May 2013 18:53:34 +0200 Subject: [PATCH 01/18] Moved SCC decomposition to AbstractModel class, which was possible due to virtual iterator facilities in model classes. --- CMakeLists.txt | 4 +- src/models/AbstractDeterministicModel.h | 51 ++++++------------ src/models/AbstractModel.h | 51 +++++++++++++++++- src/models/AbstractNondeterministicModel.h | 63 +++++++--------------- 4 files changed, 88 insertions(+), 81 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 1a5a9a0bd..ae2c1fa2c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -20,7 +20,7 @@ else() set (STORM_LIB_SUFFIX a) set (GTEST_LIBRARY ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/libgtest.${STORM_LIB_SUFFIX}) set (GTEST_MAIN_LIBRARY ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/libgtest_main.${STORM_LIB_SUFFIX}) - set (GTEST_LIBRARIES ${GTEST_LIBRARY}) # as we dont use FindGTest anymore + set (GTEST_LIBRARIES ${GTEST_LIBRARY} ${GTEST_MAIN_LIBRARY}) # as we dont use FindGTest anymore endif() message(STATUS "GTEST_INCLUDE_DIR is ${GTEST_INCLUDE_DIR}") message(STATUS "GTEST_LIBRARY is ${GTEST_LIBRARY}") @@ -126,6 +126,7 @@ file(GLOB_RECURSE STORM_MODELS_FILES ${PROJECT_SOURCE_DIR}/src/models/*.h ${PROJ file(GLOB_RECURSE STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOURCE_DIR}/src/parser/*.cpp) file(GLOB_RECURSE STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp) file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PROJECT_SOURCE_DIR}/src/utility/*.cpp) +file(GLOB_RECURSE STORM_IR_FILES ${PROJECT_SOURCE_DIR}/src/ir/*.h ${PROJECT_SOURCE_DIR}/src/ir/*.cpp) # Test Sources # Note that the tests also need the source files, except for the main file @@ -141,6 +142,7 @@ source_group(models FILES ${STORM_MODELS_FILES}) source_group(parser FILES ${STORM_PARSER_FILES}) source_group(storage FILES ${STORM_STORAGE_FILES}) source_group(utility FILES ${STORM_UTILITY_FILES}) +source_group(ir FILES ${STORM_IR_FILES}) source_group(test FILES ${STORM_TEST_FILES}) # Add base folder for better inclusion paths diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index f7594ba05..7048ab3ed 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -47,44 +47,23 @@ class AbstractDeterministicModel: public AbstractModel { } /*! - * Extracts the SCC dependency graph from the model according to the given SCC decomposition. + * Returns an iterator to the successors of the given state. * - * @param stronglyConnectedComponents A vector containing the SCCs of the system. - * @param stateToSccMap A mapping from state indices to + * @param state The state for which to return the iterator. + * @return An iterator to the successors of the given state. */ - virtual storm::storage::SparseMatrix extractSccDependencyGraph(std::vector> const& stronglyConnectedComponents, std::map const& stateToSccMap) { - // The resulting sparse matrix will have as many rows/columns as there are SCCs. - uint_fast64_t numberOfStates = stronglyConnectedComponents.size(); - storm::storage::SparseMatrix sccDependencyGraph(numberOfStates); - sccDependencyGraph.initialize(); - - for (uint_fast64_t currentSccIndex = 0; currentSccIndex < stronglyConnectedComponents.size(); ++currentSccIndex) { - // Get the actual SCC. - std::vector const& scc = stronglyConnectedComponents[currentSccIndex]; - - // Now, we determine the SCCs which are reachable (in one step) from the current SCC. - std::set allTargetSccs; - for (auto state : scc) { - for (typename storm::storage::SparseMatrix::ConstIndexIterator succIt = this->getTransitionMatrix()->constColumnIteratorBegin(state), succIte = this->getTransitionMatrix()->constColumnIteratorEnd(state); succIt != succIte; ++succIt) { - uint_fast64_t targetScc = stateToSccMap.find(*succIt)->second; - - // We only need to consider transitions that are actually leaving the SCC. - if (targetScc != currentSccIndex) { - allTargetSccs.insert(targetScc); - } - } - } - - // Now we can just enumerate all the target SCCs and insert the corresponding transitions. - for (auto targetScc : allTargetSccs) { - sccDependencyGraph.insertNextValue(currentSccIndex, targetScc, true); - } - } - - // Finalize the matrix. - sccDependencyGraph.finalize(true); - - return sccDependencyGraph; + virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) { + return this->getTransitionMatrix()->constColumnIteratorBegin(state); + } + + /*! + * Returns an iterator pointing to the element past the successors of the given state. + * + * @param state The state for which to return the iterator. + * @return An iterator pointing to the element past the successors of the given state. + */ + virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) { + return this->getTransitionMatrix()->constColumnIteratorEnd(state); } }; diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 364e501b0..e50aa683f 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -91,7 +91,56 @@ class AbstractModel: public std::enable_shared_from_this> { * @param stronglyConnectedComponents A vector containing the SCCs of the system. * @param stateToSccMap A mapping from state indices to */ - virtual storm::storage::SparseMatrix extractSccDependencyGraph(std::vector> const& stronglyConnectedComponents, std::map const& stateToSccMap) = 0; + virtual storm::storage::SparseMatrix extractSccDependencyGraph(std::vector> const& stronglyConnectedComponents, std::map const& stateToSccMap) { + // The resulting sparse matrix will have as many rows/columns as there are SCCs. + uint_fast64_t numberOfStates = stronglyConnectedComponents.size(); + storm::storage::SparseMatrix sccDependencyGraph(numberOfStates); + sccDependencyGraph.initialize(); + + for (uint_fast64_t currentSccIndex = 0; currentSccIndex < stronglyConnectedComponents.size(); ++currentSccIndex) { + // Get the actual SCC. + std::vector const& scc = stronglyConnectedComponents[currentSccIndex]; + + // Now, we determine the SCCs which are reachable (in one step) from the current SCC. + std::set allTargetSccs; + for (auto state : scc) { + for (typename storm::storage::SparseMatrix::ConstIndexIterator succIt = this->constStateSuccessorIteratorBegin(state), succIte = this->constStateSuccessorIteratorEnd(state); succIt != succIte; ++succIt) { + uint_fast64_t targetScc = stateToSccMap.find(*succIt)->second; + + // We only need to consider transitions that are actually leaving the SCC. + if (targetScc != currentSccIndex) { + allTargetSccs.insert(targetScc); + } + } + } + + // Now we can just enumerate all the target SCCs and insert the corresponding transitions. + for (auto targetScc : allTargetSccs) { + sccDependencyGraph.insertNextValue(currentSccIndex, targetScc, true); + } + } + + // Finalize the matrix. + sccDependencyGraph.finalize(true); + + return sccDependencyGraph; + } + + /*! + * Returns an iterator to the successors of the given state. + * + * @param state The state for which to return the iterator. + * @return An iterator to the successors of the given state. + */ + virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) = 0; + + /*! + * Returns an iterator pointing to the element past the successors of the given state. + * + * @param state The state for which to return the iterator. + * @return An iterator pointing to the element past the successors of the given state. + */ + virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) = 0; /*! * Returns the state space size of the model. diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index 4c51f0863..cd2700a49 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -58,49 +58,6 @@ class AbstractNondeterministicModel: public AbstractModel { uint_fast64_t getNumberOfChoices() const { return this->getTransitionMatrix()->getRowCount(); } - - /*! - * Extracts the SCC dependency graph from the model according to the given SCC decomposition. - * - * @param stronglyConnectedComponents A vector containing the SCCs of the system. - * @param stateToSccMap A mapping from state indices to - */ - virtual storm::storage::SparseMatrix extractSccDependencyGraph(std::vector> const& stronglyConnectedComponents, std::map const& stateToSccMap) { - // The resulting sparse matrix will have as many rows/columns as there are SCCs. - uint_fast64_t numberOfStates = stronglyConnectedComponents.size(); - storm::storage::SparseMatrix sccDependencyGraph(numberOfStates); - sccDependencyGraph.initialize(); - - for (uint_fast64_t currentSccIndex = 0; currentSccIndex < stronglyConnectedComponents.size(); ++currentSccIndex) { - // Get the actual SCC. - std::vector const& scc = stronglyConnectedComponents[currentSccIndex]; - - // Now, we determine the SCCs which are reachable (in one step) from the current SCC. - std::set allTargetSccs; - for (auto state : scc) { - for (uint_fast64_t rowIndex = (*nondeterministicChoiceIndices)[state]; rowIndex < (*nondeterministicChoiceIndices)[state + 1]; ++rowIndex) { - for (typename storm::storage::SparseMatrix::ConstIndexIterator succIt = this->getTransitionMatrix()->constColumnIteratorBegin(rowIndex), succIte = this->getTransitionMatrix()->constColumnIteratorEnd(rowIndex); succIt != succIte; ++succIt) { - uint_fast64_t targetScc = stateToSccMap.find(*succIt)->second; - - // We only need to consider transitions that are actually leaving the SCC. - if (targetScc != currentSccIndex) { - allTargetSccs.insert(targetScc); - } - } - } - } - - // Now we can just enumerate all the target SCCs and insert the corresponding transitions. - for (auto targetScc : allTargetSccs) { - sccDependencyGraph.insertNextValue(currentSccIndex, targetScc, true); - } - } - - // Finalize the matrix. - sccDependencyGraph.finalize(true); - - return sccDependencyGraph; - } /*! * Retrieves the size of the internal representation of the model in memory. @@ -120,6 +77,26 @@ class AbstractNondeterministicModel: public AbstractModel { std::shared_ptr> getNondeterministicChoiceIndices() const { return nondeterministicChoiceIndices; } + + /*! + * Returns an iterator to the successors of the given state. + * + * @param state The state for which to return the iterator. + * @return An iterator to the successors of the given state. + */ + virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) { + return this->getTransitionMatrix()->constColumnIteratorBegin((*nondeterministicChoiceIndices)[state]); + } + + /*! + * Returns an iterator pointing to the element past the successors of the given state. + * + * @param state The state for which to return the iterator. + * @return An iterator pointing to the element past the successors of the given state. + */ + virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) { + return this->getTransitionMatrix()->constColumnIteratorEnd((*nondeterministicChoiceIndices)[state + 1] - 1); + } private: /*! A vector of indices mapping states to the choices (rows) in the transition matrix. */ From 27de566228cf9dbd537924c24b4f20ff6cc5e210 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 13 May 2013 20:03:26 +0200 Subject: [PATCH 02/18] Moved current tests to the functional test suite in an attempt to introduce performance tests. --- CMakeLists.txt | 5 +++-- resources/3rdparty/cudd-2.5.0/Makefile | 2 +- test/{ => functional}/eigen/EigenSparseMatrixTest.cpp | 0 .../{ => modelchecker}/EigenDtmcPrctModelCheckerTest.cpp | 6 +++--- .../{ => modelchecker}/GmmxxDtmcPrctModelCheckerTest.cpp | 6 +++--- .../{ => modelchecker}/GmmxxMdpPrctModelCheckerTest.cpp | 4 ++-- test/functional/{ => modelchecker}/die/testFormulas.prctl | 0 test/{ => functional}/parser/.gitignore | 0 test/{ => functional}/parser/CslParserTest.cpp | 0 test/{ => functional}/parser/LtlParserTest.cpp | 0 test/{ => functional}/parser/ParseMdpTest.cpp | 0 test/{ => functional}/parser/ParsePrismTest.cpp | 0 test/{ => functional}/parser/PrctlParserTest.cpp | 0 test/{ => functional}/parser/ReadLabFileTest.cpp | 0 test/{ => functional}/parser/ReadTraFileTest.cpp | 0 test/{ => functional}/parser/prctl_files/apOnly.prctl | 0 .../parser/prctl_files/complexFormula.prctl | 0 .../parser/prctl_files/probabilisticFormula.prctl | 0 .../parser/prctl_files/probabilisticNoBoundFormula.prctl | 0 .../parser/prctl_files/propositionalFormula.prctl | 0 .../{ => functional}/parser/prctl_files/rewardFormula.prctl | 0 .../parser/prctl_files/rewardNoBoundFormula.prctl | 0 test/{ => functional}/parser/readme.txt | 0 test/{ => functional}/storage/BitVectorTest.cpp | 0 test/{ => functional}/storage/SparseMatrixTest.cpp | 0 test/{ => functional}/storage/adapters/EigenAdapterTest.cpp | 0 test/{ => functional}/storage/adapters/GmmAdapterTest.cpp | 0 test/{ => functional}/storage/adapters/StormAdapterTest.cpp | 0 .../storm-functional-tests.cpp} | 0 29 files changed, 12 insertions(+), 11 deletions(-) rename test/{ => functional}/eigen/EigenSparseMatrixTest.cpp (100%) rename test/functional/{ => modelchecker}/EigenDtmcPrctModelCheckerTest.cpp (91%) rename test/functional/{ => modelchecker}/GmmxxDtmcPrctModelCheckerTest.cpp (92%) rename test/functional/{ => modelchecker}/GmmxxMdpPrctModelCheckerTest.cpp (95%) rename test/functional/{ => modelchecker}/die/testFormulas.prctl (100%) rename test/{ => functional}/parser/.gitignore (100%) rename test/{ => functional}/parser/CslParserTest.cpp (100%) rename test/{ => functional}/parser/LtlParserTest.cpp (100%) rename test/{ => functional}/parser/ParseMdpTest.cpp (100%) rename test/{ => functional}/parser/ParsePrismTest.cpp (100%) rename test/{ => functional}/parser/PrctlParserTest.cpp (100%) rename test/{ => functional}/parser/ReadLabFileTest.cpp (100%) rename test/{ => functional}/parser/ReadTraFileTest.cpp (100%) rename test/{ => functional}/parser/prctl_files/apOnly.prctl (100%) rename test/{ => functional}/parser/prctl_files/complexFormula.prctl (100%) rename test/{ => functional}/parser/prctl_files/probabilisticFormula.prctl (100%) rename test/{ => functional}/parser/prctl_files/probabilisticNoBoundFormula.prctl (100%) rename test/{ => functional}/parser/prctl_files/propositionalFormula.prctl (100%) rename test/{ => functional}/parser/prctl_files/rewardFormula.prctl (100%) rename test/{ => functional}/parser/prctl_files/rewardNoBoundFormula.prctl (100%) rename test/{ => functional}/parser/readme.txt (100%) rename test/{ => functional}/storage/BitVectorTest.cpp (100%) rename test/{ => functional}/storage/SparseMatrixTest.cpp (100%) rename test/{ => functional}/storage/adapters/EigenAdapterTest.cpp (100%) rename test/{ => functional}/storage/adapters/GmmAdapterTest.cpp (100%) rename test/{ => functional}/storage/adapters/StormAdapterTest.cpp (100%) rename test/{storm-tests.cpp => functional/storm-functional-tests.cpp} (100%) diff --git a/CMakeLists.txt b/CMakeLists.txt index ae2c1fa2c..91df3d3f4 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -130,7 +130,7 @@ file(GLOB_RECURSE STORM_IR_FILES ${PROJECT_SOURCE_DIR}/src/ir/*.h ${PROJECT_SOUR # Test Sources # Note that the tests also need the source files, except for the main file -file(GLOB_RECURSE STORM_TEST_FILES ${PROJECT_SOURCE_DIR}/test/*.h ${PROJECT_SOURCE_DIR}/test/*.cpp) +file(GLOB_RECURSE STORM_FUNCTIONAL_TEST_FILES ${PROJECT_SOURCE_DIR}/test/functional/*.h ${PROJECT_SOURCE_DIR}/test/functional/*.cpp) # Group the headers and sources source_group(main FILES ${STORM_MAIN_FILE}) @@ -226,7 +226,8 @@ endif(CUDD_LIBRARY_DIRS) # Add the executables # Must be created *after* Boost was added because of LINK_DIRECTORIES add_executable(storm ${STORM_SOURCES} ${STORM_HEADERS}) -add_executable(storm-tests ${STORM_TEST_FILES} ${STORM_SOURCES_WITHOUT_MAIN} ${STORM_HEADERS}) +add_executable(storm-functional-tests ${STORM_FUNCTIONAL_TEST_FILES} ${STORM_SOURCES_WITHOUT_MAIN} ${STORM_HEADERS}) +add_executable(storm-performance-tests ${STORM_PERFORMANCE_TEST_FILES} ${STORM_SOURCES_WITHOUT_MAIN} ${STORM_HEADERS}) # Add target link deps for Boost program options target_link_libraries(storm ${Boost_LIBRARIES}) diff --git a/resources/3rdparty/cudd-2.5.0/Makefile b/resources/3rdparty/cudd-2.5.0/Makefile index 6c7fbb4d3..95a0a47d5 100644 --- a/resources/3rdparty/cudd-2.5.0/Makefile +++ b/resources/3rdparty/cudd-2.5.0/Makefile @@ -51,7 +51,7 @@ RANLIB = ranlib #ICFLAGS = # These two are typical settings for optimized code with gcc. #ICFLAGS = -g -O3 -Wall -ICFLAGS = -O3 +ICFLAGS = -O4 # Use XCFLAGS to specify machine-dependent compilation flags. # For some platforms no special flags are needed. diff --git a/test/eigen/EigenSparseMatrixTest.cpp b/test/functional/eigen/EigenSparseMatrixTest.cpp similarity index 100% rename from test/eigen/EigenSparseMatrixTest.cpp rename to test/functional/eigen/EigenSparseMatrixTest.cpp diff --git a/test/functional/EigenDtmcPrctModelCheckerTest.cpp b/test/functional/modelchecker/EigenDtmcPrctModelCheckerTest.cpp similarity index 91% rename from test/functional/EigenDtmcPrctModelCheckerTest.cpp rename to test/functional/modelchecker/EigenDtmcPrctModelCheckerTest.cpp index f2774c259..ced6139cb 100644 --- a/test/functional/EigenDtmcPrctModelCheckerTest.cpp +++ b/test/functional/modelchecker/EigenDtmcPrctModelCheckerTest.cpp @@ -9,7 +9,7 @@ TEST(EigenDtmcPrctModelCheckerTest, Die) { storm::settings::Settings* s = storm::settings::instance(); s->set("fix-deadlocks"); - storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/die/die.tra", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.coin_flips.trans.rew"); + storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/die/die.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/die/die.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/die/die.coin_flips.trans.rew"); ASSERT_EQ(parser.getType(), storm::models::DTMC); @@ -69,7 +69,7 @@ TEST(EigenDtmcPrctModelCheckerTest, Die) { TEST(EigenDtmcPrctModelCheckerTest, Crowds) { storm::settings::Settings* s = storm::settings::instance(); s->set("fix-deadlocks"); - storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/crowds/crowds5_5.tra", STORM_CPP_TESTS_BASE_PATH "/functional/crowds/crowds5_5.lab", "", ""); + storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/crowds/crowds5_5.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/crowds/crowds5_5.lab", "", ""); ASSERT_EQ(parser.getType(), storm::models::DTMC); @@ -117,7 +117,7 @@ TEST(EigenDtmcPrctModelCheckerTest, Crowds) { TEST(EigenDtmcPrctModelCheckerTest, SynchronousLeader) { storm::settings::Settings* s = storm::settings::instance(); s->set("fix-deadlocks"); - storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.tra", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.pick.trans.rew"); + storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/synchronous_leader/leader4_8.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/synchronous_leader/leader4_8.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/synchronous_leader/leader4_8.pick.trans.rew"); ASSERT_EQ(parser.getType(), storm::models::DTMC); diff --git a/test/functional/GmmxxDtmcPrctModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp similarity index 92% rename from test/functional/GmmxxDtmcPrctModelCheckerTest.cpp rename to test/functional/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index aa2a014fa..2286cd8d9 100644 --- a/test/functional/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -8,7 +8,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Die) { storm::settings::Settings* s = storm::settings::instance(); s->set("fix-deadlocks"); - storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/die/die.tra", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.coin_flips.trans.rew"); + storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/die/die.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/die/die.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/die/die.coin_flips.trans.rew"); ASSERT_EQ(parser.getType(), storm::models::DTMC); @@ -75,7 +75,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Die) { TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { storm::settings::Settings* s = storm::settings::instance(); s->set("fix-deadlocks"); - storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/crowds/crowds5_5.tra", STORM_CPP_TESTS_BASE_PATH "/functional/crowds/crowds5_5.lab", "", ""); + storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/crowds/crowds5_5.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/crowds/crowds5_5.lab", "", ""); ASSERT_EQ(parser.getType(), storm::models::DTMC); @@ -129,7 +129,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { storm::settings::Settings* s = storm::settings::instance(); s->set("fix-deadlocks"); - storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.tra", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.pick.trans.rew"); + storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/synchronous_leader/leader4_8.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/synchronous_leader/leader4_8.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/synchronous_leader/leader4_8.pick.trans.rew"); ASSERT_EQ(parser.getType(), storm::models::DTMC); diff --git a/test/functional/GmmxxMdpPrctModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp similarity index 95% rename from test/functional/GmmxxMdpPrctModelCheckerTest.cpp rename to test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp index 13136cc69..43fbd9c35 100644 --- a/test/functional/GmmxxMdpPrctModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp @@ -7,7 +7,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { storm::settings::Settings* s = storm::settings::instance(); - storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.flip.trans.rew"); + storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "functional/modelchecker/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.flip.trans.rew"); ASSERT_EQ(parser.getType(), storm::models::MDP); @@ -171,7 +171,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { storm::settings::Settings* s = storm::settings::instance(); - storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/asynchronous_leader/leader4.tra", STORM_CPP_TESTS_BASE_PATH "/functional/asynchronous_leader/leader4.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/asynchronous_leader/leader4.trans.rew"); + storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/asynchronous_leader/leader4.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/asynchronous_leader/leader4.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/asynchronous_leader/leader4.trans.rew"); ASSERT_EQ(parser.getType(), storm::models::MDP); diff --git a/test/functional/die/testFormulas.prctl b/test/functional/modelchecker/die/testFormulas.prctl similarity index 100% rename from test/functional/die/testFormulas.prctl rename to test/functional/modelchecker/die/testFormulas.prctl diff --git a/test/parser/.gitignore b/test/functional/parser/.gitignore similarity index 100% rename from test/parser/.gitignore rename to test/functional/parser/.gitignore diff --git a/test/parser/CslParserTest.cpp b/test/functional/parser/CslParserTest.cpp similarity index 100% rename from test/parser/CslParserTest.cpp rename to test/functional/parser/CslParserTest.cpp diff --git a/test/parser/LtlParserTest.cpp b/test/functional/parser/LtlParserTest.cpp similarity index 100% rename from test/parser/LtlParserTest.cpp rename to test/functional/parser/LtlParserTest.cpp diff --git a/test/parser/ParseMdpTest.cpp b/test/functional/parser/ParseMdpTest.cpp similarity index 100% rename from test/parser/ParseMdpTest.cpp rename to test/functional/parser/ParseMdpTest.cpp diff --git a/test/parser/ParsePrismTest.cpp b/test/functional/parser/ParsePrismTest.cpp similarity index 100% rename from test/parser/ParsePrismTest.cpp rename to test/functional/parser/ParsePrismTest.cpp diff --git a/test/parser/PrctlParserTest.cpp b/test/functional/parser/PrctlParserTest.cpp similarity index 100% rename from test/parser/PrctlParserTest.cpp rename to test/functional/parser/PrctlParserTest.cpp diff --git a/test/parser/ReadLabFileTest.cpp b/test/functional/parser/ReadLabFileTest.cpp similarity index 100% rename from test/parser/ReadLabFileTest.cpp rename to test/functional/parser/ReadLabFileTest.cpp diff --git a/test/parser/ReadTraFileTest.cpp b/test/functional/parser/ReadTraFileTest.cpp similarity index 100% rename from test/parser/ReadTraFileTest.cpp rename to test/functional/parser/ReadTraFileTest.cpp diff --git a/test/parser/prctl_files/apOnly.prctl b/test/functional/parser/prctl_files/apOnly.prctl similarity index 100% rename from test/parser/prctl_files/apOnly.prctl rename to test/functional/parser/prctl_files/apOnly.prctl diff --git a/test/parser/prctl_files/complexFormula.prctl b/test/functional/parser/prctl_files/complexFormula.prctl similarity index 100% rename from test/parser/prctl_files/complexFormula.prctl rename to test/functional/parser/prctl_files/complexFormula.prctl diff --git a/test/parser/prctl_files/probabilisticFormula.prctl b/test/functional/parser/prctl_files/probabilisticFormula.prctl similarity index 100% rename from test/parser/prctl_files/probabilisticFormula.prctl rename to test/functional/parser/prctl_files/probabilisticFormula.prctl diff --git a/test/parser/prctl_files/probabilisticNoBoundFormula.prctl b/test/functional/parser/prctl_files/probabilisticNoBoundFormula.prctl similarity index 100% rename from test/parser/prctl_files/probabilisticNoBoundFormula.prctl rename to test/functional/parser/prctl_files/probabilisticNoBoundFormula.prctl diff --git a/test/parser/prctl_files/propositionalFormula.prctl b/test/functional/parser/prctl_files/propositionalFormula.prctl similarity index 100% rename from test/parser/prctl_files/propositionalFormula.prctl rename to test/functional/parser/prctl_files/propositionalFormula.prctl diff --git a/test/parser/prctl_files/rewardFormula.prctl b/test/functional/parser/prctl_files/rewardFormula.prctl similarity index 100% rename from test/parser/prctl_files/rewardFormula.prctl rename to test/functional/parser/prctl_files/rewardFormula.prctl diff --git a/test/parser/prctl_files/rewardNoBoundFormula.prctl b/test/functional/parser/prctl_files/rewardNoBoundFormula.prctl similarity index 100% rename from test/parser/prctl_files/rewardNoBoundFormula.prctl rename to test/functional/parser/prctl_files/rewardNoBoundFormula.prctl diff --git a/test/parser/readme.txt b/test/functional/parser/readme.txt similarity index 100% rename from test/parser/readme.txt rename to test/functional/parser/readme.txt diff --git a/test/storage/BitVectorTest.cpp b/test/functional/storage/BitVectorTest.cpp similarity index 100% rename from test/storage/BitVectorTest.cpp rename to test/functional/storage/BitVectorTest.cpp diff --git a/test/storage/SparseMatrixTest.cpp b/test/functional/storage/SparseMatrixTest.cpp similarity index 100% rename from test/storage/SparseMatrixTest.cpp rename to test/functional/storage/SparseMatrixTest.cpp diff --git a/test/storage/adapters/EigenAdapterTest.cpp b/test/functional/storage/adapters/EigenAdapterTest.cpp similarity index 100% rename from test/storage/adapters/EigenAdapterTest.cpp rename to test/functional/storage/adapters/EigenAdapterTest.cpp diff --git a/test/storage/adapters/GmmAdapterTest.cpp b/test/functional/storage/adapters/GmmAdapterTest.cpp similarity index 100% rename from test/storage/adapters/GmmAdapterTest.cpp rename to test/functional/storage/adapters/GmmAdapterTest.cpp diff --git a/test/storage/adapters/StormAdapterTest.cpp b/test/functional/storage/adapters/StormAdapterTest.cpp similarity index 100% rename from test/storage/adapters/StormAdapterTest.cpp rename to test/functional/storage/adapters/StormAdapterTest.cpp diff --git a/test/storm-tests.cpp b/test/functional/storm-functional-tests.cpp similarity index 100% rename from test/storm-tests.cpp rename to test/functional/storm-functional-tests.cpp From 3851377064408e28a6ca317592c051b2b7e7c231 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 13 May 2013 22:53:00 +0200 Subject: [PATCH 03/18] Introduced executable storm-functional-tests and storm-performance-tests. While the former contains the previous tests, the latter is currently empty, but will hold performance tests in the future. --- CMakeLists.txt | 45 +++--- .../SparseDtmcPrctlModelChecker.h | 8 +- .../eigen/EigenSparseMatrixTest.cpp | 2 +- .../GmmxxMdpPrctModelCheckerTest.cpp | 128 +++++++++--------- test/functional/parser/CslParserTest.cpp | 7 +- test/functional/parser/ParseMdpTest.cpp | 4 +- test/functional/parser/ReadLabFileTest.cpp | 8 +- test/functional/parser/ReadTraFileTest.cpp | 8 +- test/functional/storm-functional-tests.cpp | 4 +- 9 files changed, 109 insertions(+), 105 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 91df3d3f4..a99f224da 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -95,7 +95,7 @@ else(CLANG) # As CLANG is not set as a variable, we need to set it in case we have not matched another compiler. set (CLANG ON) # Set standard flags for clang - set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O4") + set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O4") set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=libc++ -Wall -Werror -pedantic -Wno-unused-variable -DBOOST_RESULT_OF_USE_TR1 -DBOOST_NO_DECLTYPE") set (CMAKE_CXX_FLAGS_DEBUG "-g") @@ -131,6 +131,7 @@ file(GLOB_RECURSE STORM_IR_FILES ${PROJECT_SOURCE_DIR}/src/ir/*.h ${PROJECT_SOUR # Test Sources # Note that the tests also need the source files, except for the main file file(GLOB_RECURSE STORM_FUNCTIONAL_TEST_FILES ${PROJECT_SOURCE_DIR}/test/functional/*.h ${PROJECT_SOURCE_DIR}/test/functional/*.cpp) +file(GLOB_RECURSE STORM_PERFORMANCE_TEST_FILES ${PROJECT_SOURCE_DIR}/test/performance/*.h ${PROJECT_SOURCE_DIR}/test/performance/*.cpp) # Group the headers and sources source_group(main FILES ${STORM_MAIN_FILE}) @@ -143,7 +144,8 @@ source_group(parser FILES ${STORM_PARSER_FILES}) source_group(storage FILES ${STORM_STORAGE_FILES}) source_group(utility FILES ${STORM_UTILITY_FILES}) source_group(ir FILES ${STORM_IR_FILES}) -source_group(test FILES ${STORM_TEST_FILES}) +source_group(functional-test FILES ${STORM_FUNCTIONAL_TEST_FILES}) +source_group(performance-test FILES ${STORM_PERFORMANCE_TEST_FILES}) # Add base folder for better inclusion paths include_directories("${PROJECT_SOURCE_DIR}") @@ -231,11 +233,13 @@ add_executable(storm-performance-tests ${STORM_PERFORMANCE_TEST_FILES} ${STORM_S # Add target link deps for Boost program options target_link_libraries(storm ${Boost_LIBRARIES}) -target_link_libraries(storm-tests ${Boost_LIBRARIES}) +target_link_libraries(storm-functional-tests ${Boost_LIBRARIES}) +target_link_libraries(storm-performance-tests ${Boost_LIBRARIES}) if (USE_INTELTBB) target_link_libraries(storm tbb tbbmalloc) - target_link_libraries(storm-tests tbb tbbmalloc) + target_link_libraries(storm-functional-tests tbb tbbmalloc) + target_link_libraries(storm-performance-tests tbb tbbmalloc) endif(USE_INTELTBB) if (APPLE) @@ -256,14 +260,16 @@ if (STORM_USE_COTIRE) cotire(storm) target_link_libraries(storm_unity ${Boost_LIBRARIES}) - #cotire(storm-tests) + #cotire(storm-functional-tests) + #cotire(storm-performance-tests) endif() # Link against libc++abi if requested. May be needed to build on Linux systems using clang. if (LINK_LIBCXXABI) message (STATUS "Linking against libc++abi.") target_link_libraries(storm "c++abi") - target_link_libraries(storm-tests "c++abi") + target_link_libraries(storm-functional-tests "c++abi") + target_link_libraries(storm-performance-tests "c++abi") endif(LINK_LIBCXXABI) # Add a target to generate API documentation with Doxygen @@ -282,9 +288,11 @@ if (GTEST_INCLUDE_DIR) enable_testing() include_directories(${GTEST_INCLUDE_DIR}) - target_link_libraries(storm-tests ${GTEST_LIBRARIES}) + target_link_libraries(storm-functional-tests ${GTEST_LIBRARIES}) + target_link_libraries(storm-performance-tests ${GTEST_LIBRARIES}) - add_test(NAME storm-tests COMMAND storm-tests) + add_test(NAME storm-functional-tests COMMAND storm-functional-tests) + add_test(NAME storm-performance-tests COMMAND storm-performance-tests) if(MSVC) # VS2012 doesn't support correctly the tuples yet add_definitions( /D _VARIADIC_MAX=10 ) endif() @@ -296,20 +304,23 @@ if (LOG4CPLUS_INCLUDE_DIR) if (STORM_USE_COTIRE) target_link_libraries(storm_unity ${LOG4CPLUS_LIBRARIES}) endif(STORM_USE_COTIRE) - target_link_libraries(storm-tests ${LOG4CPLUS_LIBRARIES}) + target_link_libraries(storm-functional-tests ${LOG4CPLUS_LIBRARIES}) + target_link_libraries(storm-performance-tests ${LOG4CPLUS_LIBRARIES}) # On Linux, we have to link against librt if (UNIX AND NOT APPLE) target_link_libraries(storm rt) if (STORM_USE_COTIRE) target_link_libraries(storm_unity rt) endif(STORM_USE_COTIRE) - target_link_libraries(storm-tests rt) + target_link_libraries(storm-functional-tests rt) + target_link_libraries(storm-performance-tests rt) endif(UNIX AND NOT APPLE) endif(LOG4CPLUS_INCLUDE_DIR) if (CUDD_LIBRARY_DIRS) target_link_libraries(storm "-lobj -lcudd -lmtr -lst -lutil -lepd") - target_link_libraries(storm-tests "-lobj -lcudd -lmtr -lst -lutil -lepd") + target_link_libraries(storm-functional-tests "-lobj -lcudd -lmtr -lst -lutil -lepd") + target_link_libraries(storm-performance-tests "-lobj -lcudd -lmtr -lst -lutil -lepd") endif(CUDD_LIBRARY_DIRS) if (THREADS_FOUND) @@ -318,7 +329,8 @@ if (THREADS_FOUND) if (STORM_USE_COTIRE) target_link_libraries(storm_unity ${CMAKE_THREAD_LIBS_INIT}) endif(STORM_USE_COTIRE) - target_link_libraries(storm-tests ${CMAKE_THREAD_LIBS_INIT}) + target_link_libraries(storm-functional-tests ${CMAKE_THREAD_LIBS_INIT}) + target_link_libraries(storm-performance-tests ${CMAKE_THREAD_LIBS_INIT}) endif(THREADS_FOUND) # Configure a header file to pass some of the CMake settings to the source code @@ -327,10 +339,9 @@ configure_file ( "${PROJECT_BINARY_DIR}/storm-config.h" ) -add_custom_target(memcheck valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm -v --fix-deadlocks ${PROJECT_SOURCE_DIR}/examples/dtmc/crowds/crowds5_5.tra examples/dtmc/crowds/crowds5_5.lab - DEPENDS storm) -add_custom_target(memcheck-tests valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm-tests -v --fix-deadlocks - DEPENDS storm-tests) - +add_custom_target(memcheck valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm -v --fix-deadlocks ${PROJECT_SOURCE_DIR}/examples/dtmc/crowds/crowds5_5.tra examples/dtmc/crowds/crowds5_5.lab DEPENDS storm) +add_custom_target(memcheck-functional-tests valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm-functional-tests -v --fix-deadlocks DEPENDS storm-functional-tests) +add_custom_target(memcheck-performance-tests valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm-performance-tests -v --fix-deadlocks DEPENDS storm-performance-tests) + set (CPPLINT_ARGS --filter=-whitespace/tab,-whitespace/line_length,-legal/copyright,-readability/streams) add_custom_target(style python cpplint.py ${CPPLINT_ARGS} `find ./src/ -iname "*.h" -or -iname "*.cpp"`) diff --git a/src/modelchecker/SparseDtmcPrctlModelChecker.h b/src/modelchecker/SparseDtmcPrctlModelChecker.h index f55f79db5..56c7a9525 100644 --- a/src/modelchecker/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/SparseDtmcPrctlModelChecker.h @@ -94,10 +94,6 @@ public: // Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates); - // Delete obsolete intermediates. - delete leftStates; - delete rightStates; - // Create the vector with which to multiply. std::vector* result = new std::vector(this->getModel().getNumberOfStates()); storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne()); @@ -105,7 +101,9 @@ public: // Perform the matrix vector multiplication as often as required by the formula bound. this->performMatrixVectorMultiplication(tmpMatrix, *result, nullptr, formula.getBound()); - // Return result. + // Delete obsolete intermediates and return result. + delete leftStates; + delete rightStates; return result; } diff --git a/test/functional/eigen/EigenSparseMatrixTest.cpp b/test/functional/eigen/EigenSparseMatrixTest.cpp index 67b70f986..d050a6948 100644 --- a/test/functional/eigen/EigenSparseMatrixTest.cpp +++ b/test/functional/eigen/EigenSparseMatrixTest.cpp @@ -18,7 +18,7 @@ TEST(EigenSparseMatrixTest, BasicReadWriteTest) { int position_row[50] = { 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, /* first row empty, one full row ��� 25 minus the diagonal entry */ + 2, 2, 2, 2, /* first row empty, one full row 25 minus the diagonal entry */ 4, 4, /* one empty row, then first and last column */ 13, 13, 13, 13, /* a few empty rows, middle columns */ 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, diff --git a/test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp index 43fbd9c35..b440df38d 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp @@ -7,164 +7,164 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { storm::settings::Settings* s = storm::settings::instance(); - storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "functional/modelchecker/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.flip.trans.rew"); - + storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.flip.trans.rew"); + ASSERT_EQ(parser.getType(), storm::models::MDP); - + std::shared_ptr> mdp = parser.getModel>(); - + ASSERT_EQ(mdp->getNumberOfStates(), 169u); ASSERT_EQ(mdp->getNumberOfTransitions(), 436u); - + storm::modelchecker::GmmxxMdpPrctlModelChecker mc(*mdp); - + storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("two"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - + std::vector* result = mc.checkNoBoundOperator(*probFormula); - + ASSERT_NE(nullptr, result); - + ASSERT_LT(std::abs((*result)[0] - 0.0277777612209320068), s->get("precision")); - + delete probFormula; delete result; - + apFormula = new storm::property::prctl::Ap("two"); eventuallyFormula = new storm::property::prctl::Eventually(apFormula); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - + result = mc.checkNoBoundOperator(*probFormula); - + ASSERT_LT(std::abs((*result)[0] - 0.0277777612209320068), s->get("precision")); - + delete probFormula; delete result; - + apFormula = new storm::property::prctl::Ap("three"); eventuallyFormula = new storm::property::prctl::Eventually(apFormula); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - + result = mc.checkNoBoundOperator(*probFormula); - + ASSERT_LT(std::abs((*result)[0] - 0.0555555224418640136), s->get("precision")); - + delete probFormula; delete result; - + apFormula = new storm::property::prctl::Ap("three"); eventuallyFormula = new storm::property::prctl::Eventually(apFormula); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - + result = mc.checkNoBoundOperator(*probFormula); - + ASSERT_LT(std::abs((*result)[0] - 0.0555555224418640136), s->get("precision")); - + delete probFormula; delete result; - + apFormula = new storm::property::prctl::Ap("four"); eventuallyFormula = new storm::property::prctl::Eventually(apFormula); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - + result = mc.checkNoBoundOperator(*probFormula); - + ASSERT_LT(std::abs((*result)[0] - 0.083333283662796020508), s->get("precision")); - + delete probFormula; delete result; - + apFormula = new storm::property::prctl::Ap("four"); eventuallyFormula = new storm::property::prctl::Eventually(apFormula); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - + result = mc.checkNoBoundOperator(*probFormula); - + ASSERT_LT(std::abs((*result)[0] - 0.083333283662796020508), s->get("precision")); - + delete probFormula; delete result; - + apFormula = new storm::property::prctl::Ap("done"); storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); - + result = mc.checkNoBoundOperator(*rewardFormula); - + ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get("precision")); - + delete rewardFormula; delete result; - + apFormula = new storm::property::prctl::Ap("done"); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - + result = mc.checkNoBoundOperator(*rewardFormula);; - + ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get("precision")); - + delete rewardFormula; delete result; - - storm::parser::AutoParser stateRewardParser(STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.lab", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.flip.state.rew", ""); - + + storm::parser::AutoParser stateRewardParser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.lab", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.flip.state.rew", ""); + ASSERT_EQ(stateRewardParser.getType(), storm::models::MDP); - + std::shared_ptr> stateRewardMdp = stateRewardParser.getModel>(); - + storm::modelchecker::GmmxxMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp); - + apFormula = new storm::property::prctl::Ap("done"); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); - + result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula); - + ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get("precision")); - + delete rewardFormula; delete result; - + apFormula = new storm::property::prctl::Ap("done"); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - + result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula); - + ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get("precision")); - + delete rewardFormula; delete result; - - storm::parser::AutoParser stateAndTransitionRewardParser(STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.lab", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.flip.state.rew", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.flip.trans.rew"); - + + storm::parser::AutoParser stateAndTransitionRewardParser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.lab", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.flip.state.rew", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.flip.trans.rew"); + ASSERT_EQ(stateAndTransitionRewardParser.getType(), storm::models::MDP); - + std::shared_ptr> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel>(); - + storm::modelchecker::GmmxxMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp); - + apFormula = new storm::property::prctl::Ap("done"); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); - + result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula); - + ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333294987678527832)), s->get("precision")); - + delete rewardFormula; delete result; - + apFormula = new storm::property::prctl::Ap("done"); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - + result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula); - + ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333294987678527832)), s->get("precision")); - + delete rewardFormula; delete result; } diff --git a/test/functional/parser/CslParserTest.cpp b/test/functional/parser/CslParserTest.cpp index 2ebd8ea16..ebf7250a9 100644 --- a/test/functional/parser/CslParserTest.cpp +++ b/test/functional/parser/CslParserTest.cpp @@ -127,14 +127,9 @@ TEST(CslParserTest, parseComplexFormulaTest) { } - - TEST(CslParserTest, wrongProbabilisticFormulaTest) { storm::parser::CslParser* cslParser = nullptr; - ASSERT_THROW( - cslParser = new storm::parser::CslParser("P > 0.5 [ a ]"), - storm::exceptions::WrongFormatException - ); + ASSERT_THROW(cslParser = new storm::parser::CslParser("P > 0.5 [ a ]"), storm::exceptions::WrongFormatException); delete cslParser; } diff --git a/test/functional/parser/ParseMdpTest.cpp b/test/functional/parser/ParseMdpTest.cpp index 55da2ae32..dfaa0ac15 100644 --- a/test/functional/parser/ParseMdpTest.cpp +++ b/test/functional/parser/ParseMdpTest.cpp @@ -13,8 +13,8 @@ TEST(ParseMdpTest, parseAndOutput) { storm::parser::NondeterministicModelParser* mdpParser = nullptr; ASSERT_NO_THROW(mdpParser = new storm::parser::NondeterministicModelParser( - STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general_input_01.tra", - STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab")); + STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general_input_01.tra", + STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general_input_01.lab")); std::shared_ptr> mdp = mdpParser->getMdp(); std::shared_ptr> matrix = mdp->getTransitionMatrix(); diff --git a/test/functional/parser/ReadLabFileTest.cpp b/test/functional/parser/ReadLabFileTest.cpp index b17f91738..2c3122209 100644 --- a/test/functional/parser/ReadLabFileTest.cpp +++ b/test/functional/parser/ReadLabFileTest.cpp @@ -25,7 +25,7 @@ TEST(ReadLabFileTest, ParseTest) { storm::parser::AtomicPropositionLabelingParser* parser = nullptr; //Parsing the file - ASSERT_NO_THROW(parser = new storm::parser::AtomicPropositionLabelingParser(12, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab")); + ASSERT_NO_THROW(parser = new storm::parser::AtomicPropositionLabelingParser(12, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general_input_01.lab")); std::shared_ptr labeling(parser->getLabeling()); //Checking whether all propositions are in the labelling @@ -89,14 +89,14 @@ TEST(ReadLabFileTest, ParseTest) { } TEST(ReadLabFileTest, WrongHeaderTest1) { - ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header1.lab"), storm::exceptions::WrongFormatException); + ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/wrong_format_header1.lab"), storm::exceptions::WrongFormatException); } TEST(ReadLabFileTest, WrongHeaderTest2) { - ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header2.lab"), storm::exceptions::WrongFormatException); + ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/wrong_format_header2.lab"), storm::exceptions::WrongFormatException); } TEST(ReadLabFileTest, WrongPropositionTest) { - ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_proposition.lab"), storm::exceptions::WrongFormatException); + ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/wrong_format_proposition.lab"), storm::exceptions::WrongFormatException); } diff --git a/test/functional/parser/ReadTraFileTest.cpp b/test/functional/parser/ReadTraFileTest.cpp index 35ecfcbcc..fd86a8820 100644 --- a/test/functional/parser/ReadTraFileTest.cpp +++ b/test/functional/parser/ReadTraFileTest.cpp @@ -21,7 +21,7 @@ TEST(ReadTraFileTest, NonExistingFileTest) { */ TEST(ReadTraFileTest, ParseFileTest1) { storm::parser::DeterministicSparseTransitionParser* parser = nullptr; - ASSERT_NO_THROW(parser = new storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/csl_general_input_01.tra")); + ASSERT_NO_THROW(parser = new storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/csl_general_input_01.tra")); std::shared_ptr> result = parser->getMatrix(); if (result != nullptr) { @@ -73,13 +73,13 @@ TEST(ReadTraFileTest, ParseFileTest1) { } TEST(ReadTraFileTest, WrongFormatTestHeader1) { - ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header1.tra"), storm::exceptions::WrongFormatException); + ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/wrong_format_header1.tra"), storm::exceptions::WrongFormatException); } TEST(ReadTraFileTest, WrongFormatTestHeader2) { - ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header2.tra"), storm::exceptions::WrongFormatException); + ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/wrong_format_header2.tra"), storm::exceptions::WrongFormatException); } TEST(ReadTraFileTest, WrongFormatTestTransition) { - ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_transition.tra"), storm::exceptions::WrongFormatException); + ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/wrong_format_transition.tra"), storm::exceptions::WrongFormatException); } diff --git a/test/functional/storm-functional-tests.cpp b/test/functional/storm-functional-tests.cpp index e5d78bb5e..7139bed3c 100644 --- a/test/functional/storm-functional-tests.cpp +++ b/test/functional/storm-functional-tests.cpp @@ -15,7 +15,7 @@ log4cplus::Logger logger; * Initializes the logging framework. */ void setUpLogging() { - log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender("storm-tests.log")); + log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender("storm-functional-tests.log")); fileLogAppender->setName("mainFileAppender"); fileLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M} (%r ms) - %F:%L : %m%n"))); logger = log4cplus::Logger::getInstance("mainLogger"); @@ -58,7 +58,7 @@ int main(int argc, char* argv[]) { if (!parseOptions(argc, argv)) { return 0; } - std::cout << "STORM Testing Suite" << std::endl; + std::cout << "StoRM (Functional) Testing Suite" << std::endl; testing::InitGoogleTest(&argc, argv); From 6ba1cf25c88577de6571219f1580da6661caf25c Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 14 May 2013 13:28:19 +0200 Subject: [PATCH 04/18] Added new variable for base bath for project root. Changed test input files to the files from example folder. Added leader4.lab to asynchronous leader election example. --- CMakeLists.txt | 4 +- examples/mdp/two_dice/two_dice.nm | 2 +- src/modelchecker/SparseMdpPrctlModelChecker.h | 2 +- storm-config.h.in | 3 +- .../GmmxxDtmcPrctModelCheckerTest.cpp | 6 +- .../GmmxxMdpPrctModelCheckerTest.cpp | 8 +-- .../modelchecker/die/testFormulas.prctl | 4 -- test/performance/storm-performance-tests.cpp | 66 +++++++++++++++++++ 8 files changed, 79 insertions(+), 16 deletions(-) delete mode 100644 test/functional/modelchecker/die/testFormulas.prctl create mode 100644 test/performance/storm-performance-tests.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index a99f224da..744e10d9b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -130,8 +130,8 @@ file(GLOB_RECURSE STORM_IR_FILES ${PROJECT_SOURCE_DIR}/src/ir/*.h ${PROJECT_SOUR # Test Sources # Note that the tests also need the source files, except for the main file -file(GLOB_RECURSE STORM_FUNCTIONAL_TEST_FILES ${PROJECT_SOURCE_DIR}/test/functional/*.h ${PROJECT_SOURCE_DIR}/test/functional/*.cpp) -file(GLOB_RECURSE STORM_PERFORMANCE_TEST_FILES ${PROJECT_SOURCE_DIR}/test/performance/*.h ${PROJECT_SOURCE_DIR}/test/performance/*.cpp) +file(GLOB_RECURSE STORM_FUNCTIONAL_TEST_FILES ${STORM_CPP_TESTS_BASE_PATH}/functional/*.h ${STORM_CPP_TESTS_BASE_PATH}/functional/*.cpp) +file(GLOB_RECURSE STORM_PERFORMANCE_TEST_FILES ${STORM_CPP_TESTS_BASE_PATH}/performance/*.h ${STORM_CPP_TESTS_BASE_PATH}/performance/*.cpp) # Group the headers and sources source_group(main FILES ${STORM_MAIN_FILE}) diff --git a/examples/mdp/two_dice/two_dice.nm b/examples/mdp/two_dice/two_dice.nm index e1bf34aea..778153138 100644 --- a/examples/mdp/two_dice/two_dice.nm +++ b/examples/mdp/two_dice/two_dice.nm @@ -17,7 +17,7 @@ module die1 [] s1=4 -> 0.5 : (s1'=7) & (d1'=2) + 0.5 : (s1'=7) & (d1'=3); [] s1=5 -> 0.5 : (s1'=7) & (d1'=4) + 0.5 : (s1'=7) & (d1'=5); [] s1=6 -> 0.5 : (s1'=2) + 0.5 : (s1'=7) & (d1'=6); - [] s1=7 & s2=7 -> (s1'=7); + [] s1=7 & s2=7 -> 1: (s1'=7); endmodule module die2 = die1 [ s1=s2, s2=s1, d1=d2 ] endmodule diff --git a/src/modelchecker/SparseMdpPrctlModelChecker.h b/src/modelchecker/SparseMdpPrctlModelChecker.h index b9c80e24b..0c951ae8f 100644 --- a/src/modelchecker/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/SparseMdpPrctlModelChecker.h @@ -99,7 +99,7 @@ public: // Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates, *this->getModel().getNondeterministicChoiceIndices()); - + // Create the vector with which to multiply. std::vector* result = new std::vector(this->getModel().getNumberOfStates()); storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne()); diff --git a/storm-config.h.in b/storm-config.h.in index bb44dec25..0b1cd5134 100644 --- a/storm-config.h.in +++ b/storm-config.h.in @@ -1,4 +1,5 @@ // the configured options and settings for STORM #define STORM_CPP_VERSION_MAJOR @STORM_CPP_VERSION_MAJOR@ #define STORM_CPP_VERSION_MINOR @STORM_CPP_VERSION_MINOR@ -#define STORM_CPP_TESTS_BASE_PATH "@STORM_CPP_TESTS_BASE_PATH@" \ No newline at end of file +#define STORM_CPP_BASE_PATH "@PROJECT_SOURCE_DIR@" +#define STORM_CPP_TESTS_BASE_PATH "@STORM_CPP_TESTS_BASE_PATH@" diff --git a/test/functional/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index 2286cd8d9..e3eb08b68 100644 --- a/test/functional/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -8,7 +8,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Die) { storm::settings::Settings* s = storm::settings::instance(); s->set("fix-deadlocks"); - storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/die/die.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/die/die.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/die/die.coin_flips.trans.rew"); + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew"); ASSERT_EQ(parser.getType(), storm::models::DTMC); @@ -75,7 +75,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Die) { TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { storm::settings::Settings* s = storm::settings::instance(); s->set("fix-deadlocks"); - storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/crowds/crowds5_5.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/crowds/crowds5_5.lab", "", ""); + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", ""); ASSERT_EQ(parser.getType(), storm::models::DTMC); @@ -129,7 +129,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { storm::settings::Settings* s = storm::settings::instance(); s->set("fix-deadlocks"); - storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/synchronous_leader/leader4_8.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/synchronous_leader/leader4_8.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/synchronous_leader/leader4_8.pick.trans.rew"); + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.pick.trans.rew"); ASSERT_EQ(parser.getType(), storm::models::DTMC); diff --git a/test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp index b440df38d..32cf5b9a4 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp @@ -7,7 +7,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { storm::settings::Settings* s = storm::settings::instance(); - storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.flip.trans.rew"); + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew"); ASSERT_EQ(parser.getType(), storm::models::MDP); @@ -108,7 +108,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { delete rewardFormula; delete result; - storm::parser::AutoParser stateRewardParser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.lab", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.flip.state.rew", ""); + storm::parser::AutoParser stateRewardParser(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", ""); ASSERT_EQ(stateRewardParser.getType(), storm::models::MDP); @@ -138,7 +138,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { delete rewardFormula; delete result; - storm::parser::AutoParser stateAndTransitionRewardParser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.lab", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.flip.state.rew", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.flip.trans.rew"); + storm::parser::AutoParser stateAndTransitionRewardParser(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew"); ASSERT_EQ(stateAndTransitionRewardParser.getType(), storm::models::MDP); @@ -171,7 +171,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { storm::settings::Settings* s = storm::settings::instance(); - storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/asynchronous_leader/leader4.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/asynchronous_leader/leader4.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/asynchronous_leader/leader4.trans.rew"); + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew"); ASSERT_EQ(parser.getType(), storm::models::MDP); diff --git a/test/functional/modelchecker/die/testFormulas.prctl b/test/functional/modelchecker/die/testFormulas.prctl deleted file mode 100644 index 8deea6c43..000000000 --- a/test/functional/modelchecker/die/testFormulas.prctl +++ /dev/null @@ -1,4 +0,0 @@ -P=? [ F one ] -P=? [ F two ] -P=? [ F three ] -R=? [ F done ] diff --git a/test/performance/storm-performance-tests.cpp b/test/performance/storm-performance-tests.cpp new file mode 100644 index 000000000..1e1317a80 --- /dev/null +++ b/test/performance/storm-performance-tests.cpp @@ -0,0 +1,66 @@ +#include + +#include "gtest/gtest.h" +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" +#include "log4cplus/consoleappender.h" +#include "log4cplus/fileappender.h" + +#include "src/utility/Settings.h" +#include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h" + +log4cplus::Logger logger; + +/*! + * Initializes the logging framework. + */ +void setUpLogging() { + log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender("storm-functional-tests.log")); + fileLogAppender->setName("mainFileAppender"); + fileLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M} (%r ms) - %F:%L : %m%n"))); + logger = log4cplus::Logger::getInstance("mainLogger"); + logger.addAppender(fileLogAppender); + + // Uncomment these lines to enable console logging output + // log4cplus::SharedAppenderPtr consoleLogAppender(new log4cplus::ConsoleAppender()); + // consoleLogAppender->setName("mainConsoleAppender"); + // consoleLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%s} (%r ms) - %F:%L : %m%n"))); + // logger.addAppender(consoleLogAppender); +} + +/*! + * Function that parses the command line options. + * @param argc The argc argument of main(). + * @param argv The argv argument of main(). + * @return True iff the program should continue to run after parsing the options. + */ +bool parseOptions(int const argc, char const * const argv[]) { + storm::settings::Settings* s = nullptr; + try { + storm::settings::Settings::registerModule>(); + s = storm::settings::newInstance(argc, argv, nullptr, true); + } catch (storm::exceptions::InvalidSettingsException& e) { + std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl; + std::cout << std::endl << storm::settings::help; + return false; + } + + if (s->isSet("help")) { + std::cout << storm::settings::help; + return false; + } + + return true; +} + +int main(int argc, char* argv[]) { + setUpLogging(); + if (!parseOptions(argc, argv)) { + return 0; + } + std::cout << "StoRM (Performance) Testing Suite" << std::endl; + + testing::InitGoogleTest(&argc, argv); + + return RUN_ALL_TESTS(); +} From 5149a7a9436387cd4fe9d9f0a5a9cc1d3d598de3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 14 May 2013 15:01:01 +0200 Subject: [PATCH 05/18] Added lab files for asynch_leader and corrected pctl file a bit. Included first (incorrect) tests for performance test suite. --- examples/mdp/asynchronous_leader/leader.pctl | 6 +- .../GmmxxDtmcPrctModelCheckerTest.cpp | 116 ++++++++++ .../GmmxxMdpPrctModelCheckerTest.cpp | 217 ++++++++++++++++++ 3 files changed, 336 insertions(+), 3 deletions(-) create mode 100644 test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp create mode 100644 test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp diff --git a/examples/mdp/asynchronous_leader/leader.pctl b/examples/mdp/asynchronous_leader/leader.pctl index bb8fb1b82..2c87c7f27 100644 --- a/examples/mdp/asynchronous_leader/leader.pctl +++ b/examples/mdp/asynchronous_leader/leader.pctl @@ -1,8 +1,8 @@ Pmin=? [ F elected ] -const int K = 25; -Pmin=? [ F<=K elected ] -Pmax=? [ F<=K elected ] +// const int K = 25; +Pmin=? [ F<=25 elected ] +Pmax=? [ F<=25 elected ] Rmin=? [ F elected ] Rmax=? [ F elected ] diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp new file mode 100644 index 000000000..87bcf8ef6 --- /dev/null +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -0,0 +1,116 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/utility/Settings.h" +#include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h" +#include "src/parser/AutoParser.h" + +TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { + storm::settings::Settings* s = storm::settings::instance(); + s->set("fix-deadlocks"); + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); + + ASSERT_EQ(parser.getType(), storm::models::DTMC); + + std::shared_ptr> dtmc = parser.getModel>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 8607u); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460u); + + storm::modelchecker::GmmxxDtmcPrctlModelChecker mc(*dtmc); + + storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("observe0Greater1"); + storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); + storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); + + std::vector* result = probFormula->check(mc); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 0.3328800375801578281), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("observeIGreater1"); + eventuallyFormula = new storm::property::prctl::Eventually(apFormula); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); + + result = probFormula->check(mc); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 0.1522173670950556501), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("observeOnlyTrueSender"); + eventuallyFormula = new storm::property::prctl::Eventually(apFormula); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); + + result = probFormula->check(mc); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 0.32153724292835045), s->get("precision")); + + delete probFormula; + delete result; +} + +/* +TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { + storm::settings::Settings* s = storm::settings::instance(); + s->set("fix-deadlocks"); + 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", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew"); + + ASSERT_EQ(parser.getType(), storm::models::DTMC); + + std::shared_ptr> dtmc = parser.getModel>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 12400u); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894u); + + storm::modelchecker::GmmxxDtmcPrctlModelChecker mc(*dtmc); + + storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("elected"); + storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); + storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); + + std::vector* result = probFormula->check(mc); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 1), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("elected"); + storm::property::prctl::BoundedUntil* boundedUntilFormula = new storm::property::prctl::BoundedUntil(new storm::property::prctl::Ap("true"), apFormula, 20); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedUntilFormula); + + result = probFormula->check(mc); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 0.9999965911265462636), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("elected"); + storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); + storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula); + + result = rewardFormula->check(mc); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 1.0448979591835938496), s->get("precision")); + + delete rewardFormula; + delete result; +} +*/ \ No newline at end of file diff --git a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp new file mode 100644 index 000000000..322dafe8e --- /dev/null +++ b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp @@ -0,0 +1,217 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/utility/Settings.h" +#include "src/modelchecker/GmmxxMdpPrctlModelChecker.h" +#include "src/parser/AutoParser.h" + +TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { + storm::settings::Settings* s = storm::settings::instance(); + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew"); + + ASSERT_EQ(parser.getType(), storm::models::MDP); + + std::shared_ptr> mdp = parser.getModel>(); + + ASSERT_EQ(mdp->getNumberOfStates(), 3172u); + ASSERT_EQ(mdp->getNumberOfTransitions(), 7144u); + + storm::modelchecker::GmmxxMdpPrctlModelChecker mc(*mdp); + + storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("elected"); + storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); + storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + + std::vector* result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 1), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("elected"); + eventuallyFormula = new storm::property::prctl::Eventually(apFormula); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); + + result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 1), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("elected"); + storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); + + result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("elected"); + boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); + + result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("elected"); + storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); + storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); + + result = mc.checkNoBoundOperator(*rewardFormula); + + ASSERT_LT(std::abs((*result)[0] - 4.28568908480604982), s->get("precision")); + + delete rewardFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("elected"); + reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); + rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); + + result = mc.checkNoBoundOperator(*rewardFormula);; + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 4.2856904354441400784), s->get("precision")); + + delete rewardFormula; + delete result; +} + +TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { + storm::settings::Settings* s = storm::settings::instance(); + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_6.steps.state.rew", ""); + + ASSERT_EQ(parser.getType(), storm::models::MDP); + + std::shared_ptr> mdp = parser.getModel>(); + + storm::modelchecker::GmmxxMdpPrctlModelChecker mc(*mdp); + + storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("finished"); + storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); + storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + + std::vector* result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 1), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("finished"); + storm::property::prctl::Ap* apFormula2 = new storm::property::prctl::Ap("all_coins_equal_0"); + storm::property::prctl::And* andFormula = new storm::property::prctl::And(apFormula, apFormula2); + eventuallyFormula = new storm::property::prctl::Eventually(andFormula); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + + result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 1), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("finished"); + apFormula2 = new storm::property::prctl::Ap("all_coins_equal_1"); + andFormula = new storm::property::prctl::And(apFormula, apFormula2); + eventuallyFormula = new storm::property::prctl::Eventually(andFormula); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + + result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 1), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("finished"); + apFormula2 = new storm::property::prctl::Ap("agree"); + storm::property::prctl::Not* notFormula = new storm::property::prctl::Not(apFormula2); + andFormula = new storm::property::prctl::And(apFormula, notFormula); + eventuallyFormula = new storm::property::prctl::Eventually(andFormula); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + + result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 1), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("finished"); + storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 50); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); + + result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("finished"); + boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 50); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); + + result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("finished"); + storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); + storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); + + result = mc.checkNoBoundOperator(*rewardFormula); + + ASSERT_LT(std::abs((*result)[0] - 4.28568908480604982), s->get("precision")); + + delete rewardFormula; + delete result; + + apFormula = new storm::property::prctl::Ap("finished"); + reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); + rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); + + result = mc.checkNoBoundOperator(*rewardFormula);; + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 4.2856904354441400784), s->get("precision")); + + delete rewardFormula; + delete result; + +} \ No newline at end of file From c8e8e1502b5886b8fbe0b3e2d819b9308d4a71fc Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 14 May 2013 16:39:55 +0200 Subject: [PATCH 06/18] Added minimum/maximum support for probablistic no bound operators. --- src/parser/PrctlParser.cpp | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index c79485dc0..f1a8ad4ef 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -83,7 +83,15 @@ struct PrctlParser::PrctlGrammar : qi::grammar> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = + probabilisticNoBoundOperator = (probabilisticMinimumNoBoundOperator | probabilisticMaximumNoBoundOperator | probabilisticDeterministicNoBoundOperator); + + probabilisticMinimumNoBoundOperator = (qi::lit("P") >> qi::lit("min") >> qi::lit("=") >> qi::lit("?") > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, true)]; + + probabilisticMaximumNoBoundOperator = (qi::lit("P") >> qi::lit("max") >> qi::lit("=") >> qi::lit("?") > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, false)]; + + probabilisticDeterministicNoBoundOperator = (qi::lit("P") >> qi::lit("=") >> qi::lit("?") > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::new_ >(qi::_1)]; probabilisticNoBoundOperator.name("no bound operator"); rewardNoBoundOperator = (qi::lit("R") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val = @@ -141,6 +149,9 @@ struct PrctlParser::PrctlGrammar : qi::grammar*(), Skipper> noBoundOperator; qi::rule*(), Skipper> probabilisticNoBoundOperator; + qi::rule*(), Skipper> probabilisticMinimumNoBoundOperator; + qi::rule*(), Skipper> probabilisticMaximumNoBoundOperator; + qi::rule*(), Skipper> probabilisticDeterministicNoBoundOperator; qi::rule*(), Skipper> rewardNoBoundOperator; qi::rule*(), Skipper> pathFormula; From 6a1f6fbcee7a2a688161286995bc5f4a902fa4c6 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Wed, 15 May 2013 14:26:43 +0200 Subject: [PATCH 07/18] Parser changed to support P and R operators annotated with min/max. --- src/formula/abstract/PathBoundOperator.h | 2 +- src/parser/PrctlFileParser.cpp | 7 ++ src/parser/PrctlParser.cpp | 84 +++++++++++++----------- 3 files changed, 55 insertions(+), 38 deletions(-) diff --git a/src/formula/abstract/PathBoundOperator.h b/src/formula/abstract/PathBoundOperator.h index 34a6f0732..03454b3c5 100644 --- a/src/formula/abstract/PathBoundOperator.h +++ b/src/formula/abstract/PathBoundOperator.h @@ -70,7 +70,7 @@ public: * @param minimumOperator Indicator, if operator should be minimum or maximum operator. */ PathBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, FormulaType* pathFormula, bool minimumOperator) - : comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula), OptimizingOperator(minimumOperator) { + : OptimizingOperator(minimumOperator), comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) { // Intentionally left empty } diff --git a/src/parser/PrctlFileParser.cpp b/src/parser/PrctlFileParser.cpp index ed5f15a2b..0f7f877f1 100644 --- a/src/parser/PrctlFileParser.cpp +++ b/src/parser/PrctlFileParser.cpp @@ -13,6 +13,8 @@ #include "modelchecker/GmmxxDtmcPrctlModelChecker.h" #include "modelchecker/GmmxxMdpPrctlModelChecker.h" +#include + namespace storm { namespace parser { @@ -39,6 +41,11 @@ std::list*> PrctlFileParser std::string line; //The while loop reads the input file line by line while (std::getline(inputFileStream, line)) { + boost::algorithm::trim(line); + if ((line.length() == 0) || ((line[0] == '/') && (line[1] == '/'))) { + // ignore empty lines and lines starting with // + continue; + } PrctlParser parser(line); result.push_back(parser.getFormula()); } diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index f1a8ad4ef..07cf79b7a 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -35,7 +35,15 @@ namespace parser { template struct PrctlParser::PrctlGrammar : qi::grammar*(), Skipper > { PrctlGrammar() : PrctlGrammar::base_type(start) { + + //This block contains helper rules that may be used several times freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))]; + comparisonType = ( + (qi::lit(">="))[qi::_val = storm::property::GREATER_EQUAL] | + (qi::lit(">"))[qi::_val = storm::property::GREATER] | + (qi::lit("<="))[qi::_val = storm::property::LESS_EQUAL] | + (qi::lit("<"))[qi::_val = storm::property::LESS]); + comment = qi::lit("//") //This block defines rules for parsing state formulas stateFormula %= orFormula; @@ -58,44 +66,47 @@ struct PrctlParser::PrctlGrammar : qi::grammar>(qi::_1)]; atomicProposition.name("state formula"); probabilisticBoundOperator = ( - (qi::lit("P") >> qi::lit(">") >> qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::GREATER, qi::_1, qi::_2)] | - (qi::lit("P") >> qi::lit(">=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::GREATER_EQUAL, qi::_1, qi::_2)] | - (qi::lit("P") >> qi::lit("<") >> qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::LESS, qi::_1, qi::_2)] | - (qi::lit("P") >> qi::lit("<=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::LESS_EQUAL, qi::_1, qi::_2)] + (qi::lit("P") >> qi::lit("min") > comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, qi::_2, qi::_3, true)] | + (qi::lit("P") >> qi::lit("max") > comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, qi::_2, qi::_3, false)] | + (qi::lit("P") > comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, qi::_2, qi::_3)] ); + probabilisticBoundOperator.name("state formula"); rewardBoundOperator = ( - (qi::lit("R") >> qi::lit(">") >> qi::double_ >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::GREATER, qi::_1, qi::_2)] | - (qi::lit("R") >> qi::lit(">=") >> qi::double_ >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::GREATER_EQUAL, qi::_1, qi::_2)] | - (qi::lit("R") >> qi::lit("<") >> qi::double_ >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::LESS, qi::_1, qi::_2)] | - (qi::lit("R") >> qi::lit("<=")>> qi::double_ >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::LESS_EQUAL, qi::_1, qi::_2)] + (qi::lit("R") >> qi::lit("min") > comparisonType > qi::double_ > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, qi::_2, qi::_3, true)] | + (qi::lit("R") >> qi::lit("max") > comparisonType > qi::double_ > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, qi::_2, qi::_3, false)] | + (qi::lit("R") >> comparisonType > qi::double_ > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, qi::_2, qi::_3)] ); rewardBoundOperator.name("state formula"); //This block defines rules for parsing formulas with noBoundOperators noBoundOperator = (probabilisticNoBoundOperator | rewardNoBoundOperator); noBoundOperator.name("no bound operator"); - probabilisticNoBoundOperator = (probabilisticMinimumNoBoundOperator | probabilisticMaximumNoBoundOperator | probabilisticDeterministicNoBoundOperator); - - probabilisticMinimumNoBoundOperator = (qi::lit("P") >> qi::lit("min") >> qi::lit("=") >> qi::lit("?") > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(qi::_1, true)]; + probabilisticNoBoundOperator = ( + (qi::lit("P") >> qi::lit("min") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, true)] | + (qi::lit("P") >> qi::lit("max") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, false)] | + (qi::lit("P") >> qi::lit("=") >> qi::lit("?") > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1)] + ); + probabilisticNoBoundOperator.name("no bound operator"); - probabilisticMaximumNoBoundOperator = (qi::lit("P") >> qi::lit("max") >> qi::lit("=") >> qi::lit("?") > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(qi::_1, false)]; + rewardNoBoundOperator = ( + (qi::lit("R") >> qi::lit("min") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, true)] | + (qi::lit("R") >> qi::lit("max") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, false)] | + (qi::lit("R") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1)] - probabilisticDeterministicNoBoundOperator = (qi::lit("P") >> qi::lit("=") >> qi::lit("?") > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(qi::_1)]; - probabilisticNoBoundOperator.name("no bound operator"); - rewardNoBoundOperator = (qi::lit("R") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val = - phoenix::new_ >(qi::_1)]; + ); rewardNoBoundOperator.name("no bound operator"); //This block defines rules for parsing probabilistic path formulas @@ -103,19 +114,19 @@ struct PrctlParser::PrctlGrammar : qi::grammar> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val = phoenix::new_>(qi::_2, qi::_1)]; - boundedEventually.name("path formula (for probablistic operator)"); + boundedEventually.name("path formula (for probabilistic operator)"); eventually = (qi::lit("F") > stateFormula)[qi::_val = phoenix::new_ >(qi::_1)]; - eventually.name("path formula (for probablistic operator)"); + eventually.name("path formula (for probabilistic operator)"); globally = (qi::lit("G") > stateFormula)[qi::_val = phoenix::new_ >(qi::_1)]; - globally.name("path formula (for probablistic operator)"); + globally.name("path formula (for probabilistic operator)"); boundedUntil = (stateFormula[qi::_a = phoenix::construct>>(qi::_1)] >> qi::lit("U") >> qi::lit("<=") > qi::int_ > stateFormula) [qi::_val = phoenix::new_>(phoenix::bind(&storm::property::prctl::AbstractStateFormula::clone, phoenix::bind(&std::shared_ptr>::get, qi::_a)), qi::_3, qi::_2)]; - boundedUntil.name("path formula (for probablistic operator)"); + boundedUntil.name("path formula (for probabilistic operator)"); until = (stateFormula[qi::_a = phoenix::construct>>(qi::_1)] >> qi::lit("U") > stateFormula)[qi::_val = phoenix::new_>(phoenix::bind(&storm::property::prctl::AbstractStateFormula::clone, phoenix::bind(&std::shared_ptr>::get, qi::_a)), qi::_2)]; - until.name("path formula (for probablistic operator)"); + until.name("path formula (for probabilistic operator)"); //This block defines rules for parsing reward path formulas rewardPathFormula = (cumulativeReward | reachabilityReward | instantaneousReward | steadyStateReward); @@ -131,11 +142,12 @@ struct PrctlParser::PrctlGrammar : qi::grammar>()]; - start = (noBoundOperator | stateFormula); + start = (comment | noBoundOperator | stateFormula | qi::eps[qi::error()]); start.name("PRCTL formula"); } qi::rule*(), Skipper> start; + qi::rule*(), Skipper> comment; qi::rule*(), Skipper> stateFormula; qi::rule*(), Skipper> atomicStateFormula; @@ -149,9 +161,6 @@ struct PrctlParser::PrctlGrammar : qi::grammar*(), Skipper> noBoundOperator; qi::rule*(), Skipper> probabilisticNoBoundOperator; - qi::rule*(), Skipper> probabilisticMinimumNoBoundOperator; - qi::rule*(), Skipper> probabilisticMaximumNoBoundOperator; - qi::rule*(), Skipper> probabilisticDeterministicNoBoundOperator; qi::rule*(), Skipper> rewardNoBoundOperator; qi::rule*(), Skipper> pathFormula; @@ -169,6 +178,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar freeIdentifierName; + qi::rule comparisonType; }; @@ -221,7 +231,7 @@ storm::parser::PrctlParser::PrctlParser(std::string formulaString) { // The syntax can be so wrong that no rule can be matched at all // In that case, no expectation failure is thrown, but the parser just returns nullptr // Then, of course the result is not usable, hence we throw a WrongFormatException, too. - if (result_pointer == nullptr) { + if (positionIteratorBegin != formulaString.end()) { throw storm::exceptions::WrongFormatException() << "Syntax error in formula"; } From a956fc782acf82a9506331fcbb506a81f1aee7b9 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Wed, 15 May 2013 16:25:38 +0200 Subject: [PATCH 08/18] Added support for atomic propositions containing numbers. --- src/parser/PrctlParser.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index 07cf79b7a..18f470660 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -37,13 +37,13 @@ struct PrctlParser::PrctlGrammar : qi::grammar> *(qi::alnum | qi::char_('_'))]; comparisonType = ( (qi::lit(">="))[qi::_val = storm::property::GREATER_EQUAL] | (qi::lit(">"))[qi::_val = storm::property::GREATER] | (qi::lit("<="))[qi::_val = storm::property::LESS_EQUAL] | (qi::lit("<"))[qi::_val = storm::property::LESS]); - comment = qi::lit("//") + comment = (qi::lit("//") >> *(qi::char_))[qi::_val = nullptr]; //This block defines rules for parsing state formulas stateFormula %= orFormula; @@ -142,7 +142,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar>()]; - start = (comment | noBoundOperator | stateFormula | qi::eps[qi::error()]); + start = (comment | noBoundOperator | stateFormula) >> qi::eoi; start.name("PRCTL formula"); } @@ -231,7 +231,7 @@ storm::parser::PrctlParser::PrctlParser(std::string formulaString) { // The syntax can be so wrong that no rule can be matched at all // In that case, no expectation failure is thrown, but the parser just returns nullptr // Then, of course the result is not usable, hence we throw a WrongFormatException, too. - if (positionIteratorBegin != formulaString.end()) { + if (positionIteratorBegin != positionIteratorEnd) { throw storm::exceptions::WrongFormatException() << "Syntax error in formula"; } From b5baae58619b4839ac2124870ff2892f9b8f113e Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 15 May 2013 10:41:25 +0200 Subject: [PATCH 09/18] Added 3 missing example files for synchronous leader election protocol. Set release optimization level for clang to O3. --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 744e10d9b..a78fb8925 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -95,7 +95,7 @@ else(CLANG) # As CLANG is not set as a variable, we need to set it in case we have not matched another compiler. set (CLANG ON) # Set standard flags for clang - set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O4") + set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O3") set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=libc++ -Wall -Werror -pedantic -Wno-unused-variable -DBOOST_RESULT_OF_USE_TR1 -DBOOST_NO_DECLTYPE") set (CMAKE_CXX_FLAGS_DEBUG "-g") From 9ed1fa19e20c74aaee1915b2db049849096c8e52 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 15 May 2013 18:25:20 +0200 Subject: [PATCH 10/18] Added some example files. --- examples/dtmc/synchronous_leader/leader.pctl | 3 ++- examples/mdp/consensus/coin.pctl | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/examples/dtmc/synchronous_leader/leader.pctl b/examples/dtmc/synchronous_leader/leader.pctl index b14536d80..c4eb53408 100644 --- a/examples/dtmc/synchronous_leader/leader.pctl +++ b/examples/dtmc/synchronous_leader/leader.pctl @@ -1,3 +1,4 @@ P=? [ F elected ] -P=? [ F<=(4*(N+1)) elected ] +// P=? [ F<=(4*(N+1)) elected ] +P=? [ F<=28 elected ] R=? [ F elected ] diff --git a/examples/mdp/consensus/coin.pctl b/examples/mdp/consensus/coin.pctl index aa371d50b..edd87a453 100644 --- a/examples/mdp/consensus/coin.pctl +++ b/examples/mdp/consensus/coin.pctl @@ -11,8 +11,8 @@ Pmin=? [ F finished & all_coins_equal_1 ] Pmax=? [ F finished & !agree ] // Min/max probability of finishing within k steps -Pmin=? [ F<=k finished ] -Pmax=? [ F<=k finished ] +Pmin=? [ F<=50 finished ] +Pmax=? [ F<=50 finished ] // Min/max expected steps to finish Rmin=? [ F finished ] From 8c329933ec7663d765526a9e7d22e960ec4355fd Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 15 May 2013 18:26:07 +0200 Subject: [PATCH 11/18] Began correcting performance tests. --- .../GmmxxDtmcPrctModelCheckerTest.cpp | 21 ++++++------ .../GmmxxMdpPrctModelCheckerTest.cpp | 33 ++++++++++--------- 2 files changed, 28 insertions(+), 26 deletions(-) diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index 87bcf8ef6..4ce527d7e 100644 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -14,8 +14,8 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { std::shared_ptr> dtmc = parser.getModel>(); - ASSERT_EQ(dtmc->getNumberOfStates(), 8607u); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460u); + ASSERT_EQ(dtmc->getNumberOfStates(), 2036647u); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 8973900u); storm::modelchecker::GmmxxDtmcPrctlModelChecker mc(*dtmc); @@ -27,7 +27,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 0.3328800375801578281), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 0.2296803699), s->get("precision")); delete probFormula; delete result; @@ -40,7 +40,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 0.1522173670950556501), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 0.05072232915), s->get("precision")); delete probFormula; delete result; @@ -53,13 +53,13 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 0.32153724292835045), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 0.2274230551), s->get("precision")); delete probFormula; delete result; } -/* + TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { storm::settings::Settings* s = storm::settings::instance(); s->set("fix-deadlocks"); @@ -69,8 +69,8 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { std::shared_ptr> dtmc = parser.getModel>(); - ASSERT_EQ(dtmc->getNumberOfStates(), 12400u); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894u); + ASSERT_EQ(dtmc->getNumberOfStates(), 1312334u); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 2886810u); storm::modelchecker::GmmxxDtmcPrctlModelChecker mc(*dtmc); @@ -95,7 +95,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 0.9999965911265462636), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 0.9999996339), s->get("precision")); delete probFormula; delete result; @@ -108,9 +108,8 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 1.0448979591835938496), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 1.025217446), s->get("precision")); delete rewardFormula; delete result; } -*/ \ No newline at end of file diff --git a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp index 322dafe8e..82c43a4fc 100644 --- a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp @@ -13,8 +13,8 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { std::shared_ptr> mdp = parser.getModel>(); - ASSERT_EQ(mdp->getNumberOfStates(), 3172u); - ASSERT_EQ(mdp->getNumberOfTransitions(), 7144u); + ASSERT_EQ(mdp->getNumberOfStates(), 2095783u); + ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385u); storm::modelchecker::GmmxxMdpPrctlModelChecker mc(*mdp); @@ -52,7 +52,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 0), s->get("precision")); delete probFormula; delete result; @@ -65,7 +65,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 0), s->get("precision")); delete probFormula; delete result; @@ -76,7 +76,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { result = mc.checkNoBoundOperator(*rewardFormula); - ASSERT_LT(std::abs((*result)[0] - 4.28568908480604982), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 6.172433512), s->get("precision")); delete rewardFormula; delete result; @@ -89,7 +89,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 4.2856904354441400784), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 6.1724344), s->get("precision")); delete rewardFormula; delete result; @@ -97,12 +97,15 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { storm::settings::Settings* s = storm::settings::instance(); - storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_6.steps.state.rew", ""); + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", ""); ASSERT_EQ(parser.getType(), storm::models::MDP); std::shared_ptr> mdp = parser.getModel>(); + ASSERT_EQ(mdp->getNumberOfStates(), 63616u); + ASSERT_EQ(mdp->getNumberOfTransitions(), 213472u); + storm::modelchecker::GmmxxMdpPrctlModelChecker mc(*mdp); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("finished"); @@ -128,7 +131,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 1), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 0.4370098592), s->get("precision")); delete probFormula; delete result; @@ -137,13 +140,13 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { apFormula2 = new storm::property::prctl::Ap("all_coins_equal_1"); andFormula = new storm::property::prctl::And(apFormula, apFormula2); eventuallyFormula = new storm::property::prctl::Eventually(andFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); result = mc.checkNoBoundOperator(*probFormula); ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 1), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 0.4370098592), s->get("precision")); delete probFormula; delete result; @@ -159,7 +162,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 1), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 0.1034345104), s->get("precision")); delete probFormula; delete result; @@ -172,7 +175,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 0), s->get("precision")); delete probFormula; delete result; @@ -185,7 +188,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 0), s->get("precision")); delete probFormula; delete result; @@ -196,7 +199,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { result = mc.checkNoBoundOperator(*rewardFormula); - ASSERT_LT(std::abs((*result)[0] - 4.28568908480604982), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 1725.593313), s->get("precision")); delete rewardFormula; delete result; @@ -209,7 +212,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 4.2856904354441400784), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 2179.014847), s->get("precision")); delete rewardFormula; delete result; From 2fcd6c95fb1ccea8d5fcc1dca08a96c141a1d8f1 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 15 May 2013 20:00:25 +0200 Subject: [PATCH 12/18] Performance tests now run fine (and take about 3 minutes). --- .../GmmxxDtmcPrctModelCheckerTest.cpp | 4 ++-- .../GmmxxMdpPrctModelCheckerTest.cpp | 18 +++++++++--------- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index 4ce527d7e..2609ba0a1 100644 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -95,7 +95,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 0.9999996339), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 0.999394979327824395376467), s->get("precision")); delete probFormula; delete result; @@ -108,7 +108,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 1.025217446), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 1.02521744572240791626427), s->get("precision")); delete rewardFormula; delete result; diff --git a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp index 82c43a4fc..dc9bea32b 100644 --- a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp @@ -116,7 +116,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 1), s->get("precision")); + ASSERT_LT(std::abs((*result)[31168] - 1), s->get("precision")); delete probFormula; delete result; @@ -131,7 +131,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 0.4370098592), s->get("precision")); + ASSERT_LT(std::abs((*result)[31168] - 0.4370098591707694546393), s->get("precision")); delete probFormula; delete result; @@ -146,7 +146,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 0.4370098592), s->get("precision")); + ASSERT_LT(std::abs((*result)[31168] - 0.5282872761373342829216), s->get("precision")); delete probFormula; delete result; @@ -156,13 +156,13 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { storm::property::prctl::Not* notFormula = new storm::property::prctl::Not(apFormula2); andFormula = new storm::property::prctl::And(apFormula, notFormula); eventuallyFormula = new storm::property::prctl::Eventually(andFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); result = mc.checkNoBoundOperator(*probFormula); ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 0.1034345104), s->get("precision")); + ASSERT_LT(std::abs((*result)[31168] - 0.10343451035775527713), s->get("precision")); delete probFormula; delete result; @@ -175,7 +175,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 0), s->get("precision")); + ASSERT_LT(std::abs((*result)[31168] - 0), s->get("precision")); delete probFormula; delete result; @@ -188,7 +188,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 0), s->get("precision")); + ASSERT_LT(std::abs((*result)[31168] - 0), s->get("precision")); delete probFormula; delete result; @@ -199,7 +199,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { result = mc.checkNoBoundOperator(*rewardFormula); - ASSERT_LT(std::abs((*result)[0] - 1725.593313), s->get("precision")); + ASSERT_LT(std::abs((*result)[31168] - 1725.5933133943854045), s->get("precision")); delete rewardFormula; delete result; @@ -212,7 +212,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 2179.014847), s->get("precision")); + ASSERT_LT(std::abs((*result)[31168] - 2179.014847073392047605011), s->get("precision")); delete rewardFormula; delete result; From ed4c6c84293173d86ee7414b8f048dd8c838a0bf Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 15 May 2013 23:51:56 +0200 Subject: [PATCH 13/18] Fixed SCC decomposition functions. Added performance tests for GraphAnalyzer. --- src/models/AbstractDeterministicModel.h | 4 +- src/models/AbstractModel.h | 6 +- src/models/AbstractNondeterministicModel.h | 4 +- src/storage/SparseMatrix.h | 2 +- src/utility/GraphAnalyzer.h | 6 +- test/performance/graph/GraphTest.cpp | 117 ++++++++++++++++++ .../GmmxxDtmcPrctModelCheckerTest.cpp | 3 +- test/performance/storm-performance-tests.cpp | 6 +- 8 files changed, 133 insertions(+), 15 deletions(-) create mode 100644 test/performance/graph/GraphTest.cpp diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index 7048ab3ed..1986aa776 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -52,7 +52,7 @@ class AbstractDeterministicModel: public AbstractModel { * @param state The state for which to return the iterator. * @return An iterator to the successors of the given state. */ - virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) { + virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) const { return this->getTransitionMatrix()->constColumnIteratorBegin(state); } @@ -62,7 +62,7 @@ class AbstractDeterministicModel: public AbstractModel { * @param state The state for which to return the iterator. * @return An iterator pointing to the element past the successors of the given state. */ - virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) { + virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const { return this->getTransitionMatrix()->constColumnIteratorEnd(state); } }; diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index e50aa683f..806cfed67 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -91,7 +91,7 @@ class AbstractModel: public std::enable_shared_from_this> { * @param stronglyConnectedComponents A vector containing the SCCs of the system. * @param stateToSccMap A mapping from state indices to */ - virtual storm::storage::SparseMatrix extractSccDependencyGraph(std::vector> const& stronglyConnectedComponents, std::map const& stateToSccMap) { + storm::storage::SparseMatrix extractSccDependencyGraph(std::vector> const& stronglyConnectedComponents, std::map const& stateToSccMap) const { // The resulting sparse matrix will have as many rows/columns as there are SCCs. uint_fast64_t numberOfStates = stronglyConnectedComponents.size(); storm::storage::SparseMatrix sccDependencyGraph(numberOfStates); @@ -132,7 +132,7 @@ class AbstractModel: public std::enable_shared_from_this> { * @param state The state for which to return the iterator. * @return An iterator to the successors of the given state. */ - virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) = 0; + virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) const = 0; /*! * Returns an iterator pointing to the element past the successors of the given state. @@ -140,7 +140,7 @@ class AbstractModel: public std::enable_shared_from_this> { * @param state The state for which to return the iterator. * @return An iterator pointing to the element past the successors of the given state. */ - virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) = 0; + virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const = 0; /*! * Returns the state space size of the model. diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index cd2700a49..d3f0dcf25 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -84,7 +84,7 @@ class AbstractNondeterministicModel: public AbstractModel { * @param state The state for which to return the iterator. * @return An iterator to the successors of the given state. */ - virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) { + virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) const { return this->getTransitionMatrix()->constColumnIteratorBegin((*nondeterministicChoiceIndices)[state]); } @@ -94,7 +94,7 @@ class AbstractNondeterministicModel: public AbstractModel { * @param state The state for which to return the iterator. * @return An iterator pointing to the element past the successors of the given state. */ - virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) { + virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const { return this->getTransitionMatrix()->constColumnIteratorEnd((*nondeterministicChoiceIndices)[state + 1] - 1); } diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index b0d2a1cc2..4ae474304 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -219,7 +219,7 @@ public: * * @param size The number of rows and columns of the matrix. */ - SparseMatrix(uint_fast64_t size) + SparseMatrix(uint_fast64_t size = 0) : rowCount(size), colCount(size), nonZeroEntryCount(0), internalStatus(MatrixStatus::UnInitialized), currentSize(0), lastRow(0) { diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index c8530e7ef..fb272fd99 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -428,10 +428,10 @@ public: * graph of the SCCs. */ template - static std::pair>, storm::models::GraphTransitions> performSccDecomposition(storm::models::AbstractNondeterministicModel const& model) { + static std::pair>, storm::storage::SparseMatrix> performSccDecomposition(storm::models::AbstractModel const& model) { LOG4CPLUS_INFO(logger, "Computing SCC decomposition."); - std::pair>, storm::models::GraphTransitions> sccDecomposition; + std::pair>, storm::storage::SparseMatrix> sccDecomposition; uint_fast64_t numberOfStates = model.getNumberOfStates(); // Set up the environment of Tarjan's algorithm. @@ -447,7 +447,7 @@ public: uint_fast64_t currentIndex = 0; for (uint_fast64_t state = 0; state < numberOfStates; ++state) { if (!visitedStates.get(state)) { - performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, model.getTransitionMatrix(), sccDecomposition.first, stateToSccMap); + performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, *model.getTransitionMatrix(), sccDecomposition.first, stateToSccMap); } } diff --git a/test/performance/graph/GraphTest.cpp b/test/performance/graph/GraphTest.cpp new file mode 100644 index 000000000..0d69d3d57 --- /dev/null +++ b/test/performance/graph/GraphTest.cpp @@ -0,0 +1,117 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/utility/Settings.h" +#include "src/parser/AutoParser.h" +#include "src/utility/GraphAnalyzer.h" + +TEST(GraphAnalyzerTest, PerformProb01) { + 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_INFO(logger, "Computing prob01 (3 times) for crowds/crowds20_5."); + std::pair prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observe0Greater1"))); + + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 1724414u); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 46046u); + + prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observeIGreater1"))); + + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 574016u); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 825797u); + + prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observeOnlyTrueSender"))); + + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 1785309u); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 40992u); + LOG4CPLUS_INFO(logger, "Done computing prob01 (3 times) for crowds/crowds20_5."); + + 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", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew"); + + std::shared_ptr> dtmc2 = parser2.getModel>(); + + LOG4CPLUS_INFO(logger, "Computing prob01 for synchronous_leader/leader6_8"); + prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc2, storm::storage::BitVector(dtmc2->getNumberOfStates(), true), storm::storage::BitVector(dtmc2->getLabeledStates("elected"))); + LOG4CPLUS_INFO(logger, "Done computing prob01 for synchronous_leader/leader6_8"); + + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 1312334u); +} + +TEST(GraphAnalyzerTest, PerformProb01MinMax) { + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew"); + std::shared_ptr> mdp = parser.getModel>(); + + LOG4CPLUS_INFO(logger, "Computing prob01min for asynchronous_leader/leader7"); + std::pair prob01 = storm::utility::GraphAnalyzer::performProb01Min(*mdp, storm::storage::BitVector(mdp->getNumberOfStates(), true), mdp->getLabeledStates("elected")); + LOG4CPLUS_INFO(logger, "Done computing prob01min for asynchronous_leader/leader7"); + + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 2095783u); + + LOG4CPLUS_INFO(logger, "Computing prob01max for asynchronous_leader/leader7"); + prob01 = storm::utility::GraphAnalyzer::performProb01Max(*mdp, storm::storage::BitVector(mdp->getNumberOfStates(), true), mdp->getLabeledStates("elected")); + LOG4CPLUS_INFO(logger, "Done computing prob01max for asynchronous_leader/leader7"); + + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 2095783u); + + storm::parser::AutoParser parser2(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", ""); + std::shared_ptr> mdp2 = parser2.getModel>(); + + LOG4CPLUS_INFO(logger, "Computing prob01min for consensus/coin4_6"); + prob01 = storm::utility::GraphAnalyzer::performProb01Min(*mdp2, storm::storage::BitVector(mdp2->getNumberOfStates(), true), mdp2->getLabeledStates("finished")); + LOG4CPLUS_INFO(logger, "Done computing prob01min for consensus/coin4_6"); + + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 63616u); + + LOG4CPLUS_INFO(logger, "Computing prob01max for consensus/coin4_6"); + prob01 = storm::utility::GraphAnalyzer::performProb01Max(*mdp2, storm::storage::BitVector(mdp2->getNumberOfStates(), true), mdp2->getLabeledStates("finished")); + LOG4CPLUS_INFO(logger, "Done computing prob01max for consensus/coin4_6"); + + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 63616u); +} + +TEST(GraphAnalyzerTest, PerformSCCDecomposition) { + 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_INFO(logger, "Computing SCC decomposition of crowds/crowds20_5."); + std::pair>, storm::storage::SparseMatrix> sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*dtmc); + LOG4CPLUS_INFO(logger, "Done computing SCC decomposition of crowds/crowds20_5."); + + ASSERT_EQ(sccDecomposition.first.size(), 1290297u); + ASSERT_EQ(sccDecomposition.second.getNonZeroEntryCount(), 1371253u); + + 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", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew"); + std::shared_ptr> dtmc2 = parser2.getModel>(); + + LOG4CPLUS_INFO(logger, "Computing SCC decomposition of synchronous_leader/leader6_8"); + sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*dtmc2); + LOG4CPLUS_INFO(logger, "Computing SCC decomposition of synchronous_leader/leader6_8."); + + ASSERT_EQ(sccDecomposition.first.size(), 1279673u); + ASSERT_EQ(sccDecomposition.second.getNonZeroEntryCount(), 1535367u); + + storm::parser::AutoParser parser3(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew"); + std::shared_ptr> mdp = parser3.getModel>(); + + LOG4CPLUS_INFO(logger, "Computing SCC decomposition of asynchronous_leader/leader7"); + sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*mdp); + LOG4CPLUS_INFO(logger, "Done computing SCC decomposition of asynchronous_leader/leader7"); + + ASSERT_EQ(sccDecomposition.first.size(), 1914691u); + ASSERT_EQ(sccDecomposition.second.getNonZeroEntryCount(), 7023587u); + + storm::parser::AutoParser parser4(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", ""); + std::shared_ptr> mdp2 = parser4.getModel>(); + + LOG4CPLUS_INFO(logger, "Computing SCC decomposition of consensus/coin4_6"); + sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*mdp2); + LOG4CPLUS_INFO(logger, "Computing SCC decomposition of consensus/coin4_6"); + + ASSERT_EQ(sccDecomposition.first.size(), 63611u); + ASSERT_EQ(sccDecomposition.second.getNonZeroEntryCount(), 213400u); +} \ No newline at end of file diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index 2609ba0a1..3e5aa39b8 100644 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -1,6 +1,5 @@ #include "gtest/gtest.h" #include "storm-config.h" - #include "src/utility/Settings.h" #include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h" #include "src/parser/AutoParser.h" @@ -112,4 +111,4 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { delete rewardFormula; delete result; -} +} \ No newline at end of file diff --git a/test/performance/storm-performance-tests.cpp b/test/performance/storm-performance-tests.cpp index 1e1317a80..1c52acc03 100644 --- a/test/performance/storm-performance-tests.cpp +++ b/test/performance/storm-performance-tests.cpp @@ -15,10 +15,12 @@ log4cplus::Logger logger; * Initializes the logging framework. */ void setUpLogging() { - log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender("storm-functional-tests.log")); + logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main")); + logger.setLogLevel(log4cplus::INFO_LOG_LEVEL); + log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender("storm-performance-tests.log")); fileLogAppender->setName("mainFileAppender"); + fileLogAppender->setThreshold(log4cplus::WARN_LOG_LEVEL); fileLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M} (%r ms) - %F:%L : %m%n"))); - logger = log4cplus::Logger::getInstance("mainLogger"); logger.addAppender(fileLogAppender); // Uncomment these lines to enable console logging output From a08db1b2cf158b20c19bde373e8c4e5fec5602c3 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Thu, 16 May 2013 16:32:31 +0200 Subject: [PATCH 14/18] Changed prctl parser. Now, only complete lines will be matched (Before, the parser returned a result when a prefix could be matched); furthermore, comments are supported better. --- src/parser/PrctlFileParser.cpp | 13 +++++-------- src/parser/PrctlParser.cpp | 18 +++++++++--------- src/parser/PrctlParser.h | 10 ++++++++++ 3 files changed, 24 insertions(+), 17 deletions(-) diff --git a/src/parser/PrctlFileParser.cpp b/src/parser/PrctlFileParser.cpp index 0f7f877f1..4fa7a13d3 100644 --- a/src/parser/PrctlFileParser.cpp +++ b/src/parser/PrctlFileParser.cpp @@ -13,8 +13,6 @@ #include "modelchecker/GmmxxDtmcPrctlModelChecker.h" #include "modelchecker/GmmxxMdpPrctlModelChecker.h" -#include - namespace storm { namespace parser { @@ -41,13 +39,12 @@ std::list*> PrctlFileParser std::string line; //The while loop reads the input file line by line while (std::getline(inputFileStream, line)) { - boost::algorithm::trim(line); - if ((line.length() == 0) || ((line[0] == '/') && (line[1] == '/'))) { - // ignore empty lines and lines starting with // - continue; - } PrctlParser parser(line); - result.push_back(parser.getFormula()); + if (!parser.parsedComment()) { + //lines containing comments will be skipped. + LOG4CPLUS_INFO(logger, "Parsed formula \"" + line + "\" into \"" + parser.getFormula()->toString() + "\""); + result.push_back(parser.getFormula()); + } } } diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index 18f470660..446a6feb5 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -43,6 +43,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar"))[qi::_val = storm::property::GREATER] | (qi::lit("<="))[qi::_val = storm::property::LESS_EQUAL] | (qi::lit("<"))[qi::_val = storm::property::LESS]); + //Comment: Empty line or line starting with "//" comment = (qi::lit("//") >> *(qi::char_))[qi::_val = nullptr]; //This block defines rules for parsing state formulas @@ -70,7 +71,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar >(qi::_1, qi::_2, qi::_3, true)] | (qi::lit("P") >> qi::lit("max") > comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::new_ >(qi::_1, qi::_2, qi::_3, false)] | - (qi::lit("P") > comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + (qi::lit("P") >> comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::new_ >(qi::_1, qi::_2, qi::_3)] ); @@ -142,11 +143,17 @@ struct PrctlParser::PrctlGrammar : qi::grammar>()]; - start = (comment | noBoundOperator | stateFormula) >> qi::eoi; + formula = (noBoundOperator | stateFormula); + formula.name("PRCTL formula"); + + start = (((formula) > (comment | qi::eps))[qi::_val = qi::_1] | + comment + ) > qi::eoi; start.name("PRCTL formula"); } qi::rule*(), Skipper> start; + qi::rule*(), Skipper> formula; qi::rule*(), Skipper> comment; qi::rule*(), Skipper> stateFormula; @@ -228,12 +235,5 @@ storm::parser::PrctlParser::PrctlParser(std::string formulaString) { throw storm::exceptions::WrongFormatException() << msg.str(); } - // The syntax can be so wrong that no rule can be matched at all - // In that case, no expectation failure is thrown, but the parser just returns nullptr - // Then, of course the result is not usable, hence we throw a WrongFormatException, too. - if (positionIteratorBegin != positionIteratorEnd) { - throw storm::exceptions::WrongFormatException() << "Syntax error in formula"; - } - formula = result_pointer; } diff --git a/src/parser/PrctlParser.h b/src/parser/PrctlParser.h index 3778b862a..7e2b3d13d 100644 --- a/src/parser/PrctlParser.h +++ b/src/parser/PrctlParser.h @@ -38,6 +38,16 @@ class PrctlParser : Parser { return this->formula; } + /*! + * Checks whether the line which was parsed was a comment line; also returns true if the line was empty (as the semantics are + * the same) + * + * @return True if the parsed line consisted completely of a (valid) comment, false otherwise. + */ + bool parsedComment() { + return (formula == nullptr); + } + private: storm::property::prctl::AbstractPrctlFormula* formula; From 00a7c50ad4c313d599adfb0ef463e069db173d7d Mon Sep 17 00:00:00 2001 From: Lanchid Date: Thu, 16 May 2013 17:09:04 +0200 Subject: [PATCH 15/18] Implemented the improvements from the PRCTL parser also in the CSL and LTL parsers. --- src/parser/CslParser.cpp | 40 +++++++++++++----------- src/parser/LtlParser.cpp | 30 ++++++------------ src/parser/PrctlParser.cpp | 1 - test/functional/parser/CslParserTest.cpp | 2 +- test/functional/parser/LtlParserTest.cpp | 4 +-- 5 files changed, 35 insertions(+), 42 deletions(-) diff --git a/src/parser/CslParser.cpp b/src/parser/CslParser.cpp index a246aacaf..8538c8d3f 100644 --- a/src/parser/CslParser.cpp +++ b/src/parser/CslParser.cpp @@ -40,7 +40,15 @@ namespace parser { template struct CslParser::CslGrammar : qi::grammar*(), Skipper > { CslGrammar() : CslGrammar::base_type(start) { - freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))]; + //This block contains helper rules that may be used several times + freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))]; + comparisonType = ( + (qi::lit(">="))[qi::_val = storm::property::GREATER_EQUAL] | + (qi::lit(">"))[qi::_val = storm::property::GREATER] | + (qi::lit("<="))[qi::_val = storm::property::LESS_EQUAL] | + (qi::lit("<"))[qi::_val = storm::property::LESS]); + //Comment: Empty line or line starting with "//" + comment = (qi::lit("//") >> *(qi::char_))[qi::_val = nullptr]; //This block defines rules for parsing state formulas stateFormula %= orFormula; @@ -63,25 +71,13 @@ struct CslParser::CslGrammar : qi::grammar>(qi::_1)]; atomicProposition.name("state formula"); probabilisticBoundOperator = ( - (qi::lit("P") >> qi::lit(">") >> qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::GREATER, qi::_1, qi::_2)] | - (qi::lit("P") >> qi::lit(">=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::GREATER_EQUAL, qi::_1, qi::_2)] | - (qi::lit("P") >> qi::lit("<") >> qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::LESS, qi::_1, qi::_2)] | - (qi::lit("P") > qi::lit("<=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::LESS_EQUAL, qi::_1, qi::_2)] + (qi::lit("P") >> comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, qi::_2, qi::_3)] ); probabilisticBoundOperator.name("state formula"); steadyStateBoundOperator = ( - (qi::lit("S") >> qi::lit(">") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::GREATER, qi::_1, qi::_2)] | - (qi::lit("S") >> qi::lit(">=") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::GREATER_EQUAL, qi::_1, qi::_2)] | - (qi::lit("S") >> qi::lit("<") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::LESS, qi::_1, qi::_2)] | - (qi::lit("S") > qi::lit("<=") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::LESS_EQUAL, qi::_1, qi::_2)] + (qi::lit("S") >> comparisonType > qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, qi::_2, qi::_3)] ); steadyStateBoundOperator.name("state formula"); @@ -126,11 +122,18 @@ struct CslParser::CslGrammar : qi::grammar>(phoenix::bind(&storm::property::csl::AbstractStateFormula::clone, phoenix::bind(&std::shared_ptr>::get, qi::_a)), qi::_2)]; until.name("path formula (for probabilistic operator)"); - start = (noBoundOperator | stateFormula); + formula = (noBoundOperator | stateFormula); + formula.name("CSL formula"); + + start = (((formula) > (comment | qi::eps))[qi::_val = qi::_1] | + comment + ) > qi::eoi; start.name("CSL formula"); } qi::rule*(), Skipper> start; + qi::rule*(), Skipper> formula; + qi::rule*(), Skipper> comment; qi::rule*(), Skipper> stateFormula; qi::rule*(), Skipper> atomicStateFormula; @@ -155,6 +158,7 @@ struct CslParser::CslGrammar : qi::grammar freeIdentifierName; + qi::rule comparisonType; }; diff --git a/src/parser/LtlParser.cpp b/src/parser/LtlParser.cpp index 060ad5e21..6060adedc 100644 --- a/src/parser/LtlParser.cpp +++ b/src/parser/LtlParser.cpp @@ -43,6 +43,11 @@ namespace parser { template struct LtlParser::LtlGrammar : qi::grammar*(), Skipper > { LtlGrammar() : LtlGrammar::base_type(start) { + //This block contains helper rules that may be used several times + freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))]; + //Comment: Empty line or line starting with "//" + comment = (qi::lit("//") >> *(qi::char_))[qi::_val = nullptr]; + freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))]; //This block defines rules for parsing state formulas @@ -68,27 +73,9 @@ struct LtlParser::LtlGrammar : qi::grammar>(qi::_1)]; atomicProposition.name("LTL formula"); - /*probabilisticBoundOperator = ( - (qi::lit("P") >> qi::lit(">") >> qi::double_ > qi::lit("[") > LtlFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::GREATER, qi::_1, qi::_2)] | - (qi::lit("P") >> qi::lit(">=") > qi::double_ > qi::lit("[") > LtlFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::GREATER_EQUAL, qi::_1, qi::_2)] | - (qi::lit("P") >> qi::lit("<") >> qi::double_ > qi::lit("[") > LtlFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::LESS, qi::_1, qi::_2)] | - (qi::lit("P") >> qi::lit("<=") > qi::double_ > qi::lit("[") > LtlFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::property::LESS_EQUAL, qi::_1, qi::_2)] - ); - probabilisticBoundOperator.name("state formula");*/ - - //This block defines rules for parsing formulas with noBoundOperators - /*noBoundOperator = (probabilisticNoBoundOperator | rewardNoBoundOperator); - noBoundOperator.name("no bound operator"); - probabilisticNoBoundOperator = (qi::lit("P") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> LtlFormula >> qi::lit("]"))[qi::_val = - phoenix::new_ >(qi::_1)]; - probabilisticNoBoundOperator.name("no bound operator");*/ //This block defines rules for parsing probabilistic path formulas - pathFormula = (boundedEventually | eventually | globally);//(boundedEventually | eventually | globally | boundedUntil | until); + pathFormula = (boundedEventually | eventually | globally); pathFormula.name("LTL formula"); boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > ltlFormula)[qi::_val = phoenix::new_>(qi::_2, qi::_1)]; @@ -100,11 +87,14 @@ struct LtlParser::LtlGrammar : qi::grammar >(qi::_1)]; globally.name("LTL formula"); - start = ltlFormula; + start = (((ltlFormula) > (comment | qi::eps))[qi::_val = qi::_1] | + comment + ) > qi::eoi; start.name("LTL formula"); } qi::rule*(), Skipper> start; + qi::rule*(), Skipper> comment; qi::rule*(), Skipper> ltlFormula; qi::rule*(), Skipper> atomicLtlFormula; diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index 446a6feb5..88098561d 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -35,7 +35,6 @@ namespace parser { template struct PrctlParser::PrctlGrammar : qi::grammar*(), Skipper > { PrctlGrammar() : PrctlGrammar::base_type(start) { - //This block contains helper rules that may be used several times freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))]; comparisonType = ( diff --git a/test/functional/parser/CslParserTest.cpp b/test/functional/parser/CslParserTest.cpp index ebf7250a9..f6657289c 100644 --- a/test/functional/parser/CslParserTest.cpp +++ b/test/functional/parser/CslParserTest.cpp @@ -116,7 +116,7 @@ TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) { TEST(CslParserTest, parseComplexFormulaTest) { storm::parser::CslParser* cslParser = nullptr; ASSERT_NO_THROW( - cslParser = new storm::parser::CslParser("S<=0.5 [ P <= 0.5 [ a U c ] ] & (P > 0.5 [ G b] | !P < 0.4 [ G P>0.9 [F >=7 a & b] ])") + cslParser = new storm::parser::CslParser("S<=0.5 [ P <= 0.5 [ a U c ] ] & (P > 0.5 [ G b] | !P < 0.4 [ G P>0.9 [F >=7 a & b] ]) //and a comment") ); ASSERT_NE(cslParser->getFormula(), nullptr); diff --git a/test/functional/parser/LtlParserTest.cpp b/test/functional/parser/LtlParserTest.cpp index 1a50ddb28..c88885372 100644 --- a/test/functional/parser/LtlParserTest.cpp +++ b/test/functional/parser/LtlParserTest.cpp @@ -132,7 +132,7 @@ TEST(LtlParserTest, parseComplexUntilTest) { TEST(LtlParserTest, parseComplexFormulaTest) { storm::parser::LtlParser* ltlParser = nullptr; ASSERT_NO_THROW( - ltlParser = new storm::parser::LtlParser("a U F b | G a & F<=3 a U<=7 b") + ltlParser = new storm::parser::LtlParser("a U F b | G a & F<=3 a U<=7 b //and a comment :P") ); ASSERT_NE(ltlParser->getFormula(), nullptr); @@ -145,7 +145,7 @@ TEST(LtlParserTest, parseComplexFormulaTest) { TEST(LtlParserTest, wrongFormulaTest) { storm::parser::LtlParser* ltlParser = nullptr; ASSERT_THROW( - ltlParser = new storm::parser::LtlParser("(a | b) & +"), + ltlParser = new storm::parser::LtlParser("(a | c) & +"), storm::exceptions::WrongFormatException ); delete ltlParser; From fbe1f41213bef2799a9ec4ce5f3e9545786ddeb1 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 16 May 2013 16:19:00 +0200 Subject: [PATCH 16/18] Removed GraphTransition class, which is now replaced by SparseMatrix in the instances where it was used before. Changed GraphAnalyzer accordingly and adapted tests. --- src/modelchecker/GmmxxMdpPrctlModelChecker.h | 2 +- ...ogicalValueIterationMdpPrctlModelChecker.h | 6 +- src/models/AbstractDeterministicModel.h | 5 +- src/models/AbstractModel.h | 73 ++++- src/models/AbstractNondeterministicModel.h | 7 +- src/models/GraphTransitions.h | 258 ------------------ src/storage/SparseMatrix.h | 24 +- src/utility/GraphAnalyzer.h | 41 ++- test/functional/storm-functional-tests.cpp | 9 +- test/performance/graph/GraphTest.cpp | 98 +++++-- .../GmmxxDtmcPrctModelCheckerTest.cpp | 14 +- .../GmmxxMdpPrctModelCheckerTest.cpp | 40 ++- test/performance/storm-performance-tests.cpp | 12 +- 13 files changed, 244 insertions(+), 345 deletions(-) delete mode 100644 src/models/GraphTransitions.h diff --git a/src/modelchecker/GmmxxMdpPrctlModelChecker.h b/src/modelchecker/GmmxxMdpPrctlModelChecker.h index 48c4c6304..3b340dadf 100644 --- a/src/modelchecker/GmmxxMdpPrctlModelChecker.h +++ b/src/modelchecker/GmmxxMdpPrctlModelChecker.h @@ -151,7 +151,7 @@ private: if (converged) { LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iterations << " iterations."); } else { - LOG4CPLUS_WARN(logger, "Iterative solver did not converge."); + LOG4CPLUS_WARN(logger, "Iterative solver did not converge after " << iterations << " iterations."); } } }; diff --git a/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h b/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h index 1466c02ec..7368a91bf 100644 --- a/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h +++ b/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h @@ -67,10 +67,8 @@ private: bool relative = s->get("relative"); // Now, we need to determine the SCCs of the MDP and a topological sort. - std::pair>, storm::models::GraphTransitions> sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); - std::vector> stronglyConnectedComponents = std::move(sccDecomposition.first); - storm::models::GraphTransitions stronglyConnectedComponentsDependencyGraph = std::move(sccDecomposition.second); - + std::vector> stronglyConnectedComponents = storm::utility::GraphAnalyzer::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); + storm::storage::SparseMatrix stronglyConnectedComponentsDependencyGraph = this->getModel().extractSccDependencyGraph(stronglyConnectedComponents); std::vector topologicalSort = storm::utility::GraphAnalyzer::getTopologicalSort(stronglyConnectedComponentsDependencyGraph); // Set up the environment for the power method. diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index 1986aa776..a45b5df77 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -2,7 +2,6 @@ #define STORM_MODELS_ABSTRACTDETERMINISTICMODEL_H_ #include "AbstractModel.h" -#include "GraphTransitions.h" #include @@ -53,7 +52,7 @@ class AbstractDeterministicModel: public AbstractModel { * @return An iterator to the successors of the given state. */ virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) const { - return this->getTransitionMatrix()->constColumnIteratorBegin(state); + return this->transitionMatrix->constColumnIteratorBegin(state); } /*! @@ -63,7 +62,7 @@ class AbstractDeterministicModel: public AbstractModel { * @return An iterator pointing to the element past the successors of the given state. */ virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const { - return this->getTransitionMatrix()->constColumnIteratorEnd(state); + return this->transitionMatrix->constColumnIteratorEnd(state); } }; diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 806cfed67..c4896a6c6 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -91,9 +91,20 @@ class AbstractModel: public std::enable_shared_from_this> { * @param stronglyConnectedComponents A vector containing the SCCs of the system. * @param stateToSccMap A mapping from state indices to */ - storm::storage::SparseMatrix extractSccDependencyGraph(std::vector> const& stronglyConnectedComponents, std::map const& stateToSccMap) const { - // The resulting sparse matrix will have as many rows/columns as there are SCCs. + storm::storage::SparseMatrix extractSccDependencyGraph(std::vector> const& stronglyConnectedComponents) const { uint_fast64_t numberOfStates = stronglyConnectedComponents.size(); + + // First, we need to create a mapping of states to their SCC index, to ease the computation + // of dependency transitions later. + std::vector stateToSccMap(this->getNumberOfStates()); + for (uint_fast64_t i = 0; i < numberOfStates; ++i) { + for (uint_fast64_t j = 0; j < stronglyConnectedComponents[i].size(); ++j) { + stateToSccMap[stronglyConnectedComponents[i][j]] = i; + } + } + + // The resulting sparse matrix will have as many rows/columns as there are SCCs. + storm::storage::SparseMatrix sccDependencyGraph(numberOfStates); sccDependencyGraph.initialize(); @@ -105,7 +116,7 @@ class AbstractModel: public std::enable_shared_from_this> { std::set allTargetSccs; for (auto state : scc) { for (typename storm::storage::SparseMatrix::ConstIndexIterator succIt = this->constStateSuccessorIteratorBegin(state), succIte = this->constStateSuccessorIteratorEnd(state); succIt != succIte; ++succIt) { - uint_fast64_t targetScc = stateToSccMap.find(*succIt)->second; + uint_fast64_t targetScc = stateToSccMap[*succIt]; // We only need to consider transitions that are actually leaving the SCC. if (targetScc != currentSccIndex) { @@ -125,6 +136,59 @@ class AbstractModel: public std::enable_shared_from_this> { return sccDependencyGraph; } + + /*! + * Retrieves the backward transition relation of the model, i.e. a set of transitions + * between states that correspond to the reversed transition relation of this model. + * + * @return A sparse matrix that represents the backward transitions of this model. + */ + virtual storm::storage::SparseMatrix getBackwardTransitions() const { + uint_fast64_t numberOfStates = this->getNumberOfStates(); + uint_fast64_t numberOfTransitions = this->getNumberOfTransitions(); + + std::vector rowIndications(numberOfStates + 1); + std::vector columnIndications(numberOfTransitions); + std::vector values(numberOfTransitions, true); + + // First, we need to count how many backward transitions each state has. + for (uint_fast64_t i = 0; i < numberOfStates; ++i) { + for (auto rowIt = this->constStateSuccessorIteratorBegin(i), rowIte = this->constStateSuccessorIteratorEnd(i); rowIt != rowIte; ++rowIt) { + rowIndications[*rowIt + 1]++; + } + } + + // Now compute the accumulated offsets. + for (uint_fast64_t i = 1; i < numberOfStates; ++i) { + rowIndications[i] = rowIndications[i - 1] + rowIndications[i]; + } + + // Put a sentinel element at the end of the indices list. This way, + // for each state i the range of indices can be read off between + // state_indices_list[i] and state_indices_list[i + 1]. + // FIXME: This should not be necessary and already be implied by the first steps. + rowIndications[numberOfStates] = numberOfTransitions; + + // Create an array that stores the next index for each state. Initially + // this corresponds to the previously computed accumulated offsets. + std::vector nextIndices = rowIndications; + + // Now we are ready to actually fill in the list of predecessors for + // every state. Again, we start by considering all but the last row. + for (uint_fast64_t i = 0; i < numberOfStates; ++i) { + for (auto rowIt = this->constStateSuccessorIteratorBegin(i), rowIte = this->constStateSuccessorIteratorEnd(i); rowIt != rowIte; ++rowIt) { + columnIndications[nextIndices[*rowIt]++] = i; + } + } + + storm::storage::SparseMatrix backwardTransitionMatrix(numberOfStates, numberOfStates, + numberOfTransitions, + std::move(rowIndications), + std::move(columnIndications), + std::move(values)); + + return backwardTransitionMatrix; + } /*! * Returns an iterator to the successors of the given state. @@ -269,10 +333,11 @@ class AbstractModel: public std::enable_shared_from_this> { << std::endl; } - private: + protected: /*! A matrix representing the likelihoods of moving between states. */ std::shared_ptr> transitionMatrix; +private: /*! The labeling of the states of the model. */ std::shared_ptr stateLabeling; diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index d3f0dcf25..b64359d2f 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -2,7 +2,6 @@ #define STORM_MODELS_ABSTRACTNONDETERMINISTICMODEL_H_ #include "AbstractModel.h" -#include "GraphTransitions.h" #include @@ -56,7 +55,7 @@ class AbstractNondeterministicModel: public AbstractModel { * @return The number of choices for all states of the MDP. */ uint_fast64_t getNumberOfChoices() const { - return this->getTransitionMatrix()->getRowCount(); + return this->transitionMatrix->getRowCount(); } /*! @@ -85,7 +84,7 @@ class AbstractNondeterministicModel: public AbstractModel { * @return An iterator to the successors of the given state. */ virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) const { - return this->getTransitionMatrix()->constColumnIteratorBegin((*nondeterministicChoiceIndices)[state]); + return this->transitionMatrix->constColumnIteratorBegin((*nondeterministicChoiceIndices)[state]); } /*! @@ -95,7 +94,7 @@ class AbstractNondeterministicModel: public AbstractModel { * @return An iterator pointing to the element past the successors of the given state. */ virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const { - return this->getTransitionMatrix()->constColumnIteratorEnd((*nondeterministicChoiceIndices)[state + 1] - 1); + return this->transitionMatrix->constColumnIteratorEnd((*nondeterministicChoiceIndices)[state + 1] - 1); } private: diff --git a/src/models/GraphTransitions.h b/src/models/GraphTransitions.h deleted file mode 100644 index de435a00b..000000000 --- a/src/models/GraphTransitions.h +++ /dev/null @@ -1,258 +0,0 @@ -/* - * GraphTransitions.h - * - * Created on: 17.11.2012 - * Author: Christian Dehnert - */ - -#ifndef STORM_MODELS_GRAPHTRANSITIONS_H_ -#define STORM_MODELS_GRAPHTRANSITIONS_H_ - -#include "src/storage/SparseMatrix.h" - -#include -#include - -namespace storm { - -namespace models { - -/*! - * This class stores the successors of all states in a state space of the - * given size. - */ -template -class GraphTransitions { - -public: - /*! - * Just typedef the iterator as a pointer to the index type. - */ - typedef const uint_fast64_t * stateSuccessorIterator; - - //! Constructor - /*! - * Constructs an object representing the graph structure of the given - * transition relation, which is given by a sparse matrix. - * @param transitionMatrix The (0-based) matrix representing the transition - * relation. - * @param forward If set to true, this objects will store the graph structure - * of the backwards transition relation. - */ - GraphTransitions(storm::storage::SparseMatrix const& transitionMatrix, bool forward) - : numberOfStates(transitionMatrix.getColumnCount()), numberOfTransitions(transitionMatrix.getNonZeroEntryCount()), successorList(numberOfTransitions), stateIndications(numberOfStates + 1) { - if (forward) { - this->initializeForward(transitionMatrix); - } else { - this->initializeBackward(transitionMatrix); - } - } - - GraphTransitions(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, bool forward) - : numberOfStates(transitionMatrix.getColumnCount()), numberOfTransitions(transitionMatrix.getNonZeroEntryCount()), successorList(numberOfTransitions), stateIndications(numberOfStates + 1) { - if (forward) { - this->initializeForward(transitionMatrix, nondeterministicChoiceIndices); - } else { - this->initializeBackward(transitionMatrix, nondeterministicChoiceIndices); - } - } - - GraphTransitions(GraphTransitions const& transitions, std::vector> const& stronglyConnectedComponents, std::map const& stateToSccMap) - : numberOfStates(stronglyConnectedComponents.size()), numberOfTransitions(0), successorList(), stateIndications(numberOfStates + 1) { - this->initializeFromSccDecomposition(transitions, stronglyConnectedComponents, stateToSccMap); - } - - GraphTransitions() : numberOfStates(0), numberOfTransitions(0), successorList(), stateIndications() { - // Intentionally left empty. - } - - /*! - * Retrieves the size of the internal representation of the graph transitions in memory. - * @return the size of the internal representation of the graph transitions in memory - * measured in bytes. - */ - virtual uint_fast64_t getSizeInMemory() const { - uint_fast64_t result = sizeof(this) + (numberOfStates + numberOfTransitions + 1) * sizeof(uint_fast64_t); - return result; - } - - uint_fast64_t getNumberOfStates() const { - return numberOfStates; - } - - uint_fast64_t getNumberOfTransitions() const { - return numberOfTransitions; - } - - /*! - * Returns an iterator to the successors of the given state. - * @param state The state for which to get the successor iterator. - * @return An iterator to the predecessors of the given states. - */ - stateSuccessorIterator beginStateSuccessorsIterator(uint_fast64_t state) const { - return &(this->successorList[0]) + this->stateIndications[state]; - } - - /*! - * Returns an iterator referring to the element after the successors of - * the given state. - * @param state The state for which to get the iterator. - * @return An iterator referring to the element after the successors of - * the given state. - */ - stateSuccessorIterator endStateSuccessorsIterator(uint_fast64_t state) const { - return &(this->successorList[0]) + this->stateIndications[state + 1]; - } - - /*! - * Returns a (naive) string representation of the transitions in this object. - * @returns a (naive) string representation of the transitions in this object. - */ - std::string toString() const { - std::stringstream stream; - for (uint_fast64_t state = 0; state < numberOfStates; ++state) { - for (auto succIt = this->beginStateSuccessorsIterator(state), succIte = this->endStateSuccessorsIterator(state); succIt != succIte; ++succIt) { - stream << state << " -> " << *succIt << std::endl; - } - } - return stream.str(); - } - -private: - /*! - * Initializes this graph transitions object using the forward transition - * relation given by means of a sparse matrix. - */ - void initializeForward(storm::storage::SparseMatrix const& transitionMatrix) { - // First, we copy the index list from the sparse matrix as this will - // stay the same. - std::copy(transitionMatrix.constColumnIteratorBegin(), transitionMatrix.constColumnIteratorEnd(), this->stateIndications.begin()); - - // Now we can iterate over all rows of the transition matrix and record the target state. - for (uint_fast64_t i = 0, currentNonZeroElement = 0; i < numberOfStates; i++) { - for (auto rowIt = transitionMatrix.constColumnIteratorBegin(i); rowIt != transitionMatrix.constColumnIteratorEnd(i); ++rowIt) { - this->successorList[currentNonZeroElement++] = *rowIt; - } - } - } - - void initializeForward(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices) { - // We can directly copy the starting indices from the transition matrix as we do not - // eliminate duplicate transitions and therefore will have as many non-zero entries as this - // matrix. - typename storm::storage::SparseMatrix::ConstRowsIterator rowsIt(transitionMatrix); - for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - rowsIt.moveToRow(nondeterministicChoiceIndices[i]); - this->stateIndications[i] = rowsIt.index(); - } - this->stateIndications[numberOfStates] = numberOfTransitions; - - // Now we can iterate over all rows of the transition matrix and record - // the target state. - for (uint_fast64_t i = 0, currentNonZeroElement = 0; i < numberOfStates; i++) { - for (uint_fast64_t j = nondeterministicChoiceIndices[i]; j < nondeterministicChoiceIndices[i + 1]; ++j) { - for (auto rowIt = transitionMatrix.constColumnIteratorBegin(j); rowIt != transitionMatrix.constColumnIteratorEnd(j); ++rowIt) { - this->successorList[currentNonZeroElement++] = *rowIt; - } - } - } - } - - /*! - * Initializes this graph transitions object using the backwards transition - * relation, whose forward transition relation is given by means of a sparse - * matrix. - */ - void initializeBackward(storm::storage::SparseMatrix const& transitionMatrix) { - // First, we need to count how many backward transitions each state has. - for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - for (auto rowIt = transitionMatrix.constColumnIteratorBegin(i); rowIt != transitionMatrix.constColumnIteratorEnd(i); ++rowIt) { - this->stateIndications[*rowIt + 1]++; - } - } - - // Now compute the accumulated offsets. - for (uint_fast64_t i = 1; i < numberOfStates; ++i) { - this->stateIndications[i] = this->stateIndications[i - 1] + this->stateIndications[i]; - } - - // Put a sentinel element at the end of the indices list. This way, - // for each state i the range of indices can be read off between - // state_indices_list[i] and state_indices_list[i + 1]. - this->stateIndications[numberOfStates] = numberOfTransitions; - - // Create an array that stores the next index for each state. Initially - // this corresponds to the previously computed accumulated offsets. - std::vector nextIndices = stateIndications; - - // Now we are ready to actually fill in the list of predecessors for - // every state. Again, we start by considering all but the last row. - for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - for (auto rowIt = transitionMatrix.constColumnIteratorBegin(i); rowIt != transitionMatrix.constColumnIteratorEnd(i); ++rowIt) { - this->successorList[nextIndices[*rowIt]++] = i; - } - } - } - - void initializeBackward(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices) { - // First, we need to count how many backward transitions each state has. - for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - for (uint_fast64_t j = nondeterministicChoiceIndices[i]; j < nondeterministicChoiceIndices[i + 1]; ++j) { - for (auto rowIt = transitionMatrix.constColumnIteratorBegin(j); rowIt != transitionMatrix.constColumnIteratorEnd(j); ++rowIt) { - this->stateIndications[*rowIt + 1]++; - } - } - } - - // Now compute the accumulated offsets. - for (uint_fast64_t i = 1; i < numberOfStates; i++) { - this->stateIndications[i] = this->stateIndications[i - 1] + this->stateIndications[i]; - } - - // Put a sentinel element at the end of the indices list. This way, - // for each state i the range of indices can be read off between - // state_indices_list[i] and state_indices_list[i + 1]. - this->stateIndications[numberOfStates] = numberOfTransitions; - - // Create an array that stores the next index for each state. Initially - // this corresponds to the previously computed accumulated offsets. - std::vector nextIndices = stateIndications; - - // Now we are ready to actually fill in the list of predecessors for - // every state. Again, we start by considering all but the last row. - for (uint_fast64_t i = 0; i < numberOfStates; i++) { - for (uint_fast64_t j = nondeterministicChoiceIndices[i]; j < nondeterministicChoiceIndices[i + 1]; ++j) { - for (auto rowIt = transitionMatrix.constColumnIteratorBegin(j); rowIt != transitionMatrix.constColumnIteratorEnd(j); ++rowIt) { - this->successorList[nextIndices[*rowIt]++] = i; - } - } - } - } - - /*! - * Store the number of states to determine the highest index at which the - * state_indices_list may be accessed. - */ - uint_fast64_t numberOfStates; - - /*! - * Store the number of non-zero transition entries to determine the highest - * index at which the predecessor_list may be accessed. - */ - uint_fast64_t numberOfTransitions; - - /*! A list of successors for *all* states. */ - std::vector successorList; - - /*! - * A list of indices indicating at which position in the global array the - * successors of a state can be found. - */ - std::vector stateIndications; -}; - -} // namespace models - -} // namespace storm - -#endif /* STORM_MODELS_GRAPHTRANSITIONS_H_ */ diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 4ae474304..a968f7ee5 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -211,7 +211,7 @@ public: */ SparseMatrix(uint_fast64_t rows, uint_fast64_t cols) : rowCount(rows), colCount(cols), nonZeroEntryCount(0), internalStatus(MatrixStatus::UnInitialized), currentSize(0), lastRow(0) { - + // Intentionally left empty. } /*! @@ -222,8 +222,28 @@ public: SparseMatrix(uint_fast64_t size = 0) : rowCount(size), colCount(size), nonZeroEntryCount(0), internalStatus(MatrixStatus::UnInitialized), currentSize(0), lastRow(0) { - + // Intentionally left empty. } + + /*! + * Constructs a sparse matrix object with the given (moved) contents. + * + * @param rowCount The number of rows. + * @param colCount The number of columns. + * @param nonZeroEntryCount The number of non-zero entries. + * @param rowIndications The vector indicating where the rows start. + * @param columnIndications The vector indicating the column for each non-zero element. + * @param values The vector containing the non-zero values. + */ + SparseMatrix(uint_fast64_t rowCount, uint_fast64_t colCount, uint_fast64_t nonZeroEntryCount, + std::vector&& rowIndications, + std::vector&& columnIndications, std::vector&& values) + : rowCount(rowCount), colCount(colCount), nonZeroEntryCount(nonZeroEntryCount), + valueStorage(values), columnIndications(columnIndications), + rowIndications(rowIndications), internalStatus(MatrixStatus::Initialized), + currentSize(0), lastRow(0) { + // Intentionally left empty. + } /*! * Initializes the sparse matrix with the given number of non-zero entries diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index fb272fd99..577bccf74 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -58,7 +58,7 @@ public: storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates()); // Get the backwards transition relation from the model to ease the search. - storm::models::GraphTransitions backwardTransitions(*model.getTransitionMatrix(), false); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); // Add all psi states as the already satisfy the condition. statesWithProbabilityGreater0 |= psiStates; @@ -73,7 +73,7 @@ public: uint_fast64_t currentState = stack.back(); stack.pop_back(); - for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { + for(auto it = backwardTransitions.constColumnIteratorBegin(currentState); it != backwardTransitions.constColumnIteratorEnd(currentState); ++it) { if (phiStates.get(*it) && !statesWithProbabilityGreater0.get(*it)) { statesWithProbabilityGreater0.set(*it, true); stack.push_back(*it); @@ -161,7 +161,7 @@ public: storm::storage::BitVector statesWithProbability0(model.getNumberOfStates()); // Get the backwards transition relation from the model to ease the search. - storm::models::GraphTransitions backwardTransitions(*model.getTransitionMatrix(), *model.getNondeterministicChoiceIndices(), false); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); // Add all psi states as the already satisfy the condition. statesWithProbability0 |= psiStates; @@ -176,7 +176,7 @@ public: uint_fast64_t currentState = stack.back(); stack.pop_back(); - for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { + for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) { if (phiStates.get(*it) && !statesWithProbability0.get(*it)) { statesWithProbability0.set(*it, true); stack.push_back(*it); @@ -207,7 +207,7 @@ public: std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); // Get the backwards transition relation from the model to ease the search. - storm::models::GraphTransitions backwardTransitions(*model.getTransitionMatrix(), *model.getNondeterministicChoiceIndices(), false); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); storm::storage::BitVector currentStates(model.getNumberOfStates(), true); @@ -225,7 +225,7 @@ public: uint_fast64_t currentState = stack.back(); stack.pop_back(); - for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { + for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) { if (phiStates.get(*it) && !nextStates.get(*it)) { // Check whether the predecessor has only successors in the current state set for one of the // nondeterminstic choices. @@ -300,7 +300,7 @@ public: std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); // Get the backwards transition relation from the model to ease the search. - storm::models::GraphTransitions backwardTransitions(*transitionMatrix, *nondeterministicChoiceIndices, false); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); // Add all psi states as the already satisfy the condition. statesWithProbability0 |= psiStates; @@ -315,7 +315,7 @@ public: uint_fast64_t currentState = stack.back(); stack.pop_back(); - for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { + for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) { if (phiStates.get(*it) && !statesWithProbability0.get(*it)) { // Check whether the predecessor has at least one successor in the current state // set for every nondeterministic choice. @@ -366,7 +366,7 @@ public: std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); // Get the backwards transition relation from the model to ease the search. - storm::models::GraphTransitions backwardTransitions(*model.getTransitionMatrix(), *model.getNondeterministicChoiceIndices(), false); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); storm::storage::BitVector currentStates(model.getNumberOfStates(), true); @@ -384,7 +384,7 @@ public: uint_fast64_t currentState = stack.back(); stack.pop_back(); - for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { + for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) { if (phiStates.get(*it) && !nextStates.get(*it)) { // Check whether the predecessor has only successors in the current state set for all of the // nondeterminstic choices. @@ -421,17 +421,16 @@ public: } /*! - * Performs a decomposition of the given nondeterministic model into its SCCs. + * Performs a decomposition of the given model into its SCCs. * * @param model The nondeterminstic model to decompose. - * @return A pair whose first component represents the SCCs and whose second component represents the dependency - * graph of the SCCs. + * @return A vector of SCCs of the model. */ template - static std::pair>, storm::storage::SparseMatrix> performSccDecomposition(storm::models::AbstractModel const& model) { + static std::vector> performSccDecomposition(storm::models::AbstractModel const& model) { LOG4CPLUS_INFO(logger, "Computing SCC decomposition."); - std::pair>, storm::storage::SparseMatrix> sccDecomposition; + std::vector> scc; uint_fast64_t numberOfStates = model.getNumberOfStates(); // Set up the environment of Tarjan's algorithm. @@ -441,21 +440,17 @@ public: std::vector stateIndices(numberOfStates); std::vector lowlinks(numberOfStates); storm::storage::BitVector visitedStates(numberOfStates); - std::map stateToSccMap; // Start the search for SCCs from every vertex in the graph structure, because there is. uint_fast64_t currentIndex = 0; for (uint_fast64_t state = 0; state < numberOfStates; ++state) { if (!visitedStates.get(state)) { - performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, *model.getTransitionMatrix(), sccDecomposition.first, stateToSccMap); + performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, *model.getTransitionMatrix(), scc); } } - - // Finally, determine the dependency graph over the SCCs and return result. - sccDecomposition.second = model.extractSccDependencyGraph(sccDecomposition.first, stateToSccMap); LOG4CPLUS_INFO(logger, "Done computing SCC decomposition."); - return sccDecomposition; + return scc; } /*! @@ -551,10 +546,9 @@ private: * @param visitedStates A bit vector that stores all states that have already been visited. * @param matrix The transition matrix representing the graph structure. * @param stronglyConnectedComponents A vector of strongly connected components to which newly found SCCs are added. - * @param stateToSccMap A mapping from state indices to SCC indices that maps each state to its SCC. */ template - static void performSccDecompositionHelper(uint_fast64_t startState, uint_fast64_t& currentIndex, std::vector& stateIndices, std::vector& lowlinks, std::vector& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, storm::storage::SparseMatrix const& matrix, std::vector>& stronglyConnectedComponents, std::map& stateToSccMap) { + static void performSccDecompositionHelper(uint_fast64_t startState, uint_fast64_t& currentIndex, std::vector& stateIndices, std::vector& lowlinks, std::vector& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, storm::storage::SparseMatrix const& matrix, std::vector>& stronglyConnectedComponents) { // 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 @@ -623,7 +617,6 @@ private: // Add the state to the current SCC. stronglyConnectedComponents.back().push_back(lastState); - stateToSccMap[lastState] = stronglyConnectedComponents.size() - 1; } while (lastState != currentState); } diff --git a/test/functional/storm-functional-tests.cpp b/test/functional/storm-functional-tests.cpp index 7139bed3c..abfb5a125 100644 --- a/test/functional/storm-functional-tests.cpp +++ b/test/functional/storm-functional-tests.cpp @@ -15,10 +15,12 @@ log4cplus::Logger logger; * Initializes the logging framework. */ void setUpLogging() { + logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main")); + logger.setLogLevel(log4cplus::ERROR_LOG_LEVEL); log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender("storm-functional-tests.log")); fileLogAppender->setName("mainFileAppender"); + fileLogAppender->setThreshold(log4cplus::FATAL_LOG_LEVEL); fileLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M} (%r ms) - %F:%L : %m%n"))); - logger = log4cplus::Logger::getInstance("mainLogger"); logger.addAppender(fileLogAppender); // Uncomment these lines to enable console logging output @@ -62,5 +64,8 @@ int main(int argc, char* argv[]) { testing::InitGoogleTest(&argc, argv); - return RUN_ALL_TESTS(); + int result = RUN_ALL_TESTS(); + + logger.closeNestedAppenders(); + return result; } diff --git a/test/performance/graph/GraphTest.cpp b/test/performance/graph/GraphTest.cpp index 0d69d3d57..84f264004 100644 --- a/test/performance/graph/GraphTest.cpp +++ b/test/performance/graph/GraphTest.cpp @@ -9,7 +9,7 @@ TEST(GraphAnalyzerTest, PerformProb01) { std::shared_ptr> dtmc = parser.getModel>(); - LOG4CPLUS_INFO(logger, "Computing prob01 (3 times) for crowds/crowds20_5."); + LOG4CPLUS_WARN(logger, "Computing prob01 (3 times) for crowds/crowds20_5..."); std::pair prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observe0Greater1"))); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 1724414u); @@ -24,94 +24,132 @@ TEST(GraphAnalyzerTest, PerformProb01) { ASSERT_EQ(prob01.first.getNumberOfSetBits(), 1785309u); ASSERT_EQ(prob01.second.getNumberOfSetBits(), 40992u); - LOG4CPLUS_INFO(logger, "Done computing prob01 (3 times) for crowds/crowds20_5."); + LOG4CPLUS_WARN(logger, "Done."); + + 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", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew"); std::shared_ptr> dtmc2 = parser2.getModel>(); - LOG4CPLUS_INFO(logger, "Computing prob01 for synchronous_leader/leader6_8"); + LOG4CPLUS_WARN(logger, "Computing prob01 for synchronous_leader/leader6_8..."); prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc2, storm::storage::BitVector(dtmc2->getNumberOfStates(), true), storm::storage::BitVector(dtmc2->getLabeledStates("elected"))); - LOG4CPLUS_INFO(logger, "Done computing prob01 for synchronous_leader/leader6_8"); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); ASSERT_EQ(prob01.second.getNumberOfSetBits(), 1312334u); + + dtmc2 = nullptr; } TEST(GraphAnalyzerTest, PerformProb01MinMax) { storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew"); std::shared_ptr> mdp = parser.getModel>(); - LOG4CPLUS_INFO(logger, "Computing prob01min for asynchronous_leader/leader7"); + LOG4CPLUS_WARN(logger, "Computing prob01min for asynchronous_leader/leader7..."); std::pair prob01 = storm::utility::GraphAnalyzer::performProb01Min(*mdp, storm::storage::BitVector(mdp->getNumberOfStates(), true), mdp->getLabeledStates("elected")); - LOG4CPLUS_INFO(logger, "Done computing prob01min for asynchronous_leader/leader7"); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); ASSERT_EQ(prob01.second.getNumberOfSetBits(), 2095783u); - LOG4CPLUS_INFO(logger, "Computing prob01max for asynchronous_leader/leader7"); + LOG4CPLUS_WARN(logger, "Computing prob01max for asynchronous_leader/leader7..."); prob01 = storm::utility::GraphAnalyzer::performProb01Max(*mdp, storm::storage::BitVector(mdp->getNumberOfStates(), true), mdp->getLabeledStates("elected")); - LOG4CPLUS_INFO(logger, "Done computing prob01max for asynchronous_leader/leader7"); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); ASSERT_EQ(prob01.second.getNumberOfSetBits(), 2095783u); + + mdp = nullptr; storm::parser::AutoParser parser2(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", ""); std::shared_ptr> mdp2 = parser2.getModel>(); - LOG4CPLUS_INFO(logger, "Computing prob01min for consensus/coin4_6"); + LOG4CPLUS_WARN(logger, "Computing prob01min for consensus/coin4_6..."); prob01 = storm::utility::GraphAnalyzer::performProb01Min(*mdp2, storm::storage::BitVector(mdp2->getNumberOfStates(), true), mdp2->getLabeledStates("finished")); - LOG4CPLUS_INFO(logger, "Done computing prob01min for consensus/coin4_6"); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); ASSERT_EQ(prob01.second.getNumberOfSetBits(), 63616u); - LOG4CPLUS_INFO(logger, "Computing prob01max for consensus/coin4_6"); + LOG4CPLUS_WARN(logger, "Computing prob01max for consensus/coin4_6..."); prob01 = storm::utility::GraphAnalyzer::performProb01Max(*mdp2, storm::storage::BitVector(mdp2->getNumberOfStates(), true), mdp2->getLabeledStates("finished")); - LOG4CPLUS_INFO(logger, "Done computing prob01max for consensus/coin4_6"); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); ASSERT_EQ(prob01.second.getNumberOfSetBits(), 63616u); + + mdp2 = nullptr; } -TEST(GraphAnalyzerTest, PerformSCCDecomposition) { +TEST(GraphAnalyzerTest, 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_INFO(logger, "Computing SCC decomposition of crowds/crowds20_5."); - std::pair>, storm::storage::SparseMatrix> sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*dtmc); - LOG4CPLUS_INFO(logger, "Done computing SCC decomposition of crowds/crowds20_5."); + LOG4CPLUS_WARN(logger, "Computing SCC decomposition of crowds/crowds20_5..."); + std::vector> sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*dtmc); + LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(sccDecomposition.first.size(), 1290297u); - ASSERT_EQ(sccDecomposition.second.getNonZeroEntryCount(), 1371253u); + ASSERT_EQ(sccDecomposition.size(), 1290297u); + + LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of crowds/crowds20_5..."); + storm::storage::SparseMatrix sccDependencyGraph = dtmc->extractSccDependencyGraph(sccDecomposition); + LOG4CPLUS_WARN(logger, "Done."); + + ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 1371253u); + + 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", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew"); std::shared_ptr> dtmc2 = parser2.getModel>(); - LOG4CPLUS_INFO(logger, "Computing SCC decomposition of synchronous_leader/leader6_8"); + LOG4CPLUS_WARN(logger, "Computing SCC decomposition of synchronous_leader/leader6_8..."); sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*dtmc2); - LOG4CPLUS_INFO(logger, "Computing SCC decomposition of synchronous_leader/leader6_8."); + LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(sccDecomposition.first.size(), 1279673u); - ASSERT_EQ(sccDecomposition.second.getNonZeroEntryCount(), 1535367u); + ASSERT_EQ(sccDecomposition.size(), 1279673u); + + LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of synchronous_leader/leader6_8..."); + sccDependencyGraph = dtmc2->extractSccDependencyGraph(sccDecomposition); + LOG4CPLUS_WARN(logger, "Done."); + ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 1535367u); + + dtmc2 = nullptr; + + /* storm::parser::AutoParser parser3(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew"); std::shared_ptr> mdp = parser3.getModel>(); - LOG4CPLUS_INFO(logger, "Computing SCC decomposition of asynchronous_leader/leader7"); + LOG4CPLUS_WARN(logger, "Computing SCC decomposition of asynchronous_leader/leader7..."); sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*mdp); - LOG4CPLUS_INFO(logger, "Done computing SCC decomposition of asynchronous_leader/leader7"); + LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(sccDecomposition.first.size(), 1914691u); - ASSERT_EQ(sccDecomposition.second.getNonZeroEntryCount(), 7023587u); + ASSERT_EQ(sccDecomposition.size(), 1914691u); + + LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of asynchronous_leader/leader7..."); + sccDependencyGraph = mdp->extractSccDependencyGraph(sccDecomposition); + LOG4CPLUS_WARN(logger, "Done."); + + ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 7023587u); + + 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", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", ""); std::shared_ptr> mdp2 = parser4.getModel>(); - LOG4CPLUS_INFO(logger, "Computing SCC decomposition of consensus/coin4_6"); + LOG4CPLUS_WARN(logger, "Computing SCC decomposition of consensus/coin4_6..."); sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*mdp2); - LOG4CPLUS_INFO(logger, "Computing SCC decomposition of consensus/coin4_6"); + LOG4CPLUS_WARN(logger, "Done."); + + ASSERT_EQ(sccDecomposition.size(), 63611u); + + LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of consensus/coin4_6..."); + sccDependencyGraph = mdp2->extractSccDependencyGraph(sccDecomposition); + LOG4CPLUS_WARN(logger, "Done."); + + ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 213400u); - ASSERT_EQ(sccDecomposition.first.size(), 63611u); - ASSERT_EQ(sccDecomposition.second.getNonZeroEntryCount(), 213400u); + mdp2 = nullptr; } \ No newline at end of file diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index 3e5aa39b8..bf0a72403 100644 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -22,7 +22,9 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); + LOG4CPLUS_WARN(logger, "Model Checking P=? [F observe0Greater1] on crowds/crowds20_5..."); std::vector* result = probFormula->check(mc); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); @@ -35,8 +37,10 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { eventuallyFormula = new storm::property::prctl::Eventually(apFormula); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); + LOG4CPLUS_WARN(logger, "Model Checking P=? [F observeIGreater1] on crowds/crowds20_5..."); result = probFormula->check(mc); - + LOG4CPLUS_WARN(logger, "Done."); + ASSERT_NE(nullptr, result); ASSERT_LT(std::abs((*result)[0] - 0.05072232915), s->get("precision")); @@ -48,7 +52,9 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { eventuallyFormula = new storm::property::prctl::Eventually(apFormula); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); + LOG4CPLUS_WARN(logger, "Model Checking P=? [F observeOnlyTrueSender] on crowds/crowds20_5..."); result = probFormula->check(mc); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); @@ -77,7 +83,9 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); + LOG4CPLUS_WARN(logger, "Model Checking P=? [F elected] on synchronous_leader/leader6_8..."); std::vector* result = probFormula->check(mc); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); @@ -90,7 +98,9 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { storm::property::prctl::BoundedUntil* boundedUntilFormula = new storm::property::prctl::BoundedUntil(new storm::property::prctl::Ap("true"), apFormula, 20); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedUntilFormula); + LOG4CPLUS_WARN(logger, "Model Checking P=? [F<=20 elected] on synchronous_leader/leader6_8..."); result = probFormula->check(mc); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); @@ -103,7 +113,9 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula); + LOG4CPLUS_WARN(logger, "Model Checking R=? [F elected] on synchronous_leader/leader6_8..."); result = rewardFormula->check(mc); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); diff --git a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp index dc9bea32b..cf8e91581 100644 --- a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp @@ -22,7 +22,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F elected] on asynchronous_leader/leader7..."); std::vector* result = mc.checkNoBoundOperator(*probFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); @@ -35,7 +37,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { eventuallyFormula = new storm::property::prctl::Eventually(apFormula); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); + LOG4CPLUS_WARN(logger, "Model Checking Pmax=? [F elected] on asynchronous_leader/leader7..."); result = mc.checkNoBoundOperator(*probFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); @@ -48,7 +52,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); + LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F<=25 elected] on asynchronous_leader/leader7..."); result = mc.checkNoBoundOperator(*probFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); @@ -61,7 +67,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); + LOG4CPLUS_WARN(logger, "Model Checking Pmax=? [F<=25 elected] on asynchronous_leader/leader7..."); result = mc.checkNoBoundOperator(*probFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); @@ -74,7 +82,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); + LOG4CPLUS_WARN(logger, "Model Checking Rmin=? [F elected] on asynchronous_leader/leader7..."); result = mc.checkNoBoundOperator(*rewardFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_LT(std::abs((*result)[0] - 6.172433512), s->get("precision")); @@ -85,7 +95,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - result = mc.checkNoBoundOperator(*rewardFormula);; + LOG4CPLUS_WARN(logger, "Model Checking Rmax=? [F elected] on asynchronous_leader/leader7..."); + result = mc.checkNoBoundOperator(*rewardFormula); + LOG4CPLUS_WARN(logger, "Done"); ASSERT_NE(nullptr, result); @@ -97,6 +109,8 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { storm::settings::Settings* s = storm::settings::instance(); + s->set("maxiter", 20000); + std::cout << s->get("maxiter") << std::endl; storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", ""); ASSERT_EQ(parser.getType(), storm::models::MDP); @@ -112,7 +126,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F finished] on consensus/coin4_6..."); std::vector* result = mc.checkNoBoundOperator(*probFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); @@ -127,7 +143,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { eventuallyFormula = new storm::property::prctl::Eventually(andFormula); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F finished & all_coins_equal_0] on consensus/coin4_6..."); result = mc.checkNoBoundOperator(*probFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); @@ -142,10 +160,11 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { eventuallyFormula = new storm::property::prctl::Eventually(andFormula); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); + LOG4CPLUS_WARN(logger, "Model Checking Pmax=? [F finished & all_coins_equal_1] on consensus/coin4_6..."); result = mc.checkNoBoundOperator(*probFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[31168] - 0.5282872761373342829216), s->get("precision")); delete probFormula; @@ -158,10 +177,11 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { eventuallyFormula = new storm::property::prctl::Eventually(andFormula); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); + LOG4CPLUS_WARN(logger, "Model Checking Pmax=? [F finished & !agree] on consensus/coin4_6..."); result = mc.checkNoBoundOperator(*probFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[31168] - 0.10343451035775527713), s->get("precision")); delete probFormula; @@ -171,10 +191,11 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 50); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); + LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F<=50 finished] on consensus/coin4_6..."); result = mc.checkNoBoundOperator(*probFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[31168] - 0), s->get("precision")); delete probFormula; @@ -184,10 +205,11 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 50); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); + LOG4CPLUS_WARN(logger, "Model Checking Pmax=? [F<=50 finished] on consensus/coin4_6..."); result = mc.checkNoBoundOperator(*probFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[31168] - 0), s->get("precision")); delete probFormula; @@ -197,8 +219,11 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); + LOG4CPLUS_WARN(logger, "Model Checking Rmin=? [F finished] on consensus/coin4_6..."); result = mc.checkNoBoundOperator(*rewardFormula); + LOG4CPLUS_WARN(logger, "Done."); + ASSERT_NE(nullptr, result); ASSERT_LT(std::abs((*result)[31168] - 1725.5933133943854045), s->get("precision")); delete rewardFormula; @@ -208,10 +233,11 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - result = mc.checkNoBoundOperator(*rewardFormula);; + LOG4CPLUS_WARN(logger, "Model Checking Rmax=? [F finished] on consensus/coin4_6..."); + result = mc.checkNoBoundOperator(*rewardFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[31168] - 2179.014847073392047605011), s->get("precision")); delete rewardFormula; diff --git a/test/performance/storm-performance-tests.cpp b/test/performance/storm-performance-tests.cpp index 1c52acc03..49983a9e1 100644 --- a/test/performance/storm-performance-tests.cpp +++ b/test/performance/storm-performance-tests.cpp @@ -16,7 +16,7 @@ log4cplus::Logger logger; */ void setUpLogging() { logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main")); - logger.setLogLevel(log4cplus::INFO_LOG_LEVEL); + logger.setLogLevel(log4cplus::WARN_LOG_LEVEL); log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender("storm-performance-tests.log")); fileLogAppender->setName("mainFileAppender"); fileLogAppender->setThreshold(log4cplus::WARN_LOG_LEVEL); @@ -42,9 +42,8 @@ bool parseOptions(int const argc, char const * const argv[]) { storm::settings::Settings::registerModule>(); s = storm::settings::newInstance(argc, argv, nullptr, true); } catch (storm::exceptions::InvalidSettingsException& e) { - std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl; - std::cout << std::endl << storm::settings::help; - return false; + // Ignore this case. + return true; } if (s->isSet("help")) { @@ -64,5 +63,8 @@ int main(int argc, char* argv[]) { testing::InitGoogleTest(&argc, argv); - return RUN_ALL_TESTS(); + int result = RUN_ALL_TESTS(); + + logger.closeNestedAppenders(); + return result; } From 3c32eec8e10f3a3dc6c436828da9ecfd340d3f28 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 16 May 2013 16:32:56 +0200 Subject: [PATCH 17/18] Made the prob0/1 algorithms for MDPs share a common backward transition object. --- src/modelchecker/SparseMdpPrctlModelChecker.h | 4 +- src/utility/GraphAnalyzer.h | 40 +++++++++---------- 2 files changed, 22 insertions(+), 22 deletions(-) diff --git a/src/modelchecker/SparseMdpPrctlModelChecker.h b/src/modelchecker/SparseMdpPrctlModelChecker.h index 0c951ae8f..f76092cd2 100644 --- a/src/modelchecker/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/SparseMdpPrctlModelChecker.h @@ -360,9 +360,9 @@ public: storm::storage::BitVector infinityStates; storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); if (this->minimumOperatorStack.top()) { - infinityStates = storm::utility::GraphAnalyzer::performProb1A(this->getModel(), trueStates, *targetStates); + infinityStates = storm::utility::GraphAnalyzer::performProb1A(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, *targetStates); } else { - infinityStates = storm::utility::GraphAnalyzer::performProb1E(this->getModel(), trueStates, *targetStates); + infinityStates = storm::utility::GraphAnalyzer::performProb1E(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, *targetStates); } infinityStates.complement(); diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index 577bccf74..b3eab9727 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -139,8 +139,12 @@ public: template static std::pair performProb01Max(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { std::pair result; - result.first = GraphAnalyzer::performProb0A(model, phiStates, psiStates); - result.second = GraphAnalyzer::performProb1E(model, phiStates, psiStates); + + // Get the backwards transition relation from the model to ease the search. + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); + + result.first = GraphAnalyzer::performProb0A(model, backwardTransitions, phiStates, psiStates); + result.second = GraphAnalyzer::performProb1E(model, backwardTransitions, phiStates, psiStates); return result; } @@ -151,17 +155,15 @@ public: * scheduler tries to maximize this probability. * * @param model The model whose graph structure to search. + * @param backwardTransitions The reversed transition relation of the model. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. * @return A bit vector that represents all states with probability 0. */ template - static storm::storage::BitVector performProb0A(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + static storm::storage::BitVector performProb0A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { // Prepare the resulting bit vector. storm::storage::BitVector statesWithProbability0(model.getNumberOfStates()); - - // Get the backwards transition relation from the model to ease the search. - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); // Add all psi states as the already satisfy the condition. statesWithProbability0 |= psiStates; @@ -196,19 +198,17 @@ public: * scheduler tries to maximize this probability. * * @param model The model whose graph structure to search. + * @param backwardTransitions The reversed transition relation of the model. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. * @return A bit vector that represents all states with probability 1. */ template - static storm::storage::BitVector performProb1E(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + static storm::storage::BitVector performProb1E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { // Get some temporaries for convenience. std::shared_ptr> transitionMatrix = model.getTransitionMatrix(); std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); - // Get the backwards transition relation from the model to ease the search. - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - storm::storage::BitVector currentStates(model.getNumberOfStates(), true); std::vector stack; @@ -274,8 +274,12 @@ public: template static std::pair performProb01Min(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { std::pair result; - result.first = GraphAnalyzer::performProb0E(model, phiStates, psiStates); - result.second = GraphAnalyzer::performProb1A(model, phiStates, psiStates); + + // Get the backwards transition relation from the model to ease the search. + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); + + result.first = GraphAnalyzer::performProb0E(model, backwardTransitions, phiStates, psiStates); + result.second = GraphAnalyzer::performProb1A(model, backwardTransitions, phiStates, psiStates); return result; } @@ -286,12 +290,13 @@ public: * scheduler tries to minimize this probability. * * @param model The model whose graph structure to search. + * @param backwardTransitions The reversed transition relation of the model. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. * @return A bit vector that represents all states with probability 0. */ template - static storm::storage::BitVector performProb0E(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + static storm::storage::BitVector performProb0E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { // Prepare resulting bit vector. storm::storage::BitVector statesWithProbability0(model.getNumberOfStates()); @@ -299,9 +304,6 @@ public: std::shared_ptr> transitionMatrix = model.getTransitionMatrix(); std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); - // Get the backwards transition relation from the model to ease the search. - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - // Add all psi states as the already satisfy the condition. statesWithProbability0 |= psiStates; @@ -355,19 +357,17 @@ public: * scheduler tries to minimize this probability. * * @param model The model whose graph structure to search. + * @param backwardTransitions The reversed transition relation of the model. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. * @return A bit vector that represents all states with probability 0. */ template - static storm::storage::BitVector performProb1A(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + static storm::storage::BitVector performProb1A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { // Get some temporaries for convenience. std::shared_ptr> transitionMatrix = model.getTransitionMatrix(); std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); - // Get the backwards transition relation from the model to ease the search. - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - storm::storage::BitVector currentStates(model.getNumberOfStates(), true); std::vector stack; From 307911ca139a5581a47c0a1fa691dae95c83ea0e Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 16 May 2013 17:41:41 +0200 Subject: [PATCH 18/18] Fixed performance tests, they now run fine. --- src/modelchecker/EigenDtmcPrctlModelChecker.h | 1 - .../SparseDtmcPrctlModelChecker.h | 6 +- src/modelchecker/SparseMdpPrctlModelChecker.h | 10 +- src/utility/Settings.h | 15 +- src/utility/{GraphAnalyzer.h => graph.h} | 323 +++++++++--------- test/performance/graph/GraphTest.cpp | 54 ++- .../GmmxxMdpPrctModelCheckerTest.cpp | 4 +- 7 files changed, 206 insertions(+), 207 deletions(-) rename src/utility/{GraphAnalyzer.h => graph.h} (87%) diff --git a/src/modelchecker/EigenDtmcPrctlModelChecker.h b/src/modelchecker/EigenDtmcPrctlModelChecker.h index 7c5b06ad0..c6e4840c7 100644 --- a/src/modelchecker/EigenDtmcPrctlModelChecker.h +++ b/src/modelchecker/EigenDtmcPrctlModelChecker.h @@ -12,7 +12,6 @@ #include "src/models/Dtmc.h" #include "src/modelchecker/SparseDtmcPrctlModelChecker.h" -#include "src/utility/GraphAnalyzer.h" #include "src/utility/ConstTemplates.h" #include "src/exceptions/NoConvergenceException.h" diff --git a/src/modelchecker/SparseDtmcPrctlModelChecker.h b/src/modelchecker/SparseDtmcPrctlModelChecker.h index 56c7a9525..c19cc471a 100644 --- a/src/modelchecker/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/SparseDtmcPrctlModelChecker.h @@ -11,7 +11,7 @@ #include "src/modelchecker/AbstractModelChecker.h" #include "src/models/Dtmc.h" #include "src/utility/Vector.h" -#include "src/utility/GraphAnalyzer.h" +#include "src/utility/graph.h" #include @@ -209,7 +209,7 @@ public: // Then, we need to identify the states which have to be taken out of the matrix, i.e. // all states that have probability 0 and 1 of satisfying the until-formula. - std::pair statesWithProbability01 = storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates); + std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), *leftStates, *rightStates); storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second); @@ -357,7 +357,7 @@ public: // Determine which states have a reward of infinity by definition. storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); - storm::storage::BitVector infinityStates = storm::utility::GraphAnalyzer::performProb1(this->getModel(), trueStates, *targetStates); + storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->getModel(), trueStates, *targetStates); infinityStates.complement(); // Create resulting vector. diff --git a/src/modelchecker/SparseMdpPrctlModelChecker.h b/src/modelchecker/SparseMdpPrctlModelChecker.h index f76092cd2..8849cd222 100644 --- a/src/modelchecker/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/SparseMdpPrctlModelChecker.h @@ -11,7 +11,7 @@ #include "src/modelchecker/AbstractModelChecker.h" #include "src/models/Mdp.h" #include "src/utility/Vector.h" -#include "src/utility/GraphAnalyzer.h" +#include "src/utility/graph.h" #include #include @@ -215,9 +215,9 @@ public: // all states that have probability 0 and 1 of satisfying the until-formula. std::pair statesWithProbability01; if (this->minimumOperatorStack.top()) { - statesWithProbability01 = storm::utility::GraphAnalyzer::performProb01Min(this->getModel(), *leftStates, *rightStates); + statesWithProbability01 = storm::utility::graph::performProb01Min(this->getModel(), *leftStates, *rightStates); } else { - statesWithProbability01 = storm::utility::GraphAnalyzer::performProb01Max(this->getModel(), *leftStates, *rightStates); + statesWithProbability01 = storm::utility::graph::performProb01Max(this->getModel(), *leftStates, *rightStates); } storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second); @@ -360,9 +360,9 @@ public: storm::storage::BitVector infinityStates; storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); if (this->minimumOperatorStack.top()) { - infinityStates = storm::utility::GraphAnalyzer::performProb1A(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, *targetStates); + infinityStates = storm::utility::graph::performProb1A(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, *targetStates); } else { - infinityStates = storm::utility::GraphAnalyzer::performProb1E(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, *targetStates); + infinityStates = storm::utility::graph::performProb1E(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, *targetStates); } infinityStates.complement(); diff --git a/src/utility/Settings.h b/src/utility/Settings.h index 900b34673..b68aa4e6f 100644 --- a/src/utility/Settings.h +++ b/src/utility/Settings.h @@ -52,7 +52,7 @@ namespace settings { * @brief Get value of a generic option. */ template - inline const T& get( std::string const & name) const { + const T& get(std::string const& name) const { if (this->vm.count(name) == 0) throw storm::exceptions::InvalidSettingsException() << "Could not read option " << name << "."; return this->vm[name].as(); } @@ -60,32 +60,33 @@ namespace settings { /*! * @brief Get value of string option. */ - inline const std::string& getString(std::string const & name) const { + const std::string& getString(std::string const& name) const { return this->get(name); } /*! * @brief Check if an option is set. */ - inline const bool isSet(std::string const & name) const { + const bool isSet(std::string const& name) const { return this->vm.count(name) > 0; } /*! * @brief Set an option. */ - inline void set(std::string const & name) { + void set(std::string const& name) { bpo::variable_value val; - this->vm.insert( std::make_pair(name, val) ); + this->vm.insert(std::make_pair(name, val)); } /*! * @brief Set value for an option. */ template - inline void set(std::string const & name, T const & value) { + void set(std::string const& name, T const& value) { bpo::variable_value val(value, false); - this->vm.insert( std::make_pair(name, val) ); + this->vm.erase(name); + this->vm.insert(std::make_pair(name, val)); } /*! diff --git a/src/utility/GraphAnalyzer.h b/src/utility/graph.h similarity index 87% rename from src/utility/GraphAnalyzer.h rename to src/utility/graph.h index b3eab9727..d3494877d 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/graph.h @@ -5,8 +5,8 @@ * Author: Christian Dehnert */ -#ifndef STORM_UTILITY_GRAPHANALYZER_H_ -#define STORM_UTILITY_GRAPHANALYZER_H_ +#ifndef STORM_UTILITY_GRAPH_H_ +#define STORM_UTILITY_GRAPH_H_ #include "src/models/AbstractDeterministicModel.h" #include "src/models/AbstractNondeterministicModel.h" @@ -20,27 +20,8 @@ extern log4cplus::Logger logger; namespace storm { namespace utility { - -class GraphAnalyzer { -public: - /*! - * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a - * deterministic model. - * - * @param model The model whose graph structure to search. - * @param phiStates The set of all states satisfying phi. - * @param psiStates The set of all states satisfying psi. - * @return A pair of bit vectors such that the first bit vector stores the indices of all states - * with probability 0 and the second stores all indices of states with probability 1. - */ - template - static std::pair performProb01(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - std::pair result; - result.first = GraphAnalyzer::performProbGreater0(model, phiStates, psiStates); - result.second = GraphAnalyzer::performProb1(model, phiStates, psiStates, result.first); - result.first.complement(); - return result; - } + +namespace graph { /*! * Performs a backwards breadt-first search trough the underlying graph structure @@ -53,7 +34,7 @@ public: * @return A bit vector with all indices of states that have a probability greater than 0. */ template - static storm::storage::BitVector performProbGreater0(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector performProbGreater0(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { // Prepare the resulting bit vector. storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates()); @@ -100,8 +81,8 @@ public: * @return A bit vector with all indices of states that have a probability greater than 1. */ template - static storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0) { - storm::storage::BitVector statesWithProbability1 = GraphAnalyzer::performProbGreater0(model, ~psiStates, ~statesWithProbabilityGreater0); + storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0) { + storm::storage::BitVector statesWithProbability1 = performProbGreater0(model, ~psiStates, ~statesWithProbabilityGreater0); statesWithProbability1.complement(); return statesWithProbability1; } @@ -119,32 +100,29 @@ public: * @return A bit vector with all indices of states that have a probability greater than 1. */ template - static storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - storm::storage::BitVector statesWithProbabilityGreater0 = GraphAnalyzer::performProbGreater0(model, phiStates, psiStates); - storm::storage::BitVector statesWithProbability1 = GraphAnalyzer::performProbGreater0(model, ~psiStates, ~(statesWithProbabilityGreater0)); + storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector statesWithProbabilityGreater0 = performProbGreater0(model, phiStates, psiStates); + storm::storage::BitVector statesWithProbability1 = performProbGreater0(model, ~psiStates, ~(statesWithProbabilityGreater0)); statesWithProbability1.complement(); return statesWithProbability1; } - /*! - * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi - * until psi in a non-deterministic model in which all non-deterministic choices are resolved - * such that the probability is maximized. + /*! + * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a + * deterministic model. * * @param model The model whose graph structure to search. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. - * @return A pair of bit vectors that represent all states with probability 0 and 1, respectively. + * @return A pair of bit vectors such that the first bit vector stores the indices of all states + * with probability 0 and the second stores all indices of states with probability 1. */ template - static std::pair performProb01Max(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - std::pair result; - - // Get the backwards transition relation from the model to ease the search. - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - - result.first = GraphAnalyzer::performProb0A(model, backwardTransitions, phiStates, psiStates); - result.second = GraphAnalyzer::performProb1E(model, backwardTransitions, phiStates, psiStates); + static std::pair performProb01(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + std::pair result; + result.first = performProbGreater0(model, phiStates, psiStates); + result.second = performProb1(model, phiStates, psiStates, result.first); + result.first.complement(); return result; } @@ -161,7 +139,7 @@ public: * @return A bit vector that represents all states with probability 0. */ template - static storm::storage::BitVector performProb0A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector performProb0A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { // Prepare the resulting bit vector. storm::storage::BitVector statesWithProbability0(model.getNumberOfStates()); @@ -204,7 +182,7 @@ public: * @return A bit vector that represents all states with probability 1. */ template - static storm::storage::BitVector performProb1E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector performProb1E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { // Get some temporaries for convenience. std::shared_ptr> transitionMatrix = model.getTransitionMatrix(); std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); @@ -261,25 +239,26 @@ public: return currentStates; } - /*! + + /*! * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi * until psi in a non-deterministic model in which all non-deterministic choices are resolved - * such that the probability is minimized. + * such that the probability is maximized. * * @param model The model whose graph structure to search. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. * @return A pair of bit vectors that represent all states with probability 0 and 1, respectively. */ - template - static std::pair performProb01Min(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + template + std::pair performProb01Max(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { std::pair result; // Get the backwards transition relation from the model to ease the search. storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - result.first = GraphAnalyzer::performProb0E(model, backwardTransitions, phiStates, psiStates); - result.second = GraphAnalyzer::performProb1A(model, backwardTransitions, phiStates, psiStates); + result.first = performProb0A(model, backwardTransitions, phiStates, psiStates); + result.second = performProb1E(model, backwardTransitions, phiStates, psiStates); return result; } @@ -296,7 +275,7 @@ public: * @return A bit vector that represents all states with probability 0. */ template - static storm::storage::BitVector performProb0E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector performProb0E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { // Prepare resulting bit vector. storm::storage::BitVector statesWithProbability0(model.getNumberOfStates()); @@ -363,7 +342,7 @@ public: * @return A bit vector that represents all states with probability 0. */ template - static storm::storage::BitVector performProb1A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector performProb1A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { // Get some temporaries for convenience. std::shared_ptr> transitionMatrix = model.getTransitionMatrix(); std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); @@ -420,6 +399,132 @@ public: return currentStates; } + /*! + * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi + * until psi in a non-deterministic model in which all non-deterministic choices are resolved + * such that the probability is minimized. + * + * @param model The model whose graph structure to search. + * @param phiStates The set of all states satisfying phi. + * @param psiStates The set of all states satisfying psi. + * @return A pair of bit vectors that represent all states with probability 0 and 1, respectively. + */ + template + std::pair performProb01Min(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + std::pair result; + + // Get the backwards transition relation from the model to ease the search. + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); + + result.first = performProb0E(model, backwardTransitions, phiStates, psiStates); + result.second = performProb1A(model, backwardTransitions, phiStates, psiStates); + return result; + } + + /*! + * Performs an SCC decomposition using Tarjan's algorithm. + * + * @param startState The state at which the search is started. + * @param currentIndex The index that is to be used as the next free index. + * @param stateIndices The vector that stores the index for each state. + * @param lowlinks A vector that stores the lowlink of each state, i.e. the lowest index of a state reachable from + * a particular state. + * @param tarjanStack A stack used for Tarjan's algorithm. + * @param tarjanStackStates A bit vector that represents all states that are currently contained in tarjanStack. + * @param visitedStates A bit vector that stores all states that have already been visited. + * @param matrix The transition matrix representing the graph structure. + * @param stronglyConnectedComponents A vector of strongly connected components to which newly found SCCs are added. + */ + template + void performSccDecompositionHelper(uint_fast64_t startState, uint_fast64_t& currentIndex, std::vector& stateIndices, std::vector& lowlinks, std::vector& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, storm::storage::SparseMatrix const& matrix, std::vector>& stronglyConnectedComponents) { + // 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 + // all successors of a particular state are considered. + std::vector recursionStateStack; + recursionStateStack.reserve(lowlinks.size()); + std::vector::ConstIndexIterator> recursionIteratorStack; + recursionIteratorStack.reserve(lowlinks.size()); + std::vector statesInStack(lowlinks.size()); + + // Initialize the recursion stacks with the given initial state (and its successor iterator). + recursionStateStack.push_back(startState); + recursionIteratorStack.push_back(matrix.constColumnIteratorBegin(startState)); + + recursionStepForward: + while (!recursionStateStack.empty()) { + uint_fast64_t currentState = recursionStateStack.back(); + typename storm::storage::SparseMatrix::ConstIndexIterator currentIt = recursionIteratorStack.back(); + + // Perform the treatment of newly discovered state as defined by Tarjan's algorithm + visitedStates.set(currentState, true); + stateIndices[currentState] = currentIndex; + lowlinks[currentState] = currentIndex; + ++currentIndex; + tarjanStack.push_back(currentState); + tarjanStackStates.set(currentState, true); + + // Now, traverse all successors of the current state. + for(; currentIt != matrix.constColumnIteratorEnd(currentState); ++currentIt) { + // If we have not visited the successor already, we need to perform the procedure + // recursively on the newly found state. + if (!visitedStates.get(*currentIt)) { + // Save current iterator position so we can continue where we left off later. + recursionIteratorStack.pop_back(); + recursionIteratorStack.push_back(currentIt); + + // Put unvisited successor on top of our recursion stack and remember that. + recursionStateStack.push_back(*currentIt); + statesInStack[*currentIt] = true; + + // Also, put initial value for iterator on corresponding recursion stack. + recursionIteratorStack.push_back(matrix.constColumnIteratorBegin(*currentIt)); + + // Perform the actual recursion step in an iterative way. + goto recursionStepForward; + + recursionStepBackward: + lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[*currentIt]); + } else if (tarjanStackStates.get(*currentIt)) { + // Update the lowlink of the current state. + lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[*currentIt]); + } + } + + // If the current state is the root of a SCC, we need to pop all states of the SCC from + // the algorithm's stack. + if (lowlinks[currentState] == stateIndices[currentState]) { + stronglyConnectedComponents.push_back(std::vector()); + + uint_fast64_t lastState = 0; + do { + // Pop topmost state from the algorithm's stack. + lastState = tarjanStack.back(); + tarjanStack.pop_back(); + tarjanStackStates.set(lastState, false); + + // Add the state to the current SCC. + stronglyConnectedComponents.back().push_back(lastState); + } while (lastState != currentState); + } + + // If we reach this point, we have completed the recursive descent for the current state. + // That is, we need to pop it from the recursion stacks. + recursionStateStack.pop_back(); + recursionIteratorStack.pop_back(); + + // If there is at least one state under the current one in our recursion stack, we need + // to restore the topmost state as the current state and jump to the part after the + // original recursive call. + if (recursionStateStack.size() > 0) { + currentState = recursionStateStack.back(); + currentIt = recursionIteratorStack.back(); + + goto recursionStepBackward; + } + } + } + /*! * Performs a decomposition of the given model into its SCCs. * @@ -427,7 +532,7 @@ public: * @return A vector of SCCs of the model. */ template - static std::vector> performSccDecomposition(storm::models::AbstractModel const& model) { + std::vector> performSccDecomposition(storm::models::AbstractModel const& model) { LOG4CPLUS_INFO(logger, "Computing SCC decomposition."); std::vector> scc; @@ -460,7 +565,7 @@ public: * @return A vector of indices that is a topological sort of the states. */ template - static std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) { + std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) { if (matrix.getRowCount() != matrix.getColumnCount()) { LOG4CPLUS_ERROR(logger, "Provided matrix is required to be square."); throw storm::exceptions::InvalidArgumentException() << "Provided matrix is required to be square."; @@ -531,115 +636,11 @@ public: return topologicalSort; } - -private: - /*! - * Performs an SCC decomposition using Tarjan's algorithm. - * - * @param startState The state at which the search is started. - * @param currentIndex The index that is to be used as the next free index. - * @param stateIndices The vector that stores the index for each state. - * @param lowlinks A vector that stores the lowlink of each state, i.e. the lowest index of a state reachable from - * a particular state. - * @param tarjanStack A stack used for Tarjan's algorithm. - * @param tarjanStackStates A bit vector that represents all states that are currently contained in tarjanStack. - * @param visitedStates A bit vector that stores all states that have already been visited. - * @param matrix The transition matrix representing the graph structure. - * @param stronglyConnectedComponents A vector of strongly connected components to which newly found SCCs are added. - */ - template - static void performSccDecompositionHelper(uint_fast64_t startState, uint_fast64_t& currentIndex, std::vector& stateIndices, std::vector& lowlinks, std::vector& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, storm::storage::SparseMatrix const& matrix, std::vector>& stronglyConnectedComponents) { - // 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 - // all successors of a particular state are considered. - std::vector recursionStateStack; - recursionStateStack.reserve(lowlinks.size()); - std::vector::ConstIndexIterator> recursionIteratorStack; - recursionIteratorStack.reserve(lowlinks.size()); - std::vector statesInStack(lowlinks.size()); - - // Initialize the recursion stacks with the given initial state (and its successor iterator). - recursionStateStack.push_back(startState); - recursionIteratorStack.push_back(matrix.constColumnIteratorBegin(startState)); - - recursionStepForward: - while (!recursionStateStack.empty()) { - uint_fast64_t currentState = recursionStateStack.back(); - typename storm::storage::SparseMatrix::ConstIndexIterator currentIt = recursionIteratorStack.back(); - - // Perform the treatment of newly discovered state as defined by Tarjan's algorithm - visitedStates.set(currentState, true); - stateIndices[currentState] = currentIndex; - lowlinks[currentState] = currentIndex; - ++currentIndex; - tarjanStack.push_back(currentState); - tarjanStackStates.set(currentState, true); - - // Now, traverse all successors of the current state. - for(; currentIt != matrix.constColumnIteratorEnd(currentState); ++currentIt) { - // If we have not visited the successor already, we need to perform the procedure - // recursively on the newly found state. - if (!visitedStates.get(*currentIt)) { - // Save current iterator position so we can continue where we left off later. - recursionIteratorStack.pop_back(); - recursionIteratorStack.push_back(currentIt); - - // Put unvisited successor on top of our recursion stack and remember that. - recursionStateStack.push_back(*currentIt); - statesInStack[*currentIt] = true; - - // Also, put initial value for iterator on corresponding recursion stack. - recursionIteratorStack.push_back(matrix.constColumnIteratorBegin(*currentIt)); - - // Perform the actual recursion step in an iterative way. - goto recursionStepForward; - - recursionStepBackward: - lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[*currentIt]); - } else if (tarjanStackStates.get(*currentIt)) { - // Update the lowlink of the current state. - lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[*currentIt]); - } - } - - // If the current state is the root of a SCC, we need to pop all states of the SCC from - // the algorithm's stack. - if (lowlinks[currentState] == stateIndices[currentState]) { - stronglyConnectedComponents.push_back(std::vector()); - - uint_fast64_t lastState = 0; - do { - // Pop topmost state from the algorithm's stack. - lastState = tarjanStack.back(); - tarjanStack.pop_back(); - tarjanStackStates.set(lastState, false); - - // Add the state to the current SCC. - stronglyConnectedComponents.back().push_back(lastState); - } while (lastState != currentState); - } - - // If we reach this point, we have completed the recursive descent for the current state. - // That is, we need to pop it from the recursion stacks. - recursionStateStack.pop_back(); - recursionIteratorStack.pop_back(); - - // If there is at least one state under the current one in our recursion stack, we need - // to restore the topmost state as the current state and jump to the part after the - // original recursive call. - if (recursionStateStack.size() > 0) { - currentState = recursionStateStack.back(); - currentIt = recursionIteratorStack.back(); - - goto recursionStepBackward; - } - } - } -}; + +} // namespace graph } // namespace utility } // namespace storm -#endif /* STORM_UTILITY_GRAPHANALYZER_H_ */ +#endif /* STORM_UTILITY_GRAPH_H_ */ diff --git a/test/performance/graph/GraphTest.cpp b/test/performance/graph/GraphTest.cpp index 84f264004..4696ad8e5 100644 --- a/test/performance/graph/GraphTest.cpp +++ b/test/performance/graph/GraphTest.cpp @@ -2,25 +2,25 @@ #include "storm-config.h" #include "src/utility/Settings.h" #include "src/parser/AutoParser.h" -#include "src/utility/GraphAnalyzer.h" +#include "src/utility/graph.h" -TEST(GraphAnalyzerTest, PerformProb01) { +TEST(GraphTest, PerformProb01) { 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 prob01 (3 times) for crowds/crowds20_5..."); - std::pair prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observe0Greater1"))); + std::pair prob01 = storm::utility::graph::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observe0Greater1"))); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 1724414u); ASSERT_EQ(prob01.second.getNumberOfSetBits(), 46046u); - prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observeIGreater1"))); + prob01 = storm::utility::graph::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observeIGreater1"))); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 574016u); ASSERT_EQ(prob01.second.getNumberOfSetBits(), 825797u); - prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observeOnlyTrueSender"))); + prob01 = storm::utility::graph::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observeOnlyTrueSender"))); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 1785309u); ASSERT_EQ(prob01.second.getNumberOfSetBits(), 40992u); @@ -28,12 +28,12 @@ TEST(GraphAnalyzerTest, PerformProb01) { 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", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew"); + 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 prob01 for synchronous_leader/leader6_8..."); - prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc2, storm::storage::BitVector(dtmc2->getNumberOfStates(), true), storm::storage::BitVector(dtmc2->getLabeledStates("elected"))); + prob01 = storm::utility::graph::performProb01(*dtmc2, storm::storage::BitVector(dtmc2->getNumberOfStates(), true), storm::storage::BitVector(dtmc2->getLabeledStates("elected"))); LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); @@ -42,19 +42,19 @@ TEST(GraphAnalyzerTest, PerformProb01) { dtmc2 = nullptr; } -TEST(GraphAnalyzerTest, PerformProb01MinMax) { - storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew"); +TEST(GraphTest, PerformProb01MinMax) { + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", ""); std::shared_ptr> mdp = parser.getModel>(); LOG4CPLUS_WARN(logger, "Computing prob01min for asynchronous_leader/leader7..."); - std::pair prob01 = storm::utility::GraphAnalyzer::performProb01Min(*mdp, storm::storage::BitVector(mdp->getNumberOfStates(), true), mdp->getLabeledStates("elected")); + std::pair prob01 = storm::utility::graph::performProb01Min(*mdp, storm::storage::BitVector(mdp->getNumberOfStates(), true), mdp->getLabeledStates("elected")); LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); ASSERT_EQ(prob01.second.getNumberOfSetBits(), 2095783u); LOG4CPLUS_WARN(logger, "Computing prob01max for asynchronous_leader/leader7..."); - prob01 = storm::utility::GraphAnalyzer::performProb01Max(*mdp, storm::storage::BitVector(mdp->getNumberOfStates(), true), mdp->getLabeledStates("elected")); + prob01 = storm::utility::graph::performProb01Max(*mdp, storm::storage::BitVector(mdp->getNumberOfStates(), true), mdp->getLabeledStates("elected")); LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); @@ -62,18 +62,18 @@ TEST(GraphAnalyzerTest, PerformProb01MinMax) { mdp = nullptr; - storm::parser::AutoParser parser2(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", ""); + storm::parser::AutoParser parser2(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", "", ""); std::shared_ptr> mdp2 = parser2.getModel>(); LOG4CPLUS_WARN(logger, "Computing prob01min for consensus/coin4_6..."); - prob01 = storm::utility::GraphAnalyzer::performProb01Min(*mdp2, storm::storage::BitVector(mdp2->getNumberOfStates(), true), mdp2->getLabeledStates("finished")); + prob01 = storm::utility::graph::performProb01Min(*mdp2, storm::storage::BitVector(mdp2->getNumberOfStates(), true), mdp2->getLabeledStates("finished")); LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); ASSERT_EQ(prob01.second.getNumberOfSetBits(), 63616u); LOG4CPLUS_WARN(logger, "Computing prob01max for consensus/coin4_6..."); - prob01 = storm::utility::GraphAnalyzer::performProb01Max(*mdp2, storm::storage::BitVector(mdp2->getNumberOfStates(), true), mdp2->getLabeledStates("finished")); + prob01 = storm::utility::graph::performProb01Max(*mdp2, storm::storage::BitVector(mdp2->getNumberOfStates(), true), mdp2->getLabeledStates("finished")); LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); @@ -82,12 +82,12 @@ TEST(GraphAnalyzerTest, PerformProb01MinMax) { mdp2 = nullptr; } -TEST(GraphAnalyzerTest, PerformSCCDecompositionAndGetDependencyGraph) { +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..."); - std::vector> sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*dtmc); + std::vector> sccDecomposition = storm::utility::graph::performSccDecomposition(*dtmc); LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(sccDecomposition.size(), 1290297u); @@ -100,11 +100,11 @@ TEST(GraphAnalyzerTest, PerformSCCDecompositionAndGetDependencyGraph) { 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", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew"); + 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::utility::GraphAnalyzer::performSccDecomposition(*dtmc2); + sccDecomposition = storm::utility::graph::performSccDecomposition(*dtmc2); LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(sccDecomposition.size(), 1279673u); @@ -117,30 +117,28 @@ TEST(GraphAnalyzerTest, PerformSCCDecompositionAndGetDependencyGraph) { dtmc2 = nullptr; - /* - storm::parser::AutoParser parser3(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew"); + 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/leader7..."); - sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*mdp); + LOG4CPLUS_WARN(logger, "Computing SCC decomposition of asynchronous_leader/leader6..."); + sccDecomposition = storm::utility::graph::performSccDecomposition(*mdp); LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(sccDecomposition.size(), 1914691u); + ASSERT_EQ(sccDecomposition.size(), 214675); - LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of asynchronous_leader/leader7..."); + LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of asynchronous_leader/leader6..."); sccDependencyGraph = mdp->extractSccDependencyGraph(sccDecomposition); LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 7023587u); + ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 684093u); 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", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", ""); + 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::utility::GraphAnalyzer::performSccDecomposition(*mdp2); + sccDecomposition = storm::utility::graph::performSccDecomposition(*mdp2); LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(sccDecomposition.size(), 63611u); diff --git a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp index cf8e91581..971c7ec09 100644 --- a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp @@ -110,7 +110,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { storm::settings::Settings* s = storm::settings::instance(); s->set("maxiter", 20000); - std::cout << s->get("maxiter") << std::endl; + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", ""); ASSERT_EQ(parser.getType(), storm::models::MDP); @@ -149,7 +149,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[31168] - 0.4370098591707694546393), s->get("precision")); + ASSERT_LT(std::abs((*result)[31168] - 0.43742828319177884388579), s->get("precision")); delete probFormula; delete result;