When a Sequencer receives signals on b and both a_0 and a_1, it produces a signal on exactly one of the c_i-outputs (the other is delayed till the next b input arrives). The specification leaves the choice open. Often there is a fairness requirement on this choice: if a choice situation arises `infinitely often' then both outputs are chosen `infinitely often'.
Each pair of terminals (a_i, c_i) can be viewed as one passive 2-phase handshake port. A Sequencer `sequences' handshakes on its handshake ports in synchrony with signals on the b input. The b input is also referred to as next input.
Specification in Verdect:
define SEQ( a0?, a1?, b?, c0!, c1! ) = pref *[ a0?; c0! ] || pref *[ a1?; c1! ] || pref *[ b?; (c0! | c1!) ] endAlso available through this link
Specification in DI Algebra:
I = { a0, a1, b } O = { c0, c1 } S = b?; [ a0? -> c0!; S , a1? -> c1!; S ] .Also available through this link
The subscripts 0 and 1 can be interchanged systematically:
SEQ(a_0, a_1, b; c_0, c_1) =
SEQ(a_1, a_0, b; c_1, c_0)
A Sequencer is not output deterministic, since there is an output choice in state 7. The output nondeterminism is dynamic.
No information available
No information available