Merge branch 'master' into pomdp_datastructures

.gitignore

@@ -52,7 +52,5 @@ 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

.travis.yml

@@ -9,6 +9,9 @@ sudo: required
 dist: trusty
 language: cpp
 
+git:
+  depth: false
+
 # Enable caching
 cache:
   timeout: 1000
@@ -25,7 +28,7 @@ notifications:
     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="
+    - secure: "VWnsiQkt1xjgRo1hfNiNQqvLSr0fshFmLV7jJlUixhCr094mgD0U2bNKdUfebm28Byg9UyDYPbOFDC0sx7KydKiL1q7FKKXkyZH0k04wUu8XiNw+fYkDpmPnQs7G2n8oJ/GFJnr1Wp/1KI3qX5LX3xot4cJfx1I5iFC2O+p+ng6v/oSX+pewlMv4i7KL16ftHHHMo80N694v3g4B2NByn4GU2/bjVQcqlBp/TiVaUa5Nqu9DxZi/n9CJqGEaRHOblWyMO3EyTZsn45BNSWeQ3DtnMwZ73rlIr9CaEgCeuArc6RGghUAVqRI5ao+N5apekIaILwTgL6AJn+Lw/+NRPa8xclgd0rKqUQJMJCDZKjKz2lmIs3bxfELOizxJ3FJQ5R95FAxeAZ6rb/j40YqVVTw2IMBDnEE0J5ZmpUYNUtPti/Adf6GD9Fb2y8sLo0XDJzkI8OxYhfgjSy5KYmRj8O5MXcP2MAE8LQauNO3MaFnL9VMVOTZePJrPozQUgM021uyahf960+QNI06Uqlmg+PwWkSdllQlxHHplOgW7zClFhtSUpnJxcsUBzgg4kVg80gXUwAQkaDi7A9Wh2bs+TvMlmHzBwg+2SaAfWDgjeJIeOaipDkF1uSGzC+EHAiiKYMLd4Aahoi8SuelJUucoyJyLAq00WdUFQIh/izVhM4Y="
 
 #
 # Configurations
@@ -37,32 +40,32 @@ jobs:
     # Stage: Build Carl
     ###
 
-    # ubuntu-17.10 - DefaultDebugTravis
+    # ubuntu-18.04 - DefaultDebugTravis
     - stage: Build Carl
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-17.10 COMPILER=gcc
+      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc
       install:
         - travis/install_linux.sh
       script:
         - travis/build_carl.sh
       after_success:
         - docker login -u "$DOCKER_USERNAME" -p "$DOCKER_PASSWORD";
-        - docker commit carl mvolk/carl:travis-debug;
-        - docker push mvolk/carl:travis-debug;
-    # ubuntu-17.10 - DefaultReleaseTravis
+        - docker commit carl movesrwth/carl:travis-debug;
+        - docker push movesrwth/carl:travis-debug;
+    # ubuntu-18.04 - DefaultReleaseTravis
     - stage: Build Carl
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-17.10 COMPILER=gcc
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
       install:
         - travis/install_linux.sh
       script:
         - travis/build_carl.sh
       after_success:
         - docker login -u "$DOCKER_USERNAME" -p "$DOCKER_PASSWORD";
-        - docker commit carl mvolk/carl:travis;
-        - docker push mvolk/carl:travis;
+        - docker commit carl movesrwth/carl:travis;
+        - docker push movesrwth/carl:travis;
 
     ###
     # Stage: Build (1st run)
@@ -96,11 +99,25 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-17.10 - DefaultDebugTravis
+    # ubuntu-18.04 - DefaultDebugTravis
+    - stage: Build (1st run)
+      os: linux
+      compiler: gcc
+      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      install:
+        - rm -rf build
+        - travis/install_linux.sh
+      script:
+        - travis/build.sh Build1
+      before_cache:
+        - docker cp storm:/opt/storm/. .
+      after_failure:
+        - find build -iname '*err*.log' -type f -print -exec cat {} \;
+    # ubuntu-18.04 - DefaultReleaseTravis
     - stage: Build (1st run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-17.10 COMPILER=gcc
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
       install:
         - rm -rf build
         - travis/install_linux.sh
@@ -110,11 +127,25 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-17.10 - DefaultReleaseTravis
+    # ubuntu-18.04 - DefaultDebug
     - stage: Build (1st run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-17.10 COMPILER=gcc
+      env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc
+      install:
+        - rm -rf build
+        - travis/install_linux.sh
+      script:
+        - travis/build.sh Build1
+      before_cache:
+        - docker cp storm:/opt/storm/. .
+      after_failure:
+        - find build -iname '*err*.log' -type f -print -exec cat {} \;
+    # ubuntu-18.04 - DefaultRelease
+    - stage: Build (1st run)
+      os: linux
+      compiler: gcc
+      env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc
       install:
         - rm -rf build
         - travis/install_linux.sh
@@ -155,11 +186,37 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-17.10 - DefaultDebugTravis
+    # ubuntu-18.04 - DefaultDebugTravis
+    - stage: Build (2nd run)
+      os: linux
+      compiler: gcc
+      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      install:
+        - travis/install_linux.sh
+      script:
+        - travis/build.sh Build2
+      before_cache:
+        - docker cp storm:/opt/storm/. .
+      after_failure:
+        - find build -iname '*err*.log' -type f -print -exec cat {} \;
+    # ubuntu-18.04 - DefaultReleaseTravis
+    - stage: Build (2nd run)
+      os: linux
+      compiler: gcc
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      install:
+        - travis/install_linux.sh
+      script:
+        - travis/build.sh Build2
+      before_cache:
+        - docker cp storm:/opt/storm/. .
+      after_failure:
+        - find build -iname '*err*.log' -type f -print -exec cat {} \;
+    # ubuntu-18.04 - DefaultDebug
     - stage: Build (2nd run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-17.10 COMPILER=gcc
+      env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc
       install:
         - travis/install_linux.sh
       script:
@@ -168,11 +225,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-17.10 - DefaultReleaseTravis
+    # ubuntu-18.04 - DefaultRelease
     - stage: Build (2nd run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-17.10 COMPILER=gcc
+      env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc
       install:
         - travis/install_linux.sh
       script:
@@ -212,11 +269,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-17.10 - DefaultDebugTravis
+    # ubuntu-18.04 - DefaultDebugTravis
     - stage: Build (3rd run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-17.10 COMPILER=gcc
+      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc
       install:
         - travis/install_linux.sh
       script:
@@ -225,11 +282,37 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-17.10 - DefaultReleaseTravis
+    # ubuntu-18.04 - DefaultReleaseTravis
     - stage: Build (3rd run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-17.10 COMPILER=gcc
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      install:
+        - travis/install_linux.sh
+      script:
+        - travis/build.sh Build3
+      before_cache:
+        - docker cp storm:/opt/storm/. .
+      after_failure:
+        - find build -iname '*err*.log' -type f -print -exec cat {} \;
+    # ubuntu-18.04 - DefaultDebug
+    - stage: Build (3rd run)
+      os: linux
+      compiler: gcc
+      env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc
+      install:
+        - travis/install_linux.sh
+      script:
+        - travis/build.sh Build3
+      before_cache:
+        - docker cp storm:/opt/storm/. .
+      after_failure:
+        - find build -iname '*err*.log' -type f -print -exec cat {} \;
+    # ubuntu-18.04 - DefaultRelease
+    - stage: Build (3rd run)
+      os: linux
+      compiler: gcc
+      env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc
       install:
         - travis/install_linux.sh
       script:
@@ -269,11 +352,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-17.10 - DefaultDebugTravis
+    # ubuntu-18.04 - DefaultDebugTravis
     - stage: Build (4th run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-17.10 COMPILER=gcc
+      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc
       install:
         - travis/install_linux.sh
       script:
@@ -282,11 +365,37 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-17.10 - DefaultReleaseTravis
+    # ubuntu-18.04 - DefaultReleaseTravis
     - stage: Build (4th run)
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-17.10 COMPILER=gcc
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
+      install:
+        - travis/install_linux.sh
+      script:
+        - travis/build.sh BuildLast
+      before_cache:
+        - docker cp storm:/opt/storm/. .
+      after_failure:
+        - find build -iname '*err*.log' -type f -print -exec cat {} \;
+    # ubuntu-18.04 - DefaultDebug
+    - stage: Build (4th run)
+      os: linux
+      compiler: gcc
+      env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc
+      install:
+        - travis/install_linux.sh
+      script:
+        - travis/build.sh BuildLast
+      before_cache:
+        - docker cp storm:/opt/storm/. .
+      after_failure:
+        - find build -iname '*err*.log' -type f -print -exec cat {} \;
+    # ubuntu-18.04 - DefaultRelease
+    - stage: Build (4th run)
+      os: linux
+      compiler: gcc
+      env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc
       install:
         - travis/install_linux.sh
       script:
@@ -326,11 +435,11 @@ jobs:
         - docker cp storm:/opt/storm/. .
       after_failure:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
-    # ubuntu-17.10 - DefaultDebugTravis
+    # ubuntu-18.04 - DefaultDebugTravis
     - stage: Test all
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-17.10 COMPILER=gcc
+      env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc
       install:
         - travis/install_linux.sh
       script:
@@ -341,13 +450,13 @@ jobs:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
       after_success:
         - docker login -u "$DOCKER_USERNAME" -p "$DOCKER_PASSWORD";
-        - docker commit storm mvolk/storm:travis-debug;
-        - docker push mvolk/storm:travis-debug;
-    # ubuntu-17.10 - DefaultReleaseTravis
+        - docker commit storm movesrwth/storm:travis-debug;
+        - docker push movesrwth/storm:travis-debug;
+    # ubuntu-18.04 - DefaultReleaseTravis
     - stage: Test all
       os: linux
       compiler: gcc
-      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-17.10 COMPILER=gcc
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
       install:
         - travis/install_linux.sh
       script:
@@ -358,6 +467,48 @@ jobs:
         - find build -iname '*err*.log' -type f -print -exec cat {} \;
       after_success:
         - docker login -u "$DOCKER_USERNAME" -p "$DOCKER_PASSWORD";
-        - docker commit storm mvolk/storm:travis;
-        - docker push mvolk/storm:travis;
+        - docker commit storm movesrwth/storm:travis;
+        - docker push movesrwth/storm:travis;
+    # ubuntu-18.04 - DefaultDebug
+    - stage: Test all
+      os: linux
+      compiler: gcc
+      env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc
+      install:
+        - travis/install_linux.sh
+      script:
+        - travis/build.sh TestAll
+      before_cache:
+        - docker cp storm:/opt/storm/. .
+      after_failure:
+        - find build -iname '*err*.log' -type f -print -exec cat {} \;
+    # ubuntu-18.04 - DefaultRelease
+    - stage: Test all
+      os: linux
+      compiler: gcc
+      env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc
+      install:
+        - travis/install_linux.sh
+      script:
+        - travis/build.sh TestAll
+      before_cache:
+        - docker cp storm:/opt/storm/. .
+      after_failure:
+        - find build -iname '*err*.log' -type f -print -exec cat {} \;
+  allow_failures:
+    - stage: Build (1st run)
+      os: linux
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
+    - stage: Build (2nd run)
+      os: linux
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
+    - stage: Build (3rd run)
+      os: linux
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
+    - stage: Build (4th run)
+      os: linux
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
+    - stage: Test all
+      os: linux
+      env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
 

CHANGELOG.md

@@ -7,7 +7,33 @@ The releases of major and minor versions contain an overview of changes since th
 Version 1.2.x
 -------------
 
-### Version 1.2.2 (to be released)
+### Version 1.2.4 (2018/08)
+- New binary `storm-conv` that handles conversions between model files (currently: prism to jani)
+- Added support for expected time properties for discrete time models
+- Bug fix in the parser for DRN (MDPs and MAs might have been affected).
+- Several bug fixes related to jani
+- `storm-gspn`: Improved .pnpro parser
+- `storm-gspn`: Added support for single/infinite/k-server semantics for GSPNs given in the .pnpro format
+- `storm-gspn`: Added option to set a global capacity for all places
+- `storm-gspn`: Added option to include a set of standard properties when converting GSPNs to jani
+
+### Version 1.2.3 (2018/07)
+- Fix in version parsing
+
+### Version 1.2.2 (2018/07)
+- Sound value iteration (SVI) for DTMCs and MDPs
+- Topological solver for linear equation systems and MinMax equation systems (enabled by default)
+- Added support for expected total rewards in the sparse engine
+- By default, iteration-based solvers are no longer aborted after a given number of steps.
+- Improved export for jani models
+- A fix in parsing jani properties
+- Several extensions to high-level counterexamples
+- `storm-parsers` extracted to reduce linking time
+- `storm-counterexamples` extracted to reduce linking time
+- `storm-dft`: improvements in Galileo parser
+- `storm-dft`: test cases for DFT analysis
+- Improved Storm installation
+- Several bug fixes
 
 ### Version 1.2.1 (2018/02)
 - Multi-dimensional reward bounded reachability properties for DTMCs.

CMakeLists.txt

@@ -78,7 +78,15 @@ set(BIN_INSTALL_DIR lib/ CACHE PATH "Installation directory for executables")
 set(DEF_INSTALL_CMAKE_DIR "lib/CMake/storm")
 set(CMAKE_INSTALL_DIR ${DEF_INSTALL_CMAKE_DIR} CACHE PATH  "Installation directory for CMake files")
 
-message("CMAKE_INSTALL_DIR: ${CMAKE_INSTALL_DIR}")
+# Add CMake install prefix
+foreach(p LIB BIN INCLUDE CMAKE)
+  set(var ${p}_INSTALL_DIR)
+  if(NOT IS_ABSOLUTE "${${var}}")
+    set(${var} "${CMAKE_INSTALL_PREFIX}/${${var}}")
+  endif()
+endforeach()
+
+message(STATUS "Storm - CMake install dir: ${CMAKE_INSTALL_DIR}")
 
 # If the STORM_DEVELOPER option was turned on, by default we target a debug version, otherwise a release version.
 if (STORM_DEVELOPER)
@@ -145,15 +153,15 @@ elseif (WIN32)
 	set(STATIC_EXT ".lib")
 	set(LIB_PREFIX "")
 endif()
-message(STATUS "Assuming extension for shared libraries: ${DYNAMIC_EXT}")
-message(STATUS "Assuming extension for static libraries: ${STATIC_EXT}")
+message(STATUS "Storm - Assuming extension for shared libraries: ${DYNAMIC_EXT}")
+message(STATUS "Storm - Assuming extension for static libraries: ${STATIC_EXT}")
 
 if(BUILD_SHARED_LIBS)
     set(LIB_EXT ${DYNAMIC_EXT})
-    message(STATUS "Build dynamic libraries.")
+    message(STATUS "Storm - Build dynamic libraries.")
 else()
     set(LIB_EXT ${STATIC_EXT})
-    message(STATUS "Build static libraries.")
+    message(STATUS "Storm - Build static libraries.")
 endif()
 
 #############################################################
@@ -185,11 +193,6 @@ elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU")
 	# using GCC
 	if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 5.0)
 		message(FATAL_ERROR "gcc version must be at least 5.0.")
-	elseif (CMAKE_CXX_COMPILER_VERSION VERSION_EQUAL 7.0 OR CMAKE_CXX_COMPILER_VERSION VERSION_GREATER 7.0)
-		if (STORM_USE_LTO)
-			set(STORM_USE_LTO OFF)
-			message(WARNING "Disabling link-time optimization, because of known incompatibility of LTO with gcc >= 7.")
-		endif()
 	endif()
 
 	set(STORM_COMPILER_GCC ON)
@@ -236,7 +239,7 @@ if (STORM_COMPILER_CLANG OR STORM_COMPILER_APPLECLANG)
     endif()
 
     set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14 -stdlib=${CLANG_STDLIB} -ftemplate-depth=1024")
-    set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -ffast-math -fno-finite-math-only")
+    set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE}")
 
     if(LINUX)
         set (CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -rdynamic")
@@ -247,7 +250,7 @@ if (STORM_COMPILER_CLANG OR STORM_COMPILER_APPLECLANG)
     endif()
 elseif (STORM_COMPILER_GCC)
     set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14")
-    set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -fprefetch-loop-arrays -ffast-math -fno-finite-math-only")
+    set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -fprefetch-loop-arrays")
     set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -rdynamic")
     set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -rdynamic")
 endif ()
@@ -408,7 +411,7 @@ endif(DOXYGEN_FOUND)
 # try to obtain the current version from git.
 include(GetGitRevisionDescription)
 get_git_head_revision(STORM_VERSION_REFSPEC STORM_VERSION_GIT_HASH)
-git_describe_checkout(STORM_GIT_VERSION_STRING)
+git_describe(STORM_GIT_VERSION_STRING)
 
 # parse the git tag into variables
 # start with major.minor.patch
@@ -417,22 +420,22 @@ set(STORM_VERSION_MAJOR "${CMAKE_MATCH_1}")
 set(STORM_VERSION_MINOR "${CMAKE_MATCH_2}")
 set(STORM_VERSION_PATCH "${CMAKE_MATCH_3}")
 set(STORM_GIT_VERSION_REST "${CMAKE_MATCH_4}")
-# parse rest of the form (-label)-commitsahead-hash-appendix
+# parse rest of the form (-label)-commitsahead-hash(-appendix)
 string(REGEX MATCH "^(\\-([a-z][a-z0-9\\.]+))?\\-([0-9]+)\\-([a-z0-9]+)(\\-.*)?$" STORM_VERSION_REST_MATCH "${STORM_GIT_VERSION_REST}")
 set(STORM_VERSION_LABEL "${CMAKE_MATCH_2}") # might be empty
 set(STORM_VERSION_COMMITS_AHEAD "${CMAKE_MATCH_3}")
-set(STORM_VERSION_TAG_HASH "${CMAKE_MATCH_4}")
+set(STORM_VERSION_TAG_HASH "${CMAKE_MATCH_4}") # is not used
 set(STORM_VERSION_APPENDIX "${CMAKE_MATCH_5}") # might be empty
 
-# now check whether the git version lookup failed
-if (STORM_VERSION_MAJOR MATCHES "NOTFOUND")
-	include(version.cmake)
-	set(STORM_VERSION_LABEL "")
+# check whether the git version lookup failed
+if (STORM_GIT_VERSION_STRING MATCHES "NOTFOUND")
+	set(STORM_VERSION_SOURCE "VersionSource::Static")
 	set(STORM_VERSION_COMMITS_AHEAD 0)
-	set(STORM_VERSION_GIT_HASH "")
 	set(STORM_VERSION_DIRTY boost::none)
-	message(WARNING "Storm - git version information not available, statically assuming version ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}.")
+	include(version.cmake)
+	message(WARNING "Storm - Git version information not available, statically assuming version ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}.")
 else()
+	set(STORM_VERSION_SOURCE "VersionSource::Git")
 	if ("${STORM_VERSION_APPENDIX}" MATCHES "^.*dirty.*$")
 		set(STORM_VERSION_DIRTY "true")
 	else()
@@ -448,18 +451,19 @@ else()
 endif()
 
 # check for development version with commits ahead of latest tag
-set(STORM_VERSION_DEV "false")
-set(STORM_VERSION_DEV_STRING "")
 if(STORM_VERSION_COMMITS_AHEAD)
+	set(STORM_VERSION_DEV "true")
+	set(STORM_VERSION_DEV_STRING " (dev)")
 	if ("${STORM_VERSION_LABEL}" STREQUAL "")
 		# increase patch number to indicate newer version
 		MATH(EXPR STORM_VERSION_DEV_PATCH "${STORM_VERSION_PATCH}+1")
 	else()
 		set(STORM_VERSION_DEV_PATCH "${STORM_VERSION_PATCH}")
 	endif()
-	set(STORM_VERSION_DEV "true")
-	set(STORM_VERSION_DEV_STRING " (dev)")
 else()
+	set(STORM_VERSION_COMMITS_AHEAD 0)
+	set(STORM_VERSION_DEV "false")
+	set(STORM_VERSION_DEV_STRING "")
 	set(STORM_VERSION_DEV_PATCH ${STORM_VERSION_PATCH})
 endif()
 
@@ -467,7 +471,7 @@ endif()
 set(STORM_VERSION "${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_DEV_PATCH}")
 set(STORM_VERSION_STRING "${STORM_VERSION}${STORM_VERSION_LABEL_STRING}${STORM_VERSION_DEV_STRING}")
 
-message(STATUS "Storm - version is ${STORM_VERSION_STRING} (version ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}${STORM_VERSION_LABEL_STRING} + ${STORM_VERSION_COMMITS_AHEAD} commits), building from git: ${STORM_VERSION_GIT_HASH} (dirty: ${STORM_VERSION_DIRTY}).")
+message(STATUS "Storm - Version is ${STORM_VERSION_STRING} (version ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}${STORM_VERSION_LABEL_STRING} + ${STORM_VERSION_COMMITS_AHEAD} commits), building from git: ${STORM_VERSION_GIT_HASH} (dirty: ${STORM_VERSION_DIRTY}).")
 
 
 # Configure a header file to pass some of the CMake settings to the source code
@@ -502,4 +506,8 @@ add_subdirectory(src)
 
 include(export)
 
+install(FILES ${CMAKE_BINARY_DIR}/stormConfig.install.cmake DESTINATION ${CMAKE_INSTALL_DIR} RENAME stormConfig.cmake)
+install(FILES ${CMAKE_BINARY_DIR}/stormConfigVersion.cmake DESTINATION ${CMAKE_INSTALL_DIR})
+install(EXPORT storm_Targets FILE stormTargets.cmake DESTINATION ${CMAKE_INSTALL_DIR})
+
 include(StormCPackConfig.cmake)

README.md

@@ -30,15 +30,15 @@ Authors
 Storm has been developed at RWTH Aachen University.
 
 ###### Principal developers
-* Christian Dehnert
+* Christian Hensel
 * Sebastian Junges
 * Joost-Pieter Katoen
+* Tim Quatmann
 * Matthias Volk
 
 ###### Developers (lexicographical order)
 * Philipp Berger
 * David Korzeniewski
-* Tim Quatmann
 
 ###### Contributors (lexicographical order)
 * Dimitri Bohlender

doc/checklist_new_release.md

@@ -1,5 +1,5 @@
 The following steps should be performed before releasing a new storm version.
-Note that in most case a simultaneous release of [carl](https://github.com/smtrat/carl), [storm](https://github.com/moves-rwth/storm), [pycarl](https://github.com/moves-rwth/pycarl/) and [stormpy](https://github.com/moves-rwth/stormpy/) is preferred.
+Note that in most cases a simultaneous release of [carl](https://github.com/smtrat/carl), [storm](https://github.com/moves-rwth/storm), [pycarl](https://github.com/moves-rwth/pycarl/) and [stormpy](https://github.com/moves-rwth/stormpy/) is preferred.
 
 1. Update `CHANGELOG.md`
    To get all the commits from an author since the last tag execute:

resources/3rdparty/CMakeLists.txt

@@ -141,33 +141,46 @@ find_package(Z3 QUIET)
 # Z3 Defines
 set(STORM_HAVE_Z3 ${Z3_FOUND})
 
+
 if(Z3_FOUND)
-    # Check whether the version of z3 supports optimization
-    if (Z3_EXEC)
-        execute_process (COMMAND ${Z3_EXEC} -version
-                OUTPUT_VARIABLE z3_version_output
-                ERROR_QUIET
-                OUTPUT_STRIP_TRAILING_WHITESPACE)
+    # Get the z3 version by compiling and running a simple program
+    try_run(version_run_result version_compile_result "${STORM_3RDPARTY_BINARY_DIR}/z3/" "${PROJECT_SOURCE_DIR}/resources/3rdparty/z3/output_version.cpp" CMAKE_FLAGS "-DINCLUDE_DIRECTORIES=${Z3_INCLUDE_DIR}" LINK_LIBRARIES "${Z3_LIBRARIES}" RUN_OUTPUT_VARIABLE z3_version_output)
+    if (version_compile_result AND version_run_result EQUAL 0)
         if (z3_version_output MATCHES "([0-9]*\\.[0-9]*\\.[0-9]*)")
             set(Z3_VERSION "${CMAKE_MATCH_1}")
-            if(NOT "${Z3_VERSION}" VERSION_LESS "4.5.0")
-                set(STORM_HAVE_Z3_OPTIMIZE ON)
-            endif()
         endif()
     endif()
 
-    if(STORM_HAVE_Z3_OPTIMIZE)
-        message (STATUS "Storm - Linking with Z3. (Z3 version supports optimization)")
+    if(Z3_VERSION)
+        # Split Z3 version into its components
+        string(REPLACE "." ";" Z3_VERSION_LIST ${Z3_VERSION})
+        list(GET Z3_VERSION_LIST 0 STORM_Z3_VERSION_MAJOR)
+        list(GET Z3_VERSION_LIST 1 STORM_Z3_VERSION_MINOR)
+        list(GET Z3_VERSION_LIST 2 STORM_Z3_VERSION_PATCH)
+
+        # Check whether the version of z3 supports optimization
+        if(NOT "${Z3_VERSION}" VERSION_LESS "4.5.0")
+            set(STORM_HAVE_Z3_OPTIMIZE ON)
+            message (STATUS "Storm - Linking with Z3 (version ${Z3_VERSION}). (Z3 version supports optimization)")
+        else()
+            message (STATUS "Storm - Linking with Z3 (version ${Z3_VERSION}). (Z3 version does not support optimization)")
+        endif()
+        if (NOT "${Z3_VERSION}" VERSION_LESS "4.7.1")
+            set(STORM_Z3_API_USES_STANDARD_INTEGERS ON)
+        endif()
+
+        add_imported_library(z3 SHARED ${Z3_LIBRARIES} ${Z3_INCLUDE_DIRS})
+        list(APPEND STORM_DEP_TARGETS z3_SHARED)
     else()
-        message (STATUS "Storm - Linking with Z3. (Z3 version does not support optimization)")
+        message(WARNING "Storm - Could not obtain Z3 version. Building of Prism/JANI models will not be supported.")
+        set(Z3_FOUND FALSE)
     endif()
 
-    add_imported_library(z3 SHARED ${Z3_LIBRARIES} ${Z3_INCLUDE_DIRS})
-    list(APPEND STORM_DEP_TARGETS z3_SHARED)
 else()
     message (WARNING "Storm - Z3 not found. Building of Prism/JANI models will not be supported.")
 endif(Z3_FOUND)
 
+
 #############################################################
 ##
 ##	glpk
@@ -209,6 +222,7 @@ include(${STORM_3RDPARTY_SOURCE_DIR}/include_cudd.cmake)
 
 set(STORM_HAVE_CARL OFF)
 set(CARL_MINVERSION "17.12")
+set(CARL_C14VERSION "14.1")
 if (NOT STORM_FORCE_SHIPPED_CARL)
     if (NOT "${STORM_CARL_DIR_HINT}" STREQUAL "")
 		find_package(carl QUIET PATHS ${STORM_CARL_DIR_HINT} NO_DEFAULT_PATH)
@@ -226,7 +240,9 @@ if(carl_FOUND AND NOT STORM_FORCE_SHIPPED_CARL)
     else()
         message(SEND_ERROR "File ${carlLOCATION} does not exist, did you build carl?")
     endif()
-    if("${carl_VERSION_MAJOR}.${carl_VERSION_MINOR}" VERSION_LESS "${CARL_MINVERSION}")
+    if("${carl_VERSION_MAJOR}.${carl_VERSION_MINOR}" STREQUAL "${CARL_C14VERSION}")
+        # empty on purpose. Maybe put a warning here?
+    elseif("${carl_VERSION_MAJOR}.${carl_VERSION_MINOR}" VERSION_LESS "${CARL_MINVERSION}")
     	message(SEND_ERROR "Carl outdated, require ${CARL_MINVERSION}, have ${carl_VERSION}")
     endif()
 
@@ -239,7 +255,7 @@ if(carl_FOUND AND NOT STORM_FORCE_SHIPPED_CARL)
 else()
 	set(STORM_SHIPPED_CARL ON)
 	# The first external project will be built at *configure stage*
-	message("START CARL CONFIG PROCESS")
+	message(STATUS "Carl - Start of config process")
 	file(MAKE_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download)
 	execute_process(
 	COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}" "-DBoost_LIBRARY_DIRS=${Boost_LIBRARY_DIRS}" "-DBoost_INCLUDE_DIRS=${Boost_INCLUDE_DIRS}"
@@ -248,7 +264,7 @@ else()
 	RESULT_VARIABLE carlconfig_result)
 
 	if(NOT carlconfig_result)
-		message("${carlconfig_out}")
+		message(STATUS "${carlconfig_out}")
 	endif()
 	execute_process(
 		COMMAND ${CMAKE_COMMAND} --build . --target carl-config
@@ -257,9 +273,9 @@ else()
 		RESULT_VARIABLE carlconfig_result
 		)
 		if(NOT carlconfig_result)
-		message("${carlconfig_out}")
+		message(STATUS "${carlconfig_out}")
 	endif()
-    message("END CARL CONFIG PROCESS")
+    message(STATUS "Carl - End of config process")
 
     message(STATUS "Storm - Using shipped version of carl.")
     ExternalProject_Add(

resources/3rdparty/carl/CMakeLists.txt

@@ -4,11 +4,11 @@ include(ExternalProject)
 
 option(STORM_3RDPARTY_BINARY_DIR "3rd party bin dir")
 
-message(STORM_3RDPARTY_BINARY_DIR: ${STORM_3RDPARTY_BINARY_DIR})
+message(STATUS "Carl - Storm 3rdparty binary dir: ${STORM_3RDPARTY_BINARY_DIR}")
 
 ExternalProject_Add(carl-config
 	GIT_REPOSITORY https://github.com/smtrat/carl
-	GIT_TAG 17.12
+	GIT_TAG 18.06
 	PREFIX here
 	SOURCE_DIR source_dir
 	BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/carl
@@ -22,4 +22,4 @@ ExternalProject_Add(carl-config
 add_custom_target(build-carl)
 add_dependencies(build-carl carl-config)
 
-message("done")
+message(STATUS "Carl - Finished configuration.")

resources/3rdparty/z3/output_version.cpp

@@ -0,0 +1,9 @@
+#include <iostream>
+#include <z3.h>
+
+int main() {
+    unsigned major, minor, build_number, revision_number;
+    Z3_get_version(&major, &minor, &build_number, &revision_number);
+    std::cout << major << "." << minor << "." << build_number << std::endl;
+    return 0;
+}

resources/cmake/find_modules/FindZ3.cmake

@@ -10,7 +10,7 @@
 # find include dir by searching for a concrete file, which definitely must be in it
 find_path(Z3_INCLUDE_DIR 
             NAMES z3++.h 
-            PATHS ENV PATH INCLUDE "/usr/include/z3" "/usr/local/include/z3/" "${Z3_ROOT}/include"
+            PATHS ENV PATH INCLUDE "${Z3_ROOT}/include" "/usr/include/z3" "/usr/local/include/z3/"
          )
 
 # find library

resources/cmake/macros/GetGitRevisionDescription.cmake

@@ -18,6 +18,12 @@
 # and adjusting the output so that it tests false if there was no exact
 # matching tag.
 #
+#  git_local_changes(<var>)
+#
+# Returns either "CLEAN" or "DIRTY" with respect to uncommitted changes.
+# Uses the return code of "git diff-index --quiet HEAD --".
+# Does not regard untracked files.
+#
 # Requires CMake 2.6 or newer (uses the 'function' command)
 #
 # Original Author:
@@ -37,10 +43,10 @@ set(__get_git_revision_description YES)
 
 # We must run the following at "include" time, not at function call time,
 # to find the path to this module rather than the path to a calling list file
-get_filename_component(_gitdescmoddir GetGitRevisionDescription.cmake PATH)
+get_filename_component(_gitdescmoddir ${CMAKE_CURRENT_LIST_FILE} PATH)
 
 function(get_git_head_revision _refspecvar _hashvar)
-	set(GIT_PARENT_DIR ${PROJECT_SOURCE_DIR})
+	set(GIT_PARENT_DIR "${CMAKE_CURRENT_SOURCE_DIR}")
 	set(GIT_DIR "${GIT_PARENT_DIR}/.git")
 	while(NOT EXISTS "${GIT_DIR}")	# .git dir not found, search parent directories
 		set(GIT_PREVIOUS_PARENT "${GIT_PARENT_DIR}")
@@ -71,7 +77,7 @@ function(get_git_head_revision _refspecvar _hashvar)
 	set(HEAD_FILE "${GIT_DATA}/HEAD")
 	configure_file("${GIT_DIR}/HEAD" "${HEAD_FILE}" COPYONLY)
 
-	configure_file("${PROJECT_SOURCE_DIR}/resources/cmake/macros/GetGitRevisionDescription.cmake.in"
+	configure_file("${_gitdescmoddir}/GetGitRevisionDescription.cmake.in"
 		"${GIT_DATA}/grabRef.cmake"
 		@ONLY)
 	include("${GIT_DATA}/grabRef.cmake")
@@ -110,7 +116,7 @@ function(git_describe _var)
 		${hash}
 		${ARGN}
 		WORKING_DIRECTORY
-		"${CMAKE_SOURCE_DIR}"
+		"${CMAKE_CURRENT_SOURCE_DIR}"
 		RESULT_VARIABLE
 		res
 		OUTPUT_VARIABLE
@@ -124,7 +130,12 @@ function(git_describe _var)
 	set(${_var} "${out}" PARENT_SCOPE)
 endfunction()
 
-function(git_describe_checkout _var)
+function(git_get_exact_tag _var)
+	git_describe(out --exact-match ${ARGN})
+	set(${_var} "${out}" PARENT_SCOPE)
+endfunction()
+
+function(git_local_changes _var)
 	if(NOT GIT_FOUND)
 		find_package(Git QUIET)
 	endif()
@@ -138,39 +149,20 @@ function(git_describe_checkout _var)
 		return()
 	endif()
 
-	# TODO sanitize
-	#if((${ARGN}" MATCHES "&&") OR
-	#	(ARGN MATCHES "||") OR
-	#	(ARGN MATCHES "\\;"))
-	#	message("Please report the following error to the project!")
-	#	message(FATAL_ERROR "Looks like someone's doing something nefarious with git_describe! Passed arguments ${ARGN}")
-	#endif()
-
-	#message(STATUS "Arguments to execute_process: ${ARGN}")
-
 	execute_process(COMMAND
 		"${GIT_EXECUTABLE}"
-		describe
-		--tags
-		--dirty=-dirty
-		--long
-		${ARGN}
+		diff-index --quiet HEAD --
 		WORKING_DIRECTORY
-		"${CMAKE_SOURCE_DIR}"
+		"${CMAKE_CURRENT_SOURCE_DIR}"
 		RESULT_VARIABLE
 		res
 		OUTPUT_VARIABLE
 		out
 		ERROR_QUIET
 		OUTPUT_STRIP_TRAILING_WHITESPACE)
-	if(NOT res EQUAL 0)
-		set(out "${out}-${res}-NOTFOUND")
+	if(res EQUAL 0)
+		set(${_var} "CLEAN" PARENT_SCOPE)
+	else()
+		set(${_var} "DIRTY" PARENT_SCOPE)
 	endif()
-
-	set(${_var} "${out}" PARENT_SCOPE)
-endfunction()
-
-function(git_get_exact_tag _var)
-	git_describe(out --exact-match ${ARGN})
-	set(${_var} "${out}" PARENT_SCOPE)
 endfunction()

resources/cmake/macros/GetGitRevisionDescription.cmake.in

@@ -23,9 +23,12 @@ if(HEAD_CONTENTS MATCHES "ref")
 	string(REPLACE "ref: " "" HEAD_REF "${HEAD_CONTENTS}")
 	if(EXISTS "@GIT_DIR@/${HEAD_REF}")
 		configure_file("@GIT_DIR@/${HEAD_REF}" "@GIT_DATA@/head-ref" COPYONLY)
-	elseif(EXISTS "@GIT_DIR@/logs/${HEAD_REF}")
-		configure_file("@GIT_DIR@/logs/${HEAD_REF}" "@GIT_DATA@/head-ref" COPYONLY)
-		set(HEAD_HASH "${HEAD_REF}")
+	else()
+		configure_file("@GIT_DIR@/packed-refs" "@GIT_DATA@/packed-refs" COPYONLY)
+		file(READ "@GIT_DATA@/packed-refs" PACKED_REFS)
+		if(${PACKED_REFS} MATCHES "([0-9a-z]*) ${HEAD_REF}")
+			set(HEAD_HASH "${CMAKE_MATCH_1}")
+		endif()
 	endif()
 else()
 	# detached HEAD

resources/cmake/macros/export.cmake

@@ -19,10 +19,26 @@ endforeach()
 
 include(CMakePackageConfigHelpers)
 
+write_basic_package_version_file(${CMAKE_CURRENT_BINARY_DIR}/stormConfigVersion.cmake
+     VERSION 0.1.0
+     COMPATIBILITY SameMajorVersion )
+
+# For the build tree
 set(CONF_INCLUDE_DIRS "${CMAKE_BINARY_DIR}/include/")
 configure_package_config_file(
         resources/cmake/stormConfig.cmake.in
         ${PROJECT_BINARY_DIR}/stormConfig.cmake
         INSTALL_DESTINATION ${CMAKE_INSTALL_DIR}
-        PATH_VARS INCLUDE_INSTALL_DIR #SYSCONFIG_INSTALL_DIR
+        PATH_VARS INCLUDE_INSTALL_DIR
+)
+
+ # For the install tree
+file(RELATIVE_PATH REL_INCLUDE_DIR "${CMAKE_INSTALL_DIR}" "${INCLUDE_INSTALL_DIR}")
+set(CONF_INCLUDE_DIRS "\${storm_CMAKE_DIR}/${REL_INCLUDE_DIR}/storm")
+
+configure_package_config_file(
+    resources/cmake/stormConfig.cmake.in
+    ${PROJECT_BINARY_DIR}/stormConfig.install.cmake
+    INSTALL_DESTINATION ${CMAKE_INSTALL_DIR}
+    PATH_VARS INCLUDE_INSTALL_DIR
 )

resources/cmake/stormConfigVersion.cmake.in

@@ -0,0 +1,11 @@
+set(PACKAGE_VERSION "@storm_VERSION@")
+ 
+# Check whether the requested PACKAGE_FIND_VERSION is compatible
+if("${PACKAGE_VERSION}" VERSION_LESS "${PACKAGE_FIND_VERSION}")
+  set(PACKAGE_VERSION_COMPATIBLE FALSE)
+else()
+  set(PACKAGE_VERSION_COMPATIBLE TRUE)
+  if ("${PACKAGE_VERSION}" VERSION_EQUAL "${PACKAGE_FIND_VERSION}")
+    set(PACKAGE_VERSION_EXACT TRUE)
+  endif()
+endif()

resources/examples/testfiles/ctmc/simple2.sm

@@ -0,0 +1,28 @@
+
+ctmc
+
+
+module main
+	
+	s : [0..4]; // current state:
+	
+	
+	<> s=0 -> 4 : (s'=1) + 4 : (s'=2);
+	<> s=1 -> 0.3 : (s'=2) + 0.7 : (s'=1);
+	<> s=2 -> 0.5 : (s'=2) + 0.5 : (s'=3);
+	<> s=3 -> 1 : (s'=4);
+	<> s=4 -> 1 : (s'=3);
+	
+endmodule
+
+rewards "rew1"
+	s=0 : 7;
+	[] s=2 : 1;
+endrewards
+
+
+rewards "rew2"
+	s=0 : 7;
+	[] s=2 : 1;
+	[] s=4 : 100;
+endrewards

resources/examples/testfiles/dft/and.dft

@@ -0,0 +1,4 @@
+toplevel "A";
+"A" and "B" "C";
+"B" lambda=0.5 dorm=0.3;
+"C" lambda=0.5 dorm=0.3;

resources/examples/testfiles/dft/and.json

@@ -0,0 +1,71 @@
+{
+    "toplevel": "2",
+    "parameters": {},
+    "nodes": [
+        {
+            "data": {
+                "id": "0",
+                "name": "A",
+                "type": "be",
+                "rate": "1",
+                "dorm": "1",
+                "label": "A (1)"
+            },
+            "position": {
+                "x": 440,
+                "y": 260
+            },
+            "group": "nodes",
+            "removed": false,
+            "selected": false,
+            "selectable": true,
+            "locked": false,
+            "grabbable": true,
+            "classes": "be"
+        },
+        {
+            "data": {
+                "id": "1",
+                "name": "B",
+                "type": "be",
+                "rate": "1",
+                "dorm": "1",
+                "label": "B (1)"
+            },
+            "position": {
+                "x": 548,
+                "y": 265
+            },
+            "group": "nodes",
+            "removed": false,
+            "selected": false,
+            "selectable": true,
+            "locked": false,
+            "grabbable": true,
+            "classes": "be"
+        },
+        {
+            "data": {
+                "id": "2",
+                "name": "Z",
+                "type": "and",
+                "children": [
+                    "0",
+                    "1"
+                ],
+                "label": "Z"
+            },
+            "position": {
+                "x": 505,
+                "y": 119
+            },
+            "group": "nodes",
+            "removed": false,
+            "selected": false,
+            "selectable": true,
+            "locked": false,
+            "grabbable": true,
+            "classes": "and"
+        }
+    ]
+}

resources/examples/testfiles/dft/fdep.dft

@@ -0,0 +1,8 @@
+toplevel "System";
+"System" or "Power" "Machine";
+"Power" fdep "B_Power" "P" "B";
+"Machine" or "P" "B";
+
+"B_Power" lambda=0.5 dorm=0;
+"P" lambda=0.5 dorm=0;
+"B" lambda=0.5 dorm=0.5;

resources/examples/testfiles/dft/fdep2.dft

@@ -0,0 +1,5 @@
+toplevel "A";
+"A" and "B" "C";
+"F" fdep "B" "C";
+"B" lambda=0.5 dorm=0;
+"C" lambda=0.5 dorm=0;

resources/examples/testfiles/dft/fdep3.dft

@@ -0,0 +1,5 @@
+toplevel "A";
+"A" and "B" "C" "F";
+"F" fdep "B" "C";
+"B" lambda=0.4 dorm=0;
+"C" lambda=0.8 dorm=0;

resources/examples/testfiles/dft/fdep4.dft

@@ -0,0 +1,7 @@
+toplevel "A";
+"A" or "F" "B";
+"F" fdep "E" "C" "D";
+"B" wsp "C" "D";
+"C" lambda=1 dorm=0;
+"D" lambda=1 dorm=0.5;
+"E" lambda=0.5 dorm=0;

resources/examples/testfiles/dft/fdep5.dft

@@ -0,0 +1,7 @@
+toplevel "A";
+"A" and "B" "C" "D" "E";
+"F" fdep "B" "C" "D";
+"B" lambda=0.5 dorm=0;
+"C" lambda=0.5 dorm=0;
+"D" lambda=0.5 dorm=0;
+"E" lambda=0.5 dorm=0;

resources/examples/testfiles/dft/or.dft

@@ -0,0 +1,4 @@
+toplevel "A";
+"A" or "B" "C";
+"B" lambda=0.5 dorm=0.3;
+"C" lambda=0.5 dorm=0.3;

resources/examples/testfiles/dft/pand.dft

@@ -0,0 +1,4 @@
+toplevel "A";
+"A" pand "B" "C";
+"B" lambda=0.4 dorm=0.3;
+"C" lambda=0.2 dorm=0.3;

resources/examples/testfiles/dft/pdep.dft

@@ -0,0 +1,12 @@
+// From Junges2015
+// Example 3.19
+
+toplevel "SF";
+"SF" or "A" "B" "PDEP";
+"A" pand "S" "MA";
+"B" and "MA" "MB";
+"PDEP" pdep=0.2 "MA" "S";
+
+"S" lambda=0.5 dorm=0;
+"MA" lambda=0.5 dorm=0;
+"MB" lambda=0.5 dorm=0;

resources/examples/testfiles/dft/pdep2.dft

@@ -0,0 +1,9 @@
+toplevel "SF";
+"SF" or "A" "B" "PDEP";
+"A" pand "S" "MA";
+"B" and "MA" "MB";
+"PDEP" pdep=0.2 "MA" "S" "MB";
+
+"S" lambda=0.5 dorm=0;
+"MA" lambda=0.5 dorm=0;
+"MB" lambda=0.5 dorm=0;

resources/examples/testfiles/dft/pdep3.dft

@@ -0,0 +1,5 @@
+toplevel "A";
+"A" and "B" "C" "F";
+"F" pdep=0.3 "B" "C";
+"B" lambda=0.4 dorm=0;
+"C" lambda=0.8 dorm=0;

resources/examples/testfiles/dft/pdep4.dft

@@ -0,0 +1,7 @@
+toplevel "SF";
+"SF" pand "S" "A" "B";
+"PDEP" pdep=0.2 "S" "A" "B";
+
+"S" lambda=0.5 dorm=0;
+"A" lambda=0.5 dorm=0;
+"B" lambda=0.5 dorm=0;

resources/examples/testfiles/dft/por.dft

@@ -0,0 +1,5 @@
+toplevel "A";
+"A" por "B" "C" "D";
+"B" lambda=0.4 dorm=0.0;
+"C" lambda=0.2 dorm=0.0;
+"D" lambda=0.2 dorm=0.0;

resources/examples/testfiles/dft/seq.dft

@@ -0,0 +1,5 @@
+toplevel "A";
+"A" and "B" "C";
+"X" seq "B" "C";
+"B" lambda=0.5 dorm=0.3;
+"C" lambda=0.5 dorm=0.3;

resources/examples/testfiles/dft/seq2.dft

@@ -0,0 +1,6 @@
+toplevel "A";
+"A" and "B" "C" "D";
+"X" seq "B" "C" "D";
+"B" lambda=0.5 dorm=0.3;
+"C" lambda=0.5 dorm=0.3;
+"D" lambda=0.5 dorm=0.3;

resources/examples/testfiles/dft/seq3.dft

@@ -0,0 +1,6 @@
+toplevel "A";
+"A" and "C" "D";
+"X" seq "B" "C" "D";
+"B" lambda=0.5 dorm=0.3;
+"C" lambda=0.5 dorm=0.3;
+"D" lambda=0.5 dorm=0.3;

resources/examples/testfiles/dft/seq4.dft

@@ -0,0 +1,7 @@
+toplevel "A";
+"A" and "T1" "B3";
+"T1" or "B1" "B2";
+"X" seq "B1" "B2" "B3";
+"B1" lambda=0.5 dorm=0.3;
+"B2" lambda=0.5 dorm=0.3;
+"B3" lambda=0.5 dorm=0.3;

resources/examples/testfiles/dft/seq5.dft

@@ -0,0 +1,9 @@
+toplevel "A";
+"A" and "T1" "T2";
+"T1" pand "B1" "B2"; 
+"T2" pand "B3" "B4";
+"X" seq "B4" "B3";
+"B1" lambda=0.7 dorm=0.3;
+"B2" lambda=0.5 dorm=0.3;
+"B3" lambda=0.5 dorm=0.3;
+"B4" lambda=0.7 dorm=0.3;

resources/examples/testfiles/dft/spare.dft

@@ -0,0 +1,5 @@
+toplevel "A";
+"A" wsp "I" "M";
+"I" lambda=0.5 dorm=0.3;
+"M" lambda=0.5 dorm=0.3;
+

resources/examples/testfiles/dft/spare2.dft

@@ -0,0 +1,8 @@
+toplevel "A";
+"A" or "B" "C";
+"B" wsp "I" "J";
+"C" wsp "M" "J";
+"I" lambda=0.5 dorm=0.3;
+"J" lambda=0.5 dorm=0.3;
+"M" lambda=0.5 dorm=0.3;
+

resources/examples/testfiles/dft/spare3.dft

@@ -0,0 +1,10 @@
+toplevel "A";
+"A" or "B" "C" "D";
+"B" wsp "I" "M";
+"C" wsp "J" "M";
+"D" wsp "K" "M";
+"I" lambda=0.5 dorm=0.3;
+"J" lambda=0.5 dorm=0.3;
+"K" lambda=0.5 dorm=0.3;
+"M" lambda=0.5 dorm=0.3;
+

resources/examples/testfiles/dft/spare4.dft

@@ -0,0 +1,9 @@
+toplevel "A";
+"A" and "B" "C";
+"B" wsp "I" "J" "K";
+"C" wsp "M" "J";
+"I" lambda=0.5 dorm=0.3;
+"J" lambda=0.5 dorm=0.3;
+"K" lambda=0.5 dorm=0.3;
+"M" lambda=0.5 dorm=0.3;
+

resources/examples/testfiles/dft/spare5.dft

@@ -0,0 +1,9 @@
+toplevel "A";
+"A" wsp "I" "B";
+"B" or "C" "J";
+"C" or "K" "L";
+"I" lambda=0.5 dorm=0;
+"J" lambda=0.5 dorm=0;
+"K" lambda=0.5 dorm=0;
+"L" lambda=0.5 dorm=0;
+

resources/examples/testfiles/dft/spare6.dft

@@ -0,0 +1,7 @@
+toplevel "A";
+"A" or "I" "B";
+"B" wsp "J" "M";
+"I" lambda=0.5 dorm=0.5;
+"J" lambda=0.5 dorm=0.5;
+"M" lambda=0.5 dorm=0.5;
+

resources/examples/testfiles/dft/spare7.dft

@@ -0,0 +1,5 @@
+toplevel "A";
+"A" wsp "K" "J" "I";
+"I" lambda=0.5 dorm=0.5;
+"J" lambda=1 dorm=0.5;
+"K" lambda=0.5 dorm=0.5;

resources/examples/testfiles/dft/spare8.dft

@@ -0,0 +1,7 @@
+toplevel "A";
+"A" wsp "I" "B";
+"B" wsp "J" "K";
+"I" lambda=0.5 dorm=0.3;
+"J" lambda=0.5 dorm=0.3;
+"K" lambda=0.5 dorm=0.3;
+

resources/examples/testfiles/dft/voting.dft

@@ -0,0 +1,5 @@
+toplevel "A";
+"A" 1of3 "B" "C" "D";
+"B" lambda=0.1 dorm=0;
+"C" lambda=0.2 dorm=0;
+"D" lambda=0.3 dorm=0;

resources/examples/testfiles/dft/voting2.dft

@@ -0,0 +1,5 @@
+toplevel "A";
+"A" 1of3 "B" "C" "D";
+"B" lambda=0.3 dorm=0;
+"C" lambda=0.4 dorm=0;
+"D" lambda=1 dorm=0;

resources/examples/testfiles/dft/voting3.dft

@@ -0,0 +1,5 @@
+toplevel "A";
+"A" 2of3 "B" "C" "D";
+"B" lambda=0.3 dorm=0;
+"C" lambda=0.4 dorm=0;
+"D" lambda=1 dorm=0;

resources/examples/testfiles/dft/voting4.dft

@@ -0,0 +1,6 @@
+toplevel "A";
+"A" 2of3 "B" "C" "D";
+"D" or "E";
+"B" lambda=1 dorm=0.0;
+"C" lambda=1 dorm=0.0;
+"E" lambda=1 dorm=0.0;

resources/examples/testfiles/ma/jobscheduler.drn

@@ -0,0 +1,71 @@
+// Exported by storm
+// Original model type: Markov Automaton
+@type: Markov Automaton
+@parameters
+
+@reward_models
+avg_waiting_time 
+@nr_states
+17
+@model
+state 0 !0 [1] init
+	action 0 [0]
+		1 : 1
+	action 1 [0]
+		2 : 1
+	action 2 [0]
+		3 : 1
+state 1 !3 [1]
+	action 0 [0]
+		4 : 0.333333
+		5 : 0.666667
+state 2 !4 [1]
+	action 0 [0]
+		4 : 0.25
+		6 : 0.75
+state 3 !5 [1]
+	action 0 [0]
+		5 : 0.4
+		6 : 0.6
+state 4 !0 [0.666667] one_job_finished slowest_before_fastest
+	action 0 [0]
+		7 : 1
+state 5 !0 [0.666667] one_job_finished
+	action 0 [0]
+		8 : 1
+state 6 !0 [0.666667] one_job_finished
+	action 0 [0]
+		9 : 1
+state 7 !5 [0.666667] one_job_finished slowest_before_fastest
+	action 0 [0]
+		10 : 0.4
+		11 : 0.6
+state 8 !4 [0.666667] one_job_finished
+	action 0 [0]
+		10 : 0.25
+		12 : 0.75
+state 9 !3 [0.666667] one_job_finished
+	action 0 [0]
+		11 : 0.333333
+		12 : 0.666667
+state 10 !0 [0.333333] half_of_jobs_finished slowest_before_fastest
+	action 0 [0]
+		13 : 1
+state 11 !0 [0.333333] half_of_jobs_finished
+	action 0 [0]
+		14 : 1
+state 12 !0 [0.333333] half_of_jobs_finished
+	action 0 [0]
+		15 : 1
+state 13 !3 [0.333333] half_of_jobs_finished slowest_before_fastest
+	action 0 [0]
+		16 : 1
+state 14 !2 [0.333333] half_of_jobs_finished
+	action 0 [0]
+		16 : 1
+state 15 !1 [0.333333] half_of_jobs_finished
+	action 0 [0]
+		16 : 1
+state 16 !1 [0] all_jobs_finished deadlock
+	action 0 [0]
+		16 : 1

resources/examples/testfiles/ma/simple2.ma

@@ -0,0 +1,42 @@
+
+ma
+
+
+module main
+	
+	s : [0..5]; // current state:
+	
+	
+	<> s=0 -> 4 : (s'=1) + 4 : (s'=2);
+	[alpha] s=1 -> 1 : (s'=0);
+	[beta] s=1 -> 0.3 : (s'=5) + 0.7 : (s'=1);
+	<> s=5 -> 1 : (s'=2);
+	[gamma] s=2 -> 1 : (s'=1);
+	[delta] s=2 -> 0.5 : (s'=2) + 0.5 : (s'=3);
+	<> s=3 -> 1 : (s'=4);
+	[lambda] s=4 -> 1 : (s'=3);
+	
+endmodule
+
+rewards "rew0"
+	[delta] s=2 : 1;
+endrewards
+
+rewards "rew1"
+	s=0 : 7;
+	[delta] s=2 : 1;
+endrewards
+
+
+rewards "rew2"
+	s=0 : 7;
+	[delta] s=2 : 1;
+	[lambda] s=4 : 100;
+endrewards
+
+rewards "rew3"
+	s=0 : 7;
+	[delta] s=2 : 1;
+	[gamma] s=2 : 100;
+	[lambda] s=4 : 27;
+endrewards

resources/examples/testfiles/mdp/prism-mec-example1.nm

@@ -0,0 +1,12 @@
+mdp
+
+module test
+
+	x : [0..2];
+	
+	[] x=0 -> true;
+	[] x=0 -> 0.5 : (x'=1) + 0.5: (x'=2);
+	[] x=1 -> (x'=0);
+	[] x=2 -> true;
+	
+endmodule 

resources/examples/testfiles/mdp/prism-mec-example2.nm

@@ -0,0 +1,13 @@
+mdp
+
+module test
+
+	x : [0..2];
+	
+	[] x=0 -> true;
+	[] x=0 -> 0.5 : (x'=1) + 0.5: (x'=1);
+	[] x=0 -> (x'=2);
+	[] x=1 -> (x'=0);
+	[] x=2 -> true;
+	
+endmodule 

resources/examples/testfiles/mdp/two_dice.drn

@@ -3,6 +3,8 @@
 @type: MDP
 @parameters
 
+@reward_models
+coinflips 
 @nr_states
 169
 @model

src/CMakeLists.txt

@@ -5,6 +5,8 @@ set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
 add_custom_target(binaries)
 
 add_subdirectory(storm)
+add_subdirectory(storm-counterexamples)
+add_subdirectory(storm-parsers)
 add_subdirectory(storm-cli-utilities)
 add_subdirectory(storm-pgcl)
 add_subdirectory(storm-pgcl-cli)
@@ -17,6 +19,8 @@ add_subdirectory(storm-pars-cli)
 add_subdirectory(storm-pomdp)
 add_subdirectory(storm-pomdp-cli)
 
+add_subdirectory(storm-conv)
+add_subdirectory(storm-conv-cli)
 
 
 add_subdirectory(test)

src/storm-cli-utilities/CMakeLists.txt

@@ -17,7 +17,7 @@ set_target_properties(storm-cli-utilities PROPERTIES DEFINE_SYMBOL "")
 list(APPEND STORM_TARGETS storm-cli-utilities)
 set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
 
-target_link_libraries(storm-cli-utilities PUBLIC storm)
+target_link_libraries(storm-cli-utilities PUBLIC storm storm-counterexamples storm-parsers)
 
 # Install storm headers to include directory.
 foreach(HEADER ${STORM_CLI_UTIL_HEADERS})
@@ -36,5 +36,5 @@ add_custom_target(copy_storm_cli_util_headers DEPENDS ${STORM_CLI_UTIL_OUTPUT_HE
 add_dependencies(storm-cli-utilities copy_storm_pars_headers)
 
 # installation
-install(TARGETS storm-cli-utilities RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
+install(TARGETS storm-cli-utilities EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
 

src/storm-cli-utilities/cli.cpp

@@ -11,6 +11,7 @@
 
 #include <type_traits>
 #include <ctime>
+#include <boost/algorithm/string/replace.hpp>
 
 #include "storm-cli-utilities/model-handling.h"
 
@@ -48,6 +49,8 @@ namespace storm {
             storm::cli::printHeader("Storm", argc, argv);
             storm::settings::initializeAll("Storm", "storm");
 
+            storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>();
+
             storm::utility::Stopwatch totalTimer(true);
             if (!storm::cli::parseOptions(argc, argv)) {
                 return -1;
@@ -64,6 +67,26 @@ namespace storm {
             return 0;
         }
 
+        std::string shellQuoteSingleIfNecessary(const std::string& arg) {
+            // quote empty argument
+            if (arg.empty()) {
+                return "''";
+            }
+
+            if (arg.find_first_not_of("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789-_./=") != std::string::npos) {
+                // contains potentially unsafe character, needs quoting
+                if (arg.find('\'') != std::string::npos) {
+                    // contains ', we have to replace all ' with '\''
+                    std::string escaped(arg);
+                    boost::replace_all(escaped, "'", "'\\''");
+                    return "'" + escaped + "'";
+                } else {
+                    return "'" + arg + "'";
+                }
+            }
+
+            return arg;
+        }
         
         void printHeader(std::string const& name, const int argc, const char** argv) {
             STORM_PRINT(name << " " << storm::utility::StormVersion::shortVersionString() << std::endl << std::endl);
@@ -71,7 +94,7 @@ namespace storm {
             // "Compute" the command line argument string with which storm was invoked.
             std::stringstream commandStream;
             for (int i = 1; i < argc; ++i) {
-                commandStream << argv[i] << " ";
+                commandStream << " " << shellQuoteSingleIfNecessary(argv[i]);
             }
             
             std::string command = commandStream.str();
@@ -79,7 +102,7 @@ namespace storm {
             if (!command.empty()) {
                 std::time_t result = std::time(nullptr);
                 STORM_PRINT("Date: " << std::ctime(&result));
-                STORM_PRINT("Command line arguments: " << commandStream.str() << std::endl);
+                STORM_PRINT("Command line arguments:" << commandStream.str() << std::endl);
                 STORM_PRINT("Current working directory: " << storm::utility::cli::getCurrentWorkingDirectory() << std::endl << std::endl);
             }
         }

src/storm-cli-utilities/cli.h

@@ -11,6 +11,13 @@ namespace storm {
          */
         int64_t process(const int argc, const char** argv);
 
+        /*!
+         * For a command-line argument, returns a quoted version
+         * with single quotes if it contains unsafe characters.
+         * Otherwise, just returns the unquoted argument.
+         */
+        std::string shellQuoteSingleIfNecessary(const std::string& arg);
+
         void printHeader(std::string const& name, const int argc, const char** argv);
         
         void printVersion(std::string const& name);

src/storm-cli-utilities/model-handling.h

@@ -2,10 +2,14 @@
 
 #include "storm/api/storm.h"
 
+#include "storm-counterexamples/api/counterexamples.h"
+#include "storm-parsers/api/storm-parsers.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/NumberTraits.h"
 
 #include "storm/utility/initialize.h"
 #include "storm/utility/Stopwatch.h"
@@ -14,6 +18,9 @@
 
 
 #include "storm/storage/SymbolicModelDescription.h"
+#include "storm/storage/jani/Property.h"
+
+#include "storm/builder/BuilderType.h"
 
 #include "storm/models/ModelBase.h"
 
@@ -34,7 +41,6 @@
 #include "storm/settings/modules/CoreSettings.h"
 #include "storm/settings/modules/AbstractionSettings.h"
 #include "storm/settings/modules/ResourceSettings.h"
-#include "storm/settings/modules/JaniExportSettings.h"
 
 #include "storm/utility/Stopwatch.h"
 
@@ -53,21 +59,26 @@ namespace storm {
             boost::optional<std::vector<storm::jani::Property>> preprocessedProperties;
         };
         
-        void parseSymbolicModelDescription(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input) {
+        void parseSymbolicModelDescription(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input, storm::builder::BuilderType const& builderType) {
             if (ioSettings.isPrismOrJaniInputSet()) {
                 if (ioSettings.isPrismInputSet()) {
                     input.model = storm::api::parseProgram(ioSettings.getPrismInputFilename(), storm::settings::getModule<storm::settings::modules::BuildSettings>().isPrismCompatibilityEnabled());
                 } else {
-                    auto janiInput = storm::api::parseJaniModel(ioSettings.getJaniInputFilename());
-                    input.model = janiInput.first;
-                    auto const& janiPropertyInput = janiInput.second;
-                    
+                    storm::jani::ModelFeatures supportedFeatures = storm::api::getSupportedJaniFeatures(builderType);
+                    boost::optional<std::vector<std::string>> propertyFilter;
                     if (ioSettings.isJaniPropertiesSet()) {
-                        for (auto const& propName : ioSettings.getJaniProperties()) {
-                            auto propertyIt = janiPropertyInput.find(propName);
-                            STORM_LOG_THROW(propertyIt != janiPropertyInput.end(), storm::exceptions::InvalidArgumentException, "No JANI property with name '" << propName << "' is known.");
-                            input.properties.emplace_back(propertyIt->second);
+                        if (ioSettings.areJaniPropertiesSelected()) {
+                            propertyFilter = ioSettings.getSelectedJaniProperties();
+                        } else {
+                            propertyFilter = boost::none;
                         }
+                    } else {
+                        propertyFilter = std::vector<std::string>();
+                    }
+                    auto janiInput = storm::api::parseJaniModel(ioSettings.getJaniInputFilename(), supportedFeatures, propertyFilter);
+                    input.model = std::move(janiInput.first);
+                    if (ioSettings.isJaniPropertiesSet()) {
+                        input.properties = std::move(janiInput.second);
                     }
                 }
             }
@@ -86,23 +97,21 @@ namespace storm {
             }
         }
         
-        SymbolicInput parseSymbolicInput() {
+        SymbolicInput parseSymbolicInput(storm::builder::BuilderType const& builderType) {
             auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
             
             // Parse the property filter, if any is given.
             boost::optional<std::set<std::string>> propertyFilter = storm::api::parsePropertyFilter(ioSettings.getPropertyFilter());
             
             SymbolicInput input;
-            parseSymbolicModelDescription(ioSettings, input);
+            parseSymbolicModelDescription(ioSettings, input, builderType);
             parseProperties(ioSettings, input, propertyFilter);
             
             return input;
         }
         
-        SymbolicInput preprocessSymbolicInput(SymbolicInput const& input) {
+        SymbolicInput preprocessSymbolicInput(SymbolicInput const& input, storm::builder::BuilderType const& builderType) {
             auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
-            auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
-            auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
             
             SymbolicInput output = input;
             
@@ -117,25 +126,33 @@ namespace storm {
                 output.properties = storm::api::substituteConstantsInProperties(output.properties, constantDefinitions);
             }
             
+            // Make sure there are no undefined constants remaining in any property.
+            for (auto const& property : output.properties) {
+                std::set<storm::expressions::Variable> usedUndefinedConstants = property.getUndefinedConstants();
+                if (!usedUndefinedConstants.empty()) {
+                    std::vector<std::string> undefinedConstantsNames;
+                    for (auto const& constant : usedUndefinedConstants) {
+                        undefinedConstantsNames.emplace_back(constant.getName());
+                    }
+
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The property '" << property << " still refers to the undefined constants " << boost::algorithm::join(undefinedConstantsNames, ",") << ".");
+                }
+            }
+            
             // 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 && buildSettings.isJitSet();
+                bool transformToJaniForJit = builderType == storm::builder::BuilderType::Jit;
                 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<std::string, std::string> const& labelRenaming = modelAndRenaming.second;
-                        std::vector<storm::jani::Property> amendedProperties;
-                        for (auto const& property : output.properties) {
-                            amendedProperties.emplace_back(property.substituteLabels(labelRenaming));
-                        }
-                        output.preprocessedProperties = std::move(amendedProperties);
+                    auto modelAndProperties = model.toJani(output.properties);
+                    output.model = modelAndProperties.first;
+                    
+                    if (!modelAndProperties.second.empty()) {
+                        output.preprocessedProperties = std::move(modelAndProperties.second);
                     }
                 }
             }
@@ -150,16 +167,32 @@ namespace storm {
                 if (ioSettings.isExportJaniDotSet()) {
                     storm::api::exportJaniModelAsDot(model.asJaniModel(), ioSettings.getExportJaniDotFilename());
                 }
+            }
+        }
         
-                if (model.isJaniModel() && storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) {
-                    storm::api::exportJaniModel(model.asJaniModel(), input.properties, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
+        storm::builder::BuilderType getBuilderType(storm::settings::modules::CoreSettings::Engine const& engine, bool useJit) {
+            if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::DdSparse || engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) {
+                return storm::builder::BuilderType::Dd;
+            } else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) {
+                if (useJit) {
+                    return storm::builder::BuilderType::Jit;
+                } else {
+                    return storm::builder::BuilderType::Explicit;
                 }
+            } else if (engine == storm::settings::modules::CoreSettings::Engine::Exploration) {
+                return storm::builder::BuilderType::Explicit;
             }
+            STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to determine the model builder type.");
         }
         
         SymbolicInput parseAndPreprocessSymbolicInput() {
-            SymbolicInput input = parseSymbolicInput();
-            input = preprocessSymbolicInput(input);
+            // Get the used builder type to handle cases where preprocessing depends on it
+            auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
+            auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
+            auto builderType = getBuilderType(coreSettings.getEngine(), buildSettings.isJitSet());
+            
+            SymbolicInput input = parseSymbolicInput(builderType);
+            input = preprocessSymbolicInput(input, builderType);
             exportSymbolicInput(input);
             return input;
         }
@@ -183,13 +216,18 @@ namespace storm {
         
         template <typename ValueType>
         std::shared_ptr<storm::models::ModelBase> buildModelSparse(SymbolicInput const& input, storm::settings::modules::BuildSettings const& buildSettings) {
-            auto counterexampleGeneratorSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
             storm::builder::BuilderOptions options(createFormulasToRespect(input.properties));
             options.setBuildChoiceLabels(buildSettings.isBuildChoiceLabelsSet());
             options.setBuildStateValuations(buildSettings.isBuildStateValuationsSet());
-            options.setBuildChoiceOrigins(counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet());
+            if (storm::settings::manager().hasModule(storm::settings::modules::CounterexampleGeneratorSettings::moduleName)) {
+                auto counterexampleGeneratorSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
+                options.setBuildChoiceOrigins(counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet());
+            } else {
+                options.setBuildChoiceOrigins(false);
+            }
             options.setBuildAllLabels(buildSettings.isBuildFullModelSet());
             options.setBuildAllRewardModels(buildSettings.isBuildFullModelSet());
+            options.setAddOutOfBoundsState(buildSettings.isBuildOutOfBoundsStateSet());
             if (buildSettings.isBuildFullModelSet()) {
                 options.clearTerminalStates();
             }
@@ -217,9 +255,10 @@ namespace storm {
             auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
             std::shared_ptr<storm::models::ModelBase> result;
             if (input.model) {
-                if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) {
+                auto builderType = getBuilderType(engine, buildSettings.isJitSet());
+                if (builderType == storm::builder::BuilderType::Dd) {
                     result = buildModelDd<DdType, ValueType>(input);
-                } else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) {
+                } else if (builderType == storm::builder::BuilderType::Explicit || builderType == storm::builder::BuilderType::Jit) {
                     result = buildModelSparse<ValueType>(input, buildSettings);
                 }
             } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet() || ioSettings.isExplicitIMCASet()) {
@@ -322,43 +361,60 @@ namespace storm {
             }
         }
         
-        template <storm::dd::DdType DdType, typename ValueType>
-        std::shared_ptr<storm::models::Model<ValueType>> preprocessDdModelBisimulation(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input, storm::settings::modules::BisimulationSettings const& bisimulationSettings) {
+        template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
+        std::shared_ptr<storm::models::Model<ExportValueType>> preprocessDdModelBisimulation(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> 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.");
             
             STORM_LOG_INFO("Performing bisimulation minimization...");
-            return storm::api::performBisimulationMinimization<DdType, ValueType>(model, createFormulasToRespect(input.properties), storm::storage::BisimulationType::Strong, bisimulationSettings.getSignatureMode());
+            return storm::api::performBisimulationMinimization<DdType, ValueType, ExportValueType>(model, createFormulasToRespect(input.properties), storm::storage::BisimulationType::Strong, bisimulationSettings.getSignatureMode());
         }
         
-        template <storm::dd::DdType DdType, typename ValueType>
+        template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
         std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessDdModel(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input) {
             auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
             auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
-            std::pair<std::shared_ptr<storm::models::Model<ValueType>>, bool> result = std::make_pair(model, false);
+            std::pair<std::shared_ptr<storm::models::Model<ValueType>>, bool> intermediateResult = std::make_pair(model, false);
             
             if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
-                result.first = preprocessDdMarkovAutomaton(result.first->template as<storm::models::symbolic::Model<DdType, ValueType>>());
-                result.second = true;
+                intermediateResult.first = preprocessDdMarkovAutomaton(intermediateResult.first->template as<storm::models::symbolic::Model<DdType, ValueType>>());
+                intermediateResult.second = true;
             }
             
+            std::unique_ptr<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>, bool>> result;
+            auto symbolicModel = intermediateResult.first->template as<storm::models::symbolic::Model<DdType, ValueType>>();
             if (generalSettings.isBisimulationSet()) {
-                result.first = preprocessDdModelBisimulation(model, input, bisimulationSettings);
-                result.second = true;
+                std::shared_ptr<storm::models::Model<ExportValueType>> newModel = preprocessDdModelBisimulation<DdType, ValueType, ExportValueType>(symbolicModel, input, bisimulationSettings);
+                result = std::make_unique<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>, bool>>(newModel, true);
+            } else {
+                result = std::make_unique<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>, bool>>(symbolicModel->template toValueType<ExportValueType>(), !std::is_same<ValueType, ExportValueType>::value);
             }
             
-            return result;
+            if (result && result->first->isSymbolicModel() && storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::DdSparse) {
+                // Mark as changed.
+                result->second = true;
+                
+                std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> symbolicModel = result->first->template as<storm::models::symbolic::Model<DdType, ExportValueType>>();
+                std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
+                for (auto const& property : input.properties) {
+                    formulas.emplace_back(property.getRawFormula());
+                }
+                result->first = storm::api::transformSymbolicToSparseModel(symbolicModel, formulas);
+                STORM_LOG_THROW(result, storm::exceptions::NotSupportedException, "The translation to a sparse model is not supported for the given model type.");
+            }
+            
+            return *result;
         }
         
-        template <storm::dd::DdType DdType, typename ValueType>
+        template <storm::dd::DdType DdType, typename BuildValueType, typename ExportValueType = BuildValueType>
         std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
             storm::utility::Stopwatch preprocessingWatch(true);
             
             std::pair<std::shared_ptr<storm::models::ModelBase>, bool> result = std::make_pair(model, false);
             if (model->isSparseModel()) {
-                result = preprocessSparseModel<ValueType>(result.first->as<storm::models::sparse::Model<ValueType>>(), input);
+                result = preprocessSparseModel<BuildValueType>(result.first->as<storm::models::sparse::Model<BuildValueType>>(), input);
             } else {
                 STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type.");
-                result = preprocessDdModel<DdType, ValueType>(result.first->as<storm::models::symbolic::Model<DdType, ValueType>>(), input);
+                result = preprocessDdModel<DdType, BuildValueType, ExportValueType>(result.first->as<storm::models::symbolic::Model<DdType, BuildValueType>>(), input);
             }
             
             preprocessingWatch.stop();
@@ -395,6 +451,9 @@ namespace storm {
             
             STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::NotSupportedException, "Counterexample generation is currently only supported for sparse models.");
             auto sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
+            for (auto& rewModel : sparseModel->getRewardModels()) {
+                rewModel.second.reduceToStateBasedRewards(sparseModel->getTransitionMatrix(), true);
+            }
 
             STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc) || sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample is currently only supported for discrete-time models.");
             
@@ -429,29 +488,38 @@ namespace storm {
         template<typename ValueType>
         void printFilteredResult(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::modelchecker::FilterType ft) {
             if (result->isQuantitative()) {
-                switch (ft) {
-                    case storm::modelchecker::FilterType::VALUES:
-                        STORM_PRINT(*result);
-                        break;
-                    case storm::modelchecker::FilterType::SUM:
-                        STORM_PRINT(result->asQuantitativeCheckResult<ValueType>().sum());
-                        break;
-                    case storm::modelchecker::FilterType::AVG:
-                        STORM_PRINT(result->asQuantitativeCheckResult<ValueType>().average());
-                        break;
-                    case storm::modelchecker::FilterType::MIN:
-                        STORM_PRINT(result->asQuantitativeCheckResult<ValueType>().getMin());
-                        break;
-                    case storm::modelchecker::FilterType::MAX:
-                        STORM_PRINT(result->asQuantitativeCheckResult<ValueType>().getMax());
-                        break;
-                    case storm::modelchecker::FilterType::ARGMIN:
-                    case storm::modelchecker::FilterType::ARGMAX:
-                        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Outputting states is not supported.");
-                    case storm::modelchecker::FilterType::EXISTS:
-                    case storm::modelchecker::FilterType::FORALL:
-                    case storm::modelchecker::FilterType::COUNT:
-                        STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Filter type only defined for qualitative results.");
+                if (ft == storm::modelchecker::FilterType::VALUES) {
+                    STORM_PRINT(*result);
+                } else {
+                    ValueType resultValue;
+                    switch (ft) {
+                        case storm::modelchecker::FilterType::SUM:
+                            resultValue = result->asQuantitativeCheckResult<ValueType>().sum();
+                            break;
+                        case storm::modelchecker::FilterType::AVG:
+                            resultValue = result->asQuantitativeCheckResult<ValueType>().average();
+                            break;
+                        case storm::modelchecker::FilterType::MIN:
+                            resultValue = result->asQuantitativeCheckResult<ValueType>().getMin();
+                            break;
+                        case storm::modelchecker::FilterType::MAX:
+                            resultValue = result->asQuantitativeCheckResult<ValueType>().getMax();
+                            break;
+                        case storm::modelchecker::FilterType::ARGMIN:
+                        case storm::modelchecker::FilterType::ARGMAX:
+                            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Outputting states is not supported.");
+                        case storm::modelchecker::FilterType::EXISTS:
+                        case storm::modelchecker::FilterType::FORALL:
+                        case storm::modelchecker::FilterType::COUNT:
+                            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Filter type only defined for qualitative results.");
+                        default:
+                            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unhandled filter type.");
+                    }
+                    if (storm::NumberTraits<ValueType>::IsExact && storm::utility::isConstant(resultValue)) {
+                        STORM_PRINT(resultValue << " (approx. " << storm::utility::convertNumber<double>(resultValue) << ")");
+                    } else {
+                        STORM_PRINT(resultValue);
+                    }
                 }
             } else {
                 switch (ft) {
@@ -481,7 +549,7 @@ namespace storm {
         }
         
         void printModelCheckingProperty(storm::jani::Property const& property) {
-            STORM_PRINT(std::endl << "Model checking property " << *property.getRawFormula() << " ..." << std::endl);
+            STORM_PRINT(std::endl << "Model checking property \"" << property.getName() << "\": " << *property.getRawFormula() << " ..." << std::endl);
         }
         
         template<typename ValueType>
@@ -518,12 +586,85 @@ namespace storm {
             }
         }
         
+        std::vector<storm::expressions::Expression> parseConstraints(storm::expressions::ExpressionManager const& expressionManager, std::string const& constraintsString) {
+            std::vector<storm::expressions::Expression> constraints;
+            
+            std::vector<std::string> constraintsAsStrings;
+            boost::split(constraintsAsStrings, constraintsString, boost::is_any_of(","));
+            
+            storm::parser::ExpressionParser expressionParser(expressionManager);
+            std::unordered_map<std::string, storm::expressions::Expression> variableMapping;
+            for (auto const& variableTypePair : expressionManager) {
+                variableMapping[variableTypePair.first.getName()] = variableTypePair.first;
+            }
+            expressionParser.setIdentifierMapping(variableMapping);
+            
+            for (auto const& constraintString : constraintsAsStrings) {
+                if (constraintString.empty()) {
+                    continue;
+                }
+
+                storm::expressions::Expression constraint = expressionParser.parseFromString(constraintString);
+                STORM_LOG_TRACE("Adding special (user-provided) constraint " << constraint << ".");
+                constraints.emplace_back(constraint);
+            }
+            
+            return constraints;
+        }
+        
+        std::vector<std::vector<storm::expressions::Expression>> parseInjectedRefinementPredicates(storm::expressions::ExpressionManager const& expressionManager, std::string const& refinementPredicatesString) {
+            std::vector<std::vector<storm::expressions::Expression>> injectedRefinementPredicates;
+            
+            storm::parser::ExpressionParser expressionParser(expressionManager);
+            std::unordered_map<std::string, storm::expressions::Expression> variableMapping;
+            for (auto const& variableTypePair : expressionManager) {
+                variableMapping[variableTypePair.first.getName()] = variableTypePair.first;
+            }
+            expressionParser.setIdentifierMapping(variableMapping);
+            
+            std::vector<std::string> predicateGroupsAsStrings;
+            boost::split(predicateGroupsAsStrings, refinementPredicatesString, boost::is_any_of(";"));
+            
+            if (!predicateGroupsAsStrings.empty()) {
+                for (auto const& predicateGroupString : predicateGroupsAsStrings) {
+                    if (predicateGroupString.empty()) {
+                        continue;
+                    }
+                    
+                    std::vector<std::string> predicatesAsStrings;
+                    boost::split(predicatesAsStrings, predicateGroupString, boost::is_any_of(":"));
+                    
+                    if (!predicatesAsStrings.empty()) {
+                        injectedRefinementPredicates.emplace_back();
+                        for (auto const& predicateString : predicatesAsStrings) {
+                            storm::expressions::Expression predicate = expressionParser.parseFromString(predicateString);
+                            STORM_LOG_TRACE("Adding special (user-provided) refinement predicate " << predicateString << ".");
+                            injectedRefinementPredicates.back().emplace_back(predicate);
+                        }
+                        
+                        STORM_LOG_THROW(!injectedRefinementPredicates.back().empty(), storm::exceptions::InvalidArgumentException, "Expecting non-empty list of predicates to inject for each (mentioned) refinement step.");
+                        
+                        // Finally reverse the list, because we take the predicates from the back.
+                        std::reverse(injectedRefinementPredicates.back().begin(), injectedRefinementPredicates.back().end());
+                    }
+                }
+                
+                // Finally reverse the list, because we take the predicates from the back.
+                std::reverse(injectedRefinementPredicates.begin(), injectedRefinementPredicates.end());
+            }
+            
+            return injectedRefinementPredicates;
+        }
+        
         template <storm::dd::DdType DdType, typename ValueType>
         void verifyWithAbstractionRefinementEngine(SymbolicInput const& input) {
             STORM_LOG_ASSERT(input.model, "Expected symbolic model description.");
-            verifyProperties<ValueType>(input, [&input] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+            storm::settings::modules::AbstractionSettings const& abstractionSettings = storm::settings::getModule<storm::settings::modules::AbstractionSettings>();
+            storm::api::AbstractionRefinementOptions options(parseConstraints(input.model->getManager(), abstractionSettings.getConstraintString()), parseInjectedRefinementPredicates(input.model->getManager(), abstractionSettings.getInjectedRefinementPredicates()));
+
+            verifyProperties<ValueType>(input, [&input,&options] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
                 STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states.");
-                return storm::api::verifyWithAbstractionRefinementEngine<DdType, ValueType>(input.model.get(), storm::api::createTask<ValueType>(formula, true));
+                return storm::api::verifyWithAbstractionRefinementEngine<DdType, ValueType>(input.model.get(), storm::api::createTask<ValueType>(formula, true), options);
             });
         }
         
@@ -639,13 +780,13 @@ namespace storm {
             }
         }
         
-        template <storm::dd::DdType DdType, typename ValueType>
+        template <storm::dd::DdType DdType, typename BuildValueType, typename VerificationValueType = BuildValueType>
         std::shared_ptr<storm::models::ModelBase> buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, storm::settings::modules::CoreSettings::Engine engine) {
             auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
             auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
             std::shared_ptr<storm::models::ModelBase> model;
             if (!buildSettings.isNoBuildModelSet()) {
-                model = buildModel<DdType, ValueType>(engine, input, ioSettings);
+                model = buildModel<DdType, BuildValueType>(engine, input, ioSettings);
             }
             
             if (model) {
@@ -655,17 +796,17 @@ namespace storm {
             STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model.");
             
             if (model) {
-                auto preprocessingResult = preprocessModel<DdType, ValueType>(model, input);
+                auto preprocessingResult = preprocessModel<DdType, BuildValueType, VerificationValueType>(model, input);
                 if (preprocessingResult.second) {
                     model = preprocessingResult.first;
                     model->printModelInformationToStream(std::cout);
                 }
-                exportModel<DdType, ValueType>(model, input);
+                exportModel<DdType, BuildValueType>(model, input);
             }
             return model;
         }
         
-        template <storm::dd::DdType DdType, typename ValueType>
+        template <storm::dd::DdType DdType, typename BuildValueType, typename VerificationValueType = BuildValueType>
         void processInputWithValueTypeAndDdlib(SymbolicInput const& input) {
             auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
             auto abstractionSettings = storm::settings::getModule<storm::settings::modules::AbstractionSettings>();
@@ -674,19 +815,19 @@ namespace storm {
             storm::settings::modules::CoreSettings::Engine engine = coreSettings.getEngine();
             
             if (engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement && abstractionSettings.getAbstractionRefinementMethod() == storm::settings::modules::AbstractionSettings::Method::Games) {
-                verifyWithAbstractionRefinementEngine<DdType, ValueType>(input);
+                verifyWithAbstractionRefinementEngine<DdType, VerificationValueType>(input);
             } else if (engine == storm::settings::modules::CoreSettings::Engine::Exploration) {
-                verifyWithExplorationEngine<ValueType>(input);
+                verifyWithExplorationEngine<VerificationValueType>(input);
             } else {
-                std::shared_ptr<storm::models::ModelBase> model = buildPreprocessExportModelWithValueTypeAndDdlib<DdType, ValueType>(input, engine);
+                std::shared_ptr<storm::models::ModelBase> model = buildPreprocessExportModelWithValueTypeAndDdlib<DdType, BuildValueType, VerificationValueType>(input, engine);
 
                 if (model) {
                     if (coreSettings.isCounterexampleSet()) {
                         auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
-                        generateCounterexamples<ValueType>(model, input);
+                        generateCounterexamples<VerificationValueType>(model, input);
                     } else {
                         auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
-                        verifyModel<DdType, ValueType>(model, input, coreSettings);
+                        verifyModel<DdType, VerificationValueType>(model, input, coreSettings);
                     }
                 }
             }
@@ -696,12 +837,16 @@ namespace storm {
         void processInputWithValueType(SymbolicInput const& input) {
             auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
             auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
+            auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
             
             if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD && coreSettings.isDdLibraryTypeSetFromDefaultValue() && generalSettings.isExactSet()) {
                 STORM_LOG_INFO("Switching to DD library sylvan to allow for rational arithmetic.");
-                processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, ValueType>(input);
+                processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalNumber>(input);
+            } else if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD && coreSettings.isDdLibraryTypeSetFromDefaultValue() && std::is_same<ValueType, double>::value && generalSettings.isBisimulationSet() && bisimulationSettings.useExactArithmeticInDdBisimulation()) {
+                STORM_LOG_INFO("Switching to DD library sylvan to allow for rational arithmetic.");
+                processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalNumber, double>(input);
             } else if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD) {
-                processInputWithValueTypeAndDdlib<storm::dd::DdType::CUDD, ValueType>(input);
+                processInputWithValueTypeAndDdlib<storm::dd::DdType::CUDD, double>(input);
             } else {
                 STORM_LOG_ASSERT(coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "Unknown DD library.");
                 processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, ValueType>(input);

src/storm-conv-cli/CMakeLists.txt

@@ -0,0 +1,9 @@
+# Create storm-conv.
+add_executable(storm-conv-cli ${PROJECT_SOURCE_DIR}/src/storm-conv-cli/storm-conv.cpp)
+target_link_libraries(storm-conv-cli storm-conv storm-cli-utilities) # Adding headers for xcode
+set_target_properties(storm-conv-cli PROPERTIES OUTPUT_NAME "storm-conv")
+
+add_dependencies(binaries storm-conv-cli)
+
+# installation
+install(TARGETS storm-conv-cli EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)

src/storm-conv-cli/storm-conv.cpp

@@ -0,0 +1,341 @@
+
+#include "storm-conv/api/storm-conv.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm-conv/settings/ConvSettings.h"
+#include "storm-conv/settings/modules/ConversionGeneralSettings.h"
+#include "storm-conv/settings/modules/ConversionInputSettings.h"
+#include "storm-conv/settings/modules/ConversionOutputSettings.h"
+
+#include "storm/api/storm.h"
+#include "storm-parsers/api/storm-parsers.h"
+#include "storm/utility/initialize.h"
+#include "storm/utility/macros.h"
+#include "storm/utility/Stopwatch.h"
+
+#include "storm/storage/SymbolicModelDescription.h"
+#include "storm/storage/jani/Model.h"
+#include "storm/storage/jani/Property.h"
+
+
+#include "storm-cli-utilities/cli.h"
+#include "storm/exceptions/OptionParserException.h"
+
+namespace storm {
+    namespace conv {
+        
+        void setUrgentOptions() {
+            
+            // Set the correct log level
+            if (storm::settings::getModule<storm::settings::modules::ConversionOutputSettings>().isStdOutOutputEnabled()) {
+                storm::utility::setLogLevel(l3pp::LogLevel::OFF);
+            } else {
+                auto const& general = storm::settings::getModule<storm::settings::modules::ConversionGeneralSettings>();
+                if (general.isVerboseSet()) {
+                    storm::utility::setLogLevel(l3pp::LogLevel::INFO);
+                }
+                if (general.isDebugOutputSet()) {
+                    storm::utility::setLogLevel(l3pp::LogLevel::DEBUG);
+                }
+                if (general.isTraceOutputSet()) {
+                    storm::utility::setLogLevel(l3pp::LogLevel::TRACE);
+                }
+            }
+        }
+        
+        storm::utility::Stopwatch startStopwatch(std::string const& message) {
+            STORM_PRINT_AND_LOG(message);
+            return storm::utility::Stopwatch(true);
+        }
+        
+        void stopStopwatch(storm::utility::Stopwatch& stopWatch) {
+            stopWatch.stop();
+            STORM_PRINT_AND_LOG(" done. (" << stopWatch << " seconds)." << std::endl);
+        }
+        
+        void processPrismInputJaniOutput(storm::prism::Program const& prismProg, std::vector<storm::jani::Property> const& properties) {
+            auto const& output = storm::settings::getModule<storm::settings::modules::ConversionOutputSettings>();
+            auto const& input = storm::settings::getModule<storm::settings::modules::ConversionInputSettings>();
+            auto const& jani = storm::settings::getModule<storm::settings::modules::JaniExportSettings>();
+            
+            auto conversionTime = startStopwatch("Converting PRISM Program to JANI model ... " );
+
+            storm::converter::PrismToJaniConverterOptions options;
+            options.allVariablesGlobal = jani.isGlobalVarsSet();
+            options.suffix = "";
+            options.janiOptions = storm::converter::JaniConversionOptions(jani);
+            options.janiOptions.substituteConstants = true;
+            
+            // Get the name of the output file
+            std::string outputFilename = "";
+            if (output.isJaniOutputFilenameSet()) {
+                outputFilename = output.getJaniOutputFilename();
+            } else if (input.isPrismInputSet() && !output.isStdOutOutputEnabled()) {
+                outputFilename = input.getPrismInputFilename();
+                // Remove extension if present
+                auto dotPos = outputFilename.rfind('.');
+                if (dotPos != std::string::npos) {
+                    outputFilename.erase(dotPos);
+                }
+                std::string suffix = "";
+                if (input.isConstantsSet()) {
+                    suffix = input.getConstantDefinitionString();
+                    std::replace(suffix.begin(), suffix.end(), ',', '_');
+                    std::replace(suffix.begin(), suffix.end(), '=', '-');
+                }
+                suffix = suffix + ".jani";
+                outputFilename += suffix;
+            }
+            
+            // Find a good model name
+            auto startOfFilename = outputFilename.rfind("/");
+            if (startOfFilename == std::string::npos) {
+                startOfFilename = 0;
+            } else {
+                ++startOfFilename;
+            }
+            auto endOfFilename = outputFilename.rfind(".");
+            if (endOfFilename == std::string::npos) {
+                endOfFilename = outputFilename.size();
+            }
+            options.janiOptions.modelName = outputFilename.substr(startOfFilename, endOfFilename - startOfFilename);
+
+            
+            auto janiModelProperties = storm::api::convertPrismToJani(prismProg, properties, options);
+            
+            stopStopwatch(conversionTime);
+            auto exportingTime = startStopwatch("Exporting JANI model ... ");
+            
+            if (outputFilename != "") {
+                storm::api::exportJaniToFile(janiModelProperties.first, janiModelProperties.second, outputFilename, jani.isCompactJsonSet());
+                STORM_PRINT_AND_LOG("Stored to file '" << outputFilename << "'");
+            }
+            
+            if (output.isStdOutOutputEnabled()) {
+                storm::api::printJaniToStream(janiModelProperties.first, janiModelProperties.second, std::cout, jani.isCompactJsonSet());
+            }
+            stopStopwatch(exportingTime);
+        }
+        
+        void processPrismInput() {
+            auto parsingTime = startStopwatch("Parsing PRISM input ... " );
+
+            auto const& input = storm::settings::getModule<storm::settings::modules::ConversionInputSettings>();
+
+            // Parse the prism program
+            storm::storage::SymbolicModelDescription prismProg = storm::api::parseProgram(input.getPrismInputFilename(), input.isPrismCompatibilityEnabled(), false);
+
+            // Parse properties (if available)
+            std::vector<storm::jani::Property> properties;
+            if (input.isPropertyInputSet()) {
+                boost::optional<std::set<std::string>> propertyFilter = storm::api::parsePropertyFilter(input.getPropertyInputFilter());
+                properties = storm::api::parsePropertiesForSymbolicModelDescription(input.getPropertyInput(), prismProg, propertyFilter);
+            }
+            
+            // Set constant definitions in program
+            std::string constantDefinitionString = input.getConstantDefinitionString();
+            auto constantDefinitions = prismProg.parseConstantDefinitions(constantDefinitionString);
+            prismProg = storm::storage::SymbolicModelDescription(prismProg.asPrismProgram().defineUndefinedConstants(constantDefinitions));
+            // Substitution of constants can only be done after conversion in order to preserve formula definitions in which
+            // constants appear that are renamed in some modules...
+            
+            stopStopwatch(parsingTime);
+            
+            // Branch on the type of output
+            auto const& output = storm::settings::getModule<storm::settings::modules::ConversionOutputSettings>();
+            if (output.isJaniOutputSet()) {
+                processPrismInputJaniOutput(prismProg.asPrismProgram(), properties);
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "There is either no outputformat specified or the provided combination of input and output format is not compatible.");
+            }
+        }
+        
+        void processJaniInputJaniOutput(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& properties) {
+            auto conversionTime = startStopwatch("Performing transformations on JANI model ... " );
+
+            auto const& output = storm::settings::getModule<storm::settings::modules::ConversionOutputSettings>();
+            auto const& input = storm::settings::getModule<storm::settings::modules::ConversionInputSettings>();
+            auto const& jani = storm::settings::getModule<storm::settings::modules::JaniExportSettings>();
+            
+            storm::converter::JaniConversionOptions options(jani);
+            
+            // Get the name of the output file
+            std::string outputFilename = "";
+            if (output.isJaniOutputFilenameSet()) {
+                outputFilename = output.getJaniOutputFilename();
+            } else if (input.isJaniInputSet() && !output.isStdOutOutputEnabled()) {
+                outputFilename = input.getJaniInputFilename();
+                // Remove extension if present
+                auto dotPos = outputFilename.rfind('.');
+                if (dotPos != std::string::npos) {
+                    outputFilename.erase(dotPos);
+                }
+                outputFilename += "_converted.jani";
+            }
+            
+            // Get a good model name from the output filename
+            auto startOfFilename = outputFilename.rfind("/");
+            if (startOfFilename == std::string::npos) {
+                startOfFilename = 0;
+            } else {
+                ++startOfFilename;
+            }
+            auto endOfFilename = outputFilename.rfind(".");
+            if (endOfFilename == std::string::npos) {
+                endOfFilename = outputFilename.size();
+            }
+            options.modelName = outputFilename.substr(startOfFilename, endOfFilename - startOfFilename);
+
+            auto transformedJaniModel = janiModel;
+            auto transformedProperties = properties;
+            storm::api::transformJani(transformedJaniModel, transformedProperties, options);
+            
+            stopStopwatch(conversionTime);
+            auto exportingTime = startStopwatch("Exporting JANI model ... ");
+            
+            if (outputFilename != "") {
+                storm::api::exportJaniToFile(transformedJaniModel, transformedProperties, outputFilename, jani.isCompactJsonSet());
+                STORM_PRINT_AND_LOG("Stored to file '" << outputFilename << "'");
+            }
+            
+            if (output.isStdOutOutputEnabled()) {
+                storm::api::printJaniToStream(transformedJaniModel, transformedProperties, std::cout, jani.isCompactJsonSet());
+            }
+            stopStopwatch(exportingTime);
+        }
+        
+        void processJaniInput() {
+            auto parsingTime = startStopwatch("Parsing JANI input ... " );
+
+            auto const& input = storm::settings::getModule<storm::settings::modules::ConversionInputSettings>();
+
+            // Parse the jani model and selected properties
+            boost::optional<std::vector<std::string>> janiPropertyFilter;
+            if (input.isJaniPropertiesSet()) {
+                if (input.areJaniPropertiesSelected()) {
+                    janiPropertyFilter = input.getSelectedJaniProperties();
+                } else {
+                    janiPropertyFilter = boost::none;
+                }
+            } else {
+                if (input.isPropertyInputSet()) {
+                    janiPropertyFilter = std::vector<std::string>();
+                } else {
+                    // If no properties are selected, take the ones from the jani file.
+                    janiPropertyFilter = boost::none;
+                }
+            }
+            auto janiModelProperties = storm::api::parseJaniModel(input.getJaniInputFilename(), storm::jani::getAllKnownModelFeatures(), janiPropertyFilter);
+            
+            // Parse additional properties given from command line
+            std::vector<storm::jani::Property> properties = std::move(janiModelProperties.second);
+            if (input.isPropertyInputSet()) {
+                boost::optional<std::set<std::string>> propertyFilter = storm::api::parsePropertyFilter(input.getPropertyInputFilter());
+                auto additionalProperties = storm::api::parsePropertiesForSymbolicModelDescription(input.getPropertyInput(), janiModelProperties.first, propertyFilter);
+                properties.insert(properties.end(), additionalProperties.begin(), additionalProperties.end());
+            }
+            
+            storm::storage::SymbolicModelDescription symbDescr(janiModelProperties.first);
+            
+            // Substitute constant definitions in model and properties.
+            std::string constantDefinitionString = input.getConstantDefinitionString();
+            auto constantDefinitions = symbDescr.parseConstantDefinitions(constantDefinitionString);
+            auto janiModel = janiModelProperties.first.defineUndefinedConstants(constantDefinitions).substituteConstants();
+            if (!properties.empty()) {
+                properties = storm::api::substituteConstantsInProperties(properties, constantDefinitions);
+            }
+            stopStopwatch(parsingTime);
+
+            // Branch on the type of output
+            auto const& output = storm::settings::getModule<storm::settings::modules::ConversionOutputSettings>();
+            if (output.isJaniOutputSet()) {
+                processJaniInputJaniOutput(janiModel, properties);
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "There is either no outputformat specified or the provided combination of input and output format is not compatible.");
+            }
+        }
+        
+        void processOptions() {
+            // Start by setting some urgent options (log levels, etc.)
+            setUrgentOptions();
+            
+            // Branch on the type of input
+            auto const& input = storm::settings::getModule<storm::settings::modules::ConversionInputSettings>();
+            STORM_LOG_THROW(!(input.isPrismInputSet() && input.isJaniInputSet()), storm::exceptions::InvalidSettingsException, "Multiple input options were set.");
+            if (input.isPrismInputSet()) {
+                processPrismInput();
+            } else if (input.isJaniInputSet()) {
+                processJaniInput();
+            }
+        }
+    }
+}
+
+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;
+    }
+    
+    auto const& general = storm::settings::getModule<storm::settings::modules::ConversionGeneralSettings>();
+    
+    // Set options from config file (if given)
+    if (general.isConfigSet()) {
+        storm::settings::mutableManager().setFromConfigurationFile(general.getConfigFilename());
+    }
+
+    bool result = true;
+    if (general.isHelpSet()) {
+        storm::settings::manager().printHelp(general.getHelpModuleName());
+        result = false;
+    }
+    
+    if (general.isVersionSet()) {
+        storm::cli::printVersion("storm-conv");
+        result = false;;
+    }
+
+    return result;
+}
+
+/*!
+ * Main entry point of the executable storm-conv.
+ */
+int main(const int argc, const char** argv) {
+
+    try {
+        storm::utility::setUp();
+        
+        // Print header info only if output to sdtout is disabled
+        bool outputToStdOut = false;
+        for (int i = 1; i < argc; ++i) {
+            if (std::string(argv[i]) == "--" + storm::settings::modules::ConversionOutputSettings::stdoutOptionName) {
+                outputToStdOut = true;
+            }
+        }
+        if (outputToStdOut) {
+            storm::utility::setLogLevel(l3pp::LogLevel::OFF);
+        } else {
+            storm::cli::printHeader("Storm-conv", argc, argv);
+        }
+        
+        storm::settings::initializeConvSettings("Storm-conv", "storm-conv");
+        if (!parseOptions(argc, argv)) {
+            return -1;
+        }
+
+        storm::conv::processOptions();
+
+        storm::utility::cleanUp();
+        return 0;
+    } catch (storm::exceptions::BaseException const& exception) {
+        STORM_LOG_ERROR("An exception caused Storm-conv to terminate. The message of the exception is: " << exception.what());
+        return 1;
+    } catch (std::exception const& exception) {
+        STORM_LOG_ERROR("An unexpected exception occurred and caused Storm-conv to terminate. The message of this exception is: " << exception.what());
+        return 2;
+    }
+}

src/storm-conv/CMakeLists.txt

@@ -0,0 +1,40 @@
+file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-conv/*.h ${PROJECT_SOURCE_DIR}/src/storm-conv/*.cpp)
+
+register_source_groups_from_filestructure("${ALL_FILES}" storm-conv)
+
+
+
+file(GLOB_RECURSE STORM_CONV_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-conv/*/*.cpp)
+file(GLOB_RECURSE STORM_CONV_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-conv/*/*.h)
+
+
+# Create storm-conv.
+add_library(storm-conv SHARED ${STORM_CONV_SOURCES} ${STORM_CONV_HEADERS})
+
+# Remove define symbol for shared libstorm.
+set_target_properties(storm-conv PROPERTIES DEFINE_SYMBOL "")
+#add_dependencies(storm resources)
+list(APPEND STORM_TARGETS storm-conv)
+set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
+
+target_link_libraries(storm-conv PUBLIC storm ${STORM_CONV_LINK_LIBRARIES})
+
+# Install storm headers to include directory.
+foreach(HEADER ${STORM_CONV_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_CONV_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}")
+endforeach()
+add_custom_target(copy_storm_conv_headers DEPENDS ${STORM_CONV_OUTPUT_HEADERS} ${STORM_CONV_HEADERS})
+add_dependencies(storm-conv copy_storm_conv_headers)
+
+# installation
+install(TARGETS storm-conv EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
+

src/storm-conv/api/storm-conv.cpp

@@ -0,0 +1,78 @@
+#include "storm-conv/api/storm-conv.h"
+
+#include "storm/storage/prism/Program.h"
+#include "storm/storage/jani/Property.h"
+#include "storm/storage/jani/JaniLocationExpander.h"
+#include "storm/storage/jani/JSONExporter.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/CoreSettings.h"
+
+namespace storm {
+    namespace api {
+        
+        void transformJani(storm::jani::Model& janiModel, std::vector<storm::jani::Property>& properties, storm::converter::JaniConversionOptions const& options) {
+        
+            if (options.substituteConstants) {
+                janiModel = janiModel.substituteConstants();
+            }
+            
+            if (!options.locationVariables.empty()) {
+                for (auto const& pair : options.locationVariables) {
+                    storm::jani::JaniLocationExpander expander(janiModel);
+                    expander.transform(pair.first, pair.second);
+                    janiModel = expander.getResult();
+                }
+            }
+
+            if (options.flatten) {
+                std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
+                if (storm::settings::hasModule<storm::settings::modules::CoreSettings>()) {
+                    smtSolverFactory = std::make_shared<storm::utility::solver::SmtSolverFactory>();
+                } else {
+                    smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
+                }
+                janiModel = janiModel.flattenComposition(smtSolverFactory);
+            }
+
+            if (!options.edgeAssignments) {
+                janiModel.pushEdgeAssignmentsToDestinations();
+            }
+            
+            auto uneliminatedFeatures = janiModel.restrictToFeatures(options.allowedModelFeatures);
+            STORM_LOG_WARN_COND(uneliminatedFeatures.empty(), "The following model features could not be eliminated: " << uneliminatedFeatures.toString());
+            
+            if (options.modelName) {
+                janiModel.setName(options.modelName.get());
+            }
+        }
+        
+        std::pair<storm::jani::Model, std::vector<storm::jani::Property>> convertPrismToJani(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties, storm::converter::PrismToJaniConverterOptions options) {
+        
+            // Perform conversion
+            auto res = program.toJani(properties, options.allVariablesGlobal);
+            if (res.second.empty()) {
+                std::vector<storm::jani::Property> clondedProperties;
+                for (auto const& p : properties) {
+                    clondedProperties.push_back(p.clone());
+                }
+                res.second = std::move(clondedProperties);
+            }
+            
+            // Postprocess Jani model based on the options
+            transformJani(res.first, res.second, options.janiOptions);
+            
+            return res;
+        }
+        
+        void exportJaniToFile(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::string const& filename, bool compact) {
+            storm::jani::JsonExporter::toFile(model, properties, filename, true, compact);
+        }
+        
+        void printJaniToStream(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::ostream& ostream, bool compact) {
+            storm::jani::JsonExporter::toStream(model, properties, ostream, true, compact);
+        }
+
+        
+    }
+}

src/storm-conv/api/storm-conv.h

@@ -0,0 +1,28 @@
+#pragma once
+
+#include "storm-conv/converter/options/PrismToJaniConverterOptions.h"
+#include "storm-conv/converter/options/JaniConversionOptions.h"
+
+namespace storm {
+    
+    namespace prism {
+        class Program;
+    }
+    namespace jani {
+        class Model;
+        class Property;
+    }
+
+    namespace api {
+        
+        void transformJani(storm::jani::Model& janiModel, std::vector<storm::jani::Property>& properties, storm::converter::JaniConversionOptions const& options);
+
+        std::pair<storm::jani::Model, std::vector<storm::jani::Property>> convertPrismToJani(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties = std::vector<storm::jani::Property>(), storm::converter::PrismToJaniConverterOptions options = storm::converter::PrismToJaniConverterOptions());
+        
+        void exportJaniToFile(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::string const& filename, bool compact = false);
+        
+        void printJaniToStream(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::ostream& ostream, bool compact = false);
+
+        
+    }
+}

src/storm-conv/converter/options/JaniConversionOptions.cpp

@@ -0,0 +1,20 @@
+#include "storm-conv/converter/options/PrismToJaniConverterOptions.h"
+
+namespace storm {
+    namespace converter {
+
+        JaniConversionOptions::JaniConversionOptions() : edgeAssignments(false), flatten(false), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) {
+            // Intentionally left empty
+        };
+
+        JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), edgeAssignments(settings.isAllowEdgeAssignmentsSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) {
+            if (settings.isEliminateFunctionsSet()) {
+                allowedModelFeatures.remove(storm::jani::ModelFeature::Functions);
+            }
+            if (settings.isEliminateArraysSet()) {
+                allowedModelFeatures.remove(storm::jani::ModelFeature::Arrays);
+            }
+        };
+    }
+}
+

src/storm-conv/converter/options/JaniConversionOptions.h

@@ -0,0 +1,39 @@
+#pragma once
+
+#include <string>
+#include <vector>
+#include <boost/optional.hpp>
+
+#include "storm-conv/settings/modules/JaniExportSettings.h"
+#include "storm/storage/jani/ModelFeatures.h"
+
+namespace storm {
+    namespace converter {
+
+        struct JaniConversionOptions {
+            
+            JaniConversionOptions();
+            JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings);
+            
+            /// (Automaton,Variable)-pairs that will be transformed to location variables of the respective automaton.
+            std::vector<std::pair<std::string, std::string>> locationVariables;
+            
+            /// If set, the model might have transient assignments to the edges
+            bool edgeAssignments;
+            
+            /// If set, the model is transformed into a single automaton
+            bool flatten;
+            
+            /// If set, constants in expressions are substituted with their definition
+            bool substituteConstants;
+            
+            /// If given, the model will get this name
+            boost::optional<std::string> modelName;
+            
+            /// Only these model features are allowed in the output
+            storm::jani::ModelFeatures allowedModelFeatures;
+            
+        };
+    }
+}
+

src/storm-conv/converter/options/PrismToJaniConverterOptions.cpp

@@ -0,0 +1,12 @@
+#include "storm-conv/converter/options/PrismToJaniConverterOptions.h"
+
+
+namespace storm {
+    namespace converter {
+
+        PrismToJaniConverterOptions::PrismToJaniConverterOptions() : allVariablesGlobal(false), suffix("") {
+            // Intentionally left empty
+        };
+    }
+}
+

src/storm-conv/converter/options/PrismToJaniConverterOptions.h

@@ -0,0 +1,21 @@
+#pragma once
+
+#include <string>
+#include "storm-conv/converter/options/JaniConversionOptions.h"
+
+
+namespace storm {
+    namespace converter {
+        
+
+        struct PrismToJaniConverterOptions {
+            
+            PrismToJaniConverterOptions();
+            
+            bool allVariablesGlobal;
+            std::string suffix;
+            JaniConversionOptions janiOptions;
+        };
+    }
+}
+

src/storm-conv/settings/ConvSettings.cpp

@@ -0,0 +1,24 @@
+#include "storm-conv/settings/ConvSettings.h"
+
+#include "storm-conv/settings/modules/ConversionGeneralSettings.h"
+#include "storm-conv/settings/modules/ConversionInputSettings.h"
+#include "storm-conv/settings/modules/ConversionOutputSettings.h"
+#include "storm-conv/settings/modules/JaniExportSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+
+
+namespace storm {
+    namespace settings {
+        void initializeConvSettings(std::string const& name, std::string const& executableName) {
+            storm::settings::mutableManager().setName(name, executableName);
+        
+            // Register relevant settings modules.
+            storm::settings::addModule<storm::settings::modules::ConversionGeneralSettings>();
+            storm::settings::addModule<storm::settings::modules::ConversionInputSettings>();
+            storm::settings::addModule<storm::settings::modules::ConversionOutputSettings>();
+            storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
+        }
+    
+    }
+}

src/storm-conv/settings/ConvSettings.h

@@ -0,0 +1,11 @@
+#pragma once
+
+#include <string>
+
+namespace storm {
+    namespace settings {
+        
+        void initializeConvSettings(std::string const& name, std::string const& executableName);
+        
+    }
+}

src/storm-conv/settings/modules/ConversionGeneralSettings.cpp

@@ -0,0 +1,77 @@
+#include "storm-conv/settings/modules/ConversionGeneralSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/settings/Argument.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            const std::string ConversionGeneralSettings::moduleName = "general";
+            const std::string ConversionGeneralSettings::helpOptionName = "help";
+            const std::string ConversionGeneralSettings::helpOptionShortName = "h";
+            const std::string ConversionGeneralSettings::versionOptionName = "version";
+            const std::string ConversionGeneralSettings::verboseOptionName = "verbose";
+            const std::string ConversionGeneralSettings::verboseOptionShortName = "v";
+            const std::string ConversionGeneralSettings::debugOptionName = "debug";
+            const std::string ConversionGeneralSettings::traceOptionName = "trace";
+            const std::string ConversionGeneralSettings::configOptionName = "config";
+            const std::string ConversionGeneralSettings::configOptionShortName = "c";
+
+            ConversionGeneralSettings::ConversionGeneralSettings() : ModuleSettings(moduleName) {
+                this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName)
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("hint", "A regular expression to show help for all matching entities or 'all' for the complete help.").setDefaultValueString("all").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, versionOptionName, false, "Prints the version information.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, verboseOptionName, false, "Enables more verbose output.").setShortName(verboseOptionShortName).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, debugOptionName, false, "Enables verbose and debug output.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, traceOptionName, false, "Enables verbose and debug and trace output.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, configOptionName, false, "If given, this file will be read and parsed for additional configuration settings.").setShortName(configOptionShortName)
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the configuration.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
+            }
+            
+            bool ConversionGeneralSettings::isHelpSet() const {
+                return this->getOption(helpOptionName).getHasOptionBeenSet();
+            }
+            
+            bool ConversionGeneralSettings::isVersionSet() const {
+                return this->getOption(versionOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string ConversionGeneralSettings::getHelpModuleName() const {
+                return this->getOption(helpOptionName).getArgumentByName("hint").getValueAsString();
+            }
+            
+            bool ConversionGeneralSettings::isVerboseSet() const {
+                return this->getOption(verboseOptionName).getHasOptionBeenSet();
+            }
+            
+            bool ConversionGeneralSettings::isDebugOutputSet() const {
+                return this->getOption(debugOptionName).getHasOptionBeenSet();
+            }
+            
+            bool ConversionGeneralSettings::isTraceOutputSet() const {
+                return this->getOption(traceOptionName).getHasOptionBeenSet();
+            }
+            
+            bool ConversionGeneralSettings::isConfigSet() const {
+                return this->getOption(configOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string ConversionGeneralSettings::getConfigFilename() const {
+                return this->getOption(configOptionName).getArgumentByName("filename").getValueAsString();
+            }
+            
+            void ConversionGeneralSettings::finalize() {
+                // Intentionally left empty.
+            }
+
+            bool ConversionGeneralSettings::check() const {
+                return true;
+            }
+            
+        } // namespace modules
+    } // namespace settings
+} // namespace storm

src/storm-conv/settings/modules/ConversionGeneralSettings.h

@@ -0,0 +1,88 @@
+#pragma once
+#include "storm/settings/modules/ModuleSettings.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            class ConversionGeneralSettings : public ModuleSettings {
+            public:
+                
+                ConversionGeneralSettings();
+                
+                /*!
+                 * Retrieves whether the help option was set.
+                 *
+                 * @return True if the help option was set.
+                 */
+                bool isHelpSet() const;
+
+                /*!
+                 * Retrieves whether the version option was set.
+                 *
+                 * @return True if the version option was set.
+                 */
+                bool isVersionSet() const;
+
+                /*!
+                 * Retrieves the name of the module for which to show the help or "all" to indicate that the full help
+                 * needs to be shown.
+                 *
+                 * @return The name of the module for which to show the help or "all".
+                 */
+                std::string getHelpModuleName() const;
+
+                /*!
+                 * Retrieves whether the verbose option was set.
+                 *
+                 * @return True if the verbose option was set.
+                 */
+                bool isVerboseSet() const;
+
+                /*!
+                 * Retrieves whether the debug output option was set.
+                 *
+                 */
+                bool isDebugOutputSet() const;
+
+                /*!
+                 * Retrieves whether the trace output option was set.
+                 *
+                 */
+                bool isTraceOutputSet() const;
+
+                /*!
+                 * Retrieves whether the config option was set.
+                 *
+                 * @return True if the config option was set.
+                 */
+                bool isConfigSet() const;
+
+                /*!
+                 * Retrieves the name of the file that is to be scanned for settings.
+                 *
+                 * @return The name of the file that is to be scanned for settings.
+                 */
+                std::string getConfigFilename() const;
+                
+                bool check() const override;
+                void finalize() override;
+
+                // The name of the module.
+                static const std::string moduleName;
+
+            private:
+                // Define the string names of the options as constants.
+                static const std::string helpOptionName;
+                static const std::string helpOptionShortName;
+                static const std::string versionOptionName;
+                static const std::string verboseOptionName;
+                static const std::string verboseOptionShortName;
+                static const std::string debugOptionName;
+                static const std::string traceOptionName;
+                static const std::string configOptionName;
+                static const std::string configOptionShortName;
+            };
+        }
+    }
+}

src/storm-conv/settings/modules/ConversionInputSettings.cpp

@@ -0,0 +1,114 @@
+#include "storm-conv/settings/modules/ConversionInputSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/settings/Argument.h"
+#include "storm/parser/CSVParser.h"
+
+#include "storm/exceptions/InvalidSettingsException.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            const std::string ConversionInputSettings::moduleName = "input";
+            const std::string ConversionInputSettings::propertyOptionName = "prop";
+            const std::string ConversionInputSettings::propertyOptionShortName = "prop";
+            const std::string ConversionInputSettings::constantsOptionName = "constants";
+            const std::string ConversionInputSettings::constantsOptionShortName = "const";
+            const std::string ConversionInputSettings::prismInputOptionName = "prism";
+            const std::string ConversionInputSettings::prismCompatibilityOptionName = "prismcompat";
+            const std::string ConversionInputSettings::prismCompatibilityOptionShortName = "pc";
+            const std::string ConversionInputSettings::janiInputOptionName = "jani";
+            const std::string ConversionInputSettings::janiPropertyOptionName = "janiproperty";
+            const std::string ConversionInputSettings::janiPropertyOptionShortName = "jprop";
+
+
+            ConversionInputSettings::ConversionInputSettings() : ModuleSettings(moduleName) {
+                // General
+                this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies the properties to be checked on the model.").setShortName(propertyOptionShortName)
+                                        .addArgument(storm::settings::ArgumentBuilder::createStringArgument("property or filename", "The formula or the file containing the formulas.").build())
+                                        .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "The names of the properties to check.").setDefaultValueString("all").build())
+                                        .build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that this requires the model to be given as an symbolic model (e.g., via --" + prismInputOptionName + ").").setShortName(constantsOptionShortName)
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build());
+                
+                // Prism related
+                this->addOption(storm::settings::OptionBuilder(moduleName, prismInputOptionName, false, "Parses the model given in the PRISM format.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the PRISM input.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build());
+                
+                // Jani related
+                this->addOption(storm::settings::OptionBuilder(moduleName, janiInputOptionName, false, "Parses the model given in the JANI format.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the JANI input.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, janiPropertyOptionName, false, "Specifies the properties from the jani model (given by --" + janiInputOptionName + ")  to be checked.").setShortName(janiPropertyOptionShortName)
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of properties to be checked").setDefaultValueString("").build()).build());
+
+            }
+            
+            bool ConversionInputSettings::isPrismInputSet() const {
+                return this->getOption(prismInputOptionName).getHasOptionBeenSet();
+            }
+
+            std::string ConversionInputSettings::getPrismInputFilename() const {
+                return this->getOption(prismInputOptionName).getArgumentByName("filename").getValueAsString();
+            }
+            
+            bool ConversionInputSettings::isJaniInputSet() const {
+                return this->getOption(janiInputOptionName).getHasOptionBeenSet();
+            }
+
+            std::string ConversionInputSettings::getJaniInputFilename() const {
+                return this->getOption(janiInputOptionName).getArgumentByName("filename").getValueAsString();
+            }
+            
+            bool ConversionInputSettings::isPrismCompatibilityEnabled() const {
+                return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet();
+            }
+
+            bool ConversionInputSettings::isConstantsSet() const {
+                return this->getOption(constantsOptionName).getHasOptionBeenSet();
+            }
+
+            std::string ConversionInputSettings::getConstantDefinitionString() const {
+                return this->getOption(constantsOptionName).getArgumentByName("values").getValueAsString();
+            }
+
+            bool ConversionInputSettings::isPropertyInputSet() const {
+                return this->getOption(propertyOptionName).getHasOptionBeenSet();
+            }
+
+            std::string ConversionInputSettings::getPropertyInput() const {
+                return this->getOption(propertyOptionName).getArgumentByName("property or filename").getValueAsString();
+            }
+
+            std::string ConversionInputSettings::getPropertyInputFilter() const {
+                return this->getOption(propertyOptionName).getArgumentByName("filter").getValueAsString();
+            }
+
+            bool ConversionInputSettings::isJaniPropertiesSet() const {
+                return this->getOption(janiPropertyOptionName).getHasOptionBeenSet();
+            }
+
+            bool ConversionInputSettings::areJaniPropertiesSelected() const {
+                return this->getOption(janiPropertyOptionName).getHasOptionBeenSet() && (this->getOption(janiPropertyOptionName).getArgumentByName("values").getValueAsString() != "");
+            }
+
+            std::vector<std::string> ConversionInputSettings::getSelectedJaniProperties() const {
+                return storm::parser::parseCommaSeperatedValues(this->getOption(janiPropertyOptionName).getArgumentByName("values").getValueAsString());
+            }
+
+			void ConversionInputSettings::finalize() {
+                // Intentionally left empty.
+            }
+
+            bool ConversionInputSettings::check() const {
+                return true;
+            }
+            
+            
+        } // namespace modules
+    } // namespace settings
+} // namespace storm

src/storm-conv/settings/modules/ConversionInputSettings.h

@@ -0,0 +1,118 @@
+#pragma once
+#include "storm/settings/modules/ModuleSettings.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            class ConversionInputSettings : public ModuleSettings {
+            public:
+                
+                ConversionInputSettings();
+                
+                /*!
+                 * Retrieves whether the property option was set.
+                 *
+                 * @return True if the property option was set.
+                 */
+                bool isPropertyInputSet() const;
+
+                /*!
+                 * Retrieves the property specified with the property option.
+                 *
+                 * @return The property specified with the property option.
+                 */
+                std::string getPropertyInput() const;
+
+                /*!
+                 * Retrieves the property filter.
+                 *
+                 * @return The property filter.
+                 */
+                std::string getPropertyInputFilter() const;
+                
+                 /*!
+                 * Retrieves whether constant definition option was set.
+                 *
+                 * @return True if the constant definition option was set.
+                 */
+                bool isConstantsSet() const;
+
+                /*!
+                 * Retrieves the string that defines the constants of a symbolic model (given via the symbolic option).
+                 *
+                 * @return The string that defines the constants of a symbolic model.
+                 */
+                std::string getConstantDefinitionString() const;
+
+                /*!
+                 * Retrieves whether the PRISM language option was set.
+                 */
+                bool isPrismInputSet() const;
+                
+                /*!
+                 * Retrieves the name of the file that contains the PRISM model specification if the model was given
+                 * using the PRISM input option.
+                 */
+                std::string getPrismInputFilename() const;
+                
+                /*!
+                 * Retrieves whether the PRISM compatibility mode was enabled.
+                 *
+                 * @return True iff the PRISM compatibility mode was enabled.
+                 */
+                bool isPrismCompatibilityEnabled() const;
+                
+                /*!
+                 * Retrieves whether the Jani option was set.
+                 */
+                bool isJaniInputSet() const;
+                
+                /*!
+                 * Retrieves the name of the file that contains the jani model specification if the model was given.
+                 */
+                std::string getJaniInputFilename() const;
+                
+                /*!
+                 * Retrieves whether the jani-property option was set
+                 * @return
+                 */
+                bool isJaniPropertiesSet() const;
+
+                /*!
+                 * Retrieves whether one or more jani-properties have been selected
+                 * @return
+                 */
+                bool areJaniPropertiesSelected() const;
+                
+                /*!
+                 * @return  The names of the jani properties to check
+                 */
+                std::vector<std::string> getSelectedJaniProperties() const;
+
+
+                
+                bool check() const override;
+                void finalize() override;
+
+                // The name of the module.
+                static const std::string moduleName;
+
+            private:
+                // Define the string names of the options as constants.
+                static const std::string propertyOptionName;
+                static const std::string propertyOptionShortName;
+                static const std::string constantsOptionName;
+                static const std::string constantsOptionShortName;
+                static const std::string prismInputOptionName;
+                static const std::string prismCompatibilityOptionName;
+                static const std::string prismCompatibilityOptionShortName;
+                static const std::string janiInputOptionName;
+                static const std::string janiPropertyOptionName;
+                static const std::string janiPropertyOptionShortName;
+            };
+            
+                
+        }
+    }
+}

src/storm-conv/settings/modules/ConversionOutputSettings.cpp

@@ -0,0 +1,57 @@
+#include "storm-conv/settings/modules/ConversionOutputSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/settings/Argument.h"
+
+#include "storm/exceptions/InvalidSettingsException.h"
+#include "storm/exceptions/InvalidOperationException.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            const std::string ConversionOutputSettings::moduleName = "output";
+            const std::string ConversionOutputSettings::stdoutOptionName = "stdout";
+            const std::string ConversionOutputSettings::janiOutputOptionName = "tojani";
+
+            ConversionOutputSettings::ConversionOutputSettings() : ModuleSettings(moduleName) {
+                this->addOption(storm::settings::OptionBuilder(moduleName, stdoutOptionName, false, "If set, the output will be printed to stdout.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, janiOutputOptionName, false, "converts the input model to Jani.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the output file (if not empty).").setDefaultValueString("").build()).build());
+            }
+            
+            bool ConversionOutputSettings::isStdOutOutputEnabled() const {
+                return this->getOption(stdoutOptionName).getHasOptionBeenSet();
+            }
+            
+            bool ConversionOutputSettings::isJaniOutputSet() const {
+                return this->getOption(janiOutputOptionName).getHasOptionBeenSet();
+            }
+            
+            bool ConversionOutputSettings::isJaniOutputFilenameSet() const {
+                return isJaniOutputSet()
+                       && !this->getOption(janiOutputOptionName).getArgumentByName("filename").wasSetFromDefaultValue()
+                       && this->getOption(janiOutputOptionName).getArgumentByName("filename").getHasBeenSet()
+                       && this->getOption(janiOutputOptionName).getArgumentByName("filename").getValueAsString() != "";
+            }
+
+            std::string ConversionOutputSettings::getJaniOutputFilename() const {
+                STORM_LOG_THROW(isJaniOutputFilenameSet(), storm::exceptions::InvalidOperationException, "Tried to get the jani output name although none was specified.");
+                return this->getOption(janiOutputOptionName).getArgumentByName("filename").getValueAsString();
+            }
+
+			void ConversionOutputSettings::finalize() {
+                // Intentionally left empty.
+            }
+
+            bool ConversionOutputSettings::check() const {
+                STORM_LOG_THROW(!isJaniOutputFilenameSet() || ArgumentValidatorFactory::createWritableFileValidator()->isValid(getJaniOutputFilename()), storm::exceptions::InvalidSettingsException, "Unable to write at file " + getJaniOutputFilename());
+                return true;
+            }
+            
+        } // namespace modules
+    } // namespace settings
+} // namespace storm

src/storm-conv/settings/modules/ConversionOutputSettings.h

@@ -0,0 +1,49 @@
+#pragma once
+#include "storm/settings/modules/ModuleSettings.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            class ConversionOutputSettings : public ModuleSettings {
+            public:
+                
+                ConversionOutputSettings();
+                
+                /*!
+                 * Retrieves whether the output should be printed to stdout
+                 */
+                bool isStdOutOutputEnabled() const;
+                
+                /*!
+                 * Retrieves whether the output should be in the Jani format
+                 */
+                bool isJaniOutputSet() const;
+                
+                /*!
+                 * Retrieves whether an output filename for the jani file was specified
+                 */
+                bool isJaniOutputFilenameSet() const;
+
+                /*!
+                 * Retrieves the name of the jani output (if specified)
+                 */
+                std::string getJaniOutputFilename() const;
+                
+                bool check() const override;
+                void finalize() override;
+
+                // The name of the module.
+                static const std::string moduleName;
+                // name of the option that enables output to stdout. It needs to be public because we have to check this option very early
+                static const std::string stdoutOptionName;
+
+            private:
+                // Define the string names of the options as constants.
+                static const std::string janiOutputOptionName;
+            };
+            
+                
+        }
+    }
+}

src/storm-conv/settings/modules/JaniExportSettings.cpp

@@ -0,0 +1,88 @@
+#include "JaniExportSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/SettingMemento.h"
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/settings/Argument.h"
+
+#include <boost/algorithm/string.hpp>
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            const std::string JaniExportSettings::moduleName = "exportJani";
+            
+            const std::string JaniExportSettings::edgeAssignmentsOptionName = "edge-assignments";
+            const std::string JaniExportSettings::exportFlattenOptionName = "flatten";
+            const std::string JaniExportSettings::locationVariablesOptionName = "location-variables";
+            const std::string JaniExportSettings::globalVariablesOptionName = "globalvars";
+            const std::string JaniExportSettings::compactJsonOptionName = "compactjson";
+            const std::string JaniExportSettings::eliminateArraysOptionName = "remove-arrays";
+            const std::string JaniExportSettings::eliminateFunctionsOptionName = "remove-functions";
+            
+            JaniExportSettings::JaniExportSettings() : ModuleSettings(moduleName) {
+                this->addOption(storm::settings::OptionBuilder(moduleName, locationVariablesOptionName, true, "Variables to export in the location").addArgument(storm::settings::ArgumentBuilder::createStringArgument("variables", "A comma separated list of automaton and local variable names seperated by a dot, e.g. A.x,B.y.").setDefaultValueString("").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, edgeAssignmentsOptionName, false, "If set, the output model can have transient edge assignments. This can simplify the jani model but is not compliant to the jani standard.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportFlattenOptionName, false, "Flattens the composition of Automata to obtain an equivalent model that contains exactly one automaton").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, globalVariablesOptionName, false, "If set, variables will preferably be made global, e.g., to guarantee the same variable order as in the input file.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, compactJsonOptionName, false, "If set, the size of the resulting jani file will be reduced at the cost of (human-)readability.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, eliminateArraysOptionName, false, "If set, transforms the model such that array variables/expressions are eliminated.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, eliminateFunctionsOptionName, false, "If set, transforms the model such that functions are eliminated.").build());
+            }
+            
+            bool JaniExportSettings::isAllowEdgeAssignmentsSet() const {
+                return this->getOption(edgeAssignmentsOptionName).getHasOptionBeenSet();
+            }
+
+            bool JaniExportSettings::isExportFlattenedSet() const {
+                return this->getOption(exportFlattenOptionName).getHasOptionBeenSet();
+            }
+
+            bool JaniExportSettings::isLocationVariablesSet() const {
+                return this->getOption(locationVariablesOptionName).getHasOptionBeenSet();
+            }
+
+            std::vector<std::pair<std::string, std::string>> JaniExportSettings::getLocationVariables() const {
+                std::vector<std::pair<std::string, std::string>> result;
+                if (isLocationVariablesSet()) {
+                    std::string argument = this->getOption(locationVariablesOptionName).getArgumentByName("variables").getValueAsString();
+                    std::vector<std::string> arguments;
+                    boost::split( arguments, argument, boost::is_any_of(","));
+                    for (auto const& pair : arguments) {
+                        std::vector<std::string> keyvaluepair;
+                        boost::split( keyvaluepair, pair, boost::is_any_of("."));
+                        STORM_LOG_THROW(keyvaluepair.size() == 2, storm::exceptions::IllegalArgumentException, "Expected a name of the form AUTOMATON.VARIABLE (with no further dots) but got " << pair);
+                        result.emplace_back(keyvaluepair.at(0), keyvaluepair.at(1));
+                    }
+                }
+                return result;
+            }
+
+            bool JaniExportSettings::isGlobalVarsSet() const {
+                return this->getOption(globalVariablesOptionName).getHasOptionBeenSet();
+            }
+
+            bool JaniExportSettings::isCompactJsonSet() const {
+                return this->getOption(compactJsonOptionName).getHasOptionBeenSet();
+            }
+            
+            bool JaniExportSettings::isEliminateArraysSet() const {
+                return this->getOption(eliminateArraysOptionName).getHasOptionBeenSet();
+            }
+            
+            bool JaniExportSettings::isEliminateFunctionsSet() const {
+                return this->getOption(eliminateFunctionsOptionName).getHasOptionBeenSet();
+            }
+            
+            void JaniExportSettings::finalize() {
+                
+            }
+            
+            bool JaniExportSettings::check() const {
+                return true;
+            }
+        }
+    }
+}

src/storm-conv/settings/modules/JaniExportSettings.h

@@ -0,0 +1,50 @@
+#pragma once
+
+#include "storm-config.h"
+#include "storm/settings/modules/ModuleSettings.h"
+
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            class JaniExportSettings : public ModuleSettings {
+            public:
+                /*!
+                 * Creates a new JaniExport setting
+                 */
+                JaniExportSettings();
+                
+                bool isAllowEdgeAssignmentsSet() const;
+
+                bool isExportFlattenedSet() const;
+
+                bool isLocationVariablesSet() const;
+                
+                bool isGlobalVarsSet() const;
+                
+                bool isCompactJsonSet() const;
+                
+                bool isEliminateArraysSet() const;
+                
+                bool isEliminateFunctionsSet() const;
+
+                std::vector<std::pair<std::string, std::string>> getLocationVariables() const;
+
+                bool check() const override;
+                void finalize() override;
+                
+                static const std::string moduleName;
+                
+            private:
+                static const std::string edgeAssignmentsOptionName;
+                static const std::string exportFlattenOptionName;
+                static const std::string locationVariablesOptionName;
+                static const std::string globalVariablesOptionName;
+                static const std::string compactJsonOptionName;
+                static const std::string eliminateArraysOptionName;
+                static const std::string eliminateFunctionsOptionName;
+                
+            };
+        }
+    }
+}

src/storm-counterexamples/CMakeLists.txt

@@ -0,0 +1,40 @@
+file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*.h ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*.cpp)
+
+register_source_groups_from_filestructure("${ALL_FILES}" storm-counterexamples)
+
+
+
+file(GLOB_RECURSE STORM_CEX_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*/*.cpp)
+file(GLOB_RECURSE STORM_CEX_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*/*.h)
+
+
+# Create storm-dft.
+add_library(storm-counterexamples SHARED ${STORM_CEX_SOURCES} ${STORM_CEX_HEADERS})
+
+# Remove define symbol for shared libstorm.
+set_target_properties(storm-counterexamples PROPERTIES DEFINE_SYMBOL "")
+#add_dependencies(storm resources)
+list(APPEND STORM_TARGETS storm-counterexamples)
+set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
+
+target_link_libraries(storm-counterexamples PUBLIC storm)
+
+# Install storm headers to include directory.
+foreach(HEADER ${STORM_CEX_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_CEX_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}")
+endforeach()
+add_custom_target(copy_storm_cex_headers DEPENDS ${STORM_CEX_OUTPUT_HEADERS} ${STORM_CEX_HEADERS})
+add_dependencies(storm-counterexamples copy_storm_cex_headers)
+
+# installation
+install(TARGETS storm-counterexamples EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
+

src/storm/api/counterexamples.cpp → src/storm-counterexamples/api/counterexamples.cpp

@@ -1,4 +1,4 @@
-#include "storm/api/counterexamples.h"
+#include "storm-counterexamples/api/counterexamples.h"
 
 #include "storm/environment/Environment.h"
 

src/storm/api/counterexamples.h → src/storm-counterexamples/api/counterexamples.h

@@ -1,7 +1,7 @@
 #pragma once
 
-#include "storm/counterexamples/MILPMinimalLabelSetGenerator.h"
-#include "storm/counterexamples/SMTMinimalLabelSetGenerator.h"
+#include "storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h"
+#include "storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h"
 
 namespace storm {
     namespace api {

src/storm/counterexamples/Counterexample.cpp → src/storm-counterexamples/counterexamples/Counterexample.cpp

@@ -1,4 +1,4 @@
-#include "storm/counterexamples/Counterexample.h"
+#include "storm-counterexamples/counterexamples/Counterexample.h"
 
 namespace storm {
     namespace counterexamples {

src/storm/counterexamples/HighLevelCounterexample.cpp → src/storm-counterexamples/counterexamples/HighLevelCounterexample.cpp

@@ -1,4 +1,4 @@
-#include "storm/counterexamples/HighLevelCounterexample.h"
+#include "storm-counterexamples/counterexamples/HighLevelCounterexample.h"
 
 namespace storm {
     namespace counterexamples {

src/storm/counterexamples/HighLevelCounterexample.h → src/storm-counterexamples/counterexamples/HighLevelCounterexample.h

@@ -1,6 +1,6 @@
 #pragma once
 
-#include "storm/counterexamples/Counterexample.h"
+#include "Counterexample.h"
 
 #include "storm/storage/SymbolicModelDescription.h"
 

src/storm/counterexamples/MILPMinimalLabelSetGenerator.h → src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h

@@ -17,7 +17,7 @@
 
 #include "storm/solver/MinMaxLinearEquationSolver.h"
 
-#include "storm/counterexamples/HighLevelCounterexample.h"
+#include "storm-counterexamples/counterexamples/HighLevelCounterexample.h"
 
 #include "storm/utility/graph.h"
 #include "storm/utility/counterexamples.h"
@@ -29,7 +29,7 @@
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/GeneralSettings.h"
-#include "storm/settings/modules/CounterexampleGeneratorSettings.h"
+#include "storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h"
 
 namespace storm {
     
@@ -341,7 +341,7 @@ namespace storm {
                     std::list<uint_fast64_t> const& relevantChoicesForState = choiceInformation.relevantChoicesForRelevantStates.at(state);
                     for (uint_fast64_t row : relevantChoicesForState) {
                         for (auto const& successorEntry : mdp.getTransitionMatrix().getRow(row)) {
-                            if (stateInformation.relevantStates.get(successorEntry.getColumn())) {
+                            if (stateInformation.relevantStates.get(successorEntry.getColumn()) && resultingMap.find(std::make_pair(state, successorEntry.getColumn())) == resultingMap.end()) {
                                 variableNameBuffer.str("");
                                 variableNameBuffer.clear();
                                 variableNameBuffer << "t" << state << "to" << successorEntry.getColumn();
@@ -935,7 +935,7 @@ namespace storm {
                 double maximalReachabilityProbability = 0;
                 if (checkThresholdFeasible) {
                     storm::modelchecker::helper::SparseMdpPrctlHelper<T> modelcheckerHelper;
-                    std::vector<T> result = std::move(modelcheckerHelper.computeUntilProbabilities(env, false, mdp.getTransitionMatrix(), mdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::solver::GeneralMinMaxLinearEquationSolverFactory<T>()).values);
+                    std::vector<T> result = std::move(modelcheckerHelper.computeUntilProbabilities(env, false, mdp.getTransitionMatrix(), mdp.getBackwardTransitions(), phiStates, psiStates, false, false).values);
                     for (auto state : mdp.getInitialStates()) {
                         maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]);
                     }

src/storm/settings/modules/CounterexampleGeneratorSettings.cpp → src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp

@@ -1,4 +1,4 @@
-#include "storm/settings/modules/CounterexampleGeneratorSettings.h"
+#include "storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h"
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/exceptions/InvalidSettingsException.h"
@@ -16,13 +16,15 @@ namespace storm {
             const std::string CounterexampleGeneratorSettings::minimalCommandSetOptionName = "mincmd";
             const std::string CounterexampleGeneratorSettings::encodeReachabilityOptionName = "encreach";
             const std::string CounterexampleGeneratorSettings::schedulerCutsOptionName = "schedcuts";
+            const std::string CounterexampleGeneratorSettings::noDynamicConstraintsOptionName = "nodyn";
 
             CounterexampleGeneratorSettings::CounterexampleGeneratorSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> techniques = {"maxsat", "milp"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, minimalCommandSetOptionName, true, "Computes a counterexample for the given model in terms of a minimal command set. Note that this requires the model to be given in a symbolic format.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, minimalCommandSetOptionName, true, "Computes a counterexample for the given model in terms of a minimal command/edge set. Note that this requires the model to be given in a symbolic format.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used to derive the counterexample.").setDefaultValueString("maxsat").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(techniques)).build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, encodeReachabilityOptionName, true, "Sets whether to encode reachability for MAXSAT-based minimal command counterexample generation.").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based minimal command counterexample generation.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, encodeReachabilityOptionName, true, "Sets whether to encode reachability for MAXSAT-based counterexample generation.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based counterexample generation.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, noDynamicConstraintsOptionName, true, "Disables the generation of dynamic constraints in the MAXSAT-based counterexample generation.").build());
             }
             
             bool CounterexampleGeneratorSettings::isMinimalCommandSetGenerationSet() const {
@@ -45,9 +47,13 @@ namespace storm {
                 return this->getOption(schedulerCutsOptionName).getHasOptionBeenSet();
             }
 
+            bool CounterexampleGeneratorSettings::isUseDynamicConstraintsSet() const {
+                return !this->getOption(noDynamicConstraintsOptionName).getHasOptionBeenSet();
+            }
+
             bool CounterexampleGeneratorSettings::check() const {
                 // Ensure that the model was given either symbolically or explicitly.
-                STORM_LOG_THROW(!isMinimalCommandSetGenerationSet() || storm::settings::getModule<storm::settings::modules::IOSettings>().isPrismInputSet(), storm::exceptions::InvalidSettingsException, "For the generation of a minimal command set, the model has to be specified in the PRISM format.");
+                STORM_LOG_THROW(!isMinimalCommandSetGenerationSet() || storm::settings::getModule<storm::settings::modules::IOSettings>().isPrismInputSet() || storm::settings::getModule<storm::settings::modules::IOSettings>().isJaniInputSet(), storm::exceptions::InvalidSettingsException, "For the generation of a minimal command set, the model has to be specified in the PRISM/JANI format.");
                 
                 if (isMinimalCommandSetGenerationSet()) {
                     STORM_LOG_WARN_COND(isUseMaxSatBasedMinimalCommandSetGenerationSet() || !isEncodeReachabilitySet(), "Encoding reachability is only available for the MaxSat-based minimal command set generation, so selecting it has no effect.");

src/storm/settings/modules/CounterexampleGeneratorSettings.h → src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h

@@ -56,6 +56,13 @@ namespace storm {
                  */
                 bool isUseSchedulerCutsSet() const;
                 
+                /*!
+                 * Retrieves whether to use the dynamic constraints in the MAXSAT-based technique.
+                 *
+                 * @return True iff dynamic constraints are to be used.
+                 */
+                bool isUseDynamicConstraintsSet() const;
+                
                 bool check() const override;
                 
                 // The name of the module.
@@ -66,6 +73,7 @@ namespace storm {
                 static const std::string minimalCommandSetOptionName;
                 static const std::string encodeReachabilityOptionName;
                 static const std::string schedulerCutsOptionName;
+                static const std::string noDynamicConstraintsOptionName;
             };
             
         } // namespace modules

src/storm-dft-cli/CMakeLists.txt

@@ -6,4 +6,4 @@ set_target_properties(storm-dft-cli PROPERTIES OUTPUT_NAME "storm-dft")
 add_dependencies(binaries storm-dft-cli)
 
 # installation
-install(TARGETS storm-dft-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
+install(TARGETS storm-dft-cli EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)

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

@@ -1,164 +1,68 @@
-#include "storm-dft/settings/DftSettings.h"
+#include "storm-dft/api/storm-dft.h"
 
+#include "storm-dft/settings/DftSettings.h"
 #include "storm-dft/settings/modules/DftIOSettings.h"
 #include "storm-dft/settings/modules/FaultTreeSettings.h"
 #include "storm/settings/modules/IOSettings.h"
 #include "storm/settings/modules/ResourceSettings.h"
+#include "storm/settings/modules/GeneralSettings.h"
 
+
+#include "storm-parsers/api/storm-parsers.h"
 #include "storm/utility/initialize.h"
-#include "storm/api/storm.h"
 #include "storm-cli-utilities/cli.h"
 
-#include "storm-dft/parser/DFTGalileoParser.h"
-#include "storm-dft/parser/DFTJsonParser.h"
-#include "storm-dft/modelchecker/dft/DFTModelChecker.h"
-#include "storm-dft/modelchecker/dft/DFTASFChecker.h"
-#include "storm-dft/transformations/DftToGspnTransformator.h"
-#include "storm-dft/storage/dft/DftJsonExporter.h"
-
-#include "storm-gspn/storage/gspn/GSPN.h"
-#include "storm-gspn/storm-gspn.h"
-
-#include <boost/lexical_cast.hpp>
-#include <memory>
-
-template<typename ValueType>
-std::shared_ptr<storm::storage::DFT<ValueType>> loadDFT() {
-    storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule<storm::settings::modules::DftIOSettings>();
-    std::shared_ptr<storm::storage::DFT<ValueType>> dft;
-    // Build DFT from given file.
-    if (dftIOSettings.isDftJsonFileSet()) {
-        storm::parser::DFTJsonParser<ValueType> parser;
-        STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftJsonFilename());
-        dft = std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJson(dftIOSettings.getDftJsonFilename()));
-    } else {
-        storm::parser::DFTGalileoParser<ValueType> parser;
-        STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftFilename());
-        dft = std::make_shared<storm::storage::DFT<ValueType>>(parser.parseDFT(dftIOSettings.getDftFilename()));
-    }
-
-    if (dftIOSettings.isDisplayStatsSet()) {
-        std::cout << "=============DFT Statistics==============" << std::endl;
-        dft->writeStatsToStream(std::cout);
-        std::cout << "=========================================" << std::endl;
-    }
-    return dft;
-}
-
 /*!
- * Analyse the given DFT according to the given properties.
- * We first load the DFT from the given file, then build the corresponding model and last check against the given properties.
- *
- * @param properties PCTL formulas capturing the properties to check.
- * @param symred Flag whether symmetry reduction should be used.
- * @param allowModularisation Flag whether modularisation should be applied if possible.
- * @param enableDC Flag whether Don't Care propagation should be used.
- * @param approximationError Allowed approximation error.
- */
-template <typename ValueType>
-void analyzeDFT(std::vector<std::string> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) {
-    std::shared_ptr<storm::storage::DFT<ValueType>> dft = loadDFT<ValueType>();
-
-    // Build properties
-    std::string propString = properties[0];
-    for (size_t i = 1; i < properties.size(); ++i) {
-        propString += ";" + properties[i];
-    }
-    std::vector<std::shared_ptr<storm::logic::Formula const>> props = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propString));
-    STORM_LOG_ASSERT(props.size() > 0, "No properties found.");
-
-    // Check model
-    storm::modelchecker::DFTModelChecker<ValueType> modelChecker;
-    modelChecker.check(*dft, props, symred, allowModularisation, enableDC, approximationError);
-    modelChecker.printTimings();
-    modelChecker.printResults();
-}
-
-/*!
- * Analyze the DFT with use of SMT solving.
- *
- * @param filename Path to DFT file in Galileo format.
+ * Process commandline options and start computations.
  */
 template<typename ValueType>
-void analyzeWithSMT(std::shared_ptr<storm::storage::DFT<ValueType>> dft) {
-    STORM_LOG_DEBUG("Running DFT analysis with use of SMT");
-    storm::modelchecker::DFTASFChecker asfChecker(*dft);
-    asfChecker.convert();
-    asfChecker.toFile("test.smt2");
-    //bool sat = dftSmtBuilder.check();
-    //std::cout << "SMT result: " << sat << std::endl;
-}
-
 void processOptions() {
         // Start by setting some urgent options (log levels, resources, etc.)
         storm::cli::setUrgentOptions();
 
         storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule<storm::settings::modules::DftIOSettings>();
         storm::settings::modules::FaultTreeSettings const& faultTreeSettings = storm::settings::getModule<storm::settings::modules::FaultTreeSettings>();
-        storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
         storm::settings::modules::IOSettings const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+
         if (!dftIOSettings.isDftFileSet() && !dftIOSettings.isDftJsonFileSet()) {
             STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
         }
 
+        // Build DFT from given file
+        std::shared_ptr<storm::storage::DFT<ValueType>> dft;
+        if (dftIOSettings.isDftJsonFileSet()) {
+            STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftJsonFilename());
+            dft = storm::api::loadDFTJsonFile<ValueType>(dftIOSettings.getDftJsonFilename());
+        } else {
+            STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftFilename());
+            dft = storm::api::loadDFTGalileoFile<ValueType>(dftIOSettings.getDftFilename());
+        }
+
+        if (dftIOSettings.isDisplayStatsSet()) {
+            std::cout << "=============DFT Statistics==============" << std::endl;
+            dft->writeStatsToStream(std::cout);
+            std::cout << "=========================================" << std::endl;
+        }
+
         if (dftIOSettings.isExportToJson()) {
-            STORM_LOG_THROW(dftIOSettings.isDftFileSet(), storm::exceptions::InvalidSettingsException, "No input model in Galileo format given.");
-            std::shared_ptr<storm::storage::DFT<double>> dft = loadDFT<double>();
             // Export to json
-            storm::storage::DftJsonExporter<double>::toFile(*dft, dftIOSettings.getExportJsonFilename());
+            storm::api::exportDFTToJsonFile<ValueType>(*dft, dftIOSettings.getExportJsonFilename());
             return;
         }
 
-        
         if (dftIOSettings.isTransformToGspn()) {
-            std::shared_ptr<storm::storage::DFT<double>> dft = loadDFT<double>();
             // Transform to GSPN
-            storm::transformations::dft::DftToGspnTransformator<double> gspnTransformator(*dft);
-            bool smart = true;
-            gspnTransformator.transform(smart);
-            storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN();
-            uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId();
-            
-            storm::handleGSPNExportSettings(*gspn);
-
-            std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager = gspn->getExpressionManager();
-            storm::builder::JaniGSPNBuilder builder(*gspn);
-            storm::jani::Model* model =  builder.build();
-            storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace);
-
-            storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression();
-            auto evtlFormula = std::make_shared<storm::logic::AtomicExpressionFormula>(targetExpression);
-            auto tbFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), evtlFormula, storm::logic::TimeBound(false, exprManager->integer(0)), storm::logic::TimeBound(false, exprManager->integer(10)), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time));
-            auto tbUntil = std::make_shared<storm::logic::ProbabilityOperatorFormula>(tbFormula);
-            
-            auto evFormula = std::make_shared<storm::logic::EventuallyFormula>(evtlFormula, storm::logic::FormulaContext::Time);
-            auto rewFormula = std::make_shared<storm::logic::TimeOperatorFormula>(evFormula, storm::logic::OperatorInformation(), storm::logic::RewardMeasureType::Expectation);
-            
-            storm::settings::modules::JaniExportSettings const& janiSettings = storm::settings::getModule<storm::settings::modules::JaniExportSettings>();
-            if (janiSettings.isJaniFileSet()) {
-                storm::api::exportJaniModel(*model, {storm::jani::Property("time-bounded", tbUntil), storm::jani::Property("mttf", rewFormula)}, janiSettings.getJaniFilename());
-            }
-            
-            delete model;
-            delete gspn;
+            storm::api::transformToGSPN(*dft);
             return;
         }
         
-        bool parametric = false;
-#ifdef STORM_HAVE_CARL
-        parametric = generalSettings.isParametricSet();
-#endif
 
 #ifdef STORM_HAVE_Z3
         if (faultTreeSettings.solveWithSMT()) {
             // Solve with SMT
-            if (parametric) {
-            //    std::shared_ptr<storm::storage::DFT<double>> dft = loadDFT<double>();
-            //    analyzeWithSMT<storm::RationalFunction>(dftSettings.getDftFilename());
-            } else {
-                std::shared_ptr<storm::storage::DFT<double>> dft = loadDFT<double>();
-                analyzeWithSMT<double>(dft);
-            }
+            STORM_LOG_DEBUG("Running DFT analysis with use of SMT");
+            storm::api::exportDFTToSMT(*dft, "test.smt2");
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only exported to SMT file 'test.smt2' but analysis is not supported.");
             return;
         }
 #endif
@@ -170,9 +74,8 @@ void processOptions() {
             optimizationDirection = "max";
         }
         
-        // Construct properties to check for
+        // Construct properties to analyse
         std::vector<std::string> properties;
-        
         if (ioSettings.isPropertySet()) {
             properties.push_back(ioSettings.getProperty());
         }
@@ -195,38 +98,31 @@ void processOptions() {
             }
         }
 
-        if (properties.empty()) {
-            STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No property given.");
+        // Build properties
+        STORM_LOG_THROW(!properties.empty(), storm::exceptions::InvalidSettingsException, "No property given.");
+        std::string propString = properties[0];
+        for (size_t i = 1; i < properties.size(); ++i) {
+            propString += ";" + properties[i];
         }
+        std::vector<std::shared_ptr<storm::logic::Formula const>> props = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propString));
+        STORM_LOG_ASSERT(props.size() > 0, "No properties found.");
 
-        // Set possible approximation error
-        double approximationError = 0.0;
+        // Carry out the actual analysis
         if (faultTreeSettings.isApproximationErrorSet()) {
-            approximationError = faultTreeSettings.getApproximationError();
-        }
-
-        // From this point on we are ready to carry out the actual computations.
-        if (parametric) {
-#ifdef STORM_HAVE_CARL
-            analyzeDFT<storm::RationalFunction>(properties, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), approximationError);
-#else
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build.");
-#endif
+            // Approximate analysis
+            storm::api::analyzeDFTApprox<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), faultTreeSettings.getApproximationError(), true);
         } else {
-            analyzeDFT<double>(properties, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), approximationError);
+            storm::api::analyzeDFT<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), true);
         }
 }
 
 /*!
- * Entry point for the DyFTeE backend.
+ * Entry point for Storm-DFT.
  *
  * @param argc The argc argument of main().
  * @param argv The argv argument of main().
  * @return Return code, 0 if successfull, not 0 otherwise.
  */
-/*!
- * Main entry point of the executable storm-pars.
- */
 int main(const int argc, const char** argv) {
     try {
         storm::utility::setUp();
@@ -238,7 +134,12 @@ int main(const int argc, const char** argv) {
             return -1;
         }
 
-        processOptions();
+        storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
+        if (generalSettings.isParametricSet()) {
+            processOptions<storm::RationalFunction>();
+        } else {
+            processOptions<double>();
+        }
 
         totalTimer.stop();
         if (storm::settings::getModule<storm::settings::modules::ResourceSettings>().isPrintTimeAndMemorySet()) {
@@ -249,10 +150,10 @@ int main(const int argc, const char** argv) {
         storm::utility::cleanUp();
         return 0;
     } catch (storm::exceptions::BaseException const& exception) {
-        STORM_LOG_ERROR("An exception caused Storm-DyFTeE to terminate. The message of the exception is: " << exception.what());
+        STORM_LOG_ERROR("An exception caused Storm-DFT to terminate. The message of the exception is: " << exception.what());
         return 1;
     } catch (std::exception const& exception) {
-        STORM_LOG_ERROR("An unexpected exception occurred and caused Storm-DyFTeE to terminate. The message of this exception is: " << exception.what());
+        STORM_LOG_ERROR("An unexpected exception occurred and caused Storm-DFT to terminate. The message of this exception is: " << exception.what());
         return 2;
     }
 }

src/storm-dft/CMakeLists.txt

@@ -17,7 +17,7 @@ set_target_properties(storm-dft PROPERTIES DEFINE_SYMBOL "")
 list(APPEND STORM_TARGETS storm-dft)
 set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
 
-target_link_libraries(storm-dft PUBLIC storm storm-gspn ${STORM_DFT_LINK_LIBRARIES})
+target_link_libraries(storm-dft PUBLIC storm storm-gspn storm-parsers ${STORM_DFT_LINK_LIBRARIES})
 
 # Install storm headers to include directory.
 foreach(HEADER ${STORM_DFT_HEADERS})
@@ -36,5 +36,5 @@ add_custom_target(copy_storm_dft_headers DEPENDS ${STORM_DFT_OUTPUT_HEADERS} ${S
 add_dependencies(storm-dft copy_storm_dft_headers)
 
 # installation
-install(TARGETS storm-dft RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
+install(TARGETS storm-dft EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
 

src/storm-dft/api/storm-dft.cpp

@@ -0,0 +1,74 @@
+#include "storm-dft/api/storm-dft.h"
+
+namespace storm {
+    namespace api {
+
+        template<>
+        void exportDFTToJsonFile(storm::storage::DFT<double> const& dft, std::string const& file) {
+            storm::storage::DftJsonExporter<double>::toFile(dft, file);
+        }
+
+        template<>
+        void exportDFTToJsonFile(storm::storage::DFT<storm::RationalFunction> const& dft, std::string const& file) {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export to JSON not supported for this data type.");
+        }
+
+        template<>
+        std::string exportDFTToJsonString(storm::storage::DFT<double> const& dft) {
+            std::stringstream stream;
+            storm::storage::DftJsonExporter<double>::toStream(dft, stream);
+            return stream.str();
+        }
+
+        template<>
+        std::string exportDFTToJsonString(storm::storage::DFT<storm::RationalFunction> const& dft) {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export to JSON not supported for this data type.");
+        }
+
+        template<>
+        void exportDFTToSMT(storm::storage::DFT<double> const& dft, std::string const& file) {
+            storm::modelchecker::DFTASFChecker asfChecker(dft);
+            asfChecker.convert();
+            asfChecker.toFile(file);
+        }
+
+        template<>
+        void exportDFTToSMT(storm::storage::DFT<storm::RationalFunction> const& dft, std::string const& file) {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export to SMT does not support this data type.");
+        }
+
+        template<>
+        void transformToGSPN(storm::storage::DFT<double> const& dft) {
+            // Transform to GSPN
+            storm::transformations::dft::DftToGspnTransformator<double> gspnTransformator(dft);
+            bool smart = true;
+            gspnTransformator.transform(smart);
+            storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN();
+            uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId();
+
+            storm::api::handleGSPNExportSettings(*gspn, [&](storm::builder::JaniGSPNBuilder const& builder) {
+                    std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager = gspn->getExpressionManager();
+                    storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace);
+
+                    storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression();
+                    auto evtlFormula = std::make_shared<storm::logic::AtomicExpressionFormula>(targetExpression);
+                    auto tbFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), evtlFormula, storm::logic::TimeBound(false, exprManager->integer(0)), storm::logic::TimeBound(false, exprManager->integer(10)), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time));
+                    auto tbUntil = std::make_shared<storm::logic::ProbabilityOperatorFormula>(tbFormula);
+
+                    auto evFormula = std::make_shared<storm::logic::EventuallyFormula>(evtlFormula, storm::logic::FormulaContext::Time);
+                    auto rewFormula = std::make_shared<storm::logic::TimeOperatorFormula>(evFormula, storm::logic::OperatorInformation(), storm::logic::RewardMeasureType::Expectation);
+                    std::vector<storm::jani::Property> res({storm::jani::Property("time-bounded", tbUntil, {}), storm::jani::Property("mttf", rewFormula, {})});
+                    return res;
+                }
+            );
+
+            delete gspn;
+        }
+
+        template<>
+        void transformToGSPN(storm::storage::DFT<storm::RationalFunction> const& dft) {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation to GSPN not supported for this data type.");
+        }
+
+    }
+}

src/storm-dft/api/storm-dft.h

@@ -0,0 +1,138 @@
+#pragma once
+
+#include <type_traits>
+
+#include "storm-dft/parser/DFTGalileoParser.h"
+#include "storm-dft/parser/DFTJsonParser.h"
+#include "storm-dft/storage/dft/DftJsonExporter.h"
+
+#include "storm-dft/modelchecker/dft/DFTModelChecker.h"
+#include "storm-dft/modelchecker/dft/DFTASFChecker.h"
+
+#include "storm-dft/transformations/DftToGspnTransformator.h"
+#include "storm-gspn/api/storm-gspn.h"
+
+namespace storm {
+    namespace api {
+
+        /*!
+         * Load DFT from Galileo file.
+         *
+         * @param file File containing DFT description in Galileo format.
+         *
+         * @return DFT.
+         */
+        template<typename ValueType>
+        std::shared_ptr<storm::storage::DFT<ValueType>> loadDFTGalileoFile(std::string const& file) {
+             return std::make_shared<storm::storage::DFT<ValueType>>(storm::parser::DFTGalileoParser<ValueType>::parseDFT(file));
+        }
+
+        /*!
+         * Load DFT from JSON string.
+         *
+         * @param jsonString String containing DFT description in JSON format.
+         *
+         * @return DFT.
+         */
+        template<typename ValueType>
+        std::shared_ptr<storm::storage::DFT<ValueType>> loadDFTJsonString(std::string const& jsonString) {
+                storm::parser::DFTJsonParser<ValueType> parser;
+                return std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJsonFromString(jsonString));
+        }
+
+        /*!
+         * Load DFT from JSON file.
+         *
+         * @param file File containing DFT description in JSON format.
+         *
+         * @return DFT.
+         */
+        template<typename ValueType>
+        std::shared_ptr<storm::storage::DFT<ValueType>> loadDFTJsonFile(std::string const& file) {
+                storm::parser::DFTJsonParser<ValueType> parser;
+                return std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJsonFromFile(file));
+        }
+
+        /*!
+         * Analyse the given DFT according to the given properties.
+         * First the Markov model is built from the DFT and then this model is checked against the given properties.
+         *
+         * @param dft DFT.
+         * @param properties PCTL formulas capturing the properties to check.
+         * @param symred Flag whether symmetry reduction should be used.
+         * @param allowModularisation Flag whether modularisation should be applied if possible.
+         * @param enableDC Flag whether Don't Care propagation should be used.
+         *
+         * @return Result.
+         */
+        template <typename ValueType>
+        typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, bool enableDC, bool printOutput) {
+            storm::modelchecker::DFTModelChecker<ValueType> modelChecker;
+            typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, 0.0);
+            if (printOutput) {
+                modelChecker.printTimings();
+                modelChecker.printResults();
+            }
+            return results;
+        }
+
+        /*!
+         * Approximate the analysis result of the given DFT according to the given properties.
+         * First the Markov model is built from the DFT and then this model is checked against the given properties.
+         *
+         * @param dft DFT.
+         * @param properties PCTL formulas capturing the properties to check.
+         * @param symred Flag whether symmetry reduction should be used.
+         * @param allowModularisation Flag whether modularisation should be applied if possible.
+         * @param enableDC Flag whether Don't Care propagation should be used.
+         * @param approximationError Allowed approximation error.
+         *
+         * @return Result.
+         */
+        template <typename ValueType>
+        typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results analyzeDFTApprox(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError, bool printOutput) {
+            storm::modelchecker::DFTModelChecker<ValueType> modelChecker;
+            typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, approximationError);
+            if (printOutput) {
+                modelChecker.printTimings();
+                modelChecker.printResults();
+            }
+            return results;
+        }
+
+        /*!
+         * Export DFT to JSON file.
+         *
+         * @param dft DFT.
+         * @param file File.
+         */
+        template<typename ValueType>
+        void exportDFTToJsonFile(storm::storage::DFT<ValueType> const& dft, std::string const& file);
+
+        /*!
+         * Export DFT to JSON string.
+         *
+         * @param dft DFT.
+         */
+        template<typename ValueType>
+        std::string exportDFTToJsonString(storm::storage::DFT<ValueType> const& dft);
+
+        /*!
+         * Export DFT to SMT encoding.
+         *
+         * @param dft DFT.
+         * @param file File.
+         */
+        template<typename ValueType>
+        void exportDFTToSMT(storm::storage::DFT<ValueType> const& dft, std::string const& file);
+
+        /*!
+         * Transform DFT to GSPN.
+         *
+         * @param dft DFT.
+         */
+        template<typename ValueType>
+        void transformToGSPN(storm::storage::DFT<ValueType> const& dft);
+
+    }
+}

src/storm-dft/storage/dft/DFTBuilder.cpp → src/storm-dft/builder/DFTBuilder.cpp

@@ -11,15 +11,15 @@
 
 
 namespace storm {
-    namespace storage {
+    namespace builder {
         
         template<typename ValueType>
         std::size_t DFTBuilder<ValueType>::mUniqueOffset = 0;
 
         template<typename ValueType>
-        DFT<ValueType> DFTBuilder<ValueType>::build() {
+        storm::storage::DFT<ValueType> DFTBuilder<ValueType>::build() {
             for(auto& elem : mChildNames) {
-                DFTGatePointer gate = std::static_pointer_cast<DFTGate<ValueType>>(elem.first);
+                DFTGatePointer gate = std::static_pointer_cast<storm::storage::DFTGate<ValueType>>(elem.first);
                 for(auto const& child : elem.second) {
                     auto itFind = mElements.find(child);
                     if (itFind != mElements.end()) {
@@ -54,16 +54,16 @@ namespace storm {
 
             for(auto& elem : mDependencyChildNames) {
                 bool first = true;
-                std::vector<std::shared_ptr<DFTBE<ValueType>>> dependencies;
+                std::vector<std::shared_ptr<storm::storage::DFTBE<ValueType>>> dependencies;
                 for(auto const& childName : elem.second) {
                     auto itFind = mElements.find(childName);
                     STORM_LOG_ASSERT(itFind != mElements.end(), "Child '" << childName << "' not found");
                     DFTElementPointer childElement = itFind->second;
                     if (!first) {
                         STORM_LOG_ASSERT(childElement->isBasicElement(), "Child '" << childName << "' of dependency '" << elem.first->name() << "' must be BE.");
-                        dependencies.push_back(std::static_pointer_cast<DFTBE<ValueType>>(childElement));
+                        dependencies.push_back(std::static_pointer_cast<storm::storage::DFTBE<ValueType>>(childElement));
                     } else {
-                        elem.first->setTriggerElement(std::static_pointer_cast<DFTGate<ValueType>>(childElement));
+                        elem.first->setTriggerElement(std::static_pointer_cast<storm::storage::DFTGate<ValueType>>(childElement));
                         childElement->addOutgoingDependency(elem.first);
                     }
                     first = false;
@@ -92,7 +92,7 @@ namespace storm {
             }
 
             STORM_LOG_ASSERT(!mTopLevelIdentifier.empty(), "No top level element.");
-            DFT<ValueType> dft(elems, mElements[mTopLevelIdentifier]);
+            storm::storage::DFT<ValueType> dft(elems, mElements[mTopLevelIdentifier]);
 
             // Set layout info
             for (auto& elem : mElements) {
@@ -113,7 +113,7 @@ namespace storm {
                 if(elem->nrChildren() == 0 || elem->isDependency()) {
                     elem->setRank(0);
                 } else {
-                    DFTGatePointer gate = std::static_pointer_cast<DFTGate<ValueType>>(elem);
+                    DFTGatePointer gate = std::static_pointer_cast<storm::storage::DFTGate<ValueType>>(elem);
                     unsigned maxrnk = 0;
                     unsigned newrnk = 0;
 
@@ -131,7 +131,7 @@ namespace storm {
         }
 
         template<typename ValueType>
-        bool DFTBuilder<ValueType>::addRestriction(std::string const& name, std::vector<std::string> const& children, DFTElementType tp) {
+        bool DFTBuilder<ValueType>::addRestriction(std::string const& name, std::vector<std::string> const& children, storm::storage::DFTElementType tp) {
             if (children.size() <= 1) {
                 STORM_LOG_ERROR("Sequence enforcers require at least two children");
             }
@@ -140,10 +140,10 @@ namespace storm {
             }
             DFTRestrictionPointer restr;
             switch (tp) {
-                case DFTElementType::SEQ:
-                    restr = std::make_shared<DFTSeq<ValueType>>(mNextId++, name);
+                case storm::storage::DFTElementType::SEQ:
+                    restr = std::make_shared<storm::storage::DFTSeq<ValueType>>(mNextId++, name);
                     break;
-                case DFTElementType::MUTEX:
+                case storm::storage::DFTElementType::MUTEX:
                     // TODO notice that mutex state generation support is lacking anyway, as DONT CARE propagation would be broken for this.
                     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not supported.");
                     break;
@@ -159,7 +159,7 @@ namespace storm {
         }
 
         template<typename ValueType>
-        bool DFTBuilder<ValueType>::addStandardGate(std::string const& name, std::vector<std::string> const& children, DFTElementType tp) {
+        bool DFTBuilder<ValueType>::addStandardGate(std::string const& name, std::vector<std::string> const& children, storm::storage::DFTElementType tp) {
             STORM_LOG_ASSERT(children.size() > 0, "No child for " << name);
             if(mElements.count(name) != 0) {
                 // Element with that name already exists.
@@ -167,28 +167,28 @@ namespace storm {
             }
             DFTElementPointer element;
             switch(tp) {
-                case DFTElementType::AND:
-                    element = std::make_shared<DFTAnd<ValueType>>(mNextId++, name);
+                case storm::storage::DFTElementType::AND:
+                    element = std::make_shared<storm::storage::DFTAnd<ValueType>>(mNextId++, name);
                     break;
-                case DFTElementType::OR:
-                    element = std::make_shared<DFTOr<ValueType>>(mNextId++, name);
+                case storm::storage::DFTElementType::OR:
+                    element = std::make_shared<storm::storage::DFTOr<ValueType>>(mNextId++, name);
                     break;
-                case DFTElementType::PAND:
-                    element = std::make_shared<DFTPand<ValueType>>(mNextId++, name, pandDefaultInclusive);
+                case storm::storage::DFTElementType::PAND:
+                    element = std::make_shared<storm::storage::DFTPand<ValueType>>(mNextId++, name, pandDefaultInclusive);
                     break;
-                case DFTElementType::POR:
-                    element = std::make_shared<DFTPor<ValueType>>(mNextId++, name, porDefaultInclusive);
+                case storm::storage::DFTElementType::POR:
+                    element = std::make_shared<storm::storage::DFTPor<ValueType>>(mNextId++, name, porDefaultInclusive);
                     break;
-                case DFTElementType::SPARE:
-                   element = std::make_shared<DFTSpare<ValueType>>(mNextId++, name);
+                case storm::storage::DFTElementType::SPARE:
+                   element = std::make_shared<storm::storage::DFTSpare<ValueType>>(mNextId++, name);
                    break;
-                case DFTElementType::BE:
-                case DFTElementType::VOT:
-                case DFTElementType::PDEP:
+                case storm::storage::DFTElementType::BE:
+                case storm::storage::DFTElementType::VOT:
+                case storm::storage::DFTElementType::PDEP:
                     // Handled separately
                     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type handled separately.");
-                case DFTElementType::CONSTF:
-                case DFTElementType::CONSTS:
+                case storm::storage::DFTElementType::CONSTF:
+                case storm::storage::DFTElementType::CONSTS:
                     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not supported.");
                 default:
                     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not known.");
@@ -199,29 +199,29 @@ namespace storm {
         }
 
         template<typename ValueType>
-        void DFTBuilder<ValueType>::topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour, OrderElementsById<ValueType>>& visited, DFTElementVector& L) {
+        void DFTBuilder<ValueType>::topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour, storm::storage::OrderElementsById<ValueType>>& visited, DFTElementVector& L) {
             if(visited[n] == topoSortColour::GREY) {
                 throw storm::exceptions::WrongFormatException("DFT is cyclic");
             } else if(visited[n] == topoSortColour::WHITE) {
                 if(n->isGate()) {
                     visited[n] = topoSortColour::GREY;
-                    for (DFTElementPointer const& c : std::static_pointer_cast<DFTGate<ValueType>>(n)->children()) {
+                    for (DFTElementPointer const& c : std::static_pointer_cast<storm::storage::DFTGate<ValueType>>(n)->children()) {
                         topoVisit(c, visited, L);
                     }
                 }
                 // TODO restrictions and dependencies have no parents, so this can be done more efficiently.
                 if(n->isRestriction()) {
                     visited[n] = topoSortColour::GREY;
-                    for (DFTElementPointer const& c : std::static_pointer_cast<DFTRestriction<ValueType>>(n)->children()) {
+                    for (DFTElementPointer const& c : std::static_pointer_cast<storm::storage::DFTRestriction<ValueType>>(n)->children()) {
                         topoVisit(c, visited, L);
                     }
                 }
                 if(n->isDependency()) {
                     visited[n] = topoSortColour::GREY;
-                    for (DFTElementPointer const& c : std::static_pointer_cast<DFTDependency<ValueType>>(n)->dependentEvents()) {
+                    for (DFTElementPointer const& c : std::static_pointer_cast<storm::storage::DFTDependency<ValueType>>(n)->dependentEvents()) {
                         topoVisit(c, visited, L);
                     }
-                    topoVisit(std::static_pointer_cast<DFTDependency<ValueType>>(n)->triggerEvent(), visited, L);
+                    topoVisit(std::static_pointer_cast<storm::storage::DFTDependency<ValueType>>(n)->triggerEvent(), visited, L);
                 }
                 visited[n] = topoSortColour::BLACK;
                 L.push_back(n);
@@ -229,8 +229,8 @@ namespace storm {
         }
 
         template<typename ValueType>
-        std::vector<std::shared_ptr<DFTElement<ValueType>>> DFTBuilder<ValueType>::topoSort() {
-            std::map<DFTElementPointer, topoSortColour, OrderElementsById<ValueType>> visited;
+        std::vector<std::shared_ptr<storm::storage::DFTElement<ValueType>>> DFTBuilder<ValueType>::topoSort() {
+            std::map<DFTElementPointer, topoSortColour, storm::storage::OrderElementsById<ValueType>> visited;
             for(auto const& e : mElements) {
                 visited.insert(std::make_pair(e.second, topoSortColour::WHITE)); 
             }
@@ -252,22 +252,22 @@ namespace storm {
         void DFTBuilder<ValueType>::copyElement(DFTElementPointer element) {
             std::vector<std::string> children;
             switch (element->type()) {
-                case DFTElementType::AND:
-                case DFTElementType::OR:
-                case DFTElementType::PAND:
-                case DFTElementType::POR:
-                case DFTElementType::SPARE:
-                case DFTElementType::VOT:
+                case storm::storage::DFTElementType::AND:
+                case storm::storage::DFTElementType::OR:
+                case storm::storage::DFTElementType::PAND:
+                case storm::storage::DFTElementType::POR:
+                case storm::storage::DFTElementType::SPARE:
+                case storm::storage::DFTElementType::VOT:
                 {
-                    for (DFTElementPointer const& elem : std::static_pointer_cast<DFTGate<ValueType>>(element)->children()) {
+                    for (DFTElementPointer const& elem : std::static_pointer_cast<storm::storage::DFTGate<ValueType>>(element)->children()) {
                         children.push_back(elem->name());
                     }
-                    copyGate(std::static_pointer_cast<DFTGate<ValueType>>(element), children);
+                    copyGate(std::static_pointer_cast<storm::storage::DFTGate<ValueType>>(element), children);
                     break;
                 }
-                case DFTElementType::BE:
+                case storm::storage::DFTElementType::BE:
                 {
-                    std::shared_ptr<DFTBE<ValueType>> be = std::static_pointer_cast<DFTBE<ValueType>>(element);
+                    std::shared_ptr<storm::storage::DFTBE<ValueType>> be = std::static_pointer_cast<storm::storage::DFTBE<ValueType>>(element);
                     ValueType dormancyFactor = storm::utility::zero<ValueType>();
                     if (be->canFail()) {
                         dormancyFactor = be->passiveFailureRate() / be->activeFailureRate();
@@ -275,14 +275,14 @@ namespace storm {
                     addBasicElement(be->name(), be->activeFailureRate(), dormancyFactor, be->isTransient());
                     break;
                 }
-                case DFTElementType::CONSTF:
-                case DFTElementType::CONSTS:
+                case storm::storage::DFTElementType::CONSTF:
+                case storm::storage::DFTElementType::CONSTS:
                     // TODO
                     STORM_LOG_ASSERT(false, "Const elements not supported.");
                     break;
-                case DFTElementType::PDEP:
+                case storm::storage::DFTElementType::PDEP:
                 {
-                    DFTDependencyPointer dependency = std::static_pointer_cast<DFTDependency<ValueType>>(element);
+                    DFTDependencyPointer dependency = std::static_pointer_cast<storm::storage::DFTDependency<ValueType>>(element);
                     children.push_back(dependency->triggerEvent()->name());
                     for(auto const& depEv : dependency->dependentEvents()) {
                         children.push_back(depEv->name());
@@ -290,10 +290,10 @@ namespace storm {
                     addDepElement(element->name(), children, dependency->probability());
                     break;
                 }
-                case DFTElementType::SEQ:
-                case DFTElementType::MUTEX:
+                case storm::storage::DFTElementType::SEQ:
+                case storm::storage::DFTElementType::MUTEX:
                 {
-                    for (DFTElementPointer const& elem : std::static_pointer_cast<DFTRestriction<ValueType>>(element)->children()) {
+                    for (DFTElementPointer const& elem : std::static_pointer_cast<storm::storage::DFTRestriction<ValueType>>(element)->children()) {
                         children.push_back(elem->name());
                     }
                     addRestriction(element->name(), children, element->type());
@@ -308,15 +308,15 @@ namespace storm {
         template<typename ValueType>
         void DFTBuilder<ValueType>::copyGate(DFTGatePointer gate, std::vector<std::string> const& children) {
             switch (gate->type()) {
-                case DFTElementType::AND:
-                case DFTElementType::OR:
-                case DFTElementType::PAND:
-                case DFTElementType::POR:
-                case DFTElementType::SPARE:
+                case storm::storage::DFTElementType::AND:
+                case storm::storage::DFTElementType::OR:
+                case storm::storage::DFTElementType::PAND:
+                case storm::storage::DFTElementType::POR:
+                case storm::storage::DFTElementType::SPARE:
                     addStandardGate(gate->name(), children, gate->type());
                     break;
-                case DFTElementType::VOT:
-                    addVotElement(gate->name(), std::static_pointer_cast<DFTVot<ValueType>>(gate)->threshold(), children);
+                case storm::storage::DFTElementType::VOT:
+                    addVotElement(gate->name(), std::static_pointer_cast<storm::storage::DFTVot<ValueType>>(gate)->threshold(), children);
                     break;
                 default:
                     STORM_LOG_ASSERT(false, "Dft type not known.");

src/storm-dft/storage/dft/DFTBuilder.h → src/storm-dft/builder/DFTBuilder.h

@@ -11,18 +11,22 @@
 
 namespace storm {
     namespace storage {
+        // Forward declaration
         template<typename ValueType>
         class DFT;
+    }
+
+    namespace builder {
 
         template<typename ValueType>
         class DFTBuilder {
 
-            using DFTElementPointer = std::shared_ptr<DFTElement<ValueType>>;
+            using DFTElementPointer = std::shared_ptr<storm::storage::DFTElement<ValueType>>;
             using DFTElementVector = std::vector<DFTElementPointer>;
-            using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
+            using DFTGatePointer = std::shared_ptr<storm::storage::DFTGate<ValueType>>;
             using DFTGateVector = std::vector<DFTGatePointer>;
-            using DFTDependencyPointer = std::shared_ptr<DFTDependency<ValueType>>;
-            using DFTRestrictionPointer = std::shared_ptr<DFTRestriction<ValueType>>;
+            using DFTDependencyPointer = std::shared_ptr<storm::storage::DFTDependency<ValueType>>;
+            using DFTRestrictionPointer = std::shared_ptr<storm::storage::DFTRestriction<ValueType>>;
 
         private:
             std::size_t mNextId = 0;
@@ -34,7 +38,7 @@ namespace storm {
             std::unordered_map<DFTDependencyPointer, std::vector<std::string>> mDependencyChildNames;
             std::vector<DFTDependencyPointer> mDependencies;
             std::vector<DFTRestrictionPointer> mRestrictions;
-            std::unordered_map<std::string, DFTLayoutInfo> mLayoutInfo;
+            std::unordered_map<std::string, storm::storage::DFTLayoutInfo> mLayoutInfo;
             
         public:
             DFTBuilder(bool defaultInclusive = true, bool binaryDependencies = true) : pandDefaultInclusive(defaultInclusive), porDefaultInclusive(defaultInclusive), binaryDependencies(binaryDependencies) {
@@ -42,47 +46,47 @@ namespace storm {
             }
             
             bool addAndElement(std::string const& name, std::vector<std::string> const& children) {
-                return addStandardGate(name, children, DFTElementType::AND);
+                return addStandardGate(name, children, storm::storage::DFTElementType::AND);
             }
             
             bool addOrElement(std::string const& name, std::vector<std::string> const& children) {
-                return addStandardGate(name, children, DFTElementType::OR);
+                return addStandardGate(name, children, storm::storage::DFTElementType::OR);
             }
             
             bool addPandElement(std::string const& name, std::vector<std::string> const& children) {
-                return addStandardGate(name, children, DFTElementType::PAND);
+                return addStandardGate(name, children, storm::storage::DFTElementType::PAND);
             }
             
             bool addPandElement(std::string const& name, std::vector<std::string> const& children, bool inclusive) {
                 bool tmpDefault = pandDefaultInclusive;
                 pandDefaultInclusive = inclusive;
-                bool result = addStandardGate(name, children, DFTElementType::PAND);
+                bool result = addStandardGate(name, children, storm::storage::DFTElementType::PAND);
                 pandDefaultInclusive = tmpDefault;
                 return result;
             }
             
             bool addPorElement(std::string const& name, std::vector<std::string> const& children) {
-                return addStandardGate(name, children, DFTElementType::POR);
+                return addStandardGate(name, children, storm::storage::DFTElementType::POR);
             }
             
             bool addPorElement(std::string const& name, std::vector<std::string> const& children, bool inclusive) {
                 bool tmpDefault = porDefaultInclusive;
                 porDefaultInclusive = inclusive;
-                bool result = addStandardGate(name, children, DFTElementType::POR);
+                bool result = addStandardGate(name, children, storm::storage::DFTElementType::POR);
                 pandDefaultInclusive = tmpDefault;
                 return result;
             }
             
             bool addSpareElement(std::string const& name, std::vector<std::string> const& children) {
-                return addStandardGate(name, children, DFTElementType::SPARE);
+                return addStandardGate(name, children, storm::storage::DFTElementType::SPARE);
             }
 
             bool addSequenceEnforcer(std::string const& name, std::vector<std::string> const& children) {
-                return addRestriction(name, children, DFTElementType::SEQ);
+                return addRestriction(name, children, storm::storage::DFTElementType::SEQ);
             }
 
             bool addMutex(std::string const& name, std::vector<std::string> const& children) {
-                return addRestriction(name, children, DFTElementType::MUTEX);
+                return addRestriction(name, children, storm::storage::DFTElementType::MUTEX);
             }
             
             bool addDepElement(std::string const& name, std::vector<std::string> const& children, ValueType probability) {
@@ -125,15 +129,13 @@ namespace storm {
                             }
                             STORM_LOG_ASSERT(storm::utility::isOne(probability) || children.size() == 2,
                                              "PDep with multiple children supported.");
-                            DFTDependencyPointer element = std::make_shared<DFTDependency<ValueType>>(mNextId++,
-                                                                                                      nameDep,
-                                                                                                      probability);
+                            DFTDependencyPointer element = std::make_shared<storm::storage::DFTDependency<ValueType>>(mNextId++, nameDep, probability);
                             mElements[element->name()] = element;
                             mDependencyChildNames[element] = {trigger, children[i]};
                             mDependencies.push_back(element);
                         }
                     } else {
-                        DFTDependencyPointer element = std::make_shared<DFTDependency<ValueType>>(mNextId++, name, probability);
+                        DFTDependencyPointer element = std::make_shared<storm::storage::DFTDependency<ValueType>>(mNextId++, name, probability);
                         mElements[element->name()] = element;
                         mDependencyChildNames[element] = children;
                         mDependencies.push_back(element);
@@ -161,7 +163,7 @@ namespace storm {
                     STORM_LOG_ERROR("Voting gates with threshold higher than the number of children is not supported.");
                     return false;
                 }
-                DFTElementPointer element = std::make_shared<DFTVot<ValueType>>(mNextId++, name, threshold);
+                DFTElementPointer element = std::make_shared<storm::storage::DFTVot<ValueType>>(mNextId++, name, threshold);
                 
                 mElements[name] = element;
                 mChildNames[element] = children;
@@ -173,7 +175,7 @@ namespace storm {
                 //failureRate > 0
                 //0 <= dormancyFactor <= 1
 
-                mElements[name] = std::make_shared<DFTBE<ValueType>>(mNextId++, name, failureRate, dormancyFactor, transient);
+                mElements[name] = std::make_shared<storm::storage::DFTBE<ValueType>>(mNextId++, name, failureRate, dormancyFactor, transient);
                 return true;
             }
 
@@ -189,7 +191,7 @@ namespace storm {
             
             std::string getUniqueName(std::string name);
             
-            DFT<ValueType> build();
+            storm::storage::DFT<ValueType> build();
             
             /**
              * Copy element and insert it again in the builder.
@@ -211,13 +213,13 @@ namespace storm {
             
             unsigned computeRank(DFTElementPointer const& elem);
             
-            bool addStandardGate(std::string const& name, std::vector<std::string> const& children, DFTElementType tp);
+            bool addStandardGate(std::string const& name, std::vector<std::string> const& children, storm::storage::DFTElementType tp);
 
-            bool addRestriction(std::string const& name, std::vector<std::string> const& children, DFTElementType tp);
+            bool addRestriction(std::string const& name, std::vector<std::string> const& children, storm::storage::DFTElementType tp);
 
             enum class topoSortColour {WHITE, BLACK, GREY}; 
             
-            void topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour, OrderElementsById<ValueType>>& visited, DFTElementVector& L);
+            void topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour, storm::storage::OrderElementsById<ValueType>>& visited, DFTElementVector& L);
 
             DFTElementVector topoSort();
             

src/storm-dft/builder/ExplicitDFTModelBuilder.cpp

@@ -58,7 +58,7 @@ namespace storm {
                 usedHeuristic(storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().getApproximationHeuristic()),
                 generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates),
                 matrixBuilder(!generator.isDeterministicModel()),
-                stateStorage(((dft.stateVectorSize() / 64) + 1) * 64),
+                stateStorage(dft.stateBitVectorSize()),
                 // TODO Matthias: make choosable
                 //explorationQueue(dft.nrElements()+1, 0, 1)
                 explorationQueue(200, 0, 0.9)

src/storm-dft/modelchecker/dft/DFTASFChecker.h

@@ -33,13 +33,15 @@ namespace storm {
                 
             }
             
+            friend bool operator<(SpareAndChildPair const& p1, SpareAndChildPair const& p2) {
+                return p1.spareIndex < p2.spareIndex || (p1.spareIndex == p2.spareIndex && p1.childIndex < p2.childIndex);
+            }
+
+        private:
             uint64_t spareIndex;
             uint64_t childIndex;
         };
         
-        bool operator<(SpareAndChildPair const& p1, SpareAndChildPair const& p2) {
-            return p1.spareIndex < p2.spareIndex || (p1.spareIndex == p2.spareIndex && p1.childIndex < p2.childIndex);
-        }
         
         class DFTASFChecker {
             using ValueType = double;