You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
26 lines
955 B
26 lines
955 B
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
|