False negative on norm(x)

[mfry90]

False negative on norm(x)

[hbourbouh]

Thanks for opening this issue.
Non-linear and trigonometric functions are not supported by current solvers we use, therefore, an abstraction is needed.
For example, in the generated files you sent us, you can check the file "lustrec_math.lus" that contains many abstractions of non-linear functions. You can modify them with more precise one if you are familiar with the Lustre language and re-run Kind2 or CoCoSim.

Most of the time, Kind2 model checker will return a non-sensical counter-example for properties such yours that require precise abstractions of non-linear blocks. Solvers like Z3 are more suited for logic-intensive properties and do badly in numeric-intensive ones.

[mfry90]

Got it, thanks for the clarification.

[mfry90]

Does this same consideration persist for power functions (y = x^n), where x\in Reals and y\in Nats? I'm getting similar problems even when I remove the sqrt() function (i.e., replace the y=norm(x) with y=dotproduct(x,x)). I see that lustrec_math.lus has an abstraction for power functions where x AND n are Reals, but is that necessary when n is Natural?

I can attach example files if that's helpful.

[hbourbouh]

Are you able to use the Simulink Power block (Math Function block with pow parameter) with machine type integers as inputs?
I get the following Simulink error when I try to do that:

Cannot set data type of input and output ports of 'pow_PP/Math Function' to uint8. The data type must be double or single when configured to be a 'pow' operation.

Currently we only support pow(x,n) where both x and n are \in Reals.

[mfry90]

No, I'm not using the Simulink Power block, I've been feeding a single variable x = [x_1, x_2, ..., x_n] into both inputs of the DotProduct block, which might be interpreted as a summation of pow(x_i, 2). I'd like to post a MWE to demonstrate the issue I'm getting with verifying over DotProduct blocks, but I'm getting different errors from (what appears to be) unrelated sources. Will post those issues as well.