v1.9.0

Requires Storm version >= 1.9.0 and pycarl version >= 2.3.0

• Support for computing steady-state distributions
• Support for quantitative POMDP analysis
• Support for interval-based models
• Extended ADD support
• Support for all-in-one MDP
• Bindings for Smg and GameFormula
• Build parametric models from model components
• Improved access to state valuations, choice labels and choice origins
• Adaption to changes in Storm such as DFT simulator
• Developer: improved build process

v1.8.0

Requires Storm version >= 1.8.0 and pycarl version >= 2.2.0

• Scheduler extraction for exact models
• Adaption to changes in Storm such as the removal of JIT compilation and changes in storm-pomdp
• Added bindings for DFT modules
• Developer: improved build process
• Developer: updated pybind version to 2.10.0. Check compatibility to pybind version of pycarl

v1.7.0

Requires Storm version >= 1.7.0 and pycarl version >= 2.1.0

• Support for plotting via extras plot
• Support for LTL model checking via Spot
• Some support for multi-objective model checking queries
• Bindings for maximal end components
• Support for computing expected number of visits
• Added accessors for Prism program
• Added documentation for simulator
• Support for building complete/partial state space of DFT
• Instantiator for parametric DFT
• Simulator for DFT
• Added Dockerfile
• Developer: stormpy is built with C++17
• Developer: updated pybind11 to version 2.8.1 and adapted bindings accordingly
• Adaption to changes in Storm such as the new namespace storm::dft

v1.6.4

Requires Storm version >= 1.6.4 and pycarl version >= 2.0.5

• Simulator for sparse models updated, added simulator for prism programs.
• Renamed PrismProgram::isDeterministicModel -> is_deterministic_model for consistency
• Support for specifying the returned quotient format (symbolic or sparse) for symbolic bisimulation
• Added support for continuous integration with Github Actions
• Updated bindings for, e.g., Jani to reflect changes in Storm
• Bindings for end component elimination

v1.6.3

Requires Storm version >= 1.6.3 and pycarl version >= 2.0.4

• Documentation is largely based on Jupyter notebooks now and supports launch with Binder
• Support for exact arithmetic in models
• Support for timeouts/signal handlers in Storm
• Code for parametric/exact/floating-point models data structures unified
• Extended support for Prism and Jani data structures
• export_parametric_to_drn no longer exists, use export_to_drn instead

v1.6.2

Requires Storm version >= 1.6.2 and pycarl version >= 2.0.4

• Adaptions to changes in Storm
• Create models (DTMC, MDP, CTMC, MA) directly from model components. Support creation of transition matrix, labeling, reward models, etc.
• Explicit State Lookup: Finding a state based on the variable values
• Support for pPOMDPs
• (p)POMDPs: Support for unfolding memory, making POMDPs simple, and exporting POMDP to a pMC
• Export to DRN options to support exporting without placeholders
• Renamed preprocess_prism_program to preprocess_symbolic_input
• Bindings for storm-dft. Most notably transformations, symmetries and relevant events

v1.6.0

Requires Storm version >= 1.6.0 and pycarl version >= 2.0.4

• Adaptions to changes in Storm: most notably state valuations
• Support for GSPNs: parsing, exploring, building
• Support for matrix building
• Extended expression operators with {conjunction, disjunction}
• Added information collector to extract information from jani models
• Bindings for elimination of chains of non-Markovian states

v1.4.1

Requires Storm version >= 1.4.1 and pycarl version >= 2.0.4

• Adaptions to changes in Storm
• Extended simple accessors such as parse_properties, model_checking, to handle variety of inputs.
• Added and extended environments
• Changed constructor of ParameterRegion to take a valuation instead of string.
  Use ParameterRegion.create_from_string() to create a region from string.
• Added InstantiationModelChecker for pMDPs and allow instations with rational numbers
• Added transformation of CTMCs to DTMCs
• Further bindings for Prism Programs and their preprocessing
• SettingsManager updated
• Allow building models annotated with valuations
• A custom state exploration that allows to explore successor states of a prism program
• Extended documentation, in particular examples.
• Fix for compilation with Xcode 11

v1.3.0

Requires Storm version >= 1.3.0 and pycarl version >= 2.0.3

• Adaptions to changes in Storm
• Bindings for symbolic models:
  • building symbolic models
  • bisimulation
  • transforming symbolic to sparse models
• Extraction of schedulers and queries on schedulers
• High-level counterexamples connected
• Drastically extended JANI bindings
• Extended bindings for expressions
• Extended PLA bindings
• Extended DFT bindings
• Extended documentation
• Improved and extended setup

v1.2.0

Requires Storm version >= 1.2.0 and pycarl version >= 2.0.2

• Adaptions to changes in Storm
• Bindings for simplification of parametric models
• Handling of rewards
• Building of model with all labels if no formula is given
• Support for submatrix()
• Extended documentation
• Extended build script