Forked Join

Specifications

Informal

A Forked Join has two input terminals and two output terminals. It waits until input signals on both input terminals arrive, after which it produces signals on both output terminals. The environment may supply one new input after it has seen at least one output; it may supply two inputs once it has seen both outputs.

XDI

Schematic diagram for a Forked Join:

[Zoom|FIG]

XDI state graph for a Forked Join:

[Zoom|FIG]

Specification in XDI model.

Verdect

Specification in Verdect:


define FJOIN( a?, b?, c!, d! ) =
       pref *[ (a? || b) ; (c! || d!) ]
end

Also available through this link

DI Algebra

Specification in DI Algebra:


FJ = a?; b?; c!; d!; FJ

Also available through this link

Properties

XDI Report.

The roles of input a and b can be interchanged, as can the roles of outputs c and d:
FJ(a, b; c, d) =
FJ(a, b; d, c) =
FJ(b, a; c, d) =
FJ(b, a; d, c)

The Forked Join satisfies Rules Y' and Z^out, but not Zⁱⁿ because there is an input choice in states 4 and 5.

Implementations

DI Decompositions

A Forked Join can be implemented by a Join and a Fork:

[Zoom|FIG]

The Ludwig verification script of this implementation.

Using Boolean Gates

No information available

Using Transistors