Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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