Ex3_b.nm
2.3 KB
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
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
pta
formula fk1Ca = (sPr=1) | (sPr=3);
formula fk2Ca = (sCa=3);
formula fk1O = (sPr=1);
formula fk2O = (sO=2);
formula fk3O = (sF=1);
formula fk4O = (sO=4);
formula fk1P = (sF=1);
formula fk2P = (sP=3);
module mCa
xCa : clock;
sCa : [0..3] init 0;
invariant
(sCa=0 => xCa <= 5000) &
(sCa=1 => xCa <= 5000) &
(sCa=2 => xCa <= 0)
endinvariant
[] sCa=0 & xCa >= 100 -> (sCa'=1) & (xCa'=0);
[] sCa=1 & xCa >= 100 -> (sCa'=2) & (xCa'=0);
[k1Ca] sCa=2 -> (sCa'=1) & (xCa'=0);
[] sCa=2 & !fk1Ca -> (sCa'=3);
[k2Ca] sCa=3 -> (sCa'=1) & (xCa'=0);
endmodule
module mO
xO : clock;
sO : [0..4] init 0;
invariant
(sO=1 => xO <= 0) &
(sO=3 => xO <= 0)
endinvariant
[] sO=0 & xO >= 100 -> (sO'=1) & (xO'=0);
[k1O] sO=1 -> (sO'=3) & (xO'=0);
[] sO=1 & !fk1O -> (sO'=2);
[k2O] sO=2 -> (sO'=3) & (xO'=0);
[k3O] sO=3 -> (sO'=0) & (xO'=0);
[] sO=3 & !fk3O -> (sO'=4);
[k4O] sO=4 -> (sO'=0) & (xO'=0);
endmodule
module mP
xP : clock;
sP : [0..3] init 0;
invariant
(sP=0 => xP <= 5000) &
(sP=1 => xP <= 5000) &
(sP=2 => xP <= 0)
endinvariant
[] sP=0 & xP >= 100 -> (sP'=1) & (xP'=0);
[] sP=1 & xP >= 100 -> (sP'=2) & (xP'=0);
[k1P] sP=2 -> (sP'=1) & (xP'=0);
[] sP=2 & !fk1P -> (sP'=3);
[k2P] sP=3 -> (sP'=1) & (xP'=0);
endmodule
module mF
xF : clock;
sF : [0..2] init 0;
invariant
(sF=0 => xF<=0) &
(sF=2 => xF<=5000)
endinvariant
[k2P] sF=0 -> (sF'=2) & (xF'=0);
[k4O] sF=0 -> (sF'=2) & (xF'=0);
[] sF=0 & !fk2P & !fk4O -> (sF'=1);
[k1P] sF=1 -> (sF'=2) & (xF'=0);
[k13O] sF=1 -> (sF'=2) & (xF'=0);
[] sF=2 & xF >= 0 -> (sF'=0) & (xF'=0);
endmodule
module mPr
xPr : clock;
sPr : [0..4] init 0;
invariant
(sPr=0 => xPr<=0) &
(sPr=2 => xPr<=0) &
(sPr=4 => xPr<=5000)
endinvariant
[k2O] sPr=0 -> (sPr'=2) & (xPr'=0);
[k2Ca] sPr=0 -> (sPr'=4) & (xPr'=0);
[] sPr=0 & !fk2O & !fk2Ca -> (sPr'=1);
[k1O] sPr=1 -> (sPr'=2) & (xPr'=0);
[k1Ca] sPr=1 -> (sPr'=4) & (xPr'=0);
[k2Ca] sPr=2 -> (sPr'=4) & (xPr'=0);
[] sPr=2 & !fk2Ca -> (sPr'=3);
[k1Ca] sPr=3 -> (sPr'=4) & (xPr'=0);
[] sPr=4 & xPr >= 0 -> (sPr'=0) & (xPr'=0);
endmodule