generic parse_properties for simpler code

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))
     <class 'stormpy.storage.storage.SparseDtmc'>

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:

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
 

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:

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])
     

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))

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)

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)

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)

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)
 

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.

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")

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<std::set<std::string>> const& propertyFilter = boost::none) {
+    m.def("parse_properties_without_context", [](std::string const& inputString, boost::optional<std::set<std::string>> const& propertyFilter = boost::none) {
                 return storm::api::parseProperties(inputString, propertyFilter);
             }, R"dox(