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 #include #include +#include #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(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