Module NLNormalArgs

The normal_args predicate defines a normalization condition on node arguments -- those that are not on the base clock can only be instantiated with constants or variables -- that is necessary for correct generation of Obc/Clight. To see why this is necessary. Consider the NLustre equation: y = f(1, 3 when ck / x) with x on the clock ck, and y on the base clock. The generated Obc code is y := f(1, 3 / x) which has no semantics when ck = false, since x = None then 3 / x is not given a meaning. Consider what would happen were the semantics of 3 / x = None. There are two possible problems. If x is a local variable, then x = None in Obc implies that x = VUndef in Clight and 3 / VUndef has no semantics. I.e., the Obc program having a semantics would not be enough to guarantee that the Clight program generated from it does. If x is a state variable, then x = None in Obc implies that x could be anything in Clight (though it would be defined since state variables are stored in a global structure). We might then prove that x is never 0 (when ck = true) in the original Lustre program. This would guarantee the absence of division by zero in the generated Obc (since x is None when ck = false), but not in the generated Clight code; since None in Obc means "don't care" in Clight, x may well contain the value 0 when ck is false (for instance, if ck = false at the first reaction).