jani model transformers

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);

src/storage/jani.cpp

@@ -4,6 +4,8 @@
 #include <storm/storage/expressions/ExpressionManager.h>
 #include <storm/logic/RewardAccumulationEliminationVisitor.h>
 #include <storm/storage/jani/traverser/InformationCollector.h>
+#include <storm/storage/jani/JaniLocationExpander.h>
+#include <storm/storage/jani/JaniScopeChanger.h>
 #include "src/helpers.h"
 
 using namespace storm::jani;
@@ -173,3 +175,14 @@ 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_<JaniLocationExpander>(m, "JaniLocationExpander", "A transformer for Jani expanding variables into locations")
+            .def(py::init<Model const&>(), py::arg("model"))
+            .def("transform", &JaniLocationExpander::transform, py::arg("automaton_name"), py::arg("variable_name"))
+            .def("get_result", &JaniLocationExpander::getResult);
+
+    py::class_<JaniScopeChanger>(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<Property> const& props = {}) { Model newModel(model); sc.makeVariablesLocal(newModel, props); return newModel;}, py::arg("model"), py::arg("properties") = std::vector<Property>());
+}

src/storage/jani.h

@@ -3,3 +3,4 @@
 #include "common.h"
 
 void define_jani(py::module& m);
+void define_jani_transformers(py::module& m);