Communicating Mealy Machines
Outputs depend on present state and present value of inputs.
Clocking provides element of state.
Outputs can change when inputs change, independent of clock, therefore model without refinement has zero delay.
An Issue: Two Mealy Machines put in a loop may create a non-deterministic system.
The Solution: It is argued that race conditions can be identified in a piece of (Java) software and a delay element such as a latch can be added.