From fa533af4c41669a0ba04c7b88a658d76c7e79087 Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Mon, 7 Aug 2023 09:50:02 +0200 Subject: [PATCH] added basic shield export functionality --- lib/stormpy/__init__.py | 4 ++++ src/core/input.cpp | 2 ++ src/core/modelchecking.cpp | 3 +++ src/logic/formulae.cpp | 3 ++- src/mod_shields.cpp | 1 + src/shields/abstract_shield.cpp | 2 +- src/shields/optimal_shield.cpp | 2 +- src/shields/post_shield.cpp | 2 +- src/shields/pre_shield.cpp | 3 ++- src/shields/shield_handling.cpp | 3 ++- 10 files changed, 19 insertions(+), 6 deletions(-) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index c47377c..af8c27c 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -322,6 +322,10 @@ def check_model_sparse(model, property, only_initial_states=False, extract_sched else: task = core.CheckTask(formula, only_initial_states) task.set_produce_schedulers(extract_scheduler) + + if 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/core/input.cpp b/src/core/input.cpp index 72a5e40..52dd9d0 100644 --- a/src/core/input.cpp +++ b/src/core/input.cpp @@ -9,6 +9,8 @@ void define_property(py::module& m) { .def(py::init()) .def_property_readonly("name", &storm::jani::Property::getName, "Obtain the name of the property") .def_property_readonly("raw_formula", &storm::jani::Property::getRawFormula, "Obtain the formula directly") + .def_property_readonly("shielding_expression", &storm::jani::Property::getShieldingExpression, "Obtain the shielding expression") + .def("is_shielding_property", &storm::jani::Property::isShieldingProperty, "Is the property a shielding property?") .def("__str__", &streamToString) ; } diff --git a/src/core/modelchecking.cpp b/src/core/modelchecking.cpp index 7175568..b326b1a 100644 --- a/src/core/modelchecking.cpp +++ b/src/core/modelchecking.cpp @@ -65,17 +65,20 @@ void define_modelchecking(py::module& m) { //m.def("create_check_task", &storm::api::createTask, "Create task for verification", py::arg("formula"), py::arg("only_initial_states") = false); .def(py::init(), py::arg("formula"), py::arg("only_initial_states") = false) .def("set_produce_schedulers", &CheckTask::setProduceSchedulers, "Set whether schedulers should be produced (if possible)", py::arg("produce_schedulers") = true) + .def("set_shielding_expression", &CheckTask::setShieldingExpression, py::arg("expr")) ; // CheckTask py::class_, std::shared_ptr>>(m, "ExactCheckTask", "Task for model checking with exact numbers") //m.def("create_check_task", &storm::api::createTask, "Create task for verification", py::arg("formula"), py::arg("only_initial_states") = false); .def(py::init(), py::arg("formula"), py::arg("only_initial_states") = false) .def("set_produce_schedulers", &CheckTask::setProduceSchedulers, "Set whether schedulers should be produced (if possible)", py::arg("produce_schedulers") = true) + .def("set_shielding_expression", &CheckTask::setShieldingExpression, py::arg("expr")) ; py::class_, std::shared_ptr>>(m, "ParametricCheckTask", "Task for parametric model checking") //m.def("create_check_task", &storm::api::createTask, "Create task for verification", py::arg("formula"), py::arg("only_initial_states") = false); .def(py::init(), py::arg("formula"), py::arg("only_initial_states") = false) .def("set_produce_schedulers", &CheckTask::setProduceSchedulers, "Set whether schedulers should be produced (if possible)", py::arg("produce_schedulers") = true) + .def("set_shielding_expression", &CheckTask::setShieldingExpression, py::arg("expr")) ; // Model checking diff --git a/src/logic/formulae.cpp b/src/logic/formulae.cpp index 69f87e3..e011e55 100644 --- a/src/logic/formulae.cpp +++ b/src/logic/formulae.cpp @@ -2,7 +2,7 @@ #include "storm/logic/Formulas.h" #include "storm/logic/CloneVisitor.h" #include "storm/logic/LabelSubstitutionVisitor.h" - +#include "storm/logic/ShieldExpression.h" void define_formulae(py::module& m) { @@ -100,4 +100,5 @@ 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"); } diff --git a/src/mod_shields.cpp b/src/mod_shields.cpp index 0cab87c..7d76991 100644 --- a/src/mod_shields.cpp +++ b/src/mod_shields.cpp @@ -30,4 +30,5 @@ PYBIND11_MODULE(shields, m) { define_post_shield::index_type>(m, "Exact"); define_optimal_shield::index_type>(m, "Double"); define_optimal_shield::index_type>(m, "Exact"); + define_shield_handling::index_type>(m); } diff --git a/src/shields/abstract_shield.cpp b/src/shields/abstract_shield.cpp index d73da84..4f70e72 100644 --- a/src/shields/abstract_shield.cpp +++ b/src/shields/abstract_shield.cpp @@ -11,7 +11,7 @@ void define_abstract_shield(py::module& m, std::string vt_suffix) { using AbstractShield = tempest::shields::AbstractShield; std::string shieldClassName = std::string("AbstractShield") + vt_suffix; - py::class_(m, shieldClassName.c_str()) + py::class_>(m, shieldClassName.c_str()) .def("compute_row_group_size", &AbstractShield::computeRowGroupSizes) .def("get_class_name", &AbstractShield::getClassName) .def("get_optimization_direction", &AbstractShield::getOptimizationDirection) diff --git a/src/shields/optimal_shield.cpp b/src/shields/optimal_shield.cpp index 3c0a41a..46f109b 100644 --- a/src/shields/optimal_shield.cpp +++ b/src/shields/optimal_shield.cpp @@ -10,7 +10,7 @@ void define_optimal_shield(py::module& m, std::string vt_suffix) { std::string shieldClassName = std::string("OptimalShield") + vt_suffix; - py::class_(m, shieldClassName.c_str()) + py::class_>(m, shieldClassName.c_str()) ; } diff --git a/src/shields/post_shield.cpp b/src/shields/post_shield.cpp index 862e1d8..a8c518a 100644 --- a/src/shields/post_shield.cpp +++ b/src/shields/post_shield.cpp @@ -10,7 +10,7 @@ void define_post_shield(py::module& m, std::string vt_suffix) { std::string shieldClassName = std::string("PostShield") + vt_suffix; - py::class_(m, shieldClassName.c_str()) + py::class_>(m, shieldClassName.c_str()) ; } diff --git a/src/shields/pre_shield.cpp b/src/shields/pre_shield.cpp index dd42de9..c1558c5 100644 --- a/src/shields/pre_shield.cpp +++ b/src/shields/pre_shield.cpp @@ -18,7 +18,8 @@ void define_pre_shield(py::module& m, std::string vt_suffix) { std::string shieldClassName = std::string("PreShield") + vt_suffix; - py::class_(m, shieldClassName.c_str()) + py::class_>(m, shieldClassName.c_str()) + .def("construct", &PreShield::construct, "Construct the shield") ; } diff --git a/src/shields/shield_handling.cpp b/src/shields/shield_handling.cpp index b7621f5..0d4e4b1 100644 --- a/src/shields/shield_handling.cpp +++ b/src/shields/shield_handling.cpp @@ -1,10 +1,11 @@ #include "shield_handling.h" #include "storm/shields/ShieldHandling.h" +#include "storm/api/export.h" template void define_shield_handling(py::module& m) { - m.def("create_shield", &tempest::shields::createShield, "hi"); + m.def("export_shield", &storm::api::exportShield, py::arg("model"), py::arg("shield")); } template void define_shield_handling::index_type>(py::module& m);