How to say "these should not be equal"

models
1

hey, it’s git time again! I’m picking back up from the model from No instances of Tree—why?, which now looks like this:

sig Object {}

sig Tree {
  children: some (Object + Tree)
}

fact {
  no t: Tree | t in t.^children
}

pred Default {}

run Default for 3

instead of moving on to model git’s commits immediately, I’m pausing here to make sure my model’s trees do not do anything that real git trees couldn’t. After producing a bunch of instances, I see that my model can produce this instance:

image

But I can’t produce it by manipulating objects in git! Hooray for content-addressed stores, I guess.

I think the thing I want to say is “there are no two trees with the same children”. The thing I’m trying naively is adding the following fact to the fact block in the model above:

no t, u: Tree | t.children = u.children

but when I run that, I just get a bunch of empty trees, so I suspect that this does not do the thing I think it does! I sat down and thought about how . works, and my best guess is that I’m actually asking something about the nature of the children rather than the nature of the trees.

So, two questions:

  1. how do I enact the intent I described above?
  2. what is the code I wrote actually doing?
1 Like
2

Hi Brian,

The problem is that the constraint t.children = u.children will be true when u = t! So the only was to satisfy the quantified formula is to ensure there are no trees. The fix is to write something like

no t, u: Tree | t.children = u.children and t != u

or

no disj t, u: Tree | t.children = u.children

BTW, if you want to ensure that no two distinct trees overlap in their children, you’ll need something different, like

no disj t, u: Tree | some t.children & u.children

which can also be written as a declaration constraint

children in Tree lone -> (Object + Tree)

saying that at most one (less than or equal to one, or lone) tree is mapped to a given child.

1 Like
3

This is a very frequent problem I ran into. A quantification is true when there are no elements. I often have to check if there are any elements.

4

thanks again, folks! :grin: