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.
