`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. Next Slide

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.