mirela / scp

Go to a project
Toggle navigation Toggle navigation pinning
Johan ARCILE
5ce777da 1 parent f587f2e1

Upload new file

Inline Side-by-side
Showing 1 changed file with 202 additions and 0 deletions
1 +pta
2 +
3 +formula fk1Ca = (sU=1);
4 +formula fk2Ca = (sCa=3);
5 +formula fk1I = (sF=1) | (sF=8);
6 +formula fk2I = (sI=3);
7 +formula fk1F = (sL=1) | (sL=3);
8 +formula fk2F = (sF=6) | (sF=11);
9 +formula fk1U = (sL=1);
10 +formula fk2U = (sU=9);
11 +formula fk1L = (sF=1) | (sF=3);
12 +formula fk2L = (sL=11);
13 +formula flock1 = (sU=4) | (sL=6) | (sG=1);
14 +formula flock2 = (sM=1);
15 +formula funlock1 = (sU=7) | (sL=9) | (sG=4);
16 +formula funlock2 = (sM=3);
17 +
18 +
19 +
20 +module mCa
21 + xCa : clock;
22 + sCa : [0..3] init 0;
23 +
24 + invariant
25 + (sCa=0 => xCa <= 3000) &
26 + (sCa=1 => xCa <= 4500) &
27 + (sCa=2 => xCa <= 0)
28 + endinvariant
29 +
30 + [] sCa=0 & xCa >= 2000 -> (sCa'=1) & (xCa'=0);
31 + [] sCa=1 & xCa >= 3500 -> (sCa'=2) & (xCa'=0);
32 + [k1Ca] sCa=2 -> (sCa'=1) & (xCa'=0);
33 + [] sCa=2 & !fk1Ca -> (sCa'=3);
34 + [k2Ca] sCa=3 -> (sCa'=1) & (xCa'=0);
35 +endmodule
36 +
37 +module mI
38 + xI : clock;
39 + sI : [0..3] init 0;
40 +
41 + invariant
42 + (sI=0 => xI <= 600) &
43 + (sI=1 => xI <= 1000) &
44 + (sI=2 => xI <= 0)
45 + endinvariant
46 +
47 + [] sI=0 & xI >= 400 -> (sI'=1) & (xI'=0);
48 + [] sI=1 & xI >= 900 -> (sI'=2) & (xI'=0);
49 + [k1I] sI=2 -> (sI'=1) & (xI'=0);
50 + [] sI=2 & !fk1I -> (sI'=3);
51 + [k2I] sI=3 -> (sI'=1) & (xI'=0);
52 +endmodule
53 +
54 +module mU
55 + xU : clock;
56 + sU : [0..9] init 0;
57 +
58 + invariant
59 + (sU=0 => xU<=0) &
60 + (sU=2 => xU<=9000) &
61 + (sU=3 => xU<=0) &
62 + (sU=5 => xU<=400) &
63 + (sU=6 => xU<=0) &
64 + (sU=8 => xU<=0)
65 + endinvariant
66 +
67 + [k2Ca] sU=0 -> (sU'=2) & (xU'=0);
68 + [] sU=0 & !fk2Ca -> (sU'=1);
69 + [k1Ca] sU=1 -> (sU'=2) & (xU'=0);
70 + [] sU=2 & xU >= 7000 -> (sU'=3) & (xU'=0);
71 + [] sU=3 & !flock2 -> (sU'=4);
72 + [lock2U] sU=3 -> (sU'=5) & (xU'=0);
73 + [lock1U] sU=4 -> (sU'=5) & (xU'=0);
74 + [] sU=5 & xU >= 300 -> (sU'=6) & (xU'=0);
75 + [] sU=6 & !funlock2 -> (sU'=7);
76 + [unlock2U] sU=6 -> (sU'=8) & (xU'=0);
77 + [unlock1U] sU=7 -> (sU'=8) & (xU'=0);
78 + [k2U] sU=8 -> (sU'=0) & (xU'=0);
79 + [] sU=8 & !fk2U -> (sU'=9);
80 + [k1U] sU=9 -> (sU'=0) & (xU'=8);
81 +
82 +
83 +endmodule
84 +
85 +module mF
86 + xF : clock;
87 + sF : [0..11] init 7;
88 +
89 + invariant
90 + (sF=0 => xF<=0) &
91 + (sF=2 => xF<=0) &
92 + (sF=4 => xF<=60) &
93 + (sF=5 => xF<=0) &
94 + (sF=7 => xF<=0) &
95 + (sF=9 => xF<=60) &
96 + (sF=10 => xF<=0)
97 + endinvariant
98 +
99 + [k2I] sF=0 -> (sF'=2) & (xF'=0);
100 + [k2L] sF=0 -> (sF'=4) & (xF'=0);
101 + [] sF=0 & !fk2I & !fk2L -> (sF'=1);
102 + [k1I] sF=1 -> (sF'=2) & (xF'=0);
103 + [k1L] sF=1 -> (sF'=4) & (xF'=0);
104 + [k2L] sF=2 -> (sF'=4) & (xF'=0);
105 + [] sF=2 & !fk2L -> (sF'=3);
106 + [k1L] sF=3 -> (sF'=4) & (xF'=0);
107 + [] sF=4 & xF >= 40 -> (sF'=5) & (xF'=0);
108 + [] sF=5 & !fk1F -> (sF'=6);
109 + [k1F] sF=5 -> (sF'=0) & (xF'=0);
110 + [k2F] sF=6 -> (sF'=0) & (xF'=0);
111 + [k2I] sF=7 -> (sF'=9) & (xF'=0);
112 + [] sF=7 & !fk2I -> (sF'=8);
113 + [k1I] sF=8 -> (sF'=9) & (xF'=0);
114 + [] sF=9 & xF >= 40 -> (sF'=10) & (xF'=0);
115 + [] sF=10 & !fk1F -> (sF'=11);
116 + [k1F] sF=10 -> (sF'=0) & (xF'=0);
117 + [k2F] sF=11 -> (sF'=0) & (xF'=0);
118 +endmodule
119 +
120 +module mL
121 + xL : clock;
122 + sL : [0..11] init 0;
123 +
124 + invariant
125 + (sL=0 => xL<=0) &
126 + (sL=2 => xL<=0) &
127 + (sL=4 => xL<=30) &
128 + (sL=5 => xL<=0) &
129 + (sL=7 => xL<=20) &
130 + (sL=8 => xL<=0) &
131 + (sL=10 => xL<=0)
132 + endinvariant
133 +
134 + [k2U] sL=0 -> (sL'=2) & (xL'=0);
135 + [k2F] sL=0 -> (sL'=4) & (xL'=0);
136 + [] sL=0 & !fk2U & !fk2F -> (sL'=1);
137 + [k1U] sL=1 -> (sL'=2) & (xL'=0);
138 + [k1F] sL=1 -> (sL'=4) & (xL'=0);
139 + [k2F] sL=2 -> (sL'=4) & (xL'=0);
140 + [] sL=2 & !fk2F -> (sL'=3);
141 + [k1F] sL=3 -> (sL'=4) & (xL'=0);
142 + [] sL=4 & xL >= 20 -> (sL'=5) & (xL'=0);
143 + [] sL=5 & !flock2 -> (sL'=6);
144 + [lock2L] sL=5 -> (sL'=7) & (xL'=0);
145 + [lock1L] sL=6 -> (sL'=7) & (xL'=0);
146 + [] sL=7 & xL >= 10 -> (sL'=8) & (xL'=0);
147 + [] sL=8 & !funlock2 -> (sL'=9);
148 + [unlock2L] sL=8 -> (sL'=10) & (xL'=0);
149 + [unlock1L] sL=9 -> (sL'=10) & (xL'=0);
150 + [k2L] sL=10 -> (sL'=0) & (xL'=0);
151 + [] sL=10 & !fk2L -> (sL'=11);
152 + [k1L] sL=11 -> (sL'=0) & (xL'=8);
153 +
154 +endmodule
155 +
156 +module mM
157 + xM : clock;
158 + sM : [0..3] init 1;
159 +
160 + invariant
161 + (sM=0 => xM<=0) &
162 + (sM=2 => xM<=0)
163 + endinvariant
164 +
165 + [] sM=0 & !flock1-> (sM'=1);
166 + [lock1L] sM=0 -> (sM'=2) & (xM'=0);
167 + [lock1U] sM=0 -> (sM'=2) & (xM'=0);
168 + [lock1G] sM=0 -> (sM'=2) & (xM'=0);
169 + [lock2L] sM=1 -> (sM'=2) & (xM'=0);
170 + [lock2U] sM=1 -> (sM'=2) & (xM'=0);
171 + [lock2G] sM=1 -> (sM'=2) & (xM'=0);
172 + [] sM=2 & !funlock1 -> (sM'=3);
173 + [unlock1L] sM=2 -> (sM'=0) & (xM'=0);
174 + [unlock1U] sM=2 -> (sM'=0) & (xM'=0);
175 + [unlock1G] sM=2 -> (sM'=0) & (xM'=0);
176 + [unlock2L] sM=3 -> (sM'=0) & (xM'=0);
177 + [unlock2U] sM=3 -> (sM'=0) & (xM'=0);
178 + [unlock2G] sM=3 -> (sM'=0) & (xM'=0);
179 +
180 +endmodule
181 +
182 +module mG
183 + xG : clock;
184 + sG : [0..5] init 0;
185 +
186 + invariant
187 + (sG=0 => xG<=0) &
188 + (sG=2 => xG<=420) &
189 + (sG=3 => xG<=0) &
190 + (sG=5 => xG<=750)
191 + endinvariant
192 +
193 + [lock2G] sG=0 -> (sG'=2) & (xG'=0);
194 + [] sG=0 & !flock2 -> (sG'=1);
195 + [lock1G] sG=1 -> (sG'=2) & (xG'=0);
196 + [] sG=2 & xG >= 310 -> (sG'=3) & (xG'=0);
197 + [unlock2G] sG=3 -> (sG'=5) & (xG'=0);
198 + [] sG=3 & !funlock2 -> (sG'=4);
199 + [unlock1G] sG=4 -> (sG'=5) & (xG'=0);
200 + [] sG=5 & xG >= 500 -> (sG'=0) & (xG'=0);
201 +
202 +endmodule