From e831ae36c5d1503f82edb86e365c2e8720886589 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 24 Jul 2019 13:56:50 +0200
Subject: [PATCH] Binding for preprocessing prism models

---
 lib/stormpy/examples/files/pdtmc/herman5.pm | 46 +++++++++++++++++++++
 src/core/input.cpp                          | 14 +++++++
 tests/pars/test_parametric_model.py         | 13 ++++++
 3 files changed, 73 insertions(+)
 create mode 100644 lib/stormpy/examples/files/pdtmc/herman5.pm

diff --git a/lib/stormpy/examples/files/pdtmc/herman5.pm b/lib/stormpy/examples/files/pdtmc/herman5.pm
new file mode 100644
index 0000000..052f61a
--- /dev/null
+++ b/lib/stormpy/examples/files/pdtmc/herman5.pm
@@ -0,0 +1,46 @@
+// herman's self stabilising algorithm [Her90]
+// gxn/dxp 13/07/02
+
+// the procotol is synchronous with no nondeterminism (a DTMC)
+dtmc
+
+// coin
+const double p;
+
+// module for process 1
+module process1
+
+	// Boolean variable for process 1
+	x1 : [0..1];
+    i1 : bool init false;
+
+    [initial] (!i1) -> 0.5 : (x1'=0) & (i1'=true) + 0.5 : (x1'=1) & (i1'=true);
+	[step]  (i1 & x1=x0) -> p : (x1'=0) + 1-p : (x1'=1);
+	[step] (i1 & x1!=x0) -> (x1'=x0);
+	
+endmodule
+
+// add further processes through renaming
+module process2 = process1 [ x1=x2, x0=x1, i1=i2 ] endmodule
+module process3 = process1 [ x1=x3, x0=x2, i1=i3 ] endmodule
+module process4 = process1 [ x1=x4, x0=x3, i1=i4 ] endmodule
+module process5 = process1 [ x1=x0, x0=x4, i1=i5 ] endmodule
+
+formula initialized = i1 & i2 & i3 & i4 & i5;
+
+// cost - 1 in each state (expected number of steps)
+rewards "steps"
+	initialized : 1;
+endrewards
+
+// formula, for use in properties: number of tokens
+// (i.e. number of processes that have the same value as the process to their left)
+formula num_tokens = (x1=x0?1:0)
+                    +(x2=x1?1:0)
+                    +(x3=x2?1:0)
+                    +(x4=x3?1:0)
+                    +(x0=x4?1:0);
+
+// label - stable configurations (1 token)
+label "stable" = num_tokens=1 & initialized;
+
diff --git a/src/core/input.cpp b/src/core/input.cpp
index 3debf33..5b014c3 100644
--- a/src/core/input.cpp
+++ b/src/core/input.cpp
@@ -24,6 +24,20 @@ void define_input(py::module& m) {
             return storm::api::parseJaniModel(path);
         }, "Parse Jani model", py::arg("path"));
 
+    m.def("preprocess_prism_program", [](storm::storage::SymbolicModelDescription const& input, std::vector<storm::jani::Property> properties, std::string constantDefinitionString){
+            // Substitute constant definitions in symbolic input.
+            std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
+            storm::storage::SymbolicModelDescription output;
+            std::vector<storm::jani::Property> outputProperties;
+            constantDefinitions = input.parseConstantDefinitions(constantDefinitionString);
+            output = input.preprocess(constantDefinitions);
+            if (!properties.empty()) {
+                outputProperties = storm::api::substituteConstantsInProperties(properties, constantDefinitions);
+            }
+            //ensureNoUndefinedPropertyConstants(outputProperties);
+            return std::pair<storm::storage::SymbolicModelDescription, std::vector<storm::jani::Property>>(output, outputProperties);
+        }, "Preprocess Prism program", py::arg("prism_program"), py::arg("properties"), py::arg("constant_definition_string"));
+
     // JaniType
     py::enum_<storm::jani::ModelType>(m, "JaniModelType", "Type of the Jani model")
         .value("DTMC", storm::jani::ModelType::DTMC)
diff --git a/tests/pars/test_parametric_model.py b/tests/pars/test_parametric_model.py
index 76e18c2..f3631f6 100644
--- a/tests/pars/test_parametric_model.py
+++ b/tests/pars/test_parametric_model.py
@@ -54,6 +54,19 @@ class TestSymbolicParametricModel:
         assert model.has_parameters
         assert type(model) is stormpy.SymbolicSylvanParametricDtmc
 
+    def test_build_parametric_dtmc_preprocess(self):
+        program = stormpy.parse_prism_program(get_example_path("pdtmc", "herman5.pm"))
+        formulas = stormpy.parse_properties_for_prism_program("R=? [ F \"stable\" ]", program)
+        trans_program, trans_formulas = stormpy.preprocess_prism_program(program, formulas, "")
+        trans_prism = trans_program.as_prism_program()
+        model = stormpy.build_symbolic_parametric_model(trans_prism, trans_formulas)
+        assert model.nr_states == 33
+        assert model.nr_transitions == 276
+        assert model.model_type == stormpy.ModelType.DTMC
+        assert model.supports_parameters
+        assert model.has_parameters
+        assert type(model) is stormpy.SymbolicSylvanParametricDtmc
+
     def test_build_dtmc_supporting_parameters(self):
         program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
         formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program)