# Trival condition violated in a model of 2Psets?

**URL:** <https://alloytools.discourse.group/t/trival-condition-violated-in-a-model-of-2psets/404>\
**Category:** Uncategorized\
**Created:** [September 29, 2023, 6:54pm UTC](https://alloytools.discourse.group/t/trival-condition-violated-in-a-model-of-2psets/404 "2023-09-29T18:54:32Z")\
**Posts on this page:** 7\
**Page:** 1

<div class="post-metadata">

**Author:** ![brianhicks](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/brianhicks/32/5_2.png) [@brianhicks](https://alloytools.discourse.group/u/brianhicks)\
**Post date:** [September 29, 2023, 6:54pm UTC](https://alloytools.discourse.group/t/trival-condition-violated-in-a-model-of-2psets/404/1 "2023-09-29T18:54:32Z")

</div>

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](https://global.discourse-cdn.com/free1/uploads/alloytools/original/1X/587066aef7f9e72ad2c70731631d5cc5e1332b70.jpeg)

Can anyone see why I would get this for `SyncingDocumentsSetsSameItems`? 😬

## Full Model

```alloy
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])
  }
}

```

---

<div class="post-metadata">

**Author:** ![DanielJackson](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/danieljackson/32/80_2.png) [@DanielJackson](https://alloytools.discourse.group/u/DanielJackson)\
**Post date:** [October 2, 2023, 3:07pm UTC](https://alloytools.discourse.group/t/trival-condition-violated-in-a-model-of-2psets/404/2 "2023-10-02T15:07:30Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![brianhicks](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/brianhicks/32/5_2.png) [@brianhicks](https://alloytools.discourse.group/u/brianhicks)\
**Post date:** [October 2, 2023, 8:50pm UTC](https://alloytools.discourse.group/t/trival-condition-violated-in-a-model-of-2psets/404/3 "2023-10-02T20:50:46Z")

</div>

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

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

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

```

But this succeeds:

```plaintext
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?

---

<div class="post-metadata">

**Author:** ![alcino](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/alcino/32/25_2.png) [@alcino](https://alloytools.discourse.group/u/alcino)\
**Post date:** [October 3, 2023, 6:16am UTC](https://alloytools.discourse.group/t/trival-condition-violated-in-a-model-of-2psets/404/4 "2023-10-03T06:16:24Z")

</div>

Hi,

> [@brianhicks](#):
>
> This fails (non-trivially):
> 
> ```auto
> check SyncingDocumentsSetsSameItems {
> always all d1, d2: Document | action_sync[d1, d2] implies d1'.items = d2'.items
> }
> 
> ```

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:

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

```

> [@brianhicks](#):
>
> 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?

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:

```alloy
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

---

<div class="post-metadata">

**Author:** ![brianhicks](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/brianhicks/32/5_2.png) [@brianhicks](https://alloytools.discourse.group/u/brianhicks)\
**Post date:** [October 3, 2023, 10:43am UTC](https://alloytools.discourse.group/t/trival-condition-violated-in-a-model-of-2psets/404/5 "2023-10-03T10:43:09Z")

</div>

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!

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [October 3, 2023, 1:48pm UTC](https://alloytools.discourse.group/t/trival-condition-violated-in-a-model-of-2psets/404/6 "2023-10-03T13:48:25Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![brianhicks](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/brianhicks/32/5_2.png) [@brianhicks](https://alloytools.discourse.group/u/brianhicks)\
**Post date:** [October 4, 2023, 11:54am UTC](https://alloytools.discourse.group/t/trival-condition-violated-in-a-model-of-2psets/404/7 "2023-10-04T11:54:52Z")

</div>

ok, that helps me understand. Thank you all!