-- ========================================================================
--        System Specifications of ABP (Alternating Bit Protocol)
-- ========================================================================
-- KF150209

-- ========================================================================
-- bits (2 elemnts) for alternation
mod! BIT {
 [BitLt < Bit]
 ops t f : -> BitLt .
 eq (B1:BitLt = B2:BitLt) = (B1 == B2) .
 -- bit alternation
 op not_ : Bit -> Bit .
 eq not(t) = f .  
 eq not(f) = t .
}

-- ========================================================================
-- Sequence (i.e. associative list) with {id: emp}
-- Sequence 
mod! SEQ (X :: TRIV) {
[Elt < Seq]
-- empty Sequence
op emp : -> Seq . 
op (_ _) : Seq Seq -> Seq {constr assoc id: emp}
-- for the case if either side is emp and other side is non-emp
eq[1]: (emp = (S21:Seq E:Elt S22:Seq)) = false .
-- for the case if both sides are non-emp
ceq[2]: (E1:Elt S1:Seq = E2:Elt S2:Seq) =
                 ((E1 = E2) and (S1 = S2)) 
        if not((S1 = emp) and (S2 = emp)) .
ceq[3]: (S1:Seq E1:Elt = S2:Seq E2:Elt) =
                 ((E1 = E2) and (S1 = S2)) 
        if not((S1 = emp) and (S2 = emp)) .
** note that without the condition of ceq, 
** (E1 = E2) gets into infinite loop
** because (E1 = E2) matchs to the left-hand side 
** and appears also in the right-hand side of [2] and [3]
}

-- ========================================================================
-- integer numbers
-- two element set {p s}
mod! PS {[Ps] ops p s : -> Ps}
-- each integer number is modeled as a sequence of 's' and 'p'
mod! NN {ex((SEQ(PS{sort Elt -> Ps}))*{sort Seq -> Nn, op emp -> 0})
 eq N1:Nn p N2:Nn s N3:Nn = N1 N2 N3 .
 eq N1:Nn s N2:Nn p N3:Nn = N1 N2 N3 .
-- _>_ sub term order
 pred _>_ : Nn Nn .
 eq (s N1:Nn > s N2:Nn) = (N1:Nn > N2:Nn) .
 eq (p N1:Nn > p N2:Nn) = (N1:Nn > N2:Nn) .
 eq (N1:Nn > s N2:Nn) = (p N1:Nn > N2:Nn) .
 eq (N1:Nn > p N2:Nn) = (s N1:Nn > N2:Nn) .
 ceq (s N1:Nn > N2:Nn) = true if (N1:Nn > N2:Nn) .
 ceq (p N1:Nn > N2:Nn) = true if (N1:Nn > N2:Nn) .
 eq (s N:Nn > N:Nn) = true .
 eq (p N:Nn > N:Nn) = true .
-- _=_ equality (built-in predicate)
 eq (s N1:Nn = s N2:Nn) = (N1 = N2) .
 eq (p N1:Nn = p N2:Nn) = (N1 = N2) .
 ceq (N1:Nn = N2:Nn) = false if ((N1 > N2) or (N2 > N1)) .
}

-- ========================================================================
-- pair of bit and natural number
mod! BNP{pr(BIT + NN)
 [Bnp]
 op bn : Bit Nn -> Bnp {constr} .
 eq (bn(B1:Bit,N1:Nn) = bn(B2:Bit,N2:Nn)) =
      (B1 = B2) and (N1 = N2) .
 -- successor/previous Bnp
 ops (p_) (s_) : Bnp -> Bnp .
 -- 'ops p_ s_ : Bnp -> Bnp .' does not work!
 eq p(bn(B:Bit,N:Nn)) = bn(not(B),p N) .
 eq s(bn(B:Bit,N:Nn)) = bn(not(B),s N) .
 --
 eq s p BN:Bnp = BN .
 eq p s BN:Bnp = BN .
-- sub term order
 pred _>_ : Bnp Bnp .
 eq (s BN1:Bnp > s BN2:Bnp) = (BN1:Bnp > BN2:Bnp) .
 eq (p BN1:Bnp > p BN2:Bnp) = (BN1:Bnp > BN2:Bnp) .
 eq (BN1:Bnp > s BN2:Bnp) = (p BN1:Bnp > BN2:Bnp) .
 eq (BN1:Bnp > p BN2:Bnp) = (s BN1:Bnp > BN2:Bnp) .
 ceq (s BN1:Bnp > BN2:Bnp) = true if (BN1:Bnp > BN2:Bnp) .
 ceq (p BN1:Bnp > BN2:Bnp) = true if (BN1:Bnp > BN2:Bnp) .
 eq (s BN:Bnp > BN:Bnp) = true .
 eq (p BN:Bnp > BN:Bnp) = true .
-- equality (_=_ is a built-in predicate)
 ceq (BN1:Bnp = BN2:Bnp) = false if ((BN1 > BN2) or (BN2 > BN1)) .
}

-- ========================================================================
-- integer number sequence
mod! NNseq{pr(SEQ(NN{sort Elt -> Nn})
              *{op emp -> empN, sort Seq -> NnSeq})
}
-- ========================================================================
-- Sender to receiver channel: sequence of Bit-Nn pairs 
mod! SRch {pr(SEQ(BNP{sort Elt -> Bnp})
              *{op emp -> empBN, sort Seq -> SrCh})
}
-- ========================================================================
-- receiver to sender channel: bit sequecne
mod! RSch {pr(SEQ(BIT{sort Elt -> Bit})
              *{op emp -> empB, sort Seq -> RsCh})
}

-- ========================================================================
-- observers
mod! OBS {pr(NNseq + SRch + RSch) 
[Obs]
** 6 kinds of observers
-- sender's bit
op (sBit:_) : Bit -> Obs {constr}   
-- the natural number Sender wants to deliver 
op (sNn:_) : Nn -> Obs {constr}     
-- Sender-to-Receiver channel
op (srCh:_) : SrCh -> Obs {constr}  
-- Receiver's bit
op (rBit:_) : Bit -> Obs {constr}   
-- the sequence of natural numbers received by Receiver
op (rNns:_) : NnSeq -> Obs {constr} 
-- Receiver-to-Sender channel
op (rsCh:_) : RsCh -> Obs {constr}  
}

-- ========================================================================
-- a configuration is an associative list of Obs
mod! CONFIG {pr(SEQ(OBS{sort Elt -> Obs})
                *{op emp -> empC, sort Seq -> Config})
}

-- ========================================================================
-- state pattern:
-- [(sBit: B:Bit)(sNn: N:Nn)(srCh: SRC:SrCh)
--  (rBit: Br:Bit)(rNns: NS:NnSeq)(rsCh: RSC:RsCh)]
mod! PRE-STATE {pr(CONFIG) 
[PreState] op [_] : Config -> PreState {constr} 
}

-- ========================================================================
-- Sender is putting a bit-number pair into SrCh
mod! SS {pr(PRE-STATE)
trans[ss]: [(sBit: B:Bit)(sNn: N:Nn)(srCh: SRC:SrCh) S:Config]
        => [(sBit: B)(sNn: N)(srCh: (bn(B,N) SRC)) S] .
}

-- ========================================================================
-- data drops at any point of srCh
mod! SRdr {pr(PRE-STATE)
trans[srdr]: 
   [S1:Config (srCh: (SRC1:SrCh BNP:Bnp SRC2:SrCh)) S2:Config]
   => [S1 (srCh: (SRC1 SRC2)) S2] .
}

-- ========================================================================
-- data duplicates at any point of srCh
mod! SRdu {pr(PRE-STATE)
trans[srdu]: 
   [S1:Config (srCh: (SRC1:SrCh BNP:Bnp SRC2:SrCh)) S2:Config]
   => [S1 (srCh: (SRC1 BNP BNP SRC2)) S2] .
}

-- ========================================================================
-- Receiver is receiving a bit-number pair from srCh
mod! RR {pr(PRE-STATE)
trans[rr]: 
   [S1:Config 
    (srCh: (SRC:SrCh bn(B:Bit,N:Nn)))(rBit: Br:Bit)(rNns: NS:NnSeq) 
    S2:Config]
   => if (B = Br) 
      then [S1 (srCh: SRC)(rBit: not(Br))(rNns: (N NS)) S2]
      else [S1 (srCh: SRC)(rBit: Br)(rNns: NS) S2] fi .
}

-- ========================================================================
-- Receiver is sending a number to RsCh
mod! RS {pr(PRE-STATE)
trans[rs]: [S:Config (rBit: B:Bit)(rsCh: RSC:RsCh)]
           => [S (rBit: B)(rsCh: (B RSC))] .
}

-- ========================================================================
-- data drops at any point of rsCh
mod! RSdr {pr(PRE-STATE)
trans[rsdr]: 
  [S1:Config (rsCh: (RSC1:RsCh B:Bit RSC2:RsCh)) S2:Config]
           => [S1 (rsCh: (RSC1 RSC2)) S2] .
}

-- ========================================================================
-- data duplicates at any point of rsCh
mod! RSdu {pr(PRE-STATE)
trans[rsdu]: 
  [S1:Config (rsCh: (RSC1:RsCh B:Bit RSC2:RsCh)) S2:Config]
           => [S1 (rsCh: (RSC1 B B RSC2)) S2] .
}

-- ========================================================================
-- Sender is receiving a bit (an ack) from RsCh
mod! SR {pr(PRE-STATE)
trans[sr]: 
  [(sBit: Bs:Bit)(sNn: N:Nn) S:Config (rsCh: (RSC:RsCh B:Bit))]
  => if (Bs = B) 
     then [(sBit: Bs)(sNn: N) S (rsCh: RSC)]
     else [(sBit: not(Bs))(sNn: (s N)) S (rsCh: RSC)] fi .
}

-- ========================================================================
-- ABPsys (alternating bit protocol)
mod! ABPsys {pr(SS + SRdr + SRdu + RR + RS + RSdr + RSdu + SR)}

-- ========================================================================
provide abp-sys

-- ========================================================================
eof