Commit 9051e050 authored by Hans Vrapi's avatar Hans Vrapi
Browse files

add storm files

parent adc38ff7
---
Language: Cpp
# BasedOnStyle: Google
AccessModifierOffset: -1
AlignAfterOpenBracket: Align
AlignConsecutiveMacros: false
AlignConsecutiveAssignments: false
AlignConsecutiveBitFields: false
AlignConsecutiveDeclarations: false
AlignEscapedNewlines: Left
AlignOperands: Align
AlignTrailingComments: true
AllowAllArgumentsOnNextLine: true
AllowAllConstructorInitializersOnNextLine: true
AllowAllParametersOfDeclarationOnNextLine: true
AllowShortEnumsOnASingleLine: true
AllowShortBlocksOnASingleLine: Never
AllowShortCaseLabelsOnASingleLine: false
AllowShortFunctionsOnASingleLine: All
AllowShortLambdasOnASingleLine: All
AllowShortIfStatementsOnASingleLine: WithoutElse
AllowShortLoopsOnASingleLine: true
AlwaysBreakAfterDefinitionReturnType: None
AlwaysBreakAfterReturnType: None
AlwaysBreakBeforeMultilineStrings: true
AlwaysBreakTemplateDeclarations: Yes
BinPackArguments: true
BinPackParameters: true
BraceWrapping:
AfterCaseLabel: false
AfterClass: false
AfterControlStatement: Never
AfterEnum: false
AfterFunction: false
AfterNamespace: false
AfterObjCDeclaration: false
AfterStruct: false
AfterUnion: false
AfterExternBlock: false
BeforeCatch: false
BeforeElse: false
BeforeLambdaBody: false
BeforeWhile: false
IndentBraces: false
SplitEmptyFunction: true
SplitEmptyRecord: true
SplitEmptyNamespace: true
BreakBeforeBinaryOperators: None
BreakBeforeBraces: Attach
BreakBeforeInheritanceComma: false
BreakInheritanceList: BeforeColon
BreakBeforeTernaryOperators: true
BreakConstructorInitializersBeforeComma: false
BreakConstructorInitializers: BeforeColon
BreakAfterJavaFieldAnnotations: false
BreakStringLiterals: true
ColumnLimit: 160
CompactNamespaces: false
ConstructorInitializerAllOnOneLineOrOnePerLine: true
ConstructorInitializerIndentWidth: 4
ContinuationIndentWidth: 4
Cpp11BracedListStyle: true
DeriveLineEnding: true
DerivePointerAlignment: true
DisableFormat: false
ExperimentalAutoDetectBinPacking: false
FixNamespaceComments: true
ForEachMacros:
- foreach
- Q_FOREACH
- BOOST_FOREACH
IncludeBlocks: Preserve
IncludeCategories:
- Regex: '^<storm/.*\.h>'
Priority: 2
SortPriority: 0
- Regex: '^<.*\.h>'
Priority: 1
SortPriority: 0
- Regex: '^<.*'
Priority: 2
SortPriority: 0
- Regex: '.*'
Priority: 3
SortPriority: 0
IncludeIsMainRegex: '([-_](test|unittest))?$'
IncludeIsMainSourceRegex: ''
IndentCaseLabels: true
IndentCaseBlocks: false
IndentGotoLabels: true
IndentPPDirectives: None
IndentExternBlock: AfterExternBlock
IndentWidth: 4
IndentWrappedFunctionNames: false
InsertTrailingCommas: None
JavaScriptQuotes: Leave
JavaScriptWrapImports: true
KeepEmptyLinesAtTheStartOfBlocks: false
MacroBlockBegin: ''
MacroBlockEnd: ''
MaxEmptyLinesToKeep: 1
NamespaceIndentation: None
PenaltyBreakAssignment: 2
PenaltyBreakBeforeFirstCallParameter: 1
PenaltyBreakComment: 300
PenaltyBreakFirstLessLess: 120
PenaltyBreakString: 1000
PenaltyBreakTemplateDeclaration: 10
PenaltyExcessCharacter: 1000000
PenaltyReturnTypeOnItsOwnLine: 200
PointerAlignment: Left
RawStringFormats:
- Language: Cpp
Delimiters:
- cc
- CC
- cpp
- Cpp
- CPP
- 'c++'
- 'C++'
CanonicalDelimiter: ''
BasedOnStyle: google
ReflowComments: true
SortIncludes: true
SortUsingDeclarations: true
SpaceAfterCStyleCast: false
SpaceAfterLogicalNot: false
SpaceAfterTemplateKeyword: false
SpaceBeforeAssignmentOperators: true
SpaceBeforeCpp11BracedList: false
SpaceBeforeCtorInitializerColon: true
SpaceBeforeInheritanceColon: true
SpaceBeforeParens: ControlStatements
SpaceBeforeRangeBasedForLoopColon: true
SpaceInEmptyBlock: false
SpaceInEmptyParentheses: false
SpacesBeforeTrailingComments: 2
SpacesInAngles: false
SpacesInConditionalStatement: false
SpacesInContainerLiterals: true
SpacesInCStyleCastParentheses: false
SpacesInParentheses: false
SpacesInSquareBrackets: false
SpaceBeforeSquareBrackets: false
Standard: c++14
TabWidth: 4
UseCRLF: false
UseTab: Never
WhitespaceSensitiveMacros:
- STRINGIZE
- PP_STRINGIZE
- BOOST_PP_STRINGIZE
...
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:
CARL_BRANCH: "master14"
CARL_GIT_URL: "https://github.com/smtrat/carl.git"
STORM_GIT_URL: "${{ github.server_url }}/${{ github.repository }}.git"
STORM_BRANCH: "${{ github.ref }}"
# github runners currently have two cores
NR_JOBS: "2"
# cmake arguments
CMAKE_DEBUG: "-DCMAKE_BUILD_TYPE=Debug -DSTORM_DEVELOPER=ON -DSTORM_PORTABLE=ON"
CMAKE_RELEASE: "-DCMAKE_BUILD_TYPE=Release -DSTORM_DEVELOPER=OFF -DSTORM_PORTABLE=ON"
CARL_CMAKE_DEBUG: "-DCMAKE_BUILD_TYPE=Debug -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON -DTHREAD_SAFE=ON -DBUILD_ADDONS=ON -DBUILD_ADDON_PARSER=ON"
CARL_CMAKE_RELEASE: "-DCMAKE_BUILD_TYPE=Release -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON -DTHREAD_SAFE=ON -DBUILD_ADDONS=ON -DBUILD_ADDON_PARSER=ON"
jobs:
noDeploy:
name: Build and Test
runs-on: ubuntu-latest
strategy:
matrix:
distro: ["ubuntu-18.04", "debian-10", "debian-9", "ubuntu-20.04"]
debugOrRelease: ["debug", "release"]
steps:
- name: Setup cmake arguments
# this is strangely the best way to implement environment variables based on the value of another
# GITHUB_ENV is a magic variable pointing to a file; if a line with format {NAME}={VALUE}
# then the env variable with name NAME will be created/updated with VALUE
run: |
([[ ${{ matrix.debugOrRelease }} == "debug" ]] && echo "CMAKE_ARGS=${CMAKE_DEBUG}" || echo "CMAKE_ARGS=${CMAKE_RELEASE}") >> $GITHUB_ENV
- name: Init Docker
run: sudo docker run -d -it --name storm --privileged movesrwth/storm-basesystem:${{ matrix.distro }}
- name: Git clone
# git clone cannot clone individual commits based on a sha and some other refs
# this workaround fixes this and fetches only one commit
run: |
sudo docker exec storm bash -c "mkdir /opt/storm; cd /opt/storm; git init && git remote add origin ${STORM_GIT_URL} && git fetch --depth 1 origin ${STORM_BRANCH} && git checkout FETCH_HEAD"
- name: Run cmake
run: sudo docker exec storm bash -c "mkdir /opt/storm/build; cd /opt/storm/build; cmake .. ${CMAKE_ARGS}"
- name: Build storm
run: sudo docker exec storm bash -c "cd /opt/storm/build; make -j ${NR_JOBS}"
# A bit hacky... but its usefullnes has been proven in production
- name: Check release makeflags
if: matrix.debugOrRelease == 'release'
run: |
sudo docker exec storm bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -O3' || (echo \"Error: Missing flag \'-O3\' for release build.\" && false)"
sudo docker exec storm bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -DNDEBUG' || (echo \"Error: Missing flag \'-DNDEBUG\' for release build.\" && false)"
- name: Check debug makeflags
if: matrix.debugOrRelease == 'debug'
run: |
sudo docker exec storm bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -g' || (echo \"Error: Missing flag \'-g\' for debug build.\" && false)"
- name: Run unit tests
run: sudo docker exec storm bash -c "cd /opt/storm/build; ctest test --output-on-failure"
deploy:
name: Build, Test and Deploy
runs-on: ubuntu-latest
env:
DISTRO: "ubuntu-20.10"
strategy:
matrix:
debugOrRelease: ["debug", "release"]
steps:
- name: Setup cmake arguments
# this is strangely the best way to implement environment variables based on the value of another
# GITHUB_ENV is a magic variable pointing to a file; if a line with format {NAME}={VALUE}
# then the env variable with name NAME will be created/updated with VALUE
run: |
([[ ${{ matrix.debugOrRelease }} == "debug" ]] && echo "CMAKE_ARGS=${CMAKE_DEBUG}" || echo "CMAKE_ARGS=${CMAKE_RELEASE}") >> $GITHUB_ENV
([[ ${{ matrix.debugOrRelease }} == "debug" ]] && echo "CARL_CMAKE_ARGS=${CARL_CMAKE_DEBUG}" || echo "CARL_CMAKE_ARGS=${CARL_CMAKE_RELEASE}") >> $GITHUB_ENV
- name: Login into docker
# Only login if using master on original repo (and not for pull requests or forks)
if: github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master'
run: echo "${{ secrets.STORM_CI_DOCKER_PASSWORD }}" | sudo docker login -u "${{ secrets.STORM_CI_DOCKER_USERNAME }}" --password-stdin
- name: Init Docker
run: sudo docker run -d -it --name storm --privileged movesrwth/storm-basesystem:${DISTRO}
#####
# Build & DEPLOY CARL
#####
# We should not do partial updates :/
# but we need to install some dependencies
# Surely we can find a better way to do this at some point
- name: Update base system
run: |
sudo docker exec storm apt-get update
sudo docker exec storm apt-get upgrade -qqy
- name: install dependencies
run: sudo docker exec storm apt-get install -qq -y uuid-dev pkg-config
- name: Git clone carl
run: sudo docker exec storm git clone --depth 1 --branch $CARL_BRANCH $CARL_GIT_URL /opt/carl
- name: Run cmake for carl
run: sudo docker exec storm bash -c "mkdir /opt/carl/build; cd /opt/carl/build; cmake .. ${CARL_CMAKE_ARGS}"
- name: Build carl
run: sudo docker exec storm bash -c "cd /opt/carl/build; make lib_carl -j ${NR_JOBS}"
- name: Deploy carl
# Only deploy if using master on original repo (and not for pull requests or forks)
if: github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master'
run: |
sudo docker commit storm movesrwth/carl:ci-${{ matrix.debugOrRelease }}
sudo docker push movesrwth/carl:ci-${{ matrix.debugOrRelease }}
#####
# Build & TEST & DEPLOY STORM
#####
- name: Git shallow clone
# Only clone shallow if not using master on original repo (and not for pull requests or forks)
if: ${{ !(github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master') }}
run: |
# git clone cannot clone individual commits based on a sha and some other refs
sudo docker exec storm bash -c "mkdir /opt/storm; cd /opt/storm; git init && git remote add origin ${STORM_GIT_URL} && git fetch --depth 1 origin ${STORM_BRANCH} && git checkout FETCH_HEAD"
- name: Git deep clone
# needed for versioning for now on deployment
if: github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master'
run: |
sudo docker exec storm git clone --branch master $STORM_GIT_URL /opt/storm
- name: Run cmake
run: sudo docker exec storm bash -c "mkdir /opt/storm/build; cd /opt/storm/build; cmake .. ${CMAKE_ARGS}"
- name: Build storm
run: sudo docker exec storm bash -c "cd /opt/storm/build; make -j ${NR_JOBS}"
# A bit hacky... but its usefulness has been proven in production
- name: Check release makeflags
if: matrix.debugOrRelease == 'release'
run: |
sudo docker exec storm bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -O3' || (echo \"Error: Missing flag \'-O3\' for release build.\" && false)"
sudo docker exec storm bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -DNDEBUG' || (echo \"Error: Missing flag \'-DNDEBUG\' for release build.\" && false)"
- name: Check debug makeflags
if: matrix.debugOrRelease == 'debug'
run: |
sudo docker exec storm bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -g' || (echo \"Error: Missing flag \'-g\' for debug build.\" && false)"
- name: Run unit tests
run: sudo docker exec storm bash -c "cd /opt/storm/build; ctest test --output-on-failure"
- name: Deploy storm
# Only deploy if using master on original repo (and not for pull requests or forks)
if: github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master'
run: |
sudo docker commit storm movesrwth/storm:ci-${{ matrix.debugOrRelease }}
sudo docker push movesrwth/storm:ci-${{ matrix.debugOrRelease }}
notify:
name: Email notification
runs-on: ubuntu-latest
needs: [noDeploy, deploy]
# Only run in main repo and even if previous step failed
if: github.repository_owner == 'moves-rwth' && always()
steps:
- uses: technote-space/workflow-conclusion-action@v2
- uses: dawidd6/action-send-mail@v2
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 <you-broke-it@stormchecker.org>
if: env.WORKFLOW_CONCLUSION != 'success' # notify only if failure
name: Doxygen
# Builds and deploys storms doxygen documentation
on:
schedule:
# run daily
- cron: '0 8 * * *'
# needed to trigger the workflow manually
workflow_dispatch:
env:
BASE_IMG: "movesrwth/carl:ci-release"
STORM_GIT_URL: "${{ github.server_url }}/${{ github.repository }}.git"
STORM_BRANCH: "master"
# github runners currently have two cores
NR_JOBS: "2"
jobs:
deploy:
name: Create documentation
runs-on: ubuntu-latest
# Do not run on forks
if: github.repository_owner == 'moves-rwth'
steps:
- name: Init Docker
run: sudo docker run -d -it --name storm --privileged ${BASE_IMG}
# We should not do partial updates :/
# but we need to install some dependencies
# Surely we can find a better way to do this at some point
- name: Update base system
run: |
sudo docker exec storm apt-get update
sudo docker exec storm apt-get upgrade -qqy
- name: install dependencies
run: sudo docker exec storm apt-get install -qq -y doxygen graphviz
- name: Git clone storm
run: sudo docker exec storm git clone --depth 1 --branch $STORM_BRANCH $STORM_GIT_URL /opt/storm
- name: Run cmake
run: sudo docker exec storm bash -c "mkdir /opt/storm/build; cd /opt/storm/build; cmake .."
- name: Build doxygen
run: sudo docker exec storm bash -c "cd /opt/storm/build; make doc -j ${NR_JOBS}"
- name: Copy doxygen
run: sudo docker cp storm:/opt/storm/build/doc/html .
- name: Deploy doxygen
uses: peaceiris/actions-gh-pages@v3
with:
deploy_key: ${{ secrets.DOC_DEPLOY_KEY }}
publish_dir: ./html
external_repository: moves-rwth/storm-doc
publish_branch: master
force_orphan: true
notify:
name: Email notification
runs-on: ubuntu-latest
needs: [deploy]
# Only run in main repo and even if previous step failed
if: github.repository_owner == 'moves-rwth' && always()
steps:
- uses: technote-space/workflow-conclusion-action@v2
- uses: dawidd6/action-send-mail@v2
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] Doxygen generation 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 <you-broke-it@stormchecker.org>
if: env.WORKFLOW_CONCLUSION != 'success' # notify only if failure
##Third-Party libs
resources/3rdparty/l3pp/.git/
resources/3rdparty/gtest-1.7.0/
resources/3rdparty/gmm-5.2/
resources/3rdparty/cudd-3.0.0/
resources/3rdparty/xercesc-3.1.2/
#Visual Studio files
*.[Oo]bj
*.user
*.aps
*.pch
*.vspscc
*.vssscc
*_i.c
*_p.c
*.ncb
*.suo
*.tlb
*.tlh
*.bak
*.[Cc]ache
*.ilk
*.log
*.lib
*.sbr
*.sdf
*.tlog
*.lastbuildstate
*.pdb
*.idb
*.opensdf
*.unsuccessfulbuild
ipch/
obj/
CMakeFiles/
CPackConfig.cmake
# The build Dir
/*build*/
build//CMakeLists.txt
/*.vcxproj
/*.filters
/*.sln
#Temp texteditor files
*.orig
*.*~
nbproject/
.DS_Store
.idea
.vscode
*.out
resources/3rdparty/cudd-3.0.0/Makefile.in
resources/3rdparty/cudd-3.0.0/aclocal.m4
Changelog
==============
This changelog lists only the most important changes. Smaller (bug)fixes as well as non-mature features are not part of the changelog.
The releases of major and minor versions contain an overview of changes since the last major/minor update.
Version 1.6.x
-------------
## Version 1.6.4 (20xx/xx)
- Added support for PRISM models that use unbounded integer variables.
- Added an export of check results to json. Use `--exportresult` in the command line interface.
- Added computation of steady state probabilities for DTMC/CTMC in the sparse engine. Use `--steadystate` in the command line interface.
- Implemented parsing and model building of Stochastic multiplayer games (SMGs) in the PRISM language. No model checking implemented, for now.
- Added support for continuous integration with Github Actions.
- `storm-pars`: Exploit monotonicity for computing extremal values and parameter space partitioning.
## Version 1.6.3 (2020/11)
- Added support for multi-objective model checking of long-run average objectives including mixtures with other kinds of objectives.
- Added support for generating optimal schedulers for globally formulae.
- Simulator supports exact arithmetic.
- Added switch `--no-simplify` to disable simplification of PRISM programs (which sometimes costs a bit of time on extremely large inputs).
- Fixed issues with JANI inputs concerning .
- transient variable expressions in properties,
- constants in properties, and
- integer variables with either only an upper or only a lower bound.
- `storm-pomdp`: States can be labelled with values for observable predicates.
- `storm-pomdp`: (Only API) Track state estimates.
- `storm-pomdp`: (Only API) Reduce computation of state estimates to computation on unrolled MDP.
## Version 1.6.2 (2020/09)
- Prism program simplification improved.
- Revamped implementation of long-run-average algorithms, including scheduler export for LRA properties on Markov automata.
- Support for step-bounded properties of the form ... [F[x,y] ... ] for DTMCs and MDPs (sparse engine).
- Renamed portfolio engine to automatic
- `storm-dft`: Fix for relevant events when using symmetry reduction.
- `storm-pomdp`: Fix for --transformsimple and --transformbinary when used with until formulae.
- `storm-pomdp`: POMDPs can be parametric as well.
## Version 1.6.0 (2020/06)
- Changed default Dd library from `cudd` to `sylvan`. The Dd library can be changed back to `cudd` using the command line switch `--ddlib`.
- Scheduler export: Properly handle models with end components. Added export in `.json` format.
- CMake: Search for Gurobi prefers new versions.
- CMake: We no longer ship xerces-c. If xerces-c is not found on the system, storm-gspn will not be able to parse xml-based GSPN formats.
- CMake: Added option `STORM_LOAD_QVBS` to automatically download the quantitative verification benchmark set.
- Eigen library: The source code of Eigen is no longer included but downloaded from an external repository instead. Incremented Eigen version to 3.3.7 which fixes a compilation issue with recent XCode versions.
- Tests: Enabled tests for permissive schedulers.
- `storm-counterexamples`: fix when computing multiple counterexamples in debug mode.
- `storm-dft`: Renamed setting `--show-dft-stats` to `dft-statistics` and added approximation information to statistics.
- `storm-pomdp`: Implemented approximation algorithms that explore (a discritization of) the belief MDP, allowing to compute safe lower- and upper bounds for a given property.
- `storm-pomdp`: Implemented almost-sure reachability computations: graph-based, one-shot SAT-based, and iterative SAT-based.
- `storm-pomdp': Various changes such that transformation to pMCs is now again supported (and improved).
- Fixed several compiler warnings.
Version 1.5.x
-------------
## Version 1.5.1 (2020/03)
- Jani models are now parsed using exact arithmetic.
## Version 1.5.0 (2020/03)
- Added portfolio engine which picks a good engine (among other settings) based on features of the symbolic input.
- Abort of Storm (via timeout or CTRL+C for example) is now gracefully handled. After an abort signal the program waits some seconds to output the result computed so far and terminates afterwards. A second signal immediately terminates the program.
- Setting `--engine dd-to-sparse --bisimulation` now triggers extracting the sparse bisimulation quotient.
- JIT model building is now invoked via `--engine jit` (instead of `--jit`).
- DRN: support import of choice labelling.
- Added option `--build:buildchoiceorig` to build a model (PRISM or JANI) with choice origins (which are exported with, e.g. `--exportscheduler`).
- Implemented optimistic value iteration for sound computations and set it as new default in `--sound` mode.
- Time bounded properties for Markov automata are now computed with relative precision. Use `--absolute` for the previous behavior.
- Apply the maximum progress assumption while building a Markov automaton with one of the symbolic engines.
- Added option `--build:nomaxprog` to disable applying the maximum progress assumption during model building (for Markov Automata).
- Added hybrid engine for Markov Automata.
- Improved performance of the Unif+ algorithm (used for time-bounded properties on Markov Automata).
- Various performance improvements for model building with the sparse engine.
- `storm-dft`: Symmetry reduction is now enabled by default and can be disabled via `--nosymmetryreduction`.
- `storm-pomdp`: Only accept POMDPs that are canonical.
- `storm-pomdp`: Prism language extended with observable expressions.
- `storm-pomdp`: Various fixes that prevented usage.
- Several bug fixes.
Version 1.4.x
-------------
### Version 1.4.1 (2019/12)
- Implemented long run average (LRA) computation for DTMCs/CTMCs via value iteration and via gain/bias equations.
- Added several LRA related settings in a new settings module. Note that `--minmax:lramethod` has been replaced by `--lra:nondetmethod`.
### Version 1.4.0 (2019/11)
- Added support for multi-dimensional quantile queries.
- Added support for multi-objective model checking under pure (deterministic) schedulers with bounded memory using `--purescheds`.
- Allow to quickly check a benchmark from the [Quantitative Verification Benchmark Set](http://qcomp.org/benchmarks/) using the `--qvbs` option.
- Added script `resources/examples/download_qvbs.sh` to download the QVBS.
- If an option is unknown, Storm now suggests similar option names.
- Flagged several options as 'advanced' to clean up the `--help`-message. Use `--help all` to display a complete list of options.
- Support for parsing of exact time bounds for properties, e.g., `P=? [F=27 "goal"]`.
- Export of optimal schedulers when checking MDPs with the sparse engine (experimental). Use `--exportscheduler <filename>`.
- PRISM language: Support for the new `round` operator.
- PRISM language: Improved error messages of the parser.
- JANI: Allow bounded types for constants.
- JANI: Support for non-trivial reward accumulations.
- JANI: Fixed support for reward expressions over non-transient variables.
- DRN: Added support for exact parsing and action-based rewards.
- DRN: Support for placeholder variables which allows to parse recurring rational functions only once.
- Fixed sparse bisimulation of MDPs (which failed if all non-absorbing states in the quotient are initial).
- Support for export of MTBDDs from Storm.
- Support for k-shortest path counterexamples (arguments `-cex --cextype shortestpath`)
- New settings module `transformation` for Markov chain transformations. Use `--help transformation` to get a list of available transformations.
- Support for eliminating chains of Non-Markovian states in MAs via `--eliminate-chains`.
- Export to dot format allows for maximal line width in states (argument `--dot-maxwidth <width>`)
- `storm-conv` can now apply transformations on a prism file.
- `storm-pars`: Enabled building, bisimulation and analysis of symbolic models.
- `storm-dft`: Support partial-order for state space generation.
- `storm-dft`: Compute lower and upper bounds for number of BE failures via SMT.
- `storm-dft`: Allow to set relevant events which are not set to Don't Care.
- `storm-dft`: Support for constant failed BEs. Use flag `--uniquefailedbe` to create a unique constant failed BE.
- `storm-dft`: Support for probabilistic BEs via PDEPs.
- Fixed linking with Mathsat on macOS.
- Fixed linking with IntelTBB for GCC.
- Fixed compilation for macOS Mojave and higher.
- Several bug fixes.
Version 1.3.x
-------------
## Version 1.3.0 (2018/12)
- Slightly improved scheduler extraction
- Environments are now part of the c++ API
- Heavily extended JANI support, in particular:
* arrays, functions, state-exit-rewards (all engines)
* indexed assignments, complex reward expressions (sparse engine)
* several jani-related bug fixes
- New binary `storm-conv` that handles conversions between model files
- New binary `storm-pomdp` that handles the translation of POMDPs to pMCs.
- Maximal progress assumption is now applied while building Markov Automata (sparse engine).