diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 8d08d5e..93a83ad 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -40,6 +40,10 @@ def build_model(symbolic_description, properties=None): return intermediate._as_dtmc() elif intermediate.model_type == ModelType.MDP: return intermediate._as_mdp() + elif intermediate.model_type == ModelType.CTMC: + return intermediate._as_ctmc() + elif intermediate.model_type == ModelType.MA: + return intermediate._as_ma() else: raise StormError("Not supported non-parametric model constructed") @@ -66,6 +70,10 @@ def build_parametric_model(symbolic_description, properties=None): return intermediate._as_pdtmc() elif intermediate.model_type == ModelType.MDP: return intermediate._as_pmdp() + elif intermediate.model_type == ModelType.CTMC: + return intermediate._as_pctmc() + elif intermediate.model_type == ModelType.MA: + return intermediate._as_pma() else: raise StormError("Not supported parametric model constructed") diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 48f0da4..167e003 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -145,8 +145,10 @@ void define_model(py::module& m) { .def("__str__", getModelInfoPrinter("MDP")) ; py::class_, std::shared_ptr>>(m, "SparseCtmc", "CTMC in sparse representation", model) + .def("__str__", getModelInfoPrinter("CTMC")) ; py::class_, std::shared_ptr>>(m, "SparseMA", "MA in sparse representation", model) + .def("__str__", getModelInfoPrinter("MA")) ; py::class_>(m, "SparseRewardModel", "Reward structure for sparse models") .def_property_readonly("has_state_rewards", &RewardModel::hasStateRewards) @@ -186,9 +188,11 @@ void define_model(py::module& m) { ; py::class_, std::shared_ptr>>(m, "SparseParametricCtmc", "pCTMC in sparse representation", modelRatFunc) + .def("__str__", getModelInfoPrinter("ParametricCTMC")) ; py::class_, std::shared_ptr>>(m, "SparseParametricMA", "pMA in sparse representation", modelRatFunc) + .def("__str__", getModelInfoPrinter("ParametricMA")) ; py::class_>(m, "SparseParametricRewardModel", "Reward structure for parametric sparse models") diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index 9f25182..80016e4 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -56,7 +56,6 @@ class TestModel: assert reward == 1.0 or reward == 0.0 assert not model.reward_models["coin_flips"].has_transition_rewards - def test_build_parametric_dtmc_from_prism_program(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) prop = "P=? [F s=5]" @@ -141,6 +140,26 @@ class TestModel: assert not model.supports_parameters assert type(model) is stormpy.SparseMdp + def test_build_ctmc(self): + program = stormpy.parse_prism_program(get_example_path("ctmc", "polling2.sm"), True) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F<=3 \"target\" ]", program) + model = stormpy.build_model(program, formulas) + assert model.nr_states == 12 + assert model.nr_transitions == 22 + assert model.model_type == stormpy.ModelType.CTMC + assert not model.supports_parameters + assert type(model) is stormpy.SparseCtmc + + def test_build_ma(self): + program = stormpy.parse_prism_program(get_example_path("ma", "simple.ma")) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F<=2 s=2 ]", program) + model = stormpy.build_model(program, formulas) + assert model.nr_states == 5 + assert model.nr_transitions == 8 + assert model.model_type == stormpy.ModelType.MA + assert not model.supports_parameters + assert type(model) is stormpy.SparseMA + def test_initial_states(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program)