From 201aaa115d9e86909be158a2ca80283a46611962 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 2 Aug 2017 14:19:08 +0200 Subject: [PATCH] make sure examples run through again --- examples/01-getting-started.py | 16 +++++++++----- examples/02-getting-started.py | 40 +++++++++++++++++++--------------- examples/03-getting-started.py | 24 +++++++++++--------- examples/04-getting-started.py | 32 +++++++++++++++------------ lib/stormpy/__init__.py | 1 + 5 files changed, 65 insertions(+), 48 deletions(-) diff --git a/examples/01-getting-started.py b/examples/01-getting-started.py index 3a5abbc..d24c888 100644 --- a/examples/01-getting-started.py +++ b/examples/01-getting-started.py @@ -4,10 +4,14 @@ import stormpy.core import stormpy.examples import stormpy.examples.files -path = stormpy.examples.files.prism_dtmc_die -prism_program = stormpy.parse_prism_program(path) +def example_getting_started_01(): + 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)) + 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.labeling.get_labels())) + +if __name__ == 'main': + example_getting_started_01() \ No newline at end of file diff --git a/examples/02-getting-started.py b/examples/02-getting-started.py index f34ca24..6306f11 100644 --- a/examples/02-getting-started.py +++ b/examples/02-getting-started.py @@ -4,26 +4,30 @@ import stormpy.core import stormpy.examples import stormpy.examples.files -path = stormpy.examples.files.prism_dtmc_die -prism_program = stormpy.parse_prism_program(path) +def example_getting_started_02(): + 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)) + 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.labeling.get_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 = "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.labeling.get_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)) + 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.labeling.get_labels())) + +if __name__ == 'main': + example_getting_started_02() \ No newline at end of file diff --git a/examples/03-getting-started.py b/examples/03-getting-started.py index 6da175d..c406fc4 100644 --- a/examples/03-getting-started.py +++ b/examples/03-getting-started.py @@ -4,15 +4,19 @@ import stormpy.core import stormpy.examples import stormpy.examples.files -path = stormpy.examples.files.prism_dtmc_die -prism_program = stormpy.parse_prism_program(path) +def example_getting_started_03(): + 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) + 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) + +if __name__ == 'main': + example_getting_started_03() \ No newline at end of file diff --git a/examples/04-getting-started.py b/examples/04-getting-started.py index efa03e5..037015d 100644 --- a/examples/04-getting-started.py +++ b/examples/04-getting-started.py @@ -1,5 +1,6 @@ import stormpy import stormpy.core +import stormpy.pars import pycarl import pycarl.core @@ -7,21 +8,24 @@ import pycarl.core import stormpy.examples import stormpy.examples.files -path = stormpy.examples.files.prism_pdtmc_die -prism_program = stormpy.parse_prism_program(path) +def example_getting_started_04(): + 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)) + 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]) + instantiator = stormpy.pars.PDtmcInstantiator(model) + point = dict() + parameters = model.collect_probability_parameters() + for x in parameters: + print(x.name) + point[x] = stormpy.RationalRF(0.4) + instantiated_model = instantiator.instantiate(point) + result = stormpy.model_checking(instantiated_model, properties[0]) +if __name__ == 'main': + example_getting_started_04() \ No newline at end of file diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 67e998f..17350cd 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -4,6 +4,7 @@ from . import storage from .storage import * from .version import __version__ from ._config import * +from .logic import * from pycarl import Variable # needed for building parametric models