Run with pred and body only runs body? [Electrum]

Questions
1

With the model below. The justRun: command does what I would expect, all the As and Bs are linked. The second run done command does not fulfil the done clause but only links one A and B. It looks like it’s treating done as a label. If this is correct, a warning would be helpful as it cost me several days.

sig A {
  , var linked: set B
}
sig B {}

pred link[a: A] { one b: B | linked' = linked + a->b }
pred skip { linked' = linked }

pred init {
  some A
  some B
  no linked
}

fact trace {
  init
  always (some a: A | link[a])
}

justRun: run {
  #A > 1
  #B > 1
  eventually (all a: A | a in linked.B and all b: B | b in A.linked)
}

pred done {
  eventually (all a: A | a in linked.B and all b: B | b in A.linked)
}

run done { // this doesn't seem to exercise the done pred.
  #A > 1
  #B > 1  
}
2

This was answered here https://alloytools.discourse.group/t/struggling-with-multi-relations/109/9. Seem to me like it’s worth a warning.

3

To tell the truth, I didn’t even know this notation. I haven’t checked but is it different from the default behavior in plain Alloy? I suppose run done { ... } is the same as done : run { ... } , which just means the same as run {...}, the only difference being that the said command has a nice done name appearing in the Execution menu (instead of something like run$42 for .....

4

I believe this is Alloy behaviour, although I haven’t checked it. At one level it’s clear, at another it’s an accident waiting to happen (took me a week to find). That’s why I think it’s worth a warning when the name matches a predicate (actually, I’d prefer to take it out but that might upset people).

The command description in the back of the Green Book says qualName or block, which suggests that this shouldn’t be allowed.

5

Yes, that’s the same behaviour as in plain Alloy, although I’m not sure it is documented anywhere.