diff --git a/CMakeLists.txt b/CMakeLists.txt index 1a5a9a0bd..a78fb8925 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}") @@ -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") @@ -126,10 +126,12 @@ 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 -file(GLOB_RECURSE STORM_TEST_FILES ${PROJECT_SOURCE_DIR}/test/*.h ${PROJECT_SOURCE_DIR}/test/*.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}) @@ -141,7 +143,9 @@ 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(test FILES ${STORM_TEST_FILES}) +source_group(ir FILES ${STORM_IR_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}") @@ -224,15 +228,18 @@ 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}) -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) @@ -253,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 @@ -279,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() @@ -293,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) @@ -315,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 @@ -324,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/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/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/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 ] 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/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/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/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/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/SparseDtmcPrctlModelChecker.h b/src/modelchecker/SparseDtmcPrctlModelChecker.h index f55f79db5..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 @@ -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; } @@ -211,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); @@ -359,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 b9c80e24b..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 @@ -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()); @@ -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(), trueStates, *targetStates); + infinityStates = storm::utility::graph::performProb1A(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, *targetStates); } else { - infinityStates = storm::utility::GraphAnalyzer::performProb1E(this->getModel(), trueStates, *targetStates); + infinityStates = storm::utility::graph::performProb1E(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, *targetStates); } infinityStates.complement(); 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 f7594ba05..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 @@ -47,44 +46,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) const { + return this->transitionMatrix->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) const { + return this->transitionMatrix->constColumnIteratorEnd(state); } }; diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 364e501b0..c4896a6c6 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -91,7 +91,120 @@ 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; + 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(); + + 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[*succIt]; + + // 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 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. + * + * @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) const = 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) const = 0; /*! * Returns the state space size of the model. @@ -220,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 4c51f0863..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,51 +55,8 @@ 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(); } - - /*! - * 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 +76,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) const { + return this->transitionMatrix->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) const { + return this->transitionMatrix->constColumnIteratorEnd((*nondeterministicChoiceIndices)[state + 1] - 1); + } private: /*! A vector of indices mapping states to the choices (rows) in the transition matrix. */ 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/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/PrctlFileParser.cpp b/src/parser/PrctlFileParser.cpp index ed5f15a2b..4fa7a13d3 100644 --- a/src/parser/PrctlFileParser.cpp +++ b/src/parser/PrctlFileParser.cpp @@ -40,7 +40,11 @@ std::list*> PrctlFileParser //The while loop reads the input file line by line while (std::getline(inputFileStream, line)) { 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 c79485dc0..88098561d 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) { - 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; @@ -58,36 +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 = (qi::lit("P") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = - phoenix::new_ >(qi::_1)]; + 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"); - rewardNoBoundOperator = (qi::lit("R") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val = - phoenix::new_ >(qi::_1)]; + + 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)] + + ); rewardNoBoundOperator.name("no bound operator"); //This block defines rules for parsing probabilistic path formulas @@ -95,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); @@ -123,11 +142,18 @@ struct PrctlParser::PrctlGrammar : qi::grammar>()]; - start = (noBoundOperator | stateFormula); + 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; qi::rule*(), Skipper> atomicStateFormula; @@ -158,6 +184,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar freeIdentifierName; + qi::rule comparisonType; }; @@ -207,12 +234,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 (result_pointer == nullptr) { - 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; diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index b0d2a1cc2..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. } /*! @@ -219,11 +219,31 @@ 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) { - + // 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/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 79% rename from src/utility/GraphAnalyzer.h rename to src/utility/graph.h index c8530e7ef..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,12 +34,12 @@ 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()); // 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 +54,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); @@ -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,28 +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; - result.first = GraphAnalyzer::performProb0A(model, phiStates, psiStates); - result.second = GraphAnalyzer::performProb1E(model, 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; } @@ -151,17 +133,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) { + 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::models::GraphTransitions backwardTransitions(*model.getTransitionMatrix(), *model.getNondeterministicChoiceIndices(), false); // Add all psi states as the already satisfy the condition. statesWithProbability0 |= psiStates; @@ -176,7 +156,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); @@ -196,19 +176,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) { + 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::models::GraphTransitions backwardTransitions(*model.getTransitionMatrix(), *model.getNondeterministicChoiceIndices(), false); - storm::storage::BitVector currentStates(model.getNumberOfStates(), true); std::vector stack; @@ -225,7 +203,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. @@ -261,21 +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; - 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 = performProb0A(model, backwardTransitions, phiStates, psiStates); + result.second = performProb1E(model, backwardTransitions, phiStates, psiStates); return result; } @@ -286,12 +269,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) { + 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 +283,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::models::GraphTransitions backwardTransitions(*transitionMatrix, *nondeterministicChoiceIndices, false); - // Add all psi states as the already satisfy the condition. statesWithProbability0 |= psiStates; @@ -315,7 +296,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. @@ -355,19 +336,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) { + 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::models::GraphTransitions backwardTransitions(*model.getTransitionMatrix(), *model.getNondeterministicChoiceIndices(), false); - storm::storage::BitVector currentStates(model.getNumberOfStates(), true); std::vector stack; @@ -384,7 +363,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 +400,142 @@ public: } /*! - * Performs a decomposition of the given nondeterministic model into its SCCs. + * 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. * * @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::models::GraphTransitions> performSccDecomposition(storm::models::AbstractNondeterministicModel const& model) { + std::vector> performSccDecomposition(storm::models::AbstractModel const& model) { LOG4CPLUS_INFO(logger, "Computing SCC decomposition."); - std::pair>, storm::models::GraphTransitions> sccDecomposition; + std::vector> scc; uint_fast64_t numberOfStates = model.getNumberOfStates(); // Set up the environment of Tarjan's algorithm. @@ -441,21 +545,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; } /*! @@ -465,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."; @@ -536,117 +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. - * @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) { - // 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); - stateToSccMap[lastState] = stronglyConnectedComponents.size() - 1; - } 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/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/die/testFormulas.prctl b/test/functional/die/testFormulas.prctl deleted file mode 100644 index 8deea6c43..000000000 --- a/test/functional/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/eigen/EigenSparseMatrixTest.cpp b/test/functional/eigen/EigenSparseMatrixTest.cpp similarity index 96% rename from test/eigen/EigenSparseMatrixTest.cpp rename to test/functional/eigen/EigenSparseMatrixTest.cpp index 67b70f986..d050a6948 100644 --- a/test/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/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 90% rename from test/functional/GmmxxDtmcPrctModelCheckerTest.cpp rename to test/functional/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index aa2a014fa..e3eb08b68 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_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/crowds/crowds5_5.tra", STORM_CPP_TESTS_BASE_PATH "/functional/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/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_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/GmmxxMdpPrctModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp similarity index 88% rename from test/functional/GmmxxMdpPrctModelCheckerTest.cpp rename to test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp index 13136cc69..32cf5b9a4 100644 --- a/test/functional/GmmxxMdpPrctModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp @@ -7,171 +7,171 @@ 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_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); - + 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_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); - + 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_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); - + 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; } 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_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/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 96% rename from test/parser/CslParserTest.cpp rename to test/functional/parser/CslParserTest.cpp index 2ebd8ea16..f6657289c 100644 --- a/test/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); @@ -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/parser/LtlParserTest.cpp b/test/functional/parser/LtlParserTest.cpp similarity index 97% rename from test/parser/LtlParserTest.cpp rename to test/functional/parser/LtlParserTest.cpp index 1a50ddb28..c88885372 100644 --- a/test/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; diff --git a/test/parser/ParseMdpTest.cpp b/test/functional/parser/ParseMdpTest.cpp similarity index 82% rename from test/parser/ParseMdpTest.cpp rename to test/functional/parser/ParseMdpTest.cpp index 55da2ae32..dfaa0ac15 100644 --- a/test/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/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 89% rename from test/parser/ReadLabFileTest.cpp rename to test/functional/parser/ReadLabFileTest.cpp index b17f91738..2c3122209 100644 --- a/test/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/parser/ReadTraFileTest.cpp b/test/functional/parser/ReadTraFileTest.cpp similarity index 84% rename from test/parser/ReadTraFileTest.cpp rename to test/functional/parser/ReadTraFileTest.cpp index 35ecfcbcc..fd86a8820 100644 --- a/test/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/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 84% rename from test/storm-tests.cpp rename to test/functional/storm-functional-tests.cpp index e5d78bb5e..abfb5a125 100644 --- a/test/storm-tests.cpp +++ b/test/functional/storm-functional-tests.cpp @@ -15,10 +15,12 @@ log4cplus::Logger logger; * Initializes the logging framework. */ void setUpLogging() { - log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender("storm-tests.log")); + 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 @@ -58,9 +60,12 @@ 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); - 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 new file mode 100644 index 000000000..4696ad8e5 --- /dev/null +++ b/test/performance/graph/GraphTest.cpp @@ -0,0 +1,153 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/utility/Settings.h" +#include "src/parser/AutoParser.h" +#include "src/utility/graph.h" + +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::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::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::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); + 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", "", ""); + + std::shared_ptr> dtmc2 = parser2.getModel>(); + + LOG4CPLUS_WARN(logger, "Computing prob01 for synchronous_leader/leader6_8..."); + 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); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 1312334u); + + dtmc2 = nullptr; +} + +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::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::graph::performProb01Max(*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); + + 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", "", ""); + std::shared_ptr> mdp2 = parser2.getModel>(); + + LOG4CPLUS_WARN(logger, "Computing prob01min for consensus/coin4_6..."); + 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::graph::performProb01Max(*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); + + mdp2 = nullptr; +} + +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::graph::performSccDecomposition(*dtmc); + LOG4CPLUS_WARN(logger, "Done."); + + 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", "", ""); + std::shared_ptr> dtmc2 = parser2.getModel>(); + + LOG4CPLUS_WARN(logger, "Computing SCC decomposition of synchronous_leader/leader6_8..."); + sccDecomposition = storm::utility::graph::performSccDecomposition(*dtmc2); + LOG4CPLUS_WARN(logger, "Done."); + + 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/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/leader6..."); + sccDecomposition = storm::utility::graph::performSccDecomposition(*mdp); + LOG4CPLUS_WARN(logger, "Done."); + + ASSERT_EQ(sccDecomposition.size(), 214675); + + LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of asynchronous_leader/leader6..."); + sccDependencyGraph = mdp->extractSccDependencyGraph(sccDecomposition); + LOG4CPLUS_WARN(logger, "Done."); + + 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", "", ""); + std::shared_ptr> mdp2 = parser4.getModel>(); + + LOG4CPLUS_WARN(logger, "Computing SCC decomposition of consensus/coin4_6..."); + sccDecomposition = storm::utility::graph::performSccDecomposition(*mdp2); + 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); + + mdp2 = nullptr; +} \ No newline at end of file diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp new file mode 100644 index 000000000..bf0a72403 --- /dev/null +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -0,0 +1,126 @@ +#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(), 2036647u); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 8973900u); + + 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); + + 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); + + ASSERT_LT(std::abs((*result)[0] - 0.2296803699), 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); + + 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")); + + 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); + + LOG4CPLUS_WARN(logger, "Model Checking P=? [F observeOnlyTrueSender] on crowds/crowds20_5..."); + result = probFormula->check(mc); + LOG4CPLUS_WARN(logger, "Done."); + + ASSERT_NE(nullptr, result); + + 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"); + 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(), 1312334u); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 2886810u); + + 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); + + 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); + + 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); + + 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); + + ASSERT_LT(std::abs((*result)[0] - 0.999394979327824395376467), 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); + + 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); + + ASSERT_LT(std::abs((*result)[0] - 1.02521744572240791626427), 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..971c7ec09 --- /dev/null +++ b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp @@ -0,0 +1,246 @@ +#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(), 2095783u); + ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385u); + + 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); + + 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); + + 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); + + LOG4CPLUS_WARN(logger, "Model Checking Pmax=? [F elected] on asynchronous_leader/leader7..."); + result = mc.checkNoBoundOperator(*probFormula); + LOG4CPLUS_WARN(logger, "Done."); + + 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); + + 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); + + ASSERT_LT(std::abs((*result)[0] - 0), 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); + + 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); + + ASSERT_LT(std::abs((*result)[0] - 0), 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); + + 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")); + + 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); + + LOG4CPLUS_WARN(logger, "Model Checking Rmax=? [F elected] on asynchronous_leader/leader7..."); + result = mc.checkNoBoundOperator(*rewardFormula); + LOG4CPLUS_WARN(logger, "Done"); + + ASSERT_NE(nullptr, result); + + ASSERT_LT(std::abs((*result)[0] - 6.1724344), s->get("precision")); + + delete rewardFormula; + delete result; +} + +TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { + storm::settings::Settings* s = storm::settings::instance(); + s->set("maxiter", 20000); + + 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"); + 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); + + ASSERT_LT(std::abs((*result)[31168] - 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); + + 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); + + ASSERT_LT(std::abs((*result)[31168] - 0.43742828319177884388579), 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, 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; + 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, 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; + 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); + + 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; + 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); + + 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; + 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); + + 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; + delete result; + + apFormula = new storm::property::prctl::Ap("finished"); + reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); + rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); + + 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; + delete result; + +} \ No newline at end of file diff --git a/test/performance/storm-performance-tests.cpp b/test/performance/storm-performance-tests.cpp new file mode 100644 index 000000000..49983a9e1 --- /dev/null +++ b/test/performance/storm-performance-tests.cpp @@ -0,0 +1,70 @@ +#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() { + logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main")); + 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); + fileLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M} (%r ms) - %F:%L : %m%n"))); + 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) { + // Ignore this case. + return true; + } + + 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); + + int result = RUN_ALL_TESTS(); + + logger.closeNestedAppenders(); + return result; +}