Provide a way to use the model checker when only a sparse representation (and no prism description) is available

[PimLeerkes]

No description provided.

[volkm]

Can you give a bit more details what you expect stormpy should support here?
Or was this issue supposed to be for stormvogel?

[volkm]

Model checking a model (however it was created) should work as follows:

formula = stormpy.parse_properties('P=? [ F "goal" ]')[0]
result = stormpy.model_checking(model, formula)
initial_state = model.initial_states[0]
res = result.at(initial_state)