Mixer

Specifications

Informal

A (blocking) Mixer is a handshake component with three 2-phase handshake ports, two passive and one active. The handshakes on the passive ports are `multiplexed' over the active port. That is, whenever the environment requests on a passive port and the Mixer is not `busy', the Mixer requests on the active port (becoming `busy'), and when the active port receives an acknowledge, the passive port that received the original request is also acknowledged (becoming `idle').

In contrast to a Non-Receptive Mixer, the environment of a Mixer need not guarantee mutual exclusion of the passive requests. A request on a passive port while the Mixer is `busy' (processing a request on the other passive port) is not lost but is handled when the Mixer becomes `idle' again.

When a Mixer receives requests on both passive ports, it will process exactly one of them (and delay the other). The specification leaves the choice open. Often there is a fairness requirement on this choice: if a choice situation arises `infinitely often' then both outputs are chosen `infinitely often'.

XDI

Schematic diagram for a Mixer:

[Zoom|FIG]

XDI state graph for a Mixer:

[Zoom|FIG]

Specification in XDI model.

Verdect

Specification in Verdect:


define MIXER =
  |[ a0, a1, a, b0, b1 ::
     pref *[ ar?; a0; a1; aa! ]
  || pref *[ br?; b0; b1; ba! ]
  || pref *[ (a0 | b0); a ]
  || pref *[ a; cr!; ca?; (a1 | b1) ]
  ]|
end

Also available through this link

DI Algebra

Specification in DI Algebra:

NAME = "Mixer"
I = { r0, r1, a }
O = { a0, a1, r }

MX = [ r0? -> r!; M0 
     , r1? -> r!; M1
     ]
M0 = [ r1? -> M2
     , a?  -> a0!; MX
     ]
M1 = [ r0? -> M2
     , a?  -> a1!; MX
     ]
M2 = a?; [ a0! -> r!; M1, a1! -> r!; M0 ]
  
[{r0},{a0}]
[{r1},{a1}]
[{r},{a}]

Also available through this link