/*
 * Copyright (c) 1996 by Satish Chandra, Brad Richards, Mark D. Hill, 
 * James R. Larus, and David A. Wood.
 *
 * Teapot is distributed under the following conditions:
 * 
 *     You may make copies of Teapot for your own use and modify those copies.
 * 
 *     All copies of Teapot must retain our names and copyright notice.
 * 
 *     You may not sell Teapot or distributed Teapot in conjunction with a
 *     commercial product or service without the expressed written consent of
 *     the copyright holders.
 * 
 * THIS SOFTWARE IS PROVIDED ``AS IS'' AND WITHOUT ANY EXPRESS OR IMPLIED
 * WARRANTIES, INCLUDING, WITHOUT LIMITATION, THE IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.
 * 
 */


Invariant "client caches addr --> mgr thinks client caches addr"
  Forall client : NODE Do
  Forall mgr : NODE Do
  Forall addr : ID Do
    -- 
    -- Invarient only holds for one manager for each addr.
    --
    (HomeMap[addr] != mgr)
    |
    --
    -- And it only holds for real clients. Ignore when
    -- the "client" is really the mgr or if the "client"
    -- is the SS.
    --
    (client = mgr) | (client = SSMap[addr])
    |
    --
    -- Ignore transient states.
    --
    (IsTransient(Nodes[mgr].Dram[addr].State))
    |
    (IsTransient(Nodes[client].Dram[addr].State))
    |
    --
    -- Either the client is not caching the block 
    -- OR
    -- the manager knows the client is caching the block.
    -- 
    ( (Nodes[client].Dram[addr].State = Cache_Inv)
      |
      ( (Nodes[mgr].Dram[addr].State != Home_Idle)
        &
	( (InSharers(Nodes[mgr].Dram[addr], client))
          |
          (Nodes[mgr].Dram[addr].Owner = client)
        )
      )
    )
  End
  End
  End; -- client caches addr --> mgr thinks client caches addr

Invariant "Blocks cannot be both owned and shared"
  Forall mgr : NODE Do
  Forall addr: ID Do
    -- 
    -- Invariant is for managers info.
    --
    (HomeMap[addr] != mgr)
    |
    --
    -- Ignore transient states.
    --
    (IsTransient(Nodes[mgr].Dram[addr].State))
    |
    --
    -- The invariant.
    --
    !(Nodes[mgr].Dram[addr].IsOwned
      & (Nodes[mgr].Dram[addr].NumSharers > 0)
     )
  End
  End; -- "Blocks cannot be both owned and shared"

Invariant "A client cannot have write permission unless mgr thinks it owns"
  Forall client : NODE Do
  Forall mgr : NODE Do
  Forall addr : ID Do
    -- 
    -- Invarient only holds for one manager for each addr.
    --
    (HomeMap[addr] != mgr)
    |
    --
    -- And it only holds for real clients. Ignore when
    -- the "client" is really the mgr or if the "client"
    -- is the SS.
    --
    (client = mgr) | (client = SSMap[addr])
    |
    --
    -- Ignore transient states.
    --
    (IsTransient(Nodes[mgr].Dram[addr].State))
    |
    (IsTransient(Nodes[client].Dram[addr].State))
    |
    --
    -- client has write permission --> mgr knows client owns it
    --
    (Nodes[client].AccCtrl[addr] != Blk_Writable)
    |
    (Nodes[mgr].Dram[addr].Owner = client)
  End    
  End
  End; -- "A client cannot have write permission unless mgr thinks it owns"

Invariant "Same node cannot be both SS and Mgr"
  Forall addr : ID Do
    HomeMap[addr] != SSMap[addr]
  End;

  
Invariant "Dummy"
	true;

	

