can't check DTMC model

[Serendipity953]

I created a DTMC model by stormpy.parse_prism_program And I want to check the property I defined, but some error occured. The python code I wrote follows:

    path = "/home/yangjunfeng/Verify/abstract/cartpole/prism_model/cartpole_level5_train3_8.pm"
    prism_program = stormpy.parse_prism_program(path)
    formula_str = "P=? [ !(true U<=8 \"unsafe\") ]"
    properties = stormpy.parse_properties(formula_str, prism_program)
    model = stormpy.build_model(prism_program, properties)
    result = stormpy.model_checking(model, properties[0])
    initial_state = model.initial_states[0]
    print(result.at(initial_state))

And the error occured like this:

ERROR (LTL2DeterministicAutomaton.cpp:61): Storm is compiled without Spot support.
Traceback (most recent call last):
  File "teststormpy.py", line 168, in <module>
    StromChecking()
  File "teststormpy.py", line 164, in StromChecking
    result = stormpy.model_checking(model, properties[0])
  File "/home/yangjunfeng/Stormpy/stormpy-1.8.0/lib/stormpy/__init__.py", line 273, in model_checking
    extract_scheduler=extract_scheduler, force_fully_observable=force_fully_observable, environment=environment)
  File "/home/yangjunfeng/Stormpy/stormpy-1.8.0/lib/stormpy/__init__.py", line 343, in check_model_sparse
    return core._model_checking_sparse_engine(model, task, environment=environment)
RuntimeError: NotSupportedException: Storm is compiled without Spot support.

So I want to know what's wrong with my Storm. And what's more, how can I get to know more about building the dtmc model mannully insted of reading from prism files, and do some model checking?

[volkm]

The formula is not supported in your Storm installation because the Spot library is missing. Spot provides support for LTL formula. You could reinstall Storm with support for Spot (How did you install Storm? Via source?) Another idea I see could be to slightly rewrite your formula and remove the negation: P=? [ true U<=8 \"unsafe\" ]. Your current Storm installation should then be able to handle the formula. If am not mistaken, you can use 1-result to get the desired result.

Regarding manually building DTMCs: you can take a look at the documentation which describes how to manually build the transition matrix.

[tquatmann]

A small addendum to @volkm's comment: the second idea (removing the negation) should be much more scalable towards larger models and larger step bounds in the formula, as Storm will be using a dedicated algorithm for the property. With the negation inside, a general-purpose algorithm (LTL model checking) will be used.

[Serendipity953]

The formula is not supported in your Storm installation because the Spot library is missing. Spot provides support for LTL formula. You could reinstall Storm with support for Spot (How did you install Storm? Via source?) Another idea I see could be to slightly rewrite your formula and remove the negation: P=? [ true U<=8 \"unsafe\" ]. Your current Storm installation should then be able to handle the formula. If am not mistaken, you can use 1-result to get the desired result.

Regarding manually building DTMCs: you can take a look at the documentation which describes how to manually build the transition matrix.

Thank you very much for your reply. I tried your second solution and this is really the problem. I have read the documentation about building DTMC. Unfortunately, the tutorial does not explain how to proceed with the verification after the DTMC has been established using transition matrix. I don't know some details about the DTMC model I've built, neither the functions I called during the building process. Maybe I need some more reading about the API documentation. I can't thank you enough if you could give me more advice on learning Storm, anyway, thanks for the answer

And I recieved @tquatmann 's addendum, very grateful for this little tips and I think it will be useful to me. Because what I'm facing is really a large model and deep steps. Thank you again.

[volkm]

I am happy to hear that rewriting the formula allowed you to perform the analysis.

Regarding building your own models: After you have built the transition matrix and other components such as the labeling according to the documentation, you build your model with

...
components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models)
model = stormpy.storage.SparseDtmc(components)

These steps basically replace your previous step model = stormpy.build_model(prism_program, properties) in which you built the model from a Prism file. After you have built your model, you can use the same steps as before to perform the analysis:

result = stormpy.model_checking(model, properties[0])
initial_state = model.initial_states[0]
print(result.at(initial_state))

We are continuously trying to improve our documentation. If you have concrete steps which are unclear or where information is missing, please let us know.

[Serendipity953]

Thanks again for your reply, and there is something still uclear to me. That is how can I get the

 properties[0]

inside the step

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

because in the ananlysis performed before, the properties comes from

 properties = stormpy.parse_properties(formula_str, prism_program)

but here I have no prism_program for building model from matrix. Can I repalce the prism_program by dtmc model? But this looks a little strange. That's what I'm wondering. This may be a stupid question, but I appreciate your attention and advice.

[volkm]

Good question, we do indeed not properly explain it in the documentation. You can simply leave out the prism program: properties = stormpy.parse_properties(formula_str) should work.