diff --git a/CMakeLists.txt b/CMakeLists.txt index b4743d4..4891acf 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -34,6 +34,9 @@ stormpy_module(info) stormpy_module(logic) stormpy_module(storage) stormpy_module(utility) +stormpy_module(shields) + + # Optional modules if(HAVE_STORM_DFT) diff --git a/lib/stormpy/shields/__init__.py b/lib/stormpy/shields/__init__.py new file mode 100644 index 0000000..1220140 --- /dev/null +++ b/lib/stormpy/shields/__init__.py @@ -0,0 +1,3 @@ +import stormpy.shields +from . import shields +from .shields import * \ No newline at end of file diff --git a/setup.py b/setup.py index 694c872..5262efc 100755 --- a/setup.py +++ b/setup.py @@ -269,7 +269,9 @@ setup( CMakeExtension('dft', subdir='dft'), CMakeExtension('gspn', subdir='gspn'), CMakeExtension('pars', subdir='pars'), - CMakeExtension('pomdp', subdir='pomdp')], + CMakeExtension('pomdp', subdir='pomdp'), + CMakeExtension('shields', subdir='shields') + ], cmdclass={'build_ext': CMakeBuild}, zip_safe=False, diff --git a/src/core/core.cpp b/src/core/core.cpp index 218c3e6..8b2e9cd 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")); - m.def("make_sparse_model_builder_exact", &storm::api::makeExplicitModelBuilder, "Construct a builder instance", py::arg("model_description"), py::arg("options")); - m.def("make_sparse_model_builder_parametric", &storm::api::makeExplicitModelBuilder, "Construct a builder instance", py::arg("model_description"), py::arg("options")); + 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")); py::class_>(m, "ExplicitModelBuilder", "Model builder for sparse models") .def("build", &storm::builder::ExplicitModelBuilder::build, "Build the model") diff --git a/src/core/input.cpp b/src/core/input.cpp index de5635a..72a5e40 100644 --- a/src/core/input.cpp +++ b/src/core/input.cpp @@ -5,7 +5,7 @@ void define_property(py::module& m) { py::class_(m, "Property", "Property") - .def(py::init const&, std::set const&, std::string const&>(), "Construct property from formula", py::arg("name"), py::arg("formula"), py::arg("undefined_constants") = std::set(), py::arg("comment") = "") + .def(py::init const&, std::set const&, std::shared_ptr const&,std::string const&>(), "Construct property from formula", py::arg("name"), py::arg("formula"), py::arg("undefined_constants") = std::set(), py::arg("shield_expression") = nullptr, py::arg("comment") = "") .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") diff --git a/src/mod_shields.cpp b/src/mod_shields.cpp new file mode 100644 index 0000000..dde4074 --- /dev/null +++ b/src/mod_shields.cpp @@ -0,0 +1,30 @@ +#include "common.h" +#include "shields/abstract_shield.h" +#include "shields/optimal_shield.h" +#include "shields/post_shield.h" +#include "shields/pre_shield.h" +#include "shields/shield_handling.h" +#include "shields/debug.h" + + +#include "storm/storage/Scheduler.h" +#include "storm/storage/SchedulerChoice.h" +#include "storm/storage/BitVector.h" +#include "storm/storage/Distribution.h" + +PYBIND11_MODULE(shields, m) { + m.doc() = "shields"; + +#ifdef STORMPY_DISABLE_SIGNATURE_DOC + py::options options; + options.disable_function_signatures(); +#endif + + define_pet(m); + define_add(m); + define_abstract_shield::index_type>(m); + define_pre_shield::index_type>(m); + // define_optimal_shield(m); + // define_post_shield(m); + define_shield_handling::index_type>(m); +} diff --git a/src/shields/abstract_shield.cpp b/src/shields/abstract_shield.cpp new file mode 100644 index 0000000..92d9874 --- /dev/null +++ b/src/shields/abstract_shield.cpp @@ -0,0 +1,19 @@ +#include "abstract_shield.h" +#include "storm/shields/AbstractShield.h" + +#include "storm/storage/Scheduler.h" +#include "storm/storage/SchedulerChoice.h" +#include "storm/storage/BitVector.h" +#include "storm/storage/Distribution.h" + +template +void define_abstract_shield(py::module& m) { + using AbstractShield = tempest::shields::AbstractShield; + py::class_(m, "AbstractShield") + .def("compute_row_group_size", &AbstractShield::computeRowGroupSizes) + .def("get_class_name", &AbstractShield::getClassName) + .def("get_optimization_direction", &AbstractShield::getOptimizationDirection) + ; +} + +template void define_abstract_shield::index_type>(py::module& m); diff --git a/src/shields/abstract_shield.h b/src/shields/abstract_shield.h new file mode 100644 index 0000000..c355886 --- /dev/null +++ b/src/shields/abstract_shield.h @@ -0,0 +1,6 @@ +#pragma once + +#include "common.h" + +template +void define_abstract_shield(py::module& m); \ No newline at end of file diff --git a/src/shields/common.h b/src/shields/common.h new file mode 100644 index 0000000..5b6e1d7 --- /dev/null +++ b/src/shields/common.h @@ -0,0 +1 @@ +#include "src/common.h" \ No newline at end of file diff --git a/src/shields/optimal_shield.cpp b/src/shields/optimal_shield.cpp new file mode 100644 index 0000000..0df4a30 --- /dev/null +++ b/src/shields/optimal_shield.cpp @@ -0,0 +1,11 @@ +#include "optimal_shield.h" + +#include "storm/shields/AbstractShield.h" +#include "storm/shields/OptimalShield.h" + +void define_optimal_shield(py::module& m) { + // py::class_(m, "OptimalShield") + // ; +} + + diff --git a/src/shields/optimal_shield.h b/src/shields/optimal_shield.h new file mode 100644 index 0000000..d91ebb8 --- /dev/null +++ b/src/shields/optimal_shield.h @@ -0,0 +1,5 @@ +#pragma once + +#include "common.h" + +void define_optimal_shield(py::module& m); diff --git a/src/shields/post_shield.cpp b/src/shields/post_shield.cpp new file mode 100644 index 0000000..d9c65d8 --- /dev/null +++ b/src/shields/post_shield.cpp @@ -0,0 +1,6 @@ +#include "post_shield.h" + + +void define_post_shield(py::module& m) { + +} \ No newline at end of file diff --git a/src/shields/post_shield.h b/src/shields/post_shield.h new file mode 100644 index 0000000..01d05d1 --- /dev/null +++ b/src/shields/post_shield.h @@ -0,0 +1,5 @@ +#pragma once + +#include "common.h" + +void define_post_shield(py::module& m); \ No newline at end of file diff --git a/src/shields/pre_shield.cpp b/src/shields/pre_shield.cpp new file mode 100644 index 0000000..9cf218e --- /dev/null +++ b/src/shields/pre_shield.cpp @@ -0,0 +1,21 @@ +#include "pre_shield.h" + +#include "storm/shields/PreShield.h" +#include "storm/shields/AbstractShield.h" + + +#include "storm/storage/Scheduler.h" +#include "storm/storage/SchedulerChoice.h" +#include "storm/storage/BitVector.h" +#include "storm/storage/Distribution.h" + + +template +void define_pre_shield(py::module& m) { + using PreShield = tempest::shields::PreShield; + using AbstractShield = tempest::shields::AbstractShield; + py::class_(m, "PreShield") + ; +} + +template void define_pre_shield::index_type>(py::module& m); diff --git a/src/shields/pre_shield.h b/src/shields/pre_shield.h new file mode 100644 index 0000000..000d85d --- /dev/null +++ b/src/shields/pre_shield.h @@ -0,0 +1,6 @@ +#pragma once + +#include "common.h" + +template +void define_pre_shield(py::module& m); \ No newline at end of file diff --git a/src/shields/shield_handling.cpp b/src/shields/shield_handling.cpp new file mode 100644 index 0000000..b7621f5 --- /dev/null +++ b/src/shields/shield_handling.cpp @@ -0,0 +1,10 @@ +#include "shield_handling.h" + +#include "storm/shields/ShieldHandling.h" + +template +void define_shield_handling(py::module& m) { + m.def("create_shield", &tempest::shields::createShield, "hi"); +} + +template void define_shield_handling::index_type>(py::module& m); diff --git a/src/shields/shield_handling.h b/src/shields/shield_handling.h new file mode 100644 index 0000000..07aa44c --- /dev/null +++ b/src/shields/shield_handling.h @@ -0,0 +1,6 @@ +#pragma once + +#include "common.h" + +template +void define_shield_handling(py::module& m); \ No newline at end of file