diff --git a/.github/workflows/Dockerfile.alpine b/.github/workflows/Dockerfile.alpine index efbaf7f3f3..0b59b10674 100644 --- a/.github/workflows/Dockerfile.alpine +++ b/.github/workflows/Dockerfile.alpine @@ -47,6 +47,7 @@ ARG packages="" RUN apk add --no-cache \ bash \ + ccache \ cmake \ make \ gcc \ @@ -69,12 +70,17 @@ RUN apk add --no-cache \ # Build Storm ############# +ENV CCACHE_DIR=/root/.ccache RUN mkdir /opt/storm WORKDIR /opt/storm # Copy the content of the current local Storm repository into the Docker image COPY . . +# Seed ccache from the workflow cache directory if available. +RUN mkdir -p "$CCACHE_DIR" && \ + if [ -d "/opt/storm/.ci-ccache" ]; then cp -a /opt/storm/.ci-ccache/. "$CCACHE_DIR"/; fi + # Switch to build directory RUN mkdir -p /opt/storm/build WORKDIR /opt/storm/build @@ -102,6 +108,6 @@ RUN cmake -DCMAKE_BUILD_TYPE=$build_type \ # Build Storm # (This can be adapted to only build 'storm' or 'binaries' depending on custom needs) -RUN make -j $no_threads +RUN ccache --max-size=3G && ccache --zero-stats && make -j $no_threads && ccache --show-stats --verbose WORKDIR /opt/storm diff --git a/.github/workflows/Dockerfile.archlinux b/.github/workflows/Dockerfile.archlinux index 9f0935e01b..3d962b071e 100644 --- a/.github/workflows/Dockerfile.archlinux +++ b/.github/workflows/Dockerfile.archlinux @@ -51,6 +51,7 @@ ARG packages="" RUN pacman -Syu --noconfirm # Updates needed as Archlinux is rolling release RUN pacman -S --noconfirm \ base-devel \ + ccache \ cmake \ git \ boost \ @@ -67,12 +68,17 @@ RUN pacman -S --noconfirm \ # Build Storm ############# +ENV CCACHE_DIR=/root/.ccache RUN mkdir /opt/storm WORKDIR /opt/storm # Copy the content of the current local Storm repository into the Docker image COPY . . +# Seed ccache from the workflow cache directory if available. +RUN mkdir -p "$CCACHE_DIR" && \ + if [ -d "/opt/storm/.ci-ccache" ]; then cp -a /opt/storm/.ci-ccache/. "$CCACHE_DIR"/; fi + # Switch to build directory RUN mkdir -p /opt/storm/build WORKDIR /opt/storm/build @@ -100,6 +106,6 @@ RUN cmake -DCMAKE_BUILD_TYPE=$build_type \ # Build Storm # (This can be adapted to only build 'storm' or 'binaries' depending on custom needs) -RUN make -j $no_threads +RUN ccache --max-size=3G && ccache --zero-stats && make -j $no_threads && ccache --show-stats --verbose WORKDIR /opt/storm diff --git a/.github/workflows/Dockerfile.release b/.github/workflows/Dockerfile.release index 6b7aa3b52f..b220e06cab 100644 --- a/.github/workflows/Dockerfile.release +++ b/.github/workflows/Dockerfile.release @@ -55,25 +55,25 @@ COPY . . RUN mkdir -p /opt/storm/build \ && cd /opt/storm/build \ && cmake -DCMAKE_BUILD_TYPE=$build_type \ - -DSTORM_PORTABLE=ON \ - -DSTORM_BUILD_TESTS=OFF \ - -DSTORM_CARL_GIT_TAG=$carl_tag \ - -DSTORM_DISABLE_CUDD=$disable_cudd \ - -DSTORM_DISABLE_GLPK=$disable_glpk \ - -DSTORM_DISABLE_GMM=$disable_gmm \ - -DSTORM_DISABLE_GUROBI=$disable_gurobi \ - -DSTORM_DISABLE_LIBARCHIVE=$disable_libarchive \ - -DSTORM_DISABLE_MATHSAT=$disable_mathsat \ - -DSTORM_DISABLE_SOPLEX=$disable_soplex \ - -DSTORM_DISABLE_SPOT=$disable_spot \ - -DSTORM_DISABLE_SYLVAN=$disable_sylvan \ - -DSTORM_DISABLE_XERCES=$disable_xerces \ - -DSTORM_DISABLE_Z3=$disable_z3 \ - -DSTORM_DEVELOPER=$developer \ - -DSTORM_USE_CLN_EA=$cln_exact \ - -DSTORM_USE_CLN_RF=$cln_ratfunc \ - -DSTORM_COMPILE_WITH_ALL_SANITIZERS=$all_sanitizers \ - $cmake_args .. \ + -DSTORM_PORTABLE=ON \ + -DSTORM_BUILD_TESTS=OFF \ + -DSTORM_CARL_GIT_TAG=$carl_tag \ + -DSTORM_DISABLE_CUDD=$disable_cudd \ + -DSTORM_DISABLE_GLPK=$disable_glpk \ + -DSTORM_DISABLE_GMM=$disable_gmm \ + -DSTORM_DISABLE_GUROBI=$disable_gurobi \ + -DSTORM_DISABLE_LIBARCHIVE=$disable_libarchive \ + -DSTORM_DISABLE_MATHSAT=$disable_mathsat \ + -DSTORM_DISABLE_SOPLEX=$disable_soplex \ + -DSTORM_DISABLE_SPOT=$disable_spot \ + -DSTORM_DISABLE_SYLVAN=$disable_sylvan \ + -DSTORM_DISABLE_XERCES=$disable_xerces \ + -DSTORM_DISABLE_Z3=$disable_z3 \ + -DSTORM_DEVELOPER=$developer \ + -DSTORM_USE_CLN_EA=$cln_exact \ + -DSTORM_USE_CLN_RF=$cln_ratfunc \ + -DSTORM_COMPILE_WITH_ALL_SANITIZERS=$all_sanitizers \ + $cmake_args .. \ && make -j $no_threads \ && make install -j $no_threads \ && cd /opt \ diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml deleted file mode 100644 index e89ea30dab..0000000000 --- a/.github/workflows/buildtest.yml +++ /dev/null @@ -1,494 +0,0 @@ -name: Build Test -# Builds and tests storm on various platforms -# also deploys images to DockerHub - -on: - schedule: - # run daily - - cron: '0 6 * * *' - # needed to trigger the workflow manually - workflow_dispatch: - pull_request: - -env: - # GitHub runners currently have 4 cores - NR_JOBS: "4" - -jobs: - # Perform in-depth tests with different configurations - indepthTests: - name: Indepth Tests (${{ matrix.config.name }}, ${{ matrix.config.buildType }}) - runs-on: ubuntu-latest - strategy: - matrix: - config: - - {name: "GMP exact; GMP rational functions; All dependencies", - baseImg: "storm-dependencies:latest", - buildType: "Debug", - disable_cudd: "OFF", - disable_glpk: "OFF", - disable_gmm: "OFF", - disable_gurobi: "OFF", - disable_libarchive: "OFF", - disable_mathsat: "OFF", - disable_soplex: "OFF", - disable_spot: "OFF", - disable_sylvan: "OFF", - disable_xerces: "OFF", - disable_z3: "OFF", - Developer: "ON", - ClnExact: "OFF", - ClnRatfunc: "OFF", - AllSanitizers: "OFF", - cmakeArgs: "-DSTORM_WARNING_AS_ERROR=ON" - } - - {name: "CLN exact; GMP rational functions; All dependencies", - baseImg: "storm-dependencies:latest", - buildType: "Debug", - disable_cudd: "OFF", - disable_glpk: "OFF", - disable_gmm: "OFF", - disable_gurobi: "OFF", - disable_libarchive: "OFF", - disable_mathsat: "OFF", - disable_soplex: "OFF", - disable_spot: "OFF", - disable_sylvan: "OFF", - disable_xerces: "OFF", - disable_z3: "OFF", - Developer: "ON", - ClnExact: "ON", - ClnRatfunc: "OFF", - AllSanitizers: "OFF", - cmakeArgs: "-DSTORM_WARNING_AS_ERROR=ON" - } - - {name: "CLN exact; CLN rational functions; All dependencies", - baseImg: "storm-dependencies:latest", - buildType: "Debug", - disable_cudd: "OFF", - disable_glpk: "OFF", - disable_gmm: "OFF", - disable_gurobi: "OFF", - disable_libarchive: "OFF", - disable_mathsat: "OFF", - disable_soplex: "OFF", - disable_spot: "OFF", - disable_sylvan: "OFF", - disable_xerces: "OFF", - disable_z3: "OFF", - Developer: "ON", - ClnExact: "ON", - ClnRatfunc: "ON", - AllSanitizers: "OFF", - cmakeArgs: "-DSTORM_WARNING_AS_ERROR=ON" - } - - {name: "GMP exact; CLN rational functions; No dependencies", - baseImg: "storm-dependencies:latest", - buildType: "Debug", - disable_cudd: "ON", - disable_glpk: "ON", - disable_gmm: "ON", - disable_gurobi: "ON", - disable_libarchive: "ON", - disable_mathsat: "ON", - disable_soplex: "ON", - disable_spot: "ON", - disable_sylvan: "ON", - disable_xerces: "ON", - disable_z3: "ON", - Developer: "ON", - ClnExact: "OFF", - ClnRatfunc: "ON", - AllSanitizers: "OFF", - cmakeArgs: "-DSTORM_WARNING_AS_ERROR=ON" - } - - {name: "Minimal dependencies (without CLN)", - baseImg: "storm-basesystem:minimal_dependencies", - buildType: "Debug", - disable_cudd: "ON", - disable_glpk: "ON", - disable_gmm: "ON", - disable_gurobi: "ON", - disable_libarchive: "ON", - disable_mathsat: "ON", - disable_soplex: "ON", - disable_spot: "ON", - disable_sylvan: "ON", - disable_xerces: "ON", - disable_z3: "ON", - Developer: "ON", - ClnExact: "OFF", - ClnRatfunc: "OFF", - AllSanitizers: "OFF", - cmakeArgs: "-DSTORM_WARNING_AS_ERROR=ON" - } - steps: - - name: Git clone - uses: actions/checkout@v7 - - name: Build storm from Dockerfile - run: | - docker build -t movesrwth/storm:ci . \ - --build-arg BASE_IMAGE=movesrwth/${{ matrix.config.baseImg }} \ - --build-arg build_type="${{ matrix.config.buildType }}" \ - --build-arg carl_tag="master" \ - --build-arg disable_cudd="${{ matrix.config.disable_cudd }}" \ - --build-arg disable_glpk="${{ matrix.config.disable_glpk }}" \ - --build-arg disable_gmm="${{ matrix.config.disable_gmm }}" \ - --build-arg disable_gurobi="${{ matrix.config.disable_gurobi }}" \ - --build-arg disable_libarchive="${{ matrix.config.disable_libarchive }}" \ - --build-arg disable_mathsat="${{ matrix.config.disable_mathsat }}" \ - --build-arg disable_soplex="${{ matrix.config.disable_soplex }}" \ - --build-arg disable_spot="${{ matrix.config.disable_spot }}" \ - --build-arg disable_sylvan="${{ matrix.config.disable_sylvan }}" \ - --build-arg disable_xerces="${{ matrix.config.disable_xerces }}" \ - --build-arg disable_z3="${{ matrix.config.disable_z3 }}" \ - --build-arg developer="${{ matrix.config.Developer }}" \ - --build-arg cln_exact="${{ matrix.config.ClnExact }}" \ - --build-arg cln_ratfunc="${{ matrix.config.ClnRatfunc }}" \ - --build-arg all_sanitizers="${{ matrix.config.AllSanitizers }}" \ - --build-arg cmake_args="${{ matrix.config.cmakeArgs }}" \ - --build-arg no_threads=${NR_JOBS} - - name: Run Docker - run: docker run -d -it --name ci movesrwth/storm:ci - - name: Run storm - run: docker exec ci bash -c "/opt/storm/build/bin/storm --version" - - name: Check compile flags - uses: ./.github/actions/check-compile-flags-action - with: - buildType: ${{ matrix.config.buildType }} - docker: true - - name: Run tests - # Disabled sanitizer checks for now - #run: docker exec ci bash -c "cd /opt/storm/build; ASAN_OPTIONS=detect_leaks=0,detect_odr_violation=0 ctest test --output-on-failure" - run: docker exec ci bash -c "cd /opt/storm/build; ctest test --output-on-failure" - - name: Build starter-project - uses: ./.github/actions/starter-project-action - with: - docker: true - stormDir: "/opt/storm/build" - command: "--help" # TODO using --help as running the starter-project requires Z3. - - name: Install storm - run: docker exec ci bash -c "cd /opt/storm/build; make install" - - name: Remove build dir - run: | - docker exec ci bash -c "rm -rf /opt/storm/build" - - name: Run installed storm - run: | - docker exec ci bash -c "/usr/local/bin/storm --version" - - name: Build starter-project on installed Storm - uses: ./.github/actions/starter-project-action - with: - docker: true - stormDir: "" - command: "--help" # TODO using --help as running the starter-project requires Z3. - - compilerTests: - # Build and run with different compilers (GCC, Clang) - # Run on latest Archlinux version to get most recent compiler versions - name: Compiler Tests (${{ matrix.config.name }} on ${{ matrix.config.distro }}, ${{ matrix.config.buildType }}) - runs-on: ubuntu-latest - strategy: - matrix: - config: - - {name: "GCC", - buildType: "Debug", - Developer: "ON", - cmakeArgs: "-DCMAKE_C_COMPILER=gcc -DCMAKE_CXX_COMPILER=g++ -DSTORM_WARNING_AS_ERROR=ON", - packages: "", - distro: "archlinux" - } - - {name: "Clang", - buildType: "Debug", - Developer: "ON", - cmakeArgs: "-DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DSTORM_WARNING_AS_ERROR=ON", - packages: "clang", - distro: "archlinux" - } - - {name: "musl", - buildType: "Debug", - Developer: "ON", - cmakeArgs: "-DCMAKE_C_COMPILER=gcc -DCMAKE_CXX_COMPILER=g++ -DSTORM_WARNING_AS_ERROR=ON", - packages: "", - distro: "alpine" - } - steps: - - name: Git clone - uses: actions/checkout@v7 - - name: Replace Dockerfile - run: cp .github/workflows/Dockerfile.${{ matrix.config.distro }} Dockerfile - - name: Build storm from Dockerfile - run: | - docker build -t movesrwth/storm:ci . \ - --build-arg build_type="${{ matrix.config.buildType }}" \ - --build-arg carl_tag="master" \ - --build-arg developer="${{ matrix.config.Developer }}" \ - --build-arg cmake_args="${{ matrix.config.cmakeArgs }}" \ - --build-arg packages="${{ matrix.config.packages }}" \ - --build-arg no_threads=${NR_JOBS} - # Omitting arguments disable_*, cln_exact, cln_ratfunc, all_sanitizers - - name: Run Docker - run: docker run -d -it --name ci movesrwth/storm:ci - - name: Run storm - run: docker exec ci bash -c "/opt/storm/build/bin/storm --version" - - name: Check compile flags - uses: ./.github/actions/check-compile-flags-action - with: - buildType: ${{ matrix.config.buildType }} - docker: true - - name: Run tests - run: docker exec ci bash -c "cd /opt/storm/build; ctest test --output-on-failure" - - name: Build starter-project - uses: ./.github/actions/starter-project-action - with: - docker: true - stormDir: "/opt/storm/build" - command: "/opt/storm/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" - - name: Install storm - run: docker exec ci bash -c "cd /opt/storm/build; make install" - - name: Remove build dir - run: | - docker exec ci bash -c "rm -rf /opt/storm/build" - - name: Run installed storm - run: | - docker exec ci bash -c "/usr/local/bin/storm --version" - - name: Build starter-project on installed Storm - uses: ./.github/actions/starter-project-action - with: - docker: true - stormDir: "" - command: "/opt/storm/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" - - linuxTests: - name: Linux Tests (${{ matrix.distro }}, ${{ matrix.buildType }}) on ${{ matrix.runner }} - runs-on: ${{ matrix.runner }} - strategy: - matrix: - distro: ["debian-12", "ubuntu-24.04", "debian-13"] - buildType: ["Release"] - runner: [ubuntu-latest, ubuntu-24.04-arm] - steps: - - name: Git clone - uses: actions/checkout@v7 - - name: Build storm from Dockerfile - run: | - docker build -t movesrwth/storm:ci . \ - --build-arg BASE_IMAGE=movesrwth/storm-basesystem:${{ matrix.distro }} \ - --build-arg build_type="${{ matrix.buildType }}" \ - --build-arg carl_tag="master" \ - --build-arg no_threads=${NR_JOBS} \ - --build-arg cmake_args="-DSTORM_WARNING_AS_ERROR=ON" - # Omitting arguments developer, disable_*, cln_exact, cln_ratfunc, all_sanitizers - - name: Run Docker - run: docker run -d -it --name ci movesrwth/storm:ci - - name: Run storm - run: docker exec ci bash -c "/opt/storm/build/bin/storm --version" - - name: Check compile flags - uses: ./.github/actions/check-compile-flags-action - with: - buildType: ${{ matrix.buildType }} - docker: true - - name: Run tests - run: docker exec ci bash -c "cd /opt/storm/build; ctest test --output-on-failure" - - name: Build starter-project - uses: ./.github/actions/starter-project-action - with: - docker: true - stormDir: "/opt/storm/build" - command: "/opt/storm/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" - - name: Install storm - run: docker exec ci bash -c "cd /opt/storm/build; make install" - - name: Remove build dir - run: | - docker exec ci bash -c "rm -rf /opt/storm/build" - - name: Run installed storm - run: | - docker exec ci bash -c "/usr/local/bin/storm --version" - - name: Build starter-project on installed Storm - uses: ./.github/actions/starter-project-action - with: - docker: true - stormDir: "" - command: "/opt/storm/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" - - macTests: - name: macOS Tests (${{ matrix.config.name }}, ${{ matrix.config.buildType }}) - strategy: - matrix: - config: - - {name: "MacOS 14, ARM", - distro: "macos-14", - xcode: "15.4", - buildType: "Debug" - } - - {name: "MacOS 15, ARM", - distro: "macos-15", - xcode: "16.4", - buildType: "Debug" - } - - {name: "MacOS 26, ARM", - distro: "macos-26", - xcode: "latest-stable", - buildType: "Debug" - } - - {name: "MacOS 26, Intel", - distro: "macos-26-intel", - xcode: "latest-stable", - buildType: "Debug" - } - runs-on: ${{ matrix.config.distro }} - steps: - - uses: maxim-lobanov/setup-xcode@v1 - with: - xcode-version: ${{ matrix.config.xcode }} - - name: Git clone - uses: actions/checkout@v7 - - name: Install dependencies - # cmake and gmp are already installed - run: | - brew update - brew install automake boost cln ginac glpk hwloc libarchive xerces-c z3 - - name: Configure storm - run: | - mkdir build - cd build - cmake .. -DCMAKE_BUILD_TYPE="${{ matrix.config.buildType }}" -DSTORM_CARL_GIT_TAG="master" -DSTORM_WARNING_AS_ERROR=ON - - name: Build storm - working-directory: ./build - run: make -j ${NR_JOBS} - - name: Run storm (build tree) - working-directory: ./build - run: ./bin/storm - - name: Check compile flags - uses: ./.github/actions/check-compile-flags-action - with: - buildType: ${{ matrix.config.buildType }} - docker: false - - name: Run tests - working-directory: ./build - run: ctest test --output-on-failure - - name: Build starter-project - uses: ./.github/actions/starter-project-action - with: - docker: false - stormDir: "${GITHUB_WORKSPACE}/build" - command: "${GITHUB_WORKSPACE}/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" - - name: Install storm - working-directory: ./build - run: sudo make install - - name: Remove build dir - run: | - rm -rf ${GITHUB_WORKSPACE}/build - - name: Run installed storm - run: | - /usr/local/bin/storm --version - - name: Build starter-project on installed Storm - uses: ./.github/actions/starter-project-action - with: - docker: false - stormDir: "" - command: "${GITHUB_WORKSPACE}/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" - - deploy: - name: Test and Deploy (${{ matrix.buildType.name }}) - runs-on: ubuntu-latest - strategy: - matrix: - buildType: - - {name: "Debug", - dockerTag: "ci-debug", - baseImg: "storm-dependencies:latest", - Developer: "ON", - cmakeArgs: "-DSTORM_WARNING_AS_ERROR=ON" - } - - {name: "Release", - dockerTag: "ci", - baseImg: "storm-dependencies:latest", - Developer: "OFF", - cmakeArgs: "-DSTORM_WARNING_AS_ERROR=ON" - } - steps: - - name: Git clone - uses: actions/checkout@v7 - - name: Git describe - id: ghd - uses: proudust/gh-describe@v3 - - name: Set static Storm version - run: echo "set(STORM_VERSION_COMMITS_AHEAD ${{ steps.ghd.outputs.distance }})" >> version.cmake - - name: Build storm from Dockerfile - run: | - docker build -t movesrwth/storm:${{ matrix.buildType.dockerTag }} . \ - --build-arg BASE_IMAGE=movesrwth/${{ matrix.buildType.baseImg }} \ - --build-arg build_type="${{ matrix.buildType.name }}" \ - --build-arg carl_tag="master" \ - --build-arg developer="${{ matrix.buildType.Developer }}" \ - --build-arg cmake_args="${{ matrix.buildType.cmakeArgs }}" \ - --build-arg no_threads=${NR_JOBS} - # Omitting arguments disable_*, cln_exact, cln_ratfunc, all_sanitizers - - name: Run Docker - run: docker run -d -it --name ci movesrwth/storm:${{ matrix.buildType.dockerTag }} - - name: Check compile flags - uses: ./.github/actions/check-compile-flags-action - with: - buildType: ${{ matrix.buildType.name }} - docker: true - - name: Run tests - run: docker exec ci bash -c "cd /opt/storm/build; ctest test --output-on-failure" - - name: Build starter-project - uses: ./.github/actions/starter-project-action - with: - docker: true - stormDir: "/opt/storm/build" - command: "/opt/storm/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" - - name: Install storm - run: docker exec ci bash -c "cd /opt/storm/build; make install" - - name: Temporarily move build dir - run: | - docker exec ci bash -c "mv /opt/storm/build /opt/storm/build-backup" - - name: Run installed storm - run: | - docker exec ci bash -c "/usr/local/bin/storm --version" - - name: Build starter-project on installed Storm - uses: ./.github/actions/starter-project-action - with: - docker: true - stormDir: "" - command: "/opt/storm/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" - - name: Restore build dir - run: | - docker exec ci bash -c "mv /opt/storm/build-backup /opt/storm/build" - - name: Login into docker - # Only login if using master on original repo (and not for pull requests or forks) - if: github.repository_owner == 'stormchecker' && github.ref == 'refs/heads/master' - uses: docker/login-action@v4 - with: - username: ${{ secrets.STORM_CI_DOCKER_USERNAME }} - password: ${{ secrets.STORM_CI_DOCKER_TOKEN }} - - name: Deploy storm - # Only deploy if using master on original repo (and not for pull requests or forks) - if: github.repository_owner == 'stormchecker' && github.ref == 'refs/heads/master' - run: | - docker commit ci movesrwth/storm:${{ matrix.buildType.dockerTag }} - docker push movesrwth/storm:${{ matrix.buildType.dockerTag }} - - notify: - name: Email notification - runs-on: ubuntu-latest - needs: [indepthTests, compilerTests, linuxTests, macTests, deploy] - # Only run in main repo and even if previous step failed - if: github.repository_owner == 'stormchecker' && always() - steps: - - uses: technote-space/workflow-conclusion-action@v3 - - uses: dawidd6/action-send-mail@v18 - with: - server_address: ${{ secrets.STORM_CI_MAIL_SERVER }} - server_port: 587 - username: ${{ secrets.STORM_CI_MAIL_USERNAME }} - password: ${{ secrets.STORM_CI_MAIL_PASSWORD }} - subject: "[You broke it] CI run failed for ${{ github.repository }}" - body: - "CI job of ${{ github.repository }} has failed for commit ${{ github.sha }}.\n\ - The error type is: ${{ env.WORKFLOW_CONCLUSION }}.\n\n\ - For more information, see https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}" - to: ${{ secrets.STORM_CI_MAIL_RECIPIENTS }} - from: Github Actions - if: env.WORKFLOW_CONCLUSION != 'success' # notify only if failure diff --git a/.github/workflows/ci-pr.yml b/.github/workflows/ci-pr.yml new file mode 100644 index 0000000000..96fafe8624 --- /dev/null +++ b/.github/workflows/ci-pr.yml @@ -0,0 +1,140 @@ +name: CI PR +# Runs on every pull request commit: compile-flag checks and short tests. +# All jobs are cached and fail-fast. + +on: + pull_request: + +jobs: + buildTests: + if: "! contains(github.event.pull_request.labels.*.name, 'ready for review')" + strategy: + fail-fast: true + matrix: + config: + - {name: "Debug; All dependencies", + buildType: "Debug", + baseImg: "movesrwth/storm-dependencies:latest", + disable_all: false, + ClnExact: false, + ClnRatfunc: false + } + - {name: "Release; All dependencies", + buildType: "Release", + baseImg: "movesrwth/storm-dependencies:latest", + disable_all: false, + ClnExact: false, + ClnRatfunc: false + } + - {name: "Release; GMP; GMP; Minimal dependencies", + buildType: "Release", + baseImg: "movesrwth/storm-basesystem:minimal_dependencies", + disable_all: true, + ClnExact: false, + ClnRatfunc: false + } + uses: ./.github/workflows/test-build.yml + with: + nr_jobs: "4" + name: ${{ matrix.config.name }} + baseImg: ${{ matrix.config.baseImg }} + buildType: ${{ matrix.config.buildType }} + disable_cudd: ${{ matrix.config.disable_all }} + disable_glpk: ${{ matrix.config.disable_all }} + disable_gmm: ${{ matrix.config.disable_all }} + disable_gurobi: ${{ matrix.config.disable_all }} + disable_libarchive: ${{ matrix.config.disable_all }} + disable_mathsat: ${{ matrix.config.disable_all }} + disable_soplex: ${{ matrix.config.disable_all }} + disable_spot: ${{ matrix.config.disable_all }} + disable_sylvan: ${{ matrix.config.disable_all }} + disable_xerces: ${{ matrix.config.disable_all }} + disable_z3: ${{ matrix.config.disable_all }} + Developer: ${{ matrix.config.buildType == 'Debug' }} + ClnExact: ${{ matrix.config.ClnExact }} + ClnRatfunc: ${{ matrix.config.ClnRatfunc }} + AllSanitizers: false + restore_cache: true + save_cache: true + install: false + + compilerTests: + if: "! contains(github.event.pull_request.labels.*.name, 'ready for review')" + strategy: + fail-fast: true + matrix: + config: + - {name: "GCC", + cmakeArgs: "-DCMAKE_C_COMPILER=gcc -DCMAKE_CXX_COMPILER=g++ -DSTORM_WARNING_AS_ERROR=ON", + packages: "", + dockerfile: ".github/workflows/Dockerfile.archlinux", + baseImg: "archlinux:latest" + } + - {name: "Clang", + cmakeArgs: "-DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DSTORM_WARNING_AS_ERROR=ON", + packages: "clang", + dockerfile: ".github/workflows/Dockerfile.archlinux", + baseImg: "archlinux:latest" + } + uses: ./.github/workflows/test-build.yml + with: + nr_jobs: "4" + name: ${{ matrix.config.name }} + buildType: Debug + Developer: true + baseImg: ${{ matrix.config.baseImg }} + cmakeArgs: ${{ matrix.config.cmakeArgs }} + packages: ${{ matrix.config.packages }} + dockerfile: ${{ matrix.config.dockerfile }} + starterProjectCommand: "/opt/storm/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" + restore_cache: true + save_cache: true + install: false + + linuxTests: + if: "! contains(github.event.pull_request.labels.*.name, 'ready for review')" + strategy: + fail-fast: true + matrix: + distro: ["debian-12", "ubuntu-24.04"] + uses: ./.github/workflows/test-linux.yml + with: + nr_jobs: "4" + distro: ${{ matrix.distro }} + buildType: Release + runner: ubuntu-latest + restore_cache: true + save_cache: true + install: false + + macTests: + if: "! contains(github.event.pull_request.labels.*.name, 'ready for review')" + strategy: + fail-fast: true + matrix: + config: + - {name: "Mac 14, ARM", + distro: "macos-14", + xcode: "15.4", + buildType: "Release" + } + - {name: "Mac 26, ARM", + distro: "macos-26", + xcode: "latest-stable", + buildType: "Release" + } + - {name: "Mac 26, Intel", + distro: "macos-26-intel", + xcode: "latest-stable", + buildType: "Release" + } + uses: ./.github/workflows/test-mac.yml + with: + nr_jobs: "4" + name: ${{ matrix.config.name }} + distro: ${{ matrix.config.distro }} + xcode: ${{ matrix.config.xcode }} + buildType: ${{ matrix.config.buildType }} + restore_cache: true + save_cache: true + install: false diff --git a/.github/workflows/ci-ready-for-review.yml b/.github/workflows/ci-ready-for-review.yml new file mode 100644 index 0000000000..446d07149b --- /dev/null +++ b/.github/workflows/ci-ready-for-review.yml @@ -0,0 +1,175 @@ +name: CI PR Ready for Review / Master +# Runs on PRs labelled "ready for review" and on every master push. +# Full task suite: compile flags, all tests, starter project, install, deploy. +# Cache is read-only on PRs, disabled on master. + +on: + push: + branches: [master] + pull_request: + types: [opened, synchronize, reopened, labeled] + +jobs: + buildTests: + if: contains(github.event.pull_request.labels.*.name, 'ready for review') || github.event_name == 'push' + strategy: + fail-fast: true + matrix: + config: + - {name: "Debug; All dependencies", + buildType: "Debug", + baseImg: "movesrwth/storm-dependencies:latest", + disable_all: false, + ClnExact: false, + ClnRatfunc: false + } + - {name: "Release; All dependencies", + buildType: "Release", + baseImg: "movesrwth/storm-dependencies:latest", + disable_all: false, + ClnExact: false, + ClnRatfunc: false + } + - {name: "Release; GMP; GMP; Required dependencies", + buildType: "Release", + baseImg: "movesrwth/storm-basesystem:latest", + disable_all: false, + ClnExact: false, + ClnRatfunc: false + } + - {name: "Release; CLN; CLN; Required dependencies", + buildType: "Release", + baseImg: "movesrwth/storm-basesystem:latest", + disable_all: false, + ClnExact: true, + ClnRatfunc: true + } + uses: ./.github/workflows/test-build.yml + with: + nr_jobs: "4" + name: ${{ matrix.config.name }} + baseImg: ${{ matrix.config.baseImg }} + buildType: ${{ matrix.config.buildType }} + disable_cudd: ${{ matrix.config.disable_all }} + disable_glpk: ${{ matrix.config.disable_all }} + disable_gmm: ${{ matrix.config.disable_all }} + disable_gurobi: ${{ matrix.config.disable_all }} + disable_libarchive: ${{ matrix.config.disable_all }} + disable_mathsat: ${{ matrix.config.disable_all }} + disable_soplex: ${{ matrix.config.disable_all }} + disable_spot: ${{ matrix.config.disable_all }} + disable_sylvan: ${{ matrix.config.disable_all }} + disable_xerces: ${{ matrix.config.disable_all }} + disable_z3: ${{ matrix.config.disable_all }} + Developer: ${{ matrix.config.buildType == 'Debug' }} + ClnExact: ${{ matrix.config.ClnExact }} + ClnRatfunc: ${{ matrix.config.ClnRatfunc }} + AllSanitizers: false + restore_cache: ${{ github.event_name != 'push' }} + save_cache: false + install: true + + compilerTests: + if: contains(github.event.pull_request.labels.*.name, 'ready for review') || github.event_name == 'push' + strategy: + fail-fast: true + matrix: + config: + - {name: "GCC", + cmakeArgs: "-DCMAKE_C_COMPILER=gcc -DCMAKE_CXX_COMPILER=g++ -DSTORM_WARNING_AS_ERROR=ON", + packages: "", + dockerfile: ".github/workflows/Dockerfile.archlinux", + baseImg: "archlinux:latest" + } + - {name: "Clang", + cmakeArgs: "-DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DSTORM_WARNING_AS_ERROR=ON", + packages: "clang", + dockerfile: ".github/workflows/Dockerfile.archlinux", + baseImg: "archlinux:latest" + } + uses: ./.github/workflows/test-build.yml + with: + nr_jobs: "4" + name: ${{ matrix.config.name }} + buildType: Debug + Developer: true + baseImg: ${{ matrix.config.baseImg }} + cmakeArgs: ${{ matrix.config.cmakeArgs }} + packages: ${{ matrix.config.packages }} + dockerfile: ${{ matrix.config.dockerfile }} + starterProjectCommand: "/opt/storm/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" + restore_cache: ${{ github.event_name != 'push' }} + save_cache: false + install: true + + linuxTests: + if: contains(github.event.pull_request.labels.*.name, 'ready for review') || github.event_name == 'push' + strategy: + fail-fast: true + matrix: + distro: ["debian-12", "debian-13", "ubuntu-24.04"] + uses: ./.github/workflows/test-linux.yml + with: + nr_jobs: "4" + distro: ${{ matrix.distro }} + buildType: Release + runner: ubuntu-latest + restore_cache: ${{ github.event_name != 'push' }} + save_cache: false + install: true + + macTests: + if: contains(github.event.pull_request.labels.*.name, 'ready for review') || github.event_name == 'push' + strategy: + fail-fast: true + matrix: + config: + - {name: "Mac 14, ARM", + distro: "macos-14", + xcode: "15.4", + buildType: "Release" + } + - {name: "Mac 15, ARM", + distro: "macos-15", + xcode: "16.4", + buildType: "Release" + } + - {name: "Mac 26, ARM", + distro: "macos-26", + xcode: "latest-stable", + buildType: "Release" + } + - {name: "Mac 26, Intel", + distro: "macos-26-intel", + xcode: "latest-stable", + buildType: "Release" + } + uses: ./.github/workflows/test-mac.yml + with: + nr_jobs: "4" + name: ${{ matrix.config.name }} + distro: ${{ matrix.config.distro }} + xcode: ${{ matrix.config.xcode }} + buildType: ${{ matrix.config.buildType }} + restore_cache: ${{ github.event_name != 'push' }} + save_cache: false + install: true + + deploy: + if: github.event_name == 'push' && github.ref == 'refs/heads/master' + strategy: + fail-fast: true + matrix: + config: + - {buildType: "Debug", + dockerTag: "ci-debug" + } + - {buildType: "Release", + dockerTag: "ci" + } + uses: ./.github/workflows/test-deploy.yml + with: + nr_jobs: "4" + buildType: ${{ matrix.config.buildType }} + dockerTag: ${{ matrix.config.dockerTag }} + secrets: inherit diff --git a/.github/workflows/ci-weekly.yml b/.github/workflows/ci-weekly.yml new file mode 100644 index 0000000000..cf4111e5c7 --- /dev/null +++ b/.github/workflows/ci-weekly.yml @@ -0,0 +1,199 @@ +name: CI Weekly +# Comprehensive weekly test run across all configurations. +# No cache, not fail-fast, full task suite including deploy. + +on: + schedule: + - cron: '0 6 * * 1' # Every Monday at 06:00 UTC + workflow_dispatch: + +jobs: + buildTests: + strategy: + fail-fast: false + matrix: + buildType: ["Debug", "Release"] + config: + - {name: "GMP; GMP; Required dependencies", + baseImg: "movesrwth/storm-basesystem:latest", + disable_all: false, + ClnExact: false, + ClnRatfunc: false + } + - {name: "CLN; GMP; Required dependencies", + baseImg: "movesrwth/storm-basesystem:latest", + disable_all: false, + ClnExact: true, + ClnRatfunc: false + } + - {name: "GMP; CLN; Required dependencies", + baseImg: "movesrwth/storm-basesystem:latest", + disable_all: false, + ClnExact: false, + ClnRatfunc: true + } + - {name: "CLN; CLN; Required dependencies", + baseImg: "movesrwth/storm-basesystem:latest", + disable_all: false, + ClnExact: true, + ClnRatfunc: true + } + - {name: "All dependencies (disabled)", + baseImg: "movesrwth/storm-dependencies:latest", + disable_all: true, + ClnExact: false, + ClnRatfunc: false + } + - {name: "Minimal dependencies", + baseImg: "movesrwth/storm-basesystem:minimal_dependencies", + disable_all: true, + ClnExact: false, + ClnRatfunc: false + } + uses: ./.github/workflows/test-build.yml + with: + nr_jobs: "4" + name: ${{ matrix.config.name }} + baseImg: ${{ matrix.config.baseImg }} + buildType: ${{ matrix.buildType }} + disable_cudd: ${{ matrix.config.disable_all }} + disable_glpk: ${{ matrix.config.disable_all }} + disable_gmm: ${{ matrix.config.disable_all }} + disable_gurobi: ${{ matrix.config.disable_all }} + disable_libarchive: ${{ matrix.config.disable_all }} + disable_mathsat: ${{ matrix.config.disable_all }} + disable_soplex: ${{ matrix.config.disable_all }} + disable_spot: ${{ matrix.config.disable_all }} + disable_sylvan: ${{ matrix.config.disable_all }} + disable_xerces: ${{ matrix.config.disable_all }} + disable_z3: ${{ matrix.config.disable_all }} + Developer: ${{ matrix.buildType == 'Debug' }} + ClnExact: ${{ matrix.config.ClnExact }} + ClnRatfunc: ${{ matrix.config.ClnRatfunc }} + AllSanitizers: false + restore_cache: false + save_cache: false + install: true + + compilerTests: + strategy: + fail-fast: false + matrix: + buildType: ["Debug", "Release"] + config: + - {name: "GCC", + cmakeArgs: "-DCMAKE_C_COMPILER=gcc -DCMAKE_CXX_COMPILER=g++ -DSTORM_WARNING_AS_ERROR=ON", + packages: "", + dockerfile: ".github/workflows/Dockerfile.archlinux", + baseImg: "archlinux:latest" + } + - {name: "Clang", + cmakeArgs: "-DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DSTORM_WARNING_AS_ERROR=ON", + packages: "clang", + dockerfile: ".github/workflows/Dockerfile.archlinux", + baseImg: "archlinux:latest" + } + uses: ./.github/workflows/test-build.yml + with: + nr_jobs: "4" + name: ${{ matrix.config.name }} + buildType: ${{ matrix.buildType }} + Developer: ${{ matrix.buildType == 'Debug' }} + baseImg: ${{ matrix.config.baseImg }} + cmakeArgs: ${{ matrix.config.cmakeArgs }} + packages: ${{ matrix.config.packages }} + dockerfile: ${{ matrix.config.dockerfile }} + starterProjectCommand: "/opt/storm/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" + restore_cache: false + save_cache: false + install: true + + linuxTests: + strategy: + fail-fast: false + matrix: + distro: ["debian-12", "debian-13", "ubuntu-24.04"] + buildType: ["Debug", "Release"] + uses: ./.github/workflows/test-linux.yml + with: + nr_jobs: "4" + distro: ${{ matrix.distro }} + buildType: ${{ matrix.buildType }} + runner: ubuntu-latest + restore_cache: false + save_cache: false + install: true + + macTests: + strategy: + fail-fast: false + matrix: + buildType: ["Debug", "Release"] + config: + - {name: "Mac 14, ARM", + distro: "macos-14", + xcode: "15.4" + } + - {name: "Mac 15, ARM", + distro: "macos-15", + xcode: "16.4" + } + - {name: "Mac 26, ARM", + distro: "macos-26", + xcode: "latest-stable" + } + - {name: "Mac 26, Intel", + distro: "macos-26-intel", + xcode: "latest-stable" + } + uses: ./.github/workflows/test-mac.yml + with: + nr_jobs: "4" + name: ${{ matrix.config.name }} + distro: ${{ matrix.config.distro }} + xcode: ${{ matrix.config.xcode }} + buildType: ${{ matrix.buildType }} + restore_cache: false + save_cache: false + install: true + + deploy: + strategy: + fail-fast: false + matrix: + config: + - {buildType: "Debug", + dockerTag: "ci-debug" + } + - {buildType: "Release", + dockerTag: "ci" + } + # TODO: Add binaries build/publish configs + uses: ./.github/workflows/test-deploy.yml + with: + nr_jobs: "4" + buildType: ${{ matrix.config.buildType }} + dockerTag: ${{ matrix.config.dockerTag }} + secrets: inherit + + notify: + name: Email notification + runs-on: ubuntu-latest + needs: [buildTests, compilerTests, linuxTests, macTests, deploy] + if: github.repository_owner == 'stormchecker' && always() + steps: + - uses: technote-space/workflow-conclusion-action@v3 + - uses: dawidd6/action-send-mail@v18 + with: + server_address: ${{ secrets.STORM_CI_MAIL_SERVER }} + server_port: 587 + username: ${{ secrets.STORM_CI_MAIL_USERNAME }} + password: ${{ secrets.STORM_CI_MAIL_PASSWORD }} + subject: "[You broke it] CI Weekly failed for ${{ github.repository }}" + body: + "CI job of ${{ github.repository }} has failed for commit ${{ github.sha }}.\n\ + The error type is: ${{ env.WORKFLOW_CONCLUSION }}.\n\n\ + For more information, see https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}" + to: ${{ secrets.STORM_CI_MAIL_RECIPIENTS }} + from: Github Actions + if: env.WORKFLOW_CONCLUSION != 'success' diff --git a/.github/workflows/test-build.yml b/.github/workflows/test-build.yml new file mode 100644 index 0000000000..a70be8c3cb --- /dev/null +++ b/.github/workflows/test-build.yml @@ -0,0 +1,194 @@ +name: Build Tests + +on: + workflow_call: + inputs: + nr_jobs: + description: "Number of parallel build jobs" + type: string + default: "4" + name: + description: "Display name for the test configuration" + type: string + required: true + buildType: + description: "CMake build type (Debug or Release)" + type: string + default: "Debug" + Developer: + description: "Enable developer mode" + type: boolean + default: true + cmakeArgs: + description: "Extra CMake arguments" + type: string + default: "-DSTORM_WARNING_AS_ERROR=ON" + dockerfile: + description: "Path to the Dockerfile to use" + type: string + default: "Dockerfile" + starterProjectCommand: + description: "Command to pass to the starter-project" + type: string + default: "--help" + baseImg: + description: "Full base image name (e.g. movesrwth/storm-dependencies:latest or archlinux:latest)" + type: string + default: "movesrwth/storm-dependencies:latest" + disable_cudd: + type: boolean + default: false + disable_glpk: + type: boolean + default: false + disable_gmm: + type: boolean + default: false + disable_gurobi: + type: boolean + default: false + disable_libarchive: + type: boolean + default: false + disable_mathsat: + type: boolean + default: false + disable_soplex: + type: boolean + default: false + disable_spot: + type: boolean + default: false + disable_sylvan: + type: boolean + default: false + disable_xerces: + type: boolean + default: false + disable_z3: + type: boolean + default: false + ClnExact: + description: "Use CLN for exact arithmetic" + type: boolean + default: false + ClnRatfunc: + description: "Use CLN for rational functions" + type: boolean + default: false + AllSanitizers: + description: "Enable all sanitizers" + type: boolean + default: false + packages: + description: "Extra packages to install (e.g. clang)" + type: string + default: "" + restore_cache: + description: "Restore ccache from cache" + type: boolean + default: false + save_cache: + description: "Save ccache to cache" + type: boolean + default: false + install: + description: "Run post-build steps: starter project, install, run installed storm" + type: boolean + default: true + +jobs: + buildTests: + name: Build Tests (${{ inputs.name }}, ${{ inputs.buildType }}) + runs-on: ubuntu-latest + env: + NR_JOBS: ${{ inputs.nr_jobs }} + steps: + - name: Git clone + uses: actions/checkout@v7 + - name: Restore ccache (Docker) + id: ccache-restore + if: inputs.restore_cache + uses: actions/cache/restore@v4 + with: + path: .ci-ccache + key: buildtest-ccache-${{ inputs.name }}-${{ inputs.buildType }}-${{ hashFiles(inputs.dockerfile, 'CMakeLists.txt') }}-${{ github.run_id }} + restore-keys: | + buildtest-ccache-${{ inputs.name }}-${{ inputs.buildType }}- + buildtest-ccache-${{ inputs.name }}- + - name: Build storm from Dockerfile + run: | + mkdir -p .ci-ccache + docker build -t movesrwth/storm:ci --file ${{ inputs.dockerfile }} . \ + --build-arg BASE_IMAGE=${{ inputs.baseImg }} \ + --build-arg build_type="${{ inputs.buildType }}" \ + --build-arg disable_cudd="${{ inputs.disable_cudd && 'ON' || 'OFF' }}" \ + --build-arg disable_glpk="${{ inputs.disable_glpk && 'ON' || 'OFF' }}" \ + --build-arg disable_gmm="${{ inputs.disable_gmm && 'ON' || 'OFF' }}" \ + --build-arg disable_gurobi="${{ inputs.disable_gurobi && 'ON' || 'OFF' }}" \ + --build-arg disable_libarchive="${{ inputs.disable_libarchive && 'ON' || 'OFF' }}" \ + --build-arg disable_mathsat="${{ inputs.disable_mathsat && 'ON' || 'OFF' }}" \ + --build-arg disable_soplex="${{ inputs.disable_soplex && 'ON' || 'OFF' }}" \ + --build-arg disable_spot="${{ inputs.disable_spot && 'ON' || 'OFF' }}" \ + --build-arg disable_sylvan="${{ inputs.disable_sylvan && 'ON' || 'OFF' }}" \ + --build-arg disable_xerces="${{ inputs.disable_xerces && 'ON' || 'OFF' }}" \ + --build-arg disable_z3="${{ inputs.disable_z3 && 'ON' || 'OFF' }}" \ + --build-arg developer="${{ inputs.Developer && 'ON' || 'OFF' }}" \ + --build-arg cln_exact="${{ inputs.ClnExact && 'ON' || 'OFF' }}" \ + --build-arg cln_ratfunc="${{ inputs.ClnRatfunc && 'ON' || 'OFF' }}" \ + --build-arg all_sanitizers="${{ inputs.AllSanitizers && 'ON' || 'OFF' }}" \ + --build-arg cmake_args="${{ inputs.cmakeArgs }}" \ + --build-arg packages="${{ inputs.packages }}" \ + --build-arg no_threads=${NR_JOBS} + - name: Export ccache from Docker image + if: inputs.save_cache && always() && steps.ccache-restore.outputs.cache-hit != 'true' + run: | + rm -rf .ci-ccache + mkdir -p .ci-ccache + docker create --name ccache-extract movesrwth/storm:ci + docker cp ccache-extract:/root/.ccache/. .ci-ccache/ || true + docker rm ccache-extract + - name: Save ccache (Docker) + if: inputs.save_cache && always() && steps.ccache-restore.outputs.cache-hit != 'true' + uses: actions/cache/save@v4 + with: + path: .ci-ccache + key: buildtest-ccache-${{ inputs.name }}-${{ inputs.buildType }}-${{ hashFiles(inputs.dockerfile, 'CMakeLists.txt') }}-${{ github.run_id }} + - name: Run Docker + run: docker run -d -it --name ci movesrwth/storm:ci + - name: Run storm + run: docker exec ci bash -c "/opt/storm/build/bin/storm --version" + - name: Check compile flags + uses: ./.github/actions/check-compile-flags-action + with: + buildType: ${{ inputs.buildType }} + docker: true + - name: Run tests + # Disabled sanitizer checks for now + #run: docker exec ci bash -c "cd /opt/storm/build; ASAN_OPTIONS=detect_leaks=0,detect_odr_violation=0 ctest test --output-on-failure" + run: docker exec ci bash -c "cd /opt/storm/build; ctest test --output-on-failure" + - name: Build starter-project + if: inputs.install + uses: ./.github/actions/starter-project-action + with: + docker: true + stormDir: "/opt/storm/build" + command: ${{ inputs.starterProjectCommand }} + - name: Install storm + if: inputs.install + run: docker exec ci bash -c "cd /opt/storm/build; make install" + - name: Remove build dir + if: inputs.install + run: | + docker exec ci bash -c "rm -rf /opt/storm/build" + - name: Run installed storm + if: inputs.install + run: | + docker exec ci bash -c "/usr/local/bin/storm --version" + - name: Build starter-project on installed Storm + if: inputs.install + uses: ./.github/actions/starter-project-action + with: + docker: true + stormDir: "" + command: ${{ inputs.starterProjectCommand }} diff --git a/.github/workflows/test-deploy.yml b/.github/workflows/test-deploy.yml new file mode 100644 index 0000000000..3765b96681 --- /dev/null +++ b/.github/workflows/test-deploy.yml @@ -0,0 +1,108 @@ +name: Deploy + +on: + workflow_call: + inputs: + carl_tag: + description: "Carl git tag to use" + type: string + default: "master" + nr_jobs: + description: "Number of parallel build jobs" + type: string + default: "4" + buildType: + description: "Build type name (Debug or Release)" + type: string + required: true + dockerTag: + description: "Docker image tag to use (e.g. ci-debug, ci)" + type: string + required: true + baseImg: + description: "Base image name (e.g. storm-dependencies:latest)" + type: string + default: "storm-dependencies:latest" + Developer: + description: "Enable developer mode" + type: boolean + default: false + cmakeArgs: + description: "Extra CMake arguments" + type: string + default: "" + secrets: + STORM_CI_DOCKER_USERNAME: + required: false + STORM_CI_DOCKER_TOKEN: + required: false + +jobs: + deploy: + name: Test and Deploy (${{ inputs.buildType }}) + runs-on: ubuntu-latest + env: + NR_JOBS: ${{ inputs.nr_jobs }} + steps: + - name: Git clone + uses: actions/checkout@v7 + - name: Git describe + id: ghd + uses: proudust/gh-describe@v3 + - name: Set static Storm version + run: echo "set(STORM_VERSION_COMMITS_AHEAD ${{ steps.ghd.outputs.distance }})" >> version.cmake + - name: Build storm from Dockerfile + run: | + docker build -t movesrwth/storm:${{ inputs.dockerTag }} . \ + --build-arg BASE_IMAGE=movesrwth/${{ inputs.baseImg }} \ + --build-arg build_type="${{ inputs.buildType }}" \ + --build-arg carl_tag="${{ inputs.carl_tag }}" \ + --build-arg developer="${{ inputs.Developer && 'ON' || 'OFF' }}" \ + --build-arg cmake_args="${{ inputs.cmakeArgs }}" \ + --build-arg no_threads=${NR_JOBS} + # Omitting arguments disable_*, cln_exact, cln_ratfunc, all_sanitizers + - name: Run Docker + run: docker run -d -it --name ci movesrwth/storm:${{ inputs.dockerTag }} + - name: Check compile flags + uses: ./.github/actions/check-compile-flags-action + with: + buildType: ${{ inputs.buildType }} + docker: true + - name: Run tests + run: docker exec ci bash -c "cd /opt/storm/build; ctest test --output-on-failure" + - name: Build starter-project + uses: ./.github/actions/starter-project-action + with: + docker: true + stormDir: "/opt/storm/build" + command: "/opt/storm/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" + - name: Install storm + run: docker exec ci bash -c "cd /opt/storm/build; make install" + - name: Temporarily move build dir + run: | + docker exec ci bash -c "mv /opt/storm/build /opt/storm/build-backup" + - name: Run installed storm + run: | + docker exec ci bash -c "/usr/local/bin/storm --version" + - name: Build starter-project on installed Storm + uses: ./.github/actions/starter-project-action + with: + docker: true + stormDir: "" + command: "/opt/storm/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" + - name: Restore build dir + run: | + docker exec ci bash -c "mv /opt/storm/build-backup /opt/storm/build" + - name: Login into docker + # Only login if using master on original repo (and not for pull requests or forks) + if: github.repository_owner == 'stormchecker' && github.ref == 'refs/heads/master' + uses: docker/login-action@v4 + with: + username: ${{ secrets.STORM_CI_DOCKER_USERNAME }} + password: ${{ secrets.STORM_CI_DOCKER_TOKEN }} + - name: Deploy storm + # Only deploy if using master on original repo (and not for pull requests or forks) + if: github.repository_owner == 'stormchecker' && github.ref == 'refs/heads/master' + run: | + docker commit ci movesrwth/storm:${{ inputs.dockerTag }} + docker push movesrwth/storm:${{ inputs.dockerTag }} diff --git a/.github/workflows/test-linux.yml b/.github/workflows/test-linux.yml new file mode 100644 index 0000000000..031c99e7ca --- /dev/null +++ b/.github/workflows/test-linux.yml @@ -0,0 +1,112 @@ +name: Linux Tests + +on: + workflow_call: + inputs: + nr_jobs: + description: "Number of parallel build jobs" + type: string + default: "4" + distro: + description: "distro to use as base image for the docker image" + type: string + required: true + buildType: + description: "build type to use for the docker image" + type: string + required: true + runner: + description: "runner to use for the job" + type: string + default: "ubuntu-latest" + restore_cache: + description: "Restore ccache from cache" + type: boolean + default: false + save_cache: + description: "Save ccache to cache" + type: boolean + default: false + install: + description: "Run post-build steps: starter project, install, run installed storm" + type: boolean + default: true + +jobs: + linuxTests: + name: Linux Tests (${{ inputs.distro }}, ${{ inputs.buildType }}) on ${{ inputs.runner }} + runs-on: ${{ inputs.runner }} + env: + NR_JOBS: ${{ inputs.nr_jobs }} + steps: + - name: Git clone + uses: actions/checkout@v7 + - name: Restore ccache (Docker) + id: ccache-restore + if: inputs.restore_cache + uses: actions/cache/restore@v4 + with: + path: .ci-ccache + key: buildtest-ccache-linux-${{ inputs.distro }}-${{ inputs.buildType }}-${{ inputs.runner }}-${{ github.run_id }} + restore-keys: | + buildtest-ccache-linux-${{ inputs.distro }}-${{ inputs.buildType }}-${{ inputs.runner }}- + buildtest-ccache-linux- + - name: Build storm from Dockerfile + run: | + mkdir -p .ci-ccache + docker build -t movesrwth/storm:ci . \ + --build-arg BASE_IMAGE=movesrwth/storm-basesystem:${{ inputs.distro }} \ + --build-arg build_type="${{ inputs.buildType }}" \ + --build-arg no_threads=${NR_JOBS} \ + --build-arg cmake_args="-DSTORM_WARNING_AS_ERROR=ON -DSTORM_COMPILE_WITH_PCH=OFF" + # Omitting arguments developer, disable_*, cln_exact, cln_ratfunc, all_sanitizers + - name: Export ccache from Docker image + if: inputs.save_cache && always() && steps.ccache-restore.outputs.cache-hit != 'true' + run: | + rm -rf .ci-ccache + mkdir -p .ci-ccache + docker create --name ccache-extract movesrwth/storm:ci + docker cp ccache-extract:/root/.ccache/. .ci-ccache/ || true + docker rm ccache-extract + - name: Save ccache (Docker) + if: inputs.save_cache && always() && steps.ccache-restore.outputs.cache-hit != 'true' + uses: actions/cache/save@v4 + with: + path: .ci-ccache + key: buildtest-ccache-linux-${{ inputs.distro }}-${{ inputs.buildType }}-${{ inputs.runner }}-${{ github.run_id }} + - name: Run Docker + run: docker run -d -it --name ci movesrwth/storm:ci + - name: Run storm + run: docker exec ci bash -c "/opt/storm/build/bin/storm --version" + - name: Check compile flags + uses: ./.github/actions/check-compile-flags-action + with: + buildType: ${{ inputs.buildType }} + docker: true + - name: Run tests + run: docker exec ci bash -c "cd /opt/storm/build; ctest test --output-on-failure" + - name: Build starter-project + if: inputs.install + uses: ./.github/actions/starter-project-action + with: + docker: true + stormDir: "/opt/storm/build" + command: "/opt/storm/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" + - name: Install storm + if: inputs.install + run: docker exec ci bash -c "cd /opt/storm/build; make install" + - name: Remove build dir + if: inputs.install + run: | + docker exec ci bash -c "rm -rf /opt/storm/build" + - name: Run installed storm + if: inputs.install + run: | + docker exec ci bash -c "/usr/local/bin/storm --version" + - name: Build starter-project on installed Storm + if: inputs.install + uses: ./.github/actions/starter-project-action + with: + docker: true + stormDir: "" + command: "/opt/storm/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" diff --git a/.github/workflows/test-mac.yml b/.github/workflows/test-mac.yml new file mode 100644 index 0000000000..b67add236f --- /dev/null +++ b/.github/workflows/test-mac.yml @@ -0,0 +1,139 @@ +name: macOS Tests + +on: + workflow_call: + inputs: + nr_jobs: + description: "Number of parallel build jobs" + type: string + default: "4" + name: + description: "Display name (e.g. Xcode 15.4, ARM)" + type: string + required: true + distro: + description: "macOS runner image (e.g. macos-14, macos-15)" + type: string + required: true + xcode: + description: "Xcode version (e.g. 15.4, latest-stable)" + type: string + required: true + buildType: + description: "CMake build type (Debug or Release)" + type: string + required: true + restore_cache: + description: "Restore ccache and Homebrew cache" + type: boolean + default: false + save_cache: + description: "Save ccache to cache" + type: boolean + default: false + install: + description: "Run post-build steps: starter project, install, run installed storm" + type: boolean + default: true + +jobs: + macTests: + name: macOS Tests (${{ inputs.name }}, ${{ inputs.buildType }}) + runs-on: ${{ inputs.distro }} + env: + CCACHE_DIR: /Users/runner/.ccache + NR_JOBS: ${{ inputs.nr_jobs }} + steps: + - uses: maxim-lobanov/setup-xcode@v1 + with: + xcode-version: ${{ inputs.xcode }} + - name: Git clone + uses: actions/checkout@v7 + - name: Cache Homebrew downloads + if: inputs.restore_cache + uses: actions/cache@v4 + with: + path: ~/Library/Caches/Homebrew + key: buildtest-brew-${{ inputs.distro }}-${{ hashFiles('.github/workflows/buildtest.yml') }} + restore-keys: | + buildtest-brew-${{ inputs.distro }}- + - name: Ensure ccache directory exists (macOS) + if: inputs.restore_cache + run: mkdir -p /Users/runner/.ccache + - name: Restore ccache (macOS) + id: ccache-restore-macos + if: inputs.restore_cache + uses: actions/cache/restore@v4 + with: + path: /Users/runner/.ccache + key: buildtest-ccache-macos-${{ inputs.distro }}-${{ inputs.buildType }}-${{ github.run_id }} + restore-keys: | + buildtest-ccache-macos-${{ inputs.distro }}-${{ inputs.buildType }}- + buildtest-ccache-macos-${{ inputs.distro }}- + buildtest-ccache-macos- + - name: Install dependencies + # cmake and gmp are already installed + run: | + brew update + brew install automake boost ccache cln ginac glpk hwloc libarchive xerces-c z3 + - name: Prepare ccache + if: inputs.restore_cache + run: | + ccache --max-size=2G + ccache --zero-stats + ccache --show-stats --verbose + - name: Configure storm + run: | + mkdir build + cd build + cmake .. -DCMAKE_BUILD_TYPE="${{ inputs.buildType }}" -DSTORM_WARNING_AS_ERROR=ON -DSTORM_COMPILE_WITH_PCH=OFF + - name: Build storm + working-directory: ./build + run: | + make -j ${NR_JOBS} + - name: Print ccache stats + if: inputs.restore_cache + run: ccache --show-stats --verbose + - name: Save ccache (macOS) + if: inputs.save_cache && always() && steps.ccache-restore-macos.outputs.cache-hit != 'true' + uses: actions/cache/save@v4 + with: + path: /Users/runner/.ccache + key: buildtest-ccache-macos-${{ inputs.distro }}-${{ inputs.buildType }}-${{ github.run_id }} + - name: Run storm (build tree) + working-directory: ./build + run: ./bin/storm + - name: Check compile flags + uses: ./.github/actions/check-compile-flags-action + with: + buildType: ${{ inputs.buildType }} + docker: false + - name: Run tests + working-directory: ./build + run: ctest test --output-on-failure + - name: Build starter-project + if: inputs.install + uses: ./.github/actions/starter-project-action + with: + docker: false + stormDir: "${GITHUB_WORKSPACE}/build" + command: "${GITHUB_WORKSPACE}/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" + - name: Install storm + if: inputs.install + working-directory: ./build + run: sudo make install + - name: Remove build dir + if: inputs.install + run: | + rm -rf ${GITHUB_WORKSPACE}/build + - name: Run installed storm + if: inputs.install + run: | + /usr/local/bin/storm --version + - name: Build starter-project on installed Storm + if: inputs.install + uses: ./.github/actions/starter-project-action + with: + docker: false + stormDir: "" + command: "${GITHUB_WORKSPACE}/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" diff --git a/CMakeLists.txt b/CMakeLists.txt index 3ff546a1d7..9ce3adc9c0 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -48,6 +48,8 @@ option(STORM_FORCE_POPCNT "Sets whether the popcnt instruction is forced to be u MARK_AS_ADVANCED(STORM_FORCE_POPCNT) option(STORM_COMPILE_WITH_CCACHE "Compile using CCache [if found]" ON) mark_as_advanced(STORM_COMPILE_WITH_CCACHE) +option(STORM_COMPILE_WITH_PCH "Enable pre-compiled headers" ON) +mark_as_advanced(STORM_COMPILE_WITH_PCH) option(STORM_LOG_DISABLE_DEBUG "Disable log and trace message support" OFF) option(STORM_COMPILE_WITH_ADDRESS_SANITIZER "Sets whether to compile with AddressSanitizer enabled" OFF) option(STORM_COMPILE_WITH_ALL_SANITIZERS "Sets whether to compile with all sanitizers enabled" OFF) @@ -154,6 +156,8 @@ if (STORM_DEVELOPER) set(STORM_DEBUG_SPOT ON) set(STORM_DEBUG_SYLVAN ON) set(STORM_WARNING_AS_ERROR ON) + # Turn off PCH for faster ccache usage on warm caches. PCH compiled files cannot be properly cached currently. + set(STORM_COMPILE_WITH_PCH OFF) else() set(STORM_LOG_DISABLE_DEBUG ON) if (NOT CMAKE_BUILD_TYPE) @@ -164,13 +168,25 @@ set(CMAKE_COMPILE_WARNING_AS_ERROR ${STORM_WARNING_AS_ERROR}) message(STATUS "Storm - Building ${CMAKE_BUILD_TYPE} version.") +# PCH compiled files cannot be properly cached currently. Thus disabling it is recommended when doing many warm ccache builds. +if(NOT STORM_COMPILE_WITH_PCH) + set(CMAKE_DISABLE_PRECOMPILE_HEADERS ON) + message(STATUS "Storm - Disabling precompiled headers because of ccache compatibility.") +endif() + if(STORM_COMPILE_WITH_CCACHE) find_program(CCACHE_FOUND ccache) mark_as_advanced(CCACHE_FOUND) if(CCACHE_FOUND) message(STATUS "Storm - Using ccache") + # Relax ccache the caching keys, pch_defines tries to ignore precompiled headers (but often does not succeed in our case), + # the time options are commonly used and ignore time macros when calculating the cache key, improving cache hit rates. + set(ENV{CCACHE_SLOPPINESS} "pch_defines,time_macros,include_file_mtime,include_file_ctime") set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE ccache) - set_property(GLOBAL PROPERTY RULE_LAUNCH_LINK ccache) + + if(STORM_COMPILE_WITH_PCH) + message(STATUS "STORM - PCH is enabled which will lead to significantly lower ccache hit rates. Consider disabling PCH if you plan to rebuild Storm multiple times.") + endif() else() message(STATUS "Storm - Could not find ccache.") endif() @@ -314,6 +330,7 @@ SET(STORM_PRECOMPILED_HEADERS "" "" "" "" "" "" "" "" "" "" "" "" "" "" "" "") + ############################################################# ## ## Compiler tests during config diff --git a/Dockerfile b/Dockerfile index b9f9f81d9d..087414b8e9 100644 --- a/Dockerfile +++ b/Dockerfile @@ -41,16 +41,34 @@ ARG all_sanitizers="OFF" # Specify additional CMake arguments for Storm ARG cmake_args="" +ARG ccache_size="3G" # Build Storm ############# +RUN if ! command -v ccache >/dev/null 2>&1; then \ + if command -v apt-get >/dev/null 2>&1; then \ + apt-get update && apt-get install -y --no-install-recommends ccache && rm -rf /var/lib/apt/lists/*; \ + elif command -v apk >/dev/null 2>&1; then \ + apk add --no-cache ccache; \ + elif command -v pacman >/dev/null 2>&1; then \ + pacman -S --noconfirm ccache; \ + else \ + echo "No supported package manager found for ccache installation"; \ + fi; \ + fi + +ENV CCACHE_DIR=/root/.ccache RUN mkdir /opt/storm WORKDIR /opt/storm # Copy the content of the current local Storm repository into the Docker image COPY . . +# Seed ccache from the workflow cache directory if available. +RUN mkdir -p "$CCACHE_DIR" && \ + if [ -d "/opt/storm/.ci-ccache" ]; then cp -a /opt/storm/.ci-ccache/. "$CCACHE_DIR"/; fi + # Switch to build directory RUN mkdir -p /opt/storm/build WORKDIR /opt/storm/build @@ -78,6 +96,6 @@ RUN cmake -DCMAKE_BUILD_TYPE=$build_type \ # Build Storm # (This can be adapted to only build 'storm' or 'binaries' depending on custom needs) -RUN make -j $no_threads +RUN ccache --max-size=$ccache_size && ccache --zero-stats && make -j $no_threads && ccache --show-stats --verbose WORKDIR /opt/storm diff --git a/resources/3rdparty/include_spot.cmake b/resources/3rdparty/include_spot.cmake index 0ad1989a29..c6f2c85048 100644 --- a/resources/3rdparty/include_spot.cmake +++ b/resources/3rdparty/include_spot.cmake @@ -60,10 +60,13 @@ if(NOT STORM_DISABLE_SPOT) set(SPOT_SHIPPED_VERSION 2.15.1) set(STORM_SPOT_FLAGS "--disable-python;--enable-shared;--disable-static") if (NOT STORM_DEBUG_SPOT) - set(STORM_SPOT_FLAGS "${STORM_SPOT_FLAGS};--disable-devel;--disable-debug;--enable-optimizations") + set(STORM_SPOT_FLAGS "${STORM_SPOT_FLAGS};--disable-devel;--disable-debug;--enable-optimizations") else() - message(WARNING "Storm - Building Spot in DEBUG mode.") - set(STORM_SPOT_FLAGS "${STORM_SPOT_FLAGS};--enable-devel;--enable-debug;--disable-optimizations") + message(WARNING "Storm - Building Spot in DEBUG mode.") + set(STORM_SPOT_FLAGS "${STORM_SPOT_FLAGS};--disable-devel;--enable-debug;--disable-optimizations") + endif() + if (CCACHE_FOUND) + set(STORM_SPOT_FLAGS "${STORM_SPOT_FLAGS};CC=ccache\\ ${CMAKE_C_COMPILER};CXX=ccache\\ ${CMAKE_CXX_COMPILER}") endif() ExternalProject_Add(Spot URL https://www.lre.epita.fr/dload/spot/spot-${SPOT_SHIPPED_VERSION}.tar.gz https://www.lrde.epita.fr/dload/spot/spot-${SPOT_SHIPPED_VERSION}.tar.gz diff --git a/resources/scripts/benchmark-pch-ccache.sh b/resources/scripts/benchmark-pch-ccache.sh new file mode 100755 index 0000000000..8ea6e487d1 --- /dev/null +++ b/resources/scripts/benchmark-pch-ccache.sh @@ -0,0 +1,295 @@ +#!/usr/bin/env bash +set -euo pipefail + +# Benchmark Storm compile time across: +# - PCH enabled/disabled +# - ccache cold/warm +# +# The script uses ccache through CMake compiler launchers and controls PCH via +# CMAKE_DISABLE_PRECOMPILE_HEADERS, so all four combinations are measurable. + +SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +SOURCE_DIR="$(cd "${SCRIPT_DIR}/../.." && pwd)" +BUILD_ROOT="${SOURCE_DIR}/build-bench-pch-ccache" +CCACHE_ROOT="" +BUILD_TYPE="Release" +TARGET="storm" +JOBS="$(command -v nproc >/dev/null 2>&1 && nproc || echo 4)" +GENERATOR="" +EXTRA_CMAKE_ARGS=() +ENABLE_TRACE=0 +NINJATRACING_BIN="" +NINJATRACING_URL="https://raw.githubusercontent.com/nico/ninjatracing/master/ninjatracing" + +usage() { + cat <<'EOF' +Usage: benchmark-pch-ccache.sh [options] + +Options: + --source-dir Storm source directory (default: repo root) + --build-root Directory for benchmark build trees/results + --ccache-root Directory for benchmark ccache data (default: /ccache) + --build-type CMake build type (default: Release) + --target Build target (default: storm) + --jobs Parallel build jobs (default: nproc or 4) + --generator CMake generator (e.g. Ninja) + --cmake-arg Extra CMake argument (can be repeated) + --trace Generate Chrome trace files via ninjatracing + --ninjatracing Path to local ninjatracing script/binary + --help Show this help + +Output: + - Summary table in stdout + - CSV at /results.csv + - Per-run ccache stats in /results/ + - Optional traces at /results/trace--.json +EOF +} + +require_cmd() { + if ! command -v "$1" >/dev/null 2>&1; then + echo "Error: required command '$1' not found" >&2 + exit 1 + fi +} + +extract_stat() { + local label="$1" + local file="$2" + awk -F: -v key="$label" ' + $1 ~ key { + gsub(/^[[:space:]]+|[[:space:]]+$/, "", $2) + gsub(/[[:space:]]/, "", $2) + print $2 + found=1 + exit + } + END { if (!found) print 0 } + ' "$file" +} + +run_case() { + local pch_mode="$1" # on|off + local cache_state="$2" # cold|warm + local namespace="storm-bench-pch-${pch_mode}" + local ccache_dir="${CCACHE_ROOT}/${namespace}" + local enable_pch="ON" + + if [[ "$pch_mode" == "off" ]]; then + enable_pch="OFF" + fi + + local build_dir="${BUILD_ROOT}/build-${pch_mode}" + local result_dir="${BUILD_ROOT}/results" + mkdir -p "$result_dir" + + export CCACHE_DIR="$ccache_dir" + export CCACHE_NAMESPACE="$namespace" + export CCACHE_BASEDIR="$SOURCE_DIR" + export CCACHE_NOHASHDIR="1" + + if [[ "$cache_state" == "cold" ]]; then + rm -rf "$ccache_dir" + rm -rf "$build_dir" + fi + mkdir -p "$ccache_dir" + ccache --zero-stats >/dev/null + + local cmake_cmd=(cmake -S "$SOURCE_DIR" -B "$build_dir" + -DSTORM_COMPILE_WITH_PCH="$enable_pch" + -DCMAKE_BUILD_TYPE="$BUILD_TYPE") + + if [[ -n "$GENERATOR" ]]; then + cmake_cmd+=(-G "$GENERATOR") + fi + + if [[ ${#EXTRA_CMAKE_ARGS[@]} -gt 0 ]]; then + cmake_cmd+=("${EXTRA_CMAKE_ARGS[@]}") + fi + + if [[ "$cache_state" == "cold" || ! -d "$build_dir" ]]; then + echo "[benchmark] Configure: pch=${pch_mode}, cache=${cache_state}" + "${cmake_cmd[@]}" >/dev/null + fi + + if [[ "$cache_state" == "warm" ]]; then + # Rebuild in the same build directory to keep paths stable for ccache. + cmake --build "$build_dir" --target clean -j "$JOBS" >/dev/null || true + fi + + local time_file="${result_dir}/time-${pch_mode}-${cache_state}.txt" + echo "[benchmark] Build: pch=${pch_mode}, cache=${cache_state}" + /usr/bin/time -f "%e" -o "$time_file" \ + cmake --build "$build_dir" --target "$TARGET" -j "$JOBS" >/dev/null + + local stats_file="${result_dir}/ccache-${pch_mode}-${cache_state}.txt" + ccache --show-stats --verbose >"$stats_file" + + if [[ "$ENABLE_TRACE" == "1" ]]; then + local ninja_log="${build_dir}/.ninja_log" + local trace_file="${result_dir}/trace-${pch_mode}-${cache_state}.json" + if [[ ! -f "$ninja_log" ]]; then + echo "Error: ninja log not found at $ninja_log" >&2 + exit 1 + fi + python3 "$NINJATRACING_BIN" "$ninja_log" >"$trace_file" + fi + + local elapsed + elapsed="$(cat "$time_file")" + + local cacheable hits misses uncacheable + cacheable="$(extract_stat "Cacheable calls" "$stats_file")" + hits="$(extract_stat "Hits" "$stats_file")" + misses="$(extract_stat "Misses" "$stats_file")" + uncacheable="$(extract_stat "Uncacheable calls" "$stats_file")" + + local hit_rate="0.00" + if [[ "$cacheable" != "0" ]]; then + hit_rate="$(awk -v h="$hits" -v c="$cacheable" 'BEGIN { printf "%.2f", (100.0*h)/c }')" + fi + + printf "%s,%s,%s,%s,%s,%s,%s\n" \ + "$pch_mode" "$cache_state" "$elapsed" "$cacheable" "$hits" "$misses" "$uncacheable" \ + >>"${BUILD_ROOT}/results.csv" + + printf "%-8s %-6s %10s %12s %10s %10s %12s %9s\n" \ + "$pch_mode" "$cache_state" "$elapsed" "$cacheable" "$hits" "$misses" "$uncacheable" "${hit_rate}%" +} + +while [[ $# -gt 0 ]]; do + case "$1" in + --source-dir) + SOURCE_DIR="$2" + shift 2 + ;; + --build-root) + BUILD_ROOT="$2" + shift 2 + ;; + --ccache-root) + CCACHE_ROOT="$2" + shift 2 + ;; + --build-type) + BUILD_TYPE="$2" + shift 2 + ;; + --target) + TARGET="$2" + shift 2 + ;; + --jobs) + JOBS="$2" + shift 2 + ;; + --generator) + GENERATOR="$2" + shift 2 + ;; + --cmake-arg) + EXTRA_CMAKE_ARGS+=("$2") + shift 2 + ;; + --trace) + ENABLE_TRACE=1 + shift + ;; + --ninjatracing) + NINJATRACING_BIN="$2" + shift 2 + ;; + --help) + usage + exit 0 + ;; + *) + echo "Unknown argument: $1" >&2 + usage + exit 1 + ;; + esac +done + +require_cmd cmake +require_cmd ccache +require_cmd /usr/bin/time + +if [[ "$ENABLE_TRACE" == "1" ]]; then + require_cmd python3 + if [[ -z "$GENERATOR" ]]; then + GENERATOR="Ninja" + fi + if [[ "$GENERATOR" != "Ninja" ]]; then + echo "Error: --trace requires --generator Ninja (or no generator, which defaults to Ninja)." >&2 + exit 1 + fi + require_cmd ninja +fi + +if [[ -z "$CCACHE_ROOT" ]]; then + CCACHE_ROOT="${BUILD_ROOT}/ccache" +fi + +mkdir -p "$BUILD_ROOT" +mkdir -p "$CCACHE_ROOT" +: >"${BUILD_ROOT}/results.csv" +echo "pch,cache_state,build_seconds,cacheable_calls,hits,misses,uncacheable_calls" >>"${BUILD_ROOT}/results.csv" + +if [[ "$ENABLE_TRACE" == "1" ]]; then + if [[ -z "$NINJATRACING_BIN" ]]; then + NINJATRACING_BIN="${BUILD_ROOT}/tools/ninjatracing" + mkdir -p "${BUILD_ROOT}/tools" + if [[ ! -f "$NINJATRACING_BIN" ]]; then + if command -v curl >/dev/null 2>&1; then + curl -fsSL "$NINJATRACING_URL" -o "$NINJATRACING_BIN" + elif command -v wget >/dev/null 2>&1; then + wget -qO "$NINJATRACING_BIN" "$NINJATRACING_URL" + else + echo "Error: neither curl nor wget found; provide --ninjatracing ." >&2 + exit 1 + fi + chmod +x "$NINJATRACING_BIN" + fi + fi +fi + +echo +echo "Benchmark settings" +echo " source-dir: $SOURCE_DIR" +echo " build-root: $BUILD_ROOT" +echo " ccache-root: $CCACHE_ROOT" +echo " build-type: $BUILD_TYPE" +echo " target: $TARGET" +echo " jobs: $JOBS" +if [[ -n "$GENERATOR" ]]; then + echo " generator: $GENERATOR" +fi +if [[ "$ENABLE_TRACE" == "1" ]]; then + echo " trace: enabled" + echo " ninjatrace: $NINJATRACING_BIN" +else + echo " trace: disabled" +fi +if [[ ${#EXTRA_CMAKE_ARGS[@]} -gt 0 ]]; then + echo " extra args: ${EXTRA_CMAKE_ARGS[*]}" +fi + +echo +echo "Results" +printf "%-8s %-6s %10s %12s %10s %10s %12s %9s\n" \ + "pch" "cache" "seconds" "cacheable" "hits" "misses" "uncacheable" "hit-rate" +printf "%-8s %-6s %10s %12s %10s %10s %12s %9s\n" \ + "--------" "------" "----------" "------------" "----------" "----------" "------------" "---------" + +run_case off cold +run_case off warm +run_case on cold +run_case on warm + +echo +echo "CSV written to: ${BUILD_ROOT}/results.csv" +echo "Raw stats in: ${BUILD_ROOT}/results" +if [[ "$ENABLE_TRACE" == "1" ]]; then + echo "Traces in: ${BUILD_ROOT}/results" +fi diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 02123bbe29..37f91c1a82 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -34,6 +34,13 @@ if (STORM_COMPILE_WITH_ADDRESS_SANITIZER) add_link_options(-fsanitize=address) endif() +# Allow for disabling pre compiled headers +function(storm_target_precompile_headers target) + if(NOT CMAKE_DISABLE_PRECOMPILE_HEADERS) + target_precompile_headers(${target} ${ARGN}) + endif() +endfunction() + # In release mode, we turn on even more optimizations if we do not have to provide a portable binary. if (NOT STORM_PORTABLE AND (NOT APPLE_SILICON OR (STORM_COMPILER_CLANG AND CMAKE_CXX_COMPILER_VERSION VERSION_GREATER_EQUAL 15.0))) add_compile_options($<$:-march=native>) diff --git a/src/storm-cli-utilities/AutomaticSettings.h b/src/storm-cli-utilities/AutomaticSettings.h index d3a3bc69b2..ba500c05ad 100644 --- a/src/storm-cli-utilities/AutomaticSettings.h +++ b/src/storm-cli-utilities/AutomaticSettings.h @@ -1,5 +1,7 @@ #pragma once +#include + #include "storm/utility/Engine.h" namespace storm { diff --git a/src/storm-cli-utilities/CMakeLists.txt b/src/storm-cli-utilities/CMakeLists.txt index eba3308270..1af0660f31 100644 --- a/src/storm-cli-utilities/CMakeLists.txt +++ b/src/storm-cli-utilities/CMakeLists.txt @@ -9,7 +9,7 @@ target_sources(storm-cli-utilities ${STORM_CLI_UTIL_SOURCES} PUBLIC FILE_SET fs_storm_cli_utilities_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_CLI_UTIL_HEADERS}) -target_precompile_headers(storm-cli-utilities REUSE_FROM storm) +storm_target_precompile_headers(storm-cli-utilities REUSE_FROM storm) set_target_properties(storm-cli-utilities PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) target_link_libraries(storm-cli-utilities PUBLIC storm storm-counterexamples storm-gamebased-ar storm-parsers storm-version-info) set_target_properties(storm-cli-utilities PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux. diff --git a/src/storm-cli/CMakeLists.txt b/src/storm-cli/CMakeLists.txt index d5b15d2956..10fc6080d5 100644 --- a/src/storm-cli/CMakeLists.txt +++ b/src/storm-cli/CMakeLists.txt @@ -3,7 +3,7 @@ add_executable(storm-cli ${PROJECT_SOURCE_DIR}/src/storm-cli/storm-cli.cpp) target_link_libraries(storm-cli storm storm-cli-utilities) set_target_properties(storm-cli PROPERTIES OUTPUT_NAME "storm") set_target_properties(storm-cli PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) -target_precompile_headers(storm-cli PRIVATE ${STORM_PRECOMPILED_HEADERS}) +storm_target_precompile_headers(storm-cli PRIVATE ${STORM_PRECOMPILED_HEADERS}) add_dependencies(binaries storm-cli) diff --git a/src/storm-conv-cli/CMakeLists.txt b/src/storm-conv-cli/CMakeLists.txt index dc7056087b..b79633db98 100644 --- a/src/storm-conv-cli/CMakeLists.txt +++ b/src/storm-conv-cli/CMakeLists.txt @@ -3,7 +3,7 @@ add_executable(storm-conv-cli ${PROJECT_SOURCE_DIR}/src/storm-conv-cli/storm-con target_link_libraries(storm-conv-cli storm-conv storm-cli-utilities) set_target_properties(storm-conv-cli PROPERTIES OUTPUT_NAME "storm-conv") set_target_properties(storm-conv-cli PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) -target_precompile_headers(storm-conv-cli REUSE_FROM storm-cli) +storm_target_precompile_headers(storm-conv-cli REUSE_FROM storm-cli) add_dependencies(binaries storm-conv-cli) diff --git a/src/storm-conv/CMakeLists.txt b/src/storm-conv/CMakeLists.txt index 05d5a98901..89d7e234f3 100644 --- a/src/storm-conv/CMakeLists.txt +++ b/src/storm-conv/CMakeLists.txt @@ -8,7 +8,7 @@ target_sources(storm-conv ${STORM_CONV_SOURCES} PUBLIC FILE_SET fs_storm_conv_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_CONV_HEADERS}) -target_precompile_headers(storm-conv REUSE_FROM storm) +storm_target_precompile_headers(storm-conv REUSE_FROM storm) set_target_properties(storm-conv PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) target_link_libraries(storm-conv PUBLIC storm) set_target_properties(storm-conv PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux. diff --git a/src/storm-counterexamples/CMakeLists.txt b/src/storm-counterexamples/CMakeLists.txt index 4b787e33ca..7448579d0f 100644 --- a/src/storm-counterexamples/CMakeLists.txt +++ b/src/storm-counterexamples/CMakeLists.txt @@ -7,7 +7,7 @@ target_sources(storm-counterexamples ${STORM_CEX_SOURCES} PUBLIC FILE_SET fs_storm_cex_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_CEX_HEADERS}) -target_precompile_headers(storm-counterexamples REUSE_FROM storm) +storm_target_precompile_headers(storm-counterexamples REUSE_FROM storm) set_target_properties(storm-counterexamples PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) target_link_libraries(storm-counterexamples PUBLIC storm) set_target_properties(storm-counterexamples PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux. diff --git a/src/storm-dft-cli/CMakeLists.txt b/src/storm-dft-cli/CMakeLists.txt index b68602e7e9..d44d0e14a4 100644 --- a/src/storm-dft-cli/CMakeLists.txt +++ b/src/storm-dft-cli/CMakeLists.txt @@ -3,7 +3,7 @@ add_executable(storm-dft-cli ${PROJECT_SOURCE_DIR}/src/storm-dft-cli/storm-dft.c target_link_libraries(storm-dft-cli storm-dft storm-cli-utilities) set_target_properties(storm-dft-cli PROPERTIES OUTPUT_NAME "storm-dft") set_target_properties(storm-dft-cli PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) -target_precompile_headers(storm-dft-cli REUSE_FROM storm-cli) +storm_target_precompile_headers(storm-dft-cli REUSE_FROM storm-cli) add_dependencies(binaries storm-dft-cli) diff --git a/src/storm-dft/CMakeLists.txt b/src/storm-dft/CMakeLists.txt index b3e6ce4b3c..1391f7d509 100644 --- a/src/storm-dft/CMakeLists.txt +++ b/src/storm-dft/CMakeLists.txt @@ -8,7 +8,7 @@ target_sources(storm-dft ${STORM_DFT_SOURCES} PUBLIC FILE_SET fs_storm_dft_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_DFT_HEADERS}) -target_precompile_headers(storm-dft REUSE_FROM storm) +storm_target_precompile_headers(storm-dft REUSE_FROM storm) set_target_properties(storm-dft PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) target_link_libraries(storm-dft PUBLIC storm storm-gspn storm-conv storm-parsers storm-pars ${STORM_DFT_LINK_LIBRARIES}) set_target_properties(storm-dft PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux. diff --git a/src/storm-gamebased-ar/CMakeLists.txt b/src/storm-gamebased-ar/CMakeLists.txt index 190a22d89f..d9f1b92113 100644 --- a/src/storm-gamebased-ar/CMakeLists.txt +++ b/src/storm-gamebased-ar/CMakeLists.txt @@ -7,7 +7,7 @@ target_sources(storm-gamebased-ar ${STORM_GBAR_SOURCES} PUBLIC FILE_SET fs_storm_gbar_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_GBAR_HEADERS}) -target_precompile_headers(storm-gamebased-ar REUSE_FROM storm) +storm_target_precompile_headers(storm-gamebased-ar REUSE_FROM storm) set_target_properties(storm-gamebased-ar PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) target_link_libraries(storm-gamebased-ar PUBLIC storm) set_target_properties(storm-gamebased-ar PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux. diff --git a/src/storm-gspn-cli/CMakeLists.txt b/src/storm-gspn-cli/CMakeLists.txt index 1fca3c6b8e..dfc836dcf3 100644 --- a/src/storm-gspn-cli/CMakeLists.txt +++ b/src/storm-gspn-cli/CMakeLists.txt @@ -3,7 +3,7 @@ add_executable(storm-gspn-cli ${PROJECT_SOURCE_DIR}/src/storm-gspn-cli/storm-gsp target_link_libraries(storm-gspn-cli storm-gspn storm-cli-utilities) set_target_properties(storm-gspn-cli PROPERTIES OUTPUT_NAME "storm-gspn") set_target_properties(storm-gspn-cli PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) -target_precompile_headers(storm-gspn-cli REUSE_FROM storm-cli) +storm_target_precompile_headers(storm-gspn-cli REUSE_FROM storm-cli) add_dependencies(binaries storm-gspn-cli) diff --git a/src/storm-gspn/CMakeLists.txt b/src/storm-gspn/CMakeLists.txt index b8e5caeef0..c4d72c7d57 100644 --- a/src/storm-gspn/CMakeLists.txt +++ b/src/storm-gspn/CMakeLists.txt @@ -7,7 +7,7 @@ target_sources(storm-gspn ${STORM_GSPN_SOURCES} PUBLIC FILE_SET fs_storm_gspn_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_GSPN_HEADERS}) -target_precompile_headers(storm-gspn REUSE_FROM storm) +storm_target_precompile_headers(storm-gspn REUSE_FROM storm) set_target_properties(storm-gspn PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) target_link_libraries(storm-gspn PUBLIC storm storm-conv storm-parsers ${STORM_GSPN_LINK_LIBRARIES}) set_target_properties(storm-gspn PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux. diff --git a/src/storm-gspn/storage/gspn/Place.h b/src/storm-gspn/storage/gspn/Place.h index ec71b9d2bf..03fbc4fc66 100644 --- a/src/storm-gspn/storage/gspn/Place.h +++ b/src/storm-gspn/storage/gspn/Place.h @@ -1,6 +1,7 @@ #ifndef STORM_STORAGE_GSPN_PLACE_H_ #define STORM_STORAGE_GSPN_PLACE_H_ +#include #include #include "boost/optional.hpp" diff --git a/src/storm-gspn/storage/gspn/TransitionPartition.h b/src/storm-gspn/storage/gspn/TransitionPartition.h index 676e87c50c..70f1614a0c 100644 --- a/src/storm-gspn/storage/gspn/TransitionPartition.h +++ b/src/storm-gspn/storage/gspn/TransitionPartition.h @@ -1,4 +1,5 @@ #pragma once +#include #include namespace storm { diff --git a/src/storm-pars-cli/CMakeLists.txt b/src/storm-pars-cli/CMakeLists.txt index 5c51c5036a..edf199adaa 100644 --- a/src/storm-pars-cli/CMakeLists.txt +++ b/src/storm-pars-cli/CMakeLists.txt @@ -8,7 +8,7 @@ target_link_libraries(storm-pars-cli storm-pars storm-cli-utilities) target_include_directories(storm-pars-cli PRIVATE "${PROJECT_SOURCE_DIR}/src") set_target_properties(storm-pars-cli PROPERTIES OUTPUT_NAME "storm-pars") set_target_properties(storm-pars-cli PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) -target_precompile_headers(storm-pars-cli REUSE_FROM storm-cli) +storm_target_precompile_headers(storm-pars-cli REUSE_FROM storm-cli) add_dependencies(binaries storm-pars-cli) diff --git a/src/storm-pars/CMakeLists.txt b/src/storm-pars/CMakeLists.txt index 5ceba61162..cdff27042b 100644 --- a/src/storm-pars/CMakeLists.txt +++ b/src/storm-pars/CMakeLists.txt @@ -8,7 +8,7 @@ target_sources(storm-pars ${STORM_PARS_SOURCES} PUBLIC FILE_SET fs_storm_pars_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_PARS_HEADERS}) -target_precompile_headers(storm-pars REUSE_FROM storm) +storm_target_precompile_headers(storm-pars REUSE_FROM storm) set_target_properties(storm-pars PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) set_target_properties(storm-pars PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux. target_link_libraries(storm-pars PUBLIC storm) diff --git a/src/storm-pars/modelchecker/region/RegionSplittingStrategy.h b/src/storm-pars/modelchecker/region/RegionSplittingStrategy.h index df7698ad57..17db3bc944 100644 --- a/src/storm-pars/modelchecker/region/RegionSplittingStrategy.h +++ b/src/storm-pars/modelchecker/region/RegionSplittingStrategy.h @@ -1,5 +1,8 @@ #pragma once +#include +#include +#include #include #include "RegionSplitEstimateKind.h" diff --git a/src/storm-parsers/CMakeLists.txt b/src/storm-parsers/CMakeLists.txt index 8564131b35..e758deb683 100644 --- a/src/storm-parsers/CMakeLists.txt +++ b/src/storm-parsers/CMakeLists.txt @@ -11,7 +11,7 @@ target_sources(storm-parsers ${STORM_PARSER_SOURCES} PUBLIC FILE_SET fs_storm_parsers_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_PARSER_HEADERS}) -target_precompile_headers(storm-parsers REUSE_FROM storm) +storm_target_precompile_headers(storm-parsers REUSE_FROM storm) set_target_properties(storm-parsers PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) set_target_properties(storm-parsers PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux. target_link_libraries(storm-parsers PUBLIC storm) diff --git a/src/storm-parsers/parser/ExpressionParser.h b/src/storm-parsers/parser/ExpressionParser.h index 87887b04f8..e32a1aefc1 100644 --- a/src/storm-parsers/parser/ExpressionParser.h +++ b/src/storm-parsers/parser/ExpressionParser.h @@ -1,5 +1,6 @@ #pragma once +#include #include #include "storm-parsers/parser/SpiritErrorHandler.h" diff --git a/src/storm-parsers/parser/SparseChoiceLabelingParser.h b/src/storm-parsers/parser/SparseChoiceLabelingParser.h index c0e037e15f..8e463778ac 100644 --- a/src/storm-parsers/parser/SparseChoiceLabelingParser.h +++ b/src/storm-parsers/parser/SparseChoiceLabelingParser.h @@ -1,6 +1,7 @@ #ifndef STORM_PARSER_SPARSECHOICELABELINGPARSER_H_ #define STORM_PARSER_SPARSECHOICELABELINGPARSER_H_ +#include #include #include diff --git a/src/storm-parsers/parser/SpiritParserDefinitions.h b/src/storm-parsers/parser/SpiritParserDefinitions.h index 20b6a5e8b2..2c38b6ce32 100644 --- a/src/storm-parsers/parser/SpiritParserDefinitions.h +++ b/src/storm-parsers/parser/SpiritParserDefinitions.h @@ -4,6 +4,12 @@ #pragma clang diagnostic push #pragma clang diagnostic ignored "-W#pragma-messages" +// Boost Spirit's utf8.hpp uses char_traits which Apple libc++ (Xcode 26+) deprecated +#if defined(__clang__) && defined(__apple_build_version__) +#pragma clang diagnostic push +#pragma clang diagnostic ignored "-Wdeprecated-declarations" +#endif + // Include boost spirit. #define BOOST_SPIRIT_USE_PHOENIX_V3 #define BOOST_SPIRIT_UNICODE @@ -28,4 +34,8 @@ namespace spirit_encoding = boost::spirit::unicode; typedef BOOST_TYPEOF(storm::spirit_encoding::space_type() | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi)) Skipper; +#if defined(__clang__) && defined(__apple_build_version__) +#pragma clang diagnostic pop +#endif + #endif /* STORM_PARSER_SPIRITPARSERDEFINITIONS_H_ */ diff --git a/src/storm-permissive/CMakeLists.txt b/src/storm-permissive/CMakeLists.txt index 1b5138ce8b..323ac622a0 100644 --- a/src/storm-permissive/CMakeLists.txt +++ b/src/storm-permissive/CMakeLists.txt @@ -8,7 +8,7 @@ target_sources(storm-permissive ${STORM_PERMISSIVE_SOURCES} PUBLIC FILE_SET fs_storm_permissive_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_PERMISSIVE_HEADERS}) -target_precompile_headers(storm-permissive REUSE_FROM storm) +storm_target_precompile_headers(storm-permissive REUSE_FROM storm) set_target_properties(storm-permissive PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) set_target_properties(storm-permissive PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux. target_link_libraries(storm-permissive PUBLIC storm) diff --git a/src/storm-permissive/analysis/PermissiveSchedulerPenalty.h b/src/storm-permissive/analysis/PermissiveSchedulerPenalty.h index 75dd20b38b..a502a42f66 100644 --- a/src/storm-permissive/analysis/PermissiveSchedulerPenalty.h +++ b/src/storm-permissive/analysis/PermissiveSchedulerPenalty.h @@ -1,5 +1,6 @@ #pragma once +#include #include #include "storm/storage/StateActionPair.h" diff --git a/src/storm-pomdp-cli/CMakeLists.txt b/src/storm-pomdp-cli/CMakeLists.txt index db8afc778e..2bd9b8780f 100644 --- a/src/storm-pomdp-cli/CMakeLists.txt +++ b/src/storm-pomdp-cli/CMakeLists.txt @@ -5,7 +5,7 @@ add_executable(storm-pomdp-cli ${PROJECT_SOURCE_DIR}/src/storm-pomdp-cli/storm-p target_link_libraries(storm-pomdp-cli storm-pomdp storm-cli-utilities) set_target_properties(storm-pomdp-cli PROPERTIES OUTPUT_NAME "storm-pomdp") target_include_directories(storm-pomdp-cli PRIVATE "${PROJECT_SOURCE_DIR}/src") -target_precompile_headers(storm-pomdp-cli REUSE_FROM storm-cli) +storm_target_precompile_headers(storm-pomdp-cli REUSE_FROM storm-cli) set_target_properties(storm-pomdp-cli PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) add_dependencies(binaries storm-pomdp-cli) diff --git a/src/storm-pomdp/CMakeLists.txt b/src/storm-pomdp/CMakeLists.txt index 019585a307..9701f93bf7 100644 --- a/src/storm-pomdp/CMakeLists.txt +++ b/src/storm-pomdp/CMakeLists.txt @@ -8,7 +8,7 @@ target_sources(storm-pomdp ${STORM_POMDP_SOURCES} PUBLIC FILE_SET fs_storm_pomdp_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_POMDP_HEADERS}) -target_precompile_headers(storm-pomdp REUSE_FROM storm) +storm_target_precompile_headers(storm-pomdp REUSE_FROM storm) set_target_properties(storm-pomdp PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) set_target_properties(storm-pomdp PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux. target_link_libraries(storm-pomdp PUBLIC storm storm-parsers storm-pars) diff --git a/src/storm/CMakeLists.txt b/src/storm/CMakeLists.txt index 24d978ca82..024d02be20 100644 --- a/src/storm/CMakeLists.txt +++ b/src/storm/CMakeLists.txt @@ -19,7 +19,7 @@ add_library(storm SHARED) target_sources(storm PRIVATE ${STORM_SOURCES}) target_sources(storm PUBLIC FILE_SET fs_storm_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_HEADERS}) target_sources(storm PUBLIC FILE_SET fs_storm_configured_headers TYPE HEADERS BASE_DIRS "${PROJECT_BINARY_DIR}/include" FILES ${STORM_BUILD_HEADERS}) -target_precompile_headers(storm PRIVATE ${STORM_PRECOMPILED_HEADERS}) +storm_target_precompile_headers(storm PRIVATE ${STORM_PRECOMPILED_HEADERS}) set_target_properties(storm PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) set_target_properties(storm PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux. set_target_properties(storm PROPERTIES BUILD_RPATH ${STORM_3RDPARTY_BINARY_DIR}/spot/lib/) @@ -29,6 +29,7 @@ target_link_libraries(storm PUBLIC ${STORM_DEP_TARGETS} ${STORM_DEP_IMP_TARGETS} list(APPEND STORM_TARGETS storm) set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) + # installation install(TARGETS storm EXPORT storm_Targets diff --git a/src/storm/adapters/JsonForward.h b/src/storm/adapters/JsonForward.h index d8d32c6a2b..ebc410e26a 100644 --- a/src/storm/adapters/JsonForward.h +++ b/src/storm/adapters/JsonForward.h @@ -1,4 +1,5 @@ #pragma once +#include #include #include #include diff --git a/src/storm/adapters/sylvan.h b/src/storm/adapters/sylvan.h index a34e880596..cc7328e8ab 100644 --- a/src/storm/adapters/sylvan.h +++ b/src/storm/adapters/sylvan.h @@ -1,5 +1,7 @@ #pragma once +#include + #include "storm-config.h" #ifdef STORM_HAVE_SYLVAN diff --git a/src/storm/environment/solver/EigenSolverEnvironment.h b/src/storm/environment/solver/EigenSolverEnvironment.h index 0504c4e151..f42384f756 100644 --- a/src/storm/environment/solver/EigenSolverEnvironment.h +++ b/src/storm/environment/solver/EigenSolverEnvironment.h @@ -1,5 +1,7 @@ #pragma once +#include + #include "storm/adapters/RationalNumberAdapter.h" #include "storm/environment/solver/SolverEnvironment.h" #include "storm/solver/SolverSelectionOptions.h" diff --git a/src/storm/environment/solver/GameSolverEnvironment.h b/src/storm/environment/solver/GameSolverEnvironment.h index 1e2e8fb0c0..dd43de15e5 100644 --- a/src/storm/environment/solver/GameSolverEnvironment.h +++ b/src/storm/environment/solver/GameSolverEnvironment.h @@ -1,5 +1,7 @@ #pragma once +#include + #include "storm/adapters/RationalNumberAdapter.h" #include "storm/environment/solver/SolverEnvironment.h" #include "storm/solver/MultiplicationStyle.h" diff --git a/src/storm/environment/solver/GmmxxSolverEnvironment.h b/src/storm/environment/solver/GmmxxSolverEnvironment.h index 232cd25ae8..e0a83e2d0c 100644 --- a/src/storm/environment/solver/GmmxxSolverEnvironment.h +++ b/src/storm/environment/solver/GmmxxSolverEnvironment.h @@ -1,5 +1,7 @@ #pragma once +#include + #include "storm/adapters/RationalNumberAdapter.h" #include "storm/environment/solver/SolverEnvironment.h" #include "storm/solver/SolverSelectionOptions.h" diff --git a/src/storm/environment/solver/LongRunAverageSolverEnvironment.h b/src/storm/environment/solver/LongRunAverageSolverEnvironment.h index 08fe4f528a..796ddbe390 100644 --- a/src/storm/environment/solver/LongRunAverageSolverEnvironment.h +++ b/src/storm/environment/solver/LongRunAverageSolverEnvironment.h @@ -1,5 +1,7 @@ #pragma once +#include + #include "storm/adapters/RationalNumberAdapter.h" #include "storm/environment/solver/SolverEnvironment.h" #include "storm/solver/SolverSelectionOptions.h" diff --git a/src/storm/environment/solver/MinMaxSolverEnvironment.h b/src/storm/environment/solver/MinMaxSolverEnvironment.h index 07548fb63d..dbdbd22afe 100644 --- a/src/storm/environment/solver/MinMaxSolverEnvironment.h +++ b/src/storm/environment/solver/MinMaxSolverEnvironment.h @@ -1,5 +1,7 @@ #pragma once +#include + #include "storm/adapters/RationalNumberAdapter.h" #include "storm/environment/solver/SolverEnvironment.h" #include "storm/solver/MultiplicationStyle.h" diff --git a/src/storm/environment/solver/NativeSolverEnvironment.h b/src/storm/environment/solver/NativeSolverEnvironment.h index 0d68e1f5ca..d1ba321f8d 100644 --- a/src/storm/environment/solver/NativeSolverEnvironment.h +++ b/src/storm/environment/solver/NativeSolverEnvironment.h @@ -1,5 +1,7 @@ #pragma once +#include + #include "storm/adapters/RationalNumberAdapter.h" #include "storm/environment/solver/SolverEnvironment.h" #include "storm/solver/MultiplicationStyle.h" diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h index 57863e1235..ee307b3d45 100644 --- a/src/storm/logic/Formula.h +++ b/src/storm/logic/Formula.h @@ -1,7 +1,9 @@ #ifndef STORM_LOGIC_FORMULA_H_ #define STORM_LOGIC_FORMULA_H_ +#include #include +#include #include #include #include diff --git a/src/storm/logic/MultiObjectiveFormula.h b/src/storm/logic/MultiObjectiveFormula.h index b579b0955d..7e4a871c30 100644 --- a/src/storm/logic/MultiObjectiveFormula.h +++ b/src/storm/logic/MultiObjectiveFormula.h @@ -1,6 +1,8 @@ #ifndef STORM_LOGIC_MULTIOBJECTIVEFORMULA_H_ #define STORM_LOGIC_MULTIOBJECTIVEFORMULA_H_ +#include + #include "storm/logic/StateFormula.h" namespace storm { diff --git a/src/storm/logic/QuantileFormula.h b/src/storm/logic/QuantileFormula.h index 8832114dfd..e5cae605b5 100644 --- a/src/storm/logic/QuantileFormula.h +++ b/src/storm/logic/QuantileFormula.h @@ -1,5 +1,7 @@ #pragma once +#include + #include "storm/logic/StateFormula.h" namespace storm { diff --git a/src/storm/modelchecker/lexicographic/spotHelper/SpotProduct.h b/src/storm/modelchecker/lexicographic/spotHelper/SpotProduct.h index d0780ce61d..6825459a33 100644 --- a/src/storm/modelchecker/lexicographic/spotHelper/SpotProduct.h +++ b/src/storm/modelchecker/lexicographic/spotHelper/SpotProduct.h @@ -1,5 +1,7 @@ #pragma once +#include + #include "storm/automata/DeterministicAutomaton.h" #include "storm/logic/ExtractMaximalStateFormulasVisitor.h" #include "storm/logic/MultiObjectiveFormula.h" diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsAchievabilityChecker.h b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsAchievabilityChecker.h index f9c21ee0cc..bbd1528556 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsAchievabilityChecker.h +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsAchievabilityChecker.h @@ -1,5 +1,6 @@ #pragma once +#include #include #include #include diff --git a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 2c9c2aeb2b..bcdb28baa5 100644 --- a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -635,6 +635,12 @@ std::unique_ptr SparseDtmcEliminationModelChecker>(result); } +// GCC 15 raises a false positive -Wfree-nonheap-object when compiling SparseDtmcEliminationModelChecker +// with GMP rational functions (STORM_USE_CLN_RF=OFF) in Release mode: the inlined std::vector destructor +// for MatrixEntry<..., RationalFunction<..., GMP>> is incorrectly flagged. Not a real memory error. +// See https://gcc.gnu.org/bugzilla/show_bug.cgi?id=108846 +#pragma GCC diagnostic push +#pragma GCC diagnostic ignored "-Wfree-nonheap-object" template std::unique_ptr SparseDtmcEliminationModelChecker::computeConditionalProbabilities( Environment const& env, CheckTask const& checkTask) { @@ -880,6 +886,7 @@ void SparseDtmcEliminationModelChecker::performPrioritizedS #endif } } +#pragma GCC diagnostic pop template void SparseDtmcEliminationModelChecker::performOrdinaryStateElimination( diff --git a/src/storm/modelchecker/results/QualitativeCheckResult.h b/src/storm/modelchecker/results/QualitativeCheckResult.h index 4d60bd340e..d7b5c6b7fb 100644 --- a/src/storm/modelchecker/results/QualitativeCheckResult.h +++ b/src/storm/modelchecker/results/QualitativeCheckResult.h @@ -1,6 +1,8 @@ #ifndef STORM_MODELCHECKER_QUALITATIVECHECKRESULT_H_ #define STORM_MODELCHECKER_QUALITATIVECHECKRESULT_H_ +#include + #include "storm/modelchecker/results/CheckResult.h" namespace storm { diff --git a/src/storm/settings/ArgumentValidators.h b/src/storm/settings/ArgumentValidators.h index dda3a9b991..d14d55fc7a 100644 --- a/src/storm/settings/ArgumentValidators.h +++ b/src/storm/settings/ArgumentValidators.h @@ -1,5 +1,6 @@ #pragma once +#include #include #include #include diff --git a/src/storm/settings/SettingsManager.h b/src/storm/settings/SettingsManager.h index a34d77fb6c..6383cbaf7b 100644 --- a/src/storm/settings/SettingsManager.h +++ b/src/storm/settings/SettingsManager.h @@ -1,6 +1,7 @@ #ifndef STORM_SETTINGS_SETTINGSMANAGER_H_ #define STORM_SETTINGS_SETTINGSMANAGER_H_ +#include #include #include #include diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.h b/src/storm/settings/modules/MinMaxEquationSolverSettings.h index d62cc6152c..5296e76b05 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.h +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.h @@ -1,5 +1,7 @@ #pragma once +#include + #include "storm-config.h" #include "storm/settings/modules/ModuleSettings.h" diff --git a/src/storm/settings/modules/ModuleSettings.h b/src/storm/settings/modules/ModuleSettings.h index 6f0ad1684f..4f0b65174c 100644 --- a/src/storm/settings/modules/ModuleSettings.h +++ b/src/storm/settings/modules/ModuleSettings.h @@ -1,6 +1,7 @@ #ifndef STORM_SETTINGS_MODULES_MODULESETTINGS_H_ #define STORM_SETTINGS_MODULES_MODULESETTINGS_H_ +#include #include #include #include diff --git a/src/storm/solver/helper/DiscountedValueIterationHelper.h b/src/storm/solver/helper/DiscountedValueIterationHelper.h index 4bf2ca110a..fa654ca8d0 100644 --- a/src/storm/solver/helper/DiscountedValueIterationHelper.h +++ b/src/storm/solver/helper/DiscountedValueIterationHelper.h @@ -1,5 +1,6 @@ #pragma once +#include #include #include #include diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h index c292c5a6d5..5491046f1f 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.h +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.h @@ -1,5 +1,6 @@ #pragma once +#include #include #include #include diff --git a/src/storm/solver/helper/RationalSearchHelper.h b/src/storm/solver/helper/RationalSearchHelper.h index 45af97a247..7f85b4051f 100644 --- a/src/storm/solver/helper/RationalSearchHelper.h +++ b/src/storm/solver/helper/RationalSearchHelper.h @@ -1,5 +1,6 @@ #pragma once +#include #include #include #include diff --git a/src/storm/solver/helper/SchedulerTrackingHelper.h b/src/storm/solver/helper/SchedulerTrackingHelper.h index 7a3ad04c37..df700c6f77 100644 --- a/src/storm/solver/helper/SchedulerTrackingHelper.h +++ b/src/storm/solver/helper/SchedulerTrackingHelper.h @@ -1,7 +1,10 @@ #pragma once +#include #include #include +#include + #include "storm/solver/OptimizationDirection.h" #include "storm/solver/UncertaintyResolutionMode.h" #include "storm/solver/helper/ValueIterationOperatorForward.h" diff --git a/src/storm/solver/helper/ValueIterationHelper.h b/src/storm/solver/helper/ValueIterationHelper.h index 3a78450463..cfe3bee7d9 100644 --- a/src/storm/solver/helper/ValueIterationHelper.h +++ b/src/storm/solver/helper/ValueIterationHelper.h @@ -1,5 +1,6 @@ #pragma once +#include #include #include #include diff --git a/src/storm/solver/multiplier/Multiplier.h b/src/storm/solver/multiplier/Multiplier.h index b9c8e6a244..d471a85f2e 100644 --- a/src/storm/solver/multiplier/Multiplier.h +++ b/src/storm/solver/multiplier/Multiplier.h @@ -1,5 +1,6 @@ #pragma once +#include #include #include diff --git a/src/storm/solver/multiplier/NativeMultiplier.h b/src/storm/solver/multiplier/NativeMultiplier.h index fbecd2e861..3453e8a5fa 100644 --- a/src/storm/solver/multiplier/NativeMultiplier.h +++ b/src/storm/solver/multiplier/NativeMultiplier.h @@ -1,5 +1,7 @@ #pragma once +#include + #include "storm/solver/multiplier/Multiplier.h" #include "storm/solver/OptimizationDirection.h" diff --git a/src/storm/storage/ConsecutiveUint64DynamicPriorityQueue.h b/src/storm/storage/ConsecutiveUint64DynamicPriorityQueue.h index 1d5b59332e..c0f964e429 100644 --- a/src/storm/storage/ConsecutiveUint64DynamicPriorityQueue.h +++ b/src/storm/storage/ConsecutiveUint64DynamicPriorityQueue.h @@ -1,6 +1,7 @@ #pragma once #include +#include #include #include diff --git a/src/storm/storage/DeterministicTransition.h b/src/storm/storage/DeterministicTransition.h index 876e1993fe..1d2091563c 100644 --- a/src/storm/storage/DeterministicTransition.h +++ b/src/storm/storage/DeterministicTransition.h @@ -7,6 +7,9 @@ #pragma once +#include +#include + namespace storm { namespace storage { typedef uint_fast64_t StateId; diff --git a/src/storm/storage/IntegerInterval.h b/src/storm/storage/IntegerInterval.h index 4f33c1491f..57eb0005a1 100644 --- a/src/storm/storage/IntegerInterval.h +++ b/src/storm/storage/IntegerInterval.h @@ -1,6 +1,7 @@ #pragma once #include +#include namespace storm { namespace storage { diff --git a/src/storm/storage/PairHash.h b/src/storm/storage/PairHash.h index 1d53b82b46..18d1edae14 100644 --- a/src/storm/storage/PairHash.h +++ b/src/storm/storage/PairHash.h @@ -2,6 +2,7 @@ #define STORM_STORAGE_PAIRHASH_H_ #include +#include namespace std { template<> diff --git a/src/storm/storage/Qvbs.h b/src/storm/storage/Qvbs.h index 8f89c61e6e..d883e72c63 100644 --- a/src/storm/storage/Qvbs.h +++ b/src/storm/storage/Qvbs.h @@ -1,6 +1,7 @@ #pragma once #include +#include #include #include diff --git a/src/storm/storage/StateActionPair.h b/src/storm/storage/StateActionPair.h index 61a8dd6cff..335668db23 100644 --- a/src/storm/storage/StateActionPair.h +++ b/src/storm/storage/StateActionPair.h @@ -1,6 +1,7 @@ #ifndef STATEACTIONPAIR_H #define STATEACTIONPAIR_H +#include #include namespace storm { diff --git a/src/storm/storage/StateActionTargetTuple.h b/src/storm/storage/StateActionTargetTuple.h index 6c4c293d6f..9c28e2052d 100644 --- a/src/storm/storage/StateActionTargetTuple.h +++ b/src/storm/storage/StateActionTargetTuple.h @@ -2,6 +2,7 @@ #ifndef STATEACTIONTARGETTUPLE_H #define STATEACTIONTARGETTUPLE_H +#include #include namespace storm { diff --git a/src/storm/storage/bisimulation/Block.h b/src/storm/storage/bisimulation/Block.h index db412e739b..d7bc864991 100644 --- a/src/storm/storage/bisimulation/Block.h +++ b/src/storm/storage/bisimulation/Block.h @@ -1,5 +1,7 @@ #pragma once +#include + #include "storm/storage/sparse/StateType.h" namespace storm { diff --git a/src/storm/storage/bisimulation/DeterministicBlockData.h b/src/storm/storage/bisimulation/DeterministicBlockData.h index e0f345813b..84f274436c 100644 --- a/src/storm/storage/bisimulation/DeterministicBlockData.h +++ b/src/storm/storage/bisimulation/DeterministicBlockData.h @@ -1,5 +1,9 @@ #pragma once +#include +#include +#include + #include "storm/storage/bisimulation/Block.h" namespace storm { diff --git a/src/storm/storage/dd/Odd.h b/src/storm/storage/dd/Odd.h index 869020e97c..749077ac6b 100644 --- a/src/storm/storage/dd/Odd.h +++ b/src/storm/storage/dd/Odd.h @@ -1,5 +1,6 @@ #pragma once +#include #include #include #include diff --git a/src/storm/storage/jani/ParallelComposition.h b/src/storm/storage/jani/ParallelComposition.h index 9a28dfe0f7..fdeb8f4535 100644 --- a/src/storm/storage/jani/ParallelComposition.h +++ b/src/storm/storage/jani/ParallelComposition.h @@ -1,5 +1,6 @@ #pragma once +#include #include #include #include diff --git a/src/storm/storage/umb/model/FileTypes.h b/src/storm/storage/umb/model/FileTypes.h index eb41a29a44..6f892f3316 100644 --- a/src/storm/storage/umb/model/FileTypes.h +++ b/src/storm/storage/umb/model/FileTypes.h @@ -1,5 +1,6 @@ #pragma once +#include #include #include #include diff --git a/src/storm/storage/umb/model/StringEncoding.h b/src/storm/storage/umb/model/StringEncoding.h index 65d7a423e5..dadb3344b1 100644 --- a/src/storm/storage/umb/model/StringEncoding.h +++ b/src/storm/storage/umb/model/StringEncoding.h @@ -1,4 +1,5 @@ #pragma once +#include #include #include diff --git a/src/storm/utility/ProgressMeasurement.h b/src/storm/utility/ProgressMeasurement.h index 3453d72fa8..05cf2de41b 100644 --- a/src/storm/utility/ProgressMeasurement.h +++ b/src/storm/utility/ProgressMeasurement.h @@ -2,6 +2,7 @@ #include #include +#include #include namespace storm { diff --git a/src/storm/utility/SignalHandler.h b/src/storm/utility/SignalHandler.h index 59cba034b2..f7602d99d7 100644 --- a/src/storm/utility/SignalHandler.h +++ b/src/storm/utility/SignalHandler.h @@ -3,6 +3,8 @@ #include #include +#include + #include "storm-config.h" #include "storm/utility/OsDetection.h" diff --git a/src/storm/utility/math.h b/src/storm/utility/math.h index d9c1b89223..31ab45707b 100644 --- a/src/storm/utility/math.h +++ b/src/storm/utility/math.h @@ -2,6 +2,7 @@ #define STORM_UTILITY_MATH_H_ #include +#include #include "storm/utility/macros.h" namespace storm { diff --git a/src/storm/utility/numerical.h b/src/storm/utility/numerical.h index 25e15308d6..b8e904c582 100644 --- a/src/storm/utility/numerical.h +++ b/src/storm/utility/numerical.h @@ -1,5 +1,6 @@ #pragma once +#include #include namespace storm { diff --git a/src/storm/utility/random.h b/src/storm/utility/random.h index 8b711b50c4..bfd7c82792 100644 --- a/src/storm/utility/random.h +++ b/src/storm/utility/random.h @@ -1,6 +1,7 @@ #pragma once #include +#include #include #include "storm/adapters/RationalNumberAdapter.h" diff --git a/src/storm/utility/shortestPaths.h b/src/storm/utility/shortestPaths.h index 63acb9fd89..8e3696c49e 100644 --- a/src/storm/utility/shortestPaths.h +++ b/src/storm/utility/shortestPaths.h @@ -1,7 +1,13 @@ #ifndef STORM_UTIL_SHORTESTPATHS_H_ #define STORM_UTIL_SHORTESTPATHS_H_ +#include #include +#include +#include +#include +#include +#include #include #include diff --git a/src/storm/utility/threads.cpp b/src/storm/utility/threads.cpp index eee44c2e9e..0731c75edd 100644 --- a/src/storm/utility/threads.cpp +++ b/src/storm/utility/threads.cpp @@ -1,5 +1,7 @@ #include "storm/utility/threads.h" +#include +#include #include #include diff --git a/src/storm/utility/threads.h b/src/storm/utility/threads.h index a5851a0d68..2fe6e9b7b5 100644 --- a/src/storm/utility/threads.h +++ b/src/storm/utility/threads.h @@ -1,5 +1,7 @@ #pragma once +#include + namespace storm { namespace utility { uint64_t getNumberOfThreads(); diff --git a/src/test/storm-dft/CMakeLists.txt b/src/test/storm-dft/CMakeLists.txt index d8e12cc84d..bb54502a4f 100644 --- a/src/test/storm-dft/CMakeLists.txt +++ b/src/test/storm-dft/CMakeLists.txt @@ -12,7 +12,7 @@ foreach (testsuite api bdd simulator storage transformations) target_link_libraries(test-dft-${testsuite} storm-dft storm-parsers) target_link_libraries(test-dft-${testsuite} ${STORM_TEST_LINK_LIBRARIES}) target_include_directories(test-dft-${testsuite} PRIVATE "${PROJECT_SOURCE_DIR}/src") - target_precompile_headers(test-dft-${testsuite} REUSE_FROM test-builder) + storm_target_precompile_headers(test-dft-${testsuite} REUSE_FROM test-builder) add_dependencies(test-dft-${testsuite} test-resources) add_test(NAME run-test-dft-${testsuite} COMMAND $) diff --git a/src/test/storm-gamebased-ar/CMakeLists.txt b/src/test/storm-gamebased-ar/CMakeLists.txt index 7436c99b5f..5547645675 100644 --- a/src/test/storm-gamebased-ar/CMakeLists.txt +++ b/src/test/storm-gamebased-ar/CMakeLists.txt @@ -11,7 +11,7 @@ foreach (testsuite abstraction modelchecker) target_link_libraries(test-gamebased-ar-${testsuite} storm-gamebased-ar storm-parsers) target_link_libraries(test-gamebased-ar-${testsuite} ${STORM_TEST_LINK_LIBRARIES}) target_include_directories(test-gamebased-ar-${testsuite} PRIVATE "${PROJECT_SOURCE_DIR}/src") - target_precompile_headers(test-gamebased-ar-${testsuite} REUSE_FROM test-builder) + storm_target_precompile_headers(test-gamebased-ar-${testsuite} REUSE_FROM test-builder) add_dependencies(test-gamebased-ar-${testsuite} test-resources) add_test(NAME run-test-gamebased-ar-${testsuite} COMMAND $) diff --git a/src/test/storm-pars/CMakeLists.txt b/src/test/storm-pars/CMakeLists.txt index 6b66b6d6ee..32753f211d 100644 --- a/src/test/storm-pars/CMakeLists.txt +++ b/src/test/storm-pars/CMakeLists.txt @@ -11,7 +11,7 @@ foreach (testsuite derivative modelchecker transformer utility) target_link_libraries(test-pars-${testsuite} storm-pars storm-parsers) target_link_libraries(test-pars-${testsuite} ${STORM_TEST_LINK_LIBRARIES}) target_include_directories(test-pars-${testsuite} PRIVATE "${PROJECT_SOURCE_DIR}/src") - target_precompile_headers(test-pars-${testsuite} REUSE_FROM test-builder) + storm_target_precompile_headers(test-pars-${testsuite} REUSE_FROM test-builder) add_dependencies(test-pars-${testsuite} test-resources) add_test(NAME run-test-pars-${testsuite} COMMAND $) diff --git a/src/test/storm-permissive/CMakeLists.txt b/src/test/storm-permissive/CMakeLists.txt index e382cf98e0..49406045c5 100644 --- a/src/test/storm-permissive/CMakeLists.txt +++ b/src/test/storm-permissive/CMakeLists.txt @@ -11,7 +11,7 @@ foreach (testsuite analysis) target_link_libraries(test-permissive-${testsuite} storm-permissive storm-parsers) target_link_libraries(test-permissive-${testsuite} ${STORM_TEST_LINK_LIBRARIES}) target_include_directories(test-permissive-${testsuite} PRIVATE "${PROJECT_SOURCE_DIR}/src") - target_precompile_headers(test-permissive-${testsuite} REUSE_FROM test-builder) + storm_target_precompile_headers(test-permissive-${testsuite} REUSE_FROM test-builder) add_dependencies(test-permissive-${testsuite} test-resources) add_test(NAME run-test-permissive-${testsuite} COMMAND $) diff --git a/src/test/storm-pomdp/CMakeLists.txt b/src/test/storm-pomdp/CMakeLists.txt index 59956f7702..97cff7825c 100644 --- a/src/test/storm-pomdp/CMakeLists.txt +++ b/src/test/storm-pomdp/CMakeLists.txt @@ -11,7 +11,7 @@ foreach (testsuite analysis api modelchecker tracking transformation generator) target_link_libraries(test-pomdp-${testsuite} storm-pomdp storm-parsers) target_link_libraries(test-pomdp-${testsuite} ${STORM_TEST_LINK_LIBRARIES}) target_include_directories(test-pomdp-${testsuite} PRIVATE "${PROJECT_SOURCE_DIR}/src") - target_precompile_headers(test-pomdp-${testsuite} REUSE_FROM test-builder) + storm_target_precompile_headers(test-pomdp-${testsuite} REUSE_FROM test-builder) add_dependencies(test-pomdp-${testsuite} test-resources) add_test(NAME run-test-pomdp-${testsuite} COMMAND $) diff --git a/src/test/storm/CMakeLists.txt b/src/test/storm/CMakeLists.txt index b1e6831b91..ebe43a4343 100755 --- a/src/test/storm/CMakeLists.txt +++ b/src/test/storm/CMakeLists.txt @@ -26,10 +26,10 @@ foreach(testsuite ${NON_SPLIT_TESTS}) add_executable(test-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp) if (REUSE_PCH_FROM STREQUAL "") # note that reusing from storm main leads to errors on arch linux (late 2023). - target_precompile_headers(test-${testsuite} PRIVATE ${STORM_PRECOMPILED_HEADERS}) + storm_target_precompile_headers(test-${testsuite} PRIVATE ${STORM_PRECOMPILED_HEADERS}) set(REUSE_PCH_FROM "test-${testsuite}") else () - target_precompile_headers(test-${testsuite} REUSE_FROM ${REUSE_PCH_FROM}) + storm_target_precompile_headers(test-${testsuite} REUSE_FROM ${REUSE_PCH_FROM}) endif() configure_testsuite_target(${testsuite}) endforeach() @@ -39,7 +39,7 @@ foreach(modelchecker_split ${MODELCHECKER_TEST_SPLITS}) file(GLOB_RECURSE TEST_MODELCHECKER_${modelchecker_split}_FILES ${STORM_TESTS_BASE_PATH}/modelchecker/${modelchecker_split}/*.h ${STORM_TESTS_BASE_PATH}/modelchecker/${modelchecker_split}/*.cpp ${STORM_TESTS_BASE_PATH}/../storm_gtest.cpp) add_executable(test-modelchecker-${modelchecker_split} ${TEST_MODELCHECKER_${modelchecker_split}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp) configure_testsuite_target(modelchecker-${modelchecker_split}) - target_precompile_headers(test-modelchecker-${modelchecker_split} REUSE_FROM ${REUSE_PCH_FROM}) + storm_target_precompile_headers(test-modelchecker-${modelchecker_split} REUSE_FROM ${REUSE_PCH_FROM}) endforeach() # Modelchecker-Prctl testsuite split @@ -47,5 +47,5 @@ foreach(prctl_split ${MODELCHECKER_PRCTL_TEST_SPLITS}) file(GLOB_RECURSE TEST_MODELCHECKER_PRCTL_${prctl_split}_FILES ${STORM_TESTS_BASE_PATH}/modelchecker/prctl/${prctl_split}/*.h ${STORM_TESTS_BASE_PATH}/modelchecker/prctl/${prctl_split}/*.cpp ${STORM_TESTS_BASE_PATH}/../storm_gtest.cpp) add_executable(test-modelchecker-prctl-${prctl_split} ${TEST_MODELCHECKER_PRCTL_${prctl_split}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp) configure_testsuite_target(modelchecker-prctl-${prctl_split}) - target_precompile_headers(test-modelchecker-prctl-${prctl_split} REUSE_FROM ${REUSE_PCH_FROM}) + storm_target_precompile_headers(test-modelchecker-prctl-${prctl_split} REUSE_FROM ${REUSE_PCH_FROM}) endforeach()