diff --git a/src/core/result.cpp b/src/core/result.cpp index 70babdc..24ed729 100644 --- a/src/core/result.cpp +++ b/src/core/result.cpp @@ -70,6 +70,7 @@ void define_result(py::module& m) { .def("get_truth_values", &storm::modelchecker::ExplicitQualitativeCheckResult::getTruthValuesVector, "Get BitVector representing the truth values") ; py::class_, std::shared_ptr>>(m, "SymbolicQualitativeCheckResult", "Symbolic qualitative model checking result", qualitativeCheckResult) + .def("get_truth_values", &storm::modelchecker::SymbolicQualitativeCheckResult::getTruthValuesVector, "Get Dd representing the truth values") ; // QuantitativeCheckResult diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index 7576b25..552168c 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -1,6 +1,7 @@ #include "common.h" #include "storage/bitvector.h" +#include "storage/dd.h" #include "storage/model.h" #include "storage/matrix.h" #include "storage/distribution.h" @@ -24,6 +25,7 @@ PYBIND11_MODULE(storage, m) { #endif define_bitvector(m); + define_dd(m, "Sylvan"); define_model(m); define_statevaluation(m); define_sparse_model(m); diff --git a/src/storage/dd.cpp b/src/storage/dd.cpp new file mode 100644 index 0000000..09b5a39 --- /dev/null +++ b/src/storage/dd.cpp @@ -0,0 +1,27 @@ +#include "dd.h" +#include "storm/storage/dd/DdManager.h" +#include "storm/storage/dd/Dd.h" +#include "storm/storage/dd/Bdd.h" +#include "src/helpers.h" + +template +void define_dd(py::module& m, std::string const& libstring) { + py::class_> ddMetaVariable(m, (std::string("DdMetaVariable_") + libstring).c_str()); + ddMetaVariable.def("compute_indices", &storm::dd::DdMetaVariable::getIndices, py::arg("sorted")=true); + ddMetaVariable.def_property_readonly("name", &storm::dd::DdMetaVariable::getName); + + py::class_, std::shared_ptr>> ddManager(m, (std::string("DdManager_") + libstring).c_str()); + //ddManager.def("get_meta_variable", &storm::dd::DdManager::getMetaVariable, py::arg("expression_variable")); + + py::class_> dd(m, (std::string("Dd_") + libstring).c_str(), "Dd"); + dd.def_property_readonly("node_count", &storm::dd::Dd::getNodeCount, "get node count"); + dd.def_property_readonly("dd_manager", &storm::dd::Dd::getDdManager, "get the manager"); + dd.def_property_readonly("meta_variables", [](storm::dd::Dd const& dd) {return dd.getContainedMetaVariables();}, "the contained meta variables"); + + + py::class_> bdd(m, (std::string("Bdd_") + libstring).c_str(), "Bdd", dd); + bdd.def("to_expression", &storm::dd::Bdd::toExpression, py::arg("expression_manager")); +} + + +template void define_dd(py::module& m, std::string const& libstring); \ No newline at end of file diff --git a/src/storage/dd.h b/src/storage/dd.h new file mode 100644 index 0000000..9d9df2a --- /dev/null +++ b/src/storage/dd.h @@ -0,0 +1,7 @@ +#pragma once + +#include "common.h" +#include "storm/storage/dd/DdType.h" + +template +void define_dd(py::module& m, std::string const& libname);