16.3.4 Treeness Condition

We say that any 2 nodes and must satisfy the treeness condition expressed as the following disjunction:

The treeness condition that must hold between Ni and Nj is realized by four concurrent disjunctions and is controlled by choice variable Cij. The latter is a finite domain variable taking a value in [1..4].

<DC: treeness condition between Ni and Nj>=

C in C::1#4
thread  
   or C = 1 {Equal Ni Nj}
   [] C = 2 {StrictlyDominates Ni Nj}
   [] C = 3 {StrictlyDominates Nj Ni}
   [] C = 4 {Side Nj Ni}
   end 
end

The thread ... end statements in the code fragment cause the computation to create four new concurrent threads, one for each choice variable. This is necessary because the or statements within the new threads block until only one of their guards can be satisfiable, and we don't want this to block our entire computation.