From d8c4bca6a733351654b2ffb369ddde6116a82fd1 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Thu, 6 Feb 2020 14:32:14 +0100
Subject: [PATCH] added jani collector bindings

---
 CHANGELOG.md               |  3 +++
 src/storage/jani.cpp       |  7 +++++++
 tests/storage/test_jani.py | 14 ++++++++++++++
 3 files changed, 24 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 329ca5b..67e0379 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,9 @@ Version 1.4.x
 
 ### Version 1.4.2 (under development) 
 
+- Extended expression operators with {conjunction, disjunction}
+- Added information collector to extract information from jani models
+
 ### Version 1.4.1 (2019/12)
 Requires storm version >= 1.4.1 and pycarl version >= 2.0.4
 - Adaptions to changes in Storm
diff --git a/src/storage/jani.cpp b/src/storage/jani.cpp
index 9ce9771..90c127c 100644
--- a/src/storage/jani.cpp
+++ b/src/storage/jani.cpp
@@ -3,6 +3,7 @@
 #include <storm/storage/jani/JSONExporter.h>
 #include <storm/storage/expressions/ExpressionManager.h>
 #include <storm/logic/RewardAccumulationEliminationVisitor.h>
+#include <storm/storage/jani/traverser/InformationCollector.h>
 #include "src/helpers.h"
 
 using namespace storm::jani;
@@ -158,5 +159,11 @@ void define_jani(py::module& m) {
         }, "Eliminate reward accumulations", py::arg("model"), py::arg("properties"));
 
 
+    py::class_<InformationObject> informationObject(m, "JaniInformationObject", "An object holding information about a JANI model");
+    informationObject.def_readwrite("model_type", &InformationObject::modelType)
+            .def_readwrite("nr_automata", &InformationObject::nrAutomata)
+            .def_readwrite("nr_edges", &InformationObject::nrEdges)
+            .def_readwrite("nr_variables", &InformationObject::nrVariables);
+    m.def("collect_information", [](const Model& model) {return storm::jani::collect(model);});
 
 }
\ No newline at end of file
diff --git a/tests/storage/test_jani.py b/tests/storage/test_jani.py
index e69de29..0affa7c 100644
--- a/tests/storage/test_jani.py
+++ b/tests/storage/test_jani.py
@@ -0,0 +1,14 @@
+import stormpy
+import stormpy.logic
+from helpers.helper import get_example_path
+import pytest
+
+
+class TestJani:
+
+    def test_information_collection(self):
+        model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "brp.jani"))
+        information = stormpy.collect_information(model)
+        assert information.nr_automata == 5
+        assert information.nr_edges == 31
+        assert information.nr_variables == 18
\ No newline at end of file