Way to Nondeterministically Sample _Unique_ Values?

[zicklag]

Is there a way to nondeterministically choose a unique integer or string? I have a protocol in which there is an id field I'm dealing with and I know it will be globally unique, i.e. like a UUID, but I don't know how to represent that in quint.

I can pick IDs from a set, but that doesn't work because it might pick the same one multiple times.

Thanks for any guidance!

[bugarela]

The easiest thing is to just use an incremental id. If you need to generate new ids at any point, you can keep a global counter:

var id_counter: int

action create_new_item = all {
  items' = items.append({ uuid: id_counter, other_field: "foo" }),
  id_counter' = id_counter + 1,
}

Of course, in a real distributed implementation, a global counter is not feasible. But, unless you are trying to specifically verify your uuid generation, you can assume it works properly and just use this simplified approach to unique ids in Quint.

For non-incremental ids, if that's a requirement, the most straightforward way is to use powerset, which takes a set and returns all possible sets with elements of that set. I'm picturing it like:

pure val POSSIBLE_IDS = 1.to(500)

action init = {
  nondet ids = POSSIBLE_IDS.powerset().oneOf()
  items' = ids.map(unique_id => { uuid: unique_id, other_field: "foo" })
}

action create_new_item = {
  nondet id = POOSSIBLE_IDS.exclude(items.map(item => item.uuid)).oneOf()
  items' = items.append({ uuid: id, other_field: "foo" }),
}

This would generate a non-deterministic number of items as well, which idk if its desired in your case.

More generally, you can pick ids from a big enough set (so they don't collide super often) and then add a precondition stating that ids are unique, so the simulator and model checker will rule-out non-deterministic choices that don't satisfy it. See this example for a fixed number of items:

pure val POSSIBLE_IDS = 1.to(500)
pure val N_ITEMS = 5

action init = {
  nondet ids_map = 1.to(N_ITEMS).setOfMaps(POSSIBLE_IDS)
  all {
    ids_map.values().size() == N_ITEMS,
    items' = 1.to(N_ITEMS).map(i => { uuid: ids_map.get(i), other_field: "foo" }),
  }
}

PS: I'm using values() from basicSpells.qnt. This will construct a set of all values, so if an id is repeated, the size of the set will be smaller than N_ITEMS.

[zicklag]

Awesome, thanks, that's perfect!