Problem with extra parentheses in invariants

[nikos-kekatos]

Having checked the spacecraft rendevzous benchmark, we noticed that the invariants may have extra parentheses. In particular, an invariant in this paper is described by t<=125 & (y>=-100 & x+y>=-141.1 & x>=-100 & y-x<=141.1 & y<=100 & x+y<=141.1 & x<=100 & y-x>=-141.1).

This makes the parser to crash. The simple solution of always deleting the parentheses would not be sufficient as we could have guards of the form x==10x+(2+6).

It seems to me that there are two conditions when the parentheses should be deleted.

(1) There is & between the parenthesis. That means that the parentheses do not have any extra use (similar to the example described above). Note that the invariants are convex and described in DNF form (Disjunctive normal form meaning that they are only ANDs.

(2) No & symbol. For example, invariant t<=125 & (y>=-100) . In this case, the parentheses can be deleted as long as there is = symbol in between them. This condition covers all possible cases (==,<= or >=)

[schillic]

So you suggest to remove parentheses whenever there is a & or = in between. What about < and > as in (x < 10) & y < 2?

[mforets]

This makes the parser to crash. The simple solution of always deleting the parentheses would not be sufficient as we could have guards of the form x==10x+(2+6).

well, i guess you mean one like x == (1-x)*y

[mforets]

i think we should first split the string into the ampersands (either one, &, or two &&) and for the given list of subexpressions, remove the beginning and final characters ( and ) if they exist.

[schillic]

i think we should first split the string into the ampersands (either one, &, or two &&) and for the given list of subexpressions, remove the beginning and final characters ( and ) if they exist.

This does not work: x == y * (1-x) & y == 1 --> x == y * (1-x and y == 1

[nikos-kekatos]

@schillic you are right! Thanks for the comment! I completely disregarded this case (as it is typically not used). So, probably the second case should check if there is an '<', '>' or '='? What do you think?

[mforets]

i've pushed an update here. i'm not good with strings. maybe it can be improved. but the idea is that you want to remove beginning and last parentheses. the new doctests work now.

mind that my solution still doesn't work for nested parentheses, such as

parse_sxmath("(x >= y*(1-y) && ((y < 3) && (x > 5)))")

i haven't seen one of those in SX models, but it is of course semantically correct.