Plant-Controller Systems
Modelling Event-B in Event-Eiffel

Two possibilities

1) Non-determinism as interleaved concurrency
(see first attempt). Basically a cyclic executive.

2) Each event (with state, guard and action) in its own thread, but with "low cost" synchronized state up date.

An event action (whether P on the plant side or C on the controller side) finishes with a small cost, synchronous socket communication in which the controller calculated plant input is transferred to the plant and the Current plant output (un-influenced by this input) is communicated to the controller. This still allows for feedback latency as plant events fire in arbitrarty order.

The socket communication can be decoupled by having a separate communication event, but then the additional mirror state created must also be modelled in the Event-B model resulting in additional complexity. This should only be done if the socket communication time is significant.

Advantages of (2) over (1)
+ Conceptually similar to the Event-B model. An event if enabled executes and if still enabled, executes again.

+ Probably more responsive (an event does not wait for the cyclic executive to cycle).

- More complex (threads + mutex) 
