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. 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" ) 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>; 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. */ 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);