commit 1cdea8875e3485a33214e17bdb781cd73b978413
Author: sp <stefan.pranger@iaik.tugraz.at>
Date:   Tue May 27 14:15:09 2025 +0200

    added examples for first lecture

diff --git a/msg_delivery_in_class.dot b/msg_delivery_in_class.dot
new file mode 100644
index 0000000..307e256
--- /dev/null
+++ b/msg_delivery_in_class.dot
@@ -0,0 +1,11 @@
+digraph model {
+	0 [ label = "0[s=0]: {init}" ];
+	1 [ label = "1[s=1]: {}" ];
+	2 [ label = "2[s=3]: {delivered}" ];
+	3 [ label = "3[s=2]: {}" ];
+	0 -> 1 [ label= "1" ];
+	1 -> 2 [ label= "0.9" ];
+	1 -> 3 [ label= "0.1" ];
+	2 -> 2 [ label= "1" ];
+	3 -> 1 [ label= "1" ];
+}
diff --git a/msg_delivery_in_class.dot.pdf b/msg_delivery_in_class.dot.pdf
new file mode 100644
index 0000000..6bbd2d4
Binary files /dev/null and b/msg_delivery_in_class.dot.pdf differ
diff --git a/msg_delivery_in_class.prism b/msg_delivery_in_class.prism
new file mode 100644
index 0000000..dcb21a9
--- /dev/null
+++ b/msg_delivery_in_class.prism
@@ -0,0 +1,14 @@
+dtmc
+
+const double deliverySuccess = 0.9;
+
+label "delivered" = s=3;
+
+module msg_delivery
+ s : [0..3] init 0;
+
+ [] s=0 -> (s'=1);
+ [] s=1 -> deliverySuccess : (s'=3) + 1-deliverySuccess: (s'=2);
+ [] s=2 -> (s'=1);
+ [] s=3 -> (s'=0);
+endmodule
diff --git a/robot_1D_in_class.dot b/robot_1D_in_class.dot
new file mode 100644
index 0000000..7c3f986
--- /dev/null
+++ b/robot_1D_in_class.dot
@@ -0,0 +1,30 @@
+digraph model {
+	0 [ label = "0[position=0]: {init, lava}" ];
+	1 [ label = "1[position=1]: {cliff, init}" ];
+	2 [ label = "2[position=2]: {cliff, init}" ];
+	3 [ label = "3[position=3]: {init}" ];
+	4 [ label = "4[position=4]: {init}" ];
+	5 [ label = "5[position=5]: {init}" ];
+	6 [ label = "6[position=6]: {init}" ];
+	7 [ label = "7[position=7]: {cliff, init}" ];
+	8 [ label = "8[position=8]: {init}" ];
+	9 [ label = "9[position=9]: {init}" ];
+	10 [ label = "10[position=10]: {goal, init}" ];
+	0 -> 0 [ label= "1" ];
+	1 -> 0 [ label= "1" ];
+	2 -> 1 [ label= "1" ];
+	3 -> 2 [ label= "0.5" ];
+	3 -> 4 [ label= "0.5" ];
+	4 -> 3 [ label= "0.5" ];
+	4 -> 5 [ label= "0.5" ];
+	5 -> 4 [ label= "0.5" ];
+	5 -> 6 [ label= "0.5" ];
+	6 -> 5 [ label= "0.5" ];
+	6 -> 7 [ label= "0.5" ];
+	7 -> 8 [ label= "1" ];
+	8 -> 7 [ label= "0.5" ];
+	8 -> 9 [ label= "0.5" ];
+	9 -> 8 [ label= "0.5" ];
+	9 -> 10 [ label= "0.5" ];
+	10 -> 10 [ label= "1" ];
+}
diff --git a/robot_1D_in_class.dot.pdf b/robot_1D_in_class.dot.pdf
new file mode 100644
index 0000000..b65fded
Binary files /dev/null and b/robot_1D_in_class.dot.pdf differ
diff --git a/robot_1D_in_class.prism b/robot_1D_in_class.prism
new file mode 100644
index 0000000..6db6d0a
--- /dev/null
+++ b/robot_1D_in_class.prism
@@ -0,0 +1,29 @@
+dtmc
+
+formula isOnSlippery = !isOnGoal & !isOnLava & !isOnLeftCliff & !isOnRightCliff;
+formula isOnRightCliff = position=7;
+formula isOnLeftCliff = position=1 | position=2;
+formula isOnLava = position=0;
+formula isOnGoal = position=10;
+
+label "goal" = isOnGoal;
+label "lava" = isOnLava;
+label "cliff" = isOnRightCliff | isOnLeftCliff;
+
+// labels?
+const double slipToRight = 0.5;
+
+init
+true
+endinit
+
+module robot_1D
+ position : [0..10];
+
+// commands?
+[] isOnSlippery -> slipToRight: (position'=position+1) + 1-slipToRight: (position'=position-1);
+[] isOnRightCliff -> (position'=position+1);
+[] isOnLeftCliff -> (position'=position-1);
+[] isOnGoal | isOnLava -> true;
+
+endmodule