fmod PACKET is
  pr NAT .
  sort Packet .
  op pac : Nat -> Packet .
  op next : Packet -> Packet .
  op isNth : Packet Nat -> Bool .
  vars M N : Nat .
  eq next(pac(N)) = pac(N + 1) .
  eq isNth(pac(M),N) = (M == N) .
endfm

fmod PAIR is
  pr PACKET .
  sort Pair .
  op <_,_> : Bool Packet -> Pair .
  op b : Pair -> Bool .
  op p : Pair -> Packet .
  var B : Bool .
  var P : Packet .
  eq b(< B,P >) = B .
  eq p(< B,P >) = P .
endfm

fmod PAIR-CHANNEL is
  pr PAIR .
  sorts NePairChan PairChan . 
  subsort NePairChan < PairChan . 
  op empty : -> PairChan .
  op _ _ : Pair PairChan -> NePairChan .
  op put : PairChan Pair -> NePairChan .
  op get : PairChan -> PairChan .
  op top : NePairChan -> Pair .
  op len : PairChan -> Nat .
  op _\in_ : Packet PairChan -> Bool .
  vars P P' : Pair .
  vars C : PairChan .
  vars Pac Pac' : Packet .
  var B : Bool .
  eq put(empty,P) = P empty .
  eq put(P' C,P) = P' put(C,P) .
  eq get(empty) = empty .
  eq get(P C) = C .
  eq top(P C) = P .
  eq len(empty) = 0 .
  eq len(P C) = 1 + len(C) .
  eq Pac \in empty = false .
  eq Pac \in < B,Pac' > C = (Pac == Pac') or (Pac \in C) .
endfm

fmod BOOL-CHANNEL is
  pr NAT .
  sorts NeBoolChan BoolChan . 
  subsort NeBoolChan < BoolChan . 
  op empty : -> BoolChan .
  op _ _ : Bool BoolChan -> NeBoolChan .
  op put : BoolChan Bool -> NeBoolChan .
  op get : BoolChan -> BoolChan .
  op top : NeBoolChan -> Bool .
  op len : BoolChan -> Nat .
  vars B B' : Bool .
  vars C : BoolChan .
  eq put(empty,B) = B empty .
  eq put(B' C,B) = B' put(C,B) .
  eq get(empty) = empty .
  eq get(B C) = C .
  eq top(B C) = B .
  eq len(empty) = 0 .
  eq len(B C) = 1 + len(C) .
endfm

fmod LIST is
  pr PACKET .
  sort List .
  op nil : -> List .
  op _ _ : Packet List -> List .
  op mk : Packet -> List .
  op _\in_ : Packet List -> Bool .
  var N : NzNat .
  vars P P' : Packet .
  var L : List .
  eq mk(pac(0)) = pac(0) nil .
  eq mk(pac(N)) = pac(N) mk(pac(sd(N,1))) .
  eq P \in nil = false .
  eq P \in P' L = (P == P') or (P \in L) .
endfm

fmod OTS-ABP is
  pr PAIR-CHANNEL .
  pr BOOL-CHANNEL .
  pr LIST .
  --- the state space
  sort Sys .
  --- an arbitrary initial state
  op init : -> Sys .
  --- observers
  op chan1 : Sys -> PairChan .  --- Sender-to-Receiver channel 
  op chan2 : Sys -> BoolChan .  --- Receiver-to-Sender channel
  op bit1  : Sys -> Bool .      --- Sender's bit
  op bit2  : Sys -> Bool .      --- Receiver's bit
  op pac   : Sys -> Packet .    --- Packet to be sent by Sender to Receiver
  op list  : Sys -> List .      --- Packets received by Receiver
  --- transitions
  op send1 : Sys -> Sys .       --- Sender's sending pairs of bits&packets
  op rec1  : Sys -> Sys .       --- Sender's receiving bits
  op send2 : Sys -> Sys .       --- Receiver's sending bits
  op rec2  : Sys -> Sys .       --- Receiver's receiving pairs of bits&packets
  op drop1 : Sys -> Sys .       --- dropping the 1st of fifo1
  op dup1  : Sys -> Sys .       --- duplicating the 1st of fifo1
  op drop2 : Sys -> Sys .       --- dropping the 1st of fifo2
  op dup2  : Sys -> Sys .       --- duplicating the 1st of fifo2
  --- Maude variables
  var S : Sys .
  --- init
  eq chan1(init) = empty .
  eq chan2(init) = empty .
  eq bit1(init)  = false .
  eq bit2(init)  = false .
  eq pac(init)   = pac(0) .
  eq list(init)  = nil .
  --- send1
  eq chan1(send1(S)) = put(chan1(S),< bit1(S),pac(S) >) .
  eq chan2(send1(S)) = chan2(S) .
  eq bit1(send1(S))  = bit1(S) .
  eq bit2(send1(S))  = bit2(S) .
  eq pac(send1(S))   = pac(S) .
  eq list(send1(S))  = list(S) .
  --- rec1
  op c-rec1 : Sys -> Bool .
  eq c-rec1(S) = not(chan2(S) == empty) .
  ---
  eq  chan1(rec1(S)) = chan1(S) .
  ceq chan2(rec1(S)) = get(chan2(S)) if c-rec1(S) .
  ceq bit1(rec1(S))
      = (if bit1(S) == top(chan2(S)) then bit1(S) else not bit1(S) fi)
      if c-rec1(S) .
  eq  bit2(rec1(S))  = bit2(S) .
  ceq pac(rec1(S))  
      = (if bit1(S) == top(chan2(S)) then pac(S) else next(pac(S)) fi)
      if c-rec1(S) .
  eq list(rec1(S))  = list(S) .
  ceq rec1(S)      = S if not c-rec1(S) .
  --- send2
  eq chan1(send2(S)) = chan1(S) .
  eq chan2(send2(S)) = put(chan2(S),bit2(S)) .
  eq bit1(send2(S))  = bit1(S) .
  eq bit2(send2(S))  = bit2(S) .
  eq pac(send2(S))   = pac(S) .
  eq list(send2(S))  = list(S) .
  --- rec2
  op c-rec2 : Sys -> Bool .
  eq c-rec2(S) = not(chan1(S) == empty) .
  ---
  ceq chan1(rec2(S)) = get(chan1(S)) if c-rec2(S) .
  eq  chan2(rec2(S)) = chan2(S) .
  eq  bit1(rec2(S))  = bit1(S) .
  ceq bit2(rec2(S))  
      = (if bit2(S) == b(top(chan1(S))) then not bit2(S) else bit2(S) fi)
      if c-rec2(S) .
  eq  pac(rec2(S))   = pac(S) .
  ceq list(rec2(S))  
      = (if bit2(S) == b(top(chan1(S)))
         then (p(top(chan1(S))) list(S)) else list(S) fi) 
      if c-rec2(S) .
  ceq rec2(S)      = S if not c-rec2(S) .
  --- drop1
  op c-drop1 : Sys -> Bool .
  eq c-drop1(S) = not(chan1(S) == empty) .
  ---
  ceq chan1(drop1(S)) = get(chan1(S)) if c-drop1(S) .
  eq  chan2(drop1(S)) = chan2(S) .
  eq  bit1(drop1(S))  = bit1(S) .
  eq  bit2(drop1(S))  = bit2(S) .
  eq  pac(drop1(S))   = pac(S) .
  eq  list(drop1(S))  = list(S) .
  ceq drop1(S)       = S if not c-drop1(S) .
  --- dup1
  op c-dup1 : Sys -> Bool .
  eq c-dup1(S) = not(chan1(S) == empty) .
  ---
  ceq chan1(dup1(S)) = top(chan1(S)) chan1(S) if c-dup1(S) .
  eq  chan2(dup1(S)) = chan2(S) .
  eq  bit1(dup1(S))  = bit1(S) .
  eq  bit2(dup1(S))  = bit2(S) .
  eq  pac(dup1(S))   = pac(S) .
  eq  list(dup1(S))  = list(S) .
  ceq dup1(S)       = S if not c-dup1(S) .
  --- drop2
  op c-drop2 : Sys -> Bool .
  eq c-drop2(S) = not(chan2(S) == empty) .
  ---
  eq  chan1(drop2(S)) = chan1(S) .
  ceq chan2(drop2(S)) = get(chan2(S)) if c-drop2(S) .
  eq  bit1(drop2(S))  = bit1(S) .
  eq  bit2(drop2(S))  = bit2(S) .
  eq  pac(drop2(S))  = pac(S) .
  eq  list(drop2(S))  = list(S) .
  ceq drop2(S)       = S if not c-drop2(S) .
  --- dup2
  op c-dup2 : Sys -> Bool .
  eq c-dup2(S) = not(chan2(S) == empty) .
  ---
  eq  chan1(dup2(S)) = chan1(S) .
  ceq chan2(dup2(S)) = top(chan2(S)) chan2(S) if c-dup2(S) .
  eq  bit1(dup2(S))  = bit1(S) .
  eq  bit2(dup2(S))  = bit2(S) .
  eq  pac(dup2(S))   = pac(S) .
  eq  list(dup2(S))  = list(S) .
  ceq dup2(S)       = S if not c-dup2(S) .
endfm