Browse Source

added file from first lecture

main
sp 7 months ago
commit
bd5aa41188
  1. 13
      msg_delivery_blanko.prism

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