From 1930a6d612642ab702a5fb2de69882c31b27a74d Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 29 Nov 2019 23:52:30 +0100 Subject: [PATCH] generic parse_properties for simpler code --- doc/source/doc/engines.rst | 2 +- doc/source/doc/parametric_models.rst | 2 +- doc/source/doc/reward_models.rst | 2 +- doc/source/doc/schedulers.rst | 2 +- doc/source/getting_started.rst | 4 ++-- examples/02-getting-started.py | 4 ++-- examples/03-getting-started.py | 2 +- examples/04-getting-started.py | 2 +- examples/analysis/01-analysis.py | 2 +- examples/exploration/01-exploration.py | 2 +- examples/exploration/02-exploration.py | 2 +- lib/stormpy/__init__.py | 22 ++++++++++++++++++++++ src/core/core.cpp | 2 +- 13 files changed, 36 insertions(+), 14 deletions(-) diff --git a/doc/source/doc/engines.rst b/doc/source/doc/engines.rst index f145e5b..6816cee 100644 --- a/doc/source/doc/engines.rst +++ b/doc/source/doc/engines.rst @@ -16,7 +16,7 @@ In all of the examples so far we used the default sparse engine: >>> import stormpy.examples >>> import stormpy.examples.files >>> prism_program = stormpy.parse_prism_program(stormpy.examples.files.prism_dtmc_die) - >>> properties = stormpy.parse_properties_for_prism_program('P=? [F "one"]', prism_program) + >>> properties = stormpy.parse_properties('P=? [F "one"]', prism_program) >>> sparse_model = stormpy.build_sparse_model(prism_program, properties) >>> print(type(sparse_model)) diff --git a/doc/source/doc/parametric_models.rst b/doc/source/doc/parametric_models.rst index d16b597..d9c7d11 100644 --- a/doc/source/doc/parametric_models.rst +++ b/doc/source/doc/parametric_models.rst @@ -17,7 +17,7 @@ If the constants only influence the probabilities or rates, but not the topology >>> 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) + >>> properties = stormpy.parse_properties(formula_str, prism_program) >>> model = stormpy.build_parametric_model(prism_program, properties) >>> parameters = model.collect_probability_parameters() >>> for x in parameters: diff --git a/doc/source/doc/reward_models.rst b/doc/source/doc/reward_models.rst index e2b1109..4e59faf 100644 --- a/doc/source/doc/reward_models.rst +++ b/doc/source/doc/reward_models.rst @@ -17,7 +17,7 @@ We consider the die again, but with another property which talks about the expec >>> program = stormpy.parse_prism_program(stormpy.examples.files.prism_dtmc_die) >>> prop = "R=? [F \"done\"]" - >>> properties = stormpy.parse_properties_for_prism_program(prop, program, None) + >>> properties = stormpy.parse_properties(prop, program, None) >>> model = stormpy.build_model(program, properties) >>> assert len(model.reward_models) == 1 diff --git a/doc/source/doc/schedulers.rst b/doc/source/doc/schedulers.rst index 00b03bb..a06fdcb 100644 --- a/doc/source/doc/schedulers.rst +++ b/doc/source/doc/schedulers.rst @@ -22,7 +22,7 @@ As in :doc:`../getting_started`, we import some required modules and build a mod >>> path = stormpy.examples.files.prism_mdp_coin_2_2 >>> formula_str = "Pmin=? [F \"finished\" & \"all_coins_equal_1\"]" >>> program = stormpy.parse_prism_program(path) - >>> formulas = stormpy.parse_properties_for_prism_program(formula_str, program) + >>> formulas = stormpy.parse_properties(formula_str, program) >>> model = stormpy.build_model(program, formulas) Next we check the model and make sure to extract the scheduler: diff --git a/doc/source/getting_started.rst b/doc/source/getting_started.rst index e35acc1..dc624e9 100644 --- a/doc/source/getting_started.rst +++ b/doc/source/getting_started.rst @@ -72,7 +72,7 @@ To express that one is interested in the reachability of any state where the pri Stormpy can be used to parse this. As the variables in the property refer to a program, the program has to be passed as an additional parameter:: >>> formula_str = "P=? [F s=2]" - >>> properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program) + >>> properties = stormpy.parse_properties(formula_str, prism_program) Notice that properties is now a list of properties containing a single element. @@ -105,7 +105,7 @@ Checking properties The last lesson taught us to construct properties and models with matching state labels. Now default checking routines are just a simple command away:: - >>> properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program) + >>> properties = stormpy.parse_properties(formula_str, prism_program) >>> model = stormpy.build_model(prism_program, properties) >>> result = stormpy.model_checking(model, properties[0]) diff --git a/examples/02-getting-started.py b/examples/02-getting-started.py index e547c90..722e8c9 100644 --- a/examples/02-getting-started.py +++ b/examples/02-getting-started.py @@ -15,14 +15,14 @@ def example_getting_started_02(): 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) + properties = stormpy.parse_properties(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) + properties_2 = stormpy.parse_properties(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)) diff --git a/examples/03-getting-started.py b/examples/03-getting-started.py index 7b38cf5..eed0b8f 100644 --- a/examples/03-getting-started.py +++ b/examples/03-getting-started.py @@ -10,7 +10,7 @@ def example_getting_started_03(): 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) + properties = stormpy.parse_properties(formula_str, prism_program) model = stormpy.build_model(prism_program, properties) result = stormpy.model_checking(model, properties[0]) print(result) diff --git a/examples/04-getting-started.py b/examples/04-getting-started.py index e1fcd66..ca281a2 100644 --- a/examples/04-getting-started.py +++ b/examples/04-getting-started.py @@ -10,7 +10,7 @@ def example_getting_started_04(): 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) + properties = stormpy.parse_properties(formula_str, prism_program) model = stormpy.build_model(prism_program, properties) print(model.model_type) diff --git a/examples/analysis/01-analysis.py b/examples/analysis/01-analysis.py index ec32723..204512c 100644 --- a/examples/analysis/01-analysis.py +++ b/examples/analysis/01-analysis.py @@ -10,7 +10,7 @@ def example_analysis_01(): 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) + properties = stormpy.parse_properties(formula_str, prism_program) model = stormpy.build_model(prism_program, properties) prob0E, prob1A = stormpy.prob01min_states(model, properties[0].raw_formula.subformula) print(prob0E) diff --git a/examples/exploration/01-exploration.py b/examples/exploration/01-exploration.py index fd22d2e..cc48d13 100644 --- a/examples/exploration/01-exploration.py +++ b/examples/exploration/01-exploration.py @@ -12,7 +12,7 @@ def example_exploration_01(): """ program = stormpy.parse_prism_program(stormpy.examples.files.prism_pomdp_maze) prop = "R=? [F \"goal\"]" - properties = stormpy.parse_properties_for_prism_program(prop, program, None) + properties = stormpy.parse_properties(prop, program) model = stormpy.build_model(program, properties) print(model.model_type) diff --git a/examples/exploration/02-exploration.py b/examples/exploration/02-exploration.py index 951a29a..14ab63c 100644 --- a/examples/exploration/02-exploration.py +++ b/examples/exploration/02-exploration.py @@ -12,7 +12,7 @@ def example_exploration_02(): """ program = stormpy.parse_prism_program(stormpy.examples.files.prism_pomdp_maze) prop = "R=? [F \"goal\"]" - properties = stormpy.parse_properties_for_prism_program(prop, program, None) + properties = stormpy.parse_properties(prop, program) model = stormpy.build_model(program, properties) print(model.model_type) # Internally, POMDPs are just MDPs with additional observation information. diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 368fbcb..5c66ad8 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -443,3 +443,25 @@ def construct_submodel(model, states, actions, keep_unreachable_states=True, opt return core._construct_subsystem_double(model, states, actions, keep_unreachable_states, options) else: raise NotImplementedError() + +def parse_properties(properties, context = None, filters = None): + """ + + :param properties: A string with the pctl properties + :param context: A symbolic model that gives meaning to variables and constants. + :param filters: filters, if applicable. + :return: A list of properties + """ + if context is None: + return core.parse_properties_without_context(properties, filters) + elif type(context) == core.SymbolicModelDescription: + if context.is_prism_program(): + return core.parse_properties_for_prism_program(properties, context.as_prism_program(), filters) + else: + core.parse_properties_for_prism_program(properties, context.as_jani_model(), filters) + elif type(context) == storage.PrismProgram: + return core.parse_properties_for_prism_program(properties, context, filters) + elif type(context) == storage.JaniModel: + core.parse_properties_for_jani_model(properties, context, filters) + else: + raise StormError("Unclear context. Please pass a symbolic model description") diff --git a/src/core/core.cpp b/src/core/core.cpp index 67a0c24..b1619fe 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -30,7 +30,7 @@ void define_core(py::module& m) { void define_parse(py::module& m) { // Parse formulas - m.def("parse_properties", [](std::string const& inputString, boost::optional> const& propertyFilter = boost::none) { + m.def("parse_properties_without_context", [](std::string const& inputString, boost::optional> const& propertyFilter = boost::none) { return storm::api::parseProperties(inputString, propertyFilter); }, R"dox(