I’m trying to model a 2Pset CRDT in Alloy and I’m having some trouble. Basically, I think I’m telling Alloy that syncing two documents should result in them having the same items, but in reality I think there’s some trivial condition that’s being violeted, because despite having a some disj d1, d2: Document in the condition, I get this as a counterexample:

I wonder if there’s a mistake in the condition you’re checking?

always some disj a, b: T | P

would produce a counterexample in which there is a state in which

some disj a, b: T | P

is not true. That would be trivially satisfied by having T contain only one element, so that there cannot be two distinct values an and b for which P holds. And that seems to be what you have here, since the visualizer shows a single object labeled Document, the lack of an index indicating that the set only contains one element.

I was fairly certain that this should be correct, since syncing the same document should be allowed. This passes. However, then I would get the same trivial failure if I said the items should not be equal, so I was not certain that I had gotten it.

But then I remembered that I was saying always some, not always all. Changing that seems to give me a better result: now I can see something more like what I’d expect when I reverse the condition. But now I’m getting another thing I find mysterious! This fails (non-trivially):

I think this one is failing because you are not using the prime operator correctly. d1'.items is the same as d1.items since all quantified variables are immutable (rigid) and priming them will not change their value. What you should use to determine the set of items in the next state is (d1.items)', as follows:

Here the problem is quite mundane: always being a unary operator binds stronger than implies, which is a binary operator. So, the check should have been specified as follows:

pred SyncingDocumentsSetsSameItems {
all d1, d2: Document | always (action_sync[d1, d2] implies (d1.items)' = (d2.items)')
}

They are both equivalent in this case, but be aware that if Document was mutable that might not be the case.

oof, ok, thanks. I would never have guessed that d1' would not work. Can you say more about why that is the case? Why does action_sync succeed, then? It uses the primed variables that we’re supplying here too. Since items' clearly works, that’s just confusing!

x.r' is the value associated to the current value of x by the next value of r

x'.r is the value associated to the next value of x by the current value of r

(x.r)', which is equal to x'.r', is the value associated to the next value of x by the next value of r

Furthermore, if x is static (= non-var), it entails always x = x'.

Finally, suppose E is Bool, composed of True and False: surely, when you write all x : Bool | something, you don’t expect x to change its value in something ; rather, the whole quantification means that something holds when x is True and also when x is False. This is why quantified variables are immutable.

However, as Alcino suggested, a mutable relation (such as items in your example) may change, so the value it associates to atoms could change too.