hide receiverToChannel, channelToSender, timeout,senderToChannel, channelToReceiver,requestFrame encap timeout0, timeout1, timeout2, timeout3, timeout4, timeout5,receiverToChannel1, receiverToChannel2, channelToReceiver1, channelToReceiver2, senderToChannel1, senderToChannel2, channelToReceiver1, channelToReceiver2, channelToSender1, channelToSender2 comm (timeout0, timeout1, timeout2), (timeout2, timeout3, timeout4), (timeout4, timeout5, timeout), (receiverToChannel1, receiverToChannel2, receiverToChannel), (channelToReceiver1, channelToReceiver2, channelToReceiver), (senderToChannel1, senderToChannel2, senderToChannel), (channelToSender1, channelToSender2, channelToSender) constant N = 4 type SeqNrs = {0..N} type AckNrs = {0..N-1} type Data = {0..1} constant DATAMAX = 5 type DataElements = {0..DATAMAX} constant WINDOWSIZE = 2 constant LOSS = 0.05 AckChannel(firstSeq:SeqNrs, secondSeq:SeqNrs) = secondSeq = N => sum(ack:SeqNrs, receiverToChannel1(ack).( firstSeq = N => AckChannel[firstSeq := ack] ++ firstSeq != N => AckChannel[secondSeq := ack])) ++ firstSeq != N => channelToSender1(firstSeq) . AckChannel[secondSeq, N] ++ firstSeq = N => timeout5 . AckChannel[] FrameChannel(firstSeq:SeqNrs, firstData:Data, secondSeq:SeqNrs, secondData:Data) = firstSeq = N => timeout3. FrameChannel[] ++ secondSeq = N => sum(seq:SeqNrs, sum(data:Data, senderToChannel1(seq,data) . ( firstSeq = N => FrameChannel[firstSeq := seq, firstData := data] ++ firstSeq != N => FrameChannel[secondSeq := seq, secondData := data]))) ++ firstSeq != N => channelToReceiver1(firstSeq, firstData) . FrameChannel[secondSeq, secondData, N, 0] Receiver(data0:Data, data1:Data, data2:Data, data3:Data, data4:Data, nextExpected:DataElements, wantsToSend:Bool, ackToSend:AckNrs) = nextExpected = DATAMAX => finished.received(data0,data1,data2,data3,data4).Receiver[] ++ wantsToSend => receiverToChannel2(ackToSend).Receiver[wantsToSend := F, ackToSend := 0] ++ !wantsToSend & nextExpected != DATAMAX => timeout1 . Receiver[] ++ sum(seq:SeqNrs, sum(data:Data, channelToReceiver2(seq, data) . psum( LOSS -> Receiver[] ++ minus(1,LOSS) -> nextExpected != 0 & mod(nextExpected, N) != seq => Receiver[wantsToSend := T, ackToSend := mod(minus(nextExpected, 1), N)] ++ nextExpected = 0 & mod(nextExpected, N) != seq => Receiver[wantsToSend := F, ackToSend := 0] ++ mod(nextExpected, N) = seq => Receiver[ifthenelse(nextExpected = 0,data,data0), ifthenelse(nextExpected = 1,data,data1), ifthenelse(nextExpected = 2,data,data2), ifthenelse(nextExpected = 3,data,data3), ifthenelse(nextExpected = 4,data,data4), min(nextExpected + 1, DATAMAX), T, mod(nextExpected, N)]))) Sender(srcdata0:Data, srcdata1:Data, srcdata2:Data, srcdata3:Data, srcdata4:Data, lastUnAcked:DataElements, nextToSend:DataElements, wantsToSend:Bool, dataToSend:Data, seqToSend:SeqNrs) = !wantsToSend & nextToSend - lastUnAcked >= WINDOWSIZE | !wantsToSend & lastUnAcked < DATAMAX & nextToSend = DATAMAX => timeout0 . Sender[nextToSend := lastUnAcked] ++ wantsToSend => senderToChannel2(seqToSend, dataToSend) . Sender[wantsToSend := F, dataToSend := 0, seqToSend := 0] ++ sum(ack:SeqNrs, channelToSender2(ack) . psum( LOSS -> Sender[] ++ minus(1,LOSS) -> lastUnAcked = DATAMAX => Sender[] ++ sum(i:{2..3}, ack = mod(lastUnAcked + i, N) => Sender[]) ++ sum(j:{0..1}, ack = mod(lastUnAcked + j, N) => Sender[lastUnAcked := min(lastUnAcked + 1, DATAMAX), nextToSend := max(min(lastUnAcked + 1, DATAMAX),nextToSend)]))) ++ !wantsToSend & nextToSend <= DATAMAX - 1 & nextToSend - lastUnAcked < WINDOWSIZE => requestFrame . Sender[nextToSend := nextToSend + 1, wantsToSend := T, dataToSend := ifthenelse(nextToSend = 0, srcdata0, ifthenelse(nextToSend = 1, srcdata1, ifthenelse(nextToSend = 2, srcdata2, ifthenelse(nextToSend = 3, srcdata3, srcdata4)))), seqToSend := mod(nextToSend, N)] init AckChannel[N,N] || FrameChannel[N,0,N,0] || Receiver[0,0,0,0,0,0,F,0] || Sender[1,0,1,1,1,0,0,F,0,0]