Module LustreInput

Parse Lustre input into the intermediate Lustre format

An OCamllex lexer in LustreLexer and a Menhir parser in LustreParser take the input and produce a sinlge LustreAst.t value, which is a minimally processed representation of a Lustre AST.

This AST is then translated into a simplified Lustre, see LustreNode, and LustreDeclarations for the translation.

The main function of_file of this module returns a system for the analysis strategies that can be turned into an internal transition system TransSys by using functions in LustreTransSys with relevant parameters.

The whole input file is parsed and type checked first, then one node is designated as the main node. The returned Subsystem.t has this main node at the top, and all called nodes as children. Nodes that are in the input file, but not called by the main node are discarded. No further cone of influence reduction is peformed yet, this happens only in LustreTransSys when the parameters of the analysis are known.

The main node is chosen to be, in order of precedence:

An exception Invalid_argument is raised if the node given by --lustre_main is not found, there are two nodes with a --%MAIN annotation, or the input contains no nodes.

In particular, the output of the entry point LustreParser.main returns a Lustre file as a list of declarations of

A node is viewed as a tuple of an identifier, a list of inputs, a list of outputs, declarations of local constants and variables, and equations. An equation is either an assignment of an expression to a variable, an assertion, a property annotation, or flag to mark the node as the top node.

The function LustreSimplify.declarations_to_nodes is called with this list of declarations as input and produces a list of LustreNode.t that contains each node with expressions in a normalized form, with structured fields unfolded, constants propagated and type aliases substituted.

In detail, the process of normalizing an expression in a node abstracts every non-variable expression under a pre operator into a fresh local variable. All -> operators are lifted to the top of the expression so that an expression can be represented as a pair of expressions, one for the first instant and one for the following. Each variable at the previous state i the left argument to the -> operator in the resulting expression is replaced with a fresh oracle constant per variable that is added to the inputs of the node.

Node calls are factored out into assignments to fresh local variables, where input expressions are further abstracted to fresh local variables. A node call may be wrapped in a condact with an activation condition and default values.

In detail, LustreNode.t is a record representing a node with

After finding the designated main node with LustreNode.find_main, the definitions in the main node and list of nodes is reduced to the nodes in the cone of influence of the properties of the main node, see LustreNode.reduce_to_property_coi. Last, the equational definitions of each node are ordered by their dependencies with LustreNode.reduce_to_property_coi.

The module LustreTransSys turns the list of nodes into a transition system TransSys.t by means of the functions LustreTransSys.trans_sys_of_nodes and LustreTransSys.props_of_nodes.

author
Christoph Sticksel
val of_file : string -> LustreNode.t SubSystem.t * LustreGlobals.t * LustreAst.declaration list

Parse from the file, return an input system for further slicing and refinement from analysis strategies.

val ast_of_file : string -> LustreAst.declaration list

Parse from the file, returns the AST.