process InitMaster [cfsreq,cfsans,send,rcv] ( s : Site ) : noexit :=

    Site [cfsreq,cfsans,send,rcv] (s,master,nocopies,norqs)

  endproc


  process MasterSiteProxy [send,rcv] (s:Site) : noexit :=

    send !s !readrq !s;
    MasterSiteProxy [send,rcv] (s)

    []

    send !s !writerq !s;
    MasterSiteProxy [send,rcv] (s)

    []

    rcv !s !readok !s;
    MasterSiteProxy [send,rcv] (s)

    []

    rcv !s !writeok !s;
    MasterSiteProxy [send,rcv] (s)

    []

    rcv !s !invalidate !s;
    MasterSiteProxy [send,rcv] (s)

    []

    (* unreachable branch to prevent CAESAR's warnings about deadlocks; *)
    (* these warnings correspond to the initial phase of the CFS protocol, *)
    (* which is not covered in the model generated *)
    [s ne s (* i.e., false *)] -> 
    rcv !s !firstmaster !s;
    MasterSiteProxy [send,rcv] (s)

  endproc


  process SlaveSiteProxy [send,rcv] (s:Site, other:Site) : noexit :=

    rcv !s !readrq !other;
    ( send !s !readok !other;
      SlaveSiteProxy [send,rcv] (s,other)
      []
      send !s !readrq !other;
      SlaveSiteProxy [send,rcv] (s,other) )

    []

    rcv !s !writerq !other;
    ( send !s !writeok !other;
      SlaveSiteProxy [send,rcv] (s,other)
      []
      send !s !writerq !other;
      SlaveSiteProxy [send,rcv] (s,other) )

    []

    send !s !invalidate !other;
    SlaveSiteProxy [send,rcv] (s,other)

  endproc


  process Site3Proxy [send,rcv] 
      (s:Site, other1:Site, other2:Site) : noexit :=
    MasterSiteProxy [send,rcv] (s)
    |||
    SlaveSiteProxy [send,rcv] (s,other1)
    |||
    SlaveSiteProxy [send,rcv] (s,other2)
  endproc


  process SlaveSendProxy [send] (s:Site) : noexit :=

    send !s !readrq !s;
    SlaveSendProxy [send] (s)

    []

    send !s !writerq !s;
    SlaveSendProxy [send] (s)

  endproc

  process MasterSendProxy [send] (s:Site, other:Site) : noexit :=

    send !s !readok !other;
    MasterSendProxy [send] (s,other)

    []

    send !s !writeok !other;
    MasterSendProxy [send] (s,other)

    []

    send !s !readrq !other;
    MasterSendProxy [send] (s,other)

    []

    send !s !writerq !other;
    MasterSendProxy [send] (s,other)

    []

    send !s !invalidate !other;
    MasterSendProxy [send] (s,other)

  endproc


  process RcvProxy [rcv] (s:Site, other:Site) : noexit :=

    rcv !other !readrq ?z:site;
    RcvProxy [rcv] (s,other)

    []

    rcv !other !writerq ?z:site;
    RcvProxy [rcv] (s,other)

    []

    rcv !other !readok !other;
    RcvProxy [rcv] (s,other)

    []

    rcv !other !writeok !other;
    RcvProxy [rcv] (s,other)

    []

    rcv !other !readrq !other;
    RcvProxy [rcv] (s,other)

    []

    rcv !other !writerq !other;
    RcvProxy [rcv] (s,other)

    []

    rcv !other !invalidate !other;
    RcvProxy [rcv] (s,other)

  endproc


  process Channel3Proxy [send,rcv] 
    (s:Site, other1:Site, other2:Site) : noexit :=
    SlaveSendProxy [send] (s)
    |||
    MasterSendProxy [send] (s,other1)
    |||
    MasterSendProxy [send] (s,other2)
    |||
    RcvProxy [rcv] (s,other1)
    |||
    RcvProxy [rcv] (s,other2)
  endproc


  process Site2with13 [cfsreq,cfsans,send,rcv] : noexit :=
    InitSite [cfsreq,cfsans,send,rcv] (site2)
    |[send,rcv]|
    Site3Proxy [send,rcv] (site2,site1,site3)
  endproc


  process Site3with12 [cfsreq,cfsans,send,rcv] : noexit :=
    InitSite [cfsreq,cfsans,send,rcv] (site3)
    |[send,rcv]|
    Site3Proxy [send,rcv] (site3,site1,site2)
  endproc


  process Master1with23 [cfsreq,cfsans,send,rcv] : noexit :=
    InitMaster [cfsreq,cfsans,send,rcv] (site1)
    |[send,rcv]|
    Site3Proxy [send,rcv] (site1,site2,site3)
  endproc


  process OutputCell1with23 [send,rcv] : noexit :=
    OutputCell [send,rcv] (site1)
    |[send,rcv]|
    Channel3Proxy [send,rcv] (site1,site2,site3)
  endproc


  process OutputCell2with13 [send,rcv] : noexit :=
    OutputCell [send,rcv] (site2)
    |[send,rcv]|
    Channel3Proxy [send,rcv] (site2,site1,site3)
  endproc

  process OutputCell3with12 [send,rcv] : noexit :=
    OutputCell [send,rcv] (site3)
    |[send,rcv]|
    Channel3Proxy [send,rcv] (site3,site1,site2)
  endproc