|
|
@ -286,7 +286,7 @@ module Debug = struct
|
|
|
|
(pp_ast
|
|
|
|
(pp_ast
|
|
|
|
~ast_node_to_highlight ~prettifier:(ANSITerminal.sprintf highlight_style "%s"))
|
|
|
|
~ast_node_to_highlight ~prettifier:(ANSITerminal.sprintf highlight_style "%s"))
|
|
|
|
ast_root in
|
|
|
|
ast_root in
|
|
|
|
L.(debug Linters Medium)
|
|
|
|
L.progress
|
|
|
|
"@\nNode ID: %d\tEvaluation stack level: %d\tSource line-number: %s@\n"
|
|
|
|
"@\nNode ID: %d\tEvaluation stack level: %d\tSource line-number: %s@\n"
|
|
|
|
eval_node.id
|
|
|
|
eval_node.id
|
|
|
|
(Stack.length t.eval_stack)
|
|
|
|
(Stack.length t.eval_stack)
|
|
|
@ -296,13 +296,13 @@ module Debug = struct
|
|
|
|
| Eval_undefined -> true
|
|
|
|
| Eval_undefined -> true
|
|
|
|
| _ -> false in
|
|
|
|
| _ -> false in
|
|
|
|
if is_last_occurrence && is_eval_result_undefined then
|
|
|
|
if is_last_occurrence && is_eval_result_undefined then
|
|
|
|
L.(debug Linters Medium)
|
|
|
|
L.progress
|
|
|
|
"From this step, a transition to a different part of the AST may follow.@\n";
|
|
|
|
"From this step, a transition to a different part of the AST may follow.@\n";
|
|
|
|
let phi_str = Format.asprintf "%a" pp_formula eval_node.content.phi in
|
|
|
|
let phi_str = Format.asprintf "%a" pp_formula eval_node.content.phi in
|
|
|
|
L.(debug Linters Medium) "CTL Formula: %s@\n@\n" phi_str;
|
|
|
|
L.progress "CTL Formula: %s@\n@\n" phi_str;
|
|
|
|
L.(debug Linters Medium) "%s@\n" ast_str;
|
|
|
|
L.progress "%s@\n" ast_str;
|
|
|
|
let quit_token = "q" in
|
|
|
|
let quit_token = "q" in
|
|
|
|
L.(debug Linters Medium) "Press Enter to continue or type %s to quit... @?" quit_token;
|
|
|
|
L.progress "Press Enter to continue or type %s to quit... @?" quit_token;
|
|
|
|
match read_line () |> String.lowercase with
|
|
|
|
match read_line () |> String.lowercase with
|
|
|
|
| s when String.equal s quit_token -> exit 0
|
|
|
|
| s when String.equal s quit_token -> exit 0
|
|
|
|
| _ ->
|
|
|
|
| _ ->
|
|
|
@ -315,7 +315,7 @@ module Debug = struct
|
|
|
|
) in
|
|
|
|
) in
|
|
|
|
match t.debugger_active, t.breakpoint_line, line_number eval_node.content.ast_node with
|
|
|
|
match t.debugger_active, t.breakpoint_line, line_number eval_node.content.ast_node with
|
|
|
|
| false, Some break_point_ln, Some ln when ln >= break_point_ln ->
|
|
|
|
| false, Some break_point_ln, Some ln when ln >= break_point_ln ->
|
|
|
|
L.(debug Linters Medium) "Attaching debugger at line %d" ln;
|
|
|
|
L.progress "Attaching debugger at line %d" ln;
|
|
|
|
stop_and_explain_step ();
|
|
|
|
stop_and_explain_step ();
|
|
|
|
{t with debugger_active = true}
|
|
|
|
{t with debugger_active = true}
|
|
|
|
| true, _, _ ->
|
|
|
|
| true, _, _ ->
|
|
|
|