Module LustreAstNormalizer

Normalize a Lustre AST to ease in translation to a transition system

The two main requirements of this normalization are to: 1. Guard any unguarded pre expressions 2. Generate any needed local identifiers or oracles

Identifiers are constructed with a numeral prefix followed by a type suffix. e.g. 2_glocal or 6_oracle. These are not valid lustre identifiers and are expected to be transformed into indexes with the numeral as a branch and the suffix type as the leaf.

Generated locals/oracles are referenced inside the AST via an Ident expression but the actual definition is not added to the AST. Instead it is recoreded in the generated_identifiers record.

pre operators are explicitly guarded in the AST by an oracle variable if they were originally unguarded e.g. pre expr => oracle -> pre expr

The following parts of the AST are abstracted by locals:

1. Arguments to node calls that are not identifiers e.g. Node expr1 expr2 ... exprn => Node l1 l2 ... ln where each li is a local variable and li = expri

2. Arguments to the pre operator that are not identifiers e.g. pre expr => pre l where l = expr

3. Node calls e.g. x1, ..., xn = ... op node_call(a, b, c) op ... => x1, ..., xn = ... op (l1, ..., ln) op ... where (l1, ..., ln) is a group (list) expression and each li corresponds to an output of the node_call If node_call has only one output, it is instead just an ident expression (Note that there is no generated equality here, how the node call is referenced at the stage of a LustreNode is by the node_call record where the output holds the state variables produced by the node call)

4. Properties checked expression 5. Assertions checked expression 6. Condition of node calls (if it is not equivalent to true) 7. Restarts of node calls (if it is not a constant)

• author Andrew Marmaduke