The four phases of a handshake with a Mutual-Exclusion Element can be interpreted as request, grant, done, and acknowledge (of done) respectively. The grant outputs on the ports are mutually exclusive.
When a Mutual-Exclusion Element receives two requests, it will grant 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 requests are granted `infinitely often'.
Specification in Verdect:
define ME( r0?, a0!, r1?, a1! ) = |[ x0, y0, x1, y1 :: pref *[ r0?; x0; a0!; r0?; y0; a0! ] || pref *[ r1?; x1; a1!; r1?; y1; a1! ] || pref *[ x0; y0 | x1; y1 ] ]| endAlso available through this link
Specification in DI Algebra:
I = { r0, r1 } O = { a0, a1 } ME = [ r0? -> a0! ; r0? ; a0! ; ME , r1? -> a1! ; r1? ; a1! ; ME ]Also available through this link This is shown by this report. An alternative specification in DI Algebra uses alternations:
Specification in DI Algebra:
I = { r0, r1 } O = { a0, a1 } ME = [ r0? -> a0! ; r0? ; a0!; ME , r1? -> a1! ; r1? ; a1!; ME ] [{r0},{a0}] [{r1},{a1}]Also available through this link This comparison shows that this specification is correct.
The roles of the two ports can be interchanged:
ME(a, b) = ME(b, a)
A Mutual-Exclusion Element is not output deterministic, since there is an output choice in state 5. The output nondeterminism is dynamic.
No information available
No information available
No information available