diff --git a/.gitignore b/.gitignore index e8b271715..43fe390a0 100644 --- a/.gitignore +++ b/.gitignore @@ -52,3 +52,7 @@ nbproject/ *.out resources/3rdparty/cudd-3.0.0/Makefile.in resources/3rdparty/cudd-3.0.0/aclocal.m4 +# Python config +stormpy/setup.cfg +# Travis helpers +travis/mtime_cache/cache.json diff --git a/.travis.yml b/.travis.yml new file mode 100644 index 000000000..c824cddf6 --- /dev/null +++ b/.travis.yml @@ -0,0 +1,296 @@ +# This file was inspired from https://github.com/google/fruit + +# +# General config +# +branches: + only: + - master + - stable +dist: trusty +language: cpp + +# Enable caching +cache: + timeout: 1000 + directories: + - build + - travis/mtime_cache + +# Enable docker support +services: +- docker +sudo: required + +notifications: + email: + on_failure: always + on_success: change + recipients: + secure: "Q9CW/PtyWkZwExDrfFFb9n1STGYsRfI6awv1bZHcGwfrDvhpXoMCuF8CwviIfilm7fFJJEoKizTtdRpY0HrOnY/8KY111xrtcFYosxdndv7xbESodIxQOUoIEFCO0mCNHwWYisoi3dAA7H3Yn661EsxluwHjzX5vY0xSbw0n229hlsFz092HwGLSU33zHl7eXpQk+BOFmBTRGlOq9obtDZ17zbHz1oXFZntHK/JDUIYP0b0uq8NvE2jM6CIVdcuSwmIkOhZJoO2L3Py3rBbPci+L2PSK4Smv2UjCPF8KusnOaFIyDB3LcNM9Jqq5ssJMrK/KaO6BiuYrOZXYWZ7KEg3Y/naC8HjOH1dzty+P7oW46sb9F03pTsufqD4R7wcK+9wROTztO6aJPDG/IPH7EWgrBTxqlOkVRwi2eYuQouZpZUW6EMClKbMHMIxCH2S8aOk/r1w2cNwmPEcunnP0nl413x/ByHr4fTPFykPj8pQxIsllYjpdWBRQfDOauKWGzk6LcrFW0qpWP+/aJ2vYu/IoZQMG5lMHbp6Y1Lg09pYm7Q983v3b7D+JvXhOXMyGq91HyPahA2wwKoG1GA4uoZ2I95/IFYNiKkelDd3WTBoFLNF9YFoEJNdCywm1fO2WY4WkyEFBuQcgDA+YpFMJJMxjTbivYk9jvHk2gji//2w=" + +# +# Configurations +# +jobs: + include: + + ### + # Stage: Build (1st run) + ### + + # osx + - stage: Build (1st run) + os: osx + compiler: clang + env: CONFIG=DefaultDebug COMPILER=clang-4.0 STL=libc++ + install: + - rm -rf build + - travis/install_osx.sh + script: + - travis/build.sh Build1 + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + - stage: Build (1st run) + os: osx + compiler: clang + env: CONFIG=DefaultRelease COMPILER=clang-4.0 STL=libc++ + install: + - rm -rf build + - travis/install_osx.sh + script: + - travis/build.sh Build1 + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + # ubuntu-16.10 + - stage: Build (1st run) + os: linux + compiler: gcc + env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc-6 + install: + - rm -rf build + - travis/install_linux.sh + script: + - travis/build.sh Build1 + before_cache: + - docker cp storm:/storm/. . + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + - stage: Build (1st run) + os: linux + compiler: gcc + env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc-6 + install: + - rm -rf build + - travis/install_linux.sh + script: + - travis/build.sh Build1 + before_cache: + - docker cp storm:/storm/. . + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + + ### + # Stage: Build (2nd run) + ### + + # osx + - stage: Build (2nd run) + os: osx + compiler: clang + env: CONFIG=DefaultDebug COMPILER=clang-4.0 STL=libc++ + install: + - travis/install_osx.sh + script: + - travis/build.sh Build2 + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + - stage: Build (2nd run) + os: osx + compiler: clang + env: CONFIG=DefaultRelease COMPILER=clang-4.0 STL=libc++ + install: + - travis/install_osx.sh + script: + - travis/build.sh Build2 + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + # ubuntu-16.10 + - stage: Build (2nd run) + os: linux + compiler: gcc + env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc-6 + install: + - travis/install_linux.sh + script: + - travis/build.sh Build2 + before_cache: + - docker cp storm:/storm/. . + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + - stage: Build (2nd run) + os: linux + compiler: gcc + env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc-6 + install: + - travis/install_linux.sh + script: + - travis/build.sh Build2 + before_cache: + - docker cp storm:/storm/. . + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + + ### + # Stage: Build (3rd run) + ### + + # osx + - stage: Build (3rd run) + os: osx + compiler: clang + env: CONFIG=DefaultDebug COMPILER=clang-4.0 STL=libc++ + install: + - travis/install_osx.sh + script: + - travis/build.sh Build3 + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + - stage: Build (3rd run) + os: osx + compiler: clang + env: CONFIG=DefaultRelease COMPILER=clang-4.0 STL=libc++ + install: + - travis/install_osx.sh + script: + - travis/build.sh Build3 + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + # ubuntu-16.10 + - stage: Build (3rd run) + os: linux + compiler: gcc + env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc-6 + install: + - travis/install_linux.sh + script: + - travis/build.sh Build3 + before_cache: + - docker cp storm:/storm/. . + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + - stage: Build (3rd run) + os: linux + compiler: gcc + env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc-6 + install: + - travis/install_linux.sh + script: + - travis/build.sh Build3 + before_cache: + - docker cp storm:/storm/. . + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + + ### + # Stage: Build (4th run) + ### + + # osx + - stage: Build (4th run) + os: osx + compiler: clang + env: CONFIG=DefaultDebug COMPILER=clang-4.0 STL=libc++ + install: + - travis/install_osx.sh + script: + - travis/build.sh Build4 + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + - stage: Build (4th run) + os: osx + compiler: clang + env: CONFIG=DefaultRelease COMPILER=clang-4.0 STL=libc++ + install: + - travis/install_osx.sh + script: + - travis/build.sh Build4 + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + # ubuntu-16.10 + - stage: Build (4th run) + os: linux + compiler: gcc + env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc-6 + install: + - travis/install_linux.sh + script: + - travis/build.sh Build4 + before_cache: + - docker cp storm:/storm/. . + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + - stage: Build (4th run) + os: linux + compiler: gcc + env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc-6 + install: + - travis/install_linux.sh + script: + - travis/build.sh Build4 + before_cache: + - docker cp storm:/storm/. . + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + + ### + # Stage: Test all + ### + + # osx + - stage: Test all + os: osx + compiler: clang + env: CONFIG=DefaultDebug COMPILER=clang-4.0 STL=libc++ + install: + - travis/install_osx.sh + script: + - travis/build.sh TestAll + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + - stage: Test all + os: osx + compiler: clang + env: CONFIG=DefaultRelease COMPILER=clang-4.0 STL=libc++ + install: + - travis/install_osx.sh + script: + - travis/build.sh TestAll + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + # ubuntu-16.10 + - stage: Test all + os: linux + compiler: gcc + env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc-6 + install: + - travis/install_linux.sh + script: + - travis/build.sh TestAll + before_cache: + - docker cp storm:/storm/. . + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + - stage: Test all + os: linux + compiler: gcc + env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc-6 + install: + - travis/install_linux.sh + script: + - travis/build.sh TestAll + before_cache: + - docker cp storm:/storm/. . + after_failure: + - find build -iname '*err*.log' -type f -print -exec cat {} \; + diff --git a/CHANGELOG.md b/CHANGELOG.md index 90c72cd28..7c55d776d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,7 +6,6 @@ The releases of major and minor versions contain an overview of changes since th Version 1.1.x ------------- -Long run average computation via LRA, LP based MDP model checking, parametric model checking has an own binary ### Version 1.1.0 (2017/8) diff --git a/README.md b/README.md index ffcc3bc5c..a415b376e 100644 --- a/README.md +++ b/README.md @@ -1,23 +1,23 @@ -Storm -============================== +Storm - A Modern Probabilistic Model Checker +============================================ +[![Build Status](https://travis-ci.org/moves-rwth/storm.svg?branch=master)](https://travis-ci.org/moves-rwth/storm) -For more instructions, check out the documentation found in [Getting Started](https://moves-rwth.github.io/storm/getting-started.html) +For more instructions, check out the documentation found in [Getting Started](http://www.stormchecker.org/getting-started.html). Benchmarks ---------------------------- -Example input files for storm can be obtained from -https://github.com/moves-rwth/storm-examples. -Running make example-files automatically obtains these files. +Example input files for Storm can be obtained from +https://github.com/moves-rwth/storm-examples. -Further examples and benchmarks found in the following repositories: +Further examples and benchmarks can be found in the following repositories: * **Prism files** (DTMC, MDP, CTMC): -http://www.prismmodelchecker.org/benchmarks/ +http://www.prismmodelchecker.org/benchmarks * **Jani files** (DTMC, MDP, CTMC, MA): -http://jani-spec.org/ -* **GSPN**s: +http://jani-spec.org +* **GSPN**s: (private, contact: sebastian.junges@cs.rwth-aachen.de) * **DFT**s: https://github.com/moves-rwth/dft-examples @@ -31,8 +31,8 @@ Storm has been developed at RWTH Aachen University. ###### Principal developers * Christian Dehnert -* Joost-Pieter Katoen * Sebastian Junges +* Joost-Pieter Katoen * Matthias Volk ###### Developers (lexicographical order) @@ -40,7 +40,7 @@ Storm has been developed at RWTH Aachen University. * David Korzeniewski * Tim Quatmann -###### Contributors (lexicographical order) +###### Contributors (lexicographical order) * Dimitri Bohlender * Harold Bruintjes * Michael Deutschen diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index b8b9ba12a..243c0b0e5 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -200,7 +200,7 @@ include(${STORM_3RDPARTY_SOURCE_DIR}/include_cudd.cmake) set(STORM_HAVE_CARL OFF) set(CARL_MINYEAR 17) -set(CARL_MINMONTH 06) +set(CARL_MINMONTH 08) set(CARL_MINPATCH 0) if(USE_CARL) if (NOT STORM_FORCE_SHIPPED_CARL) diff --git a/resources/3rdparty/carl/CMakeLists.txt b/resources/3rdparty/carl/CMakeLists.txt index d0e046861..b41ed3785 100644 --- a/resources/3rdparty/carl/CMakeLists.txt +++ b/resources/3rdparty/carl/CMakeLists.txt @@ -8,11 +8,11 @@ message(STORM_3RDPARTY_BINARY_DIR: ${STORM_3RDPARTY_BINARY_DIR}) ExternalProject_Add(carl-config GIT_REPOSITORY https://github.com/smtrat/carl - GIT_TAG master + GIT_TAG 17.08 PREFIX here SOURCE_DIR source_dir BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/carl - CMAKE_ARGS -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DBOOST_INCLUDEDIR=${Boost_INCLUDE_DIRS} -DBOOST_LIBRARYDIR=${Boost_LIBRARY_DIRS} -DBoost_NO_SYSTEM_PATHS=ON -DEXPORT_TO_CMAKE=OFF -DTHREAD_SAFE=ON -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON -DCMAKE_SKIP_INSTALL_ALL_DEPENDENCY=ON -DCMAKE_INSTALL_PREFIX:PATH=${STORM_3RDPARTY_BINARY_DIR}/carl + CMAKE_ARGS -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DBOOST_INCLUDEDIR=${Boost_INCLUDE_DIRS} -DBOOST_LIBRARYDIR=${Boost_LIBRARY_DIRS} -DBoost_NO_SYSTEM_PATHS=ON -DEXPORT_TO_CMAKE=ON -DTHREAD_SAFE=ON -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON -DCMAKE_SKIP_INSTALL_ALL_DEPENDENCY=ON -DCMAKE_INSTALL_PREFIX:PATH=${STORM_3RDPARTY_BINARY_DIR}/carl BUILD_IN_SOURCE 0 LOG_UPDATE OFF LOG_CONFIGURE OFF diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 38b884cf7..acf819119 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -5,6 +5,7 @@ set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin) add_custom_target(binaries) add_subdirectory(storm) +add_subdirectory(storm-cli-utilities) add_subdirectory(storm-pgcl) add_subdirectory(storm-pgcl-cli) add_subdirectory(storm-gspn) diff --git a/src/storm-cli-utilities/CMakeLists.txt b/src/storm-cli-utilities/CMakeLists.txt new file mode 100644 index 000000000..64c2848c7 --- /dev/null +++ b/src/storm-cli-utilities/CMakeLists.txt @@ -0,0 +1,40 @@ +file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-cli-utilities/*.h ${PROJECT_SOURCE_DIR}/src/storm-cli-utilities/*.cpp) + +register_source_groups_from_filestructure("${ALL_FILES}" storm-cli-utilities) + + + +file(GLOB_RECURSE STORM_CLI_UTIL_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-cli-utilities/*.cpp) +file(GLOB_RECURSE STORM_CLI_UTIL_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-cli-utilities/*.h) + + +# Create storm-pars. +add_library(storm-cli-utilities SHARED ${STORM_CLI_UTIL_SOURCES} ${STORM_CLI_UTIL_HEADERS}) + +# Remove define symbol for shared libstorm. +set_target_properties(storm-cli-utilities PROPERTIES DEFINE_SYMBOL "") +#add_dependencies(storm resources) +list(APPEND STORM_TARGETS storm-cli-utilities) +set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) + +target_link_libraries(storm-cli-utilities PUBLIC storm) + +# Install storm headers to include directory. +foreach(HEADER ${STORM_CLI_UTIL_HEADERS}) + string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) + string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) + string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) + add_custom_command( + OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} + COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY} + COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} + DEPENDS ${HEADER} + ) + list(APPEND STORM_CLI_UTIL_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}") +endforeach() +add_custom_target(copy_storm_cli_util_headers DEPENDS ${STORM_CLI_UTIL_OUTPUT_HEADERS} ${STORM_CLI_UTIL_HEADERS}) +add_dependencies(storm-cli-utilities copy_storm_pars_headers) + +# installation +install(TARGETS storm-cli-utilities RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) + diff --git a/src/storm/cli/cli.cpp b/src/storm-cli-utilities/cli.cpp similarity index 98% rename from src/storm/cli/cli.cpp rename to src/storm-cli-utilities/cli.cpp index 343006c6d..66d83ece7 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm-cli-utilities/cli.cpp @@ -1,37 +1,37 @@ -#include "storm/cli/cli.h" +#include "cli.h" #include "storm/storage/SymbolicModelDescription.h" #include "storm/models/ModelBase.h" -#include "storm/settings/modules/DebugSettings.h" -#include "storm/settings/modules/IOSettings.h" -#include "storm/settings/modules/CoreSettings.h" #include "storm/exceptions/OptionParserException.h" -#include "storm/settings/modules/ResourceSettings.h" -#include "storm/settings/modules/JaniExportSettings.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/symbolic/StandardRewardModel.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/ResourceSettings.h" +#include "storm/settings/modules/JitBuilderSettings.h" +#include "storm/settings/modules/DebugSettings.h" +#include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/ResourceSettings.h" +#include "storm/settings/modules/JaniExportSettings.h" + #include "storm/utility/resources.h" #include "storm/utility/file.h" #include "storm/utility/storm-version.h" -#include "storm/utility/cli.h" +#include "storm/utility/macros.h" #include "storm/utility/initialize.h" #include "storm/utility/Stopwatch.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/ResourceSettings.h" - #include #include "storm/api/storm.h" -#include "storm/utility/macros.h" // Includes for the linked libraries and versions header. #ifdef STORM_HAVE_INTELTBB @@ -65,12 +65,12 @@ namespace storm { storm::utility::setUp(); storm::cli::printHeader("Storm", argc, argv); storm::settings::initializeAll("Storm", "storm"); - + storm::utility::Stopwatch totalTimer(true); if (!storm::cli::parseOptions(argc, argv)) { return -1; } - + processOptions(); totalTimer.stop(); @@ -370,7 +370,15 @@ namespace storm { template std::shared_ptr buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { auto counterexampleGeneratorSettings = storm::settings::getModule(); - return storm::api::buildSparseModel(input.model.get(), createFormulasToRespect(input.properties), ioSettings.isBuildChoiceLabelsSet(), counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet()); + storm::builder::BuilderOptions options(createFormulasToRespect(input.properties)); + options.setBuildChoiceLabels(ioSettings.isBuildChoiceLabelsSet()); + options.setBuildChoiceOrigins(counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet()); + options.setBuildAllLabels(ioSettings.isBuildFullModelSet()); + options.setBuildAllRewardModels(ioSettings.isBuildFullModelSet()); + if (ioSettings.isBuildFullModelSet()) { + options.clearTerminalStates(); + } + return storm::api::buildSparseModel(input.model.get(), options, ioSettings.isJitSet(), storm::settings::getModule().isDoctorSet()); } template diff --git a/src/storm/cli/cli.h b/src/storm-cli-utilities/cli.h similarity index 100% rename from src/storm/cli/cli.h rename to src/storm-cli-utilities/cli.h diff --git a/src/storm-dft-cli/CMakeLists.txt b/src/storm-dft-cli/CMakeLists.txt index 0d104405e..b8cdbbd27 100644 --- a/src/storm-dft-cli/CMakeLists.txt +++ b/src/storm-dft-cli/CMakeLists.txt @@ -1,6 +1,6 @@ # Create storm-dft. add_executable(storm-dft-cli ${PROJECT_SOURCE_DIR}/src/storm-dft-cli/storm-dyftee.cpp) -target_link_libraries(storm-dft-cli storm-dft) # Adding headers for xcode +target_link_libraries(storm-dft-cli storm-dft storm-cli-utilities) # Adding headers for xcode set_target_properties(storm-dft-cli PROPERTIES OUTPUT_NAME "storm-dft") add_dependencies(binaries storm-dft-cli) diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index b2dc40006..8eef6f0b5 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -1,12 +1,12 @@ #include "storm/logic/Formula.h" #include "storm/utility/initialize.h" #include "storm/api/storm.h" -#include "storm/cli/cli.h" +#include "storm-cli-utilities/cli.h" #include "storm/exceptions/BaseException.h" #include "storm/logic/Formula.h" -#include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/GmmxxEquationSolverSettings.h" diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 8721efd7c..d6b7e9138 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -1,5 +1,6 @@ #include "DFTModelChecker.h" +#include "storm/settings/modules/IOSettings.h" #include "storm/builder/ParallelCompositionBuilder.h" #include "storm/utility/bitoperations.h" #include "storm/utility/DirectEncodingExporter.h" @@ -357,6 +358,7 @@ namespace storm { explorationTimer.stop(); // Export the model if required + // TODO move this outside of the model checker? if (storm::settings::getModule().isExportExplicitSet()) { std::ofstream stream; storm::utility::openFile(storm::settings::getModule().getExportExplicitFilename(), stream); diff --git a/src/storm-dft/storage/dft/OrderDFTElementsById.cpp b/src/storm-dft/storage/dft/OrderDFTElementsById.cpp index 8812eb763..72e571ab1 100644 --- a/src/storm-dft/storage/dft/OrderDFTElementsById.cpp +++ b/src/storm-dft/storage/dft/OrderDFTElementsById.cpp @@ -22,12 +22,12 @@ namespace storm { // Explicitly instantiate the class. - template class OrderElementsById; - template class OrderElementsByRank; + template struct OrderElementsById; + template struct OrderElementsByRank; #ifdef STORM_HAVE_CARL - template class OrderElementsById; - template class OrderElementsByRank; + template struct OrderElementsById; + template struct OrderElementsByRank; #endif } } diff --git a/src/storm-gspn-cli/CMakeLists.txt b/src/storm-gspn-cli/CMakeLists.txt index 72e51a6da..39d656a4c 100644 --- a/src/storm-gspn-cli/CMakeLists.txt +++ b/src/storm-gspn-cli/CMakeLists.txt @@ -1,5 +1,5 @@ add_executable(storm-gspn-cli ${PROJECT_SOURCE_DIR}/src/storm-gspn-cli/storm-gspn.cpp) -target_link_libraries(storm-gspn-cli storm-gspn) # Adding headers for xcode +target_link_libraries(storm-gspn-cli storm-gspn storm-cli-utilities) # Adding headers for xcode set_target_properties(storm-gspn-cli PROPERTIES OUTPUT_NAME "storm-gspn") add_dependencies(binaries storm-gspn-cli) diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp index 9a77a56be..fc493391a 100644 --- a/src/storm-gspn-cli/storm-gspn.cpp +++ b/src/storm-gspn-cli/storm-gspn.cpp @@ -12,7 +12,7 @@ #include "storm/utility/initialize.h" #include "api/storm.h" -#include "storm/cli/cli.h" +#include "storm-cli-utilities/cli.h" #include "storm/parser/FormulaParser.h" @@ -27,7 +27,7 @@ #include "storm/exceptions/FileIoException.h" -#include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/GSPNSettings.h" #include "storm/settings/modules/GSPNExportSettings.h" #include "storm/settings/modules/CoreSettings.h" diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 0836f1e0d..1ff2fabb6 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -6,7 +6,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/api/storm.h" -#include "storm/cli/cli.h" +#include "storm-cli-utilities/cli.h" #include "storm/models/ModelBase.h" #include "storm/storage/SymbolicModelDescription.h" #include "storm/utility/file.h" @@ -23,13 +23,13 @@ #include "storm/exceptions/InvalidSettingsException.h" #include "storm/exceptions/NotSupportedException.h" -#include "storm/cli/cli.cpp" +#include "storm-cli-utilities/cli.cpp" namespace storm { namespace pars { typedef typename storm::cli::SymbolicInput SymbolicInput; - + template std::shared_ptr buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { return storm::api::buildSparseModel(input.model.get(), storm::api::extractFormulasFromProperties(input.properties), ioSettings.isBuildChoiceLabelsSet()); @@ -50,7 +50,7 @@ namespace storm { STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input."); result = storm::cli::buildModelExplicit(ioSettings); } - + modelBuildingWatch.stop(); if (result) { STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl); @@ -335,27 +335,7 @@ namespace storm { processInputWithValueTypeAndDdlib(symbolicInput); } - - int64_t process(const int argc, const char** argv) { - storm::utility::setUp(); - storm::cli::printHeader("Storm-pars", argc, argv); - storm::settings::initializeParsSettings("Storm-pars", "storm-pars"); - - storm::utility::Stopwatch totalTimer(true); - if (!storm::cli::parseOptions(argc, argv)) { - return -1; - } - - processOptions(); - - totalTimer.stop(); - if (storm::settings::getModule().isPrintTimeAndMemorySet()) { - storm::cli::printTimeAndMemoryStatistics(totalTimer.getTimeInMilliseconds()); - } - - storm::utility::cleanUp(); - return 0; - } + } } @@ -366,7 +346,24 @@ namespace storm { int main(const int argc, const char** argv) { try { - return storm::pars::process(argc, argv); + storm::utility::setUp(); + storm::cli::printHeader("Storm-pars", argc, argv); + storm::settings::initializeParsSettings("Storm-pars", "storm-pars"); + + storm::utility::Stopwatch totalTimer(true); + if (!storm::cli::parseOptions(argc, argv)) { + return -1; + } + + storm::pars::processOptions(); + + totalTimer.stop(); + if (storm::settings::getModule().isPrintTimeAndMemorySet()) { + storm::cli::printTimeAndMemoryStatistics(totalTimer.getTimeInMilliseconds()); + } + + storm::utility::cleanUp(); + return 0; } catch (storm::exceptions::BaseException const& exception) { STORM_LOG_ERROR("An exception caused Storm-pars to terminate. The message of the exception is: " << exception.what()); return 1; diff --git a/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp b/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp index 1679bdcca..9385a24a9 100644 --- a/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp +++ b/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp @@ -45,7 +45,7 @@ namespace storm { } } // reaching this point means that the provided formula is not supported. Thus, no simplification is possible. - STORM_LOG_DEBUG("Simplification not possible because the formula is not suppoerted. Formula: " << formula); + STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); return false; } @@ -63,8 +63,8 @@ namespace storm { template bool SparseParametricModelSimplifier::simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { - // If this method was not overriden by any subclass, simplification is not possible - STORM_LOG_DEBUG("Simplification not possible because the formula is not suppoerted. Formula: " << formula); + // If this method was not overridden by any subclass, simplification is not possible + STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); return false; } @@ -77,21 +77,21 @@ namespace storm { template bool SparseParametricModelSimplifier::simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { - // If this method was not overriden by any subclass, simplification is not possible + // If this method was not overridden by any subclass, simplification is not possible STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); return false; } template bool SparseParametricModelSimplifier::simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula) { - // If this method was not overriden by any subclass, simplification is not possible + // If this method was not overridden by any subclass, simplification is not possible STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); return false; } template bool SparseParametricModelSimplifier::simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula) { - // If this method was not overriden by any subclass, simplification is not possible + // If this method was not overridden by any subclass, simplification is not possible STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); return false; } @@ -100,7 +100,6 @@ namespace storm { std::shared_ptr SparseParametricModelSimplifier::eliminateConstantDeterministicStates(SparseModelType const& model, storm::storage::BitVector const& consideredStates, boost::optional const& rewardModelName) { storm::storage::SparseMatrix const& sparseMatrix = model.getTransitionMatrix(); - // get the action-based reward values std::vector actionRewards; if(rewardModelName) { diff --git a/src/storm-pgcl-cli/CMakeLists.txt b/src/storm-pgcl-cli/CMakeLists.txt index 0f051a1b4..4778d1e93 100644 --- a/src/storm-pgcl-cli/CMakeLists.txt +++ b/src/storm-pgcl-cli/CMakeLists.txt @@ -1,5 +1,5 @@ add_executable(storm-pgcl-cli ${PROJECT_SOURCE_DIR}/src/storm-pgcl-cli/storm-pgcl.cpp) -target_link_libraries(storm-pgcl-cli storm-pgcl) +target_link_libraries(storm-pgcl-cli storm-pgcl storm-cli-utilities) set_target_properties(storm-pgcl-cli PROPERTIES OUTPUT_NAME "storm-pgcl") # installation diff --git a/src/storm-pgcl-cli/storm-pgcl.cpp b/src/storm-pgcl-cli/storm-pgcl.cpp index 423afb087..ce579938f 100644 --- a/src/storm-pgcl-cli/storm-pgcl.cpp +++ b/src/storm-pgcl-cli/storm-pgcl.cpp @@ -2,7 +2,7 @@ #include "logic/Formula.h" #include "utility/initialize.h" -#include "storm/cli/cli.h" +#include "storm-cli-utilities/cli.h" #include "storm/exceptions/BaseException.h" #include "storm/utility/macros.h" #include diff --git a/src/storm/CMakeLists.txt b/src/storm/CMakeLists.txt index 193a6d4bb..0ed4b0d1c 100644 --- a/src/storm/CMakeLists.txt +++ b/src/storm/CMakeLists.txt @@ -49,7 +49,7 @@ set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) # Create storm. add_executable(storm-main ${STORM_MAIN_SOURCES} ${STORM_MAIN_HEADERS}) -target_link_libraries(storm-main PUBLIC storm) +target_link_libraries(storm-main PUBLIC storm storm-cli-utilities) set_target_properties(storm-main PROPERTIES OUTPUT_NAME "storm") # Install storm headers to include directory. diff --git a/src/storm/adapters/Smt2ExpressionAdapter.h b/src/storm/adapters/Smt2ExpressionAdapter.h index c61566177..f1b96b71e 100644 --- a/src/storm/adapters/Smt2ExpressionAdapter.h +++ b/src/storm/adapters/Smt2ExpressionAdapter.h @@ -38,8 +38,7 @@ namespace storm { std::string translateExpression(storm::expressions::Expression const& ) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); } - -#ifdef STORM_HAVE_CARL + /*! * Translates the given constraint "leftHandSide relation rightHandSide" to an equivalent expression for Smt2. @@ -60,6 +59,7 @@ namespace storm { ") " + ")"; } + /*! * Translates the given constraint "leftHandSide relation 0" to an equivalent expression for Smt2. @@ -67,31 +67,16 @@ namespace storm { * @param constraint * @return An equivalent expression for Smt2. */ - std::string translateExpression(storm::ArithConstraint const& constraint) { - std::stringstream ss; - ss << "(" << constraint.rel() << " " << - constraint.lhs().toString(false, useReadableVarNames) << " " << - "0 " << - ")"; - return ss.str(); - } - - /*! - * Translates the given constraint "leftHandSide relation 0" to an equivalent expression for Smt2. - - * @param constraint - * @return An equivalent expression for Smt2. - */ - std::string translateExpression(storm::ArithConstraint const& constraint) { + std::string translateExpression(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation) { std::stringstream ss; - ss << "(" << constraint.rel() << " " << - constraint.lhs().toString(false, useReadableVarNames) << " " << + ss << "(" << relation << " " << + leftHandSide.toString(false, useReadableVarNames) << " " << "0 " << ")"; return ss.str(); } -#endif + /*! * Translates the given variable to an equivalent expression for Smt2. * @@ -126,7 +111,7 @@ namespace storm { } -#ifdef STORM_HAVE_CARL + /*! Checks whether the variables in the given set are already declared and creates them if necessary * @param variables the set of variables to check */ @@ -167,7 +152,6 @@ namespace storm { } return result; } -#endif private: // The manager that can be used to build expressions. diff --git a/src/storm/analysis/GraphConditions.h b/src/storm/analysis/GraphConditions.h index 48b4aee64..394f11b31 100644 --- a/src/storm/analysis/GraphConditions.h +++ b/src/storm/analysis/GraphConditions.h @@ -8,12 +8,12 @@ namespace storm { namespace analysis { - + template struct ConstraintType { - typedef storm::ArithConstraint val; + typedef void* val; }; - + template struct ConstraintType::value>::type> { typedef carl::Formula val; diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index 868c47bba..ca21f99fc 100644 --- a/src/storm/api/builder.h +++ b/src/storm/api/builder.h @@ -23,10 +23,6 @@ #include "storm/builder/ExplicitModelBuilder.h" #include "storm/builder/jit/ExplicitJitJaniModelBuilder.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/IOSettings.h" -#include "storm/settings/modules/JitBuilderSettings.h" - #include "storm/utility/macros.h" #include "storm/exceptions/NotSupportedException.h" @@ -62,29 +58,18 @@ namespace storm { } template - std::shared_ptr> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool buildChoiceLabels = false, bool buildChoiceOrigins = false, bool buildStateValuations = false) { - storm::builder::BuilderOptions options(formulas); - - if (storm::settings::getModule().isBuildFullModelSet()) { - options.setBuildAllLabels(); - options.setBuildAllRewardModels(); - options.clearTerminalStates(); - } - options.setBuildChoiceLabels(buildChoiceLabels); - options.setBuildChoiceOrigins(buildChoiceOrigins); - options.setBuildStateValuations(buildStateValuations); - - if (storm::settings::getModule().isJitSet()) { + std::shared_ptr> buildSparseModel(storm::storage::SymbolicModelDescription const& model, storm::builder::BuilderOptions const& options, bool jit = false, bool doctor = false) { + if (jit) { STORM_LOG_THROW(model.isJaniModel(), storm::exceptions::NotSupportedException, "Cannot use JIT-based model builder for non-JANI model."); - + storm::builder::jit::ExplicitJitJaniModelBuilder builder(model.asJaniModel(), options); - - if (storm::settings::getModule().isDoctorSet()) { + + if (doctor) { bool result = builder.doctor(); STORM_LOG_THROW(result, storm::exceptions::NotSupportedException, "The JIT-based model builder cannot be used on your system."); STORM_LOG_INFO("The JIT-based model builder seems to be working."); } - + return builder.build(); } else { std::shared_ptr> generator; @@ -99,6 +84,14 @@ namespace storm { return builder.build(); } } + + template + std::shared_ptr> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool jit = false, bool doctor = false) { + storm::builder::BuilderOptions options(formulas); + return buildSparseModel(model, options, jit, doctor); + + + } template> std::shared_ptr> buildSparseModel(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents&& components) { diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp index 6e42745fd..b0d2641bd 100644 --- a/src/storm/builder/BuilderOptions.cpp +++ b/src/storm/builder/BuilderOptions.cpp @@ -157,8 +157,8 @@ namespace storm { return buildAllLabels; } - BuilderOptions& BuilderOptions::setBuildAllRewardModels() { - buildAllRewardModels = true; + BuilderOptions& BuilderOptions::setBuildAllRewardModels(bool newValue) { + buildAllRewardModels = newValue; return *this; } @@ -185,8 +185,8 @@ namespace storm { return *this; } - BuilderOptions& BuilderOptions::setBuildAllLabels() { - buildAllLabels = true; + BuilderOptions& BuilderOptions::setBuildAllLabels(bool newValue) { + buildAllLabels = newValue; return *this; } diff --git a/src/storm/builder/BuilderOptions.h b/src/storm/builder/BuilderOptions.h index a06de50eb..f3a6edfbf 100644 --- a/src/storm/builder/BuilderOptions.h +++ b/src/storm/builder/BuilderOptions.h @@ -81,9 +81,21 @@ namespace storm { * model. */ void setTerminalStatesFromFormula(storm::logic::Formula const& formula); - + + /*! + * Which reward models are built + * @return + */ std::vector const& getRewardModelNames() const; + /*! + * Which labels are built + * @return + */ std::set const& getLabelNames() const; + /*! + * Which expression labels are built + * @return + */ std::vector const& getExpressionLabels() const; std::vector> const& getTerminalStates() const; bool hasTerminalStates() const; @@ -96,18 +108,53 @@ namespace storm { bool isExplorationChecksSet() const; bool isExplorationShowProgressSet() const; uint64_t getExplorationShowProgressDelay() const; - - BuilderOptions& setBuildAllRewardModels(); + + /** + * Should all reward models be built? If not set, only required reward models are build. + * @param newValue The new value (default true) + * @return this + */ + BuilderOptions& setBuildAllRewardModels(bool newValue = true); + /** + * Add an additional reward model to build + * @param newValue The name of the extra reward model + * @return this + */ BuilderOptions& addRewardModel(std::string const& rewardModelName); - BuilderOptions& setBuildAllLabels(); + /** + * Should all reward models be built? If not set, only required reward models are build. + * @param newValue The new value (default true) + * @return this + */ + BuilderOptions& setBuildAllLabels(bool newValue = true); BuilderOptions& addLabel(storm::expressions::Expression const& expression); BuilderOptions& addLabel(std::string const& labelName); BuilderOptions& addTerminalExpression(storm::expressions::Expression const& expression, bool value); BuilderOptions& addTerminalLabel(std::string const& label, bool value); - BuilderOptions& setBuildChoiceLabels(bool newValue); - BuilderOptions& setBuildStateValuations(bool newValue); - BuilderOptions& setBuildChoiceOrigins(bool newValue); - BuilderOptions& setExplorationChecks(bool newValue); + /** + * Should the choice labels be built? + * @param newValue The new value (default true) + * @return this + */ + BuilderOptions& setBuildChoiceLabels(bool newValue = true); + /** + * Should the state valuation mapping be built? + * @param newValue The new value (default true) + * @return this + */ + BuilderOptions& setBuildStateValuations(bool newValue = true); + /** + * Should the origins the different choices be built? + * @param newValue The new value (default true) + * @return this + */ + BuilderOptions& setBuildChoiceOrigins(bool newValue = true); + /** + * Should extra checks be performed during exploration + * @param newValue The new value (default true) + * @return this + */ + BuilderOptions& setExplorationChecks(bool newValue = true); private: /// A flag that indicates whether all reward models are to be built. In this case, the reward model names are diff --git a/src/storm/solver/SmtlibSmtSolver.cpp b/src/storm/solver/SmtlibSmtSolver.cpp index 8dcd37ddc..69394ec8a 100644 --- a/src/storm/solver/SmtlibSmtSolver.cpp +++ b/src/storm/solver/SmtlibSmtSolver.cpp @@ -102,33 +102,6 @@ namespace storm { writeCommand("( assert " + expressionAdapter->translateExpression(leftHandSide, relation, rightHandSide) + " )", true); } - void SmtlibSmtSolver::add(storm::ArithConstraint const& constraint) { - add(constraint.lhs(), constraint.rel()); - } - - void SmtlibSmtSolver::add(storm::ArithConstraint const& constraint) { - //if some of the occurring variables are not declared yet, we will have to. - std::set variables = constraint.lhs().gatherVariables(); - std::vector const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables); - for (auto declaration : varDeclarations){ - writeCommand(declaration, true); - } - writeCommand("( assert " + expressionAdapter->translateExpression(constraint) + " )", true); - } - - void SmtlibSmtSolver::add(storm::RationalFunctionVariable const& guard, typename storm::ArithConstraint const& constraint){ - STORM_LOG_THROW((guard.getType()==carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException, "Tried to add a guarded constraint, but the guard is not of type bool."); - //if some of the occurring variables are not declared yet, we will have to (including the guard!). - std::set variables = constraint.lhs().gatherVariables(); - variables.insert(guard); - std::vector const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables); - for (auto declaration : varDeclarations){ - writeCommand(declaration, true); - } - std::string guardName= carl::VariablePool::getInstance().getName(guard, this->useReadableVarNames); - writeCommand("( assert (=> " + guardName + " " + expressionAdapter->translateExpression(constraint) + " ) )", true); - } - void SmtlibSmtSolver::add(const storm::RationalFunctionVariable& variable, bool value){ STORM_LOG_THROW((variable.getType()==carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException, "Tried to add a constraint that consists of a non-boolean variable."); std::set variableSet; diff --git a/src/storm/solver/SmtlibSmtSolver.h b/src/storm/solver/SmtlibSmtSolver.h index 70e4c325f..6ae64eb92 100644 --- a/src/storm/solver/SmtlibSmtSolver.h +++ b/src/storm/solver/SmtlibSmtSolver.h @@ -51,12 +51,7 @@ namespace storm { //adds the constraint "leftHandSide relation rightHandSide" virtual void add(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation, storm::RationalFunction const& rightHandSide=storm::RationalFunction(0)); - //adds the given carl constraint - void add(typename storm::ArithConstraint const& constraint); - void add(typename storm::ArithConstraint const& constraint); - - // adds the given carl constraint that is guarded by the given guard. The guard should have type 'bool' - void add(storm::RationalFunctionVariable const& guard, typename storm::ArithConstraint const& constraint); + // asserts that the given variable has the given value. The variable should have type 'bool' void add(storm::RationalFunctionVariable const& variable, bool value); @@ -65,10 +60,9 @@ namespace storm { virtual CheckResult check() override; virtual CheckResult checkWithAssumptions(std::set const& assumptions) override; -#ifndef WINDOWS + virtual CheckResult checkWithAssumptions(std::initializer_list const& assumptions) override; -#endif - + bool isNeedsRestart() const; //Todo: some of these might be added in the future diff --git a/src/storm/storage/expressions/Variable.h b/src/storm/storage/expressions/Variable.h index 83ee9a13e..8a51df376 100644 --- a/src/storm/storage/expressions/Variable.h +++ b/src/storm/storage/expressions/Variable.h @@ -130,9 +130,9 @@ namespace storm { bool hasRationalType() const; /*! - * Checks whether the variable is of boolean type. + * Checks whether the variable is of numerical type. * - * @return True iff the variable if of boolean type. + * @return True iff the variable if of numerical type. */ bool hasNumericalType() const; diff --git a/src/storm/storm.cpp b/src/storm/storm.cpp index 8e915d6e7..3cba6dd3d 100644 --- a/src/storm/storm.cpp +++ b/src/storm/storm.cpp @@ -1,7 +1,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/BaseException.h" -#include "storm/cli/cli.h" +#include "storm-cli-utilities/cli.h" /*! * Main entry point of the executable storm. diff --git a/travis/build-helper.sh b/travis/build-helper.sh new file mode 100755 index 000000000..c6f2dff60 --- /dev/null +++ b/travis/build-helper.sh @@ -0,0 +1,164 @@ +#!/bin/bash +# Inspired by https://github.com/google/fruit + +set -e + +# Helper for travis folding +travis_fold() { + local action=$1 + local name=$2 + echo -en "travis_fold:${action}:${name}\r" +} + +# Helper for distinguishing between different runs +run() { + case "$1" in + Build1 | Build2 | Build3 | Build4) + if [[ "$1" == "Build1" ]] + then + # CMake + travis_fold start cmake + mkdir build + cd build + cmake .. "${CMAKE_ARGS[@]}" + echo + if [ -f "CMakeFiles/CMakeError.log" ] + then + echo "Content of CMakeFiles/CMakeError.log:" + cat CMakeFiles/CMakeError.log + fi + echo + cd .. + travis_fold end cmake + fi + + # Make + travis_fold start make + cd build + make -j$N_JOBS + travis_fold end make + # Set skip-file + if [[ "$1" != "Build4" ]] + then + touch skip.txt + else + rm -rf skip.txt + fi + ;; + + TestAll) + # Test all + travis_fold start test_all + cd build + ctest test --output-on-failure + travis_fold end test_all + ;; + + *) + echo "Unrecognized value of run: $1" + exit 1 + esac +} + + +# This only exists in OS X, but it doesn't cause issues in Linux (the dir doesn't exist, so it's +# ignored). +export PATH="/usr/local/opt/coreutils/libexec/gnubin:$PATH" + +case $COMPILER in +gcc-4.8) + export CC=gcc-4.8 + export CXX=g++-4.8 + ;; + +gcc-4.9) + export CC=gcc-4.9 + export CXX=g++-4.9 + ;; + +gcc-5) + export CC=gcc-5 + export CXX=g++-5 + ;; + +gcc-6) + export CC=gcc-6 + export CXX=g++-6 + ;; + +gcc-default) + export CC=gcc + export CXX=g++ + ;; + +clang-3.5) + export CC=clang-3.5 + export CXX=clang++-3.5 + ;; + +clang-3.6) + export CC=clang-3.6 + export CXX=clang++-3.6 + ;; + +clang-3.7) + export CC=clang-3.7 + export CXX=clang++-3.7 + ;; + +clang-3.8) + export CC=clang-3.8 + export CXX=clang++-3.8 + ;; + +clang-3.9) + export CC=clang-3.9 + export CXX=clang++-3.9 + ;; + +clang-4.0) + case "$OS" in + linux) + export CC=clang-4.0 + export CXX=clang++-4.0 + ;; + osx) + export CC=/usr/local/opt/llvm/bin/clang-4.0 + export CXX=/usr/local/opt/llvm/bin/clang++ + ;; + *) echo "Error: unexpected OS: $OS"; exit 1 ;; + esac + ;; + +clang-default) + export CC=clang + export CXX=clang++ + ;; + +*) + echo "Unrecognized value of COMPILER: $COMPILER" + exit 1 +esac + +# Build +echo CXX version: $($CXX --version) +echo C++ Standard library location: $(echo '#include ' | $CXX -x c++ -E - | grep 'vector\"' | awk '{print $3}' | sed 's@/vector@@;s@\"@@g' | head -n 1) +echo Normalized C++ Standard library location: $(readlink -f $(echo '#include ' | $CXX -x c++ -E - | grep 'vector\"' | awk '{print $3}' | sed 's@/vector@@;s@\"@@g' | head -n 1)) + +case "$CONFIG" in +DefaultDebug) CMAKE_ARGS=(-DCMAKE_BUILD_TYPE=Debug -DCMAKE_CXX_FLAGS="$STLARG") ;; +DefaultRelease) CMAKE_ARGS=(-DCMAKE_BUILD_TYPE=Release -DCMAKE_CXX_FLAGS="$STLARG") ;; +*) echo "Unrecognized value of CONFIG: $CONFIG"; exit 1 ;; +esac + +# Restore timestamps of files +travis_fold start mtime +if [[ "$1" == "Build1" ]] +then + # Remove old mtime cache + rm -rf travis/mtime_cache/cache.json +fi +ruby travis/mtime_cache/mtime_cache.rb -g travis/mtime_cache/globs.txt -c travis/mtime_cache/cache.json +travis_fold end mtime + +run "$1" diff --git a/travis/build.sh b/travis/build.sh new file mode 100755 index 000000000..0b7900e70 --- /dev/null +++ b/travis/build.sh @@ -0,0 +1,71 @@ +#!/bin/bash -x +# Inspired by https://github.com/google/fruit + +N_JOBS=2 +TIMEOUT_MAC=1600 +TIMEOUT_LINUX=2300 + +OS=$TRAVIS_OS_NAME + +EXITCODE=42 + +# Skip this run? +if [ -f build/skip.txt ] +then + # Remove flag s.t. tests will be executed + if [[ "$1" == "Build4" ]] + then + rm build/skip.txt + fi + exit 0 +fi + +case $OS in +linux) + # Execute docker image on Linux + # Stop previous session + docker rm -f storm &>/dev/null + # Run container + set -e + docker run -d -it --name storm --privileged mvolk/storm-basesystem:$LINUX + # Copy local content into container + docker exec storm mkdir storm + docker cp . storm:/storm + set +e + + # Execute main process + timeout $TIMEOUT_LINUX docker exec storm bash -c " + export CONFIG=$CONFIG; + export COMPILER=$COMPILER; + export N_JOBS=$N_JOBS; + export STLARG=; + export OS=$OS; + cd storm; + travis/build-helper.sh $1" + EXITCODE=$? + ;; + +osx) + # Mac OSX + STLARG="-stdlib=libc++" + export CONFIG=$CONFIG + export COMPILER + export N_JOBS + export STLARG + export OS + gtimeout $TIMEOUT_MAC travis/build-helper.sh "$1" + EXITCODE=$? + ;; + +*) + # Unknown OS + echo "Unsupported OS: $OS" + exit 1 +esac + +if [[ $EXITCODE == 124 ]] && [[ "$1" == Build* ]] && [[ "$1" != "Build4" ]] +then + exit 0 +else + exit $EXITCODE +fi diff --git a/travis/dockerfiles/Dockerfile.debian-9 b/travis/dockerfiles/Dockerfile.debian-9 new file mode 100644 index 000000000..3735b38fd --- /dev/null +++ b/travis/dockerfiles/Dockerfile.debian-9 @@ -0,0 +1,16 @@ +FROM debian:9 +MAINTAINER Matthias Volk + +RUN apt-get update -qq && apt-get install -y --no-install-recommends \ + build-essential \ + ruby \ + git \ + cmake \ + libboost-all-dev \ + libcln-dev \ + libeigen3-dev \ + libgmp-dev \ + libginac-dev \ + automake \ + libglpk-dev \ + libz3-dev diff --git a/travis/dockerfiles/Dockerfile.storm b/travis/dockerfiles/Dockerfile.storm new file mode 100644 index 000000000..272b97825 --- /dev/null +++ b/travis/dockerfiles/Dockerfile.storm @@ -0,0 +1,8 @@ +FROM mvolk/storm-basesystem:ubuntu-16.10 +MAINTAINER Matthias Volk + +COPY build_carl.sh /opt +RUN cd opt && ./build_carl.sh + +COPY build_storm.sh /opt +RUN cd opt && ./build_storm.sh diff --git a/travis/dockerfiles/Dockerfile.ubuntu-16.10 b/travis/dockerfiles/Dockerfile.ubuntu-16.10 new file mode 100644 index 000000000..a612faccb --- /dev/null +++ b/travis/dockerfiles/Dockerfile.ubuntu-16.10 @@ -0,0 +1,17 @@ +FROM ubuntu:16.10 +MAINTAINER Matthias Volk + +RUN apt-get update -qq && apt-get install -y --no-install-recommends \ + build-essential \ + ruby \ + git \ + cmake \ + libboost-all-dev \ + libcln-dev \ + libeigen3-dev \ + libgmp-dev \ + libginac-dev \ + automake \ + libglpk-dev \ + libhwloc-dev \ + libz3-dev diff --git a/travis/dockerfiles/build_carl.sh b/travis/dockerfiles/build_carl.sh new file mode 100755 index 000000000..fc3d43d22 --- /dev/null +++ b/travis/dockerfiles/build_carl.sh @@ -0,0 +1,9 @@ +#!/bin/bash +echo "Building Carl..." +git clone https://github.com/smtrat/carl.git +cd carl +mkdir build +cd build +cmake .. -DCMAKE_BUILD_TYPE=Release -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON +make lib_carl -j2 +echo "Building Carl finished" diff --git a/travis/dockerfiles/build_docker.sh b/travis/dockerfiles/build_docker.sh new file mode 100755 index 000000000..280710566 --- /dev/null +++ b/travis/dockerfiles/build_docker.sh @@ -0,0 +1,9 @@ +#!/bin/bash + +# Build Ubuntu 16.10 "Yakkety Yak" +docker build -t mvolk/storm-basesystem:ubuntu-16.10 -f Dockerfile.ubuntu-16.10 . +docker push mvolk/storm-basesystem:ubuntu-16.10 + +# Build Debian 9 "Stretch" +docker build -t mvolk/storm-basesystem:debian-9 -f Dockerfile.debian-9 . +docker push mvolk/storm-basesystem:debian-9 diff --git a/travis/dockerfiles/build_storm.sh b/travis/dockerfiles/build_storm.sh new file mode 100755 index 000000000..4c11b708d --- /dev/null +++ b/travis/dockerfiles/build_storm.sh @@ -0,0 +1,9 @@ +#!/bin/bash +echo "Building Storm..." +git clone https://github.com/moves-rwth/storm.git +cd storm +mkdir build +cd build +cmake .. -DCMAKE_BUILD_TYPE=Release +make storm storm-dft storm-pars -j1 +echo "Building Storm finished" diff --git a/travis/generate_travis.py b/travis/generate_travis.py new file mode 100644 index 000000000..c47afac0c --- /dev/null +++ b/travis/generate_travis.py @@ -0,0 +1,123 @@ + +# Configuration for Linux +configs_linux = [ + # OS, compiler + ("ubuntu-16.10", "gcc", "-6"), + #("debian-9", "gcc", "-6"), +] + +# Configurations for Mac +configs_mac = [ + # OS, compiler + ("osx", "clang", "-4.0"), +] + +# Build types +build_types = [ + "DefaultDebug", + "DefaultRelease", +] + +# Stages in travis +stages = [ + ("Build (1st run)", "Build1"), + ("Build (2nd run)", "Build2"), + ("Build (3rd run)", "Build3"), + ("Build (4th run)", "Build4"), + ("Test all", "TestAll"), +] + + +if __name__ == "__main__": + s = "" + # Initial config + s += "# This file was inspired from https://github.com/google/fruit\n" + s += "\n" + s += "#\n" + s += "# General config\n" + s += "#\n" + s += "branches:\n" + s += " only:\n" + s += " - master\n" + s += " - stable\n" + s += "dist: trusty\n" + s += "language: cpp\n" + s += "\n" + s += "# Enable caching\n" + s += "cache:\n" + s += " timeout: 1000\n" + s += " directories:\n" + s += " - build\n" + s += " - travis/mtime_cache\n" + s += "\n" + s += "# Enable docker support\n" + s += "services:\n" + s += "- docker\n" + s += "sudo: required\n" + s += "\n" + + s += "notifications:\n" + s += " email:\n" + s += " on_failure: always\n" + s += " on_success: change\n" + s += " recipients:\n" + s += ' secure: "Q9CW/PtyWkZwExDrfFFb9n1STGYsRfI6awv1bZHcGwfrDvhpXoMCuF8CwviIfilm7fFJJEoKizTtdRpY0HrOnY/8KY111xrtcFYosxdndv7xbESodIxQOUoIEFCO0mCNHwWYisoi3dAA7H3Yn661EsxluwHjzX5vY0xSbw0n229hlsFz092HwGLSU33zHl7eXpQk+BOFmBTRGlOq9obtDZ17zbHz1oXFZntHK/JDUIYP0b0uq8NvE2jM6CIVdcuSwmIkOhZJoO2L3Py3rBbPci+L2PSK4Smv2UjCPF8KusnOaFIyDB3LcNM9Jqq5ssJMrK/KaO6BiuYrOZXYWZ7KEg3Y/naC8HjOH1dzty+P7oW46sb9F03pTsufqD4R7wcK+9wROTztO6aJPDG/IPH7EWgrBTxqlOkVRwi2eYuQouZpZUW6EMClKbMHMIxCH2S8aOk/r1w2cNwmPEcunnP0nl413x/ByHr4fTPFykPj8pQxIsllYjpdWBRQfDOauKWGzk6LcrFW0qpWP+/aJ2vYu/IoZQMG5lMHbp6Y1Lg09pYm7Q983v3b7D+JvXhOXMyGq91HyPahA2wwKoG1GA4uoZ2I95/IFYNiKkelDd3WTBoFLNF9YFoEJNdCywm1fO2WY4WkyEFBuQcgDA+YpFMJJMxjTbivYk9jvHk2gji//2w="\n' + s += "\n" + s += "#\n" + s += "# Configurations\n" + s += "#\n" + s += "jobs:\n" + s += " include:\n" + + # Generate all configurations + for stage in stages: + s += "\n" + s += " ###\n" + s += " # Stage: {}\n".format(stage[0]) + s += " ###\n" + s += "\n" + # Mac OS X + for config in configs_mac: + osx = config[0] + compiler = "{}{}".format(config[1], config[2]) + s += " # {}\n".format(osx) + buildConfig = "" + for build in build_types: + buildConfig += " - stage: {}\n".format(stage[0]) + buildConfig += " os: osx\n" + buildConfig += " compiler: {}\n".format(config[1]) + buildConfig += " env: CONFIG={} COMPILER={} STL=libc++\n".format(build, compiler) + buildConfig += " install:\n" + if stage[1] == "Build1": + buildConfig += " - rm -rf build\n" + buildConfig += " - travis/install_osx.sh\n" + buildConfig += " script:\n" + buildConfig += " - travis/build.sh {}\n".format(stage[1]) + buildConfig += " after_failure:\n" + buildConfig += " - find build -iname '*err*.log' -type f -print -exec cat {} \;\n" + s += buildConfig + + # Linux via Docker + for config in configs_linux: + linux = config[0] + compiler = "{}{}".format(config[1], config[2]) + s += " # {}\n".format(linux) + buildConfig = "" + for build in build_types: + buildConfig += " - stage: {}\n".format(stage[0]) + buildConfig += " os: linux\n" + buildConfig += " compiler: {}\n".format(config[1]) + buildConfig += " env: CONFIG={} LINUX={} COMPILER={}\n".format(build, linux, compiler) + buildConfig += " install:\n" + if stage[1] == "Build1": + buildConfig += " - rm -rf build\n" + buildConfig += " - travis/install_linux.sh\n" + buildConfig += " script:\n" + buildConfig += " - travis/build.sh {}\n".format(stage[1]) + buildConfig += " before_cache:\n" + buildConfig += " - docker cp storm:/storm/. .\n" + buildConfig += " after_failure:\n" + buildConfig += " - find build -iname '*err*.log' -type f -print -exec cat {} \;\n" + s += buildConfig + + print(s) diff --git a/travis/install_linux.sh b/travis/install_linux.sh new file mode 100755 index 000000000..c7ef04886 --- /dev/null +++ b/travis/install_linux.sh @@ -0,0 +1,11 @@ +#!/bin/bash + +set -e + +# Skip this run? +if [ -f build/skip.txt ] +then + exit 0 +fi + +sudo apt-get install -qq -y docker diff --git a/travis/install_osx.sh b/travis/install_osx.sh new file mode 100755 index 000000000..8d703a82a --- /dev/null +++ b/travis/install_osx.sh @@ -0,0 +1,73 @@ +#!/bin/bash +# Script installing dependencies +# Inspired by https://github.com/google/fruit + +set -e + +# Helper for travis folding +travis_fold() { + local action=$1 + local name=$2 + echo -en "travis_fold:${action}:${name}\r" +} + +# Helper for installing packages via homebrew +install_brew_package() { + if brew list -1 | grep -q "^$1\$"; then + # Package is installed, upgrade if needed + brew outdated "$1" || brew upgrade "$@" + else + # Package not installed yet, install. + # If there are conflicts, try overwriting the files (these are in /usr/local anyway so it should be ok). + brew install "$@" || brew link --overwrite gcc49 + fi +} + +# Skip this run? +if [ -f build/skip.txt ] +then + exit 0 +fi + +# Update packages +travis_fold start brew_update +brew update +travis_fold end brew_update + +travis_fold start brew_install_util +# For md5sum +install_brew_package md5sha1sum +# For `timeout' +install_brew_package coreutils + +which cmake &>/dev/null || install_brew_package cmake + +# Install compiler +case "${COMPILER}" in +gcc-4.8) install_brew_package gcc@4.8 ;; +gcc-4.9) install_brew_package gcc@4.9 ;; +gcc-5) install_brew_package gcc@5 ;; +gcc-6) install_brew_package gcc@6 ;; +clang-default) ;; +clang-3.7) install_brew_package llvm@3.7 --with-clang --with-libcxx;; +clang-3.8) install_brew_package llvm@3.8 --with-clang --with-libcxx;; +clang-3.9) install_brew_package llvm@3.9 --with-clang --with-libcxx;; +clang-4.0) install_brew_package llvm --with-clang --with-libcxx;; +*) echo "Compiler not supported: ${COMPILER}. See travis/install_osx.sh"; exit 1 ;; +esac +travis_fold end brew_install_util + + +# Install dependencies +travis_fold start brew_install_dependencies +install_brew_package gmp --c++11 +install_brew_package cln +install_brew_package ginac +install_brew_package doxygen +install_brew_package boost --c++11 +install_brew_package z3 # optional +brew tap homebrew/science +install_brew_package homebrew/science/glpk +install_brew_package homebrew/science/hwloc +install_brew_package eigen +travis_fold end brew_install_dependencies diff --git a/travis/mtime_cache/globs.txt b/travis/mtime_cache/globs.txt new file mode 100644 index 000000000..cd0d4d2ff --- /dev/null +++ b/travis/mtime_cache/globs.txt @@ -0,0 +1,4 @@ +src/**/*.{%{cpp}} +src/**/CMakeLists.txt +resources/3rdparty/**/*.{%{cpp}} +resources/3rdparty/eigen-3.3-beta1/StormEigen/* diff --git a/travis/mtime_cache/mtime_cache.rb b/travis/mtime_cache/mtime_cache.rb new file mode 100644 index 000000000..299a1595e --- /dev/null +++ b/travis/mtime_cache/mtime_cache.rb @@ -0,0 +1,178 @@ +#!/usr/bin/env ruby + +# +# mtime_cache +# Copyright (c) 2016 Borislav Stanimirov +# +# Permission is hereby granted, free of charge, to any person obtaining a copy +# of this software and associated documentation files (the "Software"), to +# deal in the Software without restriction, including without limitation the +# rights to use, copy, modify, merge, publish, distribute, sublicense, and/or +# sell copies of the Software, and to permit persons to whom the Software is +# furnished to do so, subject to the following conditions: +# +# The above copyright notice and this permission notice shall be included in +# all copies or substantial portions of the Software. +# +# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +# FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS +# IN THE SOFTWARE. +# + +require 'digest/md5' +require 'json' +require 'fileutils' + +VERSION = "1.0.2" + +VERSION_TEXT = "mtime_cache v#{VERSION}" + +USAGE = <] [-g globfile] [-d] [-q|V] [-c cache] +ENDUSAGE + +HELP = < '.mtime_cache.json', :globs => [] } + +ARGV.each do |arg| + case arg + when '-g', '--globfile' then param_arg = :globfile + when '-h', '-?', '--help' then ARGS[:help] = true + when '-v', '--version' then ARGS[:ver] = true + when '-q', '--quiet' then ARGS[:quiet] = true + when '-V', '--verbose' then ARGS[:verbose] = true + when '-d', '--dryrun' then ARGS[:dry] = true + when '-c', '--cache' then param_arg = :cache + else + if param_arg + ARGS[param_arg] = arg + param_arg = nil + else + ARGS[:globs] << arg + end + end +end + +def log(text, level = 0) + return if ARGS[:quiet] + return if level > 0 && !ARGS[:verbose] + puts text +end + +if ARGS[:ver] || ARGS[:help] + log VERSION_TEXT + exit if ARGS[:ver] + log USAGE + log HELP + exit +end + +if ARGS[:globs].empty? && !ARGS[:globfile] + log 'Error: Missing globs' + log USAGE + exit 1 +end + +EXTENSION_PATTERNS = { + :cpp => "c,cc,cpp,cxx,h,hpp,hxx,inl,ipp,inc,ixx" +} + +cache_file = ARGS[:cache] + +cache = {} + +if File.file?(cache_file) + log "Found #{cache_file}" + cache = JSON.parse(File.read(cache_file)) + log "Read #{cache.length} entries" +else + log "#{cache_file} not found. A new one will be created" +end + +globs = ARGS[:globs].map { |g| g % EXTENSION_PATTERNS } + +globfile = ARGS[:globfile] +if globfile + File.open(globfile, 'r').each_line do |line| + line.strip! + next if line.empty? + globs << line % EXTENSION_PATTERNS + end +end + +if globs.empty? + log 'Error: No globs in globfile' + log USAGE + exit 1 +end + +files = {} +num_changed = 0 + +globs.each do |glob| + Dir[glob].each do |file| + next if !File.file?(file) + + mtime = File.mtime(file).to_i + hash = Digest::MD5.hexdigest(File.read(file)) + + cached = cache[file] + + if cached && cached['hash'] == hash && cached['mtime'] < mtime + mtime = cached['mtime'] + + log "mtime_cache: changing mtime of #{file} to #{mtime}", 1 + + File.utime(File.atime(file), Time.at(mtime), file) if !ARGS[:dry] + num_changed += 1 + else + log "mtime_cache: NOT changing mtime of #{file}", 1 + end + + files[file] = { 'mtime' => mtime, 'hash' => hash } + end +end + +log "Changed mtime of #{num_changed} of #{files.length} files" +log "Writing #{cache_file}" + +if !ARGS[:dry] + dirname = File.dirname(cache_file) + unless File.directory?(dirname) + FileUtils.mkdir_p(dirname) + end + File.open(cache_file, 'w').write(JSON.pretty_generate(files)) +end +