lustrec-tests/regression_tests/lustre_files/success/automata/with_properties/test_ok.lus @ 02d89bbb
| 1 | 02d89bbb | bourbouh | node top (x:bool) returns (ok: bool); |
|---|---|---|---|
| 2 | var bit: bool; |
||
| 3 | coin: bool; |
||
| 4 | let
|
||
| 5 | automaton mini_states |
||
| 6 | state Even : |
||
| 7 | let
|
||
| 8 | bit = true; |
||
| 9 | tel until true restart Odd |
||
| 10 | state Odd : |
||
| 11 | let
|
||
| 12 | bit = false; |
||
| 13 | tel until true restart Even |
||
| 14 | |||
| 15 | coin = true -> not pre coin; |
||
| 16 | ok = bit = coin; |
||
| 17 | tel
|