Added support for building Interval POMDPs from DRN (#219)

Author: volkm

lib/stormpy/__init__.py

@@ -228,6 +228,8 @@ def build_interval_model_from_drn(file, options=DirectEncodingParserOptions()):
     assert intermediate.supports_uncertainty
     if intermediate.model_type == ModelType.MDP:
         return intermediate._as_sparse_imdp()
+    elif intermediate.model_type == ModelType.POMDP:
+        return intermediate._as_sparse_ipomdp()
     else:
         raise StormError("Not supported interval model constructed")
 

lib/stormpy/examples/files/ipomdp/tiny-01.drn

@@ -0,0 +1,27 @@
+@type: POMDP
+@parameters
+
+@reward_models
+
+@nr_states
+4
+@nr_choices
+5
+@model
+state 0 {0} init
+	action 0
+		1 : [0.2, 0.7]
+		2 : [0.3, 0.8]
+	action 1
+		0 : [0.4, 0.9]
+		3 : [0.5, 0.8]
+state 1 {1} target
+	action 0
+		1 : [1, 1]
+state 2 {2}
+	action 0
+		2 : [1, 1]
+state 3 {2}
+	action 0
+		0 : [0.5, 1]
+		3 : [0.1, 0.5]

src/storage/model.cpp

@@ -160,6 +160,9 @@ void define_model(py::module& m) {
         .def("_as_sparse_ppomdp", [](ModelBase &modelbase) {
             return modelbase.as<SparsePomdp<RationalFunction>>();
         }, "Get model as sparse pPOMDP")
+        .def("_as_sparse_ipomdp", [](ModelBase &modelbase) {
+            return modelbase.as<SparsePomdp<storm::Interval>>();
+        }, "Get model as sparse interval POMDP")
         .def("_as_sparse_ctmc", [](ModelBase &modelbase) {
                 return modelbase.as<SparseCtmc<double>>();
             }, "Get model as sparse CTMC")

tests/storage/test_model.py

@@ -272,3 +272,21 @@ def test_build_ma(self):
         formulas = stormpy.parse_properties_for_prism_program("P=? [ F<=2 s=2 ]", program)
         with pytest.raises(Exception):
             model = stormpy.build_symbolic_model(program, formulas)
+
+    def test_build_ipomdp(self):
+        model = stormpy.build_interval_model_from_drn(get_example_path("ipomdp", "tiny-01.drn"))
+        assert model.nr_states == 4
+        assert model.nr_choices == 5
+        assert model.nr_transitions == 8
+        assert model.nr_observations == 3
+
+        for transition in model.transition_matrix.row_iter(0, 0):
+            if transition.column == 1:
+                assert transition.value().lower() == 0.2
+                assert transition.value().upper() == 0.7
+            elif transition.column == 2:
+                assert transition.value().lower() == 0.3
+                assert transition.value().upper() == 0.8
+
+        assert model.model_type == stormpy.ModelType.POMDP
+        assert type(model) is stormpy.SparseIntervalPomdp