check multiple properties in one call

[temunds]

Hello everyone,

I was unsure whether to open an issue for this and have been searching for documentation about this feature but couldn’t find it anywhere, apologies if I overlooked something.

I am currently working with MAs formulated in the extended prism language, so that the models are reformulated to a .jani file in storm internally. Additionally, the model has to be constructed for every model-checking query. Combined (I couldn’t distinguish the exact times of both steps) those steps take up most of the time for the model-checking of a single property – at least for the first exemplary files I built.

Is there a possibility to reduce this time by constructing the model once and checking multiple properties afterwards? I am aware of the multi-objective checking, but I couldn’t see an option that allows for multiple properties without combining them for the computation of pareto-curves etc.

Thank you and best regards :)

[volkm]

You can concatenate properties with ; in-between: P=? [F "goal1"];P=? [F "goal2"].

If you need more flexibility over the individual steps, you can also try using the Python bindings stormpy.

[temunds]

Awesome, thanks.