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

mod ABP is
  pr PAIR-CHANNEL .
  pr BOOL-CHANNEL .
  pr LIST .
  sorts Trans Obs Sys .
  subsorts Trans Obs < Sys .
  *** Configuration
  op none : -> Sys .
  op _ _ : Sys Sys -> Sys [assoc comm id: none] .
  *** Observation
  op chan1:_ : PairChan -> Obs .  --- Sender-to-Receiver channel 
  op chan2:_ : BoolChan -> Obs .  --- Receiver-to-Sender channel
  op bit1:_  : Bool -> Obs .      --- Sender's bit
  op bit2:_  : Bool -> Obs .      --- Receiver's bit
  op pac:_   : Packet -> Obs .    --- Packet to be sent by Sender to Receiver
  op list:_  : List -> Obs .      --- Packets received by Receiver
  op prg1:_  : Bool -> Obs .      --- for strong fairness given to send1
  op prg2:_  : Bool -> Obs .      --- for strong fairness given to rec1
  op prg3:_  : Bool -> Obs .      --- for strong fairness given to send2
  op prg4:_  : Bool -> Obs .      --- for strong fairness given to rec2
  *** Transitions
  *** Parameters
  op NoP : -> Nat .
  op Len : -> Nat .
  eq NoP = 4 .
  eq Len = 4 .
  *** Maude variables
  var PC : PairChan .
  var BC : BoolChan .
  vars B B1 B2 X : Bool .
  var P : Packet .
  var L : List .
  var BP : Pair .
  *** Transition rules
  --- send1
  crl [send1] : (chan1: PC) (bit1: B1) (pac: P) (prg1: X)
    => (chan1: (if isNth(P,NoP) then PC else put(PC,< B1,P >) fi))
       (bit1: B1) (pac: P) (prg1: (not X)) 
    if len(PC) < Len .
  --- rec1
  rl [rec1] : (chan2: (B BC)) (bit1: B1) (pac: P) (prg2: X)
    => (chan2: BC) (bit1: (if B1 == B then B1 else not B1 fi))
       (pac: (if B1 == B then P else next(P) fi)) (prg2: (not X)) .
  --- send2
  crl [send2] : (chan2: BC) (bit2: B2) (prg3: X)
    => (chan2: put(BC,B2)) (bit2: B2) (prg3: (not X))
    if len(BC) < Len .
  --- rec2
  rl [rec2] : (chan1: (BP PC)) (bit2: B2) (list: L) (prg4: X)
    => (chan1: PC) (bit2: (if B2 == b(BP) then not B2 else B2 fi))
       (list: (if B2 == b(BP) then (p(BP) L) else L fi)) (prg4: (not X)) .
  --- drop1
  rl [drop1] : (chan1: (BP PC)) => (chan1: PC) .
  --- drop2
  rl [drop2] : (chan2: (B BC)) => (chan2: BC) .
  --- dup1
  crl [dup1] : (chan1: (BP PC)) => (chan1: (BP BP PC)) 
    if len(BP PC) < Len .
  --- dup2
  crl [dup2] : (chan2: (B BC)) => (chan2: (B B BC)) 
    if len(B BC) < Len .
endm

in model-checker .

mod ABP-PREDS is
  pr ABP .
  inc SATISFACTION .
  subsort Sys < State .
  op p-rcp : -> Prop .
  op isDelivered : Nat -> Prop .
  op enabled-send1 : Bool -> Prop .
  op applied-send1 : Bool -> Prop .
  op enabled-rec1  : Bool -> Prop .
  op applied-rec1  : Bool -> Prop .
  op enabled-send2 : Bool -> Prop .
  op applied-send2 : Bool -> Prop .
  op enabled-rec2  : Bool -> Prop .
  op applied-rec2  : Bool -> Prop .

  var S : Sys .
  var PR : Prop .
  vars B B1 B2 X : Bool .
  var P : Packet .
  var L : List .
  var N : Nat .
  var C : PairChan .
  var BP : Pair .
  var BC : BoolChan .

  eq (bit1: B1) (bit2: B2) (pac: P) (list: L) S |= p-rcp
     = ((B1 == B2) implies (mk(P) == (P L))) and
       ((B1 =/= B2) implies (mk(P) == L)) .
  eq (list: L) S |= isDelivered(N) = (pac(N) \in L) .
  eq (prg1: X) (chan1: C) S |= enabled-send1(X) = (len(C) < Len) .
  eq (prg1: X) S |= applied-send1(X) = true .
  eq (prg2: X) (chan2: (B BC)) S |= enabled-rec1(X) = true .
  eq (prg2: X) S |= applied-rec1(X) = true .
  eq (prg3: X) (chan2: BC) S |= enabled-send2(X) = (len(BC) < Len) .
  eq (prg3: X) S |= applied-send2(X) = true .
  eq (prg4: X) (chan1: (BP C)) S |= enabled-rec2(X) = true .
  eq (prg4: X) S |= applied-rec2(X) = true .
  eq S |= PR = false [owise] .
endm

mod ABP-CHECK is
  pr ABP-PREDS .
  inc MODEL-CHECKER .
  inc LTL-SIMPLIFIER .
  --- initial states
  op init : -> Sys .
  eq init = (chan1: empty) (chan2: empty) (bit1: false) (bit2: false)
            (pac: pac(0)) (list: nil)
            (prg1: true) (prg2: true) (prg3: true) (prg4: true) .
  --- properties
  op rcp : -> Formula .       *** Reliable Communication Proeprty
  op pcp : Nat -> Formula .   *** Progress Communication Property
  op sf1 : -> Formula .       *** Strong Fairness given to send1
  op sf2 : -> Formula .       *** Strong Fairness given to rec1
  op sf3 : -> Formula .       *** Strong Fairness given to send2
  op sf4 : -> Formula .       *** Strong Fairness given to rec1
  op fair : -> Formula .      *** Combining the four fairness assuptions
  
  var N : Nat .

  eq rcp = [] p-rcp .
  eq pcp(N) = <> isDelivered(N) .
  eq sf1 = (([] <> enabled-send1(true)) -> ([] <> applied-send1(false))) /\
          (([] <> enabled-send1(false)) -> ([] <> applied-send1(true))) .
  eq sf2 = (([] <> enabled-rec1(true)) -> ([] <> applied-rec1(false))) /\
          (([] <> enabled-rec1(false)) -> ([] <> applied-rec1(true))) .
  eq sf3 = (([] <> enabled-send2(true)) -> ([] <> applied-send2(false))) /\
          (([] <> enabled-send2(false)) -> ([] <> applied-send2(true))) .
  eq sf4 = (([] <> enabled-rec2(true)) -> ([] <> applied-rec2(false))) /\
          (([] <> enabled-rec2(false)) -> ([] <> applied-rec2(true))) .
  eq fair = sf1 /\ sf2 /\ sf3 /\ sf4 .
endm

eof

*** Checking Reliable Communication Proeprty
red in ABP-CHECK : modelCheck(init,rcp) .

*** Checking Progress Communication Property w/o any fairness assumptions
red in ABP-CHECK : modelCheck(init,pcp(0)) .
red in ABP-CHECK : modelCheck(init,pcp(1)) .
red in ABP-CHECK : modelCheck(init,pcp(2)) .
red in ABP-CHECK : modelCheck(init,pcp(3)) .

*** Checking Progress Communication Property with some fairness assumptions
red in ABP-CHECK : modelCheck(init,fair -> pcp(0)) .
red in ABP-CHECK : modelCheck(init,fair -> pcp(1)) .
red in ABP-CHECK : modelCheck(init,fair -> pcp(2)) .
red in ABP-CHECK : modelCheck(init,fair -> pcp(3)) .