Module rustre_core::node_state

Persisted node state (temporal operators)

In Lustre, nodes may use different operators to use the language’s temporal features, namely pre, -> and fby. While function nodes behave mostly like traditional functions, actual nodes need to persist data from an invocation to the next in order to implement the above operators correctly.

This module defines queries to obtain the state that a given node requires, that is, a list of typed “slots” of memory that a Rustre runtime would need to allocate for each instance of the aforementioned node. Additionally, it provides a check_node_function_state query to emit diagnostics as to whether or not a given node is correctly defined as function or node, if it has, respectively no, or some state.

Stateful expressions

4 kinds of Lustre expression require persisted memory between node invocations.

• The pre unary operator: evaluates to the previous value it was applied to. It requires a (nullable) “slot” of the same type as its operand.
• The fby binary operator: evaluates to the value of its first operand the first cycle, and then to the previous value of its second operand for the remaining ones. It also requires a (nullable) slot with the same type as its operands.
• The -> binary operator evaluates to the value of its first operand the first cycle, and then to the value of its second operand for the remaining ones. It only requires a boolean value to be represented as it doesn’t persist any Lustre data; it must just know if it is in its first evaluation cycle.
• Node call sites: each call site corresponds to an instanciation of a node, with its own memory. They have to be recursively accounted for.

Functions

• check_node_function_state
  Query: Checks the coherence between the use of the function or node keyword and the presence or absence of temporal state
• is_node_stateful
  Query: Returns true if a node contains any stateful expressions (and is thus stateful itself)
• stateful_expr_of_node
  Query: Returns a list of stateful expressions in a node