Bindings for importing DRN files

lib/stormpy/__init__.py

@@ -10,10 +10,12 @@ core._set_up("")
 
 def build_model(program, properties = None):
     """
-    Build a model from a symbolic description
+    Build a model from a symbolic description.
 
     :param PrismProgram program: Prism program 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 properties:
         formulae = [prop.raw_formula for prop in properties]
@@ -30,9 +32,12 @@ def build_model(program, properties = None):
 
 def build_parametric_model(program, 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 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 properties:
         formulae = [prop.raw_formula for prop in properties]
@@ -47,6 +52,48 @@ def build_parametric_model(program, properties = None):
     else:
         raise RuntimeError("Not supported parametric model constructed")
 
+def build_model_from_drn(file):
+    """
+    Build a model from the explicit DRN representation.
+
+    :param String file: DRN file containing the model.
+    :return: Model in sparse representation.
+    :rtype: SparseDtmc or SparseMdp or SparseCTMC or SparseMA
+    """
+    intermediate = core._build_sparse_model_from_drn(file)
+    assert not intermediate.supports_parameters
+    if intermediate.model_type == ModelType.DTMC:
+        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 RuntimeError("Not supported non-parametric model constructed")
+
+def build_parametric_model_from_drn(file):
+    """
+    Build a parametric model from the explicit DRN representation.
+
+    :param String file: DRN file containing the model.
+    :return: Parametric model in sparse representation.
+    :rtype: SparseParametricDtmc or SparseParametricMdp or SparseParametricCTMC or SparseParametricMA
+    """
+    intermediate = core._build_sparse_parametric_model_from_drn(file)
+    assert intermediate.supports_parameters
+    if intermediate.model_type == ModelType.DTMC:
+        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 RuntimeError("Not supported parametric model constructed")
+
 def perform_bisimulation(model, property, bisimulation_type):
     if model.supports_parameters:
         return core._perform_parametric_bisimulation(model, property.raw_formula, bisimulation_type)

lib/stormpy/examples/files/ctmc/dft.drn

@@ -0,0 +1,73 @@
+// Exported by storm
+// Original model type: CTMC
+@type: CTMC
+@parameters
+
+@nr_states
+16
+@model
+state 0 init
+	action 0
+		1 : 0.5
+		2 : 0.5
+		3 : 0.5
+		4 : 0.5
+state 1
+	action 0
+		5 : 0.5
+		9 : 0.5
+		11 : 0.5
+state 2
+	action 0
+		5 : 0.5
+		14 : 0.5
+		15 : 0.5
+state 3
+	action 0
+		9 : 0.5
+		12 : 0.5
+		15 : 0.5
+state 4
+	action 0
+		11 : 0.5
+		12 : 0.5
+		14 : 0.5
+state 5
+	action 0
+		6 : 0.5
+		8 : 0.5
+state 6
+	action 0
+		7 : 0.5
+state 7 failed
+	action 0
+		7 : 1
+state 8
+	action 0
+		7 : 0.5
+state 9
+	action 0
+		8 : 0.5
+		10 : 0.5
+state 10
+	action 0
+		7 : 0.5
+state 11
+	action 0
+		6 : 0.5
+		10 : 0.5
+state 12
+	action 0
+		10 : 0.5
+		13 : 0.5
+state 13
+	action 0
+		7 : 0.5
+state 14
+	action 0
+		6 : 0.5
+		13 : 0.5
+state 15
+	action 0
+		8 : 0.5
+		13 : 0.5

src/core/core.cpp

@@ -58,5 +58,7 @@ void define_build(py::module& m) {
     // Build model
     m.def("_build_sparse_model_from_prism_program", &storm::buildSparseModel<double>, "Build the model", py::arg("program"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
     m.def("_build_sparse_parametric_model_from_prism_program", &storm::buildSparseModel<storm::RationalFunction>, "Build the parametric model", py::arg("program"), py::arg("formulas"));
+    m.def("_build_sparse_model_from_drn", &storm::buildExplicitDRNModel<double>, "Build the model from DRN", py::arg("file"));
+    m.def("_build_sparse_parametric_model_from_drn", &storm::buildExplicitDRNModel<storm::RationalFunction>, "Build the parametric model from DRN", py::arg("file"));
     
 }

src/storage/model.cpp

@@ -53,6 +53,10 @@ void define_model(py::module& m) {
         .def("_as_pdtmc", &storm::models::ModelBase::as<storm::models::sparse::Dtmc<storm::RationalFunction>>, "Get model as pDTMC")
         .def("_as_mdp", &storm::models::ModelBase::as<storm::models::sparse::Mdp<double>>, "Get model as MDP")
         .def("_as_pmdp", &storm::models::ModelBase::as<storm::models::sparse::Mdp<storm::RationalFunction>>, "Get model as pMDP")
+        .def("_as_ctmc", &storm::models::ModelBase::as<storm::models::sparse::Ctmc<double>>, "Get model as CTMC")
+        .def("_as_pctmc", &storm::models::ModelBase::as<storm::models::sparse::Ctmc<storm::RationalFunction>>, "Get model as pCTMC")
+        .def("_as_ma", &storm::models::ModelBase::as<storm::models::sparse::MarkovAutomaton<double>>, "Get model as MA")
+        .def("_as_pma", &storm::models::ModelBase::as<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>>, "Get model as pMA")
     ;
 
     // Models
@@ -70,6 +74,10 @@ void define_model(py::module& m) {
     ;
     py::class_<storm::models::sparse::Mdp<double>, std::shared_ptr<storm::models::sparse::Mdp<double>>>(m, "SparseMdp", "MDP in sparse representation", model)
     ;
+    py::class_<storm::models::sparse::Ctmc<double>, std::shared_ptr<storm::models::sparse::Ctmc<double>>>(m, "SparseCtmc", "CTMC in sparse representation", model)
+    ;
+    py::class_<storm::models::sparse::MarkovAutomaton<double>, std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>>>(m, "SparseMA", "MA in sparse representation", model)
+    ;
 
     py::class_<storm::models::sparse::Model<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>>> modelRatFunc(m, "_SparseParametricModel", "A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix", modelBase);
     modelRatFunc.def("collect_probability_parameters", &probabilityVariables, "Collect parameters")
@@ -85,6 +93,10 @@ void define_model(py::module& m) {
     ;
     py::class_<storm::models::sparse::Mdp<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>>>(m, "SparseParametricMdp", "pMDP in sparse representation", modelRatFunc)
     ;
+    py::class_<storm::models::sparse::Ctmc<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::Ctmc<storm::RationalFunction>>>(m, "SparseParametricCtmc", "pCTMC in sparse representation", modelRatFunc)
+    ;
+    py::class_<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>>>(m, "SparseParametricMA", "pMA in sparse representation", modelRatFunc)
+    ;
 
 }
 

tests/core/test_modelchecking.py

@@ -73,3 +73,14 @@ class TestModelChecking:
         labelprop = stormpy.core.Property("cora", formulaPsi.raw_formula)
         result =  stormpy.model_checking(model, labelprop)
         assert result.get_truth_values().number_of_set_bits() == 1
+    
+    def test_model_checking_ctmc(self):
+        model = stormpy.build_model_from_drn(get_example_path("ctmc", "dft.drn"))
+        formulas = stormpy.parse_properties("T=? [ F \"failed\" ]")
+        assert model.nr_states == 16
+        assert model.nr_transitions == 33
+        assert len(model.initial_states) == 1
+        initial_state = model.initial_states[0]
+        assert initial_state == 0
+        result = stormpy.model_checking(model, formulas[0])
+        assert math.isclose(result.at(initial_state), 4.166666667)

tests/core/test_parse.py

@@ -30,3 +30,12 @@ class TestParse:
         assert model.model_type == stormpy.ModelType.MDP
         assert not model.supports_parameters
         assert type(model) is stormpy.SparseMdp
+    
+    def test_parse_drn_dtmc(self):
+        model = stormpy.build_model_from_drn(get_example_path("ctmc", "dft.drn"))
+        assert model.nr_states == 16
+        assert model.nr_transitions == 33
+        assert model.model_type == stormpy.ModelType.CTMC
+        assert not model.supports_parameters
+        assert type(model) is stormpy.SparseCtmc
+