lustrec / regression_tests / local_inline.lus @ e41592cf
History | View | Annotate | Download (8.41 KB)
1 |
|
---|---|
2 |
|
3 |
-- |=================================================================| |
4 |
-- |
5 |
-- Specification nodes. |
6 |
-- |
7 |
-- |=================================================================| |
8 |
|
9 |
|
10 |
|
11 |
node Rise |
12 |
(I : bool) |
13 |
returns |
14 |
(O : bool); |
15 |
let |
16 |
O = false -> (not pre I) and I; |
17 |
tel; |
18 |
|
19 |
|
20 |
|
21 |
-- |=================================================================| |
22 |
-- |
23 |
-- System nodes. |
24 |
-- |
25 |
-- |=================================================================| |
26 |
|
27 |
|
28 |
node PFS_Logic |
29 |
(riseTS, riseOSPF : bool; |
30 |
Primary_Side : bool; |
31 |
PFS_Initial_Value : bool) |
32 |
returns |
33 |
(PFS : bool); |
34 |
|
35 |
var |
36 |
-- Pfs_change: bool; |
37 |
-- Has_happened: bool; |
38 |
Start_to_Pilot_Flying: bool; |
39 |
Start_to_Inhibited: bool; |
40 |
Inhibited_to_Listening: bool; |
41 |
Inhibited_to_Inhibited: bool; |
42 |
Listening_to_Pilot_Flying: bool; |
43 |
Pilot_Flying_to_Inhibited : bool; |
44 |
State : int; |
45 |
Inhibit_count: int; |
46 |
Inhibit_count_bounded : bool; |
47 |
Pfs_state_consistency : bool; |
48 |
State_bounded : bool; |
49 |
St_Inhibited: int; |
50 |
St_Listening : int; |
51 |
St_Pilot_Flying : int; |
52 |
St_Start : int; |
53 |
St_Stop : int; |
54 |
Inhibit_count_max: int; |
55 |
let |
56 |
|
57 |
-- MAIN; |
58 |
assert Primary_Side = (Primary_Side -> pre( Primary_Side)); |
59 |
assert PFS_Initial_Value = (PFS_Initial_Value -> pre( PFS_Initial_Value)); |
60 |
assert State>=0 and State <=5; |
61 |
assert Inhibit_count>=0 and Inhibit_count <=2; |
62 |
|
63 |
Inhibit_count_max = 2 -> pre(Inhibit_count_max); |
64 |
St_Inhibited = 2 -> pre(St_Inhibited); |
65 |
St_Listening = 3 -> pre(St_Listening); |
66 |
St_Pilot_Flying = 4 -> pre(St_Pilot_Flying); |
67 |
St_Start = 1 -> pre(St_Start); |
68 |
St_Stop = 5-> pre(St_Stop); |
69 |
|
70 |
Start_to_Pilot_Flying = |
71 |
((St_Start -> pre(State)) = St_Start) and Primary_Side; |
72 |
|
73 |
Start_to_Inhibited = |
74 |
((St_Start -> pre(State)) = St_Start) and (not Primary_Side); |
75 |
|
76 |
Inhibited_to_Listening = |
77 |
((St_Start -> pre(State)) = St_Inhibited) and |
78 |
(0 -> pre( Inhibit_count)) >= Inhibit_count_max; |
79 |
|
80 |
Inhibited_to_Inhibited = |
81 |
((St_Start -> pre(State)) = St_Inhibited) and |
82 |
not Inhibited_to_Listening; |
83 |
|
84 |
Listening_to_Pilot_Flying = |
85 |
((St_Start -> pre(State)) = St_Listening) and riseTS; |
86 |
|
87 |
Pilot_Flying_to_Inhibited = |
88 |
((St_Start -> pre(State)) = St_Pilot_Flying) and riseOSPF; |
89 |
|
90 |
State = |
91 |
if |
92 |
Inhibited_to_Inhibited or |
93 |
Pilot_Flying_to_Inhibited or |
94 |
Start_to_Inhibited |
95 |
then |
96 |
St_Inhibited |
97 |
else if |
98 |
Inhibited_to_Listening |
99 |
then |
100 |
St_Listening |
101 |
else if |
102 |
Listening_to_Pilot_Flying or |
103 |
Start_to_Pilot_Flying |
104 |
then |
105 |
St_Pilot_Flying |
106 |
else |
107 |
(St_Start -> pre(State)); |
108 |
|
109 |
PFS = |
110 |
if |
111 |
Listening_to_Pilot_Flying |
112 |
then |
113 |
true |
114 |
else if |
115 |
Pilot_Flying_to_Inhibited |
116 |
then |
117 |
false |
118 |
else if |
119 |
Start_to_Pilot_Flying |
120 |
then |
121 |
true |
122 |
else if |
123 |
Start_to_Inhibited |
124 |
then |
125 |
false |
126 |
else |
127 |
PFS_Initial_Value -> pre(PFS); |
128 |
|
129 |
Inhibit_count = |
130 |
if |
131 |
Inhibited_to_Inhibited |
132 |
then |
133 |
(0 -> pre( Inhibit_count)) + 1 |
134 |
else if |
135 |
Pilot_Flying_to_Inhibited |
136 |
then |
137 |
0 |
138 |
else if |
139 |
Start_to_Inhibited |
140 |
then |
141 |
0 |
142 |
else |
143 |
0 -> pre( Inhibit_count); |
144 |
|
145 |
Pfs_state_consistency = |
146 |
not (State = St_Start) => (PFS = (State = St_Pilot_Flying)); |
147 |
|
148 |
-- PROPERTY Pfs_state_consistency; |
149 |
|
150 |
-- Proved as property before |
151 |
-- assert Pfs_state_consistency; |
152 |
|
153 |
Inhibit_count_bounded = |
154 |
Inhibit_count >= 0 and Inhibit_count <= Inhibit_count_max; |
155 |
|
156 |
-- PROPERTY Inhibit_count_bounded; |
157 |
|
158 |
-- Proved as property before |
159 |
-- assert Inhibit_count_bounded; |
160 |
|
161 |
State_bounded = State >= St_Start and State < St_Stop; |
162 |
|
163 |
-- -- PROPERTY State_bounded; |
164 |
|
165 |
-- Proved as property before |
166 |
-- assert State_bounded; |
167 |
|
168 |
tel; |
169 |
|
170 |
node PFS_Side |
171 |
(TS, OSPF : bool; |
172 |
Primary_Side : bool; |
173 |
PFS_Initial_Value : bool) |
174 |
|
175 |
returns |
176 |
(PFS : bool); |
177 |
|
178 |
|
179 |
var |
180 |
PFSL_PFS : bool; |
181 |
riseTS_O : bool; |
182 |
riseOSPF_O : bool; |
183 |
|
184 |
let |
185 |
|
186 |
-- assert Primary_Side= (Primary_Side -> pre(Primary_Side)); |
187 |
-- assert PFS_Initial_Value= (PFS_Initial_Value -> pre(PFS_Initial_Value)); |
188 |
|
189 |
-- MAIN; |
190 |
|
191 |
PFSL_PFS = |
192 |
PFS_Logic(riseTS_O, riseOSPF_O, Primary_Side, PFS_Initial_Value); |
193 |
|
194 |
riseTS_O = Rise(TS); |
195 |
|
196 |
riseOSPF_O = Rise(OSPF); |
197 |
|
198 |
PFS = PFSL_PFS; |
199 |
|
200 |
tel; |
201 |
|
202 |
|
203 |
|
204 |
node Cross_Channel_Bus |
205 |
(I : bool; |
206 |
O_Initial_Value : bool; |
207 |
prev_I_Initial_Value : bool) |
208 |
returns |
209 |
(O : bool); |
210 |
var |
211 |
Prev_I : bool; |
212 |
Start_to_Step : bool; |
213 |
Step_to_Step : bool; |
214 |
-- State_bounded : bool; |
215 |
|
216 |
--state : subrange [1,3] of int; |
217 |
State : int; |
218 |
-- state : enum { St_Step, St_Start }; |
219 |
|
220 |
-- const St_Step = 2; |
221 |
-- const St_Start = 1; |
222 |
-- const St_Stop = 3; |
223 |
St_Step : int; |
224 |
St_Start : int; |
225 |
St_Stop : int; |
226 |
let |
227 |
-- assert O_Initial_Value= (O_Initial_Value -> pre(O_Initial_Value)); |
228 |
-- assert prev_I_Initial_Value = (prev_I_Initial_Value -> pre( prev_I_Initial_Value )); |
229 |
assert State>=1 and State <=3; |
230 |
|
231 |
St_Step = 2 -> pre(St_Step); |
232 |
St_Start = 1 -> pre(St_Start); |
233 |
St_Stop = 3 -> pre(St_Stop); |
234 |
|
235 |
Start_to_Step = (St_Start -> pre(State)) = St_Start; |
236 |
|
237 |
Step_to_Step = (St_Start -> pre(State)) = St_Step; |
238 |
|
239 |
State = |
240 |
if |
241 |
Start_to_Step or Step_to_Step |
242 |
then |
243 |
St_Step |
244 |
else |
245 |
(St_Start -> pre(State)); |
246 |
|
247 |
Prev_I = |
248 |
if Start_to_Step then I |
249 |
else if Step_to_Step then I |
250 |
else prev_I_Initial_Value -> pre(Prev_I); |
251 |
|
252 |
O = |
253 |
if |
254 |
Start_to_Step |
255 |
then |
256 |
prev_I_Initial_Value -> pre(Prev_I) |
257 |
else if |
258 |
Step_to_Step |
259 |
then |
260 |
prev_I_Initial_Value -> pre(Prev_I) |
261 |
else |
262 |
O_Initial_Value -> pre(O); |
263 |
|
264 |
tel; |
265 |
|
266 |
|
267 |
|
268 |
|
269 |
-- |=================================================================| |
270 |
-- |
271 |
-- Top level environment nodes. |
272 |
-- |
273 |
-- |=================================================================| |
274 |
|
275 |
|
276 |
node PRESSED (p : bool) returns (b : bool); |
277 |
let |
278 |
b = false -> (not pre p and p); |
279 |
tel; |
280 |
|
281 |
node PRESSED_SEEN (p, c : bool) returns (b : bool); |
282 |
let |
283 |
b = false -> (not pre p and pre c) and (p and c); |
284 |
tel; |
285 |
|
286 |
node CHANGED (p : bool) returns (b : bool); |
287 |
let |
288 |
b = false -> not (p = pre p); |
289 |
tel; |
290 |
|
291 |
node false_longer_than (p: bool; n: int) returns (ok: bool); |
292 |
|
293 |
var |
294 |
c: int; |
295 |
|
296 |
let |
297 |
|
298 |
-- assert n = (n -> pre(n)); |
299 |
c = if p then 0 else (1 -> pre c + 1); |
300 |
|
301 |
ok = c > n; |
302 |
|
303 |
tel; |
304 |
|
305 |
node quiescent |
306 |
(TS, CLK1, CLK3, CLK2, CLK4 : bool) |
307 |
returns |
308 |
(out : bool) ; |
309 |
let |
310 |
out = |
311 |
false_longer_than(PRESSED(TS), 46) and |
312 |
false_longer_than(PRESSED(TS), 46) and |
313 |
false_longer_than(PRESSED(TS), 46) and |
314 |
false_longer_than(PRESSED(TS), 46) ; |
315 |
tel |
316 |
|
317 |
|
318 |
-- |=================================================================| |
319 |
-- |
320 |
-- Top level node. |
321 |
-- |
322 |
-- |=================================================================| |
323 |
|
324 |
|
325 |
|
326 |
node PFS |
327 |
(TS, CLK1, CLK3, CLK2, CLK4 : bool) |
328 |
returns |
329 |
(LPFS, RPFS : bool) ; |
330 |
var |
331 |
RL_O : bool; |
332 |
RS_PFS : bool; |
333 |
LR_O : bool; |
334 |
LS_PFS : bool; |
335 |
|
336 |
let |
337 |
|
338 |
LS_PFS = |
339 |
-- condact(CLK1, PFS_Side(TS, RL_O, true, true), true); |
340 |
PFS_Side(TS, RL_O, true, true); |
341 |
|
342 |
RS_PFS = |
343 |
-- condact(CLK3, PFS_Side(TS, LR_O, false, false), false); |
344 |
PFS_Side(TS, LR_O, false, false); |
345 |
|
346 |
LR_O = |
347 |
-- condact(CLK2, Cross_Channel_Bus (LS_PFS, true, true), true); |
348 |
((*! /inlining/: true; *)Cross_Channel_Bus (LS_PFS, true, true)); |
349 |
|
350 |
RL_O = |
351 |
-- condact(CLK4, Cross_Channel_Bus (RS_PFS, false, false), false); |
352 |
Cross_Channel_Bus (RS_PFS, false, false); |
353 |
|
354 |
LPFS = LS_PFS; |
355 |
|
356 |
RPFS = RS_PFS; |
357 |
|
358 |
tel; |
359 |
|
360 |
-- node PFS_contract_R5 |
361 |
-- (TS, CLK1, CLK3, CLK2, CLK4 : bool) |
362 |
-- returns |
363 |
-- (OK : bool) ; |
364 |
-- var |
365 |
-- LPFS: bool; |
366 |
-- RPFS: bool; |
367 |
-- req: bool; |
368 |
-- let |
369 |
-- req = quiescent(TS, CLK1, CLK2, CLK3, CLK4) ; |
370 |
-- assert req; |
371 |
-- LPFS, RPFS = PFS (TS, CLK1, CLK3, CLK2, CLK4); |
372 |
-- OK = not (CHANGED(RPFS) or CHANGED(LPFS)) ; |
373 |
-- --!PROPERTY : OK; |
374 |
-- --!MAIN : true; |
375 |
-- tel |
376 |
|
377 |
|
378 |
|
379 |
-- node PFS_contract_R3 |
380 |
-- (TS, CLK1, CLK3, CLK2, CLK4 : bool) |
381 |
-- returns |
382 |
-- (OK : bool) ; |
383 |
-- var |
384 |
-- LPFS: bool; |
385 |
-- RPFS: bool; |
386 |
-- req: bool; |
387 |
-- let |
388 |
|
389 |
-- LPFS, RPFS = PFS (TS, CLK1, CLK3, CLK2, CLK4); |
390 |
|
391 |
-- req = true -> pre quiescent(TS, CLK1, CLK2, CLK3, CLK4) ; |
392 |
-- assert req; |
393 |
-- OK = true -> ( |
394 |
-- (not pre LPFS and PRESSED_SEEN(TS, CLK1) => LPFS) and |
395 |
-- (not pre RPFS and PRESSED_SEEN(TS, CLK3) => RPFS) |
396 |
-- ) ; |
397 |
-- --!PROPERTY : OK; |
398 |
-- --!MAIN : true; |
399 |
-- tel |
400 |
|
401 |
|
402 |
|
403 |
node top |
404 |
(TS, CLK1, CLK3, CLK2, CLK4 : bool) |
405 |
returns |
406 |
(OK : bool) ; |
407 |
var |
408 |
LPFS: bool; |
409 |
RPFS: bool; |
410 |
req: bool; |
411 |
let |
412 |
LPFS, RPFS = PFS (TS, CLK1, CLK3, CLK2, CLK4); |
413 |
req = quiescent(TS, CLK1, CLK2, CLK3, CLK4) ; |
414 |
--assert req; |
415 |
OK = LPFS = not RPFS ; |
416 |
--!PROPERTY : OK; |
417 |
--!MAIN : true; |
418 |
tel |