changes after shield filename removal

examples/shields/01_pre_shield_extraction.py

@@ -34,7 +34,7 @@ def pre_shield_extraction():
     assert initial_state == 0
     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
+    shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.PRE_SAFETY, 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

examples/shields/02_post_shield_extraction.py

@@ -20,7 +20,7 @@ for allowed actions.
 
 def post_shield_extraction():
     path = stormpy.examples.files.prism_mdp_lava_simple
-    formula_str = "<ShieldFileName, PostSafety, gamma=0.9> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
+    formula_str = "<PostSafety, gamma=0.9> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
 
     program = stormpy.parse_prism_program(path)
     formulas = stormpy.parse_properties_for_prism_program(formula_str, program)

examples/shields/03_optimal_shield_extraction.py

@@ -11,7 +11,7 @@ import stormpy.examples.files
 
 def optimal_shield_extraction():
     path = stormpy.examples.files.prism_smg_robot
-    formula_str = "<path_correction, Optimal> <<sh>> R{\"travel_costs\"}min=? [ LRA ]"
+    formula_str = "<Optimal> <<sh>> R{\"travel_costs\"}min=? [ LRA ]"
 
     program = stormpy.parse_prism_program(path)
     formulas = stormpy.parse_properties_for_prism_program(formula_str, program)

examples/shields/04_pre_shield_export.py

@@ -17,7 +17,7 @@ to a file
 
 def pre_schield():
     path = stormpy.examples.files.prism_mdp_lava_simple
-    formula_str = "<pre, PreSafety, lambda=0.9> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
+    formula_str = "<PreSafety, lambda=0.9> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
 
     program = stormpy.parse_prism_program(path)
     formulas = stormpy.parse_properties_for_prism_program(formula_str, program)

examples/shields/05_post_shield_export.py

@@ -17,7 +17,7 @@ to a file
 
 def pre_schield():
     path = stormpy.examples.files.prism_mdp_lava_simple
-    formula_str = "<post, PostSafety, gamma=1> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
+    formula_str = "<PostSafety, gamma=1> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
 
     program = stormpy.parse_prism_program(path)
     formulas = stormpy.parse_properties_for_prism_program(formula_str, program)

examples/shields/06_optimal_shield_export.py

@@ -16,7 +16,7 @@ to a file
 
 def optimal_shield_export():
     path = stormpy.examples.files.prism_smg_lights
-    formula_str = "<optimal, Optimal> <<shield>> R{\"differenceWithInterferenceCost\"}min=? [ LRA ]"
+    formula_str = "<Optimal> <<shield>> R{\"differenceWithInterferenceCost\"}min=? [ LRA ]"
 
     program = stormpy.parse_prism_program(path)
     formulas = stormpy.parse_properties_for_prism_program(formula_str, program)

examples/shields/07_pre_shield_simulator.py

@@ -15,7 +15,7 @@ Simulating a model with the usage of a pre shield
 
 def example_pre_shield_simulator():
     path = stormpy.examples.files.prism_mdp_cliff_walking
-    formula_str = "<ShieldFileName, PreSafety, lambda=0.9> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
+    formula_str = "<PreSafety, lambda=0.9> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
 
     program = stormpy.parse_prism_program(path)
     formulas = stormpy.parse_properties_for_prism_program(formula_str, program)

examples/shields/08_post_shield_simulator.py

@@ -14,7 +14,7 @@ Simulating a model with the usage of a post shield
 
 def example_post_shield_simulator():
     path = stormpy.examples.files.prism_mdp_lava_simple
-    formula_str = "<ShieldFileName, PostSafety, gamma=0.9> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]; Pmax=? [ F \"AgentIsInLavaAndNotDone\" ];"
+    formula_str = "<PostSafety, gamma=0.9> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]; Pmax=? [ F \"AgentIsInLavaAndNotDone\" ];"
 
     program = stormpy.parse_prism_program(path)
     formulas = stormpy.parse_properties_for_prism_program(formula_str, program)

examples/shields/09_pre_shield_decision_tree.py

@@ -22,7 +22,7 @@ from stormpy.decision_tree import create_decision_tree
 
 def export_shield_as_dot():
     path = stormpy.examples.files.prism_mdp_lava_simple
-    formula_str = "<pre, PreSafety, lambda=0.9> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
+    formula_str = "<PreSafety, lambda=0.9> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
 
     program = stormpy.parse_prism_program(path)
     formulas = stormpy.parse_properties_for_prism_program(formula_str, program)
@@ -41,17 +41,16 @@ def export_shield_as_dot():
     shield = result.shield
     filename = "preshield.storm.json"
     stormpy.shields.export_shield(model, shield, filename)
-
-    if classifiers is None:        
-        aa = AxisAlignedSplittingStrategy()
-        aa.priority = 1      
-
-        classifiers = [DecisionTree([aa], Entropy(), name)]
-
     
     output_folder = "pre_trees"
     name = 'pre_my_output'
-    suite = create_decision_tree(filename, name=name , output_folder=output_folder, export_pdf=True)
+
+    aa = AxisAlignedSplittingStrategy()
+    aa.priority = 1      
+
+    classifiers = [DecisionTree([aa], Entropy(), name)]
+
+    suite = create_decision_tree(filename, name=name , output_folder=output_folder, export_pdf=True, classifiers=classifiers)
     suite.display_html()
 
 if __name__ == '__main__':

examples/shields/10_post_shield_decision_tree.py

@@ -12,7 +12,7 @@ from stormpy.decision_tree import create_decision_tree
 
 def export_shield_as_dot():
     path = stormpy.examples.files.prism_mdp_lava_simple
-    formula_str = "<post, PostSafety, gamma=1> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
+    formula_str = "<PostSafety, gamma=1> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
 
     program = stormpy.parse_prism_program(path)
     formulas = stormpy.parse_properties_for_prism_program(formula_str, program)

src/logic/formulae.cpp

@@ -114,8 +114,8 @@ void define_formulae(py::module& m) {
     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")
-        .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(py::init<storm::logic::ShieldingType>(), py::arg("type"))
+        .def(py::init<storm::logic::ShieldingType, storm::logic::ShieldComparison, double>(), py::arg("type"), 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)