Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (2.67 KB)

1

    
2
const low = 5;
3

    
4
const high = 5;
5

    
6
const delay_on = 200;
7

    
8
const delay_off = 500;
9

    
10
node edge(c : bool) returns (edge_c : bool)
11
let
12
  edge_c = false -> c && not (pre c);
13
tel
14

    
15
node count(d : int; t : bool) returns (ok : bool)
16
var cpt:int;
17
let
18
  ok = (cpt = 0);
19
  cpt = 0 -> (if t then pre cpt + 1 else pre cpt) mod d;
20
tel
21

    
22
(* controling the heat *)
23
(* returns [true] when [expected_temp] does not agree with [actual_temp] *)
24
node heat(expected_temp, actual_temp : int) returns (ok : bool)
25
let
26
  automaton heat_control
27
    state Stop :
28
          unless (actual_temp <= expected_temp - low) resume Start
29
          let
30
            ok = false; 
31
          tel
32
    state Start :
33
          unless (actual_temp >= expected_temp + high) resume Stop
34
          let
35
            ok = true;
36
          tel
37
tel
38

    
39
(* a cyclic two mode automaton with an internal timer *)
40
(* [open_light = true] and [open_gas = true] for [delay_on millisecond] *)
41
(* then [open_light = false] and [open_gas = false] for *)
42
(* [delay_off millisecond] *)
43
node command(millisecond : bool) returns (open_light, open_gas : bool)
44
let
45
  automaton command_control
46
    state Open :
47
          let
48
            open_light = true;
49
            open_gas = true;
50
          tel
51
          until count(delay_on, millisecond) restart Silent
52
    state Silent :
53
          let
54
            open_light = false;
55
            open_gas = false;
56
          tel
57
          until count(delay_off, millisecond) restart Open
58
tel
59

    
60
(* the main command which control the opening of the light and gas *)
61
node light(millisecond : bool; on_heat, on_light : bool) returns (open_light, open_gas, nok : bool)
62
let
63
  automaton light_control
64
    state Light_off :
65
          let
66
            nok = false;
67
            open_light = false;
68
            open_gas = false;
69
          tel
70
          until on_heat restart Try
71
    state Light_on :
72
          let
73
            nok = false;
74
            open_light = false;
75
            open_gas = true;
76
          tel
77
          until not on_heat restart Light_off
78
    state Try :
79
          let
80
            nok = false;
81
            (open_light, open_gas) = command(millisecond);
82
          tel
83
          until on_light restart Light_on
84
          until count(3, edge(not open_light)) restart Failure
85
    state Failure :
86
          let
87
            nok = true; 
88
            open_light = false;
89
            open_gas = false;
90
          tel
91
tel
92

    
93
(* the main function *)
94
node top(millisecond : bool; reset : bool; expected_temp, actual_temp : int; on_light : bool) returns ( ok : bool)
95
var on_heat, nok , open_light, open_gas: bool;
96
let
97
  on_heat = heat(expected_temp,actual_temp) every reset;
98
  (open_light, open_gas, nok) = light(millisecond, on_heat, on_light) every reset;
99
  ok = not nok;
100
tel