Initialized Non-Receptive 1-Bit Variable

Specifications

Informal

An Initialized Non-Receptive 1-Bit Variable has three input terminals (w0, w1, r) and three output terminals (a, v0, v1). It stores one bit. The initial value of the bit is 0. Writing is done via the terminals w0 (write 0), w1 (write 1), and a (acknowledge), on which input and output alternate. Reading is done via the terminals r (read), v0 (value 0), and v1 (value 1), on which input and output alternate as well.

The environment of an Initialized Non-Receptive 1-Bit Variable must guarantee mutual exlusion of the signals on w0 and w1. In contrast to an Initialized 1-Bit Variable, the environment must also guarantee mutual exclusion between the write and read inputs.

XDI

Schematic diagram for an Initialized Non-Receptive 1-Bit Variable:

[Zoom|FIG]

XDI state graph for an Initialized Non-Receptive 1-Bit Variable:

[Zoom|FIG]

Specification in XDI model.

Verdect

Specification in Verdect:


define VAR( w0?, w1?, a!, r?, v0!, v1! ) =
    |[ x0, x1, y0, y1 ::
       pref *[ (w0?; x0 | w1?; x1); a!
             | r?; (y0; v0! | y1; v1!)
             ]
    || pref ( *[y0] ; *[ x0; *[y0] | x1; *[y1] ])
    ]|
end

Also available through this link

DI Algebra

Specification in DI Algebra:


NAME = (Initialized Non-receptive one bit variable)
I = { w0, w1, r }
O = { v0, v1, a }

V  = V0

V0  = [w0? -> V0W, w1? -> V1W , r? -> V0R]
V1  = [w0? -> V0W, w1? -> V1W , r? -> V1R]
V0W = [a! -> V0, r? -> CHAOS, w1? -> CHAOS]
V1W = [a! -> V1, r? -> CHAOS, w0? -> CHAOS]
V0R = [v0! -> V0, w0? -> CHAOS, w1? -> CHAOS]
V1R = [v1! -> V1, w0? -> CHAOS, w1? -> CHAOS]
.

Also available through this link