From 7ea0055c11906c5fdac9f573ccdae58c47578ba7 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 22 May 2020 14:41:20 +0200 Subject: [PATCH] added an example that prints the model checking result for all states --- examples/analysis/04-analysis.py | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 examples/analysis/04-analysis.py diff --git a/examples/analysis/04-analysis.py b/examples/analysis/04-analysis.py new file mode 100644 index 0000000..2dd5a26 --- /dev/null +++ b/examples/analysis/04-analysis.py @@ -0,0 +1,28 @@ +import stormpy +import stormpy.core + +import stormpy.examples +import stormpy.examples.files + + +def example_analysis_04(): + path = stormpy.examples.files.prism_dtmc_die + prism_program = stormpy.parse_prism_program(path) + + formula_str = "P=? [F s=7 & d=2]" + properties = stormpy.parse_properties(formula_str, prism_program) + + options = stormpy.BuilderOptions([p.raw_formula for p in properties]) + options.set_build_state_valuations() + model = stormpy.build_sparse_model_with_options(prism_program, options) + + result = stormpy.model_checking(model, properties[0]) + + # Print the model checking result for all states + + print("Model checking results:") + for i in range(len(model.states)): + print("\tstate #{}\t {}:\t {}".format(i,model.state_valuations.get_state(i),result.at(i))) + +if __name__ == '__main__': + example_analysis_04() \ No newline at end of file