Browse Source

Merge branch 'master' into reward-bounded-multi-objective

main
TimQu 8 years ago
parent
commit
5025b33aac
  1. 4
      .gitignore
  2. 296
      .travis.yml
  3. 1
      CHANGELOG.md
  4. 18
      README.md
  5. 2
      resources/3rdparty/CMakeLists.txt
  6. 4
      resources/3rdparty/carl/CMakeLists.txt
  7. 1
      src/CMakeLists.txt
  8. 40
      src/storm-cli-utilities/CMakeLists.txt
  9. 32
      src/storm-cli-utilities/cli.cpp
  10. 0
      src/storm-cli-utilities/cli.h
  11. 2
      src/storm-dft-cli/CMakeLists.txt
  12. 4
      src/storm-dft-cli/storm-dyftee.cpp
  13. 2
      src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
  14. 8
      src/storm-dft/storage/dft/OrderDFTElementsById.cpp
  15. 2
      src/storm-gspn-cli/CMakeLists.txt
  16. 4
      src/storm-gspn-cli/storm-gspn.cpp
  17. 29
      src/storm-pars-cli/storm-pars.cpp
  18. 13
      src/storm-pars/transformer/SparseParametricModelSimplifier.cpp
  19. 2
      src/storm-pgcl-cli/CMakeLists.txt
  20. 2
      src/storm-pgcl-cli/storm-pgcl.cpp
  21. 2
      src/storm/CMakeLists.txt
  22. 26
      src/storm/adapters/Smt2ExpressionAdapter.h
  23. 2
      src/storm/analysis/GraphConditions.h
  24. 29
      src/storm/api/builder.h
  25. 8
      src/storm/builder/BuilderOptions.cpp
  26. 59
      src/storm/builder/BuilderOptions.h
  27. 27
      src/storm/solver/SmtlibSmtSolver.cpp
  28. 8
      src/storm/solver/SmtlibSmtSolver.h
  29. 4
      src/storm/storage/expressions/Variable.h
  30. 2
      src/storm/storm.cpp
  31. 164
      travis/build-helper.sh
  32. 71
      travis/build.sh
  33. 16
      travis/dockerfiles/Dockerfile.debian-9
  34. 8
      travis/dockerfiles/Dockerfile.storm
  35. 17
      travis/dockerfiles/Dockerfile.ubuntu-16.10
  36. 9
      travis/dockerfiles/build_carl.sh
  37. 9
      travis/dockerfiles/build_docker.sh
  38. 9
      travis/dockerfiles/build_storm.sh
  39. 123
      travis/generate_travis.py
  40. 11
      travis/install_linux.sh
  41. 73
      travis/install_osx.sh
  42. 4
      travis/mtime_cache/globs.txt
  43. 178
      travis/mtime_cache/mtime_cache.rb

4
.gitignore

@ -52,3 +52,7 @@ nbproject/
*.out *.out
resources/3rdparty/cudd-3.0.0/Makefile.in resources/3rdparty/cudd-3.0.0/Makefile.in
resources/3rdparty/cudd-3.0.0/aclocal.m4 resources/3rdparty/cudd-3.0.0/aclocal.m4
# Python config
stormpy/setup.cfg
# Travis helpers
travis/mtime_cache/cache.json

296
.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 {} \;

1
CHANGELOG.md

@ -6,7 +6,6 @@ The releases of major and minor versions contain an overview of changes since th
Version 1.1.x 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) ### Version 1.1.0 (2017/8)

18
README.md

@ -1,22 +1,22 @@
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 Benchmarks
---------------------------- ----------------------------
Example input files for storm can be obtained from
Example input files for Storm can be obtained from
https://github.com/moves-rwth/storm-examples. https://github.com/moves-rwth/storm-examples.
Running make example-files automatically obtains these files.
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): * **Prism files** (DTMC, MDP, CTMC):
http://www.prismmodelchecker.org/benchmarks/
http://www.prismmodelchecker.org/benchmarks
* **Jani files** (DTMC, MDP, CTMC, MA): * **Jani files** (DTMC, MDP, CTMC, MA):
http://jani-spec.org/
http://jani-spec.org
* **GSPN**s: * **GSPN**s:
(private, contact: sebastian.junges@cs.rwth-aachen.de) (private, contact: sebastian.junges@cs.rwth-aachen.de)
* **DFT**s: * **DFT**s:
@ -31,8 +31,8 @@ Storm has been developed at RWTH Aachen University.
###### Principal developers ###### Principal developers
* Christian Dehnert * Christian Dehnert
* Joost-Pieter Katoen
* Sebastian Junges * Sebastian Junges
* Joost-Pieter Katoen
* Matthias Volk * Matthias Volk
###### Developers (lexicographical order) ###### Developers (lexicographical order)

2
resources/3rdparty/CMakeLists.txt

@ -200,7 +200,7 @@ include(${STORM_3RDPARTY_SOURCE_DIR}/include_cudd.cmake)
set(STORM_HAVE_CARL OFF) set(STORM_HAVE_CARL OFF)
set(CARL_MINYEAR 17) set(CARL_MINYEAR 17)
set(CARL_MINMONTH 06)
set(CARL_MINMONTH 08)
set(CARL_MINPATCH 0) set(CARL_MINPATCH 0)
if(USE_CARL) if(USE_CARL)
if (NOT STORM_FORCE_SHIPPED_CARL) if (NOT STORM_FORCE_SHIPPED_CARL)

4
resources/3rdparty/carl/CMakeLists.txt

@ -8,11 +8,11 @@ message(STORM_3RDPARTY_BINARY_DIR: ${STORM_3RDPARTY_BINARY_DIR})
ExternalProject_Add(carl-config ExternalProject_Add(carl-config
GIT_REPOSITORY https://github.com/smtrat/carl GIT_REPOSITORY https://github.com/smtrat/carl
GIT_TAG master
GIT_TAG 17.08
PREFIX here PREFIX here
SOURCE_DIR source_dir SOURCE_DIR source_dir
BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/carl 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 BUILD_IN_SOURCE 0
LOG_UPDATE OFF LOG_UPDATE OFF
LOG_CONFIGURE OFF LOG_CONFIGURE OFF

1
src/CMakeLists.txt

@ -5,6 +5,7 @@ set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
add_custom_target(binaries) add_custom_target(binaries)
add_subdirectory(storm) add_subdirectory(storm)
add_subdirectory(storm-cli-utilities)
add_subdirectory(storm-pgcl) add_subdirectory(storm-pgcl)
add_subdirectory(storm-pgcl-cli) add_subdirectory(storm-pgcl-cli)
add_subdirectory(storm-gspn) add_subdirectory(storm-gspn)

40
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)

32
src/storm/cli/cli.cpp → 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/storage/SymbolicModelDescription.h"
#include "storm/models/ModelBase.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/exceptions/OptionParserException.h"
#include "storm/settings/modules/ResourceSettings.h"
#include "storm/settings/modules/JaniExportSettings.h"
#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
#include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/symbolic/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/resources.h"
#include "storm/utility/file.h" #include "storm/utility/file.h"
#include "storm/utility/storm-version.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/initialize.h"
#include "storm/utility/Stopwatch.h" #include "storm/utility/Stopwatch.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/ResourceSettings.h"
#include <type_traits> #include <type_traits>
#include "storm/api/storm.h" #include "storm/api/storm.h"
#include "storm/utility/macros.h"
// Includes for the linked libraries and versions header. // Includes for the linked libraries and versions header.
#ifdef STORM_HAVE_INTELTBB #ifdef STORM_HAVE_INTELTBB
@ -370,7 +370,15 @@ namespace storm {
template <typename ValueType> template <typename ValueType>
std::shared_ptr<storm::models::ModelBase> buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { std::shared_ptr<storm::models::ModelBase> buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) {
auto counterexampleGeneratorSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>(); auto counterexampleGeneratorSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
return storm::api::buildSparseModel<ValueType>(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<ValueType>(input.model.get(), options, ioSettings.isJitSet(), storm::settings::getModule<storm::settings::modules::JitBuilderSettings>().isDoctorSet());
} }
template <typename ValueType> template <typename ValueType>

0
src/storm/cli/cli.h → src/storm-cli-utilities/cli.h

2
src/storm-dft-cli/CMakeLists.txt

@ -1,6 +1,6 @@
# Create storm-dft. # Create storm-dft.
add_executable(storm-dft-cli ${PROJECT_SOURCE_DIR}/src/storm-dft-cli/storm-dyftee.cpp) 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") set_target_properties(storm-dft-cli PROPERTIES OUTPUT_NAME "storm-dft")
add_dependencies(binaries storm-dft-cli) add_dependencies(binaries storm-dft-cli)

4
src/storm-dft-cli/storm-dyftee.cpp

@ -1,12 +1,12 @@
#include "storm/logic/Formula.h" #include "storm/logic/Formula.h"
#include "storm/utility/initialize.h" #include "storm/utility/initialize.h"
#include "storm/api/storm.h" #include "storm/api/storm.h"
#include "storm/cli/cli.h"
#include "storm-cli-utilities/cli.h"
#include "storm/exceptions/BaseException.h" #include "storm/exceptions/BaseException.h"
#include "storm/logic/Formula.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/CoreSettings.h"
#include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/DebugSettings.h"
#include "storm/settings/modules/GmmxxEquationSolverSettings.h" #include "storm/settings/modules/GmmxxEquationSolverSettings.h"

2
src/storm-dft/modelchecker/dft/DFTModelChecker.cpp

@ -1,5 +1,6 @@
#include "DFTModelChecker.h" #include "DFTModelChecker.h"
#include "storm/settings/modules/IOSettings.h"
#include "storm/builder/ParallelCompositionBuilder.h" #include "storm/builder/ParallelCompositionBuilder.h"
#include "storm/utility/bitoperations.h" #include "storm/utility/bitoperations.h"
#include "storm/utility/DirectEncodingExporter.h" #include "storm/utility/DirectEncodingExporter.h"
@ -357,6 +358,7 @@ namespace storm {
explorationTimer.stop(); explorationTimer.stop();
// Export the model if required // Export the model if required
// TODO move this outside of the model checker?
if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet()) { if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet()) {
std::ofstream stream; std::ofstream stream;
storm::utility::openFile(storm::settings::getModule<storm::settings::modules::IOSettings>().getExportExplicitFilename(), stream); storm::utility::openFile(storm::settings::getModule<storm::settings::modules::IOSettings>().getExportExplicitFilename(), stream);

8
src/storm-dft/storage/dft/OrderDFTElementsById.cpp

@ -22,12 +22,12 @@ namespace storm {
// Explicitly instantiate the class. // Explicitly instantiate the class.
template class OrderElementsById<double>;
template class OrderElementsByRank<double>;
template struct OrderElementsById<double>;
template struct OrderElementsByRank<double>;
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template class OrderElementsById<RationalFunction>;
template class OrderElementsByRank<RationalFunction>;
template struct OrderElementsById<RationalFunction>;
template struct OrderElementsByRank<RationalFunction>;
#endif #endif
} }
} }

2
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) 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") set_target_properties(storm-gspn-cli PROPERTIES OUTPUT_NAME "storm-gspn")
add_dependencies(binaries storm-gspn-cli) add_dependencies(binaries storm-gspn-cli)

4
src/storm-gspn-cli/storm-gspn.cpp

@ -12,7 +12,7 @@
#include "storm/utility/initialize.h" #include "storm/utility/initialize.h"
#include "api/storm.h" #include "api/storm.h"
#include "storm/cli/cli.h"
#include "storm-cli-utilities/cli.h"
#include "storm/parser/FormulaParser.h" #include "storm/parser/FormulaParser.h"
@ -27,7 +27,7 @@
#include "storm/exceptions/FileIoException.h" #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/GSPNSettings.h"
#include "storm/settings/modules/GSPNExportSettings.h" #include "storm/settings/modules/GSPNExportSettings.h"
#include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/CoreSettings.h"

29
src/storm-pars-cli/storm-pars.cpp

@ -6,7 +6,7 @@
#include "storm/settings/SettingsManager.h" #include "storm/settings/SettingsManager.h"
#include "storm/api/storm.h" #include "storm/api/storm.h"
#include "storm/cli/cli.h"
#include "storm-cli-utilities/cli.h"
#include "storm/models/ModelBase.h" #include "storm/models/ModelBase.h"
#include "storm/storage/SymbolicModelDescription.h" #include "storm/storage/SymbolicModelDescription.h"
#include "storm/utility/file.h" #include "storm/utility/file.h"
@ -23,7 +23,7 @@
#include "storm/exceptions/InvalidSettingsException.h" #include "storm/exceptions/InvalidSettingsException.h"
#include "storm/exceptions/NotSupportedException.h" #include "storm/exceptions/NotSupportedException.h"
#include "storm/cli/cli.cpp"
#include "storm-cli-utilities/cli.cpp"
namespace storm { namespace storm {
namespace pars { namespace pars {
@ -336,7 +336,16 @@ namespace storm {
processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalFunction>(symbolicInput); processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalFunction>(symbolicInput);
} }
int64_t process(const int argc, const char** argv) {
}
}
/*!
* Main entry point of the executable storm-pars.
*/
int main(const int argc, const char** argv) {
try {
storm::utility::setUp(); storm::utility::setUp();
storm::cli::printHeader("Storm-pars", argc, argv); storm::cli::printHeader("Storm-pars", argc, argv);
storm::settings::initializeParsSettings("Storm-pars", "storm-pars"); storm::settings::initializeParsSettings("Storm-pars", "storm-pars");
@ -346,7 +355,7 @@ namespace storm {
return -1; return -1;
} }
processOptions();
storm::pars::processOptions();
totalTimer.stop(); totalTimer.stop();
if (storm::settings::getModule<storm::settings::modules::ResourceSettings>().isPrintTimeAndMemorySet()) { if (storm::settings::getModule<storm::settings::modules::ResourceSettings>().isPrintTimeAndMemorySet()) {
@ -355,18 +364,6 @@ namespace storm {
storm::utility::cleanUp(); storm::utility::cleanUp();
return 0; return 0;
}
}
}
/*!
* Main entry point of the executable storm-pars.
*/
int main(const int argc, const char** argv) {
try {
return storm::pars::process(argc, argv);
} catch (storm::exceptions::BaseException const& exception) { } catch (storm::exceptions::BaseException const& exception) {
STORM_LOG_ERROR("An exception caused Storm-pars to terminate. The message of the exception is: " << exception.what()); STORM_LOG_ERROR("An exception caused Storm-pars to terminate. The message of the exception is: " << exception.what());
return 1; return 1;

13
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. // 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; return false;
} }
@ -63,8 +63,8 @@ namespace storm {
template<typename SparseModelType> template<typename SparseModelType>
bool SparseParametricModelSimplifier<SparseModelType>::simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { bool SparseParametricModelSimplifier<SparseModelType>::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; return false;
} }
@ -77,21 +77,21 @@ namespace storm {
template<typename SparseModelType> template<typename SparseModelType>
bool SparseParametricModelSimplifier<SparseModelType>::simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { bool SparseParametricModelSimplifier<SparseModelType>::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); STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula);
return false; return false;
} }
template<typename SparseModelType> template<typename SparseModelType>
bool SparseParametricModelSimplifier<SparseModelType>::simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula) { bool SparseParametricModelSimplifier<SparseModelType>::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); STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula);
return false; return false;
} }
template<typename SparseModelType> template<typename SparseModelType>
bool SparseParametricModelSimplifier<SparseModelType>::simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula) { bool SparseParametricModelSimplifier<SparseModelType>::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); STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula);
return false; return false;
} }
@ -100,7 +100,6 @@ namespace storm {
std::shared_ptr<SparseModelType> SparseParametricModelSimplifier<SparseModelType>::eliminateConstantDeterministicStates(SparseModelType const& model, storm::storage::BitVector const& consideredStates, boost::optional<std::string> const& rewardModelName) { std::shared_ptr<SparseModelType> SparseParametricModelSimplifier<SparseModelType>::eliminateConstantDeterministicStates(SparseModelType const& model, storm::storage::BitVector const& consideredStates, boost::optional<std::string> const& rewardModelName) {
storm::storage::SparseMatrix<typename SparseModelType::ValueType> const& sparseMatrix = model.getTransitionMatrix(); storm::storage::SparseMatrix<typename SparseModelType::ValueType> const& sparseMatrix = model.getTransitionMatrix();
// get the action-based reward values // get the action-based reward values
std::vector<typename SparseModelType::ValueType> actionRewards; std::vector<typename SparseModelType::ValueType> actionRewards;
if(rewardModelName) { if(rewardModelName) {

2
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) 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") set_target_properties(storm-pgcl-cli PROPERTIES OUTPUT_NAME "storm-pgcl")
# installation # installation

2
src/storm-pgcl-cli/storm-pgcl.cpp

@ -2,7 +2,7 @@
#include "logic/Formula.h" #include "logic/Formula.h"
#include "utility/initialize.h" #include "utility/initialize.h"
#include "storm/cli/cli.h"
#include "storm-cli-utilities/cli.h"
#include "storm/exceptions/BaseException.h" #include "storm/exceptions/BaseException.h"
#include "storm/utility/macros.h" #include "storm/utility/macros.h"
#include <boost/lexical_cast.hpp> #include <boost/lexical_cast.hpp>

2
src/storm/CMakeLists.txt

@ -49,7 +49,7 @@ set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
# Create storm. # Create storm.
add_executable(storm-main ${STORM_MAIN_SOURCES} ${STORM_MAIN_HEADERS}) 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") set_target_properties(storm-main PROPERTIES OUTPUT_NAME "storm")
# Install storm headers to include directory. # Install storm headers to include directory.

26
src/storm/adapters/Smt2ExpressionAdapter.h

@ -39,7 +39,6 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); 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. * Translates the given constraint "leftHandSide relation rightHandSide" to an equivalent expression for Smt2.
@ -61,20 +60,6 @@ namespace storm {
")"; ")";
} }
/*!
* 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<storm::RawPolynomial> 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. * Translates the given constraint "leftHandSide relation 0" to an equivalent expression for Smt2.
@ -82,16 +67,16 @@ namespace storm {
* @param constraint * @param constraint
* @return An equivalent expression for Smt2. * @return An equivalent expression for Smt2.
*/ */
std::string translateExpression(storm::ArithConstraint<storm::Polynomial> const& constraint) {
std::string translateExpression(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation) {
std::stringstream ss; std::stringstream ss;
ss << "(" << constraint.rel() << " " <<
constraint.lhs().toString(false, useReadableVarNames) << " " <<
ss << "(" << relation << " " <<
leftHandSide.toString(false, useReadableVarNames) << " " <<
"0 " << "0 " <<
")"; ")";
return ss.str(); return ss.str();
} }
#endif
/*! /*!
* Translates the given variable to an equivalent expression for Smt2. * 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 /*! Checks whether the variables in the given set are already declared and creates them if necessary
* @param variables the set of variables to check * @param variables the set of variables to check
*/ */
@ -167,7 +152,6 @@ namespace storm {
} }
return result; return result;
} }
#endif
private: private:
// The manager that can be used to build expressions. // The manager that can be used to build expressions.

2
src/storm/analysis/GraphConditions.h

@ -11,7 +11,7 @@ namespace storm {
template <typename ValueType, typename Enable=void> template <typename ValueType, typename Enable=void>
struct ConstraintType { struct ConstraintType {
typedef storm::ArithConstraint<ValueType> val;
typedef void* val;
}; };
template<typename ValueType> template<typename ValueType>

29
src/storm/api/builder.h

@ -23,10 +23,6 @@
#include "storm/builder/ExplicitModelBuilder.h" #include "storm/builder/ExplicitModelBuilder.h"
#include "storm/builder/jit/ExplicitJitJaniModelBuilder.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/utility/macros.h"
#include "storm/exceptions/NotSupportedException.h" #include "storm/exceptions/NotSupportedException.h"
@ -62,24 +58,13 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool buildChoiceLabels = false, bool buildChoiceOrigins = false, bool buildStateValuations = false) {
storm::builder::BuilderOptions options(formulas);
if (storm::settings::getModule<storm::settings::modules::IOSettings>().isBuildFullModelSet()) {
options.setBuildAllLabels();
options.setBuildAllRewardModels();
options.clearTerminalStates();
}
options.setBuildChoiceLabels(buildChoiceLabels);
options.setBuildChoiceOrigins(buildChoiceOrigins);
options.setBuildStateValuations(buildStateValuations);
if (storm::settings::getModule<storm::settings::modules::IOSettings>().isJitSet()) {
std::shared_ptr<storm::models::sparse::Model<ValueType>> 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_LOG_THROW(model.isJaniModel(), storm::exceptions::NotSupportedException, "Cannot use JIT-based model builder for non-JANI model.");
storm::builder::jit::ExplicitJitJaniModelBuilder<ValueType> builder(model.asJaniModel(), options); storm::builder::jit::ExplicitJitJaniModelBuilder<ValueType> builder(model.asJaniModel(), options);
if (storm::settings::getModule<storm::settings::modules::JitBuilderSettings>().isDoctorSet()) {
if (doctor) {
bool result = builder.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_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."); STORM_LOG_INFO("The JIT-based model builder seems to be working.");
@ -100,6 +85,14 @@ namespace storm {
} }
} }
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool jit = false, bool doctor = false) {
storm::builder::BuilderOptions options(formulas);
return buildSparseModel<ValueType>(model, options, jit, doctor);
}
template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>> template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> buildSparseModel(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components) { std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> buildSparseModel(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components) {
switch (modelType) { switch (modelType) {

8
src/storm/builder/BuilderOptions.cpp

@ -157,8 +157,8 @@ namespace storm {
return buildAllLabels; return buildAllLabels;
} }
BuilderOptions& BuilderOptions::setBuildAllRewardModels() {
buildAllRewardModels = true;
BuilderOptions& BuilderOptions::setBuildAllRewardModels(bool newValue) {
buildAllRewardModels = newValue;
return *this; return *this;
} }
@ -185,8 +185,8 @@ namespace storm {
return *this; return *this;
} }
BuilderOptions& BuilderOptions::setBuildAllLabels() {
buildAllLabels = true;
BuilderOptions& BuilderOptions::setBuildAllLabels(bool newValue) {
buildAllLabels = newValue;
return *this; return *this;
} }

59
src/storm/builder/BuilderOptions.h

@ -82,8 +82,20 @@ namespace storm {
*/ */
void setTerminalStatesFromFormula(storm::logic::Formula const& formula); void setTerminalStatesFromFormula(storm::logic::Formula const& formula);
/*!
* Which reward models are built
* @return
*/
std::vector<std::string> const& getRewardModelNames() const; std::vector<std::string> const& getRewardModelNames() const;
/*!
* Which labels are built
* @return
*/
std::set<std::string> const& getLabelNames() const; std::set<std::string> const& getLabelNames() const;
/*!
* Which expression labels are built
* @return
*/
std::vector<storm::expressions::Expression> const& getExpressionLabels() const; std::vector<storm::expressions::Expression> const& getExpressionLabels() const;
std::vector<std::pair<LabelOrExpression, bool>> const& getTerminalStates() const; std::vector<std::pair<LabelOrExpression, bool>> const& getTerminalStates() const;
bool hasTerminalStates() const; bool hasTerminalStates() const;
@ -97,17 +109,52 @@ namespace storm {
bool isExplorationShowProgressSet() const; bool isExplorationShowProgressSet() const;
uint64_t getExplorationShowProgressDelay() 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& 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(storm::expressions::Expression const& expression);
BuilderOptions& addLabel(std::string const& labelName); BuilderOptions& addLabel(std::string const& labelName);
BuilderOptions& addTerminalExpression(storm::expressions::Expression const& expression, bool value); BuilderOptions& addTerminalExpression(storm::expressions::Expression const& expression, bool value);
BuilderOptions& addTerminalLabel(std::string const& label, 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: private:
/// A flag that indicates whether all reward models are to be built. In this case, the reward model names are /// A flag that indicates whether all reward models are to be built. In this case, the reward model names are

27
src/storm/solver/SmtlibSmtSolver.cpp

@ -102,33 +102,6 @@ namespace storm {
writeCommand("( assert " + expressionAdapter->translateExpression(leftHandSide, relation, rightHandSide) + " )", true); writeCommand("( assert " + expressionAdapter->translateExpression(leftHandSide, relation, rightHandSide) + " )", true);
} }
void SmtlibSmtSolver::add(storm::ArithConstraint<storm::RationalFunction> const& constraint) {
add(constraint.lhs(), constraint.rel());
}
void SmtlibSmtSolver::add(storm::ArithConstraint<storm::RawPolynomial> const& constraint) {
//if some of the occurring variables are not declared yet, we will have to.
std::set<storm::RationalFunctionVariable> variables = constraint.lhs().gatherVariables();
std::vector<std::string> 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<storm::Polynomial> 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<storm::RationalFunctionVariable> variables = constraint.lhs().gatherVariables();
variables.insert(guard);
std::vector<std::string> 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){ 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."); 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<storm::RationalFunctionVariable> variableSet; std::set<storm::RationalFunctionVariable> variableSet;

8
src/storm/solver/SmtlibSmtSolver.h

@ -51,12 +51,7 @@ namespace storm {
//adds the constraint "leftHandSide relation rightHandSide" //adds the constraint "leftHandSide relation rightHandSide"
virtual void add(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation, storm::RationalFunction const& rightHandSide=storm::RationalFunction(0)); 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<storm::RationalFunction> const& constraint);
void add(typename storm::ArithConstraint<storm::RawPolynomial> 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<storm::Polynomial> const& constraint);
// asserts that the given variable has the given value. The variable should have type 'bool' // asserts that the given variable has the given value. The variable should have type 'bool'
void add(storm::RationalFunctionVariable const& variable, bool value); void add(storm::RationalFunctionVariable const& variable, bool value);
@ -65,9 +60,8 @@ namespace storm {
virtual CheckResult check() override; virtual CheckResult check() override;
virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) override; virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) override;
#ifndef WINDOWS
virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) override; virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) override;
#endif
bool isNeedsRestart() const; bool isNeedsRestart() const;

4
src/storm/storage/expressions/Variable.h

@ -130,9 +130,9 @@ namespace storm {
bool hasRationalType() const; 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; bool hasNumericalType() const;

2
src/storm/storm.cpp

@ -1,7 +1,7 @@
#include "storm/utility/macros.h" #include "storm/utility/macros.h"
#include "storm/exceptions/BaseException.h" #include "storm/exceptions/BaseException.h"
#include "storm/cli/cli.h"
#include "storm-cli-utilities/cli.h"
/*! /*!
* Main entry point of the executable storm. * Main entry point of the executable storm.

164
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 <vector>' | $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 <vector>' | $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"

71
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

16
travis/dockerfiles/Dockerfile.debian-9

@ -0,0 +1,16 @@
FROM debian:9
MAINTAINER Matthias Volk <matthias.volk@cs.rwth-aachen.de>
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

8
travis/dockerfiles/Dockerfile.storm

@ -0,0 +1,8 @@
FROM mvolk/storm-basesystem:ubuntu-16.10
MAINTAINER Matthias Volk <matthias.volk@cs.rwth-aachen.de>
COPY build_carl.sh /opt
RUN cd opt && ./build_carl.sh
COPY build_storm.sh /opt
RUN cd opt && ./build_storm.sh

17
travis/dockerfiles/Dockerfile.ubuntu-16.10

@ -0,0 +1,17 @@
FROM ubuntu:16.10
MAINTAINER Matthias Volk <matthias.volk@cs.rwth-aachen.de>
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

9
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"

9
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

9
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"

123
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)

11
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

73
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

4
travis/mtime_cache/globs.txt

@ -0,0 +1,4 @@
src/**/*.{%{cpp}}
src/**/CMakeLists.txt
resources/3rdparty/**/*.{%{cpp}}
resources/3rdparty/eigen-3.3-beta1/StormEigen/*

178
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 = <<ENDUSAGE
Usage:
mtime_cache [<globs>] [-g globfile] [-d] [-q|V] [-c cache]
ENDUSAGE
HELP = <<ENDHELP
Traverse through globbed files, making a json cache based on their mtime.
If a cache exists, changes the mtime of existing unchanged (based on MD5
hash) files to the one in the cache.
Options:
globs Ruby-compatible glob strings (ex some/path/**/*.java)
A extension pattern is allowd in the form %{pattern}
(ex some/path/*.{%{pattern1},%{pattern2}})
The globs support the following patterns:
%{cpp} - common C++ extensions
-g, --globfile A file with list of globs to perform (one per line)
-?, -h, --help Show this help message.
-v, --version Show the version number (#{VERSION})
-q, --quiet Don't log anything to stdout
-V, --verbose Show extra logging
-d, --dryrun Don't change any files on the filesystem
-c, --cache Specify the cache file for input and output.
[Default is .mtime_cache.json]
ENDHELP
param_arg = nil
ARGS = { :cache => '.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
Loading…
Cancel
Save