diff --git a/examples/shields/01_pre_shield_extraction.py b/examples/shields/01_pre_shield_extraction.py index 057ae7a..72b9903 100644 --- a/examples/shields/01_pre_shield_extraction.py +++ b/examples/shields/01_pre_shield_extraction.py @@ -32,18 +32,18 @@ def pre_shield_extraction(): initial_state = model.initial_states[0] assert initial_state == 0 - test = formulas[0].shielding_expression - print(test) - 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) + + shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.PRE_SAFETY, stormpy.logic.ShieldComparison.RELATIVE, 0.9) + result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification) assert result.has_scheduler assert result.has_shield shield = result.shield + pre_scheduler = shield.construct() for state_id in model.states: - choices = shield.construct().get_choice(state_id) + choices = pre_scheduler.get_choice(state_id) print(F"Allowed choices in state {state_id}, are {choices.choice_map} ") diff --git a/examples/shields/02_post_shield_extraction.py b/examples/shields/02_post_shield_extraction.py index 8d0911e..cbb305c 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) @@ -33,14 +33,17 @@ def post_shield_extraction(): initial_state = model.initial_states[0] assert initial_state == 0 - result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) + + shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.POST_SAFETY, stormpy.logic.ShieldComparison.RELATIVE, 0.9) + result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification) assert result.has_scheduler assert result.has_shield shield = result.shield + post_scheduler = shield.construct() for state_id in model.states: - choices = shield.construct().get_choice(state_id) + choices = post_scheduler.get_choice(state_id) print(F"Applied corrections in state {state_id}, are {choices.choice_map} ") diff --git a/examples/shields/03_optimal_shield_extraction.py b/examples/shields/03_optimal_shield_extraction.py index 48ccfa7..a39679e 100644 --- a/examples/shields/03_optimal_shield_extraction.py +++ b/examples/shields/03_optimal_shield_extraction.py @@ -22,17 +22,19 @@ def optimal_shield_extraction(): options.set_build_all_labels() model = stormpy.build_sparse_model_with_options(program, options) - result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) - + shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.OPTIMAL) + result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification) + assert result.has_scheduler assert result.has_shield shield = result.shield state_ids = [x for x in model.states] + scheduler = shield.construct() for state_id in state_ids[0:50]: - choices = shield.construct().get_choice(state_id) + choices = scheduler.get_choice(state_id) print(F"Corrections in state {state_id}, are {choices.choice_map} ") diff --git a/examples/shields/04_pre_shield_export.py b/examples/shields/04_pre_shield_export.py index 0231e06..b462d41 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) @@ -30,7 +30,10 @@ def pre_schield(): initial_state = model.initial_states[0] assert initial_state == 0 - result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) + + shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.PRE_SAFETY, stormpy.logic.ShieldComparison.Absolute, 0.9) + result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification) + assert result.has_scheduler assert result.has_shield diff --git a/examples/shields/05_post_shield_export.py b/examples/shields/05_post_shield_export.py index 074fb01..5fa13e0 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) @@ -30,7 +30,8 @@ def pre_schield(): initial_state = model.initial_states[0] assert initial_state == 0 - result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) + shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.POST_SAFETY, stormpy.logic.ShieldComparison.RELATIVE, 0.9) + result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification) assert result.has_scheduler assert result.has_shield diff --git a/examples/shields/06_optimal_shield_export.py b/examples/shields/06_optimal_shield_export.py index 64cee76..34b17b3 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) @@ -27,7 +27,8 @@ def optimal_shield_export(): options.set_build_all_labels() model = stormpy.build_sparse_model_with_options(program, options) - result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) + shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.OPTIMAL) + result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification) assert result.has_scheduler assert result.has_shield diff --git a/examples/shields/07_pre_shield_simulator.py b/examples/shields/07_pre_shield_simulator.py index aa5def1..eacdffe 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) @@ -28,7 +28,10 @@ def example_pre_shield_simulator(): initial_state = model.initial_states[0] assert initial_state == 0 - result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) + + shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.PRE_SAFETY, stormpy.logic.ShieldComparison.RELATIVE, 0.9) + result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification) + assert result.has_scheduler assert result.has_shield diff --git a/examples/shields/08_post_shield_simulator.py b/examples/shields/08_post_shield_simulator.py index 36287c7..76acb08 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) @@ -27,7 +27,8 @@ def example_post_shield_simulator(): initial_state = model.initial_states[0] assert initial_state == 0 - result = stormpy.model_checking(model, formulas[0]) + shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.POST_SAFETY, stormpy.logic.ShieldComparison.RELATIVE, 0.9) + result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification) result2 = stormpy.model_checking(model, formulas[1], extract_scheduler=True) assert result.has_shield diff --git a/examples/shields/09_pre_shield_decision_tree.py b/examples/shields/09_pre_shield_decision_tree.py index 1b757a8..de8764f 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) @@ -34,8 +34,9 @@ def export_shield_as_dot(): options.set_build_with_choice_origins(True) model = stormpy.build_sparse_model_with_options(program, options) - result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) - + shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.PRE_SAFETY, stormpy.logic.ShieldComparison.RELATIVE, 0.9) + result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification) + assert result.has_shield shield = result.shield diff --git a/examples/shields/10_post_shield_decision_tree.py b/examples/shields/10_post_shield_decision_tree.py index e232b9c..cdde8bb 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) @@ -24,7 +24,8 @@ def export_shield_as_dot(): options.set_build_with_choice_origins(True) model = stormpy.build_sparse_model_with_options(program, options) - result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) + shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.POST_SAFETY, stormpy.logic.ShieldComparison.RELATIVE, 0.9) + result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification) assert result.has_shield diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 673d3e9..5ead8bb 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -324,10 +324,7 @@ def check_model_sparse(model, property, only_initial_states=False, extract_sched task.set_produce_schedulers(extract_scheduler) if shield_expression is not None: - task.set_shielding_expression(shield_expression) - elif property.is_shielding_property(): - task.set_shielding_expression(property.shielding_expression) - + task.set_shielding_expression(shield_expression) return core._model_checking_sparse_engine(model, task, environment=environment) diff --git a/src/core/core.cpp b/src/core/core.cpp index 8b2e9cd..a751f0e 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -119,9 +119,9 @@ void define_build(py::module& m) { m.def("_build_sparse_parametric_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the parametric model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions()); m.def("build_sparse_model_from_explicit", &storm::api::buildExplicitModel, "Build the model model from explicit input", py::arg("transition_file"), py::arg("labeling_file"), py::arg("state_reward_file") = "", py::arg("transition_reward_file") = "", py::arg("choice_labeling_file") = ""); - m.def("make_sparse_model_builder", &storm::api::makeExplicitModelBuilder, "Construct a builder instance", py::arg("model_description"), py::arg("options"), py::arg("action_mask")); - m.def("make_sparse_model_builder_exact", &storm::api::makeExplicitModelBuilder, "Construct a builder instance", py::arg("model_description"), py::arg("options"), py::arg("action_mask")); - m.def("make_sparse_model_builder_parametric", &storm::api::makeExplicitModelBuilder, "Construct a builder instance", py::arg("model_description"), py::arg("options"), py::arg("action_mask")); + m.def("make_sparse_model_builder", &storm::api::makeExplicitModelBuilder, "Construct a builder instance", py::arg("model_description"), py::arg("options"), py::arg("action_mask") = nullptr); + m.def("make_sparse_model_builder_exact", &storm::api::makeExplicitModelBuilder, "Construct a builder instance", py::arg("model_description"), py::arg("options"), py::arg("action_mask") = nullptr); + m.def("make_sparse_model_builder_parametric", &storm::api::makeExplicitModelBuilder, "Construct a builder instance", py::arg("model_description"), py::arg("options"), py::arg("action_mask") = nullptr); py::class_>(m, "ExplicitModelBuilder", "Model builder for sparse models") .def("build", &storm::builder::ExplicitModelBuilder::build, "Build the model") @@ -150,6 +150,9 @@ void define_build(py::module& m) { .def("set_build_choice_labels", &storm::builder::BuilderOptions::setBuildChoiceLabels, "Build with choice labels", py::arg("new_value")=true) .def("set_build_all_labels" , &storm::builder::BuilderOptions::setBuildAllLabels, "Build with all state labels", py::arg("new_value")=true) .def("set_build_all_reward_models", &storm::builder::BuilderOptions::setBuildAllRewardModels, "Build with all reward models", py::arg("new_value")=true); + + + py::class_, std::shared_ptr>> actionmask(m, "ActionMaskDouble"); } void define_optimality_type(py::module& m) { diff --git a/src/dft/analysis.cpp b/src/dft/analysis.cpp index 544d2f3..e15098b 100644 --- a/src/dft/analysis.cpp +++ b/src/dft/analysis.cpp @@ -9,8 +9,8 @@ // Thin wrapper for DFT analysis template -std::vector analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents) { - typename storm::modelchecker::DFTModelChecker::dft_results dftResults = storm::api::analyzeDFT(dft, properties, symred, allowModularisation, relevantEvents, 0.0, storm::builder::ApproximationHeuristic::DEPTH, false); +std::vector analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents, bool allowDCForRelevant) { + typename storm::modelchecker::DFTModelChecker::dft_results dftResults = storm::api::analyzeDFT(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevant ,0.0, storm::builder::ApproximationHeuristic::DEPTH, false); std::vector results; for (auto result : dftResults) { @@ -27,7 +27,7 @@ void define_analysis(py::module& m) { .def("is_relevant", &storm::utility::RelevantEvents::isRelevant, "Check whether the given name is a relevant event", py::arg("name")) ; - m.def("analyze_dft", &analyzeDFT, "Analyze the DFT", py::arg("dft"), py::arg("properties"), py::arg("symred")=true, py::arg("allow_modularisation")=false, py::arg("relevant_events")=storm::utility::RelevantEvents()); + m.def("analyze_dft", &analyzeDFT, "Analyze the DFT", py::arg("dft"), py::arg("properties"), py::arg("symred")=true, py::arg("allow_modularisation")=false, py::arg("relevant_events")=storm::utility::RelevantEvents(), py::arg("allow_dc_for_relevant")=false); m.def("transform_dft", &storm::api::applyTransformations, "Apply transformations on DFT", py::arg("dft"), py::arg("unique_constant_be"), py::arg("binary_fdeps")); @@ -35,5 +35,5 @@ void define_analysis(py::module& m) { m.def("is_well_formed", &storm::api::isWellFormed, "Check whether DFT is well-formed.", py::arg("dft"), py::arg("check_valid_for_analysis") = true); - m.def("compute_relevant_events", &storm::api::computeRelevantEvents, "Compute relevant event ids from properties and additional relevant names", py::arg("dft"), py::arg("properties"), py::arg("additional_relevant_names") = std::vector(), py::arg("allow_dc_relevant") = false); + m.def("compute_relevant_events", &storm::api::computeRelevantEvents, "Compute relevant event ids from properties and additional relevant names", py::arg("dft"), py::arg("properties"), py::arg("additional_relevant_names") = std::vector()); } diff --git a/src/logic/formulae.cpp b/src/logic/formulae.cpp index 8afea82..1a7eaf8 100644 --- a/src/logic/formulae.cpp +++ b/src/logic/formulae.cpp @@ -19,6 +19,7 @@ void define_formulae(py::module& m) { .value("PRE_SAFETY", storm::logic::ShieldingType::PreSafety) .value("OPTIMAL_PRE", storm::logic::ShieldingType::OptimalPre) .value("OPTIMAL_POST", storm::logic::ShieldingType::OptimalPost) + .value("OPTIMAL", storm::logic::ShieldingType::OptimalPost) ; py::enum_(m, "ShieldComparison")