Merging two sets of relations by some rule

1

Say I have a Document with a counts field, like this:

open util/natural

sig ID {}

sig Document {
  counts: ID -> lone Natural
}

I’d like to merge any two documents by combining the counts and taking the max Natural for each ID. So if I have these documents, I want to merge them in this way:

Document 0 Document 1 Merged
ID 0 1 2 2
ID 1 1 0 1

I’m having trouble with this! First I tried a set comprehension, which didn’t work (seems to be mostly about filtering rather than transforming?) Then I tried something like this:

fun merge[d1, d2: ID -> lone Natural]: (ID -> lone Natural) {
  let both = d1 + d2 | { kv: both }
}

That doesn’t work because both needs to be a unary set. Sure, ok, fair. But how do you do this? I can think of plenty of ways to mess with the sets as a whole, but I’m having trouble finding a way to tell Alloy that I want to make a pairwise decision on all the relations in the set!

2

Hi,

You can define the resulting relation by comprehension. For example, you could use comprehension to summarize a relation that possibly contains many naturals per id, and then use it to merge the union of the two count relations:

fun summarize[ds : ID -> set Natural] : (ID -> lone Natural) {
	{i : ID, n : Natural | i->n in ds and n = max[i.ds] }
}

fun merge[d1, d2: ID -> lone Natural]: (ID -> lone Natural) {
  	summarize[d1+d2]
}

Best,
Alcino

3

Ooh, ok, that makes sense. Thank you. The gap in my understanding here was that I got that { i : ID, n : Natural | … } would be the cartesian product, but I didn’t think to limit that to the set of ds in the condition. Makes total sense now.