sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Merge remote-tracking branch 'origin/prism-pomdp' into prism-pomdp

main
Alexander Bork 5 years ago
parent
c303ba361f c1d0d332c1
commit
9e0163ef9a
8 changed files with 72 additions and 50 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      CHANGELOG.md
  2. 2
      resources/3rdparty/CMakeLists.txt
  3. 95
      resources/cmake/find_modules/FindGurobi.cmake
  4. 3
      src/storm/modelchecker/AbstractModelChecker.cpp
  5. 3
      src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp
  6. 5
      src/storm/utility/Stopwatch.cpp
  7. 5
      src/storm/utility/Stopwatch.h
  8. 5
      src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp

4
CHANGELOG.md
View File

@ -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.

2
resources/3rdparty/CMakeLists.txt
View File

@ -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()

95
resources/cmake/find_modules/FindGurobi.cmake
View File

@ -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"
)

3
src/storm/modelchecker/AbstractModelChecker.cpp
View File

@ -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<storm::models::sparse::Dtmc<double>>;
template class AbstractModelChecker<storm::models::sparse::Ctmc<double>>;
template class AbstractModelChecker<storm::models::sparse::Mdp<double>>;
template class AbstractModelChecker<storm::models::sparse::Pomdp<double>>;
template class AbstractModelChecker<storm::models::sparse::MarkovAutomaton<double>>;
#ifdef STORM_HAVE_CARL
@ -337,6 +339,7 @@ namespace storm {
template class AbstractModelChecker<storm::models::sparse::Dtmc<storm::RationalNumber>>;
template class AbstractModelChecker<storm::models::sparse::Ctmc<storm::RationalNumber>>;
template class AbstractModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>>;
template class AbstractModelChecker<storm::models::sparse::Pomdp<storm::RationalNumber>>;
template class AbstractModelChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
template class AbstractModelChecker<storm::models::sparse::Model<storm::RationalFunction>>;

3
src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp
View File

@ -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<storm::models::sparse::Dtmc<double>>;
template class SparsePropositionalModelChecker<storm::models::sparse::Ctmc<double>>;
template class SparsePropositionalModelChecker<storm::models::sparse::Mdp<double>>;
template class SparsePropositionalModelChecker<storm::models::sparse::Pomdp<double>>;
template class SparsePropositionalModelChecker<storm::models::sparse::MarkovAutomaton<double>>;
#ifdef STORM_HAVE_CARL
@ -64,6 +66,7 @@ namespace storm {
template class SparsePropositionalModelChecker<storm::models::sparse::Dtmc<storm::RationalNumber>>;
template class SparsePropositionalModelChecker<storm::models::sparse::Ctmc<storm::RationalNumber>>;
template class SparsePropositionalModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>>;
template class SparsePropositionalModelChecker<storm::models::sparse::Pomdp<storm::RationalNumber>>;
template class SparsePropositionalModelChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
template class SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>>;

5
src/storm/utility/Stopwatch.cpp
View File

@ -55,6 +55,11 @@ namespace storm {
isStopped = true;
}
void Stopwatch::restart() {
reset();
start();
}
bool Stopwatch::stopped() const {
return isStopped;
}

5
src/storm/utility/Stopwatch.h
View File

@ -66,6 +66,11 @@ namespace storm {
*/
void reset();
/*!
* Reset the stopwatch and immediately start it
*/
void restart();
/*!
* Retrieves whether the watch is stopped.
*/

5
src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
View File

@ -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);

Write Preview
Loading…
Cancel
Save