module cfs is

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

type Site is
   site1, site2, site3
   with ==, <>, <, ord
end type

type Val is
   val1, val2
   with ==, <>
end type

type CfsCall is
   read, beginwrite, endwrite
   with ==, <>
end type

type Message is
   readrq, readok, writerq, writeok, invalidate, firstmaster
   with ==, <>
end type

type State is
   master, writing, invalid, valid, waitread, waitwrite, flushrqs,
   forwardrqs, invalwriting, invalinvalid
   with ==, <>
end type

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

type SiteSet is
   set of Site
   with ==, <>, <, (* insert, *) remove, head
end type

function nocopies: SiteSet is
   return {}
end function

function min (x: SiteSet): Site is
   return head (x)
end function

function butmin (x: SiteSet): SiteSet is
      return remove (min (x), x)
end function

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

type Pkt is
   pkt (s: Site, m: Message)
   with ==, <>, get
end type

function site (p: Pkt): Site is
   return p.s
end function

function msg (p: Pkt): Message is
   return p.m
end function

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

type PktList is
   !card 31
   list of Pkt
   with ==, <>, head, tail, append
end type

function + (x: PktList, x_1: Pkt): PktList is
   return append (x_1, x)
end function

function First (x: PktList): Pkt is
   return head (x)
end function

function ButFirst (x: PktList): PktList is
   return tail (x)
end function

function norqs: PktList is
   return {}
end function

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

type ValArray is
   array [0 .. 2 (* i.e., Site *)] of Val
end type

function setf (x_0: Site, y: Val, z: ValArray): ValArray is
   var z2: ValArray in
      z2 := z;
      z2 [ord (x_0)] := y;
      return z2
   end var
end function

function get (x_0: Site, z: ValArray): Val is
   return z [ord (x_0)]
end function

function init: ValArray is
   return ValArray (val1, val1, val1)
end function

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

channel Call is
   (s: Site, c: CfsCall)
end channel

channel Comm is
   (s1: Site, m: Message, s2: Site)
end channel

channel ReadWrite is
   (s: Site, v: Val)
end channel

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

process MAIN [cfsreq, cfsans: Call, send, rcv: Comm, read, write: ReadWrite] is
   par read, write, cfsreq, cfsans in
      par
         GeneralUser [read, write, cfsreq, cfsans] (site1)
      ||
         GeneralUser [read, write, cfsreq, cfsans] (site2)
      ||
         GeneralUser [read, write, cfsreq, cfsans] (site3)
      end par
   ||
      par send, rcv in
         par
            InitSite [cfsreq, cfsans, send, rcv] (site1)
         ||
            InitSite [cfsreq, cfsans, send, rcv] (site2)
         ||
            InitSite [cfsreq, cfsans, send, rcv] (site3)
         end par
      ||
         par send in
            rcv (?any Site, firstmaster, ?any Site);
            par
              OutputCell [send, rcv] (site1)
            ||
              OutputCell [send, rcv] (site2)
            ||
              OutputCell [send, rcv] (site3)
            end par
         ||
            InitMemory [read, write, send]
         end par
      end par
   end par
end process

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

process GeneralUser [read, write: ReadWrite, cfsreq, cfsans: Call] (s: Site) is
   loop
      alt
         cfsreq (s, read);
         cfsans (s, read);
         loop ReadingUser in
            alt
               read (s, ?any Val)
            []
               break ReadingUser
            end alt
         end loop
      []
         cfsreq (s, beginwrite);
         cfsans (s, beginwrite);
         loop WritingUser in
            alt
               read (s, ?any Val)
            []
               write (s, ?any Val)
            []
               cfsreq (s, endwrite);
               cfsans (s, endwrite);
               break WritingUser
            end alt
         end loop
      end alt
   end loop
end process

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

process OutputCell [send, rcv: Comm] (s: Site) is
   var m: Message, s1: Site in
      loop
         send (s, ?m, ?s1);
         rcv (?any Site, m, s1)
      end loop
   end var
end process

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

process InitMemory [read, write: ReadWrite, send: Comm] is
   var mems: ValArray, m: Message, s, s1, s2: Site, v: Val in
      mems := init of ValArray;
      loop
         alt
            s:= any Site;
            read (s, get (s, mems))
         []
            write (?s, ?v);
            mems := setf (s, v, mems)
         []
            send (?s1, ?m, ?s2);
            if (m == readok) or (m == writeok) then
               mems := setf (s2, get (s1, mems), mems)
            end if
         end alt
      end loop
   end var
end process

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

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

process Site [cfsreq, cfsans: Call, send, rcv: Comm] (s: Site,
          in var state: State, in var copies: SiteSet, in var rqs: PktList) is
   loop
      alt
         only if (state == master) or (state == valid) or (state == invalid) then
            cfsreq (s, read);
            if (state == master) or (state == valid) then
               cfsans (s, read)
            else
               -- assert state == invalid
               alt
                  send (s, readrq, s);
                  state := waitread
               []
                  rcv (s, firstmaster, s);
                  cfsans (s, read);
                  state := master
               end alt
            end if
         end if
      []
         only if (state == master) or (state == valid) or (state == invalid) then
            cfsreq (s, beginwrite);
            if state == master then
               cfsans (s, beginwrite);
               state := invalwriting
            elsif state == valid then
               send (s, writerq, s);
               state := waitwrite
            else
               -- assert state == invalid
               alt
                  send (s, writerq, s);
                  state := waitwrite
               []
                  rcv (s, firstmaster, s);
                  cfsans (s, beginwrite);
                  state := writing
               end alt
            end if
         end if
      []
         only if state == writing then
            cfsreq (s, endwrite);
            cfsans (s, endwrite);
            state := flushrqs
         end if
      []
         only if (state == master) or (state == writing) then
            var s1: Site in
               rcv (s, readrq, ?s1);
               if state == master then
                  send (s, readok, s1);
                  copies := insert (s1, copies)
               else
                  -- assert state == writing
                  rqs := rqs + pkt (s1, readrq)
               end if
            end var
         end if
      []
         only if (state == master) or (state == writing) then
            var s1: Site in
               rcv (s, writerq, ?s1);
               if state == master then
                  send (s, writeok, s1);
                  state := invalinvalid
               else
                  -- assert state == writing
                  rqs := rqs + pkt (s1, writerq)
               end if
            end var
         end if
      []
         only if state == waitread then
            rcv (s, readok, s);
            cfsans (s, read);
            state := valid
         end if
      []
         only if state == waitwrite then
            rcv (s, writeok, s);
            cfsans (s, beginwrite);
            state := writing
         end if
      []
         only if (state == valid) or (state == master) or (state == writing) or
         (state == waitwrite) or (state == waitread) or(state == invalid) then
            rcv (s, invalidate, s);
            if state == valid then
               state := invalid
            end if
         end if
      []
         only if state == flushrqs then
            if rqs <> norqs then
               case msg (first (rqs)) of Message in
                  readrq ->
                     send (s, readok, site (first (rqs)));
                     state := flushrqs;
                     copies := insert (site (first (rqs)), copies);
                     rqs := butfirst (rqs)
               |  writerq ->
                     send (s, writeok, site (first (rqs)));
                     state := forwardrqs;
                     rqs := butfirst (rqs)
               |  any ->
                     stop
               end case
            else
               -- assert rqs == norqs;
               state := master
            end if
         end if
      []
         only if state == forwardrqs then
            if copies <> nocopies then
               send (s, invalidate, min (copies));
               state := forwardrqs;
               copies := butmin (copies)
            elsif rqs <> norqs then
               send (s, msg (first (rqs)), site (first (rqs)));
               state := forwardrqs;
               rqs := butfirst (rqs)
            else
               state := invalid
            end if
         end if
      []
         only if state == invalwriting then
            if copies <> nocopies then
               send (s, invalidate, min (copies));
               state:= invalwriting;
               copies := butmin (copies)
            else
               state := writing
            end if
         end if
      []
         only if state == invalinvalid then
            if copies <> nocopies then
               send (s, invalidate, min (copies));
               state := invalinvalid;
               copies := butmin (copies)
            else
               state := invalid
            end if
         end if
      end alt
   end loop
end process

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

-- 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