From 824c28f3328d495fb6f4fcad7f68c8e6e69e9403 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 17 Mar 2020 15:11:58 +0100 Subject: [PATCH 1/5] Instantiation for POMDPs in Propositional model checkers. --- src/storm/modelchecker/AbstractModelChecker.cpp | 3 +++ .../propositional/SparsePropositionalModelChecker.cpp | 3 +++ 2 files changed, 6 insertions(+) diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index 233aa1733..67f03bc9a 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -14,6 +14,7 @@ #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Ctmc.h" #include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/Pomdp.h" #include "storm/models/symbolic/Dtmc.h" #include "storm/models/symbolic/Ctmc.h" #include "storm/models/symbolic/Mdp.h" @@ -328,6 +329,7 @@ namespace storm { template class AbstractModelChecker>; template class AbstractModelChecker>; template class AbstractModelChecker>; + template class AbstractModelChecker>; template class AbstractModelChecker>; #ifdef STORM_HAVE_CARL @@ -337,6 +339,7 @@ namespace storm { template class AbstractModelChecker>; template class AbstractModelChecker>; template class AbstractModelChecker>; + template class AbstractModelChecker>; template class AbstractModelChecker>; template class AbstractModelChecker>; diff --git a/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp index e0497b95e..cbd135612 100644 --- a/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp +++ b/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp @@ -5,6 +5,7 @@ #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Ctmc.h" #include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/Pomdp.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -55,6 +56,7 @@ namespace storm { template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; + template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; #ifdef STORM_HAVE_CARL @@ -64,6 +66,7 @@ namespace storm { template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; + template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; From 27ac99806e098a3c473241aa516c5111dd53f965 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 17 Mar 2020 15:12:21 +0100 Subject: [PATCH 2/5] Stopwatch: added restart() method --- src/storm/utility/Stopwatch.cpp | 5 +++++ src/storm/utility/Stopwatch.h | 5 +++++ 2 files changed, 10 insertions(+) diff --git a/src/storm/utility/Stopwatch.cpp b/src/storm/utility/Stopwatch.cpp index f694df496..b863c8da5 100644 --- a/src/storm/utility/Stopwatch.cpp +++ b/src/storm/utility/Stopwatch.cpp @@ -55,6 +55,11 @@ namespace storm { isStopped = true; } + void Stopwatch::restart() { + reset(); + start(); + } + bool Stopwatch::stopped() const { return isStopped; } diff --git a/src/storm/utility/Stopwatch.h b/src/storm/utility/Stopwatch.h index e3b41f4e9..c90bd8c7e 100644 --- a/src/storm/utility/Stopwatch.h +++ b/src/storm/utility/Stopwatch.h @@ -66,6 +66,11 @@ namespace storm { */ void reset(); + /*! + * Reset the stopwatch and immediately start it + */ + void restart(); + /*! * Retrieves whether the watch is stopped. */ From 542f94babd22317de232e8901ac1a54c205ff647 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 6 Mar 2020 12:16:19 -0800 Subject: [PATCH 3/5] report on gurobi library, extended libraries and prefer (empirically) newer versions over older versions --- resources/3rdparty/CMakeLists.txt | 2 +- resources/cmake/find_modules/FindGurobi.cmake | 95 ++++++++++--------- 2 files changed, 51 insertions(+), 46 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index a23de4601..46e927d85 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -201,7 +201,7 @@ if (STORM_USE_GUROBI) set(STORM_HAVE_GUROBI ${GUROBI_FOUND}) if (GUROBI_FOUND) if (EXISTS ${GUROBI_LIBRARY}) - message (STATUS "Storm - Linking with Gurobi.") + message (STATUS "Storm - Linking with Gurobi (${GUROBI_CXX_LIBRARY}).") add_imported_library(Gurobi SHARED ${GUROBI_LIBRARY} ${GUROBI_INCLUDE_DIRS}) list(APPEND STORM_DEP_TARGETS Gurobi_SHARED) else() diff --git a/resources/cmake/find_modules/FindGurobi.cmake b/resources/cmake/find_modules/FindGurobi.cmake index 1378e0ab8..a0e1f09d1 100644 --- a/resources/cmake/find_modules/FindGurobi.cmake +++ b/resources/cmake/find_modules/FindGurobi.cmake @@ -18,66 +18,71 @@ else (GUROBI_INCLUDE_DIR) find_path(GUROBI_INCLUDE_DIR NAMES gurobi_c++.h PATHS "$ENV{GUROBI_HOME}/include" - "/Library/gurobi502/mac64/include" - "/Library/gurobi602/mac64/include" - "/Library/gurobi604/mac64/include" - "/Library/gurobi605/mac64/include" - "/Library/gurobi650/mac64/include" - "/Library/gurobi651/mac64/include" - "/Library/gurobi652/mac64/include" - "/Library/gurobi702/mac64/include" - "/Library/gurobi801/mac64/include" - "/Library/gurobi810/mac64/include" "/Library/gurobi900/mac64/include" + "/Library/gurobi811/mac64/include" + "/Library/gurobi810/mac64/include" + "/Library/gurobi801/mac64/include" + "/Library/gurobi702/mac64/include" + "/Library/gurobi652/mac64/include" + "/Library/gurobi651/mac64/include" + "/Library/gurobi650/mac64/include" + "/Library/gurobi605/mac64/include" + "/Library/gurobi604/mac64/include" + "/Library/gurobi602/mac64/include" + "/Library/gurobi502/mac64/include" "${GUROBI_ROOT}/include" ) find_library( GUROBI_LIBRARY NAMES gurobi - gurobi45 - gurobi46 - gurobi50 - gurobi51 - gurobi52 - gurobi55 - gurobi56 - gurobi60 - gurobi65 - gurobi70 - gurobi75 - gurobi80 - gurobi81 gurobi90 + gurobi81 + gurobi80 + gurobi75 + gurobi70 + gurobi65 + gurobi60 + gurobi56 + gurobi55 + gurobi52 + gurobi51 + gurobi50 + gurobi46 + gurobi45 PATHS "$ENV{GUROBI_HOME}/lib" - "/Library/gurobi502/mac64/lib" - "/Library/gurobi602/mac64/lib" - "/Library/gurobi604/mac64/lib" - "/Library/gurobi605/mac64/lib" - "/Library/gurobi650/mac64/lib" - "/Library/gurobi651/mac64/lib" - "/Library/gurobi652/mac64/lib" - "/Library/gurobi702/mac64/lib" - "/Library/gurobi801/mac64/lib" - "/Library/gurobi810/mac64/lib" - "/Library/gurobi811/mac64/lib" + "/Library/gurobi900/mac64/lib" + "/Library/gurobi811/mac64/lib" + "/Library/gurobi810/mac64/lib" + "/Library/gurobi801/mac64/lib" + "/Library/gurobi702/mac64/lib" + "/Library/gurobi652/mac64/lib" + "/Library/gurobi651/mac64/lib" + "/Library/gurobi650/mac64/lib" + "/Library/gurobi605/mac64/lib" + "/Library/gurobi604/mac64/lib" + "/Library/gurobi602/mac64/lib" + "/Library/gurobi502/mac64/lib" "${GUROBI_ROOT}/lib" ) find_library( GUROBI_CXX_LIBRARY NAMES gurobi_c++ - PATHS "$ENV{GUROBI_HOME}/lib" - "/Library/gurobi502/mac64/lib" - "/Library/gurobi602/mac64/lib" - "/Library/gurobi604/mac64/lib" - "/Library/gurobi605/mac64/lib" - "/Library/gurobi650/mac64/lib" - "/Library/gurobi651/mac64/lib" - "/Library/gurobi652/mac64/lib" - "/Library/gurobi702/mac64/lib" - "/Library/gurobi801/mac64/lib" - "/Library/gurobi810/mac64/lib" + PATHS "$ENV{GUROBI_HOME}/lib" + "/Library/gurobi900/mac64/lib" + "/Library/gurobi811/mac64/lib" + "/Library/gurobi810/mac64/lib" + "/Library/gurobi801/mac64/lib" + "/Library/gurobi702/mac64/lib" + "/Library/gurobi652/mac64/lib" + "/Library/gurobi651/mac64/lib" + "/Library/gurobi650/mac64/lib" + "/Library/gurobi605/mac64/lib" + "/Library/gurobi604/mac64/lib" + "/Library/gurobi602/mac64/lib" + "/Library/gurobi502/mac64/lib" + "${GUROBI_ROOT}/lib" ) From 22e20e93a920b8fad53382c88de79394679faf39 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 6 Mar 2020 13:52:32 -0800 Subject: [PATCH 4/5] permissive strategy test should also run without mathsat --- .../permissiveschedulers/SmtPermissiveSchedulerTest.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp b/src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp index 8fd55a942..0553c691c 100644 --- a/src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp +++ b/src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp @@ -12,11 +12,8 @@ #include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" -#if defined STORM_HAVE_MSAT TEST(SmtPermissiveSchedulerTest, DieSelection) { -#else -TEST(SmtPermissiveSchedulerTest, DISABLED_DieSelection) { -#endif + storm::Environment env; storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/die_c1.nm"); storm::parser::FormulaParser formulaParser(program); From 01e3752d094eeaa6599c6e604efd6535ad47e90f Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 17 Mar 2020 13:33:15 -0700 Subject: [PATCH 5/5] updated changelog --- CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index b76fa2dc7..149861c2e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,10 @@ The releases of major and minor versions contain an overview of changes since th Version 1.5.x ------------- +## Version 1.5.x (Under development) +- CMake: Search for Gurobi prefers new versions +- Tests: Enabled tests for permissive schedulers + ## Version 1.5.1 (2020/03) - Jani models are now parsed using exact arithmetic.