Part 3: Advanced Features with Stormpy

Matthias Volk



[www.stormchecker.org](https://www.stormchecker.org)

Press spacebar to navigate

Stormpy

Python bindings for Storm

  • Easy access to Storm's algorithms and features
  • Maintains performance of Storm
  • Allows rapid prototyping:
    ➜ Implement your own customized approach based on probabilistic model checking

more information at:

[www.stormchecker.org/stormpy/](https://www.stormchecker.org/stormpy/)

Running Stormpy

In [ ]:
import stormpy
import stormpy.info

print("Stormpy version: " + stormpy.__version__)
print("using Storm in version: " + stormpy.info.storm_version())

Running example: MP3 player


Source: Pixabay

Setting:

  • MP3 Player with 100 songs
  • Start at random song
  • Want to listen to song number 42
  • Only two buttons:
    • next song
    • random song

Question:

  • Find fewest steps to reach song number 42
  • Which buttons should be pressed in which order?

Music shuffle in stormpy

In [ ]:
prism_program = stormpy.parse_prism_program("examples/music_shuffle.nm")
print(prism_program.model_type)
In [ ]:
options = stormpy.BuilderOptions(True, True)
options.set_build_state_valuations()
options.set_build_choice_labels()
model = stormpy.build_sparse_model_with_options(prism_program, options)
print("Number of states: {}".format(model.nr_states))
print("Number of transitions: {}".format(model.nr_transitions))
print("Labels: {}".format(model.labeling.get_labels()))

Model checking with stormpy

In [ ]:
# Set property
formula_str = 'Rmin=? [F "found"]'
properties = stormpy.parse_properties(formula_str, prism_program)

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

# Print result
initial_state = model.initial_states[0]
print("Expected number of steps to reach song 42 (from initial state): {}".format(result.at(initial_state)))

Exploring the model

In [ ]:
state = model.states[2]
state_vals = model.state_valuations
print("State {} with variable values: {}".format(state, state_vals.get_string(state.id)))
choice_labels = model.choice_labeling
for action in state.actions:
    for transition in action.transitions:
        print("With action {} and probability {}, go to state {} {}".format(choice_labels.get_labels_of_choice(action.id+3), transition.value(), transition.column, state_vals.get_string(transition.column)))
        if transition.column > 10: break

Results for all states

In [ ]:
# Results for all states
i = 0
for res in result.get_values():
    print("Result for state {} {}: {}".format(i, state_vals.get_string(i), res))
    i += 1
In [ ]:
import matplotlib.pyplot as plt
plt.rcParams["figure.figsize"] = (15,5)
plt.axvline(x=28, color="r")
plt.axvline(x=42, color="r")
plt.xticks(list(range(0,101,10)) + [28,42])
plt.xlabel('Current song number')
plt.ylabel('Expected steps till song 42')
plt.title("Music Shuffle")

# Plot results for all states
plt.plot(range(1,101), result.get_values()[1:], linewidth=2);

Exploring the solution

Question: Which button should be pressed?

Solution: Obtain scheduler specifying the optimal choice

In [ ]:
result = stormpy.model_checking(model, properties[0], extract_scheduler=True)
scheduler = result.scheduler
assert scheduler.memoryless
assert scheduler.deterministic

buttons = dict()
for state in model.states:
    choice = scheduler.get_choice(state)
    action = choice.get_deterministic_choice()
    buttons[state.id] = action
    
print(buttons)
In [ ]:
for s, b in buttons.items():
    if s == 0: continue
    print("{}: {}".format(s, choice_labels.get_labels_of_choice(b+2*s+1)))

Exploring the solution

In [ ]:
plt.xlabel('Current song number')
plt.ylabel('Button to press')
plt.title("Music Shuffle")
plt.yticks([0,1], ["next", "shuffle"])

button_list = [b for s, b in buttons.items()]

# Plot results for all states
plt.plot(button_list[1:], linewidth=2);

Multiobjective model checking

Satisfy more than one objective:

  1. Reach song 42 within 10 steps, and
  2. Do not listen to the songs 1-10 before song 42 (for the first 10 steps)

Multiobjective model checking

In [ ]:
!storm --prism examples/music_shuffle.nm --prop 'multi(Pmax=? [F<=10 "found"], Pmin=? [!"found" U<=10 "avoid"])' --multiobjective:exportplot . | tail -1
In [ ]:
import numpy as np
from numpy import genfromtxt
overapprox = genfromtxt('overapproximation.csv', delimiter=',', skip_header=1)
underapprox = genfromtxt('underapproximation.csv', delimiter=',', skip_header=1)
boundaries = genfromtxt('paretopoints.csv', delimiter=',', skip_header=1)
import matplotlib.pyplot as plt
plt.margins(0)
plt.axis((0,1,0,1))
plt.xlabel('Find song 42')
plt.ylabel('Avoid first 10 songs')
plt.title("Music Shuffle")
plt.axhspan(0, 1, facecolor='r', alpha=0.5)
plt.fill(boundaries[:,0], boundaries[:,1], 'r', alpha=1)
plt.fill(overapprox[:,0], overapprox[:,1], 'b', alpha=1)
plt.fill(underapprox[:,0], underapprox[:,1], 'g', alpha=1);

Parametric model checking

  • Leave some probabilities open and use parameters instead

Music shuffle 2:

  • 20 songs
  • Start at song 10
  • Only one (probabilistic) button:
    • with probability p go to next song
    • with probability 1-p go two songs back
  • Want to listen to song 12
In [ ]:
prism_program = stormpy.parse_prism_program("examples/music_shuffle2.nm")
properties = stormpy.parse_properties('Rmin=? [F "found"];Rmin=? [F "found2"]', prism_program)
model = stormpy.build_parametric_model(prism_program)

# Model checking
result = stormpy.model_checking(model, properties[0])
initial_state = model.initial_states[0]
ratfunc = str(result.at(initial_state))
print(ratfunc)

Parametric model checking

In [ ]:
plt.xlabel('p')
plt.ylabel('Expected steps till song 12')
plt.title("Music Shuffle")

p = np.linspace(0.001, 0.999, 100)
plt.axis((0,1,0,60))
plot_func = eval(ratfunc.replace("^", "**"))
plt.plot(p, plot_func, linewidth=2);

Parametric model checking

Reaching different songs

In [ ]:
# Model checking for song 3
result2 = stormpy.model_checking(model, properties[1])
ratfunc2 = str(result2.at(initial_state))
plt.xlabel('p')
plt.ylabel('Expected steps till song')
plt.title("Music Shuffle")
p = np.linspace(0.001, 0.999, 100)
plt.axis((0,1,0,60))
plot_func2 = eval(ratfunc2.replace("^", "**"))
plt.plot(p, plot_func, label="Song 12", linewidth=2)
plt.plot(p, plot_func2, label="Song 3", linewidth=2)
plt.legend();

Stormpy

  • Python bindings for Storm
  • Easy and rapid access to features of Storm
  • Allows user guided analysis
  • Fast prototyping of tools and approaches

Summary

Storm

  • Is efficient
  • Modular approach for solvers
  • Specialized engines
  • Broad range of properties (probabilities, expected rewards, multi-objective, ...)
  • Parametric analysis
  • and many more: Partially observable MDP, generalized stochastic Petri nets, dynamic fault trees, ...

Try it out!


[www.stormchecker.org](https://www.stormchecker.org)

In [ ]: