1 2 3 4 5 6
------------------------ MODULE FIFO ------------------------- CONSTANT Message VARIABLES in, out Inner(q) == INSTANCE InnerFIFO Spec == \EE q : Inner(q)!Spec ==============================================================