Open curiousperson-art opened 4 years ago
The problem is that arr
is also an isolate. To use the specification of arr.resize
, you need to add arr
to the "with" clause of gset_protocol
.
A few other comments: your isolate 'replica' is not very helpful because it doesn't provide an abstract interface to setrep
. That abstract interface is really provided by member
and repEqual
. So I would suggest moving setrep
into the implementation of gset_protocol
. Also, move arr
into the the implementation of gset_protocol
, since it should not be used outside the isolate. Then you don't need to put arr
in the "with" clause, since it is a sub-isolate of gset_protocol
.
Also, send
looks to me like it is intended to be specification state. You probably want to move its declaration and initializer into the specification section. And you probably don't want to put a requirement on send
in the implementation, since send
if send is not intended to be implementation state. In general, you shouldn't have "require" in the implementation section, since that is a guarantee for the calling isolate, which doesn't see the implementation code. If you really want an assertion in implementation code, you should use "ensure". Then the assertion will be a guarantee for gset_protocol
.
Finally, you should be careful about axioms such as injectivity
. Axioms are OK temporarily, but they can invalidate your verification. As an example, the axiom is not consistent with the initializer for setrep
. As it happens, this will not cause an inconsistency because the "extensionality" property for arrays (saying two arrays are equal when their contents are equal) is not used by default. In general, though, axioms are risky.
I did the changes that you suggested. I have moved the array definition and setrep inside gset_protocol. But the invariant fails again and I fail to understand why as both sets pertaining to the replicas are containing the same element after add operation (and in this counter example one element only). I still have the injectivity condition and I feel it is needed as on deleting it, i see both replicas pointing to the same arr which i do not want. I want every replica to have their copy of set.
I have an abstract representation of a model where I have two isolates : replica (that contains a set/array) and is totally ordered and another isolate that performs operations on a set belonging to a certain replica. I have an inductive invariant which states that for any two different replicas, if their set sizes are same, the sets have the same elements and in the same order. This fails, but the counter example produced by Ivy is giving a wrong behavior when an element is added to an array. If you look at the picture, we see that there are 3 sets and 2 replicas. The 2 replicas point to two different sets (arr = 0, arr = 1) at first, and after the add operation has been executed at replica R1 points to arr = 2 and the index remains 0. I fail to understand the reason for this behavior. How do I eliminate three sets and make the replica point to the same set as it was pointing before? Here is my code :