Raise StormError if symbolic description has undefined constants

lib/stormpy/__init__.py

@@ -18,20 +18,23 @@ except ImportError:
 core._set_up("")
 
 
-def build_model(program, properties=None):
+def build_model(symbolic_description, properties=None):
     """
     Build a model from a symbolic description.
 
-    :param PrismProgram program: Prism program to translate into a model.
+    :param symbolic_description: Symbolic model description to translate into a model.
     :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved.
     :return: Model in sparse representation.
     :rtype: SparseDtmc or SparseMdp
     """
+    if not symbolic_description.undefined_constants_are_graph_preserving:
+        raise StormError("Program still contains undefined constants")
+
     if properties:
         formulae = [prop.raw_formula for prop in properties]
-        intermediate = core._build_sparse_model_from_prism_program(program, formulae)
+        intermediate = core._build_sparse_model_from_prism_program(symbolic_description, formulae)
     else:
-        intermediate = core._build_sparse_model_from_prism_program(program)
+        intermediate = core._build_sparse_model_from_prism_program(symbolic_description)
     assert not intermediate.supports_parameters
     if intermediate.model_type == ModelType.DTMC:
         return intermediate._as_dtmc()
@@ -41,20 +44,23 @@ def build_model(program, properties=None):
         raise RuntimeError("Not supported non-parametric model constructed")
 
 
-def build_parametric_model(program, properties=None):
+def build_parametric_model(symbolic_description, properties=None):
     """
     Build a parametric model from a symbolic description.
     
-    :param PrismProgram program: Prism program with open constants to translate into a parametric model.
+    :param symbolic_description: Symbolic model description to translate into a model.
     :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved.
     :return: Parametric model in sparse representation.
     :rtype: SparseParametricDtmc or SparseParametricMdp
     """
+    if not symbolic_description.undefined_constants_are_graph_preserving:
+        raise StormError("Program still contains undefined constants")
+
     if properties:
         formulae = [prop.raw_formula for prop in properties]
     else:
         formulae = []
-    intermediate = core._build_sparse_parametric_model_from_prism_program(program, formulae)
+    intermediate = core._build_sparse_parametric_model_from_prism_program(symbolic_description, formulae)
     assert intermediate.supports_parameters
     if intermediate.model_type == ModelType.DTMC:
         return intermediate._as_pdtmc()

src/core/input.cpp

@@ -73,6 +73,12 @@ void define_input(py::module& m) {
         .def("instantiate_constants", [](storm::storage::SymbolicModelDescription const& description, std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) {
                 return description.preprocess(constantDefinitions);
             }, "Instantiate constants in symbolic model description", py::arg("constant_definitions"))
+        .def("as_jani_model", [](storm::storage::SymbolicModelDescription& description) {
+                return description.asJaniModel();
+            }, "Return Jani model")
+        .def("as_prism_program", [](storm::storage::SymbolicModelDescription& description) {
+                return description.asPrismProgram();
+            }, "Return Prism program")
     ;
 
     // PrismProgram and JaniModel can be converted into SymbolicModelDescription

tests/storage/test_model.py

@@ -60,7 +60,7 @@ class TestModel:
         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):
+        with pytest.raises(stormpy.StormError):
             model = stormpy.build_model(jani_model)
 
     def test_build_instantiated_dtmc(self):
@@ -69,7 +69,7 @@ class TestModel:
         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)
+        instantiated_jani_model = description.instantiate_constants(constant_definitions).as_jani_model()
         model = stormpy.build_model(instantiated_jani_model)
         assert model.nr_states == 677
         assert model.nr_transitions == 867