option EnumUnknowns=1,BddSift=1;

scalarset Proc undefined;
scalarset Data 0..1;

typedef UniType { Empty, Get, GetX, NAK, Put, PutX };

/* A message structure */

typedef msg struct{
  proc : Proc;
  mtype : { Empty, Get, GetX, NAK, Put, PutX, WB, ShWB, FAck };
  data : Data;
}

typedef Uni struct{
  proc : Proc;
  mtype : UniType;
  data : Data;
  init(mtype) := Empty;
}

typedef Header struct{
  pending : boolean;
  local : boolean;
  dirty : boolean;
  head : boolean;
  hptr : Proc;
  list : boolean;
  real : array Proc of boolean;
  upgrade : boolean;	
  shlist : array Proc of boolean;
  init(pending) := 0;
  init(local) := 0;
  init(dirty) := 0;
  init(head) := 0;
  init(list) := 0;
  init(real) := [0:i in Proc];
  init(shlist) := [0:i in Proc];
  init(upgrade) := 0;
}

typedef CacheState { invalid, shared, exclusive };
typedef WaitType { none, get, getX };
typedef CacheLine struct{
    wait : WaitType;
    invmarked : boolean;
    state : CacheState;
    data : Data;
  data_src : Proc; /* aux var */
  init(wait) := none;
  init(invmarked) := 0;
  init(state) := invalid;
}

typedef UniNet array Proc of Uni;
typedef WBNet struct{
  proc:Proc;
  mtype : {Empty,WB};
  data:Data;
  init(mtype) := Empty;
}

typedef ShWBNet struct{
  proc:Proc;
  mtype : {Empty,ShWB,FAck};
  data:Data;
  init(mtype) := Empty;
}

typedef InvType { Empty, Inv, InvAck };
typedef InvNet  array Proc of InvType;

typedef RPNet array Proc of boolean;

typedef Processor array Proc of CacheLine;
 
typedef gstate struct{
  cache: Processor;
  mem: Data;
  dir: Header;
  wbnet: WBNet;
  shwbnet : ShWBNet;
  nakc: boolean;
  unet: UniNet;
  invnet: InvNet;
  rp: RPNet;
  error:boolean resolve;
  init(nakc) := 0;
  init(invnet) := [Empty:i in Proc];
  init(rp) := [0:i in Proc];
  init(error) := 0;
}


#if 0
#endif

#define SendGet(src, dst, t) { next(unet[src].proc) := dst;  next(unet[src].mtype) := t;  next(unet[src].data) := undefined; if(dst ~= home)  next(fwd_get) := t; }

#define SendPut(src, dst, t, d) {\
  next(unet[dst].proc) := src;\
  next(unet[dst].mtype) :=t;\
  next(unet[dst].data) :=d;\
}

#define SendWB(src, dst, t, d) { next(wbnet.proc) := src; next(wbnet.mtype) :=t; next(wbnet.data) :=d;}
#define SendShWB(src, dst, t, d) { next(shwbnet.proc) := src; next(shwbnet.mtype) :=t; next(shwbnet.data) :=d;}



#define ConsumeUnet(src) {\
 next(unet[src].mtype) := Empty;\
}

#define ConsumeWBnet(src) {\
 next(wbnet.mtype) := Empty;\
}

#define ConsumeShWBnet(src) {\
 next(shwbnet.mtype) := Empty;\
}

#define CC_Inv(proc) {\
  if(cache[proc].wait=get){\
    next(cache[proc].invmarked) := 1;\
    next(cache[proc].state) := invalid;\
  }\
  else{\
    next(cache[proc].state):= invalid;\
  }\
}

  /* O.K. after here */

#define CC_Put(proc, d) {\
  if(cache[proc].invmarked){\
    next(cache[proc].wait):= none;\
    next(cache[proc].invmarked):= 0;\
    next(cache[proc].state):= invalid;\
  }\
  else {\
    next(cache[proc].wait):= none;\
    next(cache[proc].data):= d;\
    next(cache[proc].state):= shared;\
  }\
}

#define CC_PutX(proc, d) {\
    next(cache[proc].data):=d;\
    next(cache[proc].wait):=none;\
    next(cache[proc].invmarked):=0;\
    next(cache[proc].state):=exclusive;\
}

#define CC_UpAck(proc) {\
  if(cache[proc].invmarked){\
    next(cache[proc].wait):= none;\
    next(cache[proc].invmarked):= 0;\
    next(cache[proc].state):= invalid;\
  }\
  else{\
    next(cache[proc].wait):= none;\
    next(cache[proc].state):= exclusive;\
  }\
}


#define SendInvs(){\
  forall(i in Proc)\
    next(invnet[i]) :=\
      (i ~= home & (dir.list & dir.shlist[i] | dir.hptr=i)) ? Inv : Empty;\
}

#define SendInvsEx(ex){\
  forall(i in Proc)\
    next(invnet[i]) :=\
      (i ~= home & i ~= ex\
       & (dir.list & dir.shlist[i] | dir.hptr=i)) ? Inv : Empty;\
}

module main(){

  /* The abstract model */

  m,m1 : Data;
  store : boolean resolve 0;
  store_data : Data;

  /* aux var */

  real_owner : Proc;
  init(real_owner) := home;
  requester : Proc;
  collecting : boolean;
  init(collecting) := 0;
  last_WB : Proc;
  shwb_src : Proc;
  last_writer : Proc;
  fwd_get : {Get,GetX,Empty};
  init(fwd_get) := Empty;
  fwd_src : Proc;
  last_invack, last_other_invack : Proc;

  /* The protocol model */

  /* Define the home processor (breaks symmetry) */

  home : Proc;
#ifdef MAKE_FINITE
  home := 0;
#else
  next(home) := home;
#endif
  
  self : gstate;
  init(dir.hptr) := home;
  
  /* Here are the protocol rules */

  rule : {PI_Local_Get, PI_Remote_Get,PI_Local_GetX,PI_Remote_GetX,PI_Local_PutX,PI_Remote_PutX,PI_Local_Replace,PI_Remote_Replace,NI_NAK,
	      NI_NAK_Clear,NI_Local_Get,NI_Remote_Get,NI_Local_GetX,NI_Remote_GetX,NI_Local_Put,NI_Remote_Put,NI_Local_PutXAcksDone,
	      NI_Remote_PutX,NI_Inv,NI_InvAck,NI_WB,NI_FAck,NI_ShWB,NI_Replace,Store};
  src,dst : Proc;
  
  dst_dirty : boolean;
  dst_dirty := cache[dst].state = exclusive;

  rp_src : boolean;
  rp_src := rp[src];
  src_invmarked : boolean;
  src_invmarked := cache[src].invmarked;
  src_invack : boolean;
  src_invack := invnet[src]=InvAck & dir.real[src];
  some_others_left : boolean;
  some_others_left := |[dir.real[i] & i ~= src : i in Proc];
  not_need_invs : boolean;
  not_need_invs := (src_eq_hptr  & (~ |[dir.shlist[i] & i~=src : i in Proc]));
  dst_eq_proc : boolean;
  dst_eq_proc := mi.proc=dst;
  dst_eq_src : boolean;
  dst_eq_src := dst = src;
  src_eq_hptr : boolean;
  src_eq_hptr := src=dir.hptr;
  cache_dst_data : Data;
  cache_dst_data := cache[dst].data;
  
  mi : msg; /* the incoming message */
  min : Proc;
  unetin : boolean;
  mi := unet[min];

  default unetin := 0;
  in switch(rule){
    PI_Local_Get:{
      if(cache[home].state=invalid & cache[home].wait=none
	 & ~dir.pending & dir.dirty){
	  next(dir.pending) := 1;
	  next(collecting) := 0;
	  next(cache[home].wait) := get;
	  SendGet(home,dir.hptr,Get);
	  next(requester) := home;
      }
      else if(cache[home].state=invalid & cache[home].wait=none
	      & ~dir.pending & ~dir.dirty){
	  next(dir.local) := 1;
	  CC_Put(home, mem);
      }
    }      
    PI_Remote_Get:{
      if(cache[src].state=invalid & cache[src].wait=none & src ~= home){
	  next(cache[src].wait) := get;
	  SendGet(src, home, Get);
      }
    }
    PI_Local_GetX:{
      if((cache[home].state=invalid | cache[home].state=shared)
	 & cache[home].wait=none
	 & ~ dir.pending & dir.dirty){
	next(dir.pending ):= 1;
        next(collecting) := 0;
	next(cache[home].wait ):= getX;
	  SendGet(home, dir.hptr, GetX);
	  next(requester) := home;
      }
      else if(( cache[home].state=invalid | cache[home].state=shared )
	      & cache[home].wait=none 
	      & ~ dir.pending & ~ dir.dirty){
	  default{
	    next(dir.local ):= 1;
	    next(dir.dirty ):= 1;
	    next(real_owner) := home;
	      CC_PutX( home, mem);
	  }
	  in if(~ dir.head){}
	  else{
	    SendInvs();
	    next(collecting) := 1;
	    next(m1) := m;
	    next(last_other_invack) := dir.hptr;
	    next(dir.pending ):= 1;
	    next(dir.head ):= 0;
	    next(dir.shlist):= [0:i in Proc];
	    next(dir.list):=0;
              /* dir.real:=card({p:Proc| invnet(s3)(p)=Inv}) ] ]  can't do this, see below */
	      forall(i in Proc)
		next(dir.real[i]) :=
		  i ~= home & (dir.list & dir.shlist[i] | dir.hptr=i);
	  }
      }
    }       

    PI_Remote_GetX:{
      if(cache[src].state=invalid & cache[src].wait=none & src ~= home){
	next(cache[src].wait ):= getX;
	  SendGet(src, home, GetX);
      }
    }

    PI_Local_PutX:{
      if(cache[home].state=exclusive & cache[home].wait=none){
	  if(dir.pending){
	    next(dir.dirty ):= 0;
	    next(mem):= cache[home].data;
	    next(last_WB) := home;
	    next(cache[home].state ):= invalid;
	  }
	  else{
	    next(dir.local ):= 0;
	    next(dir.dirty ):= 0;
	    next(mem):= cache[home].data;
	    next(last_WB) := home;
	    next(cache[home].state ):= invalid;
	  }
      }
    }
    PI_Remote_PutX:{
      if(dst_dirty & /* cache[dst].wait=none & */ dst ~= home){
	next(cache[dst].state ):= invalid;
	SendWB(dst,home,WB,cache_dst_data);
	/* next(real_owner) := home; */
      }
    }
    PI_Local_Replace:{
      if(cache[home].state=shared & cache[home].wait=none){
	next(dir.local ):= 0;
	next(cache[home].state ):= invalid;
      }
    }
    PI_Remote_Replace:{
      if(cache[src].state=shared & cache[src].wait=none & src ~= home){
	next(cache[src].state ):= invalid;
	next(rp[src]):=1;
      }
    }

    NI_NAK:{
      if(unet[dst].mtype=NAK){
	  ConsumeUnet(dst);
	  next(cache[dst].wait ):= none;
	  next(cache[dst].invmarked ):= 0;
      }
    }

    NI_NAK_Clear:{
      if(nakc){
	next(dir.pending ):= 0;
	next(nakc ):= 0;
      }
    }

    NI_Local_Get:{
      unetin := 1; min :=  src;
      if(mi.mtype=Get & home~=src
	 & mi.proc=home & ~ rp_src){
	  if(dir.pending | 
	     (dir.dirty & dir.local & cache[home].state~=exclusive)){
	      SendPut(home, src, NAK, undefined);
	  } else if(dir.dirty & ~dir.local){
	      if(src_eq_hptr){
		  SendPut(home, src, NAK, undefined);
	      } else {
		next(dir.pending):=1;
         	  next(collecting) := 0;
		  SendGet(src, dir.hptr, Get);
		  next(requester) := src;
	      }
	  }
	  else if(mi.mtype=Get & home~=src
		  & mi.proc=home & ~ dir.pending & 
		  ( ~ dir.dirty | ( dir.local &
				    cache[home].state=exclusive ))
		  & ~ rp_src & ~src_invmarked){
	    if(dir.dirty){
	      next(dir.dirty ):= 0;
	      next(dir.head ):= 1;
	      next(dir.hptr):=src;
	      next(mem):= cache[home].data;
	      next(last_WB) := home;
	      next(cache[home].state ):= shared;
	      SendPut(home, src, Put, cache[home].data);
	    }
	    else {
	      SendPut(home, src, Put, mem);
	      if(dir.head){
		next(dir.list):=1;
		next(dir.shlist[src] ):= 1;
		next(dir.real ):= [((i = src) ? 1 : dir.shlist[i]) : i in Proc];
	      }
	      else{ 
		next( dir.head ):= 1;
		next(dir.hptr ):= src;
	      }
	    }
	  }
	  else if(mi.mtype=Get & home~=src
		  & mi.proc=home & ~ dir.pending 
		  & ( ~ dir.dirty | ( dir.local &
				      cache[home].state=exclusive ))
		  & ~ rp_src & src_invmarked){
	    if(dir.dirty){
	      next(dir.dirty ):= 0;
	      next(dir.head ):= 1;
	      next(dir.hptr):=src;
	      next(mem):= cache[home].data;
	      next(last_WB) := home;
	      next(cache[home].state ):= shared;
	      SendPut(home, src, Put, cache[home].data);
	    }
	    else{
	      SendPut(home, src, Put, mem);
	      if(dir.head) {
		next(dir.list):=1;
		next(dir.shlist[src] ):= 1;
		next(dir.real ):= [((i = src) ? 1 : dir.shlist[i]) : i in Proc];
	      } else {
		next(dir.head ):= 1;
		next(dir.hptr ):= src;
	      }
	    }
	  }
      }
    }

    NI_Remote_Get:{
      unetin := 1; min :=  src;
      if(mi.mtype=Get & ~dst_eq_src
	 & dst_eq_proc & dst~=home 
	 & ~dst_dirty /* cache[dst].state~=exclusive */){
	next(fwd_get) := Empty;
	next(fwd_src) := src;
	default {ConsumeUnet(src);}
	in {
	  next(nakc ):= 1;
	  SendPut(dst, src, NAK, undefined);
	}
      }
      else if(mi.mtype=Get & ~dst_eq_src
	      & dst_eq_proc & dst~=home 
	      & dst_dirty /* cache[dst].state=exclusive */
	      & ~ src_invmarked){
	next(cache[dst].state ):= shared;
	  next(fwd_get) := Empty;
	  next(fwd_src) := src;
	  default {SendPut(dst, src, Put, cache_dst_data);}
	  in if( src~=home ) {
	      SendShWB(src, home, ShWB, cache_dst_data);
	      next(real_owner) := home;
	      next(shwb_src) := dst;
	  }
      }
      else if(mi.mtype=Get & ~dst_eq_src
	      & dst_eq_proc & dst~=home 
	      & dst_dirty /* cache[dst].state=exclusive */
	      & src_invmarked){
	next(cache[dst].state ):= shared;
	next(fwd_get) := Empty;
	next(fwd_src) := src;
	  default {SendPut(dst, src, Put, cache_dst_data);}
	  in if( src~=home ) {
	      SendShWB(src, home, ShWB, cache_dst_data);
	      next(real_owner) := home;
	      next(shwb_src) := dst;
	  }
      }
    }
    NI_Local_GetX:{
      unetin := 1; min :=  src;
      if(mi.mtype=GetX & home~=src & mi.proc=home){
	  if( dir.pending ) {
	      SendPut(home, src, NAK, undefined);
	  } else if( dir.dirty ) {
	      if( dir.local ) {
		  if( cache[home].state=exclusive ) {
		  } else {
		      SendPut(home, src, NAK, undefined);
		  }
	      } else if( src_eq_hptr ) {
		  SendPut(home, src, NAK, undefined);
	      } else {
		next(dir.pending):=1;
               	  next(collecting) := 0;
		  SendGet(src, dir.hptr, GetX);
		  next(requester) := src;
	      }
	  }
	  else if(mi.mtype=GetX & home~=src
		  & mi.proc=home & ~ dir.pending &
		  ( dir.dirty -> dir.local & cache[home].state=exclusive)){
	    if( dir.dirty ) {
	      next(dir.local ):= 0;
	      next(dir.dirty):=1;
	      next(dir.head ):= 1;
	      next(dir.hptr):=src;
	      next(dir.list):=0;
	      next(dir.real):=[0:i in Proc];
	      next(dir.shlist ):= [0:i in Proc];
	      next(cache[home].state ):= invalid;
	      next(unet[src].proc):=home;
	      next(unet[src].mtype):= PutX;
	      next(unet[src].data):=cache[home].data;
	    } else if( ~ dir.head | not_need_invs) {
	      next(dir.local ):= 0;
	      next(dir.dirty):=1;
	      next(dir.head ):= 1;
	      
	      next(dir.hptr):=src;
	      next(dir.list):=0;
	      next(dir.real):=[0:i in Proc];
	      next(dir.shlist ):= [0:i in Proc];
	      next(unet[src].proc):=home;
	      next(unet[src].mtype):= PutX;
	      next(unet[src].data):=mem;
	      next(real_owner) := src;
	      default next(cache[home].state ):= invalid;
	      in if( dir.local ) {
		CC_Inv(home);
	      } else {
	      }
	    } else {
	      SendInvsEx(src);
	      next(collecting) := 1;
	      next(m1) := m;
	      next(last_other_invack) := (dir.hptr ~= src) ? dir.hptr : {i  : i in Proc, dir.shlist[i] & i~=src}; 
	      next(dir.local ):= 0;
	      next(dir.dirty):=1;
	      next(dir.head ):= 1; 
	      next(dir.hptr):=src;
	      next(dir.list):=0;
	      next(dir.shlist ):= [0:i in Proc];
	      next(dir.pending ):= 1;
	      /*real:=card({p:Proc| invnet(si)(p)=Inv}) ]; */
	      forall(i in Proc)
		next(dir.real[i]):=
		(i ~= home & i ~= src
		 & (dir.list & dir.shlist[i] | dir.hptr=i));
              next(unet[src].proc):=home;
	      next(unet[src].mtype):= PutX;
	      next(unet[src].data):=mem;
	      next(real_owner) := src;
	      if( dir.local ) {
		CC_Inv(home);
	      } else {
	      }
	    }
	  }
      }
    }

    NI_Remote_GetX:{
      unetin := 1; min :=  src;
      if(mi.mtype=GetX & ~dst_eq_src
	 & dst_eq_proc & dst~=home 
	 &  ~dst_dirty /* cache[dst].state~=exclusive */ ){
	next(fwd_get) := Empty;
	next(fwd_src) := src;
	default {ConsumeUnet(src);}
	in {
	  next(nakc ):= 1;
	  SendPut(dst, src, NAK, undefined);
	}
      }
      else if(mi.mtype=GetX & ~dst_eq_src
	      & dst_eq_proc & dst~=home 
	      &  dst_dirty /* cache[dst].state=exclusive */ ){
	next(cache[dst].state ):= invalid;
	next(fwd_get) := Empty;
	next(fwd_src) := src;
	  default {SendPut(dst, src, PutX, cache_dst_data); next(real_owner) := src; }
	  in if( src~=home ) {
	      SendShWB(src, home, FAck, undefined);
	  } else {
	  }
      }
    }
    NI_Local_Put:{
      unetin := 1; min :=  home;
      if(dst = home & mi.mtype=Put){
	  ConsumeUnet(home);
	  next(dir.pending ):= 0;
	  next(dir.dirty ):= 0;
	  next(dir.local ):= 1; 
	  next(mem ):= mi.data;
	  next(last_WB) := mi.proc;
	  CC_Put(home, mi.data);
	  next(cache[home].data_src):= mi.proc;
      }
    }
    NI_Remote_Put:{
      unetin := 1; min :=  dst;
      if(mi.mtype=Put & dst~=home){
	  ConsumeUnet(dst);
	  CC_Put(dst, mi.data);
	  next(cache[dst].data_src):= mi.proc;
      }
    }
    NI_Local_PutXAcksDone:{
      unetin := 1; min :=  home;
      if(dst = home & mi.mtype=PutX){
	  ConsumeUnet(home);
	  next(dir.pending ):= 0;
	  next(dir.head ):= 0;
	  next(dir.local ):= 1;
	  CC_PutX(home, mi.data);
	  next(cache[home].data_src):= mi.proc;
      }
    }
    NI_Remote_PutX:{
      unetin := 1; min :=  dst;
      if(mi.mtype=PutX & dst~=home & cache[dst].wait = getX){
	  ConsumeUnet(dst);
	  CC_PutX(dst, mi.data);
	  next(cache[dst].data_src):= mi.proc;
      }
    }
    NI_Inv:{
      if(invnet[dst]=Inv & dst~=home){
	next(invnet[dst] ):= InvAck;
	  CC_Inv(dst);
      }
    }
    NI_InvAck:{
      if(dir.pending & src_invack & some_others_left & src~=home){
	next(invnet[src]):= Empty;
	next(dir.real[src] ):= 0;
	next(last_invack) := src;
	next(last_other_invack) := {i : i in Proc, dir.real[i] & i ~= src};
      }
      else if(dir.pending & src_invack & src~=home){
	next(dir.pending):=0;
	next(collecting) := 0;
	next(m1) := undefined;
	next(invnet[src] ):= Empty; 
	next(dir.real[src]):=0;
	next(last_invack) := src;
	  if( dir.local & ~ dir.dirty ) {
	    next(dir.local ):= 0;
	  }
      }
    }

    NI_WB:{
      if(wbnet.mtype=WB){
	ConsumeWBnet(home);
	next(dir.dirty ):= 0;
	next(dir.head):=0;
	next(mem):= wbnet.data;
	next(last_WB) := wbnet.proc;
      }
    }
    NI_FAck:{
      if(shwbnet.mtype=FAck ){
	  ConsumeShWBnet(home);
	  next(dir.pending):=0;
	  if( dir.dirty ) {
	    next(dir.hptr):= shwbnet.proc;
	  } else {
	  }
      }
    }

    NI_ShWB:{
      if(shwbnet.mtype=ShWB){
	  ConsumeShWBnet(home);
	  next(dir.pending):=0;
	  next(dir.dirty):=0;
	  next(dir.list):= 1; 
	  next(dir.shlist[shwbnet.proc] ):= 1;
	  next(dir.real ):= [((i = shwbnet.proc) ? 1 : dir.shlist[i]) : i in Proc];
	  next(mem):=shwbnet.data;
	  next(last_WB) := shwb_src;
      }
    }

    NI_Replace:{
      if(rp_src){
	next(rp[src] ):= 0;
	  if( dir.list ) {
	    next(dir.shlist[src] ):= 0;
	    next(dir.real[src] ):= 0;
	  }
      }
    }
      
    Store: {
        store := dst_dirty;
	if(store){
	  next(m) := store_data;
	  next(cache[dst].data) := store_data;
	  next(last_writer) := dst;
	}
    }
  }



  /* witness function */

  init(m) := mem;

  /* refinement relations */

  forall(i in Proc){
    observable[i] : boolean;
    observable[i] := ~(dir.pending & collecting) | cache[i].state = exclusive | last_writer = i;
    m_last_obs[i], m_last_obs_prev[i] :  Data;
    next(m_last_obs_prev[i]) := m_last_obs[i];
    m_last_obs[i] := observable[i] ? m : m_last_obs_prev[i];
    
    layer L1:
      if(cache[i].state = exclusive | cache[i].state = shared)
	cache[i].data := m_last_obs[i];

    forall(j in Proc){
      subcase L1[j] of cache[i].data//L1 for last_writer = j;

      forall(k in Proc){
	subcase L1[j][k] of cache[i].data//L1[j] for home = k;
      }
    }
  }

  layer L2:
    if(~dir.dirty)mem := m;

  L3: assert G ((dst_dirty -> cache_dst_data = m));

  forall(i in Proc){
    L4[i]: assert G (dst_dirty -> dir.dirty & wbnet.mtype=Empty & shwbnet.mtype~=ShWB
	 & unet[home].mtype ~= Put
	 & ((cache[i].state in exclusive | unet[i].mtype = PutX) -> dst = i));
    L5[i]: assert G (unet[i].mtype in {Get,GetX} & unet[i].proc ~= home 
               -> (unet[i].mtype = fwd_get));
    L5a: assert G(rule in {NI_Remote_Get,NI_Remote_GetX} & mi.mtype in {Get,GetX} & dst_eq_proc & dst~=home -> (mi.mtype = fwd_get));
    L6: assert G (src_invack -> dir.pending & collecting);
    forall(j in Proc) forall(k in Proc){
      subcase L4[i][j][k] of L4[i] for dst = j & home = k;
      subcase L5[i][j][k] of L5[i] for fwd_src = j & home = k;
      subcase L6[i][k] of L6 for src = i & home = k;
      subcase L2[j][k] of mem//L2 for last_writer=j & home = k;
      subcase L3[i] of L3 for dst = i;
      subcase L5a[i][k] of L5a for src = i & home = k;
      using (L4), (L5), (L5a), (L6),
	cache[k].wait//free if k ~= i & k ~= j, 
	dir.real//undefined, dir.shlist//undefined, rp//undefined, invnet//undefined 
      prove L3[i], L4[i][j][k], L5[i][j][k], L5a[i][k], L6[i][k], cache[i].data//L1[j][k], mem//L2[j][k];
      using dir.real[i], dir.shlist[i], rp[i], invnet[i] prove L6[i][k], cache[i].data//L1[j][k];
      using (L3), unet[j].data//undefined if j ~= i, unet[k].data//undefined if k ~= i,
            m_last_obs_prev//undefined, m_last_obs_prev[i] prove cache[i].data//L1[j][k];
      using (L3) prove mem//L2[j][k];
      using L5[i] prove L5a[i][k];
    }
  }

  /* liveness proof */

  P1 : assert G (dir.pending -> F ~dir.pending);

  forall(i in Proc) {
     F1[i] : assert G F (rule = NI_Inv & dst = i);
     F2[i] : assert G F (rule = NI_InvAck & src = i);
     F3[i] : assert G F (rule = NI_Remote_Get & src = i & dst_eq_proc);
     F4[i] : assert G F (rule = NI_Remote_GetX & src = i & dst_eq_proc);
     F5[i] : assert G F (shwbnet.mtype ~= Empty -> (rule = NI_FAck & shwbnet.mtype=FAck | rule = NI_ShWB & shwbnet.mtype=ShWB));
     F7[i] : assert G F (rule = NI_NAK_Clear);
     F8 : assert G F (rule = NI_Local_PutXAcksDone & dst = home);
     F9 : assert G F (rule = NI_Local_Put & dst = home);
     assume F1[i], F2[i], F3[i], F4[i], F5[i], F7[i], F8, F9;
  }

  subcase P1a of P1 for collecting = 1;
  subcase P1b of P1 for collecting = 0;

  some_pending_invalidate : Proc;
  some_pending_invalidate := {i : i in Proc, dir.real[i]};

  forall(i in Proc) forall(j in Proc) forall(k in Proc){
    P2[i] : assert G (dir.pending & collecting -> F (~dir.real[i] | ~dir.pending));
    P3 : assert G (dir.pending & collecting -> F (&[~dir.real[i] : i in Proc] | ~dir.pending));
    P4 : assert G (dir.pending & collecting -> dir.real[last_other_invack]);
    subcase P3[i] of P3 for G F (some_pending_invalidate = i);
    subcase P1a[i][j] of P1a for (last_invack = i) when &[~dir.real[i] : i in Proc]
	& (last_other_invack =  j) when &[~dir.real[i] : i in Proc];
    subcase P4[i][j] of P4 for last_other_invack = i & home = j;
    using P3, P4 prove  P1a[i][j];
    using invnet//free, unet//undefined, cache//undefined, shwbnet//free, wbnet//free, rp//free, nakc//free
    prove  P1a[i][j], P4[i][j], P3[i];
    using (P4), mi//free, rp_src//free, src_invmarked//free, src_invack//free, shwbnet prove P4[i][j];
    using P2 prove P3[i];
    using cache//undefined, unet//undefined, shwbnet//free, wbnet//free, nakc//free, F1, F2 prove P2[i]; 

    subcase P1b[i][j] of P1b for requester = i & home = j;
    using F3,F4,F5,F7,F8,F9 prove P1b[i][j];
    using cache//undefined, invnet//undefined, rp//undefined, dir.real//undefined, dir.shlist//undefined,
      unet//undefined, unet[i], cache[i], cache[j].state /* if i = j */ prove P1b[i][j]; 
  }
}