From bcab426bd51389a25e55df90e6b39e2458050092 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 13 Dec 2017 19:47:58 +0100
Subject: [PATCH] Added missing cases for CTMC and MA in model building

---
 lib/stormpy/__init__.py     |  8 ++++++++
 src/storage/model.cpp       |  4 ++++
 tests/storage/test_model.py | 21 ++++++++++++++++++++-
 3 files changed, 32 insertions(+), 1 deletion(-)

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<double>("MDP"))
     ;
     py::class_<storm::models::sparse::Ctmc<double>, std::shared_ptr<storm::models::sparse::Ctmc<double>>>(m, "SparseCtmc", "CTMC in sparse representation", model)
+        .def("__str__", getModelInfoPrinter<double>("CTMC"))
     ;
     py::class_<storm::models::sparse::MarkovAutomaton<double>, std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>>>(m, "SparseMA", "MA in sparse representation", model)
+        .def("__str__", getModelInfoPrinter<double>("MA"))
     ;
     py::class_<storm::models::sparse::StandardRewardModel<double>>(m, "SparseRewardModel", "Reward structure for sparse models")
         .def_property_readonly("has_state_rewards", &RewardModel<double>::hasStateRewards)
@@ -186,9 +188,11 @@ void define_model(py::module& m) {
     ;
 
     py::class_<storm::models::sparse::Ctmc<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::Ctmc<storm::RationalFunction>>>(m, "SparseParametricCtmc", "pCTMC in sparse representation", modelRatFunc)
+        .def("__str__", getModelInfoPrinter<RationalFunction>("ParametricCTMC"))
     ;
 
     py::class_<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>>>(m, "SparseParametricMA", "pMA in sparse representation", modelRatFunc)
+        .def("__str__", getModelInfoPrinter<RationalFunction>("ParametricMA"))
     ;
 
     py::class_<storm::models::sparse::StandardRewardModel<storm::RationalFunction>>(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)