### Profile

« Previous | Next »

## Revision e599394b

#### Added by Teme Kahsaiover 6 years ago

cleaned up bin

View differences:

regression_tests/check_validity.lus
1

2
```node check_validity (x: bool; n: int) returns (y: bool; nb_times: int);
```
3
```var
```
4
```compt: int;
```
5
```let
```
6
```  compt = (if x then 1 else 0) -> if x then pre compt + 1 else 0;
```
7
```  y = (compt >= n);
```
8
```  nb_times= (if x then 1 else 0) ->
```
9
```    if x then pre nb_times + 1 else
```
10
```      (if pre nb_times > 0 then pre nb_times - 1 else 0);
```
11
```tel
```
12

13

14
```node lock (x, reset: bool) returns (y: bool);
```
15
```let
```
16
```y = x -> if reset then x else x or pre y;
```
17
```tel
```
18

19

20
```node check_validity_lock (x: bool; n: int) returns (y: bool);
```
21
```var
```
22
```  nb_times: int;
```
23
```  er: bool;
```
24
```let
```
25
```	(er, nb_times) = check_validity(x, n);
```
26
```	y = x or lock(er, (nb_times = 0));
```
27
```tel
```
28

29
```node top (x: bool; n: int) returns (ok: bool);
```
30
```let
```
31
``` ok = x => check_validity_lock(x, n);
```
32
``` --!PROPERTY: ok;
```
33
``` --!MAIN: true;
```
34
```tel
```
regression_tests/local_inline.lus
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
```
regression_tests/stateful_assert.lus
1

2
```node top
```
3
```  (TS, OSPF : bool;
```
4
```   Primary_Side : bool)
```
5

6
```returns
```
7
```  (PFS : bool);
```
8

9
```var
```
10
```  PFSL_PFS : bool;
```
11
```  riseTS_O : bool;
```
12
```  riseOSPF_O : bool;
```
13
```
```
14
```let
```
15
```assert Primary_Side = (Primary_Side -> pre(Primary_Side));
```
16
```  PFSL_PFS = riseTS_O or  riseOSPF_O or Primary_Side;
```
17
```
```
18
```  riseTS_O = true;
```
19

20
```  riseOSPF_O = false;
```
21

22
```  PFS = PFSL_PFS;
```
23

24
```tel;
```
regression_tests/traffic.lus
1

2
```--
```
3
```-- Source: Koen Classen
```
4
```--
```
5
```-- given
```
6

7
```node Sofar( X : bool ) returns ( Y : bool );
```
8
```let
```
9
```  Y = (true -> pre Y) and X;
```
10
```tel
```
11

12
```-- assignment other
```
13

14
```node Store( Delta : int ) returns ( Total : int );
```
15
```var Prev : int;
```
16
```let
```
17
```
```
18
```  Prev  = 0 -> pre Total;
```
19
```  Total = if Delta < 0 and Prev > 0  then Prev+Delta
```
20
```     else if Delta > 0 and Prev < 10 then Prev+Delta
```
21
```     else Prev;
```
22
```tel
```
23

24

25

26
```node top( Delta : int ) returns ( OK : bool );
```
27
```var Total : int;
```
28
```    S: bool;
```
29
```    -- Delta_const :  int;
```
30
```let
```
31
```  -- Delta_const = Delta -> pre Delta_const;
```
32
```  Total = Store( Delta );
```
33
```
```
34
```  S =  Sofar( -1 <= Delta and Delta <= 1 );
```
35
```  OK = S => 0 <= Total and Total <= 20;
```
36
```  --!PROPERTY :  OK=true;
```
37
```  --!MAIN:true;
```
38
```tel
```

Also available in: Unified diff