diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml index 8688a690e8297a4fa7f86368f9e8f48e83896ce3..2f5fd5eeb474a7ff3f2642567967a8abb0d339b5 100644 --- a/src/lib/CoAlgMisc.ml +++ b/src/lib/CoAlgMisc.ml @@ -727,6 +727,11 @@ let lfToInt lf = lf let lfFromInt num = num let lfGetFormula sort f = !arrayFormula.(sort).(f) +let escapeHtml (input : string) : string = + List.fold_right (fun (x, y) (str : string) -> Str.global_replace (Str.regexp x) y str) + [("<", "<") ; (">", ">") ; ("&", "&")] + input + let bsetToString sort bset : string = let toFormula (lf:localFormula) (lst: string list) : string list = let formula: C.formula = lfGetFormula sort lf in @@ -797,6 +802,13 @@ let stateToDot (state:state): string = | Open -> "yellow" | Expandable -> "white" in + let toFormula (lf:localFormula) (lst: string list) : string list = + let formula: C.formula = lfGetFormula state.sortS lf in + if (bsetMem state.deferralS lf) + then ("<B>"^(escapeHtml (C.string_of_formula formula))^"</B>") :: lst + else (escapeHtml (C.string_of_formula formula)) :: lst + in + let formulaList = bsetFold toFormula state.bsS [] in let ownidx = (string_of_int state.idx) in let parents = List.map (fun (co:core) -> @@ -804,10 +816,9 @@ let stateToDot (state:state): string = state.parentsS in "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color - ^ ",label=\"State " ^ ownidx - ^ "\\n" ^ (Str.global_replace (Str.regexp ", ") "\\n" - (bsetToString state.sortS state.bsS)) - ^ "\"];\n" + ^ ",label=<State " ^ ownidx + ^ "<BR/>" ^ (String.concat "<BR/>" formulaList) + ^ ">];\n" ^ (String.concat "\n" parents) @@ -818,6 +829,13 @@ let coreToDot (core:core): string = | Open -> "yellow" | Expandable -> "white" in + let toFormula (lf:localFormula) (lst: string list) : string list = + let formula: C.formula = lfGetFormula core.sortC lf in + if (bsetMem core.deferralC lf) + then ("<B>"^(escapeHtml (C.string_of_formula formula))^"</B>") :: lst + else (escapeHtml (C.string_of_formula formula)) :: lst + in + let formulaList = bsetFold toFormula core.bsC [] in let ownidx = (string_of_int core.idx) in let parents = List.map (fun (st,_:state*int) -> @@ -825,10 +843,9 @@ let coreToDot (core:core): string = core.parentsC in "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color - ^ ",label=\"Core " ^ ownidx - ^ "\\n" ^ (Str.global_replace (Str.regexp ", ") "\\n" - (bsetToString core.sortC core.bsC)) - ^ "\"];\n" + ^ ",label=<Core " ^ ownidx + ^ "<BR/>" ^ (String.concat "<BR/>" formulaList) + ^ ">];\n" ^ (String.concat "\n" parents)