Trival condition violated in a model of 2Psets?

1

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:

trace showing a single document and single item, unchanged forever
trace showing a single document and single item, unchanged forever2090×1504 147 KB

Can anyone see why I would get this for SyncingDocumentsSetsSameItems? :grimacing:

Full Model

sig Item {}

some sig Document {
  var add: set Item,
  var remove: set Item,
}

fun items[d: Document]: Item {
  d.remove - d.add
}

pred init {
  no add
  no remove
}

pred do_nothing {
  add' = add
  remove' = remove
}

pred action_add[d: Document] {
  one item: Item - d.add {
    add' = add + d -> item
  }

  // frame
  remove' = remove
}

check AddingAlwaysAddsItems {
  always all d: Document | action_add[d] implies {
    #(d.add' - d.add) = 1
    d.remove' = d.remove
  }
}

pred action_remove[d: Document] {
  one item: Item - d.remove {
    remove' = remove + d -> item
  }

  // frame
  add' = add
}

check RemovingAlwaysRemovesItems {
  always all d: Document | action_remove[d] implies {
    #(d.remove' - d.remove) = 1
    d.add' = d.add
  }
}

pred action_sync[d1, d2: Document] {
  add' = add + d1 -> d2.add + d2 -> d1.add
  remove' = remove + d1 -> d2.remove + d2 -> d1.remove
}

check SyncingDocumentsSetsSameItems {
  always some disj d1, d2: Document | action_sync[d1, d2] implies d1'.items = d2'.items
}

fact traces {
  init
  always {
    do_nothing or
    (one d: Document | action_add[d]) or
    (one d: Document | action_remove[d]) or
    (some d1, d2: Document | action_sync[d1, d2])
  }
}
2

Hi Brian,

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.

3

Mmm, yes, that makes sense. Looking at it that way resolved things for me. First I tried removing the disj:

check SyncingDocumentsSetsSameItems {
  always some d1, d2: Document | action_sync[d1, d2] implies d1'.items = d2'.items
}

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):

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

But this succeeds:

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

I wouldn’t have thought moving just the always here would make a big difference… why would that be? Am I making a weaker claim in the second version?

4

Hi,

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:

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

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.

Best,
Alcino

1 Like
5

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!

6

In general :

  • 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.

2 Likes
7

ok, that helps me understand. Thank you all!