pietercollins
commented
1 year ago The main issue here is that (using non-complex arithmetic) sqrt(x) is an error for 'x<0'. This also includes cases where all we know is that x lies in bounds which which include strictly negative numbers.
We use the Positive modifier to indicate that numbers are positive, but don't apply this to functions. Allowing this for functions may help in some cases, but will also increase the number of classes needed, so I would like to avoid this.
By caching range information, we may be able to handle some cases.
An alternative would be to use a global sqrt function. Possibilities are sqrt(abs(x)), sqrt(max(0,x)) or sgn(x)*sqrt(abs(x)). But then for x<0 we lose the identity x=sqrt(x)*sqrt(x), which is undesirable.
It is often the case that we want to model the square root of strictly positive quantities in the dynamics and guards, for example the norm of a vector like sqrt(sqr(x)+sqr(y)) to represent distance. If the set is very close to zero, which is a region quite commonly reached during evolution, then the square root fails: namely, we get a DomainException in algebra/algebra_operations.tpl.hpp:234 .
While for predicates and algebraic equations we may be able to remove the sqrt operation, this is not the case for differential equations, so this should be handled (possibly only for specific expressions?). Otherwise, we need to work around the issue by changing the model, thus failing to be accurate in respect to the original system.