Search code examples
alloy

Alloy predicate for a tree

I am trying to write a predicate in alloy which will determine if a set of nodes is a tree. I have the pseudo code, but am confused on how to implement it. I am new to alloy so thank you to all of those who respond in advance.

sig Node[]

pred isTree [r: Node -> Node] {
// Every node reachable from root
// No cycles
// No node has more than 1 more parent.
}
Solution

  • You can check out this online Alloy tutorial in which a fileSystem is modeled. It's also a tree structure, so you pretty much have your answers.

    More specific answers require more specific questions and a display of your attempts.

    We're not giving away solutions to homeworks ;-).