-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathtir_arc_brigitte_marion_mdp.prism
46 lines (38 loc) · 2.18 KB
/
tir_arc_brigitte_marion_mdp.prism
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
mdp
const int k;
module Brigitte
scoreB: [0..3];
nbTirsB : [0..100] init 0;
pretB : bool init false;
rateB: bool init false;
[initB] pretB=false & pretM=false & nbTirsB < 100 -> (pretB'=true);
[initB] pretB=false & pretM=false & nbTirsB < 100 -> (pretB'=false);
[tirB] pretB= true & !rateB & !rateM & nbTirsB < 100 -> 1/8 : (scoreB' = 3) & (pretB'=false) & (nbTirsB'=nbTirsB+1) +
1/4 : (scoreB' = 2) & (pretB'=false) & (nbTirsB'=nbTirsB+1) +
1/2: (scoreB'= 1) & (pretB'=false) & (nbTirsB'=nbTirsB+1) +
(1-(1/8+1/4+1/2)) : (scoreB' = 0) & (rateB'=true) & (pretB'=false) & (nbTirsB'=nbTirsB+1) ;
[tirB] pretB= true & (rateB | rateM) & nbTirsB < 100 -> 1/16 : (scoreB' = 3) & (rateB'=false) & (pretB'=false) & (nbTirsB'=nbTirsB+1) +
1/8 : (scoreB' = 2) & (rateB'=false) & (pretB'=false) & (nbTirsB'=nbTirsB+1) +
1/4: (scoreB'= 1) & (rateB'=false) & (pretB'=false) & (nbTirsB'=nbTirsB+1) +
(1-(1/16+1/8+1/4)) : (scoreB' = 0) & (rateB'=true) & (pretB'=false) & (nbTirsB'=nbTirsB+1) ;
endmodule
module Marion
scoreM: [0..3];
pretM : bool init false;
rateM : bool init false;
nbTirsM: [0..100] init 0;
[initM] pretM=false & pretB=false & nbTirsM < 100 -> (pretM'=true);
[initM] pretM=false & pretB=false & nbTirsM < 100 -> (pretM'=false);
[tirM] pretM=true & nbTirsM+nbTirsB < 4 & nbTirsM < 100 -> 1/16 : (scoreM' = 3) & (pretM'=false) & (nbTirsM' = nbTirsM+1) & (rateM'=false) +
1/6 : (scoreM' = 2) & (pretM'=false) & (nbTirsM' = nbTirsM+1) & (rateM'=false) +
3/16 : (scoreM'= 1) & (pretM'=false) & (nbTirsM' = nbTirsM+1) & (rateM'=false) +
(1-(1/16+1/6+3/16)) : (scoreM' = 0) & (pretM'=false) & (nbTirsM' = nbTirsM+1) & (rateM'=true) ;
[tirM] pretM=true & nbTirsM+nbTirsB >= 4 & nbTirsM < 100 -> 1/8: (scoreM' = 3) & (pretM'=false) & (nbTirsM' = nbTirsM+1) & (rateM'=false) +
1/3 : (scoreM' = 2) & (pretM'=false) & (nbTirsM' = nbTirsM+1) & (rateM'=false) +
3/8 : (scoreM'= 1) & (pretM'=false) & (nbTirsM' = nbTirsM+1) & (rateM'=false) +
(1-(1/8+1/3+3/8)) : (scoreM' = 0) & (pretM'=false) & (nbTirsM' = nbTirsM+1) & (rateM'=true) ;
endmodule
rewards
[initB] true : scoreM;
[initM] true: scoreB;
endrewards