+(* Note that we do not consider the nil nodes *)
+
+(* Build the Oracle *)
+let rec bu_oracle asta run tree tnode =
+ let init_set node =
+ let set = (StateSet.empty,StateSet.empty) in
+ NodeHash.add run node set
+ and node = Tree.preorder tree tnode in
+ if (Tree.is_leaf tree tnode)
+ then
+ if not (tnode == Tree.nil)
+ then
+ init_set node
+ else ()
+ else
+ begin
+ bu_oracle asta run tree (Tree.first_child tree tnode);
+ bu_oracle asta run tree (Tree.next_sibling tree tnode);
+ ();
+ end
+
+(* Build the over-approx. of the maximal run *)
+let rec bu_over_max asta run tree node =
+ ()
+
+(* Build the maximal run *)
+let rec tp_max asta run tree node =
+ ()
+