Getting the prime/next state of a variable

Question

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?

Answer 1

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.

Answer 2

You may also use Atelier B to develop Event-B specifications. There are some variations with respect to Rodin, but the principles remain the same. For your issue, with Atelier B, you can specify an event as follows:

door_change = BEGIN
  door :( door : { Open, Closed } & 
    (PrimaryLock = On => doors = doors$0
  )
END

There, door and door$0 stand for the values before and after the event.

You can have such an event at the most abstract level of the specification. Then, you introduce a refinement with all the events of your system that may change the state of the door and have such events refine door_change.

This "trick" allows one to specify properties about variable changes in the system. I do not know if this feature is available in Rodin, though.