specification abracadabra_protocol [a, m] (N, P: nat) : noexit

  (*
  library Boolean, NaturalNumber, DecDigit endlib
  *)
  type Boolean is
    sorts
      bool
    opns
      true, false : -> bool
      not : bool -> bool
      _ and _, _ or _ : bool, bool -> bool
    eqns
      forall m, n: bool
      ofsort bool
        not (true) = false ;
        not (false) = true ;
  
        m and true = m ;
        true and n = n ;
        m and false = false ;
        false and n = false ;
  
        m or true = true ;
        true or n = true ;
        m or false = m ;
        false or n = n ;
    endtype
  
  type NaturalNumber is Boolean
    sorts
      nat
    opns
      0 :               -> nat
      Succ :   nat      -> nat
      _ eq _ ,
      _ gt _ : nat, nat -> bool
    eqns
      forall m, n: nat
      ofsort bool
        0 eq 0 = true ;
        Succ (m) eq 0 = false ;
        0 eq Succ (n) = false ;
        Succ (m) eq Succ (n) = m eq n ;
  
        0 gt n = false ;
        Succ (m) gt 0 = true ;
        Succ (m) gt Succ (n) = m gt n ;
    endtype
  
  type DecDigit is Boolean, NaturalNumber
    sorts
      decdigit
    opns
      0, 1, 2, 3, 4, 5, 6, 7, 8, 9 : -> decdigit
      map :    decdigit           -> nat
      _ eq _ : decdigit, decdigit -> bool
    eqns
      forall m, n: decdigit
      ofsort nat
        map (0) = 0 ;
        map (1) = Succ (map (0)) ;
        map (2) = Succ (map (1)) ;
        map (3) = Succ (map (2)) ;
        map (4) = Succ (map (3)) ;
        map (5) = Succ (map (4)) ;
        map (6) = Succ (map (5)) ;
        map (7) = Succ (map (6)) ;
        map (8) = Succ (map (7)) ;
        map (9) = Succ (map (8)) ;
      ofsort bool
        m eq n = map (m) eq map (n) ;
    endtype
  
  type SAPs is
    sorts
      SAP
    opns
      sap1: -> SAP
    endtype
  type SDUs is
    sorts
      SDU
    opns
      d1, d2, d3, d4: -> SDU
    endtype
  type SPs is SDUs, Boolean, DecDigit
    sorts
      SP
    opns
      ConReq, ConInd,
      ConResp, ConConf :     -> SP
      DatReq, DatInd :   SDU -> SP
      DisReq, DisInd :       -> SP
  
      SDUof:             SP  -> SDU
  
      isConReq, isConInd,
      isConResp, isConConf,
      isDatReq, isDatInd,
      isDisReq, isDisInd :  SP -> bool
      isCon, isDat, isDis :  SP -> bool
  
      map : SP -> decdigit
    eqns
      forall sp: SP, D: SDU
      ofsort SDU
        SDUof (DatReq (D)) = D ;
        SDUof (DatInd (D)) = D ;
      ofsort decdigit
        map (ConReq)     = 0 ; map (ConInd)     = 1 ;
        map (ConResp)    = 2 ; map (ConConf)    = 3 ;
        map (DatReq (D)) = 4 ; map (DatInd (D)) = 5 ;
        map (DisReq)     = 6 ; map (DisInd)     = 7 ;
      ofsort bool
        isConReq  (sp) = map (sp) eq 0 ;
        isConInd  (sp) = map (sp) eq 1 ;
        isConResp (sp) = map (sp) eq 2 ;
        isConConf (sp) = map (sp) eq 3 ;
        isDatReq  (sp) = map (sp) eq 4 ;
        isDatInd  (sp) = map (sp) eq 5 ;
        isDisReq  (sp) = map (sp) eq 6 ;
        isDisInd  (sp) = map (sp) eq 7 ;
  
        isCon (sp) = isConReq  (sp) or isConInd  (sp) or
                     isConResp (sp) or isConConf (sp) ;
        isDat (sp) = isDatReq  (sp) or isDatInd  (sp) ;
        isDis (sp) = isDisReq  (sp) or isDisInd  (sp) ;
    endtype
  
  type Bits is
    sorts
      bit
    opns
      A0, A1 :     -> bit
      next :   bit -> bit
    eqns
      ofsort bit
        next (A0) = A1 ;
        next (A1) = A0 ;
    endtype
  
  type PDUs is Bits, SDUs
    sorts
      PDU
    opns
      CR, CC :          -> PDU
      DT :     bit, SDU -> PDU
      AK :     bit      -> PDU
      DR, DC :          -> PDU
    endtype
  
  type CMSAPs is
    sorts
      CMSAP
    opns
      cmsap1: -> CMSAP
    endtype
  type CMSPs is PDUs, Boolean, DecDigit
    sorts
      CMSP
    opns
      UnitReq, UnitInd: PDU -> CMSP
  
      SDUof : CMSP -> SDU
      bitof : CMSP -> bit
  
      isUnitReq, isUnitInd: CMSP -> bool
      isCR, isCC,
      isDT, isAK,
      isDR, isDC :          CMSP -> bool
  
      map : CMSP -> decdigit
    eqns
      forall b: bit, D: SDU, pdu: PDU, cmsp: CMSP
      ofsort SDU
        SDUof (UnitReq (DT (b, D))) = D ;
        SDUof (UnitInd (DT (b, D))) = D ;
  
      ofsort bit
        bitof (UnitReq (DT (b, D))) = b ;
        bitof (UnitInd (DT (b, D))) = b ;
        bitof (UnitReq (AK (b))) = b ;
        bitof (UnitInd (AK (b))) = b ;
      ofsort DecDigit
        map (UnitReq (CR))        = 0 ; map (UnitInd (CR))        = 0 ;
        map (UnitReq (CC))        = 1 ; map (UnitInd (CC))        = 1 ;
        map (UnitReq (DT (b, D))) = 2 ; map (UnitInd (DT (b, D))) = 2 ;
        map (UnitReq (AK (b)))    = 3 ; map (UnitInd (AK (b)))    = 3 ;
        map (UnitReq (DR))        = 4 ; map (UnitInd (DR))        = 4 ;
        map (UnitReq (DC))        = 5 ; map (UnitInd (DC))        = 5 ;
      ofsort bool
        isUnitReq (UnitReq (pdu)) = true ;
        isUnitReq (UnitInd (pdu)) = false ;
  
        isUnitInd (UnitReq (pdu)) = false ;
        isUnitInd (UnitInd (pdu)) = true ;
  
        isCR (cmsp) = map (cmsp) eq 0 ;
        isCC (cmsp) = map (cmsp) eq 1 ;
        isDT (cmsp) = map (cmsp) eq 2 ;
        isAK (cmsp) = map (cmsp) eq 3 ;
        isDR (cmsp) = map (cmsp) eq 4 ;
        isDC (cmsp) = map (cmsp) eq 5 ;
    endtype

behaviour
  hide start, retry, kill in
      protocol [a, m, start, retry, kill]
    |[start, retry, kill]|
      timer [start, retry, kill] (N, P)

  where
    process protocol [a, m, s, r, k] : noexit :=
      one_connection [a, m, s, r, k]
      >>
      protocol [a, m, s, r, k]
    
      where
        process one_connection [a, m, s, r, k] : exit :=
          (   upper_association [a] ||| lower_association [m]   )
          |[a, m]|
          coordination [a, m, s, r, k]
        
          where
            process upper_association [a] : exit :=
                a ?sap: SAP ?sp: SP;
                stick [a] (sap)
              [>
                exit
            
              where
                process stick [a] (sap: SAP) : noexit :=
                  a !sap ?sp: SP ;
                  stick [a] (sap)
                  endproc
              endproc
            process lower_association [m] : exit :=
                m ?cmsap: CMSAP ?cmsp: CMSP;
                stick [m] (cmsap)
              [>
                exit
            
              where
                process stick [m] (cmsap: CMSAP) : noexit :=
                  m !cmsap ?cmsp: CMSP;
                  stick [m] (cmsap)
                  endproc
              endproc
            process coordination [a, m, s, r, k] : exit :=
              hide ERROR, Eaction in
                  noticer [ERROR, Eaction]
                |[ERROR, Eaction]|
                ( ( (   connection [a, m, s, r, k, ERROR]
                      >>
                        transfer [a, m, s, r, k, ERROR]
                    )
                    [>
                        disconnection [a, m, s, r, k]
                      []
                        error [a, m, s, r, k, Eaction]
                  )
                  |[a, m]|
                    disc_conditions [a, m] (false)
                )
            
              where
                process connection [a, m, s, r, k, ERROR] : exit :=
                  ( a ?sap: SAP !ConReq ;
                    s ;
                    m ?cmsap: CMSAP !UnitReq (CR) ;
                    TryConnect [a, m, r, k, ERROR]
                    >>
                    a ?sap: SAP !ConConf ;
                    exit
                  )
                  []
                    m ?cmsap: CMSAP !UnitInd (CR) ;
                    a ?sap: SAP !ConInd ;
                    a ?sap: SAP !ConResp ;
                    m ?cmsap: CMSAP !UnitReq (CC) ;
                    exit
                  []
                    m ?cmsap: CMSAP ?cmsp: CMSP [isUnitInd (cmsp) and
                                            not (isCR (cmsp) or isDR (cmsp))] ;
                    connection [a, m, s, r, k, ERROR]
                
                  where
                    process TryConnect [a, m, r, k, ERROR] : exit :=
                        m ?cmsap: CMSAP ?cmsp: CMSP [isUnitInd (cmsp) and
                                                     (isCR (cmsp) or isCC (cmsp))] ;
                        exit
                      []
                        m ?cmsap: CMSAP ?cmsp: CMSP [isUnitInd (cmsp) and
                                        (isDT (cmsp) or isAK (cmsp) or isDC (cmsp))] ;
                        TryConnect [a, m, r, k, ERROR]
                      []
                        r ;
                        m ?cmsap: CMSAP !UnitReq (CR) ;
                        TryConnect [a, m, r, k, ERROR]
                      []
                        k ;
                        ERROR ;
                        stop
                      endproc
                  endproc
                process transfer [a, m, s, r, k, ERROR] : noexit :=
                    sender [a, m, s, r, k, ERROR] (A0)
                  |||
                    receiver [a, m, ERROR] (A0, empty, true)
                
                  where
                    type FIFO is Boolean, SDUs
                      sorts
                        queue
                      opns
                        empty :              -> queue
                        _ + _ :   queue, SDU -> queue
                        first:    queue      -> SDU
                        advance : queue      -> queue
                        hasany :  queue      -> bool
                      eqns
                        forall d, dd: SDU,
                               q: queue
                        ofsort SDU
                          first (empty + d) = d ;
                          first (q + d + dd) = first (q + d) ;
                        ofsort queue
                          advance (empty + d) = empty ;
                          advance (q + d + dd) = advance (q + d) + dd ;
                        ofsort bool
                          hasany (empty) = false ;
                          hasany (q + d) = true ;
                      endtype
                    process sender [a, m, s, r, k, ERROR] (b: bit) : noexit :=
                      a ?sap: SAP ?sp: SP [isDatReq (sp)] ;
                      s ;
                      m ?cmsap: CMSAP !UnitReq (DT (b, SDUof (sp))) ;
                      TrySend [a, m, r, k, ERROR] (b, SDUof (sp))
                      >>
                      sender [a, m, s, r, k, ERROR] (next (b))
                    
                      where
                        process TrySend [a, m, r, k, ERROR] (b: bit, D: SDU) : exit :=
                            m ?cmsap: CMSAP !UnitInd (AK (next (b))) ;
                            exit
                          []
                            r ;
                            m ?cmsap: CMSAP !UnitReq (DT (b, D)) ;
                            TrySend [a, m, r, k, ERROR] (b, D)
                          []
                            k ;
                            ERROR ;
                            stop
                          []
                            m ?cmsap: CMSAP !UnitInd (AK (b)) ;
                            ERROR ;
                            stop
                          endproc
                      endproc
                    process receiver [a, m, ERROR]
                            (b: bit, q: queue, beginning: bool) :
                            noexit :=
                        [beginning]->
                        m ?cmsap: CMSAP !UnitInd (CR) ;
                        m ?cmsap: CMSAP !UnitReq (CC) ;
                        receiver [a, m, ERROR] (b, q, beginning)
                      []
                        [not (beginning)]->
                        m ?cmsap: CMSAP !UnitInd (CR) ;
                        ERROR ;
                        stop
                      []
                        m ?cmsap: CMSAP ?cmsp: CMSP [isUnitInd (cmsp) and
                                                     (isCC (cmsp) or isDC (cmsp))] ;
                        ERROR ;
                        stop
                      []
                        m ?cmsap: CMSAP ?cmsp: CMSP [isUnitInd (cmsp) and
                                                     isDT (cmsp)] ;
                        ( m ?cmsap: CMSAP ?cmsp: CMSP [isUnitInd (cmsp) and
                                                       isDT (cmsp)] ;
                          ERROR ;
                          stop
                        []
                          m ?cmsap: CMSAP !UnitReq (AK (next (bitof (cmsp)))) ;
                          (
                            [bitof (cmsp) = b]->
                            receiver [a, m, ERROR] (next (b), q + SDUof (cmsp), false)
                          []
                            [bitof (cmsp) = next (b)]->
                            receiver [a, m, ERROR] (b, q, false)
                          )
                        )
                      []
                        [hasany (q)]->
                        a ?sap: SAP !DatInd (first (q)) ;
                        receiver [a, m, ERROR] (b, advance (q), beginning)
                      endproc
                  endproc
                process disconnection [a, m, s, r, k] : exit :=
                    a ?sap: SAP !DisReq ;
                    s ;
                    m ?cmsap: CMSAP !UnitReq (DR) ;
                    TryDisconnect [a, m, r, k]
                  []
                    m ?cmsap: CMSAP !UnitInd (DR) ;
                    m ?cmsap: CMSAP !UnitReq (DC) ;
                    ( a ?sap: SAP ?sp : SP [isDis (sp)] ;
                      exit
                    []
                      exit
                    )
                  endproc
                process error [a, m, s, r, k, Eaction] : exit :=
                  Eaction ;
                  a ?sap: SAP ?sp : SP [isDis (sp)] ;
                  s ;
                  m ?cmsap: CMSAP !UnitReq (DR) ;
                  TryDisconnect [a, m, r, k]
                  endproc
                process disc_conditions [a, m] (may_disc: bool) : exit :=
                    a ?sap: SAP ?sp : SP [isCon (sp) or isDat (sp)] ;
                    disc_conditions [a, m] (true)
                  []
                    [may_disc]->
                    a ?sap: SAP ?sp: SP [isDis (sp)] ;
                    anyCMSP [m]
                  []
                    m ?cmsap: CMSAP ?cmsp: CMSP [isUnitInd (cmsp)] ;
                    ( [isDR (cmsp)]->
                      m ?cmsap: CMSAP !UnitReq (DC) ;
                      ( [may_disc]->
                        a ?sap: SAP ?sp : SP [isDis (sp)] ;
                        exit
                      []
                        [not (may_disc)]->
                        exit
                      )
                    []
                      [not (isDR (cmsp))]->
                      disc_conditions [a, m] (may_disc)
                    )
                  []
                    m ?cmsap: CMSAP ?cmsp: CMSP [isUnitReq (cmsp)] ;
                    disc_conditions [a, m] (may_disc)
                
                  where
                    process anyCMSP [m] : exit :=
                        m ?cmsap: CMSAP ?cmsp: CMSP ;
                        anyCMSP [m]
                      []
                        exit
                      endproc
                  endproc
                process noticer [ERROR, Eaction] : exit :=
                    ERROR ;
                    Eaction ;
                    stop
                  [>
                    exit
                  endproc
                process TryDisconnect [a, m, r, k] : exit :=
                    m ?cmsap: CMSAP ?cmsp: CMSP [isUnitInd (cmsp) and
                                                 (isDR (cmsp) or isDC (cmsp))] ;
                    exit
                  []
                    m ?cmsap: CMSAP ?cmsp: CMSP [isUnitInd (cmsp) and
                                                 (isCR (cmsp) or isCC (cmsp) or
                                                  isDT (cmsp) or isAK (cmsp)   )] ;
                    TryDisconnect [a, m, r, k]
                  []
                    r ;
                    m ?cmsap: CMSAP !UnitReq (DR) ;
                    TryDisconnect [a, m, r, k]
                  []
                    k ;
                    exit
                  endproc
              endproc
          endproc
      endproc
    process timer [start, retry, kill] (N, P: nat) : noexit :=
      start ;
      ( count [retry, kill] (0 of nat, N, P)
      [>
        timer [start, retry, kill] (N, P)
      )
    
      where
        process count [retry, kill] (count, max, P: nat) : noexit :=
            [max gt count]->
                                (* timeout P *)
            retry ;
            count [retry, kill] (Succ (count), max, P)
          []
            [max = count]->
                                (* timeout P *)
            kill ;
            stop
          endproc
      endproc
  endspec (* abracadabra_protocol *)
