From 0ef93e57b31e8e0b4ff1eadfb77a508925ec1c14 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 28 Sep 2018 13:25:42 +0200
Subject: [PATCH] Adapted Jani bindings according to changes in Storm

---
 src/core/input.cpp    |  6 ++++--
 src/storage/jani.cpp  | 10 +++++++---
 src/storage/prism.cpp |  5 ++++-
 3 files changed, 15 insertions(+), 6 deletions(-)

diff --git a/src/core/input.cpp b/src/core/input.cpp
index 1df9f9c..3debf33 100644
--- a/src/core/input.cpp
+++ b/src/core/input.cpp
@@ -18,9 +18,11 @@ void define_property(py::module& m) {
 void define_input(py::module& m) {
 
     // Parse Prism program
-    m.def("parse_prism_program", &storm::api::parseProgram, "Parse Prism program", py::arg("path"), py::arg("prism_compat") = false);
+    m.def("parse_prism_program", &storm::api::parseProgram, "Parse Prism program", py::arg("path"), py::arg("prism_compat") = false, py::arg("simplify") = true);
     // Parse Jani model
-    m.def("parse_jani_model", &storm::api::parseJaniModel, "Parse Jani model", py::arg("path"));
+    m.def("parse_jani_model", [](std::string const& path){
+            return storm::api::parseJaniModel(path);
+        }, "Parse Jani model", py::arg("path"));
 
     // JaniType
     py::enum_<storm::jani::ModelType>(m, "JaniModelType", "Type of the Jani model")
diff --git a/src/storage/jani.cpp b/src/storage/jani.cpp
index 877518a..db5a2bc 100644
--- a/src/storage/jani.cpp
+++ b/src/storage/jani.cpp
@@ -32,13 +32,17 @@ void define_jani(py::module& m) {
     ;
 
     py::class_<Automaton, std::shared_ptr<Automaton>> automaton(m, "JaniAutomaton", "A Jani Automation");
-    automaton.def_property_readonly("edges",[](const Automaton& a) {return a.getEdges();}, "get edges")
-            .def_property_readonly("name", &Automaton::getName)
+    automaton.def_property_readonly("edges",[](const Automaton& a) {
+            return a.getEdges();
+        }, "get edges")
+        .def_property_readonly("name", &Automaton::getName)
     ;
 
     py::class_<Edge, std::shared_ptr<Edge>> edge(m, "JaniEdge", "A Jani Edge");
     edge.def_property_readonly("source_location_index", &Edge::getSourceLocationIndex, "index for source location")
-        .def_property_readonly("destinations", &Edge::getDestinations, "edge destinations")
+        .def_property_readonly("destinations", [](Edge const& e) {
+                return e.getDestinations();
+             }, "edge destinations")
         .def_property_readonly("nr_destinations", &Edge::getNumberOfDestinations, "nr edge destinations")
         .def_property_readonly("guard", &Edge::getGuard, "edge guard")
         .def("substitute", &Edge::substitute, py::arg("mapping"))
diff --git a/src/storage/prism.cpp b/src/storage/prism.cpp
index b1b8a7c..57b0b80 100644
--- a/src/storage/prism.cpp
+++ b/src/storage/prism.cpp
@@ -3,6 +3,7 @@
 #include "src/helpers.h"
 #include <storm/storage/expressions/ExpressionManager.h>
 #include <storm/storage/jani/Model.h>
+#include <storm/storage/jani/Property.h>
 
 using namespace storm::prism;
 
@@ -20,7 +21,9 @@ void define_prism(py::module& m) {
             .def("simplify", &Program::simplify, "Simplify")
             .def("used_constants",&Program::usedConstants, "Compute Used Constants")
             .def_property_readonly("expression_manager", &Program::getManager, "Get the expression manager for expressions in this program")
-            .def("to_jani", &Program::toJaniWithLabelRenaming, "Transform to Jani program", py::arg("all_variables_global")=false, py::arg("suffix") = "", py::arg("standard_compliant")=false)
+            .def("to_jani", [](storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties, bool allVariablesGlobal, std::string suffix) {
+                    return program.toJani(properties, allVariablesGlobal, suffix);
+                }, "Transform to Jani program", py::arg("properties"), py::arg("all_variables_global") = true, py::arg("suffix") = "")
             .def("__str__", &streamToString<storm::prism::Program>);
 
     py::class_<Module> module(m, "PrismModule", "A module in a Prism program");