Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / doc / automata_spec.org @ 93119c3f

History | View | Annotate | Download (12 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
    node triangle (r :bool) returns (o: int );
139
    let
140
      automaton trivial
141
        state One:
142
        unless r or (pre o = 100) restart One
143
        let
144
           o = 0 -> 1 + pre o;
145
        tel
146
    tel
147

    
148
    Our produced v4 code with clocks is the following:
149

    
150
    type trivial__type = enum {One };
151
  
152
    node trivial__One_handler_until (trivial__restart_act: bool) returns (trivial__restart_in: bool; trivial__state_in: trivial__type; o_out: int)
153
    var __trivial__One_handler_until_2: int;
154
        __trivial__One_handler_until_1: bool;
155
        o: int;
156
    let
157
      trivial__restart_in, trivial__state_in = (false,One);
158
      o_out = o;
159
      o = (if __trivial__One_handler_until_1 then 0 else (1 + __trivial__One_handler_until_2));
160
      __trivial__One_handler_until_2 = pre o;
161
      __trivial__One_handler_until_1 = (true -> false);    
162
    tel
163

    
164
    node trivial__One_unless (trivial__restart_in: bool; r: bool; o: int) returns (trivial__restart_act: bool; trivial__state_act: trivial__type)
165
    var __trivial__One_unless_2: bool;
166
        __trivial__One_unless_1: int;
167
    let 
168
      trivial__restart_act, trivial__state_act = (if __trivial__One_unless_2 then (true,One) else (trivial__restart_in,One));
169
      __trivial__One_unless_2 = (r or (__trivial__One_unless_1 = 100));
170
      __trivial__One_unless_1 = pre o;
171
    tel
172
 
173
    node triangle (r: bool) returns (o: int)
174
    var trivial__state_in: trivial__type clock;
175
        trivial__state_act: trivial__type clock;
176
        __triangle_7: bool;
177
        __triangle_8: trivial__type;
178
        __triangle_6: bool;
179
        __triangle_3: bool when One(trivial__state_act);
180
        __triangle_4: trivial__type when One(trivial__state_act);
181
        __triangle_5: int when One(trivial__state_act);
182
        __triangle_1: bool when One(trivial__state_in);
183
        __triangle_2: trivial__type when One(trivial__state_in);
184
        trivial__next_restart_in: bool;
185
        trivial__restart_in: bool;
186
        trivial__restart_act: bool;
187
        trivial__next_state_in: trivial__type;
188
    let    
189
        trivial__restart_in, trivial__state_in = (if __triangle_6 then (false,One) else (__triangle_7,__triangle_8));
190
        __triangle_7, __triangle_8 = pre (trivial__next_restart_in,trivial__next_state_in);
191
        __triangle_6 = (true -> false);
192
        trivial__next_restart_in, trivial__next_state_in, o = merge trivial__state_act (One -> (__triangle_3,__triangle_4,__triangle_5));
193
        __triangle_3, __triangle_4, __triangle_5 = trivial__One_handler_until (trivial__restart_act when One(trivial__state_act)) every (trivial__restart_act);
194
        trivial__restart_act, trivial__state_act = merge trivial__state_in (One -> (__triangle_1,__triangle_2));
195
        __triangle_1, __triangle_2 = trivial__One_unless (trivial__restart_in when One(trivial__state_in),r when One(trivial__state_in),o when One(trivial__state_in)) every (trivial__restart_in);
196
    tel
197
 
198
    The use of a stateful trivial__One_unless function leads to a scheduling
199
    error, hence a possible algebraic loop: o, __triangle_1, trivial__state_act,
200
    __triangle_5, trivial__restart_act, node trivial__One_handler_until_50_2,
201
    __triangle_2, node trivial__One_unless_52_1.
202

    
203
    In practice, if one inlines (manually) the function trivial__One_unless, we
204
    obtain the following valid code (for our compiler):
205
    
206
    __triangle_1, __triangle_2 = (if (r or (pre o = 100)) then (true, One) else (trivial__restart_in, One)) when One(trivial__state_in);
207

    
208

    
209
** Scade automata [SQRC]
210

    
211
Scade automata are different:
212
- initial and final states
213
- signals (events emit)
214
- synchro transition that seems to rely on final states 
215

    
216
With only [SQRC], it is difficult to elaborate more:
217
- can we encode signals?
218
- what is the specific syntax of conditions? The examples cover if-then-else and
219
  emits. Is it allowed to define more?
220
- how do you read or react to signals?
221

    
222
In terms of syntax, 
223
- both unless and until are defined at the beginning of the state
224
- the automaton prototype explicitely declares the assigned flows
225

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

    
232

    
233
* References
234

    
235
[CP] Colaco, Pouzet and co
236
[SQRC] Scade Quick Reference Card
237

    
238
* Garbage
239

    
240
** Cex of pre in unless
241

    
242
    
243
    automaton bar
244
      state Run:
245
      unless true -> (pre a < 0) restart Error
246
      let
247
         a = input -> pre a + 1;
248
      tel
249
      state Error:
250
      let 
251
         a = -1;
252
      tel
253
    
254
    In this model, the intended semantics is the following, if the input is non
255
    negative, the state remains Run and the a flow is increased at each
256
    step. However if the previous state was negative than the automaton jumps to
257
    a Stop state and remains there.
258

    
259
    When compiled into Lustre v4 flows with clocked expressions, we have the
260
    following definitions:
261

    
262
    type bar__type = enum {Run, Error };
263
    
264
    node test (input: _a) returns (o: _b)
265
    var bar__next_restart_in: _c;
266
        bar__restart_in: _d;
267
        bar__restart_act: _e;
268
        bar__next_state_in: _f;
269
        bar__state_in: _g;
270
        bar__state_act: _h;
271
        a: _i;
272
   let
273
       o = a;
274
       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));
275
       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));
276
       bar__restart_in, bar__state_in = ((false,Run) -> pre (bar__next_restart_in,bar__next_state_in));  
277
   tel
278
 
279
   node bar__Run_unless (bar__restart_in: _j; a: _k) returns (bar__restart_act: _l; bar__state_act: _m)
280
   let
281
      bar__restart_act, bar__state_act = (if (true -> (pre a < 0)) then (true,Error) else (bar__restart_in,Run));
282
   tel
283
 
284
   node bar__Error_unless (bar__restart_in: _n) returns (bar__restart_act: _o; bar__state_act: _p)
285
   let    
286
     bar__restart_act, bar__state_act = (bar__restart_in,Error);   
287
   tel
288
 
289
   node bar__Run_handler_until (bar__restart_act: _q; input: _r) returns (bar__restart_in: _s; bar__state_in: _t; a_out: _u)
290
   var a: _v;
291
   let    
292
      a = (input -> (pre a + 1));
293
      a_out = a;
294
      bar__restart_in, bar__state_in = (false,Run);
295
   tel
296
 
297
   node bar__Error_handler_until (bar__restart_act: _w) returns (bar__restart_in: _x; bar__state_in: _y; a_out: _z)
298
   var a: _a1;
299
   let 
300
     a = (- (1));
301
     a_out = a;
302
     bar__restart_in, bar__state_in = (false,Error);
303
   tel
304

    
305
** Scade
306

    
307
According to [] the syntax is the following
308

    
309
automaton SM1 returns ...;
310
(initial | final | ) state Id
311
let
312

    
313
tel
314

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