module main[type symmetric Data,
            type symmetric CacheRange
            init_owner: CacheRange] =
begin
 datatype trans = read | none

 type Bus = { data: Data,
              trans: trans,
              master: CacheRange }

 module cache[i: CacheRange]
	     (bus: Bus) =
 begin
  datatype State = invalid | exclusive
  datatype Line = { state: State, data: Data }

  stateVar line: Line
  stateVar req: trans

  req := anyvalue

  init(line) := fn x => anyvalue with 
      [ state = if i=init_owner then exclusive else invalid endif ]

  case bus.trans of
      read =>
        if bus.master = i then -- I'm the master
          next(line) := { state = exclusive, data = bus.data }
        else next(line) := anyvalue with [ state = invalid ] endif
      none => noop
  endcase

  export all
 end -- cache

 module bus =
  begin
   stateVar bus: Bus

   var d: Data
   var i: CacheRange

   module c[i] = cache[i](bus)

   let val line = fn i => c[i].line
       val req  = fn i => c[i].req
   in
     bus.master :=anyvalue
     bus.trans := req(bus.master)
     bus.data := choose d: (exists i: line(i).state = exclusive
                                  & line(i).data = d)
   end -- let
   module system = bus || (sync i: c[i])
   export all
 end -- bus

 var i,j: CacheRange

 theorem coherence =
   system |= ag(exists i: c[i].line.state = exclusive
                  & forall j: i != j => c[i].line.state = invalid)

 statevar the_data: Data
 init(the_data) := c[init_owner].line.data
 -- and the_data never changes

 theorem data_thm =
   system |= ag(forall i: c[i].line.state = exclusive
                     => c[i].line.data = the_data)

end -- main

-- |CacheRange| = 3 (the master, the exclusive, and the other)
-- |Data| = 4+1 (the 3 caches have their copies, plus the initial data,
--               plus "error")