From a89c9711bffdba58baa39b30c331f72f9b91a237 Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Fri, 11 Aug 2023 14:27:15 +0200 Subject: [PATCH] changes after shield filename removal --- examples/shields/01_pre_shield_extraction.py | 2 +- examples/shields/02_post_shield_extraction.py | 2 +- .../shields/03_optimal_shield_extraction.py | 2 +- examples/shields/04_pre_shield_export.py | 2 +- examples/shields/05_post_shield_export.py | 2 +- examples/shields/06_optimal_shield_export.py | 2 +- examples/shields/07_pre_shield_simulator.py | 2 +- examples/shields/08_post_shield_simulator.py | 2 +- examples/shields/09_pre_shield_decision_tree.py | 17 ++++++++--------- .../shields/10_post_shield_decision_tree.py | 2 +- src/logic/formulae.cpp | 4 ++-- 11 files changed, 19 insertions(+), 20 deletions(-) diff --git a/examples/shields/01_pre_shield_extraction.py b/examples/shields/01_pre_shield_extraction.py index 8a83fb0..057ae7a 100644 --- a/examples/shields/01_pre_shield_extraction.py +++ b/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 diff --git a/examples/shields/02_post_shield_extraction.py b/examples/shields/02_post_shield_extraction.py index 6bb0128..8d0911e 100644 --- a/examples/shields/02_post_shield_extraction.py +++ b/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 = " Pmax=? [G !\"AgentIsInLavaAndNotDone\"]" + formula_str = " Pmax=? [G !\"AgentIsInLavaAndNotDone\"]" program = stormpy.parse_prism_program(path) formulas = stormpy.parse_properties_for_prism_program(formula_str, program) diff --git a/examples/shields/03_optimal_shield_extraction.py b/examples/shields/03_optimal_shield_extraction.py index ffdb009..48ccfa7 100644 --- a/examples/shields/03_optimal_shield_extraction.py +++ b/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 = " <> R{\"travel_costs\"}min=? [ LRA ]" + formula_str = " <> R{\"travel_costs\"}min=? [ LRA ]" program = stormpy.parse_prism_program(path) formulas = stormpy.parse_properties_for_prism_program(formula_str, program) diff --git a/examples/shields/04_pre_shield_export.py b/examples/shields/04_pre_shield_export.py index 83b9fa7..0231e06 100644 --- a/examples/shields/04_pre_shield_export.py +++ b/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 = " Pmax=? [G !\"AgentIsInLavaAndNotDone\"]" + formula_str = " Pmax=? [G !\"AgentIsInLavaAndNotDone\"]" program = stormpy.parse_prism_program(path) formulas = stormpy.parse_properties_for_prism_program(formula_str, program) diff --git a/examples/shields/05_post_shield_export.py b/examples/shields/05_post_shield_export.py index d678dff..074fb01 100644 --- a/examples/shields/05_post_shield_export.py +++ b/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 = " Pmax=? [G !\"AgentIsInLavaAndNotDone\"]" + formula_str = " Pmax=? [G !\"AgentIsInLavaAndNotDone\"]" program = stormpy.parse_prism_program(path) formulas = stormpy.parse_properties_for_prism_program(formula_str, program) diff --git a/examples/shields/06_optimal_shield_export.py b/examples/shields/06_optimal_shield_export.py index ddf1453..64cee76 100644 --- a/examples/shields/06_optimal_shield_export.py +++ b/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 = " <> R{\"differenceWithInterferenceCost\"}min=? [ LRA ]" + formula_str = " <> R{\"differenceWithInterferenceCost\"}min=? [ LRA ]" program = stormpy.parse_prism_program(path) formulas = stormpy.parse_properties_for_prism_program(formula_str, program) diff --git a/examples/shields/07_pre_shield_simulator.py b/examples/shields/07_pre_shield_simulator.py index b4167a5..aa5def1 100644 --- a/examples/shields/07_pre_shield_simulator.py +++ b/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 = " Pmax=? [G !\"AgentIsInLavaAndNotDone\"]" + formula_str = " Pmax=? [G !\"AgentIsInLavaAndNotDone\"]" program = stormpy.parse_prism_program(path) formulas = stormpy.parse_properties_for_prism_program(formula_str, program) diff --git a/examples/shields/08_post_shield_simulator.py b/examples/shields/08_post_shield_simulator.py index 5f51c99..36287c7 100644 --- a/examples/shields/08_post_shield_simulator.py +++ b/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 = " Pmax=? [G !\"AgentIsInLavaAndNotDone\"]; Pmax=? [ F \"AgentIsInLavaAndNotDone\" ];" + formula_str = " Pmax=? [G !\"AgentIsInLavaAndNotDone\"]; Pmax=? [ F \"AgentIsInLavaAndNotDone\" ];" program = stormpy.parse_prism_program(path) formulas = stormpy.parse_properties_for_prism_program(formula_str, program) diff --git a/examples/shields/09_pre_shield_decision_tree.py b/examples/shields/09_pre_shield_decision_tree.py index 7c67809..1b757a8 100644 --- a/examples/shields/09_pre_shield_decision_tree.py +++ b/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 = " Pmax=? [G !\"AgentIsInLavaAndNotDone\"]" + formula_str = " 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__': diff --git a/examples/shields/10_post_shield_decision_tree.py b/examples/shields/10_post_shield_decision_tree.py index ebaf5be..e232b9c 100644 --- a/examples/shields/10_post_shield_decision_tree.py +++ b/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 = " Pmax=? [G !\"AgentIsInLavaAndNotDone\"]" + formula_str = " Pmax=? [G !\"AgentIsInLavaAndNotDone\"]" program = stormpy.parse_prism_program(path) formulas = stormpy.parse_properties_for_prism_program(formula_str, program) diff --git a/src/logic/formulae.cpp b/src/logic/formulae.cpp index 63bd7c4..8afea82 100644 --- a/src/logic/formulae.cpp +++ b/src/logic/formulae.cpp @@ -114,8 +114,8 @@ void define_formulae(py::module& m) { py::class_>(m, "BooleanBinaryStateFormula", "Boolean binary state formula", binaryStateFormula); py::class_>(m, "ShieldExpression") - .def(py::init(), py::arg("type"), py::arg("filename")) - .def(py::init(), py::arg("type"), py::arg("filename"), py::arg("comparison"), py::arg("value")) + .def(py::init(), py::arg("type")) + .def(py::init(), 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)