No instances of Tree—why?

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.

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

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.”

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