Issue 65: Implications with constraints aren't 'remembered'
Status:  Verified
Owner:
Closed:  May 2009
Project Member Reported by nels.bec...@gmail.com, May 13, 2009
If a state invariant includes an implication, and none of the fields in 
that implication are touched/modified, we normally get to remember that 
implication, and we can use it to satisfy the packing requirements for that 
same invariant.

However, this doesn't work when the permission in the implication has 
constraints. For example, a permission with a guarantee, (e.g., 
reject_incoming_requests == true -> full(this,PROTOCOL) in STILLOPEN). This 
is because the check to see whether or not we already know this permission 
(which looks in the knownImplications field of the dynamic state logic) 
uses a call to 'contains' which in turn calls 'equals.' 

The result is false because the known implication includes const 
constraints (there exists) and the implication we have to prove includes 
VAR constraints (forall). These two constraints are literally not equal to 
one another.

We need to check that the implication we know SATISFIES the implication we 
need.
May 18, 2009
Project Member #2 nels.bec...@gmail.com
DynamicStateLogic.isKnownImplication(Aliasing, Implication)
May 18, 2009
Project Member #3 nels.bec...@gmail.com
Fixed in r307, at least to the point where the test passes.

In the long run, this may need more work for other types of implications.
Status: Verified