lustrec-tests/tests/automata/heater4.lus @ 4784e95f
| 1 |
(*@ ensures open_light; *)
|
|---|---|
| 2 |
node command(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
|