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.

module NI = NodeId
module LG = LustreGlobals

Types

type call_cond =
  1. | CActivate of StateVar.t
  2. | CRestart of StateVar.t

Call condition: activate or restart

type node_call = {
  1. call_id : int;
  2. call_pos : Lib.position;
    (*

    Position of node call in input file

    *)
  3. call_node_id : NI.t;
    (*

    Identifier of the called node

    *)
  4. call_cond : call_cond list;
    (*

    Boolean activation and/or restart conditions if any

    *)
  5. call_context : StateVar.t option;
    (*

    Boolean variable representing the condition of a function call if any

    *)
  6. 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.

    *)
  7. 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.

    *)
  8. 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.

    *)
  9. 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.

    *)
  10. call_inlined : bool;
    (*

    Whether this call was inlined or not

    *)
  11. call_rec_decrease_expr : string option;
    (*

    Source-level rendering of the decrease constraint generated for a recursive call (e.g. "(n - 1 < n)"), used as the displayed expression of the corresponding decrease_check property. None for non-recursive calls or when the source expression could not be reconstructed.

    *)
  12. call_ties : (StateVar.t * StateVar.t option * HString.t) list;
    (*

    Tuples (tie, init_tie, x) where tie is a generated boolean local stating that the when-block variable x (whose off-branch holds its previous value) agrees with the output of this (activated) call, and init_tie, if any, is a generated boolean local stating that x has its initial value. LustreTransSys turns each tuple into candidate invariants expressing that tie holds once the activation clock has ticked, and that init_tie holds before the first tick.

    *)
}

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 gen_metadata =
  1. | Plain
    (*

    Generic generated variable, no extra metadata

    *)
  2. | Discriminant of HString.t
    (*

    Discriminant field for some ADT

    *)

Metadata attached to a Generated state variable source

type state_var_source =
  1. | Input
    (*

    Declared input variable

    *)
  2. | Output
    (*

    Declared output variable

    *)
  3. | Local
    (*

    Declared local variable

    *)
  4. | Call
    (*

    Tied to a node call.

    *)
  5. | Ghost
    (*

    Declared ghost variable

    *)
  6. | Generated of gen_metadata
    (*

    Kind 2 invisible generated variable

    *)
  7. | Oracle
    (*

    Generated non-deterministic input

    *)

Source of a state variable

type contract = LustreContract.t

A contract.

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 func_info = {
  1. uf_symbols : UfSymbol.t StateVar.StateVarMap.t;
  2. rec_info : (int * LustreExpr.expr list) option;
  3. is_lemma : bool;
}
type type_of_component =
  1. | Node
  2. | Function of func_info
type t = {
  1. node_id : NI.t;
    (*

    Name of the node

    *)
  2. is_extern : bool;
    (*

    Is the node extern?

    *)
  3. opacity : Opacity.t;
    (*

    Whether the node should be always abstracted by its contract, never, or sometimes

    *)
  4. instance : StateVar.t;
    (*

    Distinguished constant state variable uniquely identifying the node instance

    *)
  5. init_flag : StateVar.t;
    (*

    Distinguished state variable to be true in the first instant only

    *)
  6. 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.

    *)
  7. 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.

    *)
  8. 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.

    *)
  9. 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.

    *)
  10. equations : equation list;
    (*

    Equations for local and output variables

    *)
  11. calls : node_call list;
    (*

    Node calls inside the node

    *)
  12. asserts : (Lib.position * StateVar.t) list;
    (*

    Assertions of node

    *)
  13. props : (StateVar.t * string * Property.prop_source * Property.prop_kind * string) list;
    (*

    Proof obligations for the node

    *)
  14. contract : contract option;
    (*

    Contract.

    *)
  15. is_main : bool;
    (*

    Flag node as the top node

    *)
  16. comp_type : type_of_component;
  17. 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.

    *)
  18. oracle_state_var_map : StateVar.t StateVar.StateVarHashtbl.t;
    (*

    Map from state variables to state variables providing a non-deterministic pre-initial value

    *)
  19. state_var_expr_map : LustreExpr.t StateVar.StateVarHashtbl.t;
  20. assumption_svars : StateVar.StateVarSet.t;
  21. history_svars : (StateVar.t * StateVar.t) list Type.TypeMap.t;
}

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 LustreExpr.bound_or_fixed.Fixed. If the state variable is not an array, or all its bounds are LustreExpr.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 =
  1. | Assumption
  2. | WeakAssumption
  3. | Guarantee
  4. | WeakGuarantee
  5. | Require
  6. | 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 =
  1. | CallOutput of Lib.position * LustreIndex.index
  2. | ProperEq of Lib.position * LustreIndex.index
  3. | GeneratedEq of Lib.position * LustreIndex.index
  4. | FrameBlock of Lib.position
  5. | IfBlock of Lib.position
  6. | ContractItem of Lib.position * LustreContract.svar * contract_item_type
  7. | Assertion of Lib.position

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_input_name : LustreIdent.t -> t list -> t

Return the node of the given name from a list of nodes

val node_of_node_id : NI.t -> t list -> t
val node_of_scope : LustreIdent.t -> t list -> t
val exists_node_of_name : NI.t -> t list -> bool

Return true if a node of the given name exists in the a list of nodes

val get_main_annotated_nodes : t list -> NI.t list

Return all nodes with --%MAIN annotations

val find_main : t list -> NI.t list

Return name of all nodes annotated with --%MAIN. Raise Not_found if no node has a --%MAIN annotation. If the processing mode does not support multiple main nodes, then it is the caller's responsibility to ensure there is only a single main node.

val ident_of_top : t list -> NI.t

Return the identifier of the top node

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

val has_effective_contract : t -> bool

Return true if the node has a contract with at least one guarantee or one mode

val subsystems_of_nodes : NI.t list -> t list -> t SubSystem.t list

Return a list of tree-like subsystem hierarchies from a flat list of nodes, where the names of the top nodes are given as first argument.

val subsystem_of_nodes : NI.t -> t list -> t SubSystem.t

Return a tree-like subsystem hierarchy from a flat list of nodes, where the name of the top node is given as first argument.

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 : LG.state_var_bounds -> t -> StateVar.StateVarSet.t

Return all stateful variables from expressions in a node

val node_id_of_node : t -> NI.t

Return the name of the node

val is_function : t -> bool

Return whether the component is a function

val is_recursive : t -> bool

Return whether the component is a recursive function

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 partially_defined : t -> bool

Returns true if the node is partially defined, that is, there is an output without an equational definition

val source_of_svar : t -> StateVar.t -> state_var_source option

Returns the source of 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 node_call_svars : t -> StateVar.StateVarSet.t

Returns a set of state variables that are output of some node call

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

Every state variable is either defined in a node, or was introduced in pre-processing, see state_var_source.

val pp_print_state_var_source : Stdlib.Format.formatter -> state_var_source -> unit

Pretty-print a source of a state variable

val pp_print_state_var_def : Stdlib.Format.formatter -> state_var_def -> unit

Pretty-print a definition 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_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 * state_var_def list

Get the definitions (with positions in the Lustre program) of a state variable. In the return type, the first list contains state var defs where the state variable is explicitly mentioned. The second list contains state var defs that are dependencies (the node item does not explicitly reference the state variable, but the state variable depends on it)

val add_state_var_def : ?is_dep:bool -> StateVar.t -> state_var_def -> unit

Add a definition (with positions in the Lustre program) for a state variable. is_dep should be true iff the state_var_def is a dependency (where the state variable is not explicitly referenced by the definition, but somehow depends on it)

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 node_is_visible : t -> bool

Return true if the node should be visible to the user, false if it was created internally.

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