| Issue 65: | Implications with constraints aren't 'remembered' | |
| 1 person starred this issue and may be notified of changes. | Back to list |
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
May 18, 2009
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
|