Browse Source
Support for parsing jani model from string
refactoring
Matthias Volk
4 years ago
No known key found for this signature in database
GPG Key ID: 83A57678F739FCD3
2 changed files with
14 additions and
0 deletions
-
src/core/input.cpp
-
tests/core/test_parse.py
|
@ -23,6 +23,9 @@ void define_input(py::module& m) { |
|
|
m.def("parse_jani_model", [](std::string const& path){ |
|
|
m.def("parse_jani_model", [](std::string const& path){ |
|
|
return storm::api::parseJaniModel(path); |
|
|
return storm::api::parseJaniModel(path); |
|
|
}, "Parse Jani model", py::arg("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<storm::jani::Property> properties, std::string constantDefinitionString){ |
|
|
m.def("preprocess_symbolic_input", [](storm::storage::SymbolicModelDescription const& input, std::vector<storm::jani::Property> properties, std::string constantDefinitionString){ |
|
|
// Substitute constant definitions in symbolic input.
|
|
|
// Substitute constant definitions in symbolic input.
|
|
|
|
@ -29,6 +29,17 @@ class TestParse: |
|
|
assert not description.is_prism_program |
|
|
assert not description.is_prism_program |
|
|
assert description.is_jani_model |
|
|
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): |
|
|
def test_parse_formula(self): |
|
|
formula = "P=? [F \"one\"]" |
|
|
formula = "P=? [F \"one\"]" |
|
|
properties = stormpy.parse_properties(formula) |
|
|
properties = stormpy.parse_properties(formula) |
|
|