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 LIST2 is
pr PACKET .
sort List2 .
op nil : -> List2 .
op _ _ : Packet List2 -> List2 .
op mk : Packet -> List2 .
op _\in_ : Packet List2 -> Bool .
var N : NzNat .
vars P P' : Packet .
var L : List2 .
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 LIST2 .

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:_  : List2 -> Obs .      --- Packets received by Receiver
*** Transitions
*** Maude variables


*** Transitions
*** Parameters
op NoP : -> Nat .
op Len : -> Nat .
eq NoP = 20 .
eq Len = 10.
*** Maude variables
var PC : PairChan .
var BC : BoolChan .
vars B B1 B2 X : Bool .
var P : Packet .
var L : List2 .
var BP : Pair .
*** Transition rules
--- send1
crl [send1] : (chan1: PC) (bit1: B1) (pac: P)
=> (chan1: (if isNth(P,NoP) then PC else put(PC,< B1,P >) fi))
(bit1: B1) (pac: P)
if len(PC) < Len .
--- rec1
rl [rec1] : (chan2: (B BC)) (bit1: B1) (pac: P)
=> (chan2: BC) (bit1: (if B1 == B then B1 else not B1 fi))
(pac: (if B1 == B then P else next(P) fi)) .
--- send2
crl [send2] : (chan2: BC) (bit2: B2)
=> (chan2: put(BC,B2)) (bit2: B2)
if len(BC) < Len .
--- rec2
rl [rec2] : (chan1: (BP PC)) (bit2: B2) (list: L)
=> (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)) .
--- 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


mod ABP-INIT is
pr ABP .
pr SEARCH .
sorts Trans Obs Sys ListSys .
subsorts Trans Obs < Sys < ListSys .

op init : -> Sys .

op nil : -> ListSys .
op _||_ : Sys ListSys -> ListSys .
op downTermSearch : TermList -> ListSys .

var TERM : Term .
var TERMLIST : TermList .
var S : Sys .
vars B1 B2 B3 : Bool .
var P : Packet .
var L : List2 .
var BC : BoolChan .

eq init = (chan1: empty) (chan2: empty) (bit1: false) (bit2: false) (pac: pac(0)) (list: (nil)) .

eq downTermSearch(empty) = nil .
eq downTermSearch(TERM) = downTerm(TERM, nil)  .
eq downTermSearch(nil) = nil .
eq downTermSearch((TERM,TERMLIST)) =  downTerm(TERM, nil) || downTermSearch(TERMLIST) .

endm


 reduce in ABP-INIT : downTermSearch(genSeq('ABP, upTerm(init), 9, 1000 )) .

*** etAllSuccessors(upModule(ABP, false), upTerm(init),getLabels(upModule(ABP, false)) ) .

*** downTermSearch(genSeq('ABP, upTerm(init), 5, 115 )) .


**** getAllSuccessors : Module Term QidList -> TermList .