Binding for undefined_constants_are_graph_preserving

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<storm::prism::Program>)
     ;
 
@@ -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

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)

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"))

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)