Stormpy

https://github.com/stormchecker/stormpy
Admin
Stormpy provides Python bindings for Storm, a probabilistic model checker, enabling users to work...
Tokens:24,299
Snippets:297
Trust Score:6.6
Update:6 months ago
Show doc for...
Tokens:
Raw
### Install documentation dependencies

Source: https://github.com/stormchecker/stormpy/blob/master/doc/build_website.md

Install the necessary packages to build the documentation from the project root.

```console
pip install .[doc]
```

--------------------------------

### Install documentation dependencies

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/installation.md

Command to install the necessary Python packages for building the documentation.

```bash
pip install .[doc,numpy]
```

--------------------------------

### Initialize MDP Model

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/simulator.ipynb

Setup an MDP model for simulation with nondeterministic choices.

```python
import random

random.seed(23)
path = stormpy.examples.files.prism_mdp_slipgrid
prism_program = stormpy.parse_prism_program(path)

model = stormpy.build_model(prism_program)
simulator = stormpy.simulator.create_simulator(model, seed=42)
```

--------------------------------

### Test stormpy installation

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/installation.md

Commands to install the testing framework and execute the test suite.

```bash
pip install pytest
py.test tests/
```

--------------------------------

### Build stormpy from source

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/installation.md

Install the package from the local directory after cloning.

```bash
pip install -v .
```

--------------------------------

### Install stormpy via pip

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/installation.md

Standard installation method for the stormpy package.

```bash
pip install stormpy
```

--------------------------------

### Import Stormpy Examples

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/building_models.ipynb

Imports necessary modules from the stormpy library for accessing examples and files.

```python
import stormpy.examples
import stormpy.examples.files
```

--------------------------------

### Import StormPy Libraries

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/simulator.ipynb

Import necessary libraries for using StormPy simulators and examples. This is a common setup for StormPy functionalities.

```python
import stormpy
import stormpy.examples
import stormpy.examples.files
import stormpy.simulator
```

--------------------------------

### Parse and Build MDP Model

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/exploration.ipynb

Parses a PRISM program for an MDP and builds the corresponding model. Requires stormpy and its examples module.

```python
import doctest

doctest.ELLIPSIS_MARKER = "-etc-"
import stormpy
import stormpy.examples
import stormpy.examples.files

program = stormpy.parse_prism_program(stormpy.examples.files.prism_mdp_maze)
prop = 'R=? [F "goal"]'

properties = stormpy.parse_properties_for_prism_program(prop, program, None)
model = stormpy.build_model(program, properties)
```

--------------------------------

### Simulate MDP with Explicit Action Selection

Source: https://context7.com/stormchecker/stormpy/llms.txt

Simulate Markov Decision Processes (MDPs) by explicitly selecting actions at each nondeterministic choice point. This example demonstrates setting action mode to GLOBAL_NAMES and observing program-level states.

```python
import stormpy
import stormpy.simulator
import stormpy.examples
import stormpy.examples.files
import random

random.seed(42)

# Build MDP with action labels
path = stormpy.examples.files.prism_mdp_slipgrid
prism_program = stormpy.parse_prism_program(path)

options = stormpy.BuilderOptions()
options.set_build_choice_labels()
options.set_build_state_valuations()
model = stormpy.build_sparse_model_with_options(prism_program, options)

# Create simulator with named actions
simulator = stormpy.simulator.create_simulator(model, seed=42)
simulator.set_action_mode(stormpy.simulator.SimulatorActionMode.GLOBAL_NAMES)
simulator.set_observation_mode(stormpy.simulator.SimulatorObservationMode.PROGRAM_LEVEL)

# Simulate a path with random action selection
state, reward, labels = simulator.restart()
path = [f"({state['x']},{state['y']})"]

for _ in range(20):
    actions = simulator.available_actions()
    selected = random.choice(actions)
    path.append(f"--{selected}-->")
    state, reward, labels = simulator.step(selected)
    path.append(f"({state['x']},{state['y']})")
    if simulator.is_done():
        break

print(" ".join(path))
```

--------------------------------

### Configure Model Checking Algorithms

Source: https://context7.com/stormchecker/stormpy/llms.txt

Customize the model checking environment to select specific solvers and algorithm parameters. This example configures the linear equation solver for a DTMC model.

```python
import stormpy
import stormpy.examples
import stormpy.examples.files

# Build model
path = stormpy.examples.files.prism_dtmc_die
prism_program = stormpy.parse_prism_program(path)
formula_str = "P=? [F s=7 & d=2]"
properties = stormpy.parse_properties(formula_str, prism_program)
model = stormpy.build_model(prism_program, properties)

# Create custom environment
env = stormpy.Environment()

# Set linear equation solver type
env.solver_environment.set_linear_equation_solver_type(
    stormpy.EquationSolverType.native
)

# Configure solver method
env.solver_environment.native_solver_environment.method = \
    stormpy.NativeLinearEquationSolverMethod.power_iteration

# Set iteration limit
env.solver_environment.native_solver_environment.maximum_iterations = 1000

# Model check with custom environment
result = stormpy.model_checking(model, properties[0], environment=env)
initial_state = model.initial_states[0]
print(f"Result: {result.at(initial_state)}")
```

--------------------------------

### Parse and Build POMDP Model

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/exploration.ipynb

Parses a PRISM program for a POMDP and builds the corresponding model. Similar to MDP model building but uses a POMDP example file.

```python
import stormpy
import stormpy.examples
import stormpy.examples.files

program = stormpy.parse_prism_program(stormpy.examples.files.prism_pomdp_maze)
prop = 'R=? [F "goal"]'
properties = stormpy.parse_properties_for_prism_program(prop, program, None)
model = stormpy.build_model(program, properties)
```

--------------------------------

### Build General Module (CMake)

Source: https://github.com/stormchecker/stormpy/blob/master/CMakeLists.txt

A CMake helper function to build a general module, handling source files, includes, libraries, and installation.

```cmake
function(build_module MOD_NAME # Module name
                      OUT_DIR OUT_NAME # Output directory and name for library
                      MOD_FILE SOURCE_PATH # Module source file and regex for all module source files
                      ADDITIONAL_INCLUDES ADDITIONAL_LIBS) # Additional include directories and libraries
    file(GLOB_RECURSE "${MOD_NAME}_SOURCES" "${CMAKE_CURRENT_SOURCE_DIR}/src/${SOURCE_PATH}")
    pybind11_add_module(${MOD_NAME} "${CMAKE_CURRENT_SOURCE_DIR}/src/${MOD_FILE}" ${${MOD_NAME}_SOURCES})
    target_include_directories(${MOD_NAME} PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${ADDITIONAL_INCLUDES} ${CMAKE_CURRENT_BINARY_DIR}/src)
    target_link_libraries(${MOD_NAME} PRIVATE ${ADDITIONAL_LIBS})
    set_target_properties(${MOD_NAME} PROPERTIES LIBRARY_OUTPUT_DIRECTORY "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/${OUT_DIR}" OUTPUT_NAME "_${OUT_NAME}")
    install(TARGETS ${MOD_NAME} DESTINATION ${OUT_DIR})
endfunction(build_module)
```

--------------------------------

### Bisimulation Minimization

Source: https://context7.com/stormchecker/stormpy/llms.txt

Reduce model size while preserving properties using bisimulation quotient construction. This example performs strong bisimulation on a DTMC model and verifies a property on the reduced model.

```python
import stormpy
import stormpy.examples
import stormpy.examples.files

# Build model
path = stormpy.examples.files.prism_dtmc_die
prism_program = stormpy.parse_prism_program(path)
formula_str = "P=? [F s=7 & d=2]"
properties = stormpy.parse_properties(formula_str, prism_program)
model = stormpy.build_model(prism_program, properties)

print(f"Original model: {model.nr_states} states")

# Perform bisimulation (strong)
reduced_model = stormpy.perform_bisimulation(
    model,
    properties,
    stormpy.BisimulationType.STRONG
)

print(f"Reduced model: {reduced_model.nr_states} states")

# Verify property on reduced model
result = stormpy.model_checking(reduced_model, properties[0])
print(f"Result: {result.at(reduced_model.initial_states[0])}")
```

--------------------------------

### Build documentation

Source: https://github.com/stormchecker/stormpy/blob/master/doc/build_website.md

Navigate to the documentation directory and execute the build process.

```console
cd doc
make html
```

--------------------------------

### Create and activate a virtual environment

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/installation.md

Recommended practice to isolate project dependencies and Python versions.

```bash
python -m venv env
source env/bin/activate
```

--------------------------------

### Initialize Model for Shortest Path Analysis

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/shortest_paths.ipynb

Load a PRISM model from a file and build it using Stormpy.

```python
import stormpy.examples
import stormpy.examples.files

path = stormpy.examples.files.prism_dtmc_die
prism_program = stormpy.parse_prism_program(path)
model = stormpy.build_model(prism_program)
```

--------------------------------

### Initialize SparseMatrixBuilder

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/models/building_dtmcs.ipynb

Create a builder instance for constructing the transition matrix.

```python
builder = stormpy.SparseMatrixBuilder(rows=0, columns=0, entries=0, force_dimensions=False, has_custom_row_grouping=False)
```

--------------------------------

### Sample Multiple Paths

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/simulator.ipynb

Run the simulator multiple times to collect statistics on final state outcomes.

```python
simulator.restart()
final_outcomes = dict()
for n in range(100):
    while not simulator.is_done():
        observation, reward, labels = simulator.step()
    if observation not in final_outcomes:
        final_outcomes[observation] = 1
    else:
        final_outcomes[observation] += 1
    simulator.restart()
final_outcomes
```

--------------------------------

### Get Result for Initial State

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/getting_started.ipynb

Retrieves the result for the first initial state of a model. Ensure the result object is already computed.

```python
initial_state = model.initial_states[0]
print(result.at(initial_state))
```

--------------------------------

### Create a program-level simulator

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/simulator.ipynb

Initializes a simulator directly from a PRISM program without requiring the model to be built in memory.

```python
simulator = stormpy.simulator.create_simulator(prism_program, seed=42)
```

--------------------------------

### Configure Storm library from system

Source: https://github.com/stormchecker/stormpy/blob/master/CMakeLists.txt

Locates the Storm library on the system, verifies the minimum version, and configures optional libraries.

```cmake
if(ALLOW_STORM_SYSTEM)
    # Version should be synced with STORM_GIT_TAG in pyproject.toml
    set(STORM_MIN_VERSION "1.12.0")
    if (ALLOW_STORM_FETCH)
        find_package(storm HINTS ${STORM_DIR_HINT}) # NOT REQUIRED, can be fetched.
    else()
        find_package(storm REQUIRED HINTS ${STORM_DIR_HINT}) # REQUIRED, cannot be fetched.
    endif()
    if (storm_FOUND)
        check_hint("Storm" ${storm_DIR} "${STORM_DIR_HINT}" ${storm_VERSION})
        # Check Storm version
        if (${storm_VERSION} VERSION_LESS ${STORM_MIN_VERSION})
            MESSAGE(FATAL_ERROR "Stormpy - Storm version ${storm_VERSION} from ${storm_DIR} is not supported anymore!\nStormpy requires at least Storm version >= ${STORM_MIN_VERSION}.\nFor more information, see https://moves-rwth.github.io/stormpy/installation.html#compatibility-of-stormpy-and-storm")
        endif()
        if (STORM_VERSION_DEV)
            message(WARNING "Stormpy - Using a development version of Storm. This may lead to issues and we recommend using a release of Storm instead.")
        endif()

        set(STORM_FROM_SYSTEM TRUE)
        get_filename_component(STORM_DIR_PATH ${storm_DIR} ABSOLUTE)
        set(STORM_DIR "\"${STORM_DIR_PATH}\"")
        if (STORMPY_INFO_PRETEND_FETCH)
            # This is a workaround for our wheel construction which uses a system version for efficiency,
            # but should provide wheels as if it they were fetched.
            message(WARNING "Stormpy - The behavior of STORMPY_INFO_PRETEND_FETCH is something we only want when building wheels. Please ensure that STORM_GIT_REPO and STORM_GIT_TAG are set accordingly.")
            set(STORM_FETCHED_FROM_REPO ${STORM_GIT_REPO})
            set(STORM_FETCHED_FROM_TAG ${STORM_GIT_TAG})
            set(STORM_FROM_SYSTEM FALSE)
            set(STORM_DIR "None")
        endif()
        # Set dependency variables
        set_dependency_var(SPOT)
        set_dependency_var(XERCES)
        # Check for optional Storm libraries
        storm_with_lib(DFT)
        storm_with_lib(GSPN)
        storm_with_lib(PARS)
        storm_with_lib(POMDP)
    elseif (STORM_DIR_HINT)
        MESSAGE(FATAL_ERROR "Stormpy - Storm could not be found in ${STORM_DIR_HINT}.")
    endif()
endif()
```

--------------------------------

### Define Transitions for Remaining States

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/models/building_mdps.ipynb

Specify the starting rows for row groups and add transitions for the remaining states in the MDP. This ensures all states and their transitions are correctly defined.

```python
builder.new_row_group(2)
builder.add_next_value(2, 3, 0.5)
builder.add_next_value(2, 4, 0.5)
builder.new_row_group(3)
builder.add_next_value(3, 5, 0.5)
builder.add_next_value(3, 6, 0.5)
builder.new_row_group(4)
builder.add_next_value(4, 7, 0.5)
builder.add_next_value(4, 1, 0.5)
builder.new_row_group(5)
builder.add_next_value(5, 8, 0.5)
builder.add_next_value(5, 9, 0.5)
builder.new_row_group(6)
builder.add_next_value(6, 10, 0.5)
builder.add_next_value(6, 11, 0.5)
builder.new_row_group(7)
builder.add_next_value(7, 2, 0.5)
builder.add_next_value(7, 12, 0.5)
```

```python
for s in range(8, 14):
    builder.new_row_group(s)
    builder.add_next_value(s, s - 1, 1)
```

--------------------------------

### Initialize Sparse Model

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/engines.ipynb

Parses a PRISM program and builds a sparse model for analysis.

```python
import stormpy.examples
import stormpy.examples.files

prism_program = stormpy.parse_prism_program(stormpy.examples.files.prism_dtmc_die)
properties = stormpy.parse_properties('P=? [F "one"]', prism_program)
sparse_model = stormpy.build_sparse_model(prism_program, properties)
print(type(sparse_model))
```

--------------------------------

### Define Nondeterministic Transitions

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/models/building_mdps.ipynb

Define nondeterministic choices for a state by starting a new row group and adding transitions with associated probabilities. Each group represents a distinct action or choice.

```python
builder.new_row_group(0)
builder.add_next_value(0, 1, 0.5)
builder.add_next_value(0, 2, 0.5)
builder.add_next_value(1, 1, 0.2)
builder.add_next_value(1, 2, 0.8)
```

--------------------------------

### Fetch Storm library via FetchContent

Source: https://github.com/stormchecker/stormpy/blob/master/CMakeLists.txt

Downloads and builds Storm from a remote repository if it is not found on the system.

```cmake
if (NOT storm_FOUND)
    if (ALLOW_STORM_FETCH)
        if (STORMPY_INFO_PRETEND_FETCH)
            message(FATAL_ERROR "Stormpy - Do not set STORMPY_INFO_PRETEND_FETCH when fetching." )
        endif()
        # Storm not yet available.
        include(FetchContent)
        SET(FETCHCONTENT_QUIET OFF)
        SET(STORM_BUILD_EXECUTABLES OFF)
        SET(STORM_BUILD_TESTS OFF)
        FetchContent_Declare(
                storm
                GIT_REPOSITORY ${STORM_GIT_REPO}
                GIT_TAG        ${STORM_GIT_TAG}
        )
        FETCHCONTENT_MAKEAVAILABLE(storm)
        include(${storm_BINARY_DIR}/stormOptions.cmake)
        set(HAVE_STORM_DFT TRUE)
        set(HAVE_STORM_GSPN TRUE)
        set(HAVE_STORM_PARS TRUE)
        set(HAVE_STORM_POMDP TRUE)
        # Set dependency variables
        set_dependency_var(SPOT)
        set_dependency_var(XERCES)
        if (FETCHCONTENT_SOURCE_DIR_storm)
            # We are setting the Storm source to be something local from the outside.
            set(STORM_FETCHED_FROM_REPO ${FETCHCONTENT_SOURCE_DIR_storm})
            set(STORM_FETCHED_FROM_TAG "__local-source-dir__")
        else()
            set(STORM_FETCHED_FROM_REPO ${STORM_GIT_REPO})
            set(STORM_FETCHED_FROM_TAG ${STORM_GIT_TAG})
        endif()
        set(STORM_FROM_SYSTEM FALSE)
        set(STORM_DIR "None")
    else()
        # Should not be reachable because storm is required if we cannot fetch it.
        message(FATAL_ERROR "Stormpy - No version of Storm configured. This situation should not occur. Please contact the Storm developers.")
    endif()
endif()
```

--------------------------------

### Symbolic Model Checking with BDDs

Source: https://context7.com/stormchecker/stormpy/llms.txt

Build and analyze models using a symbolic (BDD-based) representation. This approach offers better scalability for structured models. The example checks a probabilistic property on a DTMC.

```python
import stormpy
import stormpy.examples
import stormpy.examples.files

# Parse program and properties
path = stormpy.examples.files.prism_dtmc_die
prism_program = stormpy.parse_prism_program(path)
formula_str = "P=? [F s=7 & d=2]"
properties = stormpy.parse_properties(formula_str, prism_program)

# Build symbolic model (uses BDDs)
model = stormpy.build_symbolic_model(prism_program, properties)

# Model check symbolically
result = stormpy.model_checking(model, properties[0])

# Filter result to initial states
filter = stormpy.create_filter_initial_states_symbolic(model)
result.filter(filter)

# For single initial state, min equals max
assert result.min == result.max
print(f"Result: {result.min}")
```

--------------------------------

### Import Stormpy Library

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/models/building_ctmcs.ipynb

Import the Stormpy library to begin using its functionalities for building Markov chains.

```python
import stormpy
```

--------------------------------

### Initialize State Labeling

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/models/building_dtmcs.ipynb

Create a state labeling object and register available labels.

```python
state_labeling = stormpy.storage.StateLabeling(13)

labels = {"init", "one", "two", "three", "four", "five", "six", "done", "deadlock"}
for label in labels:
    state_labeling.add_label(label)
```

--------------------------------

### Parse and Build a Reward Model

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/reward_models.ipynb

Initializes a model from a PRISM file and verifies the presence of a reward model.

```python
import stormpy
import stormpy.examples
import stormpy.examples.files

program = stormpy.parse_prism_program(stormpy.examples.files.prism_dtmc_die)
prop = 'R=? [F "done"]'

properties = stormpy.parse_properties(prop, program, None)
model = stormpy.build_model(program, properties)
assert len(model.reward_models) == 1
```

--------------------------------

### Initialize DTMC Model and Simulator

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/simulator.ipynb

Create a DTMC model from a PRISM file and initialize a simulator with a fixed seed.

```python
path = stormpy.examples.files.prism_dtmc_die
prism_program = stormpy.parse_prism_program(path)
model = stormpy.build_model(prism_program)

simulator = stormpy.simulator.create_simulator(model, seed=42)
```

--------------------------------

### Initialize SparseModelComponents

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/models/building_dtmcs.ipynb

Collects transition matrices, state labeling, and reward models into a single component object.

```python
components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models)
```

--------------------------------

### Initialize SparseMatrixBuilder for MDP

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/models/building_mdps.ipynb

Initialize a SparseMatrixBuilder with custom row grouping enabled to define nondeterministic transitions for an MDP.

```python
builder = stormpy.SparseMatrixBuilder(rows=0, columns=0, entries=0, force_dimensions=False, has_custom_row_grouping=True, row_groups=0)
```

--------------------------------

### Import ShortestPathsGenerator

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/shortest_paths.ipynb

Import the necessary utility class for path generation.

```python
from stormpy.utility import ShortestPathsGenerator
```

--------------------------------

### Parse JANI Model and Build

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/building_models.ipynb

Parses a JANI description file, extracts properties, and then builds the model. Prints the model type.

```python
path = stormpy.examples.files.jani_dtmc_die
jani_program, properties = stormpy.parse_jani_model(path)
model = stormpy.build_model(jani_program)
print(model.model_type)
```

--------------------------------

### Configure State and Choice Labeling

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/models/building_mas.ipynb

Initialize state and choice labeling objects and assign labels to specific states and choices.

```python
state_labeling = stormpy.storage.StateLabeling(5)
state_labels = {"init", "deadlock"}
for label in state_labels:
    state_labeling.add_label(label)
state_labeling.add_label_to_state("init", 0)

choice_labeling = stormpy.storage.ChoiceLabeling(6)
choice_labels = {"alpha", "beta"}
for label in choice_labels:
    choice_labeling.add_label(label)
choice_labeling.add_label_to_choice("alpha", 0)
choice_labeling.add_label_to_choice("beta", 1)
```

--------------------------------

### Build Transition Matrix

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/models/building_dtmcs.ipynb

Finalize the construction of the sparse matrix from the builder.

```python
transition_matrix = builder.build()
```

--------------------------------

### Build MDP Model for Scheduler Extraction

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/schedulers.ipynb

Builds a sparse MDP model from a PRISM program, enabling scheduler extraction. Ensure to set options for state valuations, choice labels, and choice origins.

```python
import stormpy
import stormpy.examples
import stormpy.examples.files

path = stormpy.examples.files.prism_mdp_coin_2_2
formula_str = 'Pmin=? [F "finished" & "all_coins_equal_1"]'
program = stormpy.parse_prism_program(path)
formulas = stormpy.parse_properties(formula_str, program)
options = stormpy.BuilderOptions(True, True)
options.set_build_state_valuations()
options.set_build_choice_labels()
options.set_build_with_choice_origins()
model = stormpy.build_sparse_model_with_options(program, options)
```

--------------------------------

### Build and Check Standard Model

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/analysis.ipynb

Builds a standard model from a PRISM program and properties, then performs model checking.

```python
model = stormpy.build_model(prism_program, properties)
result = stormpy.model_checking(model, properties[0])
```

--------------------------------

### Perform Simulator Steps

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/simulator.ipynb

Execute individual steps in the simulator to traverse the model.

```python
simulator.restart()
```

```python
simulator.step()
```

--------------------------------

### Initialize GSPN Builder

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/gspns.ipynb

Creates a new GSPN builder instance and sets the model name.

```python
builder = stormpy.gspn.GSPNBuilder()
builder.set_name("my_gspn")
```

--------------------------------

### Working with Reward Models in StormPy

Source: https://context7.com/stormchecker/stormpy/llms.txt

Import necessary StormPy modules for defining and querying reward structures for computing expected rewards and costs.

```python
import stormpy
import stormpy.examples
import stormpy.examples.files
```

--------------------------------

### Build Model with Symbolic State Valuations

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/simulator.ipynb

Configure builder options to enable symbolic state representations based on PRISM variables.

```python
options = stormpy.BuilderOptions()
options.set_build_state_valuations()
model = stormpy.build_sparse_model_with_options(prism_program, options)
```

--------------------------------

### Generate paths with program-level labels

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/simulator.ipynb

Configures the simulator to use global action names and program-level state valuations for more readable path output.

```python
options = stormpy.BuilderOptions()
options.set_build_choice_labels()
options.set_build_state_valuations()
model = stormpy.build_sparse_model_with_options(prism_program, options)
simulator = stormpy.simulator.create_simulator(model, seed=42)
simulator.set_action_mode(stormpy.simulator.SimulatorActionMode.GLOBAL_NAMES)
simulator.set_observation_mode(stormpy.simulator.SimulatorObservationMode.PROGRAM_LEVEL)
# 3 paths of at most 20 steps.
paths = []
for m in range(3):
    path = []
    state, reward, labels = simulator.restart()
    path = [f"({state['x']},{state['y']})"]
    for n in range(20):
        actions = simulator.available_actions()
        select_action = random.randint(0, len(actions) - 1)
        path.append(f"--{actions[select_action]}-->")
        state, reward, labels = simulator.step(actions[select_action])
        path.append(f"({state['x']},{state['y']})")
        if simulator.is_done():
            break
    paths.append(path)
for path in paths:
    print(" ".join(path))
```

--------------------------------

### Run Symbolic Simulation

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/simulator.ipynb

Execute simulation using symbolic state observations and print reward names.

```python
simulator.restart()
final_outcomes = dict()
print(simulator.get_reward_names())
for n in range(100):
    while not simulator.is_done():
        observation, reward, labels = simulator.step()
    if observation not in final_outcomes:
        final_outcomes[observation] = 1
    else:
        final_outcomes[observation] += 1
    simulator.restart()
print(", ".join([f"{str(k)}: {v}" for k, v in final_outcomes.items()]))
```

--------------------------------

### Launch Python Interpreter

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/using_pycarl.md

To begin using Pycarl, first launch the Python3 interpreter from your terminal.

```bash
python3
```

--------------------------------

### Build Model from PRISM Program

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/getting_started.ipynb

Constructs a Stormpy model from a PRISM program file. This is a common first step for analyzing models.

```python
path = stormpy.examples.files.prism_dtmc_die
prism_program = stormpy.parse_prism_program(path)
model = stormpy.build_model(prism_program)
```

--------------------------------

### Model Simulation

Source: https://context7.com/stormchecker/stormpy/llms.txt

Uses the simulator interface to sample paths through models without exhaustive state space construction. It requires building a model first and then creating a simulator with an optional seed for reproducibility.

```python
import stormpy
import stormpy.simulator
import stormpy.examples
import stormpy.examples.files

path = stormpy.examples.files.prism_dtmc_die
prism_program = stormpy.parse_prism_program(path)
model = stormpy.build_model(prism_program)

simulator = stormpy.simulator.create_simulator(model, seed=42)

final_outcomes = {}
for n in range(1000):
    simulator.restart()
    while not simulator.is_done():
        observation, reward, labels = simulator.step()

    if observation not in final_outcomes:
        final_outcomes[observation] = 1
    else:
        final_outcomes[observation] += 1

print(f"Final state distribution: {final_outcomes}")
```

--------------------------------

### Instantiate Parametric Model

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/parametric_models.ipynb

Instantiates a parametric model by mapping parameters to specific values using a dictionary. Requires a PDtmcInstantiator and a dictionary of parameter-value mappings. The RationalRF class is used for rational function representation of values.

```python
import stormpy.pars

instantiator = stormpy.pars.PDtmcInstantiator(model)
point = dict()
for x in parameters:
    print(x.name)
    point[x] = stormpy.RationalRF(0.4)
instantiated_model = instantiator.instantiate(point)
result = stormpy.model_checking(instantiated_model, properties[0])
```

--------------------------------

### Parse and Build a Markov Chain

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/getting_started.ipynb

Loads a PRISM file path, parses it into a program, and builds the corresponding model.

```python
path = stormpy.examples.files.prism_dtmc_die
prism_program = stormpy.parse_prism_program(path)
```

```python
model = stormpy.build_model(prism_program)
print("Number of states: {}".format(model.nr_states))
```

```python
print("Number of transitions: {}".format(model.nr_transitions))
```

```python
print("Labels: {}".format(model.labeling.get_labels()))
```

--------------------------------

### Build Parametric Model

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/parametric_models.ipynb

Builds a parametric model from a Prism program and properties. Collects all parameters for later instantiation. Ensure the Prism program path is correct.

```python
import stormpy
import stormpy.examples
import stormpy.examples.files

path = stormpy.examples.files.prism_pdtmc_die
prism_program = stormpy.parse_prism_program(path)
formula_str = "P=? [F s=7 & d=2]"
properties = stormpy.parse_properties(formula_str, prism_program)
model = stormpy.build_parametric_model(prism_program, properties)
parameters = model.collect_all_parameters()
for x in parameters:
    print(x)
```

--------------------------------

### Tag and push release

Source: https://github.com/stormchecker/stormpy/blob/master/doc/checklist_new_release.md

Create a signed Git tag for the new version and push it to the remote repository.

```console
git tag -a X.Y.Z -m "Stormpy version X.Y.Z" -s
git push origin X.Y.Z
```

--------------------------------

### Iterate Over MDP Model States and Transitions

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/exploration.ipynb

Iterates through all states, actions, and transitions of a stormpy model. Prints information about initial states and transition details.

```python
for state in model.states:
    if state.id in model.initial_states:
        print("State {} is initial".format(state.id))
    for action in state.actions:
        for transition in action.transitions:
            print("From state {} by action {}, with probability {}, go to state {}".format(state, action, transition.value(), transition.column))
```

--------------------------------

### Build Symbolic Model

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/engines.ipynb

Constructs a symbolic model using binary decision diagrams.

```python
symbolic_model = stormpy.build_symbolic_model(prism_program, properties)
print(type(symbolic_model))
```

--------------------------------

### Initialize State Labeling

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/models/building_mdps.ipynb

Create a StateLabeling object and add labels to states. Labels can be added individually or set for multiple states using a BitVector.

```python
state_labeling = stormpy.storage.StateLabeling(13)
labels = {"init", "one", "two", "three", "four", "five", "six", "done", "deadlock"}
for label in labels:
    state_labeling.add_label(label)

state_labeling.add_label_to_state("init", 0)
state_labeling.add_label_to_state("one", 7)
state_labeling.add_label_to_state("two", 8)
state_labeling.add_label_to_state("three", 9)
state_labeling.add_label_to_state("four", 10)
state_labeling.add_label_to_state("five", 11)
state_labeling.add_label_to_state("six", 12)
state_labeling.set_states("done", stormpy.BitVector(13, [7, 8, 9, 10, 11, 12]))
```

--------------------------------

### Assemble CTMC Model Components

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/models/building_ctmcs.ipynb

Create a SparseModelComponents object, providing the transition matrix, state labeling, and setting 'rate_transitions' to True to indicate that transition values are rates.

```python
components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, rate_transitions=True)
```

--------------------------------

### Build MDP with Nondeterministic Choice using StormPy

Source: https://context7.com/stormchecker/stormpy/llms.txt

Construct a Markov Decision Process (MDP) with multiple actions per state using custom row grouping in the transition matrix and choice labeling to name actions.

```python
import stormpy

# Create matrix with custom row grouping for nondeterminism
builder = stormpy.SparseMatrixBuilder(rows=0, columns=0, entries=0,
                                       force_dimensions=False,
                                       has_custom_row_grouping=True,
                                       row_groups=0)

# State 0 has two actions (nondeterministic choice)
builder.new_row_group(0)
builder.add_next_value(0, 1, 0.5)  # Action 0: go to 1 or 2 with prob 0.5
builder.add_next_value(0, 2, 0.5)
builder.add_next_value(1, 1, 0.2)  # Action 1: go to 1 (0.2) or 2 (0.8)
builder.add_next_value(1, 2, 0.8)

# Remaining states have single actions
builder.new_row_group(2)
builder.add_next_value(2, 3, 0.5)
builder.add_next_value(2, 4, 0.5)
# ... continue for other states

transition_matrix = builder.build()

# Create choice labeling to name actions
choice_labeling = stormpy.storage.ChoiceLabeling(14)  # Total number of choices
choice_labeling.add_label("a")
choice_labeling.add_label("b")
choice_labeling.add_label_to_choice("a", 0)  # First action in state 0
choice_labeling.add_label_to_choice("b", 1)  # Second action in state 0

# Build MDP with choice labeling
state_labeling = stormpy.storage.StateLabeling(13)
# ... set up labeling

components = stormpy.SparseModelComponents(
    transition_matrix=transition_matrix,
    state_labeling=state_labeling,
    rate_transitions=False
)
components.choice_labeling = choice_labeling

mdp = stormpy.storage.SparseMdp(components)
print(mdp)
```

--------------------------------

### Parse Prism Program and Properties

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/analysis.ipynb

Loads a PRISM model and properties for analysis. Ensure the path to the PRISM file is correct.

```python
import stormpy
import stormpy.examples
import stormpy.examples.files

path = stormpy.examples.files.prism_dtmc_die
prism_program = stormpy.parse_prism_program(path)
formula_str = "P=? [F s=7 & d=2]"
properties = stormpy.parse_properties(formula_str, prism_program)
```

--------------------------------

### Build Markov Automaton Model

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/schedulers.ipynb

Parses a PRISM program for a Markov automaton and builds the model. This is a prerequisite for transforming it into an MDP.

```python
path = stormpy.examples.files.prism_ma_simple
formula_str = "Tmin=? [ F s=4 ]"

program = stormpy.parse_prism_program(path, False, True)
formulas = stormpy.parse_properties_for_prism_program(formula_str, program)
ma = stormpy.build_model(program, formulas)
```

--------------------------------

### Collect Model Components

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/models/building_mdps.ipynb

Assemble the transition matrix, state labeling, and reward models into a SparseModelComponents object. This object is used to build the final MDP.

```python
components = stormpy.SparseModelComponents(
    transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models, rate_transitions=False
)
components.choice_labeling = choice_labeling
```

--------------------------------

### Iterate Through Model Transitions

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/getting_started.ipynb

Explores the state space of a model, printing details about each transition. Works for both deterministic and non-deterministic models.

```python
for state in model.states:
    for action in state.actions:
        for transition in action.transitions:
            print("From state {}, with probability {}, go to state {}".format(state, transition.value(), transition.column))
```

--------------------------------

### Add Transitions to GSPN

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/gspns.ipynb

Adds immediate and timed transitions to the builder with associated layout information.

```python
it_1 = builder.add_immediate_transition(1, 0.0, "it_1")
it_layout = stormpy.gspn.LayoutInfo(1.5, 2.0)
builder.set_transition_layout_info(it_1, it_layout)
```

```python
tt_1 = builder.add_timed_transition(0, 0.4, "tt_1")
tt_layout = stormpy.gspn.LayoutInfo(12.5, 2.0)
builder.set_transition_layout_info(tt_1, tt_layout)
```

--------------------------------

### Build Stormpy Info Module (CMake)

Source: https://github.com/stormchecker/stormpy/blob/master/CMakeLists.txt

CMake command to build the stormpy info module and configure its associated Python configuration file.

```cmake
stormpy_module(info info "${storm-version-info_INCLUDE_DIR}" storm-version-info)
configure_file(${CMAKE_CURRENT_SOURCE_DIR}/cmake/info_config.py.in ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/info/_config.py @ONLY)
```

--------------------------------

### Define check_hint helper function

Source: https://github.com/stormchecker/stormpy/blob/master/CMakeLists.txt

Validates that the found library directory matches the provided hint directory and prints status messages.

```cmake
function(check_hint NAME DIR_FOUND HINT_DIR FOUND_VERSION)
    # Get absolute path
    get_filename_component(PATH_FOUND ${DIR_FOUND} ABSOLUTE)
    # Print path
    if (NOT "${FOUND_VERSION}" STREQUAL "")
        message(STATUS "Stormpy - Using ${NAME} version ${FOUND_VERSION} from ${PATH_FOUND}")
    else()
        message(STATUS "Stormpy - Using ${NAME} from ${PATH_FOUND}")
    endif()

    # Check that hint was used
    if (NOT "${HINT_DIR}" STREQUAL "")
        get_filename_component(PATH_HINT ${HINT_DIR} ABSOLUTE)
        if (NOT "${PATH_FOUND}" STREQUAL "${PATH_HINT}")
            MESSAGE(SEND_ERROR "Stormpy - Using different ${NAME} directory ${PATH_FOUND} instead of given ${HINT_DIR}!")
        endif()
    endif()
endfunction(check_hint)
```

--------------------------------

### Build Models from PRISM Programs

Source: https://context7.com/stormchecker/stormpy/llms.txt

Parses a PRISM program file and constructs a sparse model representation. The model type is automatically inferred from the program content.

```python
import stormpy
import stormpy.examples
import stormpy.examples.files

# Parse a PRISM program describing a DTMC
path = stormpy.examples.files.prism_dtmc_die
prism_program = stormpy.parse_prism_program(path)

# Build the model
model = stormpy.build_model(prism_program)

# Inspect basic model properties
print("Number of states: {}".format(model.nr_states))
# Output: Number of states: 13
print("Number of transitions: {}".format(model.nr_transitions))
# Output: Number of transitions: 20
print("Model type: {}".format(model.model_type))
# Output: Model type: ModelType.DTMC
print("Labels: {}".format(model.labeling.get_labels()))
# Output: Labels: {'init', 'deadlock', 'done', 'one', 'two', 'three', 'four', 'five', 'six'}
```

--------------------------------

### Initialize ShortestPathsGenerator

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/shortest_paths.ipynb

Create an instance of the generator for the specified model and target state.

```python
spg = ShortestPathsGenerator(model, state_id)
```

--------------------------------

### Build Stormpy Utility Module (CMake)

Source: https://github.com/stormchecker/stormpy/blob/master/CMakeLists.txt

CMake command to build the stormpy utility module.

```cmake
stormpy_module(utility utility "" "")
```

--------------------------------

### Build Stormpy Storage Module (CMake)

Source: https://github.com/stormchecker/stormpy/blob/master/CMakeLists.txt

CMake command to build the stormpy storage module.

```cmake
stormpy_module(storage storage "" "")
```

--------------------------------

### Build Sparse MDP

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/models/building_mdps.ipynb

Construct the final SparseMdp object from the collected components. This represents the complete Markov Decision Process.

```python
mdp = stormpy.storage.SparseMdp(components)
print(mdp)
```

--------------------------------

### Build Sparse Markov Automaton

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/models/building_mas.ipynb

Finalize the construction of the SparseMA model.

```python
ma = stormpy.storage.SparseMA(components)
print(ma)
```

--------------------------------

### Simulate paths with Stormpy

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/simulator.ipynb

Generates three random paths of up to 20 steps each using the simulator's restart and step methods.

```python
paths = []
for m in range(3):
    path = []
    state, reward, labels = simulator.restart()
    path = [f"({state['x']},{state['y']})"]
    for n in range(20):
        actions = simulator.available_actions()
        select_action = random.randint(0, len(actions) - 1)
        path.append(f"--{actions[select_action]}-->")
        state, reward, labels = simulator.step(actions[select_action])
        path.append(f"({state['x']},{state['y']})")
        if simulator.is_done():
            break
    paths.append(path)
for path in paths:
    print(" ".join(path))
```

--------------------------------

### Adapt Model Checking Algorithm with Environment

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/analysis.ipynb

Customizes the model checking algorithm by setting an environment, including the linear equation solver type and method. This can affect result accuracy.

```python
env = stormpy.Environment()
env.solver_environment.set_linear_equation_solver_type(stormpy.EquationSolverType.native)
env.solver_environment.native_solver_environment.method = stormpy.NativeLinearEquationSolverMethod.power_iteration
result = stormpy.model_checking(model, properties[0], environment=env)
```

--------------------------------

### Build Stormpy Logic Module (CMake)

Source: https://github.com/stormchecker/stormpy/blob/master/CMakeLists.txt

CMake command to build the stormpy logic module.

```cmake
stormpy_module(logic logic "" "")
```

--------------------------------

### Build and Print a DTMC

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/models/building_dtmcs.ipynb

Constructs a SparseDtmc from pre-defined components and outputs the result.

```python
dtmc = stormpy.storage.SparseDtmc(components)
print(dtmc)
```

--------------------------------

### Assemble Model Components

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/models/building_mas.ipynb

Collect all defined components into a SparseModelComponents object.

```python
components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, markovian_states=markovian_states)
components.choice_labeling = choice_labeling
components.exit_rates = exit_rates
```

--------------------------------

### Define Reward Models

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/models/building_dtmcs.ipynb

Create a reward model using a state-action reward vector.

```python
reward_models = {}
action_reward = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0]
reward_models["coin_flips"] = stormpy.SparseRewardModel(optional_state_action_reward_vector=action_reward)
```

--------------------------------

### Load GSPN from PNML

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/gspns.ipynb

Initializes a GSPN parser to load a model from a PNML file path.

```python
import stormpy
import stormpy.gspn
import stormpy.examples
import stormpy.examples.files

import_path = stormpy.examples.files.gspn_pnml_simple
gspn_parser = stormpy.gspn.GSPNParser()
gspn = gspn_parser.parse(import_path)
```

--------------------------------

### Parametric Model Checking

Source: https://context7.com/stormchecker/stormpy/llms.txt

Builds and analyzes parametric models where transition probabilities are symbolic functions of parameters. It demonstrates collecting parameters, instantiating the model with concrete values, and checking both instantiated and parametric models.

```python
import stormpy
import stormpy.pars
import stormpy.examples
import stormpy.examples.files

path = stormpy.examples.files.prism_pdtmc_die
prism_program = stormpy.parse_prism_program(path)
formula_str = "P=? [F s=7 & d=2]"
properties = stormpy.parse_properties(formula_str, prism_program)

model = stormpy.build_parametric_model(prism_program, properties)
print(f"Model supports parameters: {model.supports_parameters}")

parameters = model.collect_all_parameters()
for param in parameters:
    print(f"Parameter: {param.name}")

instantiator = stormpy.pars.PDtmcInstantiator(model)

point = {}
for param in parameters:
    point[param] = stormpy.RationalRF(0.4)

instantiated_model = instantiator.instantiate(point)

result = stormpy.model_checking(instantiated_model, properties[0])
print(f"Result at p=0.4: {result.at(instantiated_model.initial_states[0])}")

result = stormpy.model_checking(model, properties[0])
func = result.at(model.initial_states[0])
print(f"Parametric result: {func}")
```

--------------------------------

### Parse Program with Reward Property

Source: https://context7.com/stormchecker/stormpy/llms.txt

Parses a PRISM program and a reward property, then builds a model including the reward model. Useful for analyzing expected rewards in probabilistic models.

```python
import stormpy

program = stormpy.parse_prism_program(stormpy.examples.files.prism_dtmc_die)
prop = 'R=? [F "done"]'
properties = stormpy.parse_properties(prop, program)

model = stormpy.build_model(program, properties)
assert len(model.reward_models) == 1

reward_model_name = list(model.reward_models.keys())[0]
print(f"Reward model: {reward_model_name}")

rm = model.reward_models[reward_model_name]
print(f"Has state rewards: {rm.has_state_rewards}")
print(f"Has state-action rewards: {rm.has_state_action_rewards}")
print(f"Has transition rewards: {rm.has_transition_rewards}")

if rm.has_state_action_rewards:
    for idx, reward in enumerate(rm.state_action_rewards):
        print(f"Choice {idx}: reward = {reward}")

result = stormpy.model_checking(model, properties[0])
initial_state = model.initial_states[0]
print(f"Expected coin flips: {result.at(initial_state)}")
```

--------------------------------

### Build Optional Stormpy GSPN Module (CMake)

Source: https://github.com/stormchecker/stormpy/blob/master/CMakeLists.txt

CMake command to conditionally build the optional stormpy GSPN module.

```cmake
stormpy_optional_module(gspn "GSPN")
```

--------------------------------

### Inspect Sparse Model Metrics

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/engines.ipynb

Retrieves state and transition counts from a sparse model.

```python
print("Number of states: {}".format(sparse_model.nr_states))
```

```python
print("Number of transitions: {}".format(sparse_model.nr_transitions))
```

--------------------------------

### Build and Export GSPN

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/gspns.ipynb

Finalizes the GSPN construction and exports the model to a file.

```python
gspn = builder.build_gspn()
```

```python
export_path = stormpy.examples.files.gspn_pnpro_simple
gspn.export_gspn_pnpro_file(export_path)
```

--------------------------------

### Generate paths with internal action indices

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/simulator.ipynb

Uses a simulator to traverse a model and print paths using internal state and action identifiers.

```python
# 3 paths of at most 20 steps.
paths = []
for m in range(3):
    path = []
    state, reward, labels = simulator.restart()
    path = [f"{state}"]
    for n in range(20):
        actions = simulator.available_actions()
        select_action = random.randint(0, len(actions) - 1)
        path.append(f"--act={actions[select_action]}-->")
        state, reward, labels = simulator.step(actions[select_action])
        path.append(f"{state}")
        if simulator.is_done():
            break
    paths.append(path)
for path in paths:
    print(" ".join(path))
    print("------")
```

--------------------------------

### Initialize and Operate on Polynomials

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/using_pycarl.md

Clear the variable pool, create variables, and perform arithmetic operations to create and manipulate polynomials.

```python
pycarl.clear_variable_pool()
x = pycarl.Variable("x")
y = pycarl.Variable("y")
pol1 = x * x + pycarl.gmp.Integer(2)
pol2 = y + pycarl.gmp.Integer(1)
result = pol1 * pol2
print("({}) * ({}) = {}".format(pol1, pol2, result))
```

--------------------------------

### Build and Check Symbolic Model

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/analysis.ipynb

Constructs a symbolic model and performs model checking. The result needs to be filtered to access specific state information.

```python
model = stormpy.build_symbolic_model(prism_program, properties)
result = stormpy.model_checking(model, properties[0])
```

```python
filter = stormpy.create_filter_initial_states_symbolic(model)
result.filter(filter)
assert result.min == result.max
```

--------------------------------

### Query K-Shortest Paths

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/shortest_paths.ipynb

Iterate through the first three shortest paths and retrieve their sequences and distances.

```python
for k in range(1, 4):
    path = spg.get_path_as_list(k)
    distance = spg.get_distance(k)
    print("{}-shortest path to state #{}: {}, with distance {}".format(k, state_id, path, distance))
```

--------------------------------

### Initialize Choice Labeling

Source: https://github.com/stormchecker/stormpy/blob/master/doc/source/doc/models/building_mdps.ipynb

Initialize a ChoiceLabeling object to assign labels to the nondeterministic choices within states. This is useful for distinguishing different actions.

```python
choice_labeling = stormpy.storage.ChoiceLabeling(14)
choice_labels = {"a", "b"}

for label in choice_labels:
    choice_labeling.add_label(label)
```

--------------------------------

### Build Models from JANI Format

Source: https://context7.com/stormchecker/stormpy/llms.txt

Loads models from JANI JSON-based descriptions, which may contain embedded properties.

```python
import stormpy
import stormpy.examples
import stormpy.examples.files

# Parse JANI model (returns model and any embedded properties)
path = stormpy.examples.files.jani_dtmc_die
jani_program, properties = stormpy.parse_jani_model(path)

# Build the model
model = stormpy.build_model(jani_program)
print("Model type: {}".format(model.model_type))
# Output: Model type: ModelType.DTMC
```
Tokens:
Raw