From 08e389a9dadf58aa94304e5a55c4bdea5614d5ca Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Fri, 11 Aug 2023 10:40:08 +0200 Subject: [PATCH] added shield_expression parameter for model checking call --- examples/shields/01_pre_shield_extraction.py | 8 +++++-- lib/stormpy/__init__.py | 11 +++++---- src/logic/formulae.cpp | 25 +++++++++++++++++++- 3 files changed, 37 insertions(+), 7 deletions(-) diff --git a/examples/shields/01_pre_shield_extraction.py b/examples/shields/01_pre_shield_extraction.py index 4b24a85..8a83fb0 100644 --- a/examples/shields/01_pre_shield_extraction.py +++ b/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 diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index af8c27c..673d3e9 100644 --- a/lib/stormpy/__init__.py +++ b/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) diff --git a/src/logic/formulae.cpp b/src/logic/formulae.cpp index e011e55..63bd7c4 100644 --- a/src/logic/formulae.cpp +++ b/src/logic/formulae.cpp @@ -14,6 +14,18 @@ void define_formulae(py::module& m) { .value("GEQ", storm::logic::ComparisonType::GreaterEqual) ; + py::enum_(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_(m, "ShieldComparison") + .value("ABSOLUTE", storm::logic::ShieldComparison::Absolute) + .value("RELATIVE", storm::logic::ShieldComparison::Relative) + ; + py::class_> 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_> binaryStateFormula(m, "BinaryStateFormula", "State formula with two operands", stateFormula); py::class_>(m, "BooleanBinaryStateFormula", "Boolean binary state formula", binaryStateFormula); - py::class_>(m, "ShieldExpression"); + + 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("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") + ; }