added shield_expression parameter for

model checking call

examples/shields/01_pre_shield_extraction.py

@@ -4,6 +4,7 @@ import stormpy.simulator
 
 
 import stormpy.shields
+import stormpy.logic
 
 import stormpy.examples
 import stormpy.examples.files
@@ -31,8 +32,11 @@ def pre_shield_extraction():
 
     initial_state = model.initial_states[0]
     assert initial_state == 0
-    #shield_specification = ShieldingExpression(type="PreSafety", gamma=0.8) TODO Parameter for shield expression would be nice to have
-    result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) #, shielding_expression=shield_specification)
+    test = formulas[0].shielding_expression
+    print(test)
+    shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.PRE_SAFETY, "pre", stormpy.logic.ShieldComparison.RELATIVE, 0.9) #TODO Parameter for shield expression would be nice to have
+    result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification) #, shielding_expression=shield_specification)
+    
     assert result.has_scheduler
     assert result.has_shield
     

lib/stormpy/__init__.py

@@ -256,7 +256,7 @@ def perform_symbolic_bisimulation(model, properties):
         return core._perform_symbolic_bisimulation(model, formulae, bisimulation_type)
 
 
-def model_checking(model, property, only_initial_states=False, extract_scheduler=False, force_fully_observable=False, environment=Environment()):
+def model_checking(model, property, only_initial_states=False, extract_scheduler=False, force_fully_observable=False, environment=Environment(), shield_expression=None):
     """
     Perform model checking on model for property.
     :param model: Model.
@@ -268,7 +268,7 @@ def model_checking(model, property, only_initial_states=False, extract_scheduler
     """
     if model.is_sparse_model:
         return check_model_sparse(model, property, only_initial_states=only_initial_states,
-                                  extract_scheduler=extract_scheduler, force_fully_observable=force_fully_observable, environment=environment)
+                                  extract_scheduler=extract_scheduler, force_fully_observable=force_fully_observable, environment=environment, shield_expression=shield_expression)
     else:
         assert (model.is_symbolic_model)
         if extract_scheduler:
@@ -277,7 +277,7 @@ def model_checking(model, property, only_initial_states=False, extract_scheduler
                               environment=environment)
 
 
-def check_model_sparse(model, property, only_initial_states=False, extract_scheduler=False, force_fully_observable=False, environment=Environment()):
+def check_model_sparse(model, property, only_initial_states=False, extract_scheduler=False, force_fully_observable=False, environment=Environment(), shield_expression=None):
     """
     Perform model checking on model for property.
     :param model: Model.
@@ -323,9 +323,12 @@ def check_model_sparse(model, property, only_initial_states=False, extract_sched
             task = core.CheckTask(formula, only_initial_states)
             task.set_produce_schedulers(extract_scheduler)
 
-            if property.is_shielding_property():
+            if shield_expression is not None:
+                task.set_shielding_expression(shield_expression)
+            elif property.is_shielding_property():
                 task.set_shielding_expression(property.shielding_expression)
 
+
             return core._model_checking_sparse_engine(model, task, environment=environment)
 
 

src/logic/formulae.cpp

@@ -14,6 +14,18 @@ void define_formulae(py::module& m) {
         .value("GEQ", storm::logic::ComparisonType::GreaterEqual)
     ;
 
+    py::enum_<storm::logic::ShieldingType>(m, "ShieldingType")
+        .value("POST_SAFETY", storm::logic::ShieldingType::PostSafety)
+        .value("PRE_SAFETY", storm::logic::ShieldingType::PreSafety)
+        .value("OPTIMAL_PRE", storm::logic::ShieldingType::OptimalPre)
+        .value("OPTIMAL_POST", storm::logic::ShieldingType::OptimalPost)
+    ;
+
+    py::enum_<storm::logic::ShieldComparison>(m, "ShieldComparison")
+        .value("ABSOLUTE", storm::logic::ShieldComparison::Absolute)
+        .value("RELATIVE", storm::logic::ShieldComparison::Relative)
+    ;
+
     py::class_<storm::logic::Formula, std::shared_ptr<storm::logic::Formula>> formula(m, "Formula", "Generic Storm Formula");
     formula.def("__str__", &storm::logic::Formula::toString)
         .def("clone", [](storm::logic::Formula const& f) { storm::logic::CloneVisitor cv; return cv.clone(f);})
@@ -100,5 +112,16 @@ void define_formulae(py::module& m) {
             .def_property_readonly("reward_name", &storm::logic::RewardOperatorFormula::getRewardModelName);
     py::class_<storm::logic::BinaryStateFormula, std::shared_ptr<storm::logic::BinaryStateFormula>> binaryStateFormula(m, "BinaryStateFormula", "State formula with two operands", stateFormula);
     py::class_<storm::logic::BinaryBooleanStateFormula, std::shared_ptr<storm::logic::BinaryBooleanStateFormula>>(m, "BooleanBinaryStateFormula", "Boolean binary state formula", binaryStateFormula);
-    py::class_<storm::logic::ShieldExpression, std::shared_ptr<storm::logic::ShieldExpression>>(m, "ShieldExpression");
+    
+    py::class_<storm::logic::ShieldExpression, std::shared_ptr<storm::logic::ShieldExpression>>(m, "ShieldExpression")
+        .def(py::init<storm::logic::ShieldingType, std::string>(), py::arg("type"), py::arg("filename"))
+        .def(py::init<storm::logic::ShieldingType, std::string, storm::logic::ShieldComparison, double>(), py::arg("type"), py::arg("filename"), py::arg("comparison"), py::arg("value"))
+        .def("is_relative", &storm::logic::ShieldExpression::isRelative)
+        .def("is_pre_safety_shield", &storm::logic::ShieldExpression::isPreSafetyShield)
+        .def("is_post_safety_shield", &storm::logic::ShieldExpression::isPostSafetyShield)
+        .def("is_optimal_shield", &storm::logic::ShieldExpression::isOptimalShield)
+        .def("is_optimal_pre_shield", &storm::logic::ShieldExpression::isOptimalPreShield)
+        .def("is_optimal_post_shield", &storm::logic::ShieldExpression::isOptimalPostShield)
+        .def_property_readonly("value", &storm::logic::ShieldExpression::getValue, "shield value")
+    ;
 }