diff --git a/_posts/2017-03-11-version-1.0.0.md b/_posts/2017-03-11-version-1.0.0.md index 6db5d54..55de21e 100644 --- a/_posts/2017-03-11-version-1.0.0.md +++ b/_posts/2017-03-11-version-1.0.0.md @@ -19,4 +19,4 @@ $ brew update $ brew upgrade stormchecker ``` -If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/troubleshooting.html#file-an-issue' | relative_url }}). +If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/build-troubleshooting.html#file-an-issue' | relative_url }}). diff --git a/_posts/2017-08-10-version.1.1.0.md b/_posts/2017-08-10-version.1.1.0.md index bce4056..2b8ae8a 100644 --- a/_posts/2017-08-10-version.1.1.0.md +++ b/_posts/2017-08-10-version.1.1.0.md @@ -18,4 +18,4 @@ $ brew update $ brew upgrade stormchecker ``` -If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/troubleshooting.html#file-an-issue' | relative_url }}). +If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/build-troubleshooting.html#file-an-issue' | relative_url }}). diff --git a/_posts/2017-12-12-version.1.2.0.md b/_posts/2017-12-12-version.1.2.0.md index 29db9e6..7a2111a 100644 --- a/_posts/2017-12-12-version.1.2.0.md +++ b/_posts/2017-12-12-version.1.2.0.md @@ -20,4 +20,4 @@ $ brew upgrade stormchecker Moreover the python bindings [stormpy](https://stormchecker.github.io/stormpy/) are now also released in version [1.2.0](https://github.com/stormchecker/stormpy/releases/tag/1.2.0). -If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/troubleshooting.html#file-an-issue' | relative_url }}). +If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/build-troubleshooting.html#file-an-issue' | relative_url }}). diff --git a/_posts/2018-12-15-version.1.3.0.md b/_posts/2018-12-15-version.1.3.0.md index 69f1c64..1d491be 100644 --- a/_posts/2018-12-15-version.1.3.0.md +++ b/_posts/2018-12-15-version.1.3.0.md @@ -19,4 +19,4 @@ $ brew update $ brew upgrade stormchecker ``` -If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/troubleshooting.html#file-an-issue' | relative_url }}). +If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/build-troubleshooting.html#file-an-issue' | relative_url }}). diff --git a/_posts/2019-11-15-version.1.4.0.md b/_posts/2019-11-15-version.1.4.0.md index 44709bb..b68067d 100644 --- a/_posts/2019-11-15-version.1.4.0.md +++ b/_posts/2019-11-15-version.1.4.0.md @@ -19,4 +19,4 @@ $ brew update $ brew upgrade stormchecker ``` -If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/troubleshooting.html#file-an-issue' | relative_url }}). +If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/build-troubleshooting.html#file-an-issue' | relative_url }}). diff --git a/_posts/2020-03-12-version.1.5.0.md b/_posts/2020-03-12-version.1.5.0.md index 78ba13a..993f962 100644 --- a/_posts/2020-03-12-version.1.5.0.md +++ b/_posts/2020-03-12-version.1.5.0.md @@ -22,4 +22,4 @@ You can get the new release of Storm via your preferred installation option: ``` - or by using a [Docker container]({{ '/documentation/obtain-storm/docker.html' | relative_url }}). -If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/troubleshooting.html#file-an-issue' | relative_url }}). +If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/build-troubleshooting.html#file-an-issue' | relative_url }}). diff --git a/_posts/2020-06-08-version.1.6.0.md b/_posts/2020-06-08-version.1.6.0.md index 4e3a31b..142af30 100644 --- a/_posts/2020-06-08-version.1.6.0.md +++ b/_posts/2020-06-08-version.1.6.0.md @@ -27,4 +27,4 @@ You can get the new release of Storm via your preferred installation option: ``` - or by using a [Docker container]({{ '/documentation/obtain-storm/docker.html' | relative_url }}). -If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/troubleshooting.html#file-an-issue' | relative_url }}). +If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/build-troubleshooting.html#file-an-issue' | relative_url }}). diff --git a/_posts/2022-07-31-version.1.7.0.md b/_posts/2022-07-31-version.1.7.0.md index 12f0d41..1d0e289 100644 --- a/_posts/2022-07-31-version.1.7.0.md +++ b/_posts/2022-07-31-version.1.7.0.md @@ -21,4 +21,4 @@ For detailed information on all the changes, please check the [release notes of You can get the new release of Storm either by building from [source]({{ '/documentation/obtain-storm/build.html' | relative_url }}), via [Homebrew]({{ '/documentation/obtain-storm/homebrew.html' | relative_url }}) or by using a [Docker container]({{ '/documentation/obtain-storm/docker.html' | relative_url }}). -If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/troubleshooting.html#file-an-issue' | relative_url }}). +If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/build-troubleshooting.html#file-an-issue' | relative_url }}). diff --git a/_posts/2023-06-13-version.1.8.0.md b/_posts/2023-06-13-version.1.8.0.md index a22595a..9136c5f 100644 --- a/_posts/2023-06-13-version.1.8.0.md +++ b/_posts/2023-06-13-version.1.8.0.md @@ -17,4 +17,4 @@ For detailed information on all the changes, please check the [release notes of You can get the new release of Storm either by building from [source]({{ '/documentation/obtain-storm/build.html' | relative_url }}), via [Homebrew]({{ '/documentation/obtain-storm/homebrew.html' | relative_url }}) or by using a [Docker container]({{ '/documentation/obtain-storm/docker.html' | relative_url }}). -If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/troubleshooting.html#file-an-issue' | relative_url }}). +If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/build-troubleshooting.html#file-an-issue' | relative_url }}). diff --git a/_posts/2024-08-23-version.1.9.0.md b/_posts/2024-08-23-version.1.9.0.md index 34c8349..6d290e8 100644 --- a/_posts/2024-08-23-version.1.9.0.md +++ b/_posts/2024-08-23-version.1.9.0.md @@ -16,4 +16,4 @@ For detailed information on all the changes, please check the [release notes of You can get the new release of Storm either by building from [source]({{ '/documentation/obtain-storm/build.html' | relative_url }}), via [Homebrew]({{ '/documentation/obtain-storm/homebrew.html' | relative_url }}) or by using a [Docker container]({{ '/documentation/obtain-storm/docker.html' | relative_url }}). -If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/troubleshooting.html#file-an-issue' | relative_url }}). +If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/build-troubleshooting.html#file-an-issue' | relative_url }}). diff --git a/_posts/2025-06-02-version.1.10.0.md b/_posts/2025-06-02-version.1.10.0.md index e628760..8c94234 100644 --- a/_posts/2025-06-02-version.1.10.0.md +++ b/_posts/2025-06-02-version.1.10.0.md @@ -16,4 +16,4 @@ For detailed information on all the changes, please check the [release notes of You can get the new release of Storm either by building from [source]({{ '/documentation/obtain-storm/build.html' | relative_url }}), via [Homebrew]({{ '/documentation/obtain-storm/homebrew.html' | relative_url }}) or by using a [Docker container]({{ '/documentation/obtain-storm/docker.html' | relative_url }}). The Docker images now natively support both Intel and ARM architectures. -If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/troubleshooting.html#file-an-issue' | relative_url }}). +If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/build-troubleshooting.html#file-an-issue' | relative_url }}). diff --git a/_posts/2025-09-11-version.1.11.0.md b/_posts/2025-09-11-version.1.11.0.md index 4f69b01..dcdb4af 100644 --- a/_posts/2025-09-11-version.1.11.0.md +++ b/_posts/2025-09-11-version.1.11.0.md @@ -19,4 +19,4 @@ For detailed information on all the changes, please check the [release notes of You can get the new release of Storm either by building from [source]({{ '/documentation/obtain-storm/build.html' | relative_url }}), via [Homebrew]({{ '/documentation/obtain-storm/homebrew.html' | relative_url }}) or by using a [Docker container]({{ '/documentation/obtain-storm/docker.html' | relative_url }}). You can obtain the stormpy Python package by simply executing `pip install stormpy`. -If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/troubleshooting.html#file-an-issue' | relative_url }}). +If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/build-troubleshooting.html#file-an-issue' | relative_url }}). diff --git a/_posts/2026-03-11-version.1.12.0.md b/_posts/2026-03-11-version.1.12.0.md index 4977534..cbb3e17 100644 --- a/_posts/2026-03-11-version.1.12.0.md +++ b/_posts/2026-03-11-version.1.12.0.md @@ -18,4 +18,4 @@ We refer to the [release notes of stormpy](https://github.com/stormchecker/storm You can get the new release of Storm either by building from [source]({{ '/documentation/obtain-storm/build.html' | relative_url }}), via [Homebrew]({{ '/documentation/obtain-storm/homebrew.html' | relative_url }}) or by using a [Docker container]({{ '/documentation/obtain-storm/docker.html' | relative_url }}). You can obtain the stormpy Python package by simply executing `pip install stormpy`. -If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/troubleshooting.html#file-an-issue' | relative_url }}). +If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/build-troubleshooting.html#file-an-issue' | relative_url }}). diff --git a/_posts/2026-03-26-stormchecker.md b/_posts/2026-03-26-stormchecker.md index 45bed31..f51f53f 100644 --- a/_posts/2026-03-26-stormchecker.md +++ b/_posts/2026-03-26-stormchecker.md @@ -18,4 +18,4 @@ For example, the following command updates the `origin` remote for the Storm rep ``` git remote set-url origin git@github.com:stormchecker/storm.git ``` -Please [let us know](https://www.stormchecker.org/documentation/obtain-storm/troubleshooting.html#file-an-issue) in case you found dead links or encounter any issue. +Please [let us know]({{ '/documentation/obtain-storm/build-troubleshooting.html#file-an-issue' | relative_url }}) in case you found dead links or encounter any issue. diff --git a/_posts/2026-05-16-version.1.13.0.md b/_posts/2026-05-16-version.1.13.0.md index bb8b4e1..051db2d 100644 --- a/_posts/2026-05-16-version.1.13.0.md +++ b/_posts/2026-05-16-version.1.13.0.md @@ -17,4 +17,4 @@ We refer to the [release notes of stormpy](https://github.com/stormchecker/storm You can get the new release of Storm either by building from [source]({{ '/documentation/obtain-storm/build.html' | relative_url }}), via the pre-built binaries from [Homebrew]({{ '/documentation/obtain-storm/homebrew.html' | relative_url }}), via the pre-built Debian packages attached to the [release](https://github.com/stormchecker/storm/releases/tag/1.13.0) or by using a [Docker container]({{ '/documentation/obtain-storm/docker.html' | relative_url }}). You can obtain the stormpy Python package by simply executing `pip install stormpy`. -If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/troubleshooting.html#file-an-issue' | relative_url }}). +If you experience any bugs, please [let us know]({{ '/documentation/obtain-storm/build-troubleshooting.html#file-an-issue' | relative_url }}). diff --git a/about.md b/about.md index 6bcdd2a..fef8329 100644 --- a/about.md +++ b/about.md @@ -81,7 +81,7 @@ While Storm tries to make it easy to include new functionality, a developer stil Storm -- has roughly ~220k lines of C++ code (as of April 2023) +- has roughly ~290k lines of C++ code (as of August 2026) - is under development since 2012 - went open source in 2017 - has over 15 [contributors](https://github.com/stormchecker/storm/graphs/contributors) diff --git a/documentation/background/drn.md b/documentation/background/drn.md index 631f3f6..4ae4e82 100644 --- a/documentation/background/drn.md +++ b/documentation/background/drn.md @@ -3,7 +3,7 @@ title: DRN input format layout: default documentation: true category_weight: 2 -categories: [languages] +categories: [Languages] ---

DRN input format

diff --git a/documentation/background/engines.md b/documentation/background/engines.md index 8483e55..7a2d1c8 100644 --- a/documentation/background/engines.md +++ b/documentation/background/engines.md @@ -46,7 +46,7 @@ Storm's main engine is the sparse engine in the sense that it tends to have the - target query does not involve heavy numerical computations (for example qualitative queries) **Major restrictions**: -- only supports [discrete-time models](models.html) +- only supports [discrete-time models]({{ '/documentation/background/models.html' | relative_url }}) ## Hybrid @@ -75,7 +75,7 @@ All engines so far have the requirement that a representation of the model needs - low target precision **Major restrictions**: -- only supports [discrete-time models](models.html) +- only supports [discrete-time models]({{ '/documentation/background/models.html' | relative_url }}) - only supports reachability objectives ## Abstraction-Refinement @@ -92,5 +92,5 @@ This engine relies heavily on SMT solving (more concretely an enumeration of all - model is well structured **Major restrictions**: -- only supports [discrete-time models](models.html) +- only supports [discrete-time models]({{ '/documentation/background/models.html' | relative_url }}) - only supports reachability objectives diff --git a/documentation/background/properties.md b/documentation/background/properties.md index b93ef2c..4b60382 100644 --- a/documentation/background/properties.md +++ b/documentation/background/properties.md @@ -10,14 +10,14 @@ categories: [Background] {% include includes/toc.html %} -Storm takes properties in a format that can be described as an "extended subset" of the [PRISM property language](https://www.prismmodelchecker.org/manual/PropertySpecification/Introduction){:target="_blank"}. Alternatively, if the input is given in terms of a [JANI](languages.html#jani) model, the properties are embedded in the model in the appropriate format. +Storm takes properties in a format that can be described as an "extended subset" of the [PRISM property language](https://www.prismmodelchecker.org/manual/PropertySpecification/Introduction){:target="_blank"}. Alternatively, if the input is given in terms of a [JANI]({{ '/documentation/background/languages.html#jani' | relative_url }}) model, the properties are embedded in the model in the appropriate format. {:.alert .alert-info} For DFTs, GSPNs and probabilistic programs, domain-specific properties can be given. For this, we refer to the guide on how to [run Storm]({{ '/documentation/usage/running-storm.html' | relative_url }}){:.alert-link} on those inputs. ## Identifying States -Storm allows to identify sets of states by either labels or via the symbolic variables describing the model. Note that it depends on the [input language](languages.html) which of these two ways are enabled. For example, for explicit models, there are no symbolic variables and therefore only labels can be used. For PRISM and JANI input, both labels and expressions over model variables are valid. Finally, the expression `true` can be used to describe the set of all states. +Storm allows to identify sets of states by either labels or via the symbolic variables describing the model. Note that it depends on the [input language]({{ '/documentation/background/languages.html' | relative_url }}) which of these two ways are enabled. For example, for explicit models, there are no symbolic variables and therefore only labels can be used. For PRISM and JANI input, both labels and expressions over model variables are valid. Finally, the expression `true` can be used to describe the set of all states. ### Labels diff --git a/documentation/obtain-storm/troubleshooting.md b/documentation/obtain-storm/build-troubleshooting.md similarity index 75% rename from documentation/obtain-storm/troubleshooting.md rename to documentation/obtain-storm/build-troubleshooting.md index 5ab3ccb..b0456c1 100644 --- a/documentation/obtain-storm/troubleshooting.md +++ b/documentation/obtain-storm/build-troubleshooting.md @@ -1,12 +1,12 @@ --- -title: Troubleshooting +title: Build Troubleshooting layout: default documentation: true category_weight: 7 categories: [Obtain Storm] --- -

Troubleshooting

+

Build Troubleshooting

{% include includes/toc.html %} @@ -28,16 +28,6 @@ We list common issues for specific operating systems. - Start Xcode at least once such that required components might be installed automatically. -- For macOS 10.14 "Mojave" a common error is the following: - ``` console - configure: error: cannot run C compiled programs. - ``` - This error might be due to missing header files which can be installed by the following tool: - ``` console - $ open /Library/Developer/CommandLineTools/Packages/macOS_SDK_headers_for_macOS_10.14.pkg - ``` - For more infos see this [GitHub issue](https://github.com/neovim/neovim/issues/9050#issuecomment-424417456). - ## File an issue If you encounter problems when building (or using) Storm, feel free to [contact us]({{ '/about.html#people' | relative_url }}) by writing a mail to diff --git a/documentation/obtain-storm/build.md b/documentation/obtain-storm/build.md index b463f75..768fcaf 100644 --- a/documentation/obtain-storm/build.md +++ b/documentation/obtain-storm/build.md @@ -79,7 +79,7 @@ Then, use cmake to configure the build of Storm on your system by invoking $ cmake .. ``` -Check the output carefully for errors and warnings. If all dependencies are properly installed and found, you are ready to build Storm and move to the next step. In case of errors, check the [dependencies](dependencies.html), consult the [troubleshooting guide](troubleshooting.html) and, if necessary, [file an issue](troubleshooting.html#file-an-issue). +Check the output carefully for errors and warnings. If all dependencies are properly installed and found, you are ready to build Storm and move to the next step. In case of errors, check the [dependencies](dependencies.html), consult the [troubleshooting guide](build-troubleshooting.html) and, if necessary, [file an issue](build-troubleshooting.html#file-an-issue). ## Build Step @@ -129,4 +129,4 @@ We recommend to execute it to verify that Storm produces correct results on your $ make check ``` -will build and run the tests. In case of errors, please do not hesitate to [file an issue](troubleshooting.html#file-an-issue). +will build and run the tests. In case of errors, please do not hesitate to [file an issue](build-troubleshooting.html#file-an-issue). diff --git a/documentation/obtain-storm/docker.md b/documentation/obtain-storm/docker.md index a614cb0..5bfa094 100644 --- a/documentation/obtain-storm/docker.md +++ b/documentation/obtain-storm/docker.md @@ -17,7 +17,7 @@ To use the containers you first have to install [Docker](https://docs.docker.com On macOS you can use [homebrew](https://brew.sh/){:target="_blank"} to install Docker. ```console -$ brew cask install docker +$ brew install --cask docker ``` Next you should start the Docker app and its tray icon should be visible. diff --git a/documentation/obtain-storm/vm.md b/documentation/obtain-storm/vm.md index 365aae2..d3c06ef 100644 --- a/documentation/obtain-storm/vm.md +++ b/documentation/obtain-storm/vm.md @@ -62,7 +62,7 @@ make check ``` {:.alert .alert-danger} -If any problems occur during this process (in particular when using a standard Ubuntu version) please [let us know](troubleshooting.html#file-an-issue){:.alert-link}. +If any problems occur during this process (in particular when using a standard Ubuntu version) please [let us know](build-troubleshooting.html#file-an-issue){:.alert-link}. ## Storm 1.6.3 (2020/12) diff --git a/documentation/usage/troubleshooting.md b/documentation/usage/runtime-troubleshooting.md similarity index 97% rename from documentation/usage/troubleshooting.md rename to documentation/usage/runtime-troubleshooting.md index 82a7c5c..6b279e1 100644 --- a/documentation/usage/troubleshooting.md +++ b/documentation/usage/runtime-troubleshooting.md @@ -1,12 +1,12 @@ --- -title: Troubleshooting +title: Runtime Troubleshooting layout: default documentation: true category_weight: 4 categories: [Use Storm] --- -

Troubleshooting

+

Runtime Troubleshooting

{% include includes/toc.html %} diff --git a/getting-started.md b/getting-started.md index 8e454da..bb17829 100644 --- a/getting-started.md +++ b/getting-started.md @@ -10,20 +10,20 @@ layout: default To be able to run Storm, you need to obtain it and run it on your system. Currently, you can choose one of the following options: -* Build Storm [from source](documentation/obtain-storm/build.html) on macOS or Linux +* Build Storm [from source]({{ '/documentation/obtain-storm/build.html' | relative_url }}) on macOS or Linux * Install Storm via a supported package manager - * [Homebrew](documentation/obtain-storm/homebrew.html) on macOS + * [Homebrew]({{ '/documentation/obtain-storm/homebrew.html' | relative_url }}) on macOS * [AUR](https://aur.archlinux.org/packages/stormchecker) on Arch Linux -* Use a [Docker container](documentation/obtain-storm/docker.html) on macOS, Linux or Windows -* Use a [virtual machine](documentation/obtain-storm/vm.html) on macOS, Linux or Windows +* Use a [Docker container]({{ '/documentation/obtain-storm/docker.html' | relative_url }}) on macOS, Linux or Windows +* Use a [virtual machine]({{ '/documentation/obtain-storm/vm.html' | relative_url }}) on macOS, Linux or Windows ## 2. Prepare a model checking query -After you have obtained Storm, you need to make sure that your input model has the right form. That is, on a fundamental level, you need to ensure that your input model falls into one of the [model types](documentation/background/models.html) supported by Storm. +After you have obtained Storm, you need to make sure that your input model has the right form. That is, on a fundamental level, you need to ensure that your input model falls into one of the [model types]({{ '/documentation/background/models.html' | relative_url }}) supported by Storm. -If your model indeed does, then the next thing is to have the model available in an [input language](documentation/background/languages.html) of Storm. If you don't have such a model yet, you need to first model the system you are interested in or transcribe it from a different input format. +If your model indeed does, then the next thing is to have the model available in an [input language]({{ '/documentation/background/languages.html' | relative_url }}) of Storm. If you don't have such a model yet, you need to first model the system you are interested in or transcribe it from a different input format. -However, the input model is only "half" of the input you need to provide, the other "half" being the property you want to verify. Please consult our [guide to properties](documentation/background/properties.html) for details on how to specify them. +However, the input model is only "half" of the input you need to provide, the other "half" being the property you want to verify. Please consult our [guide to properties]({{ '/documentation/background/properties.html' | relative_url }}) for details on how to specify them. An extensive list of example models and properties is available at the [Quantitative Verification Benchmark Set](https://qcomp.org/benchmarks). @@ -32,4 +32,4 @@ An extensive list of example models and properties is available at the [Quantita Finally, if both the input model as well as the property are captured in an appropriate format, then you are ready to run Storm! -Our [guide](documentation/usage/running-storm.html) illustrates how you can do so. Since the calls (and even the binaries) you need to invoke depend on the input language for each of the input languages, the guide shows how to run Storm depending on the input you have. +Our [guide]({{ '/documentation/usage/running-storm.html' | relative_url }}) illustrates how you can do so. Since the calls (and even the binaries) you need to invoke depend on the input language for each of the input languages, the guide shows how to run Storm depending on the input you have.