The main function
LustreInput.of_file of this module returns a system for
the analysis strategies that can be turned into an internal
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
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:
Invalid_argumentis raised if the node given by
--lustre_mainis not found, there are two nodes with a
--%MAINannotation, or the input contains no nodes.
In particular, the output of the entry point
returns a Lustre file as a list of declarations of
type t = t',
const c = v, and
node X (...) returns (...); let ... tel.
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
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
-> 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.
LustreNode.t is a record representing a node with
inputsthe list of input variables
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
LustreTransSys turns the list of nodes into a
TransSys.t by means of the functions
Author(s): Christoph Sticksel
val of_file :
string -> LustreNode.t SubSystem.t * LustreGlobals.t
val ast_of_file :
string -> LustreAst.declaration list