No instances of Tree—why?

models
1

While modeling git objects, I came up with this model:

sig Object {}

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

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

It produces instances, but none with any Tree. Alloy (well, Electrum) says “Predicate is consistent, contrary to expectation.”

What I’m intending to do is say that a tree cannot be its own parent (which may itself be a bad assumption, but I couldn’t make that happen using git hash-object and friends.)

Where have I gone sideways here? It’s been a while since I read Software Abstractions, so a lot of this is trying to get the memory of how to do this back in my fingers.

2

Hi Brian,

Looks good, but you have one small snag here: the star is reflexive transitive closure, so t.*children includes t, and will therefore never allow a tree to exist! Try using ^, transitive closure, instead.

Not sure why you get that message. Peter – can you help with this? I suspect it’s that an implicit run command (running when you have no explicit command) is incorrectly defaulting to expecting no instances.

1 Like
3

ahh, thanks. I tried ^ before (when trying the form sig Tree { … } { assertion } but hadn’t once I moved it to a separate fact block.

You intuition regarding the default command seems to have been correct as well; once I added an empty predicate and ran it the result goes to “Instance found. Predicate is consistent.”

4

Great! Let us know how it goes and feel free to ask if you need more help…