交错位协议(Alternating Bit Protocol, ABP)
    它是最早的端到端通讯协议之一。它在一条不可靠的传输介质上，提供一个可靠的数据连接服务。AB协议的总目标是按顺序传递数据，恢复数据丢失。AB协议分为四个实体：发送方、接受方、消息信道和确认信道。
    发送方将消息的第一部分，连同控制位0一起发送。如果接受方收到了带有控制为0的信息，它通过确认信道发送0。发送方收到这个消息确认后，它发送下一个数据包，连同控制位1。如果接收方收到这条消息，它通过确认信道发送1以示确认。并且，它们忽略含有非预期控制位的信息。通过交错位，接收方和发送方可以防止消息的重复和丢失。
    如果发送发没有得到预期的确认，它继续重发那条消息，知道确认到达。如果接收方没有收到带有预期控制位的消息，它将继续重发先前的确认。

要验证的PPTL性质：
[]((s.st=sent)&&(s.message1=TRUE) -> msg_chan.output1=TRUE)
含义：如果消息位1已经发送并且返回正确的确认，则接收方实际接收到一个1。
模型满足该性质。