Browse Source

added examples for first lecture

main
sp 5 days ago
commit
1cdea8875e
  1. 11
      msg_delivery_in_class.dot
  2. BIN
      msg_delivery_in_class.dot.pdf
  3. 14
      msg_delivery_in_class.prism
  4. 30
      robot_1D_in_class.dot
  5. BIN
      robot_1D_in_class.dot.pdf
  6. 29
      robot_1D_in_class.prism

11
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" ];
}

BIN
msg_delivery_in_class.dot.pdf

14
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

30
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" ];
}

BIN
robot_1D_in_class.dot.pdf

29
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
Loading…
Cancel
Save