Miscellaneous features

7 Miscellaneous features

Here we describe some features of sf2lus which can be used to help debugging Stateflow charts. Most of these are more useful for debugging the translator itself, however.

7.1 Matlab revisions

-r13,-r14: Currently, only Matlab revisions r13 and r14 are supported. These are controlled by the -r13 and -r14 options (-r14 is the default).

7.2 Syntax control

Stateflow has a number of features which make it difficult to translate verbatim into Lustre without complex (and probably unreliable) compilation support. The following options have been implemented to help with compatibility:

-kw,-nkw: Add/remove a keyword to/from the list of keywords allowed as identifiers. Stateflow allows keywords to be used as identifiers which is difficult to handle with a lex/yacc-style parser. These options allow the use of some selected keywords to be included or excluded from the syntax. Use these with care, strictly-speaking you should eliminate keywords from the chart altogether.
-paths: Use full path names for states. This triggers the mechanism which allows full pathnames to be use in action code. This is not on by default, however, since it slows down the translator and pollutes the namespace since all variables have to be in long format, for example, the node reference ``A.B.C'' would probably become sA_B_C throughout the code. Note that local data is not supported yet.

This option is automatically set if more than one Stateflow chart is found in a model. This is to prevent name clashes between different Stateflow charts with identical state names. There is no check, as yet, for such states, in future this mechanism may only be triggered when such states exist.
-no_paths: Do not automatically set -paths. If you know that there are no state name conflicts between the Stateflow charts in a model then this allows processing of multiple-Stateflow charts without full path names.

7.3 Output formatting

These are some options to control the format of the output Lustre file. You can actually find some of these documented in the OCaml manual under the Format library.

-margin: Set the margin for formatted output.
-max_indent: Set the maximum indent for formatted output.
-text_limit: Limit output strings to this number of characters. This is not a Format library variable but is used to limit the amount of text copied into the Lustre file from Stateflow sources, for example when creating comments from state or transition labels.

7.4 Output language

Four output languages are currently supported, triggered by the following options:

-pollux

Generate Lustre V4 output. This is the default mode and the most fully supported.

-nbac

Generate Nbac output. Nbac is almost completely compatible with Lustre V4 via the lus2nbac utility supplied with the Lustre distribution. This option simply triggers emulation of the integer modulus function which seems to be missing from Nbac.

-reluc

Use Reluc modifications. Again, since the sf2lus translator uses only a small subset of Lustre the output is almost compatible with Reluc. Currently, this option triggers some additional parenthesization which seems to be needed. Currently, arrays and the event stack are not supported since Reluc does not have Lustre's static recursion mechanism.

-scade

Use SCADE modifications. There are some syntactic differences between SCADE and Lustre, some of which can be ironed out by a simple transformation on the output. These involve constructs such as:

(x,y) = if p then f(a,b) else (c,d);

which are not supported by SCADE. Again, there are no arrays or event stack.

7.5 Namespace management

Namespace management in the sf2lus translator is not fixed, for several reasons:

There is the tension between providing human-readable Lustre output without making the code too verbose.
Different users may have different preferences as to what is readable, depending upon their intended usage of the resulting code.
It is difficult to translate namespaces accurately between two such widely differing languages as Stateflow and Lustre. It is simple to convert names from one syntax space to another but doing so while retaining the flavour of the original language is difficult.
It is possible that different translations may have to coexist in the same context which will inevitably result in namespace collisions. This is exacerbated by the fact that Lustre V4 has no concept of modularity.

For these reasons, sf2lus supports several options controlling the way the output namespace is generated:

-names

Use state names in variables. So, for example, a state called A generates a variable sA (or state_A).

-ids

Use state ids in variables. A state with id 3 will be referenced by s3 (state_3).

-names_ids

Use both names and state ids in variables. For example s3_A (state_3_A).

-long_names

Use unabrreviated names in the output. Currently, the complete list of abbreviations is:

_point		action	a	after	aft	at	at
before	bfr	call	ca	change	ch	condition	c
count	cnt	counter	cntr	counts	cnts	during	du
end	end	enter	ent	entry	en	error	err
event	ev	events	evs	every	evry	exit	ex
flag	flg	graph	g	history	h	in	in
increment	inc	init	ini	inners	ins	junction	j
link	l	okay	ok	out	o	pre	p
print	pr	property	prop	state	s	stateflow	sf
stub	st	subgraph	sg	term	trm	tmp	t
transition	tr	update	u	valid	v	verify	verif

-varprefix

Prefix all variables (for namespace conflict avoidance). Do not use this, it is present for debug purposes only.

-prefix,-suffix

Prefix/suffix all toplevel names. This is used, for instance, when one wishes to compare the output from two different translations. All the visible identifiers in the output code are prefixed by the given string, for example, ``-prefix A'' might give:

type Aevent = bool;
const Aset = true; Aclr = false;
node Asf_2(Set, Reset: Aevent) returns(sOff, sOn: bool);

7.6 General translator control

These options control the translation process at the most basic level. Some of these are discussed in the preceding sections. The effect of others is described in the associated papers.

-no_self_init

Top level graph does not provide initialization. Normally, the init and term flags are automatically set to:

init = true -> false;
term = false;

at the top level of the code. This option disables this behaviour but is only present for debugging the translator.

-ess

Event stack size. This sets the depth of the event stack, see Section 3 for usage information and caveats.

-sends

Enable sends to specific states. This option triggers some additional processing which allows Stateflow's send function to be implemented. Note that events become integers which may affect subsequent analysis and that currently this feature is only partially implemented. See Section 3.2.

-junc_states

Treat junctions as states. When this is set junctions are given a physical state (called j<ID> or junction_<ID>) and the chart can stay in a junction after a reaction. An additional output boolean (v or valid) is generated which is true if and only if the current state is not a junction. See Section 4.1.

-errstate

Add error processing to event broadcasts. This generates an extra output boolean variable (err or error) which is set to true if an event is broadcast at the lowest level of the event stack. This logic is switched off if the event stack size is zero. See Section 5.3.2.

-unroll

Unroll loops according to loop counters. Using the annotations in the Stateflow chart described in Section 4.2 transition networks involving loops are unfolded a fixed number of times resulting in a loop-free chart. The unrolling algorithm is currently very primitive and has complexity problems.

7.7 Data management

Handling Matlab's workspace is complicated by the fact that it is stored in a binary format which external tools cannot read. Hence, the translator has to make some assumptions about the workspace which it communicates via the .mws file. These options allow some additional control over workspace values:

-create_missing

Add missing data to data dictionary. If a chart contains a reference to a variable not in Stateflow's data dictionary then it can be automatically created. All such variables have to have the same scope and type, however.

-missing_scope

Scope for missing data (default: INPUT_DATA). Recognized values are:

r13/r14	`INPUT_EVENT`	`OUTPUT_EVENT`	`LOCAL_EVENT`
	`OUTPUT_DATA`	`INPUT_DATA`	`LOCAL_DATA`
	`TEMPORARY_DATA`	`CONSTANT_DATA`
r14	`FUNCTION_INPUT_DATA`	`FUNCTION_OUTPUT_DATA`	`PARAMETER_DATA`

-missing_datatype

Data type for missing data (default: double). Known values are (not all are supported):

`double`	`single`	`int8`	`int16`
`int32`	`uint8`	`uint16`	`uint32`
`boolean`	`fixpt`	`ml`

-no_constants

Omit workspace constants from output. This is used by ss2lus and prevents sf2lus from including constants defined in the Matlab workspace file from being included. The output is not legal Lustre since the constants are expected to be provided by s2l.

7.8 Time

The Stateflow implicit time variable t is slightly problematical since Lustre does not have any notion of absolute time. For stand-alone Stateflow-generated Lustre code the following options allow t to be generated automatically assuming a fixed time difference between reactions. If time is not emulated here then it is assumed to be an input to the chart. The Matlab workspace file contains an entry indicating whether t is an input or not.

-emulate_time: Provide internal time value. References to Stateflow's time value are implemented internally in the Lustre code according to the following two options.
-start_time: Start time for emulated time (default: 0.0). The value of t at reaction zero.
-time_increment: Time increment for emulated time (default: 1.0). The t variable is incremented by this amount at the start of each reaction.

7.9 Observers

One of the main uses of the sf2lus translator is in the proof of safety properties. The following options support this activity:

-observe: Add observer node for given expression. Generate a single Lustre node observing the expression given as a string of Lustre code. State variables can be observed provided the -states_visible option is set.
-no_observers: Don't read observer file. By default, sf2lus looks for a file <file>.obs when given a model file <file>.mdl. If it exists it is assumed to be a file containing observable expressions, one per line. Lustre-style comments (--) are permitted.
-consistency: Add a state consistency observer. This option causes an observer for the state variables to be generated. The observer is called consistency_<CID> and is mostly used to verify the translation process, see Section 5.3.3. The -states_visible option is set automatically.
-counters: Add loop counters to junction networks. An additional integer output for each junction in the chart is generated. The counters are called cntrj<ID> where <ID> is the id number for the junction. Each counter is incremented when its junction is entered during transition path analysis. Currently, maximum values are not maintained so the values have to be checked after each reaction. In addition, an observer (called loop_counters_<CID>) is generated for all the junctions annotated as in Section 4.2. The -junc_states option is set automatically.

7.10 Debugging features

These are some miscellaneous options used to help in debugging the translator. Some may be of use in debugging Stateflow charts, however.

-trace: Add trace output. Generates a print function for each node generated. These are supported by external C functions in a file <file>_ext.c which print out the arguments and results of each node as it is processed. Some effort is made to defeat demand-driven computation which can elide operations which are pure side-effects.
-trace_inputs: Number of inputs to add to trace output. These seems to be a resource limit of the nummber of arguments which can be passed to C functions through Lustre's FFI. This sets the number of inputs to print for each function.
-trace_locals: Number of locals to add to trace output. The number of locals to print for each node during a trace.
-states_visible: Make state variables visible for toplevel graph. States are named as in Section 7.5.
-temps_visible: Make temporary variables visible for toplevel graph. Currently, this is not complete since there are problems with the event stack due to inter-level transitions.
-stubs_visible: Make stub nodes visible in output. When the event stack is implemented a skeleton node is generated at the start of translation as a pro forma event broadcast node. The output will not be legal Lustre if this option is set.
-locals_visible: Make chart locals outputs. Again, only works for a subset of local values.
-no_typecheck: Do not typecheck generated nodes. If the typechecker fails, this can either help debug the typechecker or generate partial output which can be hand-edited to give legal code.
-no_sequence: Do not sequence generated nodes. Another debugging feature, sequencing refers to the generation of intermediate flows to force the evaluation order of imperative actions in Lustre. Output will not be legal Lustre.
-no_normalize: Do not normalize generated nodes. Normalization refers to sequencing, typechecking and some other small transformations applied to the generated Lustre.
-input_bools_ints: Transform input booleans into integers. Used to allow Luciole to set more than one boolean input simultaneously, see Section 2.2.3.
-write_now: Write output as generated. Normally, the Lustre code is built up in memory and then dumped at the end of translation. This is a debug feature which allows inspection of partial code when the translator crashes.
-g,-gp,-v: Enable debug printouts. Enables debug printouts. Normally, these are disabled when the distribution is made.
-help,--help: Display the list of options.