[Rodin-b-sharp-user] Inverting a boolean variable

[Stephen B. <ste...@gm...>]

Hi,

I'm still very new to both Event-B and Rodin (and to some extent predicate
logic), and I have encountered an issue with inverting a boolean variable in
Rodin. The error I received was, "Syntax error: Unexpected sub-formula,
expected: a predicate but was: an expression".

What I hoped to achieve is shown below:

variable - b
invariant - b : BOOL
event action - b := not(b)

However, this does not work. I think this is because BOOL is merely the
'meaningless' set {TRUE,FALSE} that we then attach meaning to ourselves. I
have written an alternative action that should do what I need:

event action - b :: BOOL \ {b}

Is this an appropriate way to achieve what I want? Is there a better way?

Steve