Browse Source

added jani collector bindings

refactoring
Sebastian Junges 5 years ago
parent
commit
d8c4bca6a7
  1. 3
      CHANGELOG.md
  2. 7
      src/storage/jani.cpp
  3. 14
      tests/storage/test_jani.py

3
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

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

14
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
Loading…
Cancel
Save