lustrec-tests/regression_tests/lustre_files/success/automata/with_properties/heater4.lus @ 02d89bbb
1 |
(*@ ensures open_light; *)
|
---|---|
2 |
node top(millisecond : bool) returns (open_light : bool) |
3 |
let
|
4 |
automaton command_control |
5 |
state Open : |
6 |
let
|
7 |
open_light = true; |
8 |
tel
|
9 |
|
10 |
state Silent : |
11 |
let
|
12 |
open_light = false; |
13 |
tel
|
14 |
|
15 |
tel
|