-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathmodules
executable file
·56 lines (50 loc) · 2.63 KB
/
modules
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
47
48
49
50
51
52
53
54
55
56
dtmc
module Dmitry
scoreD: [0..3];
pretD : bool;
nbTirsD : [0..100] init 0;
[initD] pretD=false & nbTirsD < 100 -> (pretD'=true);
[tirD] pretD=true & nbTirsD < 100 -> 1/10 : (scoreD'=3) & (pretD'=false) & (nbTirsD'=nbTirsD+1) +
1/6 : (scoreD'=2) & (pretD'=false) & (nbTirsD'=nbTirsD+1) +
1/4 : (scoreD'=1) & (pretD'=false) & (nbTirsD'=nbTirsD+1) +
(1-(1/10+1/6+1/4)) : (scoreD'=0) & (pretD'=false) & (nbTirsD'=nbTirsD+1) ;
endmodule
module Brigitte
scoreB: [0..3];
nbTirsB : [0..100] init 0;
pretB : bool;
rateB: bool init false;
[initB] pretB=false & nbTirsB < 100 -> (pretB'=true);
[tirB] pretB= true & !rateB & 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 & 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;
nbTirsM: [0..100] init 0;
[initM] pretM=false & nbTirsM < 100 -> (pretM'=true);
[tirM] pretM=true & nbTirsM < 4 & nbTirsM < 100 -> 1/16 : (scoreM' = 3) & (pretM'=false) & (nbTirsM' = nbTirsM+1) +
1/6 : (scoreM' = 2) & (pretM'=false) & (nbTirsM' = nbTirsM+1) +
3/16 : (scoreM'= 1) & (pretM'=false) & (nbTirsM' = nbTirsM+1) +
(1-(1/16+1/6+3/16)) : (scoreM' = 0) & (pretM'=false) & (nbTirsM' = nbTirsM+1) ;
[tirM] pretM=true & nbTirsM >= 4 & nbTirsM < 100 -> 1/8: (scoreM' = 3) & (pretM'=false) & (nbTirsM' = nbTirsM+1) +
1/3 : (scoreM' = 2) & (pretM'=false) & (nbTirsM' = nbTirsM+1) +
3/8 : (scoreM'= 1) & (pretM'=false) & (nbTirsM' = nbTirsM+1) +
(1-(1/8+1/3+3/8)) : (scoreM' = 0) & (pretM'=false) & (nbTirsM' = nbTirsM+1) ;
endmodule
module Horatiu
scoreH: [0..3];
pretH : bool;
nbTirsH: [0..100] init 0;
[initH] pretH=false & nbTirsH < 100 -> (pretH'=true);
[tirH] pretH=true & nbTirsH != 4 & nbTirsH < 100 -> 1/4 : (scoreH' = 3) & (nbTirsH'= nbTirsH + 1) & (pretH'=false)+
3/4 : (scoreH' = 0) & (nbTirsH' = nbTirsH+1) & (pretH'=false);
[tirH] pretH=true & nbTirsH >= 4 & nbTirsH < 100 -> 1/8 : (scoreH' = 3) & (nbTirsH'= nbTirsH + 1) & (pretH'=false)+
7/8 : (scoreH' = 0) & (nbTirsH'= nbTirsH + 1) & (pretH'=false);
endmodule