Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / regression_tests / check_validity.lus @ e2068500

History | View | Annotate | Download (721 Bytes)

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