preferences.texi 11 KB
Newer Older
point's avatar
point committed
1
@node User preferences
point's avatar
point committed
2
3
@appendix User preferences
@anchor{preferences}
point's avatar
point committed
4
5
6
7
8
9
10
@macro pref{p}
@t{\p\} :
@end macro

This appendix gathers user-definable preferences that modify the behavior of
parts of @arc{}. To modify or simply display the current value of preferences
use the @command{set} command (@xref{setcmd, ,@command{set}}).
point's avatar
point committed
11
12
13

@appendixsec Shell

point's avatar
point committed
14
15
This section lists preferences related to the command-line of @arc{}. Each 
preference identifier as to be prefixed with the @t{arc.shell.} string.
point's avatar
point committed
16

point's avatar
point committed
17
18
@table @pref
@item check-card-abort
point's avatar
point committed
19
@anchor{arc.shell.check-card-abort}
point's avatar
point committed
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
Abort the program if the check-card command fails.

Possible values: Booleans

Default value: @code{false}

@item history_file
The name of the file use to save the history of commands used during the last 
@arc{} session.

Possible values: Any valid file name

Default value: ~/.arc_history

@item preprocessor
point's avatar
point committed
35
@anchor{arc.shell.preprocessor}
36
@arc{} permits to preprocess @altarica{}, @mecv{} or @acheck{} files. One can assosiate to filename extensions (except @code{.arc}, @code{.lus} and @code{.rel}) a program used as a preprocessor. To specify that files terminating with the extension @code{.ext} must be preprocessed using a specific program, set the preference @code{arc.shell.preprocessor.ext.command} to the a string that contains the name of the executable (that must accessible via the @code{PATH} environment variable). A @code{%s} in the specified string indicates the position of the file to process. If no @code{%s} is found then the filename is just concatenated with the specified command and a separating white space.
point's avatar
point committed
37

38
Additional arguments can be appended to the command using the preferences @code{arc.shell.preprocessor.ext.args}. Such additional arguments are added each time the preprocessor is called.
point's avatar
point committed
39

40
41
42
43
44
If ARC can not associate a preprocessor to an extension it looks for preferences for @code{arc.shell.preprocessor.default.command} and @code{arc.shell.preprocessor.default.args}. If these latters are not set the file is parsed as-is.

Note that the parser handles @code{#line} indications generated by certain preprocessors.

Examples: With the following setting, any file @code{F} with the extension @code{.php} are preprocessed with the command @code{php F 5}.
point's avatar
point committed
45
@smallexample
46
47
 set arc.shell.preprocessor.php.command "php"
 set arc.shell.preprocessor.php.args "5"
point's avatar
point committed
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
@end smallexample

Possible values: String

Default value: none

@item prompt.0
The level 0 prompt.

Possible values: Any character string without newline

Default value: arc>

@item prompt.1
The level 1 prompt.

Possible values: Any character string without newline

Default value: .

@item verbose
Enable/disable (verbose) informative messages emitted by the ARC shell.

Possible values: Booleans

Default value: @code{true}
@end table

@appendixsec Acheck
This section list preferences related to @acheck{} specifications.

@table @pref
@item acheck.cleanup-semantics
Enable/disable the deletion of semantics after computation.

Possible values: Booleans

Default value: @code{false}

@item acheck.timers
Enable/disable timers for acheck computations.

Possible values: Booleans

Default value: @code{false}
@end table

@appendixsec Mec V
This section list preferences related to @mecv{} specifications.
@table @pref
@item mec5.timers
Enable/disable timers for @mecv{} computations.

Possible values: Booleans

Default value: @code{false}
@end table

point's avatar
point committed
106
107
108

@appendixsec Translation of @altarica{} models into @lustre{} programs
@anchor{a2lprefs}
point's avatar
point committed
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
Here are preferences related to the @command{to-lustre} command. Each preference
identifier as to be prefixed with the @t{translators.a2l.} string.

@table @pref
@item deterministic
In @altarica{} nodes an event can be used for several (macro-)transitions; this 
feature permits to create non-deterministic behaviors. Since non-determinism is
not suitable in the context of Lustre, this preference (if true) can be use to 
enforce (with an assertion) that only one of the possible (macro-)transitions 
is authorized.

Possible values: Booleans

Default value: @code{true}

@item enum-prefix
@altarica{} permits the use of symbolic values (like 'enum's in C). Each such 
value is translated into Lustre as a global integer constant. In order to 
prevent identifier conflicts a prefix  (defined by this preference) is added to
each symbolic value.

Possible values: Identifier

Default value: ENUM_

@item event-var-suffix
Prefix added to each identifiers of events.

Possible values: Identifier

Default value: _

@item flow-var-prefix
Prefix added to each identifiers of flow variables.

Possible values: Identifier
Default value: f_

@item guard-var-prefix
Prefix of local variables used to store the current variable of guards.

Possible values: Identifier

Default value: ec_

@item missing-init-prefix
If a state variable is not initialized then a dummy parameter is added to the 
@lustre{} node. This dummy parameter is used to initialize the state variable.
The name of the dummy parameter is the concatenation of this setting and the 
name of the state variable.

Possible values: Identifier

Default value: INIT_VAL_

@item noinput-name
If an @altarica{} node does not use any variable with an 'in' attribute then a 
dummy variable is created. The identifier of this variable is defined by this 
preference.

Possible values: Identifier

Default value: noinput

@item noreturn-name
If an @altarica{} node does not use any variable with an 'out' attribute then 
a dummy variable is created. The identifier of this variable is defined by this
preference.

Possible values: Identifier

Default value: noreturn

@item parameter-prefix
Prefix added to each identifiers of parameters.

Possible values: Identifier

Default value: p_

@item show-sections
Enable/disable comments identifying parts of the produced code.

Possible values: Booleans

Default value: @code{true}

@item signature-arg-prefix
Prefix of arguments of external functions

Possible values: Identifier

Default value: _arg_

@item signature-ret-suffix
Suffix of the return value for external functions

Possible values: Identifier

Default value: _return

@item state-var-prefix
Prefix added to each identifiers of state variables.

Possible values: Identifier

Default value: s_

@item verbose
Enable/disable the display of timers for acheck computations

Possible values: Booleans
point's avatar
point committed
221

point's avatar
point committed
222
223
224
225
226
227
228
229
230
Default value: @code{true}

@item warning
Enable/Disable the display of warnig messages.

Possible values: Booleans

Default value: @code{true}
@end table
point's avatar
point committed
231
232

@appendixsec Translation of @lustre{} programs into @altarica{} models
point's avatar
point committed
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
This section lists preferences related to the translator of @lustre{} programs
into @altarica. Each preference identifier as to be prefixed with the 
@t{translators.l2.} string.

@table @pref
@item clock-event-name
All translated nodes used one event (in addition to epsilon -- @math{@epsilon}).
This event is used at the top-level to synchronize all nodes together.

Possible values: Identifier

Default value: clock

@item initial-state-name
If a @lustre{} node is not purely functional i.e. it uses @code{pre} like 
operators, then the translator uses a new state variable to encode the fact 
that the node is initialized or not. The initial state is used to initialized
the actual state variables of the @lustre{} node.

Possible values: Identifier

Default value: _is_init

@item integers.as-range
If this preference is set to true then each occurrence of the @code{int} type 
in the @lustre{} code is replaced by a range of integers in the @altarica{} 
model. The bounds of the range are defined with the 
@code{translator.l2a.integers.min} and @code{translator.l2a.integers.max}
preferences.

Possible values: Booleans

Default value: @code{false}

@item integers.max
If @code{translator.l2a.integers.as-range} is true then the value specified by 
this preference is used as the upper bound of the range used in replacement of 
the @code{int} type.

Possible values: Integer

Default value: 10

@item integers.min
If @code{translator.l2a.integers.as-range} is true then the value specified by 
this preference is used as the lower bound of the range used in replacement of 
the @code{int} type.

Possible values: Integer

Default value: -10

@item pre-var-prefix
The use of the 'pre' operator in the Lustre code induces the creation of state 
variables in the @altarica{} node. This preference defines the common prefix 
for all such variables.

Possible values: Identifier

Default value: pre_

@item reals.add
Identifier of the signature of the addition between @code{real}s.

Possible values: Identifier

Default value: real_add

@item reals.div
Identifier of the signature of the division between @code{real}s.

Possible values: Identifier

Default value: real_div

@item reals.geq
Identifier of the signature of the @math{@geq} relation over 'real's.

Possible values: Identifier

Default value: real_geq

@item reals.gt
Identifier of the signature of the @math{>} relation over @code{real}s.

Possible values: Identifier

Default value: real_gt

@item reals.leq
Identifier of the signature of the @math{@leq} relation over @code{real}s.

Possible values: Identifier

Default value: real_leq

@item reals.lt
Identifier of the signature of the @math{<} relation over @code{real}s.

Possible values: Identifier

Default value: real_lt

@item reals.mod
Identifier of the signature of the modulo between @code{real}s.

Possible values: Identifier

Default value: real_mod

@item reals.mul
Identifier of the signature of the multiplication between @code{real}s.

Possible values: Identifier

Default value: real_mul

@item reals.neg
Identifier of the signature of the opposite of a @code{real} number.

Possible values: Identifier

Default value: real_neg

@item reals.sub
Identifier of the signature of the substraction between @code{real}s.

Possible values: Identifier

Default value: real_sub

@item reals.typename
Identifier of the abstract type used in place of @code{real}.

Possible values: Identifier

Default value: REALS

@item reals.zero
Identifier of the abstract constant of type 'real' encoding zero.

Possible values: Identifier

Default value: real_zero

@item struct_field_prefix
Composite types of Lustre are replaced by structures in @altarica{}. This 
preference is used to name fields of such structures.

Possible values: Identifier

Default value: _field_

@item subnodes-prefix
Each node call in the Lustre code implies the creation of a sub-node in the 
@altarica{} node of the caller. Each sub-node is identified with a name of the 
form @emph{pref@ind{i}} where @emph{pref} is the prefix specified by this 
setting and @emph{i} is an integer.

Possible values: Identifier

Default value: sc_

@item tmp_flow_var_prefix
The translator may create auxiliary variables in the AltaRica (e.g. to store 
sub-expression values. This preference sets the prefix of such variables.

Possible values: Identifier

Default value: _f_tmp_

@item verbose
Enable/disable the display of informatives messages during the translation.

Possible values: Booleans

Default value: @code{true}

@item warning
Enable/disable the display of warning messages.

Possible values: Booleans
point's avatar
point committed
415

point's avatar
point committed
416
417
Default value: @code{true}
@end table