Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / automata / with_properties / test_ok.lus @ 02d89bbb

History | View | Annotate | Download (290 Bytes)

1
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
18