Browse Source

added basic shield class bindings

refactoring
Thomas Knoll 1 year ago
parent
commit
5617735b69
  1. 2
      src/core/result.cpp
  2. 9
      src/mod_shields.cpp
  3. 1
      src/shields/abstract_shield.cpp
  4. 11
      src/shields/optimal_shield.cpp
  5. 1
      src/shields/optimal_shield.h
  6. 11
      src/shields/post_shield.cpp
  7. 1
      src/shields/post_shield.h
  8. 1
      src/shields/pre_shield.cpp

2
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<double> const& res) {return res.getValueVector();}, "Get model checking result values for all states")
.def_property_readonly("scheduler", [](storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& res) {return res.getScheduler();}, "get scheduler")
.def_property_readonly("shield", [](storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& res) {return res.getShield();}, "get shield")
;
py::class_<storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>, std::shared_ptr<storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>>>(m, "SymbolicQuantitativeCheckResult", "Symbolic quantitative model checking result", quantitativeCheckResult)
.def("clone", [](storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double> const& dd) {return dd.clone()->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); })

9
src/mod_shields.cpp

@ -23,8 +23,11 @@ PYBIND11_MODULE(shields, m) {
define_pet(m);
define_add(m);
define_abstract_shield<double, typename storm::storage::SparseMatrix<double>::index_type>(m);
define_abstract_shield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::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);
define_pre_shield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>(m);
define_post_shield<double, typename storm::storage::SparseMatrix<double>::index_type>(m);
define_post_shield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>(m);
define_optimal_shield<double, typename storm::storage::SparseMatrix<double>::index_type>(m);
define_optimal_shield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>(m);
}

1
src/shields/abstract_shield.cpp

@ -17,3 +17,4 @@ void define_abstract_shield(py::module& m) {
}
template void define_abstract_shield<double, typename storm::storage::SparseMatrix<double>::index_type>(py::module& m);
template void define_abstract_shield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>(py::module& m);

11
src/shields/optimal_shield.cpp

@ -3,9 +3,14 @@
#include "storm/shields/AbstractShield.h"
#include "storm/shields/OptimalShield.h"
template <typename ValueType, typename IndexType>
void define_optimal_shield(py::module& m) {
// py::class_<tempest::shields::OptimalShield, tempest::shields::AbstractShield>(m, "OptimalShield")
// ;
}
using OptimalShield = tempest::shields::OptimalShield<ValueType, IndexType>;
using AbstractShield = tempest::shields::AbstractShield<ValueType, IndexType>;
py::class_<OptimalShield, AbstractShield>(m, "OptimalShield")
;
}
template void define_optimal_shield<double, typename storm::storage::SparseMatrix<double>::index_type>(py::module& m);
template void define_optimal_shield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>(py::module& m);

1
src/shields/optimal_shield.h

@ -2,4 +2,5 @@
#include "common.h"
template <typename ValueType, typename IndexType>
void define_optimal_shield(py::module& m);

11
src/shields/post_shield.cpp

@ -1,6 +1,17 @@
#include "post_shield.h"
#include "storm/shields/AbstractShield.h"
#include "storm/shields/PostShield.h"
template <typename ValueType, typename IndexType>
void define_post_shield(py::module& m) {
using PostShield = tempest::shields::PostShield<ValueType, IndexType>;
using AbstractShield = tempest::shields::AbstractShield<ValueType, IndexType>;
py::class_<PostShield, AbstractShield>(m, "PostShield")
;
}
template void define_post_shield<double, typename storm::storage::SparseMatrix<double>::index_type>(py::module& m);
template void define_post_shield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>(py::module& m);

1
src/shields/post_shield.h

@ -2,4 +2,5 @@
#include "common.h"
template <typename ValueType, typename IndexType>
void define_post_shield(py::module& m);

1
src/shields/pre_shield.cpp

@ -19,3 +19,4 @@ void define_pre_shield(py::module& m) {
}
template void define_pre_shield<double, typename storm::storage::SparseMatrix<double>::index_type>(py::module& m);
template void define_pre_shield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>(py::module& m);
Loading…
Cancel
Save