Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / doc / automata_spec.org @ 6eb92970

History | View | Annotate | Download (8.73 KB)

1
* Syntax 
2

    
3
An automaton definition is similar to the definition of flows in a Lustre node. 
4
The syntax in lustrec is the following:
5

    
6
automaton id
7
   (state Id:
8
     (unless cond (resume | restart) Id)*
9
     (var (id: type)+)?
10
     let
11
        (lustre_defs)+
12
     tel
13
     (until cond (resume | restart) Id)*
14
   )+
15

    
16
where
17
  id denotes regular lustre identifier 
18
  Id denotes an identifier starting with an uppercase letter
19
  type denotes a type
20
  cond denotes a lustre expression of type bool
21
  lustre_def denotes lustre flow definitions, either assignments or automata
22
  *,+,? denotes classical notations for regular expressions
23

    
24

    
25
Example
26

    
27
node auto (x:bool) returns (ok: bool);
28
var bit: bool;
29
    coin: bool;
30
let
31
  automaton mini_states
32
  state Even : 
33
  let 
34
    bit = true;
35
  tel until true restart Odd
36
  state Odd : 
37
  let 
38
    bit = false;
39
  tel until true restart Even
40

    
41
  coin = true -> not pre coin;
42
  ok = bit = coin;
43
tel
44
  
45
* Semantics
46

    
47
In terms of semantics, each automaton defines a tuple of flows. In our modelling
48
choice, each state should define all the elements of this tuple. Local variable
49
specific to a given state will also have to be defined is this state.
50

    
51
** Semantics
52

    
53
The semantics is the following: 
54

    
55
- the initial state is the first one described
56
- when executing a transition, the current active state is evaluated. 
57
  - UNLESS: First its unless definitions are executed, in order. The first one that
58
    matches identifies the real state that will be executed. 
59
  - CONTENT: If no such unless condition has been activated, the regular flow equations
60
    of the current node are performed. Otherwise we evaluate the content of the
61
    node selected by the activated unless definition. 
62
  - UNTIL: Once these equations have been performed, the until definitions are executed
63
    to identify the next active state. If no such until definition can be
64
    activated, the current state remains active.
65
- the kind resume/restart of state switch describe whether the node equation
66
  will have to rely on the initial definition or the regular one. Eg if x = 0 ->
67
  pre x in state S, a unless or until condition to state S with a restart will
68
  execute the equation x = 0 when it would have been x = pre x with a resume.
69

    
70
** Design choices 
71

    
72
*** Id for state names
73
During compilation, the tuple of variables defined by the automaton will be
74
substituted by regular Lustre v4 flow equations using clocks and merge. Clocks
75
will be defined over enumerated datatype representing the states of the
76
automaton. This explains the use of Id instead of id for state names.
77

    
78
*** No pre of internal memories for unless conditions
79
A syntactic restriction of our language prevents the use of the Lustre pre
80
construct over variables defined in the automaton in the condition appearing in
81
a unless definition: this would introduce a (potentially spurious) algebraic
82
loop. This is explained below.
83

    
84
*** Modular Lustre v4 compiled code
85

    
86
Our compilation scheme is modular and generates a Lustre v4 model where each
87
state is defined by a dedicated node -- more specifically two of them, one for
88
evaluating the unless conditions, and the other for node content and until
89
conditions. The resulting model will rely on enumerated clocks, clocked
90
expressions (expr when clock=clock_val) and merge of clocked expressions
91
(merge(e1, e2, ...) ).
92
 
93
* Comparison with other modeling choices
94

    
95
** Pouzet, Colaco [CP]
96

    
97
Our design is largely inspired by this publication. We made however a few
98
different design choices:
99

    
100
- in [CP] unless and until equations are gathered at the beginning of the node,
101
  similar to our unless definitions. We assume that their order should be
102
  preserved (unless before until) even if we don't have access to a specific
103
  implementation of such paper. 
104
  => This can be easily changed by accepting until transitions in state headers.
105

    
106
- the compilation scheme proposed by [CP] amounts to inline all definitions of
107
  states in the parent node. 
108
  - pro wrt us: all equations defining unless/until/state contents are available
109
    at the same 'level' without any encapsulating into node calls. Therefore no
110
    spurious algebraic loop is introduced. This authorizes the use of (pre mem)
111
    in unless conditions where mem is a stateful flow defined by the same
112
    automaton.
113
  - cons wrt us: because of inline and of the way the merge is clocked
114
    expression is performed, all variables in the tuple of flows defined by the
115
    automaton should share the same scheduling. In our design, since each state
116
    content is defined by a specific node, it can accept a different state-local
117
    scheduling of flows.
118
    Let us consider the following automaton:
119

    
120
    automaton foo
121
      state Case1:
122
      let
123
         a = 0 -> pre a;
124
         b = a + 1;
125
      tel
126
      state Case2:
127
      let
128
         b = 0 -> pre b;
129
         a = b + 1;
130
      tel
131

    
132
    This automaton defined the flows (a,b) but requires to compute a before b in
133
    Case1 and b before a in Case2. While this model is syntactically valid, it
134
    will be rejected by [CP] scheduling and accepted by our.
135

    
136
    On the contrary, let us consider the following automaton:
137

    
138
    TODO mettre un exemple avec un pre dans le unless et montrer qu'en inlinant
139
    ca marche.
140

    
141

    
142
** Scade automata [SQRC]
143

    
144
Scade automata are different:
145
- initial and final states
146
- signals (events emit)
147
- synchro transition that seems to rely on final states 
148

    
149
With only [SQRC], it is difficult to elaborate more:
150
- can we encode signals?
151
- what is the specific syntax of conditions? The examples cover if-then-else and
152
  emits. Is it allowed to define more?
153
- how do you read or react to signals?
154

    
155
In terms of syntax, 
156
- both unless and until are defined at the beginning of the state
157
- the automaton prototype explicitely declares the assigned flows
158

    
159
In terms of semantics:
160
- all assigned flows of the automaton should not need to be defined as in [CP]
161
  or our approach. By default an undefined flow preserves its value: x = pre x;
162
- without performing inlining as in [CP], it seems that Scade enables a
163
  different scheduling btw different states.
164

    
165

    
166
* References
167

    
168
[CP] Colaco, Pouzet and co
169
[SQRC] Scade Quick Reference Card
170

    
171
* Garbage
172

    
173
** Cex of pre in unless
174

    
175
    
176
    automaton bar
177
      state Run:
178
      unless true -> (pre a < 0) restart Error
179
      let
180
         a = input -> pre a + 1;
181
      tel
182
      state Error:
183
      let 
184
         a = -1;
185
      tel
186
    
187
    In this model, the intended semantics is the following, if the input is non
188
    negative, the state remains Run and the a flow is increased at each
189
    step. However if the previous state was negative than the automaton jumps to
190
    a Stop state and remains there.
191

    
192
    When compiled into Lustre v4 flows with clocked expressions, we have the
193
    following definitions:
194

    
195
    type bar__type = enum {Run, Error };
196
    
197
    node test (input: _a) returns (o: _b)
198
    var bar__next_restart_in: _c;
199
        bar__restart_in: _d;
200
        bar__restart_act: _e;
201
        bar__next_state_in: _f;
202
        bar__state_in: _g;
203
        bar__state_act: _h;
204
        a: _i;
205
   let
206
       o = a;
207
       bar__restart_act, bar__state_act = merge bar__state_in (Run -> bar__Run_unless (bar__restart_in when Run(bar__state_in),a when Run(bar__state_in)) every (bar__restart_in)) (Error -> bar__Error_unless (bar__restart_in when Error(bar__state_in)) every (bar__restart_in));
208
       bar__next_restart_in, bar__next_state_in, a = merge bar__state_act (Run -> bar__Run_handler_until (bar__restart_act when Run(bar__state_act),input when Run(bar__state_act)) every (bar__restart_act)) (Error -> bar__Error_handler_until (bar__restart_act when Error(bar__state_act)) every (bar__restart_act));
209
       bar__restart_in, bar__state_in = ((false,Run) -> pre (bar__next_restart_in,bar__next_state_in));  
210
   tel
211
 
212
   node bar__Run_unless (bar__restart_in: _j; a: _k) returns (bar__restart_act: _l; bar__state_act: _m)
213
   let
214
      bar__restart_act, bar__state_act = (if (true -> (pre a < 0)) then (true,Error) else (bar__restart_in,Run));
215
   tel
216
 
217
   node bar__Error_unless (bar__restart_in: _n) returns (bar__restart_act: _o; bar__state_act: _p)
218
   let    
219
     bar__restart_act, bar__state_act = (bar__restart_in,Error);   
220
   tel
221
 
222
   node bar__Run_handler_until (bar__restart_act: _q; input: _r) returns (bar__restart_in: _s; bar__state_in: _t; a_out: _u)
223
   var a: _v;
224
   let    
225
      a = (input -> (pre a + 1));
226
      a_out = a;
227
      bar__restart_in, bar__state_in = (false,Run);
228
   tel
229
 
230
   node bar__Error_handler_until (bar__restart_act: _w) returns (bar__restart_in: _x; bar__state_in: _y; a_out: _z)
231
   var a: _a1;
232
   let 
233
     a = (- (1));
234
     a_out = a;
235
     bar__restart_in, bar__state_in = (false,Error);
236
   tel
237

    
238
** Scade
239

    
240
According to [] the syntax is the following
241

    
242
automaton SM1 returns ...;
243
(initial | final | ) state Id
244
let
245

    
246
tel
247

    
248
They have a notion of initial and final states. In our case the initial one is
249
the first defined.