added shields module files

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)

lib/stormpy/shields/__init__.py

@@ -0,0 +1,3 @@
+import stormpy.shields
+from . import shields
+from .shields import *

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,

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<storm::RationalFunction>, "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<double>, "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<double>, "Construct a builder instance", py::arg("model_description"), py::arg("options"));
-    m.def("make_sparse_model_builder_exact", &storm::api::makeExplicitModelBuilder<storm::RationalNumber>, "Construct a builder instance", py::arg("model_description"), py::arg("options"));
-    m.def("make_sparse_model_builder_parametric", &storm::api::makeExplicitModelBuilder<double>, "Construct a builder instance", py::arg("model_description"), py::arg("options"));
+    m.def("make_sparse_model_builder", &storm::api::makeExplicitModelBuilder<double>, "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<storm::RationalNumber>, "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<double>, "Construct a builder instance", py::arg("model_description"), py::arg("options"), py::arg("action_mask"));
 
     py::class_<storm::builder::ExplicitModelBuilder<double>>(m, "ExplicitModelBuilder", "Model builder for sparse models")
         .def("build", &storm::builder::ExplicitModelBuilder<double>::build, "Build the model")

src/core/input.cpp

@@ -5,7 +5,7 @@
 
 void define_property(py::module& m) {
     py::class_<storm::jani::Property>(m, "Property", "Property")
-        .def(py::init<std::string const&, std::shared_ptr<storm::logic::Formula const> const&, std::set<storm::expressions::Variable> const&, std::string const&>(), "Construct property from formula", py::arg("name"), py::arg("formula"), py::arg("undefined_constants") = std::set<storm::expressions::Variable>(), py::arg("comment") = "")
+        .def(py::init<std::string const&, std::shared_ptr<storm::logic::Formula const> const&, std::set<storm::expressions::Variable> const&, std::shared_ptr<storm::logic::ShieldExpression const> const&,std::string const&>(), "Construct property from formula", py::arg("name"), py::arg("formula"), py::arg("undefined_constants") = std::set<storm::expressions::Variable>(), py::arg("shield_expression") = nullptr, py::arg("comment") = "")
         .def(py::init<storm::jani::Property>())
         .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")

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<double, typename storm::storage::SparseMatrix<double>::index_type>(m);
+    define_pre_shield<double, typename storm::storage::SparseMatrix<double>::index_type>(m);
+    // define_optimal_shield(m);
+    // define_post_shield(m);
+    define_shield_handling<double, typename storm::storage::SparseMatrix<double>::index_type>(m);
+}

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 <typename ValueType, typename IndexType>
+void define_abstract_shield(py::module& m) {
+    using AbstractShield = tempest::shields::AbstractShield<ValueType, IndexType>;
+    py::class_<AbstractShield>(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<double, typename storm::storage::SparseMatrix<double>::index_type>(py::module& m);

src/shields/abstract_shield.h

@@ -0,0 +1,6 @@
+#pragma once
+
+#include "common.h"
+
+template <typename ValueType, typename IndexType>
+void define_abstract_shield(py::module& m);

src/shields/common.h

@@ -0,0 +1 @@
+#include "src/common.h"

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_<tempest::shields::OptimalShield, tempest::shields::AbstractShield>(m, "OptimalShield")
+    // ;
+}
+
+

src/shields/optimal_shield.h

@@ -0,0 +1,5 @@
+#pragma once
+
+#include "common.h"
+
+void define_optimal_shield(py::module& m);

src/shields/post_shield.cpp

@@ -0,0 +1,6 @@
+#include "post_shield.h"
+
+
+void define_post_shield(py::module& m) {
+
+}

src/shields/post_shield.h

@@ -0,0 +1,5 @@
+#pragma once
+
+#include "common.h"
+
+void define_post_shield(py::module& m);

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 <typename ValueType, typename IndexType>
+void define_pre_shield(py::module& m) {
+    using PreShield = tempest::shields::PreShield<ValueType, IndexType>;
+    using AbstractShield = tempest::shields::AbstractShield<ValueType, IndexType>;
+    py::class_<PreShield, AbstractShield>(m, "PreShield")
+    ;
+}
+
+template void define_pre_shield<double, typename storm::storage::SparseMatrix<double>::index_type>(py::module& m);

src/shields/pre_shield.h

@@ -0,0 +1,6 @@
+#pragma once
+
+#include "common.h"
+
+template <typename ValueType, typename IndexType>
+void define_pre_shield(py::module& m);

src/shields/shield_handling.cpp

@@ -0,0 +1,10 @@
+#include "shield_handling.h"
+
+#include "storm/shields/ShieldHandling.h"
+
+template <typename ValueType, typename IndexType>
+void define_shield_handling(py::module& m) {
+    m.def("create_shield", &tempest::shields::createShield<ValueType, IndexType>, "hi");
+}
+
+template void define_shield_handling<double, typename storm::storage::SparseMatrix<double>::index_type>(py::module& m);

src/shields/shield_handling.h

@@ -0,0 +1,6 @@
+#pragma once
+
+#include "common.h"
+
+template <typename ValueType, typename IndexType>
+void define_shield_handling(py::module& m);