diff --git a/src/core/result.cpp b/src/core/result.cpp index 24ed729..961626d 100644 --- a/src/core/result.cpp +++ b/src/core/result.cpp @@ -40,6 +40,7 @@ void define_result(py::module& m) { .def_property_readonly("_pareto_curve", &storm::modelchecker::CheckResult::isParetoCurveCheckResult, "Flag if result is a pareto curve") .def_property_readonly("result_for_all_states", &storm::modelchecker::CheckResult::isResultForAllStates, "Flag if result is for all states") .def_property_readonly("has_scheduler", &storm::modelchecker::CheckResult::hasScheduler, "Flag if a scheduler is present") + .def_property_readonly("has_schield", &storm::modelchecker::CheckResult::hasShield, "Flag if a schield is present") .def("as_explicit_qualitative", [](storm::modelchecker::CheckResult const& result) { return result.asExplicitQualitativeCheckResult(); @@ -85,6 +86,7 @@ void define_result(py::module& m) { }, py::arg("state"), "Get result for given state") .def("get_values", [](storm::modelchecker::ExplicitQuantitativeCheckResult const& res) {return res.getValueVector();}, "Get model checking result values for all states") .def_property_readonly("scheduler", [](storm::modelchecker::ExplicitQuantitativeCheckResult const& res) {return res.getScheduler();}, "get scheduler") + .def_property_readonly("shield", [](storm::modelchecker::ExplicitQuantitativeCheckResult const& res) {return res.getShield();}, "get shield") ; py::class_, std::shared_ptr>>(m, "SymbolicQuantitativeCheckResult", "Symbolic quantitative model checking result", quantitativeCheckResult) .def("clone", [](storm::modelchecker::SymbolicQuantitativeCheckResult const& dd) {return dd.clone()->asSymbolicQuantitativeCheckResult(); }) diff --git a/src/mod_shields.cpp b/src/mod_shields.cpp index dde4074..ed1a806 100644 --- a/src/mod_shields.cpp +++ b/src/mod_shields.cpp @@ -23,8 +23,11 @@ PYBIND11_MODULE(shields, m) { define_pet(m); define_add(m); define_abstract_shield::index_type>(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); + define_pre_shield::index_type>(m); + define_post_shield::index_type>(m); + define_post_shield::index_type>(m); + define_optimal_shield::index_type>(m); + define_optimal_shield::index_type>(m); } diff --git a/src/shields/abstract_shield.cpp b/src/shields/abstract_shield.cpp index 92d9874..d29475c 100644 --- a/src/shields/abstract_shield.cpp +++ b/src/shields/abstract_shield.cpp @@ -17,3 +17,4 @@ void define_abstract_shield(py::module& m) { } template void define_abstract_shield::index_type>(py::module& m); +template void define_abstract_shield::index_type>(py::module& m); \ No newline at end of file diff --git a/src/shields/optimal_shield.cpp b/src/shields/optimal_shield.cpp index 0df4a30..6b5ef26 100644 --- a/src/shields/optimal_shield.cpp +++ b/src/shields/optimal_shield.cpp @@ -3,9 +3,14 @@ #include "storm/shields/AbstractShield.h" #include "storm/shields/OptimalShield.h" +template void define_optimal_shield(py::module& m) { - // py::class_(m, "OptimalShield") - // ; -} + using OptimalShield = tempest::shields::OptimalShield; + using AbstractShield = tempest::shields::AbstractShield; + py::class_(m, "OptimalShield") + ; +} +template void define_optimal_shield::index_type>(py::module& m); +template void define_optimal_shield::index_type>(py::module& m); \ No newline at end of file diff --git a/src/shields/optimal_shield.h b/src/shields/optimal_shield.h index d91ebb8..fd35e21 100644 --- a/src/shields/optimal_shield.h +++ b/src/shields/optimal_shield.h @@ -2,4 +2,5 @@ #include "common.h" +template void define_optimal_shield(py::module& m); diff --git a/src/shields/post_shield.cpp b/src/shields/post_shield.cpp index d9c65d8..87d449a 100644 --- a/src/shields/post_shield.cpp +++ b/src/shields/post_shield.cpp @@ -1,6 +1,17 @@ #include "post_shield.h" +#include "storm/shields/AbstractShield.h" +#include "storm/shields/PostShield.h" +template void define_post_shield(py::module& m) { + using PostShield = tempest::shields::PostShield; + using AbstractShield = tempest::shields::AbstractShield; + + py::class_(m, "PostShield") + ; +} -} \ No newline at end of file + +template void define_post_shield::index_type>(py::module& m); +template void define_post_shield::index_type>(py::module& m); \ No newline at end of file diff --git a/src/shields/post_shield.h b/src/shields/post_shield.h index 01d05d1..24421d8 100644 --- a/src/shields/post_shield.h +++ b/src/shields/post_shield.h @@ -2,4 +2,5 @@ #include "common.h" +template 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 index 9cf218e..da36556 100644 --- a/src/shields/pre_shield.cpp +++ b/src/shields/pre_shield.cpp @@ -19,3 +19,4 @@ void define_pre_shield(py::module& m) { } template void define_pre_shield::index_type>(py::module& m); +template void define_pre_shield::index_type>(py::module& m); \ No newline at end of file