mxn-Decision-Wait

Specifications

Informal

An mxn-Decision-Wait (m>0, n>0) has m+n input terminals a_i (0<=i<m) and b_j (0<=j<n), and mn output terminals c_i_j. It waits for a signal on one of the a inputs and a signal on one of the b inputs. The environment has to guarantee mutual exclusion on the a-inputs and also the b-inputs. Having received input signals on a_i (0 >=i > m) and b_j (0 >=j > n) it produces a signal on output terminal c_ij.

XDI

Schematic diagram for an mxn-Decision-Wait:

[Zoom|FIG]

Verdect

Parameterized definitions are not possible in VERDECT, but this sketch gives the general idea:

Specification in Verdect:

define JOINMXN( a0?,.., a(m-1)?, b0?, ..,b(n-1)?, c00!,.., c(m-1)(n-1)! ) =
       pref *[ (a0? || b0?); c00!
		..
             | (a(m-1)? || b(n-1)?); c(m-1)(n-1)!
             ]
end

Also available through this link

DI Algebra

The specification of the 3x2-Decision-Wait is as follows:

Specification in DI Algebra.

. (Not available for general m and n.)

Properties

XDI Report for the 3x2-Decision-Wait.

The mxn-Decision-Wait is very symmetric. The roles of subscripts can be interchanged, independently on both a and on b, and also the roles of a and b can be interchanged, provided that the c outputs are permuted accordingly.

The mxn-Decision-Wait satisfies Rules Y' and Z^out, but not Z^in (choice between a inputs, and also between b inputs).