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 statelocal 
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 ifthenelse 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. 