search

bmoth-mc / bmoth

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

Parser does not support ~ (relational inverse) #72

Closed leuschel closed 7 years ago

leuschel commented 7 years ago

p = {3|->5, 3|->9, 6|->3, 9|->2} & q =p~

in REPL gives

Parse error: Unexpected input '~' in line 1 column 168. Additional information: mismatched input '~' expecting {, EQUIVALENCE, IMPLIES, '&', 'or'} Exception in thread "JavaFX Application Thread" Parse error: Unexpected input '~' in line 1 column 168.run

dohan commented 7 years ago

'~' is not yet supported by the Z3 translator

wysiib commented 7 years ago

should be supported now