diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index db9282d..7447afa 100644 --- a/lib/stormpy/__init__.py +++ b/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() diff --git a/src/core/input.cpp b/src/core/input.cpp index 29ae2c1..2ce3ca8 100644 --- a/src/core/input.cpp +++ b/src/core/input.cpp @@ -73,6 +73,12 @@ void define_input(py::module& m) { .def("instantiate_constants", [](storm::storage::SymbolicModelDescription const& description, std::map 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 diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index 19e8540..8bec592 100644 --- a/tests/storage/test_model.py +++ b/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