search

bmoth-mc / bmoth

Model Checker for (a subset of) classical B based on Z3
MIT License
9 stars 1 forks source link

&, or: wrong operator precedence #76

Closed x-moe-x closed 7 years ago

x-moe-x commented 7 years ago

Given two formulas

  1. TRUE or (FALSE & FALSE)
  2. TRUE or FALSE & FALSE

which should be obviously satisfiable, FormulaToZ3Translator::translatePredicate(...) builds the following:

  1. (or true (and false false))
  2. (and (or true false) false)

This evaluates to SAT for 1. and UNSAT for 2.

wysiib commented 7 years ago

Has to be fixed in the parser, the translation does not handle precedences

dohan commented 7 years ago

The assumption is wrong that the second formula is satisfiable. 'or' and '&' both have priority 40. Hence, TRUE or FALSE & FALSE is equivalent to (TRUE or FALSE) & FALSE which is obviously unsatisfiable.

x-moe-x commented 7 years ago

Wikipedia says it might have the same priority in some compilers. For convenience I suggest giving & a higher priority even if it's not striclty necessary.

dohan commented 7 years ago

Operator priorities differ in different formal languages. The B reference manual (page 187 and following) says that both operators have the same priority. In order to be compatible with other tools for the B language we can't change these priorities. I personally prefer the way TLA+ handles priorities by reporting a "Precedence conflict between operators" while evaluating the formula "TRUE or FALSE & FALSE".

wysiib commented 7 years ago

I think we could add a warning in this case as well?

dohan commented 7 years ago

Yes, we can add a warning as we have a concrete syntax tree as well.