From e025ddf8b5e57e843040131263b134a11e7995c1 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 1 Feb 2017 12:07:43 +0100 Subject: [PATCH] examples to accompany our getting started guide --- examples/01-getting-started.py | 13 +++++++++++++ examples/02-getting-started.py | 29 +++++++++++++++++++++++++++++ examples/03-getting-started.py | 18 ++++++++++++++++++ examples/04-getting-started.py | 27 +++++++++++++++++++++++++++ examples/05-getting-started.py | 0 5 files changed, 87 insertions(+) create mode 100644 examples/01-getting-started.py create mode 100644 examples/02-getting-started.py create mode 100644 examples/03-getting-started.py create mode 100644 examples/04-getting-started.py create mode 100644 examples/05-getting-started.py diff --git a/examples/01-getting-started.py b/examples/01-getting-started.py new file mode 100644 index 0000000..fbff4b8 --- /dev/null +++ b/examples/01-getting-started.py @@ -0,0 +1,13 @@ +import stormpy +import stormpy.core + +import stormpy.examples +import stormpy.examples.files + +path = stormpy.examples.files.prism_dtmc_die +prism_program = stormpy.parse_prism_program(path) + +model = stormpy.build_model(prism_program) +print("Number of states: {}".format(model.nr_states)) +print("Number of transitions: {}".format(model.nr_transitions)) +print("Labels: {}".format(model.labels)) \ No newline at end of file diff --git a/examples/02-getting-started.py b/examples/02-getting-started.py new file mode 100644 index 0000000..f34ca24 --- /dev/null +++ b/examples/02-getting-started.py @@ -0,0 +1,29 @@ +import stormpy +import stormpy.core + +import stormpy.examples +import stormpy.examples.files + +path = stormpy.examples.files.prism_dtmc_die +prism_program = stormpy.parse_prism_program(path) + + +model = stormpy.build_model(prism_program) +print("Number of states: {}".format(model.nr_states)) +print("Number of transitions: {}".format(model.nr_transitions)) +print("Labels in the model: {}".format(model.labels)) + +formula_str = "P=? [F s=2]" +properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program) +model_for_formula = stormpy.build_model(prism_program, properties) +print("Number of states: {}".format(model_for_formula.nr_states)) +print("Number of transitions: {}".format(model_for_formula.nr_transitions)) +print("Labels in the model: {}".format(model_for_formula.labels)) + + +formula_str_2 = "P=? [F s=7 & d=2]" +properties_2 = stormpy.parse_properties_for_prism_program(formula_str_2, prism_program) +model_for_formula_2 = stormpy.build_model(prism_program, properties_2) +print("Number of states: {}".format(model_for_formula_2.nr_states)) +print("Number of transitions: {}".format(model_for_formula_2.nr_transitions)) +print("Labels in the model: {}".format(model_for_formula_2.labels)) diff --git a/examples/03-getting-started.py b/examples/03-getting-started.py new file mode 100644 index 0000000..6da175d --- /dev/null +++ b/examples/03-getting-started.py @@ -0,0 +1,18 @@ +import stormpy +import stormpy.core + +import stormpy.examples +import stormpy.examples.files + +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_for_prism_program(formula_str, prism_program) +model = stormpy.build_model(prism_program, properties) +result = stormpy.model_checking(model, properties[0]) +print(result) +assert result.result_for_all_states +for x in result.get_values(): + print(x) diff --git a/examples/04-getting-started.py b/examples/04-getting-started.py new file mode 100644 index 0000000..efa03e5 --- /dev/null +++ b/examples/04-getting-started.py @@ -0,0 +1,27 @@ +import stormpy +import stormpy.core + +import pycarl +import pycarl.core + +import stormpy.examples +import stormpy.examples.files + +path = stormpy.examples.files.prism_pdtmc_die +prism_program = stormpy.parse_prism_program(path) + + +formula_str = "P=? [F s=7 & d=2]" +properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program) +model = stormpy.build_parametric_model(prism_program, properties) +print("Model supports parameters: {}".format(model.supports_parameters)) + +instantiator = stormpy.PdtmcInstantiator(model) +point = dict() +parameters = model.collect_probability_parameters() +for x in parameters: + print(x.name) + point[x] = 0.4 +instantiated_model = instantiator.instantiate(point) +result = stormpy.model_checking(instantiated_model, properties[0]) + diff --git a/examples/05-getting-started.py b/examples/05-getting-started.py new file mode 100644 index 0000000..e69de29