flash2 invariant works

test/flash2.ivy

@@ -87,7 +87,8 @@ after init {
     real_owner := home;
     invnet(X) := false;
     invack(X) := false;
-    nakc := false
+    nakc := false;
+    dir.local_ := false
 }
 
 action pi_Local_Get_dirty = {
@@ -242,6 +243,7 @@ action ni_Local_GetX = {
     real_owner := src; # ghost
     cache(home).state := invalid;
     cache(home).invmarked := (cache(home).wait = get & dir.local_) | cache(home).invmarked;
+    dir.local_ := false;
     src := *
 }
 
@@ -488,7 +490,7 @@ invariant [coherent1]
   cache(X).state = exclusive -> X = real_owner
 
 invariant [coherent2]
-  cache(X).state = exclusive & ~cache.invmarked(Y) -> cache(Y).state ~= shared
+  cache(X).state = exclusive & ~cache.invmarked(Y) & ~dir.pending -> cache(Y).state ~= shared
 
 invariant [nodups]
   cache(X).state = exclusive -> dir.dirty & ~wbnet.wb & ~net.shwb(Y,home)
@@ -512,14 +514,13 @@ invariant net.get(X,Y) & net.get(X,Z) -> Y = Z
 invariant net.put(X,Y) -> ~net.get(Y,Z) & ~net.getX(Y,Z) & ~net.putX(Z,Y)
 
 invariant (net.put(X,Y) | cache.state(Y) = shared) & ~cache.invmarked(Y) 
-       -> dir.head & ~(dir.dirty & ~dir.pending)
-          & (dir.pending & ~collecting & (net.shwb(Y,home) | Y = home & ~cache.state(Y) = shared) | dir.shlist(Y))
+       -> ~(dir.dirty & ~dir.pending)
+          & (dir.pending & ~collecting & dir.head & (net.shwb(Y,home) | Y = home & ~cache.state(Y) = shared) | dir.pending & collecting & dir.real(Y) & invnet(Y) & Y ~= home | dir.head & dir.shlist(Y) & Y ~= home | dir.local_ & Y = home)
           & (dir.pending & collecting -> dir.real(Y))
           & ~net.fack(Q,home) & ~nakc
-          & ~wbnet.wb & cache(Z).state ~= exclusive
-          & ~net.putX(Q,R)
+          & ((net.putX(Q,R) | cache(R).state = exclusive | wbnet.wb) -> dir.pending & collecting  & dir.real(Y) & invnet(Y) & Y ~= home)
 
-invariant net.fack(X,home) -> dir.dirty & dir.pending & ~collecting  & real_owner = X
+invariant net.fack(X,home) -> dir.pending & ~collecting  & real_owner = X & ~nakc &  ~net.shwb(Y,home)
 
 invariant net.fack(X,home) & net.fack(Y,home) -> X = Y
 
@@ -535,10 +536,10 @@ invariant collecting -> dir.pending
 invariant nakc -> dir.pending & ~collecting & ~net.fack(Q,home)
 
 invariant (net.getX(X,Y) | net.get(X,Y)) & Y ~= home ->
-         dir.head & dir.dirty & dir.pending & ~collecting & ~net.fack(Q,home)
+         (dir.dirty -> dir.head) & dir.pending & ~collecting & ~net.fack(Q,home)
          & ~nakc & Y = real_owner & real_owner = dir.hptr
          & ~((net.put(Q,R) | cache.state(R) = shared) & ~cache.invmarked(R))
-         & ~net.shwb(Q,home)
+         & ~net.shwb(Q,home) & ~net.put(Q,home)
 
 invariant ~((net.getX(X,Y) | net.get(X,Y)) & (net.getX(Z,Y) | net.get(Z,Y)) & X ~= Z & Y ~= home)
 
@@ -561,6 +562,14 @@ invariant net.getX(X,Y) -> ~net.putX(Z,X)
 invariant net.getX(X,Y) & net.getX(X,Z) -> Y = Z
 
 invariant rp_net(X) -> cache.state(X) = invalid & ~net.put(Y,X) & ~(net.get(X,Z) & Z ~= home)
-    & ~net.putX(Y,X) & ~(net.getX(X,Z) & Z ~= home)
+    & ~net.putX(Y,X) & ~(net.getX(X,Z) & Z ~= home) & X ~= home
 
 invariant dir.head -> dir.shlist(dir.hptr)
+
+invariant net.put(X,home) -> dir.pending & ~collecting & ~net.fack(Y,home) & ~nakc & ~wbnet.wb & ~net.shwb(Y,home) & cache.state(Y) ~= exclusive & ~net.putX(Z,Y)
+
+invariant cache.state(home) = shared -> ~dir.pending & ~dir.dirty
+
+invariant cache.state(home) = invalid -> ~dir.local_
+
+invariant cache.state(home) = exclusive -> dir.local_ & dir.dirty