add prism files from first lecture

car_pedestrian_dtmc_blanko.prism

@@ -0,0 +1,42 @@
+dtmc
+
+const int lanes = 4; // Counting the sidewalk as a lane
+const int street_length = 20;
+
+const double prob_cross_street = 0.1;
+
+global move : [0..1] init 0;
+
+formula ped_at_edge = ped_street_pos = 1 | ped_street_pos = street_length;
+
+formula car_at_end = car_street_pos = street_length;
+
+formula crash = car_street_pos = ped_street_pos & ped_lane_pos = car_lane_pos;
+label "crashed" = crash;
+
+module car
+
+car_street_pos : [0..street_length];
+car_lane_pos : [2..lanes-1];
+
+[] move=0                       -> 1/3 : (car_lane_pos'=min(car_lane_pos+1, lanes-1)) & (car_street_pos'=mod(car_street_pos+1,street_length)) & (move'=1) +
+                                   1/3 : (car_lane_pos'=max(2, car_lane_pos-1))       & (car_street_pos'=mod(car_street_pos+1,street_length)) & (move'=1) +
+                                   1/3 :                                                (car_street_pos'=mod(car_street_pos+1,street_length)) & (move'=1);
+
+
+endmodule
+
+module pedestrian
+
+ped_street_pos : [0..street_length] init floor(street_length/2);
+ped_lane_pos : [1..lanes] init 1;
+
+[] move=1 & ped_lane_pos=1 -> (1/3 * (1 - prob_cross_street)) : (move'=0) +
+                              (1/3 * (1 - prob_cross_street)) : (move'=0) & (ped_street_pos'=min(ped_street_pos+1,street_length)) +
+                              (1/3 * (1 - prob_cross_street)) : (move'=0) & (ped_street_pos'=max(ped_street_pos-1,1)            ) +
+                              prob_cross_street :             (move'=0) & (ped_lane_pos'=2);
+
+[] move=1 & ped_lane_pos>1 & ped_lane_pos<lanes -> (move'=0) & (ped_lane_pos'=ped_lane_pos+1);
+
+
+endmodule

msg_delivery.prism

@@ -0,0 +1,20 @@
+dtmc
+
+label "success" = delivered=1;
+label "lost" = lost=1;
+
+const int MAX_COUNT;
+
+module msg_delivery
+    start: [0..1] init 1;
+    try: [0..1] init 0;
+    lost: [0..1] init 0;
+    delivered: [0..1] init 0;
+
+
+    [] start=1      -> 1: (start'=0) & (try'=1);
+    [] try=1        -> 0.1: (try'=0) & (lost'=1) +
+                       0.9: (try'=0) & (delivered'=1);
+    [] lost=1      -> 1: (lost'=0) & (try'=1);
+    [] delivered=1 -> 1: (delivered'=0) & (start'=1);
+endmodule

msg_delivery_with_counting.prism

@@ -0,0 +1,26 @@
+dtmc
+
+label "success" = delivered=1;
+label "lost" = lost=1;
+
+const int MAX_COUNT = 20;
+
+module msg_delivery
+    start: [0..1] init 1;
+    try: [0..1] init 0;
+    lost: [0..1] init 0;
+    delivered: [0..1] init 0;
+    delivered_count: [0..MAX_COUNT] init 0;
+    lost_count: [0..MAX_COUNT] init 0;
+
+
+    [] start=1      -> 1: (start'=0) & (try'=1);
+    [] try=1        -> 0.1: (try'=0) & (lost'=1) +
+                       0.9: (try'=0) & (delivered'=1);
+    [] lost=1       & lost_count<MAX_COUNT       -> 1: (lost'=0) & (try'=1) & (lost_count'=lost_count+1);
+    [] delivered=1  & delivered_count<MAX_COUNT  -> 1: (delivered'=0) & (start'=1) & (delivered_count'=delivered_count+1) & (lost_count'=0);
+
+    [] lost=1       & lost_count=MAX_COUNT       -> 1: (lost'=0) & (try'=1) & (lost_count'=lost_count);
+    [] delivered=1  & delivered_count=MAX_COUNT  -> 1: (delivered'=0) & (start'=1) & (delivered_count'=delivered_count) & (lost_count'=0);
+
+endmodule