Given some condition, I want to check that a variables next state holds for some proposition. I have not been able to create something that rodin has accepted.
My exact case is the following invariant. I want to make sure that the variable door never changes when the lock is on. The variable door is either Open or Closed
inv4: PrimaryLock = On ⇒ door :∣ door' = door
If the PrimaryLock is On this means that the door state will not change, no matter what event is triggered next.
Is this possible using Event-b or do I need to solve my issue by adding additional variables?
Currently, the only place where you can specify properties about state changes is in events themselfes. Thus, you have to add the guard PrimaryLock /= On to each event that modifies the variable door.
If you work with refinement (you should! :), then this is actually not that bad because you specify the abstract events that might change the door and all the events in refinements must follow their specification.
open_door = WHEN PrimaryLock /= On THEN door := Open END
close_door = WHEN PrimaryLock /= On THEN door := Closed END
New events in refinements that do not refine open_door or close_door implicitly refine skip are not allowed to change the door status. So if open_door and close_door are the only events in the abstract specification that change the variable door, door can only be modified in refinements if it is not locked.
You could specify it even more abstract with
change_door_status = WHEN PrimaryLock /= On THEN door :: {Open,Closed} END
and specify the events that open or close it as refinements.
I admit that it would be a nice feature to express such properties for all events.