From bd5aa41188c30abf4f8d3636aa8fa1c1cae2f463 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Mon, 3 Jun 2024 21:10:38 +0200
Subject: [PATCH] added file from first lecture

---
 msg_delivery_blanko.prism | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 msg_delivery_blanko.prism

diff --git a/msg_delivery_blanko.prism b/msg_delivery_blanko.prism
new file mode 100644
index 0000000..d4dfa4a
--- /dev/null
+++ b/msg_delivery_blanko.prism
@@ -0,0 +1,13 @@
+dtmc
+
+module msg_delivery
+
+state : [0..3] init 0;
+// s = 0 -> start, s=1 -> try, s=2 -> lost, s=3 -> delivered
+
+[] state = 0  -> (state'=1);
+[] state = 1 -> 1/10 : (state'=2) + 9/10 : (state'=3);
+[] state = 2 -> (state'=1);
+[] state = 3 -> (state'=0);
+
+endmodule