lustrectests/regression_tests/lustre_files/success/automata/without_properties/tawoa_automata.lus @ cc6eda98
1  

2 
node tawoa_automata(input : int) returns (ok: bool); 
3 
var x1, x2 : int; 
4 
y1, y2:int; 
5 
let

6 
automaton aut1 
7 
state A : 
8 
let

9 
x1 = input; 
10 
y1 = x2; 
11 
tel

12 
until true restart B 
13 
state B : 
14 
let

15 
x1 = 1;  x1 = x2; 
16 
y1 = 1; 
17 
tel

18 
until true restart A 
19 
automaton aut2 
20 
state C : 
21 
let

22 
x2 = x1; 
23 
y2 = 2; 
24 
tel

25 
until true restart D 
26 
state D : 
27 
let

28 
x2 = input; 
29 
y2 = x2;  y2 = x1; 
30 
tel

31 
until true restart C 
32  
33 
ok = y1 = input  y2 = input; 
34 
tel
