From 831353bca0af731f7c2d6ff26882001aef8b89e8 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Thu, 23 Apr 2020 15:38:07 -0700
Subject: [PATCH] jani model transformers

---
 src/mod_storage.cpp  |  1 +
 src/storage/jani.cpp | 13 +++++++++++++
 src/storage/jani.h   |  1 +
 3 files changed, 15 insertions(+)

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 <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;
@@ -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_<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>());
 }
\ 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