64 ;;Quote: use synchronous languages for real-time, embedded, safety critical applications

64+;;Quote: designers of safety-critical systems must convince themselves, the customer, and certification authorities that the design and implementation are correct

66 ;;Quote: the parallel composition of guarded microsteps has confusing semantics and multiple interpretations; used by VHDL, Verilog, and others

66 ;;Quote: acyclic, embedded control systems do not have zero-delay loops; e.g., sample-driven, compute outputs on each clock tick

66 ;;Quote: fixpoint control treats each reaction as the unique fixpoint for 'state+input -> state+output'; e.g., Esterel; difficult to prove unique

66 ;;Quote: constrained control systems may allow blocked reactions or multiple, nondeterministic reactions; proving uniqueness is difficult; e.g., Signal and Sildex

66 ;;Quote: treat control variables as a flow of values, one per clock tick; system of equations or dataflow network; each variable defined exactly once

66+;;Quote: Lustre extends the usual operators to operate pointwise on flows of values

67 ;;Quote: for any flow x, pre(x) is the previous value; a- >x is initially a then x; e.g., count of rising edges

67 ;;Quote: a node in Lustre is a function of typed input flows; defined by a system of equations and local flows; exactly one definition for each output or local flow

67 ;;Quote: flows can follow slower clocks; e.g., 'x when c' is x's values when c is true; most flow operators use the same clock

67 ;;Quote: flow operators deactivated if an operand clock is false

67+;;Quote: Lustre controls program activation by clocks

67 ;;Quote: if activation condition is false, a flow node's value is either frozen or a default value; deactivation by clocks too restrictive

67 ;;Quote: Lustre scheduling by topological sort; disallows syntactically cyclic definitions

67+;;Quote: Scade requires a pre operator for feedback values; enables separate compilation; i.e., execution order within a node is independent of the node's caller

69 ;;Quote: Esterel's formal semantics is based on constructive causality

69+;;Quote: formal semantics enables compile-time optimization, analysis, and verification