Module `LustreNode`

Internal representation of a Lustre node

Nodes are normalized for easy translation into a transition system, mainly by introducing new variables.

The node equations taken together become a map of state variables to expressions. All node calls are factored out with fresh state variables as inputs and outputs.

The node signature as input and output variables as well as its local variables is in inputs, outputs and locals, respectively. Local constants are propagated and do not need to be stored. The inputs of a node can be extended by constant state variables in oracles for the initial value of unguarded pre operations.

Assertions, properties to prove and contracts as assumptions and guarantees are lists of expressions in asserts, props, contracts fo into global_contracts and mode_contracts.

The flag node_is_main is set if the node has been annotated as main, it is not checked if more than one node or no node at all may have that annotation.

author: Christoph Sticksel

Types

type call_cond = | CActivate of StateVar.t | CRestart of StateVar.t: Call condition: activate or restart

type node_call = { call_pos : Lib.position; Position of node call in input file call_node_name : LustreIdent.t; Identifier of the called node call_cond : call_cond list; Boolean activation and/or restart conditions if any call_inputs : StateVar.t LustreIndex.t; Variables for actual input parameters The keys of the index match those in the t.inputs field of the called node. call_oracles : StateVar.t list; Variables providing non-deterministic inputs The length of the list is equal to the length of the list in the t.oracles field of the called node. call_outputs : StateVar.t LustreIndex.t; Variables capturing the outputs The keys of the index match those in the t.outputs field of the called node. call_defaults : LustreExpr.t LustreIndex.t option; Expressions for initial return values This value should be None for node calls on the base clock, and Some l for node calls with a clock. A node call with a clock may only have None here if it occurs directly under a merge operator. If the option value is not None, the keys of the index match those in the t.outputs field of the called node. }

A call to a node

Calls are uniquely identified by the position, no two calls may share the same position, therefore the call_pos must not be a dummy position.

type state_var_source = | Input Declared input variable | Output Declared output variable | Local Declared local variable | KLocal Kind 2 invisible local variable | Call Tied to a node call. | Ghost Declared ghost variable | Oracle Generated non-deterministic input | Alias of StateVar.t * state_var_source option Alias for another state variable.: Source of a state variable

type contract = LustreContract.t: A contract.

type equation_lhs = StateVar.t * LustreExpr.expr LustreExpr.bound_or_fixed list

Type of left hand side of equations.

An equation defines defines the state variable state_var, and a list bounds of indexes.

An array can be defined either only at a given index, or at all indexes, when the expression on the right-hand side is interpreted as a function of the running variable of the index.

type equation = equation_lhs * LustreExpr.t: An equation is a tuple (eqlhs, expr) that defines a possibly indexed state variable as an expression.

type t = { name : LustreIdent.t; Name of the node is_extern : bool; Is the node extern? instance : StateVar.t; Distinguished constant state variable uniquely identifying the node instance init_flag : StateVar.t; Distinguished state variable to be true in the first instant only inputs : StateVar.t LustreIndex.t; Input streams defined in the node The inputs are considered as a list with an integer indexes corresponding to their position in the formal parameters if there is more than one input parameter. If there is only one input parameter, the list index is omitted, the index is empty if there are no input parameters. oracles : StateVar.t list; Oracle inputs added to the node inputs Input streams added to the node to obtain non-deterministic values for the initial values of unguarded pre operators. The state variables are constant. outputs : StateVar.t LustreIndex.t; Output streams defined in the node The outputs are considered as a list with an integer indexes corresponding to their position in the formal parameters. locals : StateVar.t LustreIndex.t list; Local variables of node The order of the list is irrelevant, we are doing dependency analysis and cone of influence reduction later. equations : equation list; Equations for local and output variables calls : node_call list; Node calls inside the node asserts : (Lib.position * StateVar.t) list; Assertions of node props : (StateVar.t * string * Property.prop_source) list; Proof obligations for the node contract : contract option; Contract. is_main : bool; Flag node as the top node is_function : bool; Node is actually a function state_var_source_map : state_var_source StateVar.StateVarMap.t; Map from a state variable to its source Variables that were introduced to abstract expressions do not have a source. oracle_state_var_map : StateVar.t StateVar.StateVarHashtbl.t; Map from state variables to state variables providing a non-deterministic pre-initial value state_var_expr_map : LustreExpr.t StateVar.StateVarHashtbl.t; silent_contracts : string list; Contracts that were silently loaded. }

A Lustre node

Every state variable occurs exactly once in t.inputs, t.outputs, and t.oracles, and at most once on the left-hand side of t.calls. If the state variable is of array type, there may be more than one occurrence of it in t.equations, each defining the index variable at a different value with bound_or_fixed.Fixed. If the state variable is not an array, or all its bounds are bound_or_fixed.Bound, then it occurs at most once on the left-hand side of t.equations.

type state_var_instance = Lib.position * LustreIdent.t * StateVar.t: Instance of state vars as streams with their position

type contract_item_type = | Assumption | WeakAssumption | Guarantee | WeakGuarantee | Require | Ensure A definition of a state variable in the initial Lustre program. For a given state var s, it indicates the position p of an expression e that defines s as well as the corresponding index i, such that s defined by the value of e at index i.
type state_var_def = | CallOutput of Lib.position * LustreIndex.index | ProperEq of Lib.position * LustreIndex.index | GeneratedEq of Lib.position * LustreIndex.index | ContractItem of Lib.position * LustreContract.svar * contract_item_type | Assertion of Lib.position

val empty_node : LustreIdent.t -> bool -> t: Return a node of the given name and is extern flag without inputs, outputs, oracles, equations, etc. Create a state variable for the t.instance and t.init_flag fields, and set t.is_main to false.

Pretty-printers

val pp_print_node_equation : bool -> Stdlib.Format.formatter -> equation -> unit

Pretty-print a node equation in Lustre format

If the flag in the first argument is true, print identifiers in Lustre syntax.

val pp_print_call : bool -> Stdlib.Format.formatter -> node_call -> unit

Pretty-print a node call in Lustre format

If the flag in the first argument is true, print identifiers in Lustre syntax.

val pp_print_node : bool -> Stdlib.Format.formatter -> t -> unit

Pretty-print a node in Lustre format

If the flag in the first argument is true, print identifiers in Lustre syntax.

val pp_print_node_signature : Stdlib.Format.formatter -> t -> unit: Pretty-prints the signature of a node in Lustre format, WITHOUT NODE KEYWORD AND NAME. (Used in contract generation.)

val pp_print_node_debug : Stdlib.Format.formatter -> t -> unit: Pretty-print the node as a record with all information

Node Lists

val node_of_name : LustreIdent.t -> t list -> t: Return the node of the given name from a list of nodes

val exists_node_of_name : LustreIdent.t -> t list -> bool: Return true if a node of the given name exists in the a list of nodes

val find_main : t list -> LustreIdent.t: Return name of the first node annotated with --%MAIN. Raise Not_found if no node has a --%MAIN annotation or Failure "find_main" if more than one node has a --%MAIN annotation.

val ident_of_top : t list -> LustreIdent.t

Return the identifier of the top node

Fail with Invalid_argument "ident_of_top" if list of nodes is empty

val has_contract : t -> bool: Return true if the node has a global or at least one mode contract

val subsystem_of_nodes : t list -> t SubSystem.t: Return a tree-like subsystem hierarchy from a flat list of nodes, where the top node is at the head of the list.

val nodes_of_subsystem : t SubSystem.t -> t list: Return list of topologically ordered list of nodes from subsystem. The top node is the head of the list.

val stateful_vars_of_node : t -> StateVar.StateVarSet.t: Return all stateful variables from expressions in a node

val name_of_node : t -> LustreIdent.t: Return the name of the node

val ordered_equations_of_node : t -> StateVar.t list -> bool -> equation list: ordered_equations_of_node n stateful init Returns the equations of n, topologically sorted by their base (step) expression if init (not init).

val equation_of_svar : t -> StateVar.t -> equation option: Returns the equation for a state variable if any.

val source_of_svar : t -> StateVar.t -> state_var_source option: Returns the equation for a state variable if any.

val node_call_of_svar : t -> StateVar.t -> node_call option: Returns the node call the svar is (one of) the output(s) of, if any.

val scope_of_node : t -> Scope.t: Return the scope of the node

Iterators

val fold_node_calls_with_trans_sys : t list -> (t -> TransSys.t -> (TransSys.t * TransSys.instance * call_cond list) list -> 'a list -> 'a) -> t -> TransSys.t -> 'a

Fold bottom-up over node calls together with the transition system

fold_node_calls_with_trans_sys l f n t evaluates f m s i a for each node call in the node n, including n itself. The list of nodes l must at least contain all sub-nodes of n, and n itself, the transition system t must at least contain subsystem instances for all node calls. Both l and t may contain more nodes and subsystems, respectively, only the node calls in n are relevant.

The function f is evaluated with the node m, its transition system s, and the reverse sequence of instantiations i that reach the top system t. The last parameter a is the list of evaluations of f on the called nodes and subsystems of s. The sequence of instantiations i contains at its head a system that has s as a direct subsystem, together with the instance parameters. For the top system i is the empty list. Each element of i also contains the call activation conditions that effectively sample the node.

The systems are presented in topological order such that each system is presented to f after all its subsystem instances have been presented.

Sources

val pp_print_state_var_source : Stdlib.Format.formatter -> state_var_source -> unit: Pretty-print a source of a state variable

val set_state_var_source : t -> StateVar.t -> state_var_source -> t: Set source of state variable

val set_state_var_source_if_undef : t -> StateVar.t -> state_var_source -> t: Set source of state variable if not already defined.

val get_state_var_source : t -> StateVar.t -> state_var_source: Get source of state variable

val set_state_var_alias : t -> StateVar.t -> StateVar.t -> t: Sets the first svar as alias for the second svar.

val set_state_var_node_call : t -> StateVar.t -> t: Register state var as tied to a node call if not already registered.

val set_state_var_instance : StateVar.t -> Lib.position -> LustreIdent.t -> StateVar.t -> unit: State variable is identical to a state variable in a node instance

val set_oracle_state_var : t -> StateVar.t -> StateVar.t -> unit
val get_oracle_state_var_map : t -> StateVar.t StateVar.StateVarHashtbl.t
val set_state_var_expr : t -> StateVar.t -> LustreExpr.t -> unit
val get_state_var_expr_map : t -> LustreExpr.t StateVar.StateVarHashtbl.t
val get_all_state_vars : t -> StateVar.t list
val get_state_var_instances : StateVar.t -> state_var_instance list: get all instances of a state variable

val pp_print_state_var_instances_debug : Stdlib.Format.formatter -> t -> unit: print state var instances for debug

val get_state_var_defs : StateVar.t -> state_var_def list: Get the definitions (with positions in the Lustre program) of a state variable

val add_state_var_def : StateVar.t -> state_var_def -> unit: Add a definition (with positions in the Lustre program) for a state variable

val pos_of_state_var_def : state_var_def -> Lib.position
val index_of_state_var_def : state_var_def -> LustreIndex.index
val pp_print_state_var_defs_debug : Stdlib.Format.formatter -> t -> unit: print state var defs for debug

val state_var_is_visible : t -> StateVar.t -> bool

Return true if the state variable should be visible to the user, false if it was created internally

Return true if the source of the state variable is either Input, Output, or Local, and false otherwise.

val is_automaton_state_var : StateVar.t -> (string * string) option: Return the automaton to which the state variable belongs if any

val node_is_visible : t -> bool: Return true if the node should be visible to the user, false if it was created internally.

val node_is_state_handler : t -> string option: Return the state that is handled by the node if any.

val state_var_is_input : t -> StateVar.t -> bool: Return true if the state variable is an input

val state_var_is_output : t -> StateVar.t -> bool: Return true if the state variable is an output

val state_var_is_local : t -> StateVar.t -> bool: Return true if the state variable is a local variable

val map_svars_in_equation : (StateVar.t -> StateVar.t) -> equation -> equation: Replace state variables in equation

`call_pos : Lib.position;`	Position of node call in input file
`call_node_name : LustreIdent.t;`	Identifier of the called node
`call_cond : call_cond list;`	Boolean activation and/or restart conditions if any
`call_inputs : StateVar.t LustreIndex.t;`	Variables for actual input parameters The keys of the index match those in the `t.inputs` field of the called node.
`call_oracles : StateVar.t list;`	Variables providing non-deterministic inputs The length of the list is equal to the length of the list in the `t.oracles` field of the called node.
`call_outputs : StateVar.t LustreIndex.t;`	Variables capturing the outputs The keys of the index match those in the `t.outputs` field of the called node.
`call_defaults : LustreExpr.t LustreIndex.t option;`	Expressions for initial return values This value should be `None` for node calls on the base clock, and `Some l` for node calls with a clock. A node call with a clock may only have `None` here if it occurs directly under a `merge` operator. If the option value is not `None`, the keys of the index match those in the `t.outputs` field of the called node.

`\|` `Input`	Declared input variable
`\|` `Output`	Declared output variable
`\|` `Local`	Declared local variable
`\|` `KLocal`	Kind 2 invisible local variable
`\|` `Call`	Tied to a node call.
`\|` `Ghost`	Declared ghost variable
`\|` `Oracle`	Generated non-deterministic input
`\|` `Alias of StateVar.t * state_var_source option`	Alias for another state variable.

`name : LustreIdent.t;`	Name of the node
`is_extern : bool;`	Is the node extern?
`instance : StateVar.t;`	Distinguished constant state variable uniquely identifying the node instance
`init_flag : StateVar.t;`	Distinguished state variable to be true in the first instant only
`inputs : StateVar.t LustreIndex.t;`	Input streams defined in the node The inputs are considered as a list with an integer indexes corresponding to their position in the formal parameters if there is more than one input parameter. If there is only one input parameter, the list index is omitted, the index is empty if there are no input parameters.
`oracles : StateVar.t list;`	Oracle inputs added to the node inputs Input streams added to the node to obtain non-deterministic values for the initial values of unguarded pre operators. The state variables are constant.
`outputs : StateVar.t LustreIndex.t;`	Output streams defined in the node The outputs are considered as a list with an integer indexes corresponding to their position in the formal parameters.
`locals : StateVar.t LustreIndex.t list;`	Local variables of node The order of the list is irrelevant, we are doing dependency analysis and cone of influence reduction later.
`equations : equation list;`	Equations for local and output variables
`calls : node_call list;`	Node calls inside the node
`asserts : (Lib.position * StateVar.t) list;`	Assertions of node
`props : (StateVar.t * string * Property.prop_source) list;`	Proof obligations for the node
`contract : contract option;`	Contract.
`is_main : bool;`	Flag node as the top node
`is_function : bool;`	Node is actually a function
`state_var_source_map : state_var_source StateVar.StateVarMap.t;`	Map from a state variable to its source Variables that were introduced to abstract expressions do not have a source.
`oracle_state_var_map : StateVar.t StateVar.StateVarHashtbl.t;`	Map from state variables to state variables providing a non-deterministic pre-initial value
`state_var_expr_map : LustreExpr.t StateVar.StateVarHashtbl.t;`
`silent_contracts : string list;`	Contracts that were silently loaded.

`\|` `Assumption`
`\|` `WeakAssumption`
`\|` `Guarantee`
`\|` `WeakGuarantee`
`\|` `Require`
`\|` `Ensure`	A definition of a state variable in the initial Lustre program. For a given state var s, it indicates the position p of an expression e that defines s as well as the corresponding index i, such that s defined by the value of e at index i.