Resettable Join

Specifications

Informal

A Resettable Join has three input terminals, a,b and r, and two output terminals, c and k.

Restricted to the terminals a, b and c it behaves just like a Join. However, in a state where only one of the inputs a or b has been sent, but not the other, the sent signal can be 'withdrawn' by sending a signal on r, that will reset the component and that will be acknowledged by output on k.

XDI

Specification in XDI model.

Verdect

Specification in Verdect:


define RJOIN( a?, b?, c!, r?, k! ) =
       pref *[ ((a? || b?); c!) | (((a? | b?) || r?) ; k!) ]
end
show(RJOIN)

Also available through this link

DI Algebra

Specification in DI Algebra:


NAME = "Resettable Join"
I = { a?, b?, r? }
O = { c!, k! }
RJOIN = [ a? -> [r? -> [k! -> RJOIN, b? -> CHAOS], 
		 b? -> [c! -> RJOIN, r? -> CHAOS]]
        , b? -> [r? -> [k! -> RJOIN, a? -> CHAOS],
		 a? -> [c! -> RJOIN, r? -> CHAOS]]
        ]

Also available through this link