New to model checking: how to check properties of custom-made model?

[nielsneerhoff]

Dear Stormpy team,

I am having difficulties understanding how to check a property of a custom-made model. I am trying to create a DTMC according to the tutorial in the Stormpy documentation (from the Advanced Examples). I would like to check properties of this DTMC - let us say compute the reachability of state 'six'.

dtmc = stormpy.storage.SparseDtmc(components) # according to documentation

formula_str = "P=? [F {}]"
properties = stormpy.parse_properties(formula_str)

Now the reason I put {} in the formula specification string is because whatever I put there, I get the error

ERROR (SpiritErrorHandler.h:26): Parsing error at 1:6:  expecting <path formula>, here:
        P=? [F {}]
             ^

I have also tried entering other formulas from PRISMs documentation (those without F in them), but with no luck.

After parsing the properties I would imagine I would have to do something like this:

model = stormpy.build_model(dtmc, properties)
result = stormpy.model_checking(model, properties[0])

I feel that I fail the understand the logic of where/when the variables in a formula string are 'binded' to labels of the model (in my case the DTMC) - although also that guess might be completely wrong.

Could anyone help me out here?

Thanks in advance! Best,

[tquatmann]

You need to put the labels in quotes, so e.g. P=? [ F "six" ] should work (assuming six is a label. Make sure to properly escape the quotes in your python code, like this

    formula_str = "P=? [ F \"six\"]"

or

   formula_str = 'P=? [ F "six"]'

The model building step can be skipped here and you can use the dtmc for model checking directly. Model building is only necessary if your model is described symbolically e.g. by a PRISM file.

[nielsneerhoff]

Perfect @tquatmann , thanks a lot for your fast reply! This indeed fixed it.

Having fun with your library so far, great work!