APPENDIX C $$ VERIFICATION MODEL OF A SLIDING WINDOW PROTOCOL This model of a go$-$back$-$n sliding window protocol follows the description from p$.214,$ pp$.232-233,[71].$ The model below includes some annotations to facilitate random and guided simulations with SPIN. $1$ #define MaxSeq $5/*$ window size $*/2$ #define Wrong$($x$)$ x $=($x$+1)$ percent $($MaxSeq$)3$ #define Right$($x$)$ x $=($x$+1)$ percent $($MaxSeq $+1)4$ #define inc$($x$)$ Right$($x$)56$ chan q$[2]=[$MaxSeq$]$ of $\{$ byte, byte $\}$; $/*$ message passing channel $*/78$ active $[2]$ proctype p$5()/*$ starts two copies of proctype p$5*/9\{$ byte NextFrame, AckExp, FrameExp, r$,$ s$,$ nbuf, i; $10$ chan in$,$ out; $11$ in $=$ q$[\_$pid$]$; $12$ out $=$ q$[1-\_$pid$]$; $13$ xr in; xs out; $/*$ partial order reduction claims $*/1415$ do $16$ :: nbuf $<$ MaxSeq $->/*$ outgoing messages $*/17$ nbuf$++$; $18$ out!NextFrame, $($FrameExp $+$ MaxSeq$)$ percent $($MaxSeq $+1)$; $19$ inc$($NextFrame$)2021$ :: q$[\_$pid$]?$r$,$s $->/*$ incoming messages $*/22$ if $23$ :: r $==$ FrameExp $->24$ printf$($MSC: accept percentd

$,$ r$)$; $25$ inc$($FrameExp$)26$ :: else $/*$ ignore message $*/27$ fi; $28$ do $29$ :: $(($AckExp $<=$ s$)$ && $($s $<$ NextFrame$))30||(($AckExp $<=$ s$)$ && $($NextFrame $<$ AckExp$))31||(($s $<$ NextFrame$)$ && $($NextFrame $<$ AckExp$))->32$ nbuf$--$; $33$ inc$($AckExp$)34$ :: else $->$ break $35$ od $3637$ :: timeout $->$ && $/*$ retransmission timeout $*/38$ NextFrame $=$ AckExp; $39$ printf$($MSC: timeout

$)$; $40$ i $=1$; $41$ do $42$ :: i $<=$ nbuf $->43$ out!NextFrame, $($FrameExp $+$ MaxSeq$)$ percent $($MaxSeq $+1)$; $44$ inc$($NextFrame$)$; $45$ i$++46$ :: else $->$ break $47$ od $48$ od $49\}$ ACKNOWLEDGMENT