lustrec-tests/tests/automata/tawoa_automata.lus @ 4784e95f
1 |
|
---|---|
2 |
node essai(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
|