// ----------------------------------------------------------------------------
// ---------------------- Philips Audio Control Protocol ----------------------
// ----------------------------------------------------------------------------
//
// As described in D. Bosscher, I. Polak, and F. Vaandrager,
// "Verification of an Audio Control Protocol."  In H. Langmaack,
// W.-P. de Roever, and J. Vytopil, editors, FTRTFT '94: Formal
// Techniques in Real-time and Fault-tolerant Systems, Lecture Notes in
// Computer Science 863, pages 170-192.  Springer-Verlag, 1994.
//
// By the analysis presented in that paper, the protocol is correct
// for T < 1/17.
//

// Constants

#define Q 10		// One quarter  of the length of a bit slot
#define T 1/20		// Clock tolerance: +/- T

#define MT 2		// Empty input: No more bits
#define InTransit 4	// Max number of bits in transit in sender & receiver

// Macro to create a delay from the range [TICKS-TICKS*T,TICKS+TICKS*T].
// The exact delay is determined by the nondeterministic choice to exit
// on the interrupt process (tau,0).NEXT after TICKS-TICKS*T has elapsed.

#define IDLER (rec X.({}:X))
#define PAUSE(TICKS,NEXT) \
	scope(IDLER,dummy,(TICKS)-((TICKS)*T),NIL, \
		scope(IDLER,dummy,2*((TICKS)*T),NIL,NEXT,(tau,0).NEXT) \
					     ,NIL)

// If/then/else process: (if COND then IF_P else ELSE_P)

#define IFELSE(COND,IF_P,ELSE_P) \
  Choice1( \
          Choice[(IF_P) , {IFELSEindex,1,1,1,(COND)}] + \
          Choice[(ELSE_P) , {IFELSEindex,1,1,1,!(COND)}] \
         )

// ============================================================================
// Sender: receives data to send one bit at a time.  Bits are output with 
// proper timing using Manchester encoding.
//
// Inputs- bit[0], bit[1]: data
//         empty: end of input marker
// Outputs- UP, DOWN: rise and fall of data signal
//

Sender = (bit[0],1).wh_t[0,0] + (bit[1],1).wh_t[1,0] + {}:Sender;

// ----------------------------------------------------------------------------
//
// wh_t[BIT,TIME]: !wire_high && !transmitting with head(list)=BIT and x=TIME
// wh_T[BIT,TIME]: !wire_high && transmitting with head(list)=BIT and x=TIME
//
// (wire_high and transmitting variables are described in \ref{BPV94}.)

wh_t[0,0] = ('LeadingBitError,1).NIL;  // First bit cannot be zero
wh_t[1,0] = ('UP,1).WH_T_next;

wh_T[0,0] = PAUSE(2*Q,wh_T[0,2*Q]);
wh_T[0,2*Q] = ('UP,1).WH_T[0,2*Q];

wh_T[1,0] = PAUSE(4*Q,wh_T[1,4*Q]);
wh_T[1,2*Q] = PAUSE(2*Q,wh_T[1,4*Q]);
wh_T[1,4*Q] = ('UP,1).WH_T_next;

WH_T_next = (bit[0],1).WH_T[0,0]+(bit[1],1).WH_T[1,0]+(empty,1).WH_T[MT,0];

// ----------------------------------------------------------------------------
//
// WH_t[BIT,TIME]: wire_high && !transmitting with head(list)=BIT and x=TIME
// WH_T[BIT,TIME]: wire_high && transmitting with head(list)=BIT and x=TIME
//
// (wire_high and transmitting variables are described in \ref{BPV94}.)

WH_T[0,0] = PAUSE(4*Q,WH_T[0,4*Q]);
WH_T[0,2*Q] = PAUSE(2*Q,WH_T[0,4*Q]);
WH_T[0,4*Q] = ('DOWN,1).wh_T_next;

WH_T[1,0] = PAUSE(2*Q,WH_T[1,2*Q]);
WH_T[1,2*Q] = ('DOWN,1).wh_T[1,2*Q];

WH_T[MT,0] = PAUSE(2*Q,('DOWN,1).Sender);

wh_T_next = (bit[0],1).wh_T[0,0] + (bit[1],1).wh_T[1,0] + (empty,1).Sender;

// ============================================================================
// Receiver: Receives incoming data signal from Sender.  Recognizes only
// UP events; DOWN's are ignored.
//
// Inputs- UP: Rising edges on incoming data signal
// Outputs- Bit[0], Bit[1]: Decoded bit values
//          rready: Signal BitStream that sequence is complete (see below)
//

Receiver = (Receive || Finalize) \ {fBit,fOdd,fEven,fReset};

// ----------------------------------------------------------------------------
// Start receiving when you see an UP.  (First bit is always a 1.)

Receive = (UP,1).('fReset,1).('Bit[1],1).('fBit,1).recv[1,0] + {}:Receive;

// ----------------------------------------------------------------------------
//
// Process to keep track of whether number of bits received is odd or
// even.  If the total number of bits received is even then a final
// Bit[0] is added to the output in process recv[1,9*Q] (see below).
//

Finalize = FinalizeE + FinalizeO;	// Initial state is undefined
FinalizeE = (fBit,1).FinalizeO +	// FinalizeE is even state
	    ('fEven,1).FinalizeE +
	    (fReset,1).FinalizeE +
	    {}:FinalizeE;
FinalizeO = (fBit,1).FinalizeE +	// FinalizeO is odd state
	    ('fOdd,1).FinalizeO +
	    (fReset,1).FinalizeE +
	    {}:FinalizeO;

// Macro to tack an extra 0 bit onto sequences that end in zero or
// have even length.

#define FINALIZE(LASTBIT,NEXT) \
	IFELSE(((LASTBIT)==1),((fOdd,1).NEXT + \
			       (fEven,1).('Bit[0],1).('fBit,1).NEXT), \
			      (('Bit[0],1).('fBit,1).NEXT))

// ----------------------------------------------------------------------------
// 
// recv[BIT,TIME]: initial interval; head(list)=BIT and x=TIME
// recv'[BIT,TIME]: clock error portion of interval; head(list)=BIT and x=TIME
//
// The recv[*,*] processes represent the exact part of the interval--the
// minimum time that must pass given the maximum clock error of T.
// The recv'[*,*] processes represent the timer interval when the clock
// error is determined nondeterministically.

recv[0,0] = scope(IDLER,dummy,3*Q-(3*Q)*T,NIL,recv'[0,0],recvError);
recv'[0,0] = scope(IDLER,dummy,2*(3*Q)*T-1,NIL,recv[0,3*Q],
					      (tau,0).recv[0,3*Q] + recvError);
recv[0,3*Q] = scope(IDLER,dummy,2*Q-(2*Q)*T,NIL,recv'[0,3*Q],recvZero);
recv'[0,3*Q] = scope(IDLER,dummy,2*(2*Q)*T-1,NIL,recv[0,5*Q],
					      (tau,0).recv[0,5*Q] + recvZero);
recv[0,5*Q] = scope(IDLER,dummy,2*Q-(2*Q)*T,NIL,recv'[0,5*Q],recvZrOn);
recv'[0,5*Q] = scope(IDLER,dummy,2*(2*Q)*T-1,NIL,recv[0,7*Q],
	       (tau,0).recv[0,7*Q] + (tau,0).((tau,1).recv[0,7*Q] + recvZrOn));
recv[0,7*Q] = FINALIZE(0,recvDone);

recv[1,0] = scope(IDLER,dummy,3*Q-(3*Q)*T,NIL,recv'[1,0],recvError);
recv'[1,0] = scope(IDLER,dummy,2*(3*Q)*T-1,NIL,recv[1,3*Q],
					      (tau,0).recv[1,3*Q] + recvError);
recv[1,3*Q] = scope(IDLER,dummy,2*Q-(2*Q)*T,NIL,recv'[1,3*Q],recvOne);
recv'[1,3*Q] = scope(IDLER,dummy,2*(2*Q)*T-1,NIL,recv[1,5*Q],
					      (tau,0).recv[1,5*Q] + recvOne);
recv[1,5*Q] = scope(IDLER,dummy,2*Q-(2*Q)*T,NIL,recv'[1,5*Q],recvZero);
recv'[1,5*Q] = scope(IDLER,dummy,2*(2*Q)*T-1,NIL,recv[1,7*Q],
					      (tau,0).recv[1,7*Q] + recvZero);
recv[1,7*Q] = scope(IDLER,dummy,2*Q-(2*Q)*T,NIL,recv'[1,7*Q],recvZrOn);
recv'[1,7*Q] = scope(IDLER,dummy,2*(2*Q)*T-1,NIL,recv[1,9*Q],
	       (tau,0).recv[1,9*Q] + (tau,0).((tau,1).recv[1,9*Q] + recvZrOn));
recv[1,9*Q] = FINALIZE(1,recvDone);

recvError = (UP,1).('ReceiveError,1).NIL;		// Received UP too soon
recvZero = (UP,1).('Bit[0],1).('fBit,1).recv[0,0];	// Got a 0
recvOne = (UP,1).('Bit[1],1).('fBit,1).recv[1,0];	// Got a 1
recvZrOn = (UP,1).('Bit[0],1).('fBit,1).		// Got 01
		  ('Bit[1],1).('fBit,1).recv[1,0];
recvDone = ('rready,1).Receive;				// Finished this seq.

// ============================================================================
//
// Implementation: A sink process to absorb the DOWN events that nobody
// is observing in parallel with the Sender and Receiver processes.  The
// UP event is restricted to force synchronization within Impl.

Sink = {}:Sink + (DOWN,1).Sink;
Impl = ((Sender || Sink) \ {DOWN} || Receiver) \ {UP};

// ============================================================================
//
// BitGen and BitTest: Processes to generate bit sequences and check 
// the correctness of the output.
//

// BitGen: Generate sequences of bits that (1) start with 1; and (2) either
// have odd length or end in <00>.
//
// Inputs- tready: BitTest's signal that it is ready for the next sequence
// Outputs- bit[0],bit[1],empty: Data for Sender
//          tbit[0],tbit[1],tempty: Copy of data for BitTest

BitGen = {}:BitGen + (tau,0).('bit[1],1).('tbit[1],1).BG[1,MT,1];

// BG: residue is (# of bits sent)%2; old2 and old1 are the last two bits sent

BG[residue,old2,old1] = 
	(tau,0).(rec X.(('bit[0],1).('tbit[0],1).BG[1-residue,old1,0] +
		        ('bit[1],1).('tbit[1],1).BG[1-residue,old1,1] +
		        {}:BG[residue,old2,old1])) +
	(tau,0).BGfinis[residue,old2,old1]
{residue,0,1},{old2,0,2},{old1,0,2};

// BGfinis: finish off the sequence; make sure it has odd length or ends in 00

BGfinis[1,old2,old1] = BitGenDone {old2,0,2},{old1,0,2};
BGfinis[0,0,0] = BitGenDone;
BGfinis[0,old2,old1] = 
		('bit[0],1).('tbit[0],1).BGfinis[1,old1,0] + 
		{}:BGfinis[0,old2,old1]
{old2,0,2},{old1,0,2,1,((old1+old2)!=0)};

// Signal BitTest that we've sent all the bits and wait to be told (by
// BitTest) when Receiver has finished its work.

BitGenDone = ('empty,1).('tempty,1).BitGenDone' + {}:BitGenDone;
BitGenDone' = {}:BitGenDone' + (tready,1).BitGen;

// ----------------------------------------------------------------------------
//
// BitTest: Keep track of the bits sent by BitGen and check that they are
// output in the correct order by Receiver.  BT[*] receives copies of the
// input and checks them against outputs.  If tempty is received then
// BT[*] switches to BT'[*] which accepts no more input but waits for
// the outputs to complete.
//
// Inputs- tbit[0],tbit[1],tempty: Copy of data being sent to Sender
//         rready: Receiver's signal that it is ready for next sequence
// Outputs- tready: Signal BitGen that it's time to make more bits
//
// Bits are queued as a base-3 integer used as the index to the BT and
// BT' processes.  Base-3 is used so that bits can be represented as
// 1 (for 0) and 2 (for 1).  This eliminates the problem of figuring out
// whether index 0 represents an empty queue or a queue full of zero bits.
//
// LeadingDigit(Q,b) is a VERSA built-in that returns the highest order
// non-zero digit of Q interpreted as a base b number.
// TrailingDigits(Q,b) is a VERSA built-in that returns Q after its
// LeadingDigit has been removed.
//

#define HEAD(Q) (LeadingDigit((Q),3)-1) /* Return head of queue */
#define TAIL(Q) (TrailingDigits((Q),3)) /* Return queue with head popped */
#define PUSH(Q,D) ((Q)*3+((D)+1))	/* Add a value at the queue's tail */

BitTest = {}:BitTest + (tbit[0],1).BT[1] + (tbit[1],1).BT[2];

BT[0] = 	// empty queue
	{}:BT[0] +						// Idle
	(tempty,1).BT'[0] +					// Input done
	(tbit[0],1).BT[PUSH(0,0)] + (tbit[1],1).BT[PUSH(0,1)];	// Push a bit
BT[Qval] = 	// Queue is not empty; more input still possible
	{}:BT[Qval] +
	(tempty,1).BT'[Qval] +
	(tbit[0],1).BT[PUSH(Qval,0)] + (tbit[1],1).BT[PUSH(Qval,1)] +
	(Bit[HEAD(Qval)],10).BT[TAIL(Qval)]			// Pop a bit
{Qval,1,3**InTransit-1};

BT'[Qval] = 	// Queue is draining; no more input allowed
	{}:BT'[Qval] +
	(Bit[HEAD(Qval)],10).BT'[TAIL(Qval)]
{Qval,1,3**InTransit-1};
BT'[0] =	// Queue is empty, input is done; output must complete
	(rready,1).('tready,1).BitTest + {}:BT'[0];

BitStream = (BitGen || BitTest) \ {tbit[0],tbit[1],tempty,tready};

// ============================================================================
//
// Test of the audio control protocol implementation.
//
// Impl is correct if Test is deadlock-free.  A deadlock indicates that
// (1) an explicit error was encountered that forced a NIL process term; or
// (2) an error in the length or content of output occurred and BitTest
// was not able to receive a Bit[0]/Bit[1] or the rready event when 
// Receiver generated it.

Test = (BitStream || Impl) \ {bit[0],bit[1],Bit[0],Bit[1],empty,rready};