Browse Source

Added CMAKE option STORM_LOAD_QVBS to automatically download the quantitative verification benchmark set

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
commit
90ade051c2
  1. 1
      CHANGELOG.md
  2. 4
      CMakeLists.txt
  3. 22
      resources/3rdparty/CMakeLists.txt

1
CHANGELOG.md

@ -12,6 +12,7 @@ Version 1.5.x
- Scheduler export: Properly handle models with end components. Added export in `.json` format. - Scheduler export: Properly handle models with end components. Added export in `.json` format.
- CMake: Search for Gurobi prefers new versions - CMake: Search for Gurobi prefers new versions
- CMake: We no longer ship xerces-c. If xerces-c is not found on the system, storm-gspn will not be able to parse xml-based GSPN formats - CMake: We no longer ship xerces-c. If xerces-c is not found on the system, storm-gspn will not be able to parse xml-based GSPN formats
- CMake: Added option `STORM_LOAD_QVBS` to automatically download the quantitative verification benchmark set.
- Eigen library: The source code of Eigen is no longer included but downloaded from an external repository instead. Incremented Eigen version to 3.3.7 which fixes a compilation issue with recent XCode versions. - Eigen library: The source code of Eigen is no longer included but downloaded from an external repository instead. Incremented Eigen version to 3.3.7 which fixes a compilation issue with recent XCode versions.
- Tests: Enabled tests for permissive schedulers - Tests: Enabled tests for permissive schedulers
- `storm-counterexamples`: fix when computing multiple counterexamples in debug mode - `storm-counterexamples`: fix when computing multiple counterexamples in debug mode

4
CMakeLists.txt

@ -66,7 +66,9 @@ set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optiona
set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).") set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).")
set(CUDA_ROOT "" CACHE STRING "The hint to the root directory of CUDA (optional).") set(CUDA_ROOT "" CACHE STRING "The hint to the root directory of CUDA (optional).")
set(MSAT_ROOT "" CACHE STRING "The hint to the root directory of MathSAT (optional).") set(MSAT_ROOT "" CACHE STRING "The hint to the root directory of MathSAT (optional).")
set(STORM_QVBS_ROOT "" CACHE STRING "The hint to the root directory of the Quantitative Verification Benchmark Set (QVBS) (optional).")
option(STORM_LOAD_QVBS "Sets whether the Quantitative Verification Benchmark Set (QVBS) should be downloaded." OFF)
set(STORM_QVBS_ROOT "" CACHE STRING "The root directory of the Quantitative Verification Benchmark Set (QVBS) in case it should not be downloaded (optional).")
MARK_AS_ADVANCED(STORM_QVBS_ROOT)
set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.") set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.")
set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the link directories.") set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the link directories.")
set(USE_XERCESC ${XML_SUPPORT}) set(USE_XERCESC ${XML_SUPPORT})

22
resources/3rdparty/CMakeLists.txt

@ -450,14 +450,32 @@ endif(ENABLE_MSAT)
############################################################# #############################################################
set(STORM_HAVE_QVBS OFF) set(STORM_HAVE_QVBS OFF)
if (NOT "${STORM_QVBS_ROOT}" STREQUAL "")
if (STORM_LOAD_QVBS)
ExternalProject_Add(
download_qvbs
GIT_REPOSITORY https://github.com/ahartmanns/qcomp.git
GIT_SHALLOW 1
PREFIX ${PROJECT_BINARY_DIR}/qvbs
UPDATE_COMMAND ""
CONFIGURE_COMMAND ""
BUILD_COMMAND ""
INSTALL_COMMAND ""
LOG_INSTALL ON
)
add_dependencies(resources download_qvbs)
set(STORM_HAVE_QVBS ON)
ExternalProject_Get_Property(download_qvbs source_dir)
set(STORM_QVBS_ROOT "${source_dir}/benchmarks")
elseif (NOT "${STORM_QVBS_ROOT}" STREQUAL "")
if( EXISTS "${STORM_QVBS_ROOT}/index.json") if( EXISTS "${STORM_QVBS_ROOT}/index.json")
set(STORM_HAVE_QVBS ON) set(STORM_HAVE_QVBS ON)
message (STATUS "Storm - Enabled inputs from QVBS located at ${STORM_QVBS_ROOT}")
else() else()
message(FATAL_ERROR "No file 'index.json' in provided QVBS root directory ${STORM_QVBS_ROOT}") message(FATAL_ERROR "No file 'index.json' in provided QVBS root directory ${STORM_QVBS_ROOT}")
endif() endif()
endif() endif()
if (STORM_HAVE_QVBS)
message (STATUS "Storm - Enabled inputs from QVBS located at ${STORM_QVBS_ROOT}")
endif()
############################################################# #############################################################

Loading…
Cancel
Save