I wanted to solve the exercise A.1.5 from the book Software Abstractions. The task is to define a model which instances are exactly trees. I specifically chose to define directed trees.
I also added a relation that lets me count how many nodes have incoming degree not equal to 1. I expected there to be exactly one such node with incoming degree 0 — the root.
Here is the code:
sig X {relation: set X}
sig Pointer {point: X}
fact isTree
{
no x: X | x in x.(^relation)
one x: X | # relation.x != 1
}
fact pointing
{
all x: X | # relation.x != 1 <=> # point.x = 1
all x: X | # relation.x = 1 <=> # point.x = 0
no disj pointer1, pointer2: Pointer | pointer1.point = pointer2.point
}
run {} for 10 but exactly 9 X
check {# point = 1} for 9
Now, it could be that my facts do not define a tree. But then why do I only get these ill trees when I ask for examples of size 9 or more? There should be ill trees of size 4 already, for example a lozenge shaped graph — but I cannot find any.
I am using Alloy version 6.1.0.202111031525 on Linux.
Haven’t you made a mistake at some point because I think there’s no way in your model for some X to have more than one parent. Indeed, since your finite graph is acyclic (first line of the fact), at least one node has no parent, but then it’s the only one because of the second line.
Furthermore, notice that using cardinalities is in general unadvised because you’re bringing integers in, and since ints can wrap around (e.g. with a scope of 4 Int, 8 wraps to -8), you may have surprises sometimes. It’s better practice to use qualifiers such as one when possible:
pred isTree
{
no x: X | x in x.(^relation)
one x: X | not one relation.x
}
Well, this is what I thought too… Something seems to be subtly wrong. You see the code, you see the pictures — can you reproduce this on your computer?
This sounds terrible. So you are saying that # relation = 1 may assert that a relation has cardinality 1, or cardinality 2^n + 1, or generally cardinality ℤ × 2^n + 1? We can observe that the amount of arrows pointing at the pathological node in both pictures is 8. Apparently this becomes conflated with 0 at some point!
I didn’t click Next until exhaustion but after 20+ times, no. One possibility would be that you had this Viz window open from an earlier version of the spec and left it open, then confused that with the result of your last version. This happens to me sometimes.
I don’t think this is the issue here (besides, 8 doesn’t wrap to 0 with the default bitwidth of 4). I was just warning you in general that, due to the wrap-around semantics (which makes sense when the solver is based on SAT, as in Alloy), arithmetic reasoning can be misleading.
No need to click — just execute the check. I iterated on this many times before writing here, in different variations, so it is unlikely to be an accident. I can do it again. Let me record a screencast… Here:
aside Would someone with privileges enable video attachments as described here?
Well, I am not saying that integers wrap in this case. With the scope of 10, there should be what, 1024 values for integers? And if, as you say, bit width is fixed at 4, there would be 16 — still enough. But if the cardinality comparison were, for whatever reason, to wrap at 2^3 = 8, we should observe exactly this kind of a pathological tree! And exactly at scope 9! (We need exactly 8 atoms pointing at the 9th.) This is too unlikely to be a coincidence.
Well, it is good to know that this can happen! Sincerely, I think this is dangerous and misleading behaviour. At least it should be documented in capital letters on the first page of every document, and then on every other page for good measure…
Welcome to the forum, @kindaro. I’ll let you and guru @grayswandyr work out the details, but I wanted to point out that it’s always better to avoid introducing integers if you can. The formula
# relation.x != 1
says that there is not exactly one atom linked to x via relation, which is better written as
There is still something I do not understand. Is the behaviour shown on the video I attached above expected and documented, or should an issue be opened?
