Strompy conversion

Models can be converted back and forth between stormvogel and stormpy with ease using the mapping module. This is useful, because this allows you to combine both APIs. For example, you could create a model in stormvogel becuase it has an easy API, do some model checking in stormpy, and then convert it back to display the results. (Note that there is also a direct model checking function available that uses stormpy behind the scenes.)

from stormvogel import *
stormvogel_model = examples.create_car_mdp()
vis = show(stormvogel_model, layout=stormvogel.layout.Layout("layouts/car.json"))

Test request failed. See 'Communication server remark' in docs. Disable warning by use_server=False.

First, let’s convert the stormvogel model to the same model in stormpy.

import stormvogel.stormpy_utils.mapping as mapping

stormpy_model = mapping.stormvogel_to_stormpy(stormvogel_model)
print(stormpy_model)

--------------------------------------------------------------
Model type:     MDP (sparse)
States:         5
Transitions:    9
Choices:        9
Reward Models:  none
State Labels:   6 labels
   * green light -> 2 item(s)
   * red light -> 2 item(s)
   * still -> 2 item(s)
   * moving -> 2 item(s)
   * accident -> 1 item(s)
   * init -> 1 item(s)
Choice Labels:  3 labels
   * wait -> 4 item(s)
   * brake -> 2 item(s)
   * accelerate -> 2 item(s)
--------------------------------------------------------------

And now we convert it back.

stormvogel_model2 = stormpy_to_stormvogel(stormpy_model)
vis = show(stormvogel_model2, layout=Layout("layouts/car.json"))

The result of the double conversion is equal to the original model.

stormvogel_model == stormvogel_model2

True