From: Lucca Hirschi Date: Wed, 4 Jul 2012 14:13:38 +0000 (+0200) Subject: structure of Run.compute + pretty-printing (run+tree with preorder) X-Git-Tag: Core~5 X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=ce22e0dd0d0dbb234bc965feb14ab8f250be2da4 structure of Run.compute + pretty-printing (run+tree with preorder) --- diff --git a/src/run.ml b/src/run.ml index 57e037d..bd85dd4 100644 --- a/src/run.ml +++ b/src/run.ml @@ -23,14 +23,43 @@ module NodeHash = Hashtbl.Make (Node) type t = (StateSet.t*StateSet.t) NodeHash.t (** Map from node to query and recognizing states *) - +(* 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 = + () + let compute tree asta = let size_tree = 10000 in (* todo *) let map = NodeHash.create size_tree in - - + bu_oracle asta map tree (Tree.root tree); + bu_over_max asta map tree (Tree.root tree); + tp_max asta map tree (Tree.root tree); map - + let print fmt run = let print_d_set fmt (s_1,s_2) = Format.fprintf fmt "@[(%a,@ %a)@]" @@ -40,11 +69,11 @@ let print fmt run = if NodeHash.length run = 0 then Format.fprintf fmt "ø" else - NodeHash.iter (fun cle set -> pp "@ | %i-->%a" cle print_d_set set) + NodeHash.iter (fun cle set -> pp "| %i-->%a @ " cle print_d_set set) run in let print_box fmt run = let pp = Format.fprintf fmt in - pp "@[# Mapping: %a@]" + pp "@[@. # Mapping:@. @[%a@]@]" print_map run in - Format.fprintf fmt "@[##### RUN #####@, %a@]@." print_box run + Format.fprintf fmt "@[##### RUN #####@, %a@]@." print_box run diff --git a/src/stateSet.ml b/src/stateSet.ml index 47ad460..082ac8e 100644 --- a/src/stateSet.ml +++ b/src/stateSet.ml @@ -18,5 +18,10 @@ open Format include Ptset.Make (Hcons.PosInt) let print ppf s = - fprintf ppf "{ %a }" - (Pretty.print_list ~sep:" " (State.print)) (elements s) + let p_set ppf s = + if is_empty s + then fprintf ppf "ø" + else + (Pretty.print_list ~sep:" " (State.print)) ppf (elements s) in + fprintf ppf "{ %a }" p_set s + diff --git a/src/test.ml b/src/test.ml index 935023d..00f75f0 100644 --- a/src/test.ml +++ b/src/test.ml @@ -63,4 +63,6 @@ let () = output_string stderr "\n"; Asta.print err_formatter asta; Run.print err_formatter run; + output_string stderr "\n # Doc: \n"; + Tree.print_xml_preorder stderr doc (Tree.root doc); exit 0 diff --git a/src/tree.ml b/src/tree.ml index 1cfc77a..2b0fa4e 100644 --- a/src/tree.ml +++ b/src/tree.ml @@ -263,6 +263,43 @@ let root t = t.root let first_child _ n = n.first_child let next_sibling _ n = n.next_sibling let parent _ n = n.parent +(* Begin Lucca Hirschi *) +let is_leaf t n = (first_child t n == nil) && (next_sibling t n == nil) +(* End *) let tag _ n = n.tag let data _ n = n.data let preorder _ n = n.preorder + +(*Lucca Hirschi: *) +let rec print_xml_preorder out tree_ node = + if node != nil then + let () = + if node.tag == QName.text then + begin + output_escape_string out node.data; + output_string out ("'"^(string_of_int(preorder tree_ node))); + end + else + let tag = QName.to_string node.tag in + output_char out '<'; + output_string out tag; + output_string out (" '"^(string_of_int(preorder tree_ node))); + let fchild = + if node.first_child.tag == QName.attribute_map then + let () = + print_attributes out tree_ node.first_child.first_child + in + node.first_child.next_sibling + else + node.first_child + in + if fchild == nil then output_string out "/>" + else begin + output_char out '>'; + print_xml_preorder out tree_ fchild; + output_string out "' + end + in + print_xml_preorder out tree_ node.next_sibling diff --git a/src/tree.mli b/src/tree.mli index 1d5d77b..c75fd26 100644 --- a/src/tree.mli +++ b/src/tree.mli @@ -61,6 +61,9 @@ val parent : t -> node -> node Returns [nil] if [n == nil]. *) +val is_leaf : t -> node -> bool +(** Return true if the node is a *) + val tag : t -> node -> QName.t (** Returns the label of a given node *) @@ -74,3 +77,7 @@ val preorder : t -> node -> int (** Returns the position of a node in pre-order in the tree. The root has preorder 0. [nil] has pre-order [-1]. *) + +val print_xml_preorder : out_channel -> t -> node -> unit +(** Outputs the tree with IDs for nodes as an XML document on the + given output_channel *) diff --git a/tests/results/my.result b/tests/results/my.result index c2f4cd7..53567dc 100644 --- a/tests/results/my.result +++ b/tests/results/my.result @@ -38,5 +38,21 @@ Parse Tree OK ! Parse query OK ! Compil OK ! Run OK ! | q₇ ----F(c)---> ↓₁q₆ ∧ ̅↓̅₁̅q̅₅ | q₇ ----Cof(ø)---> ↓₁q₇ ∨ ↓₂q₇ -##### RUN ##### - # Mapping: ø +##### RUN ##### + # Mapping: + | 14-->({ ø }, { ø }) | 16-->({ ø }, { ø }) + | 21-->({ ø }, { ø }) | 24-->({ ø }, { ø }) + | 25-->({ ø }, { ø }) | 34-->({ ø }, { ø }) + | 35-->({ ø }, { ø }) + + # Doc: +<#document '0> + '2 + '4 + '6 + '8 + '10 '17 '19 '21 + '22 '24 + '25 + '26 '28 '30 '32 '34 +'35 \ No newline at end of file