--- ---------------------------------------------
--- ---------------------------------------------
--- Note : Since Maude doesn't allow to import theories in protecting model, 
--- all modules wil be imported with "including" but the intended semantics is that of protecting
--- ---------------------------------------------
--- ---------------------------------------------
fmod SEQUENCE{X :: TRIV} is
 sort Sequence .
 subsorts X$Elt < Sequence .
--- constructors 
 op empty : -> Sequence [ctor] .
 op _`,_ : Sequence Sequence -> Sequence [ctor id: empty assoc] .
---
 vars E F : X$Elt .
 vars Sq Se Sn : Sequence .
--- proof rule
 ceq true = false if Sq,E,Se := empty .
--- equality predicate 
 op _~_ : Sequence Sequence -> Bool .
 eq Sq ~ Sq = true .
 eq E,Sq ~ F,Se = (E == F) and (Sq ~ Se) .
--- matching predicate Se,E,Sn := Sq
 op match : Sequence Sequence Sequence -> Bool . 
 eq match(empty,Se,Sn) = false .
 eq match((E,Sq),empty,Sn) = Sq ~ Sn .  
 eq match((E,Sq),(F,Se),Sn) = (E == F)and match(Sq,Se,Sn) .
endfm
--- ---------------------------------------------
--- ---------------------------------------------
fmod PAIR{X :: TRIV, Y :: TRIV} is
 sort Pair .
 --- 
 op <_`,_> : X$Elt Y$Elt -> Pair [ctor] .
 op fst : Pair -> X$Elt .
 op snd : Pair -> Y$Elt .
 --- 
 vars A A' : X$Elt .
 vars B B' : Y$Elt .
 --- 
 eq fst(< A,B >) = A .
 eq snd(< A,B >) = B .
endfm
--- ---------------------------------------------
--- ---------------------------------------------
fmod DATA is inc NAT .
 sort Data .
 op data : Nat -> Data [ctor] .
endfm
--- ---------------------------------------------
--- ---------------------------------------------
fmod BIT is
 sort Bit .
 op t : -> Bit [ctor] .
 op f : -> Bit [ctor] .
 op not_ : Bit -> Bit .
 eq not f = t .
 eq not t = f .
---
 var B : Bit .
 eq  not not B = B .
--- proof rule --- discharges goal1(init) ---
 ceq true = false if t = f .
endfm
--- ---------------------------------------------
--- ---------------------------------------------
view TRIV2BIT from TRIV to BIT is 
 sort Elt to Bit .
endv

view TRIV2DATA from TRIV to DATA is 
 sort Elt to Data .
endv


fmod BIT-DATA-PAIR is 
 inc PAIR{TRIV2BIT, TRIV2DATA} * (sort Pair to BDPair) . 
endfm


view TRIV2BIT-DATA-PAIR from TRIV to BIT-DATA-PAIR is
 sort Elt to BDPair .
endv

fmod CHANNEL is 
 inc SEQUENCE{TRIV2BIT-DATA-PAIR} * (sort Sequence to Channel) .
endfm
--- ---------------------------------------------
--- ---------------------------------------------
fmod PACKET-LIST is
 inc SEQUENCE{TRIV2DATA} * 
  (sort Sequence to List,
   op empty to nil) .
 op mk : Nat -> List .
 var N : Nat .
 eq mk(0) = data(0),nil .
 eq mk(s N) = data(s N), mk(N) . 
endfm
--- ---------------------------------------------
--- ---------------------------------------------
th DS is inc CHANNEL . inc PACKET-LIST .
 sort Sys .
--- constructors ---
 op init : -> Sys [ctor].
 op send : Sys -> Sys [ctor].
 op rec : Sys -> Sys  [ctor].
 op drop : Sys -> Sys [ctor].
--- observations --- 
 op channel : Sys -> Channel .
 op bit  : Sys -> Bit .
 op next : Sys -> Nat .
 op list : Sys -> List .
--- variables ---
  vars S S' : Sys . var B : Bit . var C : Channel . var D : Data .
--- init ---
 eq channel(init) = (empty).Channel .
 eq bit(init) = f .
 eq next(init) = 0 .
 eq list(init) = nil .
--- send ---
 eq channel(send(S)) = channel(S),< bit(S),data(next(S)) > .
 eq bit(send(S)) = bit(S).
 eq next(send(S)) = next(S) .
 eq list(send(S)) = list(S) .
--- rec --- 
 ceq channel(rec(S)) = channel(S)   if channel(S) = empty       [metadata "CA-r1"].
 ceq channel(rec(S)) = C            if < B,D >,C := channel(S)  [metadata "CA-r2"].
 ceq bit(rec(S)) = bit(S)     if channel(S) = empty                        [metadata "CA-b1"].
 ceq bit(rec(S)) = bit(S)     if < B,D >,C := channel(S) /\ B = not bit(S) [metadata "CA-b2"].
 ceq bit(rec(S)) = not bit(S) if < B,D >,C := channel(S) /\ B = bit(S)     [metadata "CA-b3"].
 ceq next(rec(S)) = next(S)   if channel(S) = empty                        [metadata "CA-n1"].
 ceq next(rec(S)) = next(S)   if < B,D >,C := channel(S) /\ B = not bit(S) [metadata "CA-n2"].
 ceq next(rec(S)) = s next(S) if < B,D >,C := channel(S) /\ B = bit(S)     [metadata "CA-n3"].
 ceq list(rec(S)) = list(S)               if channel(S) = empty                        [metadata "CA-l1"].
 ceq list(rec(S)) = list(S)               if < B,D >,C := channel(S) /\ B = not bit(S) [metadata "CA-l2"].
 ceq list(rec(S)) = data(next(S)),list(S) if < B,D >,C := channel(S) /\ B = bit(S)     [metadata "CA-l3"].
--- underspecified operations ---
 ops x y : Sys -> Channel .
--- drop ---
 ceq channel(drop(S)) = x(S),y(S)  if x(S),< B,D >,y(S) := channel(S)     [metadata "CA-d1"].
 ceq channel(drop(S)) = channel(S) if match(channel(S),x(S),y(S)) = false [metadata "CA-d2"].
 eq bit(drop(S)) = bit(S).
 eq next(drop(S)) = next(S) .
 eq list(drop(S)) = list(S) .
---
 crl true => false if not bit(S) => bit(S)[metadata "1" nonexec].
endth