Alloy : pre-order traversal of binary tree in required ordering
<p>I want a "pre-order" traversal of the nodes in BinaryTree visits them in 
this order [N0,N1,N2,N3]
What should I do with the following structure?</p>

<pre><code>one sig Ordering { // model a linear order on nodes 
  first: Node, // the first node in the linear order 
  order: Node -&gt; Node // for each node n, n.(Ordering.order) represents the
                      // node (if any) immediately after n in order 
}
fact LinearOrder { // the first node in the linear order is N0; and 
                   // the four nodes are ordered as [N0, N1, N2, N3]
}
pred SymmetryBreaking(t: BinaryTree) { // if t has a root node, it is the
   //first node according to the linear order; and 
   // a "pre-order" traversal of the nodes in t visits them according 
   //to the linear order
}
</code></pre>