When using classes that are not linked to data, the expression usually needs to be bracketed in the generated Event-B. It would help to always add the brackets automatically.
Log in to post a comment.