1 open list
 2 open pool
 3 open queue
 4 
 5 val traverse
 6   [unvisited, visiting, visited, p : perm]
 7   exclusive visited =>
 8   (
 9     (* A pool of all nodes. *)
10     nodes: pool unvisited,
11     (* A list of the root nodes. *)
12     roots: list dynamic,
13     (* A function that changes the state of a node from [unvisited] to [visiting]. *)
14     pre: (consumes node: unvisited | p) -> (| node @ visiting),
15     (* A function that changes the state of a node from [visiting]
16        to [visited] and returns its successors. *)
17     post: (consumes node: visiting | p) -> (list dynamic | node @ visited)
18     (* The permission [p] required by [pre] and [post]. *)
19     | p
20   )
21 :
22   (* A new pool of the visited nodes. *)
23   pool visited
24   =
25 
26   (* Create a new pool. *)
27   let completed = Pool in
28 
29   (* Create a waiting queue of the discovered, but not completed, nodes. *)
30   let waiting = queue::create () in
31 
32   (* Examining a node. If it is new, we change its state to [visiting]
33      and enqueue it. *)
34   let examine (node: dynamic |
35     nodes @ pool unvisited *
36     waiting @ fifo visiting *
37     completed @ pool visited *
38     p
39   ) : () =
40     (* Perform a dynamic ownership test. *)
41     if nodes owns node then begin
42       (* This node has not been reached yet. *)
43       take node from nodes;
44       (* Change its state to [visiting]. *)
45       pre node;
46       (* Enqueue it. *)
47       queue::insert (node, waiting)
48     end
49   in
50 
51   (* The main loop. *)
52   let rec loop (|
53     nodes @ pool unvisited *
54     waiting @ queue::fifo visiting *
55     completed @ pool visited *
56     p
57   ) : () =
58     (* Take a node off the queue. *)
59     match queue::retrieve waiting with
60     | None ->
61         ()
62     | Some { contents = node } ->
63         (* Change its state to [visited]. *)
64         let successors = post node in
65         (* Place it in the final pool. *)
66         give node to completed;
67         (* Examine its successors. *)
68         list::iter (successors, examine);
69         (* Continue. *)
70         loop()
71     end
72   in
73 
74   (* Examine each of the roots, and enter the main loop. *)
75   list::iter (roots, examine);
76   loop();
77 
78   (* Return the new pool. *)
79   completed