more information at:
import stormpy
import stormpy.info
print("Stormpy version: " + stormpy.__version__)
print("using Storm in version: " + stormpy.info.storm_version())
prism_program = stormpy.parse_prism_program("examples/music_shuffle.nm")
print(prism_program.model_type)
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()))
# 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)))
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
i = 0
for res in result.get_values():
print("Result for state {} {}: {}".format(i, state_vals.get_string(i), res))
i += 1
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);
Question: Which button should be pressed?
Solution: Obtain scheduler specifying the optimal choice
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)
for s, b in buttons.items():
if s == 0: continue
print("{}: {}".format(s, choice_labels.get_labels_of_choice(b+2*s+1)))
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);
Satisfy more than one objective:
!storm --prism examples/music_shuffle.nm --prop 'multi(Pmax=? [F<=10 "found"], Pmin=? [!"found" U<=10 "avoid"])' --multiobjective:exportplot . | tail -1
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);
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)
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);
Reaching different songs
# 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();