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..56004ed4f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,7 +6,12 @@ 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 +Long run average computation via ValueIteration, LP based MDP model checking, parametric model checking has an own binary + +### Version 1.1.1 +- c++ api changes: Building model takes BuilderOptions instead of extended list of Booleans, does not depend on settings anymore. +- storm-cli-utilities now contains cli related stuff, instead of storm-lib +- storm-pars: support for welldefinedness constraints in mdps. ### 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 1591fa464..ce379dc0e 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -208,7 +208,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 (NOT STORM_FORCE_SHIPPED_CARL) if (NOT "${STORM_CARL_DIR_HINT}" STREQUAL "") 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-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp new file mode 100644 index 000000000..cb33c3205 --- /dev/null +++ b/src/storm-cli-utilities/cli.cpp @@ -0,0 +1,265 @@ +#include "cli.h" + + +#include "storm/utility/resources.h" +#include "storm/utility/file.h" +#include "storm/utility/storm-version.h" +#include "storm/utility/macros.h" + +#include "storm/utility/initialize.h" +#include "storm/utility/Stopwatch.h" + +#include + +#include "storm-cli-utilities/model-handling.h" + + +// Includes for the linked libraries and versions header. +#ifdef STORM_HAVE_INTELTBB +# include "tbb/tbb_stddef.h" +#endif +#ifdef STORM_HAVE_GLPK +# include "glpk.h" +#endif +#ifdef STORM_HAVE_GUROBI +# include "gurobi_c.h" +#endif +#ifdef STORM_HAVE_Z3 +# include "z3.h" +#endif +#ifdef STORM_HAVE_MSAT +# include "mathsat.h" +#endif +#ifdef STORM_HAVE_CUDA +#include +#include +#endif + +#ifdef STORM_HAVE_SMTRAT +#include "lib/smtrat.h" +#endif + +namespace storm { + namespace cli { + + int64_t process(const int argc, const char** argv) { + 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(); + if (storm::settings::getModule().isPrintTimeAndMemorySet()) { + storm::cli::printTimeAndMemoryStatistics(totalTimer.getTimeInMilliseconds()); + } + + storm::utility::cleanUp(); + return 0; + } + + + void printHeader(std::string const& name, const int argc, const char* argv[]) { + STORM_PRINT(name << " " << storm::utility::StormVersion::shortVersionString() << std::endl << std::endl); + + // "Compute" the command line argument string with which storm was invoked. + std::stringstream commandStream; + for (int i = 1; i < argc; ++i) { + commandStream << argv[i] << " "; + } + + std::string command = commandStream.str(); + + if (!command.empty()) { + STORM_PRINT("Command line arguments: " << commandStream.str() << std::endl); + STORM_PRINT("Current working directory: " << storm::utility::cli::getCurrentWorkingDirectory() << std::endl << std::endl); + } + } + + void printVersion(std::string const& name) { + STORM_PRINT(storm::utility::StormVersion::longVersionString() << std::endl); + STORM_PRINT(storm::utility::StormVersion::buildInfo() << std::endl); + +#ifdef STORM_HAVE_INTELTBB + STORM_PRINT("Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl); +#endif +#ifdef STORM_HAVE_GLPK + STORM_PRINT("Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl); +#endif +#ifdef STORM_HAVE_GUROBI + STORM_PRINT("Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl); +#endif +#ifdef STORM_HAVE_Z3 + unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber; + Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber); + STORM_PRINT("Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl); +#endif +#ifdef STORM_HAVE_MSAT + char* msatVersion = msat_get_version(); + STORM_PRINT("Linked with " << msatVersion << "." << std::endl); + msat_free(msatVersion); +#endif +#ifdef STORM_HAVE_SMTRAT + STORM_PRINT("Linked with SMT-RAT " << SMTRAT_VERSION << "." << std::endl); +#endif +#ifdef STORM_HAVE_CARL + // TODO get version string + STORM_PRINT("Linked with CArL." << std::endl); +#endif + +#ifdef STORM_HAVE_CUDA + int deviceCount = 0; + cudaError_t error_id = cudaGetDeviceCount(&deviceCount); + + if (error_id == cudaSuccess) { + STORM_PRINT("Compiled with CUDA support, "); + // This function call returns 0 if there are no CUDA capable devices. + if (deviceCount == 0){ + STORM_PRINT("but there are no available device(s) that support CUDA." << std::endl); + } else { + STORM_PRINT("detected " << deviceCount << " CUDA capable device(s):" << std::endl); + } + + int dev, driverVersion = 0, runtimeVersion = 0; + + for (dev = 0; dev < deviceCount; ++dev) { + cudaSetDevice(dev); + cudaDeviceProp deviceProp; + cudaGetDeviceProperties(&deviceProp, dev); + + STORM_PRINT("CUDA device " << dev << ": \"" << deviceProp.name << "\"" << std::endl); + + // Console log + cudaDriverGetVersion(&driverVersion); + cudaRuntimeGetVersion(&runtimeVersion); + STORM_PRINT(" CUDA Driver Version / Runtime Version " << driverVersion / 1000 << "." << (driverVersion % 100) / 10 << " / " << runtimeVersion / 1000 << "." << (runtimeVersion % 100) / 10 << std::endl); + STORM_PRINT(" CUDA Capability Major/Minor version number: " << deviceProp.major << "." << deviceProp.minor << std::endl); + } + STORM_PRINT(std::endl); + } + else { + STORM_PRINT("Compiled with CUDA support, but an error occured trying to find CUDA devices." << std::endl); + } +#endif + } + + bool parseOptions(const int argc, const char* argv[]) { + try { + storm::settings::mutableManager().setFromCommandLine(argc, argv); + } catch (storm::exceptions::OptionParserException& e) { + storm::settings::manager().printHelp(); + throw e; + return false; + } + + storm::settings::modules::GeneralSettings const& general = storm::settings::getModule(); + + bool result = true; + if (general.isHelpSet()) { + storm::settings::manager().printHelp(storm::settings::getModule().getHelpModuleName()); + result = false; + } + + if (general.isVersionSet()) { + printVersion("storm"); + result = false;; + } + + return result; + } + + void setResourceLimits() { + storm::settings::modules::ResourceSettings const& resources = storm::settings::getModule(); + + // If we were given a time limit, we put it in place now. + if (resources.isTimeoutSet()) { + storm::utility::resources::setCPULimit(resources.getTimeoutInSeconds()); + } + } + + void setLogLevel() { + storm::settings::modules::GeneralSettings const& general = storm::settings::getModule(); + storm::settings::modules::DebugSettings const& debug = storm::settings::getModule(); + + if (general.isVerboseSet()) { + storm::utility::setLogLevel(l3pp::LogLevel::INFO); + } + if (debug.isDebugSet()) { + storm::utility::setLogLevel(l3pp::LogLevel::DEBUG); + } + if (debug.isTraceSet()) { + storm::utility::setLogLevel(l3pp::LogLevel::TRACE); + } + if (debug.isLogfileSet()) { + storm::utility::initializeFileLogging(); + } + } + + void setFileLogging() { + storm::settings::modules::DebugSettings const& debug = storm::settings::getModule(); + if (debug.isLogfileSet()) { + storm::utility::initializeFileLogging(); + } + } + + void setUrgentOptions() { + setResourceLimits(); + setLogLevel(); + setFileLogging(); + } + + + void processOptions() { + // Start by setting some urgent options (log levels, resources, etc.) + setUrgentOptions(); + + // Parse and preprocess symbolic input (PRISM, JANI, properties, etc.) + SymbolicInput symbolicInput = parseAndPreprocessSymbolicInput(); + + auto generalSettings = storm::settings::getModule(); + if (generalSettings.isParametricSet()) { +#ifdef STORM_HAVE_CARL + processInputWithValueType(symbolicInput); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build."); +#endif + } else if (generalSettings.isExactSet()) { +#ifdef STORM_HAVE_CARL + processInputWithValueType(symbolicInput); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No exact numbers are supported in this build."); +#endif + } else { + processInputWithValueType(symbolicInput); + } + } + + void printTimeAndMemoryStatistics(uint64_t wallclockMilliseconds) { + struct rusage ru; + getrusage(RUSAGE_SELF, &ru); + + std::cout << std::endl << "Performance statistics:" << std::endl; +#ifdef MACOS + // For Mac OS, this is returned in bytes. + uint64_t maximumResidentSizeInMegabytes = ru.ru_maxrss / 1024 / 1024; +#endif +#ifdef LINUX + // For Linux, this is returned in kilobytes. + uint64_t maximumResidentSizeInMegabytes = ru.ru_maxrss / 1024; +#endif + std::cout << " * peak memory usage: " << maximumResidentSizeInMegabytes << "MB" << std::endl; + char oldFillChar = std::cout.fill('0'); + std::cout << " * CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << ru.ru_utime.tv_usec/1000 << "s" << std::endl; + if (wallclockMilliseconds != 0) { + std::cout << " * wallclock time: " << (wallclockMilliseconds/1000) << "." << std::setw(3) << (wallclockMilliseconds % 1000) << "s" << std::endl; + } + std::cout.fill(oldFillChar); + } + + } +} 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/cli/cli.cpp b/src/storm-cli-utilities/model-handling.h similarity index 71% rename from src/storm/cli/cli.cpp rename to src/storm-cli-utilities/model-handling.h index 166ab07cf..588d0d330 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm-cli-utilities/model-handling.h @@ -1,259 +1,52 @@ -#include "storm/cli/cli.h" +#pragma once + +#include "storm/api/storm.h" + +#include "storm/utility/resources.h" +#include "storm/utility/file.h" +#include "storm/utility/storm-version.h" +#include "storm/utility/macros.h" + +#include "storm/utility/initialize.h" +#include "storm/utility/Stopwatch.h" + +#include -#include -#include -#include -#include #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/utility/resources.h" -#include "storm/utility/file.h" -#include "storm/utility/storm-version.h" -#include "storm/utility/cli.h" - -#include "storm/utility/initialize.h" -#include "storm/utility/Stopwatch.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 - -#include "storm/api/storm.h" - -#include "storm/utility/macros.h" - -// Includes for the linked libraries and versions header. -#ifdef STORM_HAVE_INTELTBB -# include "tbb/tbb_stddef.h" -#endif -#ifdef STORM_HAVE_GLPK -# include "glpk.h" -#endif -#ifdef STORM_HAVE_GUROBI -# include "gurobi_c.h" -#endif -#ifdef STORM_HAVE_Z3 -# include "z3.h" -#endif -#ifdef STORM_HAVE_MSAT -# include "mathsat.h" -#endif -#ifdef STORM_HAVE_CUDA -#include -#include -#endif - -#ifdef STORM_HAVE_SMTRAT -#include "lib/smtrat.h" -#endif +#include "storm/utility/Stopwatch.h" namespace storm { namespace cli { - - int64_t process(const int argc, const char** argv) { - 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(); - if (storm::settings::getModule().isPrintTimeAndMemorySet()) { - storm::cli::printTimeAndMemoryStatistics(totalTimer.getTimeInMilliseconds()); - } - - storm::utility::cleanUp(); - return 0; - } - - std::string currentTimeAndDate() { - auto now = std::chrono::system_clock::now(); - auto in_time_t = std::chrono::system_clock::to_time_t(now); - - std::stringstream ss; - ss << std::put_time(std::localtime(&in_time_t), "%d/%m/%Y %X"); - return ss.str(); - } - - void printHeader(std::string const& name, const int argc, const char* argv[]) { - STORM_PRINT(name << " " << storm::utility::StormVersion::shortVersionString() << std::endl << std::endl); - - // "Compute" the command line argument string with which storm was invoked. - std::stringstream commandStream; - for (int i = 1; i < argc; ++i) { - commandStream << argv[i] << " "; - } - - std::string command = commandStream.str(); - - if (!command.empty()) { - STORM_PRINT("Command line arguments: " << commandStream.str() << std::endl); - STORM_PRINT("Current working directory: " << storm::utility::cli::getCurrentWorkingDirectory() << std::endl); - STORM_PRINT("Current date/time: " << currentTimeAndDate() << std::endl << std::endl); - } - } - - void printVersion(std::string const& name) { - STORM_PRINT(storm::utility::StormVersion::longVersionString() << std::endl); - STORM_PRINT(storm::utility::StormVersion::buildInfo() << std::endl); - -#ifdef STORM_HAVE_INTELTBB - STORM_PRINT("Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl); -#endif -#ifdef STORM_HAVE_GLPK - STORM_PRINT("Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl); -#endif -#ifdef STORM_HAVE_GUROBI - STORM_PRINT("Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl); -#endif -#ifdef STORM_HAVE_Z3 - unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber; - Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber); - STORM_PRINT("Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl); -#endif -#ifdef STORM_HAVE_MSAT - char* msatVersion = msat_get_version(); - STORM_PRINT("Linked with " << msatVersion << "." << std::endl); - msat_free(msatVersion); -#endif -#ifdef STORM_HAVE_SMTRAT - STORM_PRINT("Linked with SMT-RAT " << SMTRAT_VERSION << "." << std::endl); -#endif -#ifdef STORM_HAVE_CARL - // TODO get version string - STORM_PRINT("Linked with CArL." << std::endl); -#endif - -#ifdef STORM_HAVE_CUDA - int deviceCount = 0; - cudaError_t error_id = cudaGetDeviceCount(&deviceCount); - - if (error_id == cudaSuccess) { - STORM_PRINT("Compiled with CUDA support, "); - // This function call returns 0 if there are no CUDA capable devices. - if (deviceCount == 0){ - STORM_PRINT("but there are no available device(s) that support CUDA." << std::endl); - } else { - STORM_PRINT("detected " << deviceCount << " CUDA capable device(s):" << std::endl); - } - - int dev, driverVersion = 0, runtimeVersion = 0; - - for (dev = 0; dev < deviceCount; ++dev) { - cudaSetDevice(dev); - cudaDeviceProp deviceProp; - cudaGetDeviceProperties(&deviceProp, dev); - - STORM_PRINT("CUDA device " << dev << ": \"" << deviceProp.name << "\"" << std::endl); - - // Console log - cudaDriverGetVersion(&driverVersion); - cudaRuntimeGetVersion(&runtimeVersion); - STORM_PRINT(" CUDA Driver Version / Runtime Version " << driverVersion / 1000 << "." << (driverVersion % 100) / 10 << " / " << runtimeVersion / 1000 << "." << (runtimeVersion % 100) / 10 << std::endl); - STORM_PRINT(" CUDA Capability Major/Minor version number: " << deviceProp.major << "." << deviceProp.minor << std::endl); - } - STORM_PRINT(std::endl); - } - else { - STORM_PRINT("Compiled with CUDA support, but an error occured trying to find CUDA devices." << std::endl); - } -#endif - } - - bool parseOptions(const int argc, const char* argv[]) { - try { - storm::settings::mutableManager().setFromCommandLine(argc, argv); - } catch (storm::exceptions::OptionParserException& e) { - storm::settings::manager().printHelp(); - throw e; - return false; - } - - storm::settings::modules::GeneralSettings const& general = storm::settings::getModule(); - bool result = true; - if (general.isHelpSet()) { - storm::settings::manager().printHelp(storm::settings::getModule().getHelpModuleName()); - result = false; - } - - if (general.isVersionSet()) { - printVersion("storm"); - result = false;; - } - return result; - } - - void setResourceLimits() { - storm::settings::modules::ResourceSettings const& resources = storm::settings::getModule(); - - // If we were given a time limit, we put it in place now. - if (resources.isTimeoutSet()) { - storm::utility::resources::setCPULimit(resources.getTimeoutInSeconds()); - } - } - - void setLogLevel() { - storm::settings::modules::GeneralSettings const& general = storm::settings::getModule(); - storm::settings::modules::DebugSettings const& debug = storm::settings::getModule(); - - if (general.isVerboseSet()) { - storm::utility::setLogLevel(l3pp::LogLevel::INFO); - } - if (debug.isDebugSet()) { - storm::utility::setLogLevel(l3pp::LogLevel::DEBUG); - } - if (debug.isTraceSet()) { - storm::utility::setLogLevel(l3pp::LogLevel::TRACE); - } - if (debug.isLogfileSet()) { - storm::utility::initializeFileLogging(); - } - } - - void setFileLogging() { - storm::settings::modules::DebugSettings const& debug = storm::settings::getModule(); - if (debug.isLogfileSet()) { - storm::utility::initializeFileLogging(); - } - } - - void setUrgentOptions() { - setResourceLimits(); - setLogLevel(); - setFileLogging(); - } - struct SymbolicInput { // The symbolic model description. boost::optional model; - + // The properties to check. std::vector properties; }; - + void parseSymbolicModelDescription(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input) { if (ioSettings.isPrismOrJaniInputSet()) { if (ioSettings.isPrismInputSet()) { @@ -262,7 +55,7 @@ namespace storm { auto janiInput = storm::api::parseJaniModel(ioSettings.getJaniInputFilename()); input.model = janiInput.first; auto const& janiPropertyInput = janiInput.second; - + if (ioSettings.isJaniPropertiesSet()) { for (auto const& propName : ioSettings.getJaniProperties()) { auto propertyIt = janiPropertyInput.find(propName); @@ -273,7 +66,7 @@ namespace storm { } } } - + void parseProperties(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input, boost::optional> const& propertyFilter) { if (ioSettings.isPropertySet()) { std::vector newProperties; @@ -282,30 +75,30 @@ namespace storm { } else { newProperties = storm::api::parseProperties(ioSettings.getProperty(), propertyFilter); } - + input.properties.insert(input.properties.end(), newProperties.begin(), newProperties.end()); } } - + SymbolicInput parseSymbolicInput() { auto ioSettings = storm::settings::getModule(); // Parse the property filter, if any is given. boost::optional> propertyFilter = storm::api::parsePropertyFilter(ioSettings.getPropertyFilter()); - + SymbolicInput input; parseSymbolicModelDescription(ioSettings, input); parseProperties(ioSettings, input, propertyFilter); - + return input; } - + SymbolicInput preprocessSymbolicInput(SymbolicInput const& input) { auto ioSettings = storm::settings::getModule(); auto coreSettings = storm::settings::getModule(); SymbolicInput output = input; - + // Substitute constant definitions in symbolic input. std::string constantDefinitionString = ioSettings.getConstantDefinitionString(); std::map constantDefinitions; @@ -316,19 +109,19 @@ namespace storm { if (!output.properties.empty()) { output.properties = storm::api::substituteConstantsInProperties(output.properties, constantDefinitions); } - + // Check whether conversion for PRISM to JANI is requested or necessary. if (input.model && input.model.get().isPrismProgram()) { bool transformToJani = ioSettings.isPrismToJaniSet(); bool transformToJaniForJit = coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse && ioSettings.isJitSet(); STORM_LOG_WARN_COND(transformToJani || !transformToJaniForJit, "The JIT-based model builder is only available for JANI models, automatically converting the PRISM input model."); transformToJani |= transformToJaniForJit; - + if (transformToJani) { storm::prism::Program const& model = output.model.get().asPrismProgram(); auto modelAndRenaming = model.toJaniWithLabelRenaming(true); output.model = modelAndRenaming.first; - + if (!modelAndRenaming.second.empty()) { std::map const& labelRenaming = modelAndRenaming.second; std::vector amendedProperties; @@ -339,10 +132,10 @@ namespace storm { } } } - + return output; } - + void exportSymbolicInput(SymbolicInput const& input) { auto ioSettings = storm::settings::getModule(); if (input.model && input.model.get().isJaniModel()) { @@ -350,23 +143,23 @@ namespace storm { if (ioSettings.isExportJaniDotSet()) { storm::api::exportJaniModelAsDot(model.asJaniModel(), ioSettings.getExportJaniDotFilename()); } - + if (model.isJaniModel() && storm::settings::getModule().isJaniFileSet()) { storm::api::exportJaniModel(model.asJaniModel(), input.properties, storm::settings::getModule().getJaniFilename()); } } } - + SymbolicInput parseAndPreprocessSymbolicInput() { SymbolicInput input = parseSymbolicInput(); input = preprocessSymbolicInput(input); exportSymbolicInput(input); return input; } - + std::vector> createFormulasToRespect(std::vector const& properties) { std::vector> result = storm::api::extractFormulasFromProperties(properties); - + for (auto const& property : properties) { if (!property.getFilter().getStatesFormula()->isInitialFormula()) { result.push_back(property.getFilter().getStatesFormula()); @@ -375,16 +168,24 @@ namespace storm { return result; } - + template std::shared_ptr buildModelDd(SymbolicInput const& input) { - return storm::api::buildSymbolicModel(input.model.get(), createFormulasToRespect(input.properties)); + return storm::api::buildSymbolicModel(input.model.get(), createFormulasToRespect(input.properties), storm::settings::getModule().isBuildFullModelSet()); } 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 @@ -416,7 +217,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 = buildModelExplicit(ioSettings); } - + modelBuildingWatch.stop(); if (result) { STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl); @@ -424,7 +225,7 @@ namespace storm { return result; } - + template std::shared_ptr> preprocessSparseMarkovAutomaton(std::shared_ptr> const& model) { std::shared_ptr> result = model; @@ -441,40 +242,40 @@ namespace storm { if (bisimulationSettings.isWeakBisimulationSet()) { bisimType = storm::storage::BisimulationType::Weak; } - + STORM_LOG_INFO("Performing bisimulation minimization..."); return storm::api::performBisimulationMinimization(model, createFormulasToRespect(input.properties), bisimType); } - + template std::pair>, bool> preprocessSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { - auto generalSettings = storm::settings::getModule(); - auto bisimulationSettings = storm::settings::getModule(); - auto ioSettings = storm::settings::getModule(); - - std::pair>, bool> result = std::make_pair(model, false); - - if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { - result.first = preprocessSparseMarkovAutomaton(result.first->template as>()); - result.second = true; - } - - if (generalSettings.isBisimulationSet()) { - result.first = preprocessSparseModelBisimulation(result.first, input, bisimulationSettings); - result.second = true; - } - - return result; + auto generalSettings = storm::settings::getModule(); + auto bisimulationSettings = storm::settings::getModule(); + auto ioSettings = storm::settings::getModule(); + + std::pair>, bool> result = std::make_pair(model, false); + + if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { + result.first = preprocessSparseMarkovAutomaton(result.first->template as>()); + result.second = true; } - + + if (generalSettings.isBisimulationSet()) { + result.first = preprocessSparseModelBisimulation(result.first, input, bisimulationSettings); + result.second = true; + } + + return result; + } + template void exportSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { auto ioSettings = storm::settings::getModule(); - + if (ioSettings.isExportExplicitSet()) { storm::api::exportSparseModelAsDrn(model, ioSettings.getExportExplicitFilename(), input.model ? input.model.get().getParameterNames() : std::vector()); } - + if (ioSettings.isExportDotSet()) { storm::api::exportSparseModelAsDot(model, ioSettings.getExportDotFilename()); } @@ -484,7 +285,7 @@ namespace storm { void exportDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { // Intentionally left empty. } - + template void exportModel(std::shared_ptr const& model, SymbolicInput const& input) { if (model->isSparseModel()) { @@ -493,7 +294,7 @@ namespace storm { exportDdModel(model->as>(), input); } } - + template std::shared_ptr> preprocessDdModelBisimulation(std::shared_ptr> const& model, SymbolicInput const& input, storm::settings::modules::BisimulationSettings const& bisimulationSettings) { STORM_LOG_WARN_COND(!bisimulationSettings.isWeakBisimulationSet(), "Weak bisimulation is currently not supported on DDs. Falling back to strong bisimulation."); @@ -519,7 +320,7 @@ namespace storm { template std::pair, bool> preprocessModel(std::shared_ptr const& model, SymbolicInput const& input) { storm::utility::Stopwatch preprocessingWatch(true); - + std::pair, bool> result = std::make_pair(model, false); if (model->isSparseModel()) { result = preprocessSparseModel(result.first->as>(), input); @@ -529,16 +330,17 @@ namespace storm { } preprocessingWatch.stop(); + if (result.second) { STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl); } return result; } - + void printComputingCounterexample(storm::jani::Property const& property) { STORM_PRINT_AND_LOG("Computing counterexample for property " << *property.getRawFormula() << " ..." << std::endl); } - + void printCounterexample(std::shared_ptr const& counterexample, storm::utility::Stopwatch* watch = nullptr) { if (counterexample) { STORM_PRINT_AND_LOG(*counterexample << std::endl); @@ -554,17 +356,17 @@ namespace storm { void generateCounterexamples(std::shared_ptr const& model, SymbolicInput const& input) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Counterexample generation is not supported for this data-type."); } - + template <> void generateCounterexamples(std::shared_ptr const& model, SymbolicInput const& input) { typedef double ValueType; - + STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::NotSupportedException, "Counterexample generation is currently only supported for sparse models."); auto sparseModel = model->as>(); - + STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample is currently only supported for MDPs."); auto mdp = sparseModel->template as>(); - + auto counterexampleSettings = storm::settings::getModule(); if (counterexampleSettings.isMinimalCommandSetGenerationSet()) { STORM_LOG_THROW(input.model && input.model.get().isPrismProgram(), storm::exceptions::NotSupportedException, "Minimal command set counterexamples are only supported for PRISM model input."); @@ -587,7 +389,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The selected counterexample formalism is unsupported."); } } - + template void printFilteredResult(std::unique_ptr const& result, storm::modelchecker::FilterType ft) { if (result->isQuantitative()) { @@ -641,7 +443,7 @@ namespace storm { } STORM_PRINT_AND_LOG(std::endl); } - + void printModelCheckingProperty(storm::jani::Property const& property) { STORM_PRINT_AND_LOG(std::endl << "Model checking property " << *property.getRawFormula() << " ..." << std::endl); } @@ -660,25 +462,25 @@ namespace storm { STORM_PRINT_AND_LOG(" failed, property is unsupported by selected engine/settings." << std::endl); } } - + struct PostprocessingIdentity { void operator()(std::unique_ptr const&) { // Intentionally left empty. } }; - + template void verifyProperties(std::vector const& properties, std::function(std::shared_ptr const& formula, std::shared_ptr const& states)> const& verificationCallback, std::function const&)> const& postprocessingCallback = PostprocessingIdentity()) { - for (auto const& property : properties) { - printModelCheckingProperty(property); - storm::utility::Stopwatch watch(true); - std::unique_ptr result = verificationCallback(property.getRawFormula(), property.getFilter().getStatesFormula()); - watch.stop(); - postprocessingCallback(result); - printResult(result, property, &watch); - } + for (auto const& property : properties) { + printModelCheckingProperty(property); + storm::utility::Stopwatch watch(true); + std::unique_ptr result = verificationCallback(property.getRawFormula(), property.getFilter().getStatesFormula()); + watch.stop(); + postprocessingCallback(result); + printResult(result, property, &watch); } - + } + template void verifyWithAbstractionRefinementEngine(SymbolicInput const& input) { STORM_LOG_ASSERT(input.model, "Expected symbolic model description."); @@ -697,7 +499,7 @@ namespace storm { return storm::api::verifyWithExplorationEngine(input.model.get(), storm::api::createTask(formula, true)); }); } - + template void verifyWithSparseEngine(std::shared_ptr const& model, SymbolicInput const& input) { auto sparseModel = model->as>(); @@ -706,7 +508,7 @@ namespace storm { bool filterForInitialStates = states->isInitialFormula(); auto task = storm::api::createTask(formula, filterForInitialStates); std::unique_ptr result = storm::api::verifyWithSparseEngine(sparseModel, task); - + std::unique_ptr filter; if (filterForInitialStates) { filter = std::make_unique(sparseModel->getInitialStates()); @@ -725,10 +527,10 @@ namespace storm { verifyProperties(input.properties, [&model] (std::shared_ptr const& formula, std::shared_ptr const& states) { bool filterForInitialStates = states->isInitialFormula(); auto task = storm::api::createTask(formula, filterForInitialStates); - + auto symbolicModel = model->as>(); std::unique_ptr result = storm::api::verifyWithHybridEngine(symbolicModel, task); - + std::unique_ptr filter; if (filterForInitialStates) { filter = std::make_unique>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()); @@ -788,11 +590,36 @@ namespace storm { verifySymbolicModel(model, input, coreSettings); } } - + + template + std::shared_ptr buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, storm::settings::modules::CoreSettings::Engine engine) { + auto ioSettings = storm::settings::getModule(); + std::shared_ptr model; + if (!ioSettings.isNoBuildModelSet()) { + model = buildModel(engine, input, ioSettings); + } + + if (model) { + model->printModelInformationToStream(std::cout); + } + + STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model."); + + if (model) { + auto preprocessingResult = preprocessModel(model, input); + if (preprocessingResult.second) { + model = preprocessingResult.first; + model->printModelInformationToStream(std::cout); + } + exportModel(model, input); + } + return model; + } + template void processInputWithValueTypeAndDdlib(SymbolicInput const& input) { auto coreSettings = storm::settings::getModule(); - + // For several engines, no model building step is performed, but the verification is started right away. storm::settings::modules::CoreSettings::Engine engine = coreSettings.getEngine(); if (engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) { @@ -800,43 +627,24 @@ namespace storm { } else if (engine == storm::settings::modules::CoreSettings::Engine::Exploration) { verifyWithExplorationEngine(input); } else { - auto ioSettings = storm::settings::getModule(); - - std::shared_ptr model; - if (!ioSettings.isNoBuildModelSet()) { - model = buildModel(engine, input, ioSettings); - } - - if (model) { - model->printModelInformationToStream(std::cout); - } - - STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model."); - - if (model) { - auto preprocessingResult = preprocessModel(model, input); - if (preprocessingResult.second) { - model = preprocessingResult.first; - model->printModelInformationToStream(std::cout); - } - } - + std::shared_ptr model = buildPreprocessExportModelWithValueTypeAndDdlib(input, engine); + if (model) { - exportModel(model, input); - if (coreSettings.isCounterexampleSet()) { + auto ioSettings = storm::settings::getModule(); generateCounterexamples(model, input); } else { + auto ioSettings = storm::settings::getModule(); verifyModel(model, input, coreSettings); } } } } - + template void processInputWithValueType(SymbolicInput const& input) { auto coreSettings = storm::settings::getModule(); - + if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD) { processInputWithValueTypeAndDdlib(input); } else { @@ -844,53 +652,6 @@ namespace storm { processInputWithValueTypeAndDdlib(input); } } - - void processOptions() { - // Start by setting some urgent options (log levels, resources, etc.) - setUrgentOptions(); - - // Parse and preprocess symbolic input (PRISM, JANI, properties, etc.) - SymbolicInput symbolicInput = parseAndPreprocessSymbolicInput(); - - auto generalSettings = storm::settings::getModule(); - if (generalSettings.isParametricSet()) { -#ifdef STORM_HAVE_CARL - processInputWithValueType(symbolicInput); -#else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build."); -#endif - } else if (generalSettings.isExactSet()) { -#ifdef STORM_HAVE_CARL - processInputWithValueType(symbolicInput); -#else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No exact numbers are supported in this build."); -#endif - } else { - processInputWithValueType(symbolicInput); - } - } - void printTimeAndMemoryStatistics(uint64_t wallclockMilliseconds) { - struct rusage ru; - getrusage(RUSAGE_SELF, &ru); - - std::cout << std::endl << "Performance statistics:" << std::endl; -#ifdef MACOS - // For Mac OS, this is returned in bytes. - uint64_t maximumResidentSizeInMegabytes = ru.ru_maxrss / 1024 / 1024; -#endif -#ifdef LINUX - // For Linux, this is returned in kilobytes. - uint64_t maximumResidentSizeInMegabytes = ru.ru_maxrss / 1024; -#endif - std::cout << " * peak memory usage: " << maximumResidentSizeInMegabytes << "MB" << std::endl; - char oldFillChar = std::cout.fill('0'); - std::cout << " * CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << ru.ru_utime.tv_usec/1000 << "s" << std::endl; - if (wallclockMilliseconds != 0) { - std::cout << " * wallclock time: " << (wallclockMilliseconds/1000) << "." << std::setw(3) << (wallclockMilliseconds % 1000) << "s" << std::endl; - } - std::cout.fill(oldFillChar); - } - - } +} } 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..5fa744c59 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); @@ -306,15 +306,8 @@ namespace storm { if (parSettings.onlyObtainConstraints()) { STORM_LOG_THROW(parSettings.exportResultToFile(), storm::exceptions::InvalidSettingsException, "When computing constraints, export path has to be specified."); - if (model->isOfType(storm::models::ModelType::Dtmc)) { - auto dtmc = model->template as>(); - storm::api::exportParametricResultToFile(boost::none, storm::analysis::ConstraintCollector(*dtmc),parSettings.exportResultPath()); - return; - } else { - STORM_LOG_THROW(parSettings.exportResultToFile(), storm::exceptions::NotImplementedException, "Constraints for MDPs and CTMCs not implemented."); - - } - + storm::api::exportParametricResultToFile(boost::none, storm::analysis::ConstraintCollector(*(model->as>())), parSettings.exportResultPath()); + return; } if (model) { @@ -335,27 +328,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 +339,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/RationalFunctionAdapter.h b/src/storm/adapters/RationalFunctionAdapter.h index ba9858fe0..f403103f5 100644 --- a/src/storm/adapters/RationalFunctionAdapter.h +++ b/src/storm/adapters/RationalFunctionAdapter.h @@ -7,7 +7,6 @@ #include #include #include -#include #include namespace carl { @@ -58,5 +57,5 @@ namespace storm { typedef carl::RationalFunction RationalFunction; typedef carl::Interval Interval; - template using ArithConstraint = carl::SimpleConstraint; } + 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.cpp b/src/storm/analysis/GraphConditions.cpp index bf3beeb0c..be8073bf7 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -1,4 +1,6 @@ +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/Ctmc.h" #include "GraphConditions.h" #include "storm/utility/constants.h" #include "storm/exceptions/NotImplementedException.h" @@ -9,8 +11,8 @@ namespace storm { template - ConstraintCollector::ConstraintCollector(storm::models::sparse::Dtmc const& dtmc) { - process(dtmc); + ConstraintCollector::ConstraintCollector(storm::models::sparse::Model const& model) { + process(model); } template @@ -50,10 +52,12 @@ namespace storm { } template - void ConstraintCollector::process(storm::models::sparse::Dtmc const& dtmc) { - for(uint_fast64_t state = 0; state < dtmc.getNumberOfStates(); ++state) { + void ConstraintCollector::process(storm::models::sparse::Model const& model) { + for(uint_fast64_t action = 0; action < model.getTransitionMatrix().getRowCount(); ++action) { ValueType sum = storm::utility::zero(); - for (auto const& transition : dtmc.getRows(state)) { + + for (auto transitionIt = model.getTransitionMatrix().begin(action); transitionIt != model.getTransitionMatrix().end(action); ++transitionIt) { + auto const& transition = *transitionIt; sum += transition.getValue(); if (!storm::utility::isConstant(transition.getValue())) { auto const& transitionVars = transition.getValue().gatherVariables(); @@ -90,9 +94,17 @@ namespace storm { // Assert: sum == 1 wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomialWithCoefficient(), storm::CompareRelation::EQ); } + } + if (model.getType() == storm::models::ModelType::Ctmc) { + auto const& exitRateVector = static_cast const&>(model).getExitRateVector(); + wellformedRequiresNonNegativeEntries(exitRateVector); + } else if (model.getType() == storm::models::ModelType::MarkovAutomaton) { + auto const& exitRateVector = static_cast const&>(model).getExitRates(); + wellformedRequiresNonNegativeEntries(exitRateVector); } - for(auto const& rewModelEntry : dtmc.getRewardModels()) { + + for(auto const& rewModelEntry : model.getRewardModels()) { if (rewModelEntry.second.hasStateRewards()) { wellformedRequiresNonNegativeEntries(rewModelEntry.second.getStateRewardVector()); } @@ -117,13 +129,13 @@ namespace storm { } } } - } + } template - void ConstraintCollector::operator()(storm::models::sparse::Dtmc const& dtmc) { - process(dtmc); + void ConstraintCollector::operator()(storm::models::sparse::Model const& model) { + process(model); } template class ConstraintCollector; diff --git a/src/storm/analysis/GraphConditions.h b/src/storm/analysis/GraphConditions.h index 48b4aee64..a901dfa68 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; @@ -38,12 +38,12 @@ namespace storm { void wellformedRequiresNonNegativeEntries(std::vector const&); public: /*! - * Constructs a constraint collector for the given DTMC. The constraints are built and ready for + * Constructs a constraint collector for the given Model. The constraints are built and ready for * retrieval after the construction. * - * @param dtmc The DTMC for which to create the constraints. + * @param model The Model for which to create the constraints. */ - ConstraintCollector(storm::models::sparse::Dtmc const& dtmc); + ConstraintCollector(storm::models::sparse::Model const& model); /*! * Returns the set of wellformed-ness constraints. @@ -66,18 +66,18 @@ namespace storm { std::set const& getVariables() const; /*! - * Constructs the constraints for the given DTMC. + * Constructs the constraints for the given Model. * - * @param dtmc The DTMC for which to create the constraints. + * @param model The DTMC for which to create the constraints. */ - void process(storm::models::sparse::Dtmc const& dtmc); + void process(storm::models::sparse::Model const& model); /*! - * Constructs the constraints for the given DTMC by calling the process method. + * Constructs the constraints for the given Model by calling the process method. * - * @param dtmc The DTMC for which to create the constraints. + * @param model The Model for which to create the constraints. */ - void operator()(storm::models::sparse::Dtmc const& dtmc); + void operator()(storm::models::sparse::Model const& model); }; diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index 1be905837..715e6e1ac 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" @@ -34,12 +30,12 @@ namespace storm { namespace api { template - std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas) { + std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool buildFullModel = false) { if (model.isPrismProgram()) { typename storm::builder::DdPrismModelBuilder::Options options; options = typename storm::builder::DdPrismModelBuilder::Options(formulas); - if (storm::settings::getModule().isBuildFullModelSet()) { + if (buildFullModel) { options.buildAllLabels = true; options.buildAllRewardModels = true; } @@ -51,7 +47,7 @@ namespace storm { typename storm::builder::DdJaniModelBuilder::Options options; options = typename storm::builder::DdJaniModelBuilder::Options(formulas); - if (storm::settings::getModule().isBuildFullModelSet()) { + if (buildFullModel) { options.buildAllLabels = true; options.buildAllRewardModels = true; } @@ -62,39 +58,28 @@ namespace storm { } template<> - inline std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas) { + inline std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool buildFullModel) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "CUDD does not support rational numbers."); } template<> - inline std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas) { + inline std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool buildFullModel) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "CUDD does not support rational functions."); } 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; @@ -109,6 +94,12 @@ 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) { @@ -157,6 +148,5 @@ namespace storm { return storm::parser::ImcaMarkovAutomatonParser::parseImcaFile(imcaFile); } - } } 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/models/sparse/Mdp.cpp b/src/storm/models/sparse/Mdp.cpp index 38226702d..081940600 100644 --- a/src/storm/models/sparse/Mdp.cpp +++ b/src/storm/models/sparse/Mdp.cpp @@ -37,27 +37,7 @@ namespace storm { // Intentionally left empty } - template - Mdp Mdp::restrictChoices(storm::storage::BitVector const& enabledChoices) const { - storm::storage::sparse::ModelComponents newComponents(this->getTransitionMatrix().restrictRows(enabledChoices)); - newComponents.stateLabeling = this->getStateLabeling(); - for (auto const& rewardModel : this->getRewardModels()) { - newComponents.rewardModels.emplace(rewardModel.first, rewardModel.second.restrictActions(enabledChoices)); - } - if (this->hasChoiceLabeling()) { - newComponents.choiceLabeling = this->getChoiceLabeling().getSubLabeling(enabledChoices); - } - newComponents.stateValuations = this->getOptionalStateValuations(); - if (this->hasChoiceOrigins()) { - newComponents.choiceOrigins = this->getChoiceOrigins()->selectChoices(enabledChoices); - } - return Mdp(std::move(newComponents)); - } - template - uint_least64_t Mdp::getChoiceIndex(storm::storage::StateActionPair const& stateactPair) const { - return this->getNondeterministicChoiceIndices()[stateactPair.getState()]+stateactPair.getAction(); - } template class Mdp; diff --git a/src/storm/models/sparse/Mdp.h b/src/storm/models/sparse/Mdp.h index e65770275..9e5ea7509 100644 --- a/src/storm/models/sparse/Mdp.h +++ b/src/storm/models/sparse/Mdp.h @@ -1,9 +1,7 @@ #ifndef STORM_MODELS_SPARSE_MDP_H_ #define STORM_MODELS_SPARSE_MDP_H_ -#include "storm/storage/StateActionPair.h" #include "storm/models/sparse/NondeterministicModel.h" -#include "storm/utility/OsDetection.h" namespace storm { namespace models { @@ -50,19 +48,6 @@ namespace storm { Mdp(Mdp&& other) = default; Mdp& operator=(Mdp&& other) = default; - - /*! - * Constructs an MDP by copying the current MDP and restricting the choices of each state to the ones given by the bitvector. - * - * @param enabledActions A BitVector of lenght numberOfChoices(), which is one iff the action should be kept. - * @return A subMDP. - */ - Mdp restrictChoices(storm::storage::BitVector const& enabledActions) const; - - /*! - * For a state/action pair, get the choice index referring to the state-action pair. - */ - uint_fast64_t getChoiceIndex(storm::storage::StateActionPair const& stateactPair) const; }; } // namespace sparse diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index 3382bfd95..acdbd3885 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -185,7 +185,12 @@ namespace storm { outStream << "}" << std::endl; } } - + + template + uint_least64_t NondeterministicModel::getChoiceIndex(storm::storage::StateActionPair const& stateactPair) const { + return this->getNondeterministicChoiceIndices()[stateactPair.getState()]+stateactPair.getAction(); + } + template class NondeterministicModel; #ifdef STORM_HAVE_CARL diff --git a/src/storm/models/sparse/NondeterministicModel.h b/src/storm/models/sparse/NondeterministicModel.h index ab0a21a04..dd1335718 100644 --- a/src/storm/models/sparse/NondeterministicModel.h +++ b/src/storm/models/sparse/NondeterministicModel.h @@ -2,7 +2,7 @@ #define STORM_MODELS_SPARSE_NONDETERMINISTICMODEL_H_ #include "storm/models/sparse/Model.h" -#include "storm/utility/OsDetection.h" +#include "storm/storage/StateActionPair.h" namespace storm { @@ -54,7 +54,11 @@ namespace storm { uint_fast64_t getNumberOfChoices(uint_fast64_t state) const; virtual void reduceToStateBasedRewards() override; - + + /*! + * For a state/action pair, get the choice index referring to the state-action pair. + */ + uint_fast64_t getChoiceIndex(storm::storage::StateActionPair const& stateactPair) const; /*! * Applies the given scheduler to this model. * @param scheduler the considered scheduler. diff --git a/src/storm/permissivesched/PermissiveSchedulers.h b/src/storm/permissivesched/PermissiveSchedulers.h index eb09d4b24..cc29f7113 100644 --- a/src/storm/permissivesched/PermissiveSchedulers.h +++ b/src/storm/permissivesched/PermissiveSchedulers.h @@ -2,6 +2,7 @@ #ifndef PERMISSIVESCHEDULERS_H #define PERMISSIVESCHEDULERS_H +#include #include "../logic/ProbabilityOperatorFormula.h" #include "../models/sparse/Mdp.h" #include "../models/sparse/StandardRewardModel.h" @@ -38,7 +39,8 @@ namespace storm { storm::models::sparse::Mdp apply() const { - return mdp.restrictChoices(enabledChoices); + storm::transformer::ChoiceSelector cs(mdp); + return *(cs.transform(enabledChoices)->template as>()); } template diff --git a/src/storm/settings/Argument.cpp b/src/storm/settings/Argument.cpp index ddb39c0ab..555bcdb9d 100644 --- a/src/storm/settings/Argument.cpp +++ b/src/storm/settings/Argument.cpp @@ -12,12 +12,12 @@ namespace storm { namespace settings { template - Argument::Argument(std::string const& name, std::string const& description, std::vector>> const& validators): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType()), validators(validators), isOptional(false), defaultValue(), hasDefaultValue(false) { + Argument::Argument(std::string const& name, std::string const& description, std::vector>> const& validators): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType()), validators(validators), isOptional(false), defaultValue(), hasDefaultValue(false), wasSetFromDefaultValueFlag(false) { // Intentionally left empty. } template - Argument::Argument(std::string const& name, std::string const& description, std::vector>> const& validators, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType()), validators(validators), isOptional(isOptional), defaultValue(), hasDefaultValue(true) { + Argument::Argument(std::string const& name, std::string const& description, std::vector>> const& validators, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType()), validators(validators), isOptional(isOptional), defaultValue(), hasDefaultValue(true), wasSetFromDefaultValueFlag(false) { this->setDefaultValue(defaultValue); } @@ -71,6 +71,12 @@ namespace storm { STORM_LOG_THROW(this->hasDefaultValue, storm::exceptions::IllegalFunctionCallException, "Unable to set value from default value, because the argument " << name << " has none."); bool result = this->setFromTypeValue(this->defaultValue, false); STORM_LOG_THROW(result, storm::exceptions::IllegalArgumentValueException, "Unable to assign default value to argument " << name << ", because it was rejected."); + this->wasSetFromDefaultValueFlag = true; + } + + template + bool Argument::wasSetFromDefaultValue() const { + return wasSetFromDefaultValueFlag; } template diff --git a/src/storm/settings/Argument.h b/src/storm/settings/Argument.h index 080d06409..2074557cf 100644 --- a/src/storm/settings/Argument.h +++ b/src/storm/settings/Argument.h @@ -85,6 +85,8 @@ namespace storm { void setFromDefaultValue() override; + virtual bool wasSetFromDefaultValue() const override; + virtual std::string getValueAsString() const override; virtual int_fast64_t getValueAsInteger() const override; @@ -116,6 +118,9 @@ namespace storm { // A flag indicating whether a default value has been provided. bool hasDefaultValue; + // A flag indicating whether the argument was set from the default value. + bool wasSetFromDefaultValueFlag; + /*! * Sets the default value of the argument to the provided value. * diff --git a/src/storm/settings/ArgumentBase.h b/src/storm/settings/ArgumentBase.h index 6808bd815..b48a46183 100644 --- a/src/storm/settings/ArgumentBase.h +++ b/src/storm/settings/ArgumentBase.h @@ -80,6 +80,8 @@ namespace storm { */ virtual void setFromDefaultValue() = 0; + virtual bool wasSetFromDefaultValue() const = 0; + /*! * Tries to set the value of the argument from the given string. * @@ -134,7 +136,7 @@ namespace storm { friend std::ostream& operator<<(std::ostream& out, ArgumentBase const& argument); - protected: + protected: // A flag indicating whether the argument has been set. bool hasBeenSet; diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 493ea71a2..e38c5daf2 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -271,7 +271,7 @@ namespace storm { return moduleIterator->second->getPrintLengthOfLongestOption(); } - void SettingsManager::addModule(std::unique_ptr&& moduleSettings) { + void SettingsManager::addModule(std::unique_ptr&& moduleSettings, bool doRegister) { auto moduleIterator = this->modules.find(moduleSettings->getModuleName()); STORM_LOG_THROW(moduleIterator == this->modules.end(), storm::exceptions::IllegalFunctionCallException, "Unable to register module '" << moduleSettings->getModuleName() << "' because a module with the same name already exists."); @@ -281,12 +281,15 @@ namespace storm { this->modules.emplace(moduleSettings->getModuleName(), std::move(moduleSettings)); auto iterator = this->modules.find(moduleName); std::unique_ptr const& settings = iterator->second; - - // Now register the options of the module. - this->moduleOptions.emplace(moduleName, std::vector>()); - for (auto const& option : settings->getOptions()) { - this->addOption(option); + + if (doRegister) { + // Now register the options of the module. + this->moduleOptions.emplace(moduleName, std::vector>()); + for (auto const& option : settings->getOptions()) { + this->addOption(option); + } } + } void SettingsManager::addOption(std::shared_ptr