This is a modification of the Alternating Bit Protocol, except the sender only has finite number of messages (PckCount) to send, and the channels (msgC, ackC) are reliable, they can not lose messages.
The liveness condition is <>(pc["R"]="Done"); i.e. the Receiver eventually receives all messages and finishes
The model checker should not generate infinite number of states for this spec, all the state variables are bounded: All the integer variables are bounded by range 0..PckCount. PckCount is a constant, and I give it a value 10 to the model checker. I also tell the model checker to restrict the length of the two tuples (msgC and ackC) to 10. element of those two tuples can only be in 0..(PckCount-1).