From 1197155d8d976d100222e3eba5f5ca99b05429b2 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 8 Aug 2017 14:34:31 +0200 Subject: [PATCH] Binding for undefined_constants_are_graph_preserving --- src/core/input.cpp | 2 ++ tests/core/test_bisimulation.py | 1 + tests/core/test_parse.py | 1 + tests/storage/test_model.py | 9 +++++++++ 4 files changed, 13 insertions(+) diff --git a/src/core/input.cpp b/src/core/input.cpp index d9f2705..29ae2c1 100644 --- a/src/core/input.cpp +++ b/src/core/input.cpp @@ -34,6 +34,7 @@ void define_input(py::module& m) { .def_property_readonly("nr_modules", &storm::prism::Program::getNumberOfModules, "Number of modules") .def_property_readonly("model_type", &storm::prism::Program::getModelType, "Model type") .def_property_readonly("has_undefined_constants", &storm::prism::Program::hasUndefinedConstants, "Flag if program has undefined constants") + .def_property_readonly("undefined_constants_are_graph_preserving", &storm::prism::Program::undefinedConstantsAreGraphPreserving, "Flag if the undefined constants do not change the graph structure") .def("__str__", &streamToString) ; @@ -59,6 +60,7 @@ void define_input(py::module& m) { .def_property_readonly("name", &storm::jani::Model::getName, "Name of the jani model") .def_property_readonly("model_type", &storm::jani::Model::getModelType, "Model type") .def_property_readonly("has_undefined_constants", &storm::jani::Model::hasUndefinedConstants, "Flag if Jani model has undefined constants") + .def_property_readonly("undefined_constants_are_graph_preserving", &storm::jani::Model::undefinedConstantsAreGraphPreserving, "Flag if the undefined constants do not change the graph structure") ; // SymbolicModelDescription diff --git a/tests/core/test_bisimulation.py b/tests/core/test_bisimulation.py index f160fa9..418defc 100644 --- a/tests/core/test_bisimulation.py +++ b/tests/core/test_bisimulation.py @@ -36,6 +36,7 @@ class TestBisimulation: assert program.nr_modules == 5 assert program.model_type == stormpy.PrismModelType.DTMC assert program.has_undefined_constants + assert program.undefined_constants_are_graph_preserving prop = "P=? [F s=5]" properties = stormpy.parse_properties_for_prism_program(prop, program) model = stormpy.build_parametric_model(program, properties) diff --git a/tests/core/test_parse.py b/tests/core/test_parse.py index 569a60d..22aa3af 100644 --- a/tests/core/test_parse.py +++ b/tests/core/test_parse.py @@ -18,6 +18,7 @@ class TestParse: assert program.nr_modules == 5 assert program.model_type == stormpy.PrismModelType.DTMC assert program.has_undefined_constants + assert program.undefined_constants_are_graph_preserving def test_parse_jani_model(self): jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani")) diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index 55b70e1..19e8540 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -1,6 +1,7 @@ import stormpy import stormpy.logic from helpers.helper import get_example_path +import pytest class TestModel: @@ -55,9 +56,17 @@ class TestModel: assert not model.supports_parameters assert type(model) is stormpy.SparseDtmc + def test_build_dtmc_with_undefined_constants(self): + jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "brp.jani")) + assert jani_model.has_undefined_constants + assert not jani_model.undefined_constants_are_graph_preserving + with pytest.raises(RuntimeError): + model = stormpy.build_model(jani_model) + def test_build_instantiated_dtmc(self): jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "brp.jani")) assert jani_model.has_undefined_constants + assert not jani_model.undefined_constants_are_graph_preserving description = stormpy.SymbolicModelDescription(jani_model) constant_definitions = description.parse_constant_definitions("N=16, MAX=2") instantiated_jani_model = description.instantiate_constants(constant_definitions)