commit bd5aa41188c30abf4f8d3636aa8fa1c1cae2f463 Author: sp Date: Mon Jun 3 21:10:38 2024 +0200 added file from first lecture 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