Model checking (using Storm)

In this notebook, we will show how to do model checking in stormvogel. This is efficient because it uses Storm as a backend. We first use the simple study model. The idea is that if you do not study, then you save some time, hence you will gain 15 reward. If you pass the test you get 100 reward because you want to graduate eventually. If you study, then the chance of passing the test becomes higher. Now should you study?

from stormvogel import *

study = examples.create_study_mdp()
vis = show(study, layout=Layout("layouts/pinkgreen.json"))

Now we let stormpy solve the question whether you should study. Model checking requires a property string. This is a string that specifies what result the model checker should aim for. Stormvogel has a graphical interface that makes it easier to create these. Try to create a property that maximizes the reward at the end. The result should be Rmax=? [F "end"].

# build_property_string(study)

Now we run our model checking, and then display the result on the model. The action that is chosen to maximize the reward is marked in red. In conclusion, you should study! The red action is called the scheduled action. The star symbol indicates the result of a state. In this case, the result can be seen as the expected reward. The scheduler finds that going to the state with ‘didn’t study’ results in an expected reward of 55, while the state with ‘studied’ results in an expected value of 90.

result = model_checking(
    study, 'Rmax=? [F "end"]', True
)  # true lets it return a scheduler as well
vis = show(study, layout=Layout("layouts/pinkgreen.json"), result=result)

Now, imagine that the exam is not so important after all. Say you only get 20 reward for passing. Is it still worth studying now? It turns out not to be the case! (The turning point is 30)

study2 = examples.create_study_mdp()

reward_model = study2.get_rewards("R")
pass_test = study2.get_states_with_label("pass test")[0]
reward_model.set_state_reward(pass_test, 20)
result3 = model_checking(study2, 'Rmax=? [F "end"]')
vis3 = show(study2, layout=Layout("layouts/pinkgreen.json"), result=result3)