sort Bool
func T,F: -> Bool
map  and,or: Bool # Bool -> Bool
     not: Bool -> Bool
     if: Bool # Bool # Bool -> Bool
     eq: Bool # Bool -> Bool
var  x,y: Bool
rew  and(T,x)=x
     and(x,T)=x
     and(x,F)=F
     and(F,x)=F
     or(T,x)=T
     or(x,T)=T
     or(x,F)=x
     or(F,x)=x
     not(F)=T
     not(T)=F
     if(T,x,y)=x
     if(F,x,y)=y
     eq(x,x)=T
     eq(T,F)=F
     eq(F,T)=F

sort State
func 0,1,2,3,4: -> State
map  if: Bool # State # State -> State
     eq: State # State -> Bool
var  a,b: State
rew  if(T,a,b)=a
     if(F,a,b)=b
     eq(a,a)=T
     eq(0,1)=F
     eq(0,2)=F
     eq(0,3)=F
     eq(0,4)=F
     eq(1,0)=F
     eq(1,2)=F
     eq(1,3)=F
     eq(1,4)=F
     eq(2,0)=F
     eq(2,1)=F
     eq(2,3)=F
     eq(2,4)=F
     eq(3,0)=F
     eq(3,1)=F
     eq(3,2)=F
     eq(3,4)=F
     eq(4,0)=F
     eq(4,1)=F
     eq(4,2)=F
     eq(4,3)=F

sort Node
func O:-> Node
	S:Node->Node
map  eq: Node # Node -> Bool
var  m,n:Node
rew  eq(n,n)=T
	eq(O,S(n))=F
	eq(S(n),O)=F
	eq(S(m),S(n))=eq(m,n)

map n0,n1,n2,n3,n4,n5,n6,n7,n8,n9,n10,n11,n12,n13,n14,n15,n16,n17:->Node
rew	n0=O
	n1=S(n0)
	n2=S(n1)
	n3=S(n2)
	n4=S(n3)
	n5=S(n4)
	n6=S(n5)
	n7=S(n6)
	n8=S(n7)
	n9=S(n8)
	n10=S(n9)
	n11=S(n10)
	n12=S(n11)
	n13=S(n12)
	n14=S(n13)
	n15=S(n14)
	n16=S(n15)
	n17=S(n16)

sort Nodelist
func emptylist: -> Nodelist
     in: Node # Nodelist -> Nodelist
map  if: Bool # Nodelist # Nodelist -> Nodelist
     remove: Node # Nodelist -> Nodelist
     occur: Node # Nodelist -> Bool
     empty: Nodelist -> Bool
     singleton: Nodelist -> Bool
     singleton: Nodelist # Node -> Bool
	eq:Nodelist # Nodelist -> Bool
var  i,j,k: Node
     p,q: Nodelist
rew
	eq(p,p)=T
	eq(emptylist,emptylist)=T
	eq(in(i,p),emptylist)=F
	eq(emptylist,in(i,p))=F
	eq(in(i,p),in(j,q))=and(eq(i,j),eq(p,q))

     if(T,p,q)=p
     if(F,p,q)=q
     remove(i,emptylist)=emptylist
     remove(i,in(j,p))=if(eq(i,j),remove(i,p),in(j,remove(i,p)))
     occur(i,emptylist)=F
     occur(i,in(j,p))=if(eq(i,j),T,occur(i,p))
     empty(emptylist)=T
     empty(in(i,p))=F
     singleton(emptylist)=F
     singleton(in(i,emptylist))=T
     singleton(in(i,in(j,p)))=F
     singleton(emptylist,i)=F
     singleton(in(j,emptylist),i)=eq(i,j)
     singleton(in(j,in(k,p)),i)=F

sort Signal
func req,ack: -> Signal
map  eq: Signal # Signal -> Bool
rew  eq(req,req)=T
     eq(ack,ack)=T
     eq(req,ack)=F
     eq(ack,req)=F

act  r,s,c,r',s',c': Node # Node # Signal
     leader: Node

comm s|r   = c
     s'|r' = c'

proc
X(i:Node,p:Nodelist,q:Nodelist,a:State) =
  sum(j:Node,r(j,i,req).X(i,remove(j,p),in(j,q),if(singleton(p),1,0))
        <| and(eq(a,0),occur(j,p)) |> delta)
+ sum(j:Node,s'(i,j,ack).X(i,p,remove(j,q),1)
        <| and(and(eq(a,0),singleton(p)),occur(j,q)) |> delta)
+ sum(j:Node,s'(i,j,req).X(i,p,q,2)
        <| and(and(eq(a,0),singleton(p,j)),empty(q)) |> delta)
+ sum(j:Node,s'(i,j,ack).X(i,p,remove(j,q),1)
        <| and(eq(a,1),occur(j,q)) |> delta)
+ sum(j:Node,s'(i,j,req).X(i,p,q,2)
        <| and(and(eq(a,1),singleton(p,j)),empty(q)) |> delta)
+ leader(i).X(i,p,q,4)
        <| and(and(eq(a,1),empty(p)),empty(q)) |> delta
+ sum(j:Node,r(j,i,req).X(i,emptylist,in(j,q),1)
        <| and(eq(a,1),singleton(p,j)) |> delta)
+ sum(j:Node,r(j,i,ack).X(i,p,q,4)
        <| and(eq(a,2),singleton(p,j)) |> delta)
+ sum(j:Node,r(j,i,req).X(i,p,q,3)
        <| and(eq(a,2),singleton(p,j)) |> delta)
+ sum(j:Node,r(j,i,req).X(i,emptylist,p,1)
        <| and(eq(a,3),singleton(p,j)) |> delta)
+ sum(j:Node,s'(i,j,req).X(i,p,q,2)
        <| and(eq(a,3),singleton(p,j)) |> delta)

B(i:Node,j:Node) = r'(i,j,req).s(i,j,req).B(i,j)
                 + r'(i,j,ack).s(i,j,ack).B(i,j)

init  hide({c,c'},
          encap({r,s,r',s'},
     X(n0,in(n1,in(n2,in(n3,emptylist))),emptylist,0) ||
     X(n1,in(n0,emptylist),emptylist,0) ||
     X(n2,in(n0,emptylist),emptylist,0) ||
     X(n3,in(n0,in(n4,emptylist)),emptylist,0) ||
     X(n4,in(n3,in(n5,in(n12,emptylist))),emptylist,0) ||
     X(n5,in(n4,in(n6,in(n7,in(n8,emptylist)))),emptylist,0) ||
     X(n6,in(n5,emptylist),emptylist,0) ||
     X(n7,in(n5,emptylist),emptylist,0) ||
     X(n8,in(n5,in(n9,in(n10,in(n11,emptylist)))),emptylist,0) ||
     X(n9,in(n8,emptylist),emptylist,0) ||
     X(n10,in(n8,emptylist),emptylist,0) ||
     X(n11,in(n8,emptylist),emptylist,0) ||
     X(n12,in(n4,in(n13,emptylist)),emptylist,0) ||
     X(n13,in(n12,emptylist),emptylist,0) ||

     B(n0,n1) || B(n0,n2) || B(n0,n3) || B(n1,n0) || B(n2,n0) || B(n3,n0) ||
     B(n3,n4) || B(n4,n3) || B(n5,n4) || B(n4,n5) ||
     B(n5,n6) || B(n6,n5) ||B(n5,n7) || B(n7,n5) ||B(n5,n8) || B(n8,n5) ||
     B(n8,n9) || B(n9,n8)||B(n8,n10) || B(n10,n8)||B(n8,n11) || B(n11,n8) ||
B(n4,n12)||B(n12,n4)||B(n13,n12)||B(n12,n13)
))

map C2-Bool : Bool#Bool#Bool->Bool
var b,b1,b2:Bool
rew
	C2-Bool(T,b1,b2)=b1
	C2-Bool(F,b1,b2)=b2
	C2-Bool(b,b1,b1)=b1