-- ========================================================================
--              Property Specification of ABP
-- ========================================================================

-- ========================================================================
require abp-sys
require predCj

-- ========================================================================
-- well formed PreState is State
mod! STATE {ex(PREDcj(PRE-STATE{sort Elt -> PreState}))
-- well formed PreState = State
op st : -> Pname .
eq cj(st,[((sBit: Bs:Bit)(sNn: Ns:Nn)(srCh: SRC:SrCh)
          (rBit: Br:Bit)(rNns: NS:NnSeq)(rsCh: RSC:RsCh))]) = true .
[State < PreState] 
eq (C:PreState :is State) = cj(st,C) .
}

-- ========================================================================
-- the initial state; notice that (cj(st,init) = true)
mod! INIT {ex(STATE)
op init : -> State .
eq init = [(sBit: f)(sNn: 0)(srCh: empBN)(rBit: f)(rNns: empN)(rsCh: empB)] .
op init : -> Pname .
eq cj(init,[((sBit: f)(sNn: 0)(srCh: empBN)
            (rBit: f)(rNns: empN)(rsCh: empB))]) = true .
}

-- ========================================================================
-- elemental predicates over SrCh
mod! SRchPred {ex(SRch)
-- zero gap: 0g(BN:Bnp,SRC:SrCh) asserts that any element in SRC is BN
pred 0g : Bnp SrCh .
eq 0g(BN:Bnp,empBN) = true .
eq 0g(BN1:Bnp,(SRC1:SrCh BN2:Bnp SRC2:SrCh)) = 
   ((BN1 = BN2) implies (0g(BN1,SRC1) and 0g(BN2,SRC2))) and
   (not(BN1 = BN2) implies false) .
-- at most one gap: 1g(BN:Bnp,:SRC:SrCh) asserts that
--                  any element in SRC is either BN or p(BN) 
--                  and any BN never appears after any p(BN) 
pred 1g : Bnp SrCh .
eq 1g(BN:Bnp,empBN) = true .
eq 1g(BN1:Bnp,SRC1:SrCh BN2:Bnp SRC2:SrCh) =
   ((BN1 = BN2) implies (0g(BN1,SRC1) and 1g(BN2,SRC2))) and
   (not(BN1 = BN2) implies
     (((BN2 = p(BN1)) implies (1g(BN1,SRC1) and 0g(BN2,SRC2))) and
      (not(BN2 = p(BN1)) implies false))) .
}

-- ========================================================================
-- elemental predicates over RsCh
mod! RSchPred {ex(RSch)
-- zero gap: 0g(B:Bit,RSC:RsCh) asserts that 
--           RSC starts with B and all elements of RSC is B
pred 0g : Bit RsCh .
eq 0g(B:Bit,empB) = true .
eq 0g(B1:Bit,(RSC1:RsCh B2:Bit RSC2:RsCh)) = 
   ((B1 = B2) implies (0g(B2,RSC1) and 0g(B2,RSC2))) and
   (not(B1 = B2) implies false) .
-- at most one gap: 1g(B:Bit,:RSC:RsCh) asserts that
--                  any element in RSC is either B or not(B) 
--                  and any B never appears after any not(B) 
pred 1g : Bit RsCh .
eq 1g(B:Bit,empB) = true .
eq 1g(B1:Bit,RSC1:RsCh B2:Bit RSC2:RsCh) =
   ((B1 = B2) implies (0g(B1,RSC1) and 1g(B2,RSC2))) and
   (not(B1 = B2) implies (1g(B1,RSC1) and 0g(B2,RSC2))) .
}

-- ========================================================================
-- making a  NNseq (number sequence)
mod! NNSmk{pr(NNseq)
-- make sequence
op mk : Nn -> NnSeq .
eq mk(0) = (0 empN) .
eq mk(s N:Nn) = ((s N) mk(N)) .
}

-- ========================================================================
-- ABP's possible invariant state predicates
mod! ABPpred {ex(STATE + NNSmk + SRchPred + RSchPred)
-- ft: faithful transmission, goal/targer predicate
op ft : -> Pname .
eq cj(ft,[((sBit: Bs:Bit)(sNn: N:Nn) C1:Config 
          (rBit: Br:Bit)(rNns: NS:NnSeq) C2:Config)])
   = ((Bs = Br) implies (mk(N) = (N NS))) and
     (not(Bs = Br) implies (mk(N) = NS)) .

-- sender-receiver channel
op sr : -> Pname .
eq cj(sr,[((sBit: Bs:Bit)(sNn: Ns:Nn)(srCh: SRC:SrCh)
          (rBit: Br:Bit)C:Config)])
   = ((Bs = Br) implies 1g(bn(Bs,Ns),SRC)) and
     (not(Bs = Br) implies 0g(bn(Bs,Ns),SRC)) .

-- receiver-sender channel
op rs : -> Pname .
eq cj(rs,[((sBit: Bs:Bit)C1:Config
          (rBit: Br:Bit)C2:Config(rsCh: RSC:RsCh))])
   = ((Bs = Br) implies 0g(Br,RSC)) and
     (not(Bs = Br) implies 1g(Br,RSC)) .
}

-- ========================================================================
-- ABP's possible inductive invariant predicates
mod! IINV {pr(ABPpred)
ops iinv1 iinv2 : -> PnameSeq .
eq iinv1 = st .
eq iinv2 = ft sr rs .
}

-- ========================================================================
provide abp-prop

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

-- ========================================================================
#|comment-start kf150210

The transition patterns of ABP are explained.

State patterns/configurations are represented as:
   [(sBit: Bs:Bit)(sNn: Ns:Nn)(srCh: SRC:SrCh)
    (rBit: Br:Bit)(rNns: NS:NnSeq)(rsCh: RSC:RsCh)]
and the ABP transitions are fully described in the following
transition scheme with the state patterns.

(1) <SR1>, <RS1>, <SR2>, or <RS2> represents some SrCh or RsCh sequence 
    that satisfies the following equations.
      eq 0g(dn(B,N), <SR1>) = true .
      eq 0g(B, <RS1>) = true .
      eq 0g(dn(~B,(s N)), <SR2>) = true .
      eq 0g(~B, <RS2>) = true .
(2) (mk(N) = (N NS)) and (~B = not(B)).
(3) Data (i.e. Bnp and Bit) are getting through 
    SrCh (sender-reciever channel) and RsCh (reciever-sender channel) 
    from left to right.

-- ========================================================================
[(sBit: B) (sNn: N)      (srCh: <SR1>)      {SS,SRdr,SRdu,RS,RSdr,RSdu,SR}
 (rBit: B) (rNns: NS)    (rsCh: <RS1>)]
 {RR}=> 
[(sBit: B) (sNn: N)      (srCh: <SR1>)      {SS,SRdr,SRdu,RR,RSdr,RSdu,SR}
 (rBit: ~B)(rNns: (N NS))(rsCh: <RS1>)]
 {RS}=> <={RSdr}
[(sBit: B) (sNn: N)      (srCh: <SR1>)      {SS,SRdr,SRdu,RR,RSdr,RSdu,SR}
 (rBit: ~B)(rNns: (N NS))(rsCh: <RS2><RS1>)]
 {SR,RSdr}=> 
[(sBit: B) (sNn: N)      (srCh: <SR1>)      {SS,SRdr,SRdu,RR,RS,RSdr,RSdu}
 (rBit: ~B)(rNns: (N NS))(rsCh: <RS2>)]
 {SR}=> 
[(sBit: ~B)(sNn: (s N))  (srCh: <SR1>)      {SRdr,SRdu,RR,RS,RSdr,RSdu,SR}
 (rBit: ~B)(rNns: (N NS))(rsCh: <RS2>)]
 {SS}=> <={SRdr}
[(sBit: ~B)(sNn: (s N))  (srCh: <SR2><SR1>) {SS,SRdr,SRdu,RR,RS,RSdr,RSdu}
 (rBit: ~B)(rNns: (N NS))(rsCh: <RS2>)]
 {RR,SRdr}=>
[(sBit: ~B)(sNn: (s N))  (srCh: <SR2>)      {SS,SRdr,SRdu,RS,RSdr,RSdu,SR}
 (rBit: ~B)(rNns: (N NS))(rsCh: <RS2>)]
-- ========================================================================

Note that the first and the last state patterns represent the same class of
states, and the transition scheme represents the cycle with six state
patterns that describes all the possible transitions of ABP.

comment-end|#
-- ========================================================================