From dc94843aca90b3fcd9f1de779bd6bc700ae96fb1 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 10 Nov 2020 17:04:08 +0100 Subject: [PATCH] Support for parsing jani model from string --- src/core/input.cpp | 3 +++ tests/core/test_parse.py | 11 +++++++++++ 2 files changed, 14 insertions(+) diff --git a/src/core/input.cpp b/src/core/input.cpp index 30e53e6..de5635a 100644 --- a/src/core/input.cpp +++ b/src/core/input.cpp @@ -23,6 +23,9 @@ void define_input(py::module& m) { m.def("parse_jani_model", [](std::string const& path){ return storm::api::parseJaniModel(path); }, "Parse Jani model", py::arg("path")); + m.def("parse_jani_model_from_string", [](std::string const& jsonstring){ + return storm::api::parseJaniModelFromString(jsonstring); + }, "Parse Jani model from string", py::arg("json_string")); m.def("preprocess_symbolic_input", [](storm::storage::SymbolicModelDescription const& input, std::vector properties, std::string constantDefinitionString){ // Substitute constant definitions in symbolic input. diff --git a/tests/core/test_parse.py b/tests/core/test_parse.py index 22aa3af..546c8de 100644 --- a/tests/core/test_parse.py +++ b/tests/core/test_parse.py @@ -29,6 +29,17 @@ class TestParse: assert not description.is_prism_program assert description.is_jani_model + def test_parse_jani_model_string(self): + with open(get_example_path("dtmc", "die.jani"), 'r') as file: + json_string = file.read() + jani_model, properties = stormpy.parse_jani_model_from_string(json_string) + assert jani_model.name == "die.jani" + assert jani_model.model_type == stormpy.JaniModelType.DTMC + assert not jani_model.has_undefined_constants + description = stormpy.SymbolicModelDescription(jani_model) + assert not description.is_prism_program + assert description.is_jani_model + def test_parse_formula(self): formula = "P=? [F \"one\"]" properties = stormpy.parse_properties(formula)