EDIT: Idiomatic specification of graph with ordered adjacency?

Questions
1

I looked at util/graph and util/ordering to see whether I could straightforwardly express ordered trees by a combination of the two modules.

open util/ordering[Node->Node]
open util/graph[Node]
sig Node {}
run tree

But Alloy does not allow the Node->Node argument to instantiate the module. I’m not looking for just any way to specify ordered trees (e.g. with seq Node). Instead, I suspect that there is a idiomatic and concise way of expressing them. Any hints?

EDIT: Trying to understand this made me realize that

  • for trees opening util/ordering[Node] should be enough, but more importantly that
  • what I had in mind are graphs on which the adjacent nodes are considered in order, e.g. a node A could be the first neighbor of another node B, but the second neighbor of another node C.

I suspect that I really do need seqs here, but I’d like to know if there are other (recommended) ways to specify this.

2

I don’t know if this is the idiomatic way, but it seems to “work”. Iterate through the instances using the Viz and you will see rooted trees with each node having an ordered sequence of outgoing edges.

-- rooted trees with ordered children

sig Node {
  out: seq Node -- out is a ternary relation of type Node x Int x Node
}

-- the set of children of a node
fun children[u: Node]: set Node { u.out.elems }

-- the next-node binary relation, { (u,v) | v is a child of u }
fun nxt[]: Node->Node { { u: Node, v: Node | v in children[u] } }

fact {
  some root: Node | { -- the tree has a root node
    -- the root has no incoming edge:
    no nxt.root
    -- every non-root has one incoming edge:
    all v: Node - root | one u: Node, i: Int | v = u.out[i]
    -- every node is reachable from the root:
    Node = root.*nxt
  }
}

pred show[] { #Node > 4 }
run show for 6
3

Thanks!

What you suggest is in essence what I am doing. Since I only iterate over the adjacent nodes, I thought that the actual indexing that seq provides is not needed and that maybe it could be expressed elegantly with only util/ordering but then again the same nodes could appear in different order for two distinct nodes.