diff options
Diffstat (limited to 'Assignment2/src/die.prism')
| -rw-r--r-- | Assignment2/src/die.prism | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/Assignment2/src/die.prism b/Assignment2/src/die.prism index 45442d6..06de40a 100644 --- a/Assignment2/src/die.prism +++ b/Assignment2/src/die.prism @@ -1,16 +1,18 @@ dtmc +const double p = 0.4; + module die s : [0..7] init 0; d : [0..6] init 0; - [] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); - [] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4); - [] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6); - [] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1); - [] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3); - [] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5); - [] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6); + [] s=0 -> p : (s'=1) + (1-p) : (s'=2); + [] s=1 -> p : (s'=3) + (1-p) : (s'=4); + [] s=2 -> (1-p) : (s'=5) + p : (s'=6); + [] s=3 -> p : (s'=1) + (1-p) : (s'=7) & (d'=1); + [] s=4 -> p : (s'=7) & (d'=2) + (1-p) : (s'=7) & (d'=3); + [] s=5 -> p : (s'=7) & (d'=4) + (1-p) : (s'=7) & (d'=5); + [] s=6 -> p : (s'=2) + (1-p) : (s'=7) & (d'=6); [] s=7 -> 1 : (s'=7); endmodule |