diff --git a/src/debugger/debugger.ml b/src/debugger/debugger.ml index e685a5989f0cdaaffb082dba4e9ae259c6f5794e..8e631d43dd6c5776f81789c20dd3a1c12cae764f 100644 --- a/src/debugger/debugger.ml +++ b/src/debugger/debugger.ml @@ -69,6 +69,12 @@ let listCores args = let listStates args = CM.graphIterStates (fun state -> print_endline (CM.stateToString state)) +let exportGraph args = + print_endline "digraph reasonerstate {"; + CM.graphIterCores (fun core -> print_endline (CM.coreToDot core)); + CM.graphIterStates (fun state -> print_endline (CM.stateToDot state)); + print_endline "}" + let showNode = function | (n::_) -> let n = int_of_string n in @@ -101,11 +107,10 @@ let _ = Repl.bind "status" (fun _ -> printStatus ()) "Prints reasoning status" ""; Repl.bind "lscores" listCores "Lists all cores" ""; Repl.bind "lsstates" listStates "Lists all states" ""; + Repl.bind "graphviz" exportGraph "Graphviz source of reasoner state" ""; Repl.bind "node" showNode "shows details of a node" "usage: node n"; Repl.exitBinding ]; } in Repl.start session - - diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml index 3d5b280370165dd3a9e217071fd7f319faf11e65..2ea83af44002edae8f2f5a581ac85bc3c1df01b3 100644 --- a/src/lib/CoAlgMisc.ml +++ b/src/lib/CoAlgMisc.ml @@ -709,7 +709,7 @@ let bsetToString sort bset : string = let csetToString sort cset = bsetToString sort cset -let coreToString core = +let coreToString (core:core): string = let helper cset lst : string list = (csetToString core.sortC cset):: lst in @@ -758,6 +758,32 @@ let stateToString (state:state): string = " Parents: { "^(String.concat ", " parents)^" }\n"^ "}" +let stateToDot (state:state): string = + let ownidx = (string_of_int state.idx) in + let parents = + List.map (fun (co:core) -> "Node"^string_of_int co.idx^" -> Node"^ownidx^";") + state.parentsS + in + "Node" ^ ownidx ^ " [shape=ellipse,label=\"State " ^ ownidx + ^ "\\n" ^ (Str.global_replace (Str.regexp ", ") "\\n" + (bsetToString state.sortS state.bsS)) + ^ "\"];\n" + ^ (String.concat "\n" parents) + + +let coreToDot (core:core): string = + let ownidx = (string_of_int core.idx) in + let parents = + List.map (fun (st,_:state*int) -> "Node"^string_of_int st.idx^" -> Node"^ownidx^";") + core.parentsC + in + "Node" ^ ownidx ^ " [shape=ellipse,label=\"Core " ^ ownidx + ^ "\\n" ^ (Str.global_replace (Str.regexp ", ") "\\n" + (bsetToString core.sortC core.bsC)) + ^ "\"];\n" + ^ (String.concat "\n" parents) + + let queuePrettyStatus () = let printList (sl : int list) : string = String.concat ", " (List.map string_of_int sl) diff --git a/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli index 12aa96366ed12190d4714efd6c1dd63bf10431cb..160222c47a9a95dff147e113dd8f00f3bb27453c 100644 --- a/src/lib/CoAlgMisc.mli +++ b/src/lib/CoAlgMisc.mli @@ -229,6 +229,7 @@ val stateGetConstraints : state -> csetSet val stateSetConstraints : state -> csetSet -> unit val stateNextRule : state -> ruleEnumeration val stateToString : state -> string +val stateToDot : state -> string val stateGetIdx : state -> int @@ -256,6 +257,7 @@ val coreGetIdx : core -> int val coreGetConstraintParents : core -> cset list val coreAddConstraintParent : core -> cset -> unit val coreToString : core -> string +val coreToDot : core -> string (*****************************************************************************)