Merge from master

volkm · Aug 26, 2024 · 74451e2 · 74451e2
2 parents a394899 + 79908cc
commit 74451e2
Show file tree

Hide file tree

Showing 202 changed files with 1,998 additions and 1,225 deletions.
diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs
@@ -13,3 +13,4 @@ e58679da05190fe064ca063b07ac56428162a8fb
 634053fe63e39b80fff2355bb4e5b50839cd1e68
 a177724097d3f807a6b8950b1cd378c34d040d1b
 5016fac7d4014f1113c3d410a65aa5b39a74be64
+c0dae886d1e8283a783ab884f64b443e436c106b
diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml
@@ -11,8 +11,8 @@ on:
   pull_request:
 
 env:
-  # GitHub runners currently have two cores
-  NR_JOBS: "2"
+  # GitHub runners currently have 4 cores
+  NR_JOBS: "4"
 
 jobs:
   # Perform in-depth tests with different configurations
@@ -185,7 +185,7 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        distro: ["debian-11", "debian-12", "ubuntu-20.04", "ubuntu-22.04", "ubuntu-24.04"]
+        distro: ["debian-12", "ubuntu-22.04", "ubuntu-24.04"]
         buildType: ["Release"]
     steps:
       - name: Git clone

diff --git a/.github/workflows/doxygen.yml b/.github/workflows/doxygen.yml
@@ -12,8 +12,8 @@ env:
   BASE_IMG: "movesrwth/carl-storm:ci-release"
   STORM_GIT_URL: "${{ github.server_url }}/${{ github.repository }}.git"
   STORM_BRANCH: "master"
-  # github runners currently have two cores
-  NR_JOBS: "2"
+  # GitHub runners currently have 4 cores
+  NR_JOBS: "4"
 
 
 jobs:
@@ -25,7 +25,7 @@ jobs:
     if: github.repository_owner == 'moves-rwth'
     steps:
       - name: Init Docker
-        run: sudo docker run -d -it --name storm --privileged ${BASE_IMG}
+        run: sudo docker run -d -it --name storm ${BASE_IMG}
 
         # We should not do partial updates :/
         # but we need to install some dependencies

diff --git a/.github/workflows/formatapply.yml b/.github/workflows/formatapply.yml
@@ -9,16 +9,16 @@ jobs:
     steps:
       - uses: actions/checkout@v4
       # apply the formatting twice as a workaround for a clang-format bug
-      - uses: DoozyX/clang-format-lint-action@v0.17
+      - uses: DoozyX/clang-format-lint-action@v0.18
         with:
           source: './src'
-          clangFormatVersion: 17
+          clangFormatVersion: 18
           style: file
           inplace: True
-      - uses: DoozyX/clang-format-lint-action@v0.17
+      - uses: DoozyX/clang-format-lint-action@v0.18
         with:
           source: './src'
-          clangFormatVersion: 17
+          clangFormatVersion: 18
           style: file
           inplace: True
       - name: Commit Formatting

diff --git a/.github/workflows/formatcheck.yml b/.github/workflows/formatcheck.yml
@@ -8,8 +8,8 @@ jobs:
 
     steps:
     - uses: actions/checkout@v4
-    - uses: DoozyX/clang-format-lint-action@v0.17
+    - uses: DoozyX/clang-format-lint-action@v0.18
       with:
         source: './src'
-        clangFormatVersion: 17
+        clangFormatVersion: 18
         style: file
diff --git a/.github/workflows/release_docker.yml b/.github/workflows/release_docker.yml
@@ -10,8 +10,8 @@ on:
         default: 'x.y.z'
 
 env:
-  # GitHub runners currently have two cores
-  NR_JOBS: "2"
+  # GitHub runners currently have 4 cores
+  NR_JOBS: "4"
 
 jobs:
   deploy:

diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,21 +1,42 @@
-
 Changelog
 ==============
 
 This changelog lists only the most important changes. Smaller (bug)fixes as well as non-mature features are not part of the changelog.
 The releases of major and minor versions contain an overview of changes since the last major/minor update.
 
-Version 1.8.x
+Version 1.9.x
 -------------
 
-## Version 1.8.2
+## Version 1.9.0 (2024/08)
+- Improved expected visiting times (EVTs) and steady state distribution computations.
+- Support for interval-based models.
+- Robust VI.
+- Significantly improved compilation times.
+- Support for logarithm expressions in PRISM and JANI.
+- Support for sin and cos operators, and PI and Euler constants in JANI parser.
+- Extraction of schedulers for minimal expected total rewards.
+- More efficient MEC and SCC decompositions.
+- Revised LP encoding for multi-objective verification under simple strategies.
+- Added CLI option `--permute` to re-order the states after building.
+- Added CLI option `--build:state limit <number>` to limit the number of explored states.
 - Print all linked libraries when using `--version`.
-- Removed HyPro as dependency.
+- Removed support for HyPro and Cuda.
+- Moved gamebased-ar to own library.
+- Various bug fixes.
 - `storm-conv`: Removed option `--stdout`.
-- `storm-pars`: completely reworked the command-line interface (and partially the c++ API).
+- `storm-dft`: Fixes and improvements for DFT symmetries and DFT simulation.
+- `storm-pars`: Completely reworked the command-line interface (and partially the C++ API).
+- `storm-pars`: "Time travelling" optimization.
+- `storm-pgcl`: Removed the library.
 - Developer: Require at least CMake version 3.15.
 - Developer: Moved `storm-config.h.in` into `src` directory.
-- Developer: Use Dockerfile in CI.
+- Developer: Use various Dockerfiles in CI.
+- Developer: Revised includes and use pre-compiled headers.
+- Developer: Fixed various compiler warnings.
+
+
+Version 1.8.x
+-------------
 
 ## Version 1.8.1 (2023/06)
 - Workaround for issue with Boost >= 1.81

diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -1,6 +1,6 @@
-cmake_minimum_required (VERSION 3.16)
+cmake_minimum_required (VERSION 3.22)
 
-set(CMAKE_CXX_STANDARD 17)
+set(CMAKE_CXX_STANDARD 20)
 
 # Set project name
 project (storm CXX C)
@@ -157,21 +157,25 @@ set(STORM_TEST_RESOURCES_DIR "${PROJECT_SOURCE_DIR}/resources/examples/testfiles
 # Auto-detect operating system.
 set(MACOSX 0)
 set(LINUX 0)
+set(APPLE_SILICON 0)
 if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
 	# Mac OS
 	set(OPERATING_SYSTEM "Mac OS")
         set(MACOSX 1)
+	if(${CMAKE_SYSTEM_PROCESSOR} MATCHES arm64)
+		set(APPLE_SILICON 1)
+	endif()
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
-    # Linux
+	# Linux
 	set(OPERATING_SYSTEM "Linux")
         set(LINUX 1)
 elseif(WIN32)
-    # Assuming Windows.
-    set(OPERATING_SYSTEM "Windows")
+	# Assuming Windows.
+	set(OPERATING_SYSTEM "Windows")
 else()
-    message(WARNING "We are unsure about your operating system.")
-    set(OPERATING_SYSTEM "Linux")
-    set(LINUX 1)
+	message(WARNING "We are unsure about your operating system.")
+	set(OPERATING_SYSTEM "Linux")
+	set(LINUX 1)
 ENDIF()
 message(STATUS "Storm - Detected operating system ${OPERATING_SYSTEM}.")
 
@@ -184,20 +188,12 @@ else()
 	set(SHIPPED_CARL_USE_GINAC OFF)
 endif()
 
-# Detect Apple Silicon and adjust settings
-if(APPLE AND ${CMAKE_SYSTEM_PROCESSOR} MATCHES arm64)
-	message(STATUS "Storm - Detected that target system uses Apple Silicon.")
-	message(WARNING "Compiling natively on Apple Silicon is experimental. Please report issues to [email protected]. For more information visit https://www.stormchecker.org/documentation/obtain-storm/apple-silicon.html")
-	set(APPLE_SILICON 1)
-	if(STORM_USE_CLN_EA OR STORM_USE_CLN_RF)
-		message(WARNING "CLN and GiNaC are currently not supported on Apple Silicon-based architectures. Disabling Storm and carl usage of the libraries.")
-		set(STORM_USE_CLN_EA OFF)
-		set(STORM_USE_CLN_RF OFF)
-	endif()
-	set(SHIPPED_CARL_USE_CLN_NUMBERS OFF)
-	set(SHIPPED_CARL_USE_GINAC OFF)
+# Warning for Apple Silicon
+if(APPLE_SILICON)
+	message(WARNING "Compiling natively on Apple Silicon is experimental. Please report any issues to [email protected].")
 endif()
 
+
 set(DYNAMIC_EXT ".so")
 set(STATIC_EXT ".a")
 set(LIB_PREFIX "lib")

diff --git a/doc/offline_package.md b/doc/offline_package.md
@@ -51,7 +51,7 @@ cd storm
 mkdir -p build
 cd build
 cmake ..
-make storm-main -j$THREADS
+make storm-cli -j$THREADS
 cd ../../
 
 echo "Installation successfull."

diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
@@ -379,7 +379,7 @@ if (STORM_SHIPPED_CARL)
             SOURCE_DIR ${STORM_3RDPARTY_BINARY_DIR}/carl
             CONFIGURE_COMMAND ""
             BUILD_IN_SOURCE 1
-            BUILD_COMMAND make lib_carl
+            BUILD_COMMAND make lib_carl -j${STORM_RESOURCES_BUILD_JOBCOUNT}
             INSTALL_COMMAND make install -j${STORM_RESOURCES_BUILD_JOBCOUNT}
             LOG_BUILD ON
 			LOG_INSTALL ON

diff --git a/resources/3rdparty/include_cudd.cmake b/resources/3rdparty/include_cudd.cmake
@@ -51,8 +51,9 @@ ExternalProject_Add(
         PREFIX ${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0
         PATCH_COMMAND ${CMAKE_COMMAND} -E env ${CUDD_AUTOTOOLS_LOCATIONS} ${AUTORECONF}
         CONFIGURE_COMMAND ${STORM_3RDPARTY_SOURCE_DIR}/cudd-3.0.0/configure --enable-shared --enable-obj --with-pic=yes --prefix=${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0 --libdir=${CUDD_LIB_DIR} CC=${CMAKE_C_COMPILER} CXX=${CUDD_CXX_COMPILER} ${CUDD_INCLUDE_FLAGS}
-        BUILD_COMMAND make ${STORM_CUDD_FLAGS} ${CUDD_AUTOTOOLS_LOCATIONS}
-        INSTALL_COMMAND make install -j${STORM_RESOURCES_BUILD_JOBCOUNT} ${CUDD_AUTOTOOLS_LOCATIONS}
+	# Multi-threaded compilation could lead to compile issues
+        BUILD_COMMAND make -j1 ${STORM_CUDD_FLAGS} ${CUDD_AUTOTOOLS_LOCATIONS}
+        INSTALL_COMMAND make install -j1 ${CUDD_AUTOTOOLS_LOCATIONS}
         BUILD_IN_SOURCE 0
         LOG_CONFIGURE ON
         LOG_BUILD ON

diff --git a/resources/3rdparty/include_glpk.cmake b/resources/3rdparty/include_glpk.cmake
@@ -16,7 +16,7 @@ else()
         PREFIX ${STORM_3RDPARTY_BINARY_DIR}/glpk-5.0
         SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/glpk-5.0
         CONFIGURE_COMMAND ${STORM_3RDPARTY_SOURCE_DIR}/glpk-5.0/configure --prefix=${STORM_3RDPARTY_BINARY_DIR}/glpk-5.0  --libdir=${GLPK_LIB_DIR} CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} ${GLPK_INCLUDE_FLAGS}
-        BUILD_COMMAND make "CFLAGS=-O3 -w"
+        BUILD_COMMAND make "CFLAGS=-O3 -w" -j${STORM_RESOURCES_BUILD_JOBCOUNT}
         INSTALL_COMMAND make install -j${STORM_RESOURCES_BUILD_JOBCOUNT}
         BUILD_IN_SOURCE 0
         LOG_CONFIGURE ON
@@ -35,4 +35,4 @@ set(STORM_HAVE_GLPK ON)
 message (STATUS "Storm - Linking with glpk ${GLPK_VERSION_STRING}")
 
 add_imported_library(glpk SHARED ${GLPK_LIBRARIES} ${GLPK_INCLUDE_DIR})
-list(APPEND STORM_DEP_TARGETS glpk_SHARED)
+list(APPEND STORM_DEP_TARGETS glpk_SHARED)
diff --git a/resources/3rdparty/include_spot.cmake b/resources/3rdparty/include_spot.cmake
@@ -30,28 +30,28 @@ if(STORM_USE_SPOT_SHIPPED AND NOT STORM_HAVE_SPOT)
 
     # download and install shipped Spot
     ExternalProject_Add(spot
-        URL http://www.lrde.epita.fr/dload/spot/spot-2.10.4.tar.gz # When updating, also change version output below
+        URL https://www.lrde.epita.fr/dload/spot/spot-2.12.tar.gz # When updating, also change version output below
         DOWNLOAD_NO_PROGRESS TRUE
         DOWNLOAD_DIR ${STORM_3RDPARTY_BINARY_DIR}/spot_src
         SOURCE_DIR ${STORM_3RDPARTY_BINARY_DIR}/spot_src
         PREFIX ${STORM_3RDPARTY_BINARY_DIR}/spot
         CONFIGURE_COMMAND ${STORM_3RDPARTY_BINARY_DIR}/spot_src/configure --prefix=${STORM_3RDPARTY_BINARY_DIR}/spot --disable-python
         BUILD_COMMAND make -j${STORM_RESOURCES_BUILD_JOBCOUNT}
-        INSTALL_COMMAND make install
+        INSTALL_COMMAND make install -j${STORM_RESOURCES_BUILD_JOBCOUNT}
         LOG_CONFIGURE ON
         LOG_BUILD ON
         LOG_INSTALL ON
         BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/spot/lib/libspot${DYNAMIC_EXT}
     )
-	add_dependencies(resources spot)
+    add_dependencies(resources spot)
     set(SPOT_INCLUDE_DIR "${STORM_3RDPARTY_BINARY_DIR}/spot/include/")
     set(SPOT_DIR "${STORM_3RDPARTY_BINARY_DIR}/spot/")
     set(SPOT_LIBRARIES ${STORM_3RDPARTY_BINARY_DIR}/spot/lib/libspot${DYNAMIC_EXT})
     set(SPOT_LIBRARIES "${SPOT_LIBRARIES};${STORM_3RDPARTY_BINARY_DIR}/spot/lib/libbddx${DYNAMIC_EXT}")
     set(STORM_HAVE_SPOT ON)
     set(STORM_SHIPPED_SPOT ON)
 
-    message(STATUS "Storm - Using shipped version of Spot 2.10.4 (include: ${SPOT_INCLUDE_DIR}, library ${SPOT_LIBRARIES}).")
+    message(STATUS "Storm - Using shipped version of Spot 2.12 (include: ${SPOT_INCLUDE_DIR}, library ${SPOT_LIBRARIES}).")
 
 endif()
 

diff --git a/resources/examples/testfiles/ctmc/simple1.sm b/resources/examples/testfiles/ctmc/simple1.sm
@@ -0,0 +1,11 @@
+ctmc
+
+module main
+x : [0..1] init 0;
+[] x=0 -> 6 : (x'=1);
+endmodule
+
+rewards
+	x=0: 1;
+endrewards
+
diff --git a/resources/examples/testfiles/dft/symmetry7.dft b/resources/examples/testfiles/dft/symmetry7.dft
@@ -0,0 +1,13 @@
+toplevel "A";
+"A" or "M" "N";
+"M" and "M1" "M2" "M3" "M4";
+"N" and "N1" "N2" "N3" "N4";
+"M1" lambda=0.5 dorm=0;
+"M2" lambda=0.5 dorm=0;
+"M3" lambda=0.5 dorm=0;
+"M4" lambda=1 dorm=0;
+"N1" lambda=0.5 dorm=0;
+"N2" lambda=0.5 dorm=0;
+"N3" lambda=1 dorm=0;
+"N4" lambda=1 dorm=0;
+