module cfs_compo (cfs) is

!library

------------------------------------------------------------------------------

-- the following processes are only useful to compositional verification

process MasterSiteProxy [send, rcv: Comm] (s: Site) is
   loop
      alt
         send (s, readrq, s)
      []
         send (s, writerq, s)
      []
         rcv (s, readok, s)
      []
         rcv (s, writeok, s)
      []
         rcv (s, invalidate, s)
      []
         only if s <> s (* i.e., false *) then
            -- 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
            rcv (s, firstmaster, s)
         end if
      end alt
   end loop
end process

process SlaveSiteProxy [send, rcv: Comm] (s, other: Site) is
   loop
      alt
         rcv (s, readrq, other);
         alt
            send (s, readok, other)
         []
            send (s, readrq, other)
         end alt
      []
         rcv (s, writerq, other);
         alt
            send (s, writeok, other)
         []
            send (s, writerq, other)
         end alt
      []
         send (s, invalidate, other)
      end alt
   end loop
end process

process Site3Proxy [send, rcv: Comm] (s, other1, other2: Site) is
   par
      MasterSiteProxy [send, rcv] (s)
   ||
      SlaveSiteProxy [send, rcv] (s, other1)
   ||
      SlaveSiteProxy [send, rcv] (s, other2)
   end par
end process

process SlaveSendProxy [send: Comm] (s: Site) is
   loop
      alt
         send (s, readrq, s)
      []
         send (s, writerq, s)
      end alt
   end loop
end process

process MasterSendProxy [send: Comm] (s, other: Site) is
   loop
      alt
         send (s, readok, other)
      []
         send (s, writeok, other)
      []
         send (s, readrq, other)
      []
         send (s, writerq, other)
      []
         send (s, invalidate, other)
      end alt
   end loop
end process

process RcvProxy [rcv: Comm] (s, other: Site) is
   use s; -- parameter s is never used
   loop
      alt
         rcv (other, readrq, ?any Site)
      []
         rcv (other, writerq, ?any Site)
      []
         rcv (other, readok, other)
      []
         rcv (other, writeok, other)
      []
         rcv (other, readrq, other)
      []
         rcv (other, writerq, other)
      []
         rcv (other, invalidate, other)
      end alt
   end loop
end process

process Channel3Proxy [send, rcv: Comm] (s, other1, other2: Site) is
   par
      SlaveSendProxy [send] (s)
   ||
      MasterSendProxy [send] (s, other1)
   ||
      MasterSendProxy [send] (s, other2)
   ||
      RcvProxy [rcv] (s, other1)
   ||
      RcvProxy [rcv] (s, other2)
   end par
end process

process Site2with13 [cfsreq, cfsans: Call, send, rcv: Comm] is
   par send, rcv in
      InitSite [cfsreq, cfsans, send, rcv] (site2)
   ||
      Site3Proxy [send, rcv] (site2, site1, site3)
   end par
end process

process Site3with12 [cfsreq, cfsans: Call, send, rcv: Comm] is
   par send, rcv in
      InitSite [cfsreq, cfsans, send, rcv] (site3)
   ||
      Site3Proxy [send, rcv] (site3, site1, site2)
   end par
end process

process Master1with23 [cfsreq, cfsans: Call, send, rcv: Comm] is
   par send, rcv in
      InitMaster [cfsreq, cfsans, send, rcv] (site1)
   ||
      Site3Proxy [send, rcv] (site1, site2, site3)
   end par
end process

process InitMaster [cfsreq, cfsans: Call, send, rcv: Comm] (s: Site) is
   Site [cfsreq, cfsans, send, rcv] (s, master, nocopies, norqs)
end process

process OutputCell1with23 [send, rcv: Comm] is
   par send, rcv in
      OutputCell [send, rcv] (site1)
   ||
      Channel3Proxy [send, rcv] (site1, site2, site3)
   end par
end process

process OutputCell2with13 [send, rcv: Comm] is
   par send, rcv in
      OutputCell [send, rcv] (site2)
   ||
      Channel3Proxy [send, rcv] (site2, site1, site3)
   end par
end process

process OutputCell3with12 [send, rcv: Comm] is
   par send, rcv in
      OutputCell [send, rcv] (site3)
   ||
      Channel3Proxy [send, rcv] (site3, site1, site2)
   end par
end process

------------------------------------------------------------------------------

end module