diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index 4bdca9c..7abfffd 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -33,6 +33,7 @@ PYBIND11_MODULE(storage, m) { define_state(m); define_prism(m); define_jani(m); + define_jani_transformers(m); define_labeling(m); define_origins(m); define_expressions(m); diff --git a/src/storage/jani.cpp b/src/storage/jani.cpp index 4197976..3dd5831 100644 --- a/src/storage/jani.cpp +++ b/src/storage/jani.cpp @@ -4,6 +4,8 @@ #include #include #include +#include +#include #include "src/helpers.h" using namespace storm::jani; @@ -172,4 +174,15 @@ void define_jani(py::module& m) { m.def("collect_information", [](const Model& model) {return storm::jani::collectModelInformation(model);}); +} + +void define_jani_transformers(py::module& m) { + py::class_(m, "JaniLocationExpander", "A transformer for Jani expanding variables into locations") + .def(py::init(), py::arg("model")) + .def("transform", &JaniLocationExpander::transform, py::arg("automaton_name"), py::arg("variable_name")) + .def("get_result", &JaniLocationExpander::getResult); + + py::class_(m, "JaniScopeChanger", "A transformer for Jani changing variables from local to global and vice versa") + .def(py::init<>()) + .def("make_variables_local", [](JaniScopeChanger const& sc, Model const& model , std::vector const& props = {}) { Model newModel(model); sc.makeVariablesLocal(newModel, props); return newModel;}, py::arg("model"), py::arg("properties") = std::vector()); } \ No newline at end of file diff --git a/src/storage/jani.h b/src/storage/jani.h index 27d5cef..45cfc50 100644 --- a/src/storage/jani.h +++ b/src/storage/jani.h @@ -3,3 +3,4 @@ #include "common.h" void define_jani(py::module& m); +void define_jani_transformers(py::module& m); \ No newline at end of file