diff --git a/infer/src/al/AL.ml b/infer/src/al/AL.ml
index 7955c74e0..d4e497c19 100644
--- a/infer/src/al/AL.ml
+++ b/infer/src/al/AL.ml
@@ -296,7 +296,7 @@ and do_frontend_checks_decl linters (context : CLintersContext.context) decl =
         ALIssues.invoke_set_of_checkers_on_node linters context' an ;
         (* We need to visit explicitly nodes reachable via Parameters transitions
            because they won't be visited during the evaluation of the formula *)
-        do_frontend_checks_via_transition linters context' an CTL.Parameters ;
+        do_frontend_checks_via_transition linters context' an CTLTypes.Parameters ;
         match CAst_utils.get_method_body_opt decl with
         | Some stmt ->
             do_frontend_checks_stmt linters context' stmt
diff --git a/infer/src/al/ALDebugger.ml b/infer/src/al/ALDebugger.ml
new file mode 100644
index 000000000..34c510120
--- /dev/null
+++ b/infer/src/al/ALDebugger.ml
@@ -0,0 +1,340 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+module L = Logging
+
+let pp_ast ~ast_node_to_highlight ?(prettifier = Fn.id) fmt root =
+  let open Ctl_parser_types in
+  let pp_node_info fmt an =
+    let name = Ctl_parser_types.ast_node_name an in
+    let typ = Ctl_parser_types.ast_node_type an in
+    let cast_kind = Ctl_parser_types.ast_node_cast_kind an in
+    Format.fprintf fmt " %s %s %s" name typ cast_kind
+  in
+  let rec pp_children pp_node wrapper fmt level nodes =
+    match nodes with
+    | [] ->
+        ()
+    | node :: nodes ->
+        pp_node fmt (wrapper node) level "|-" ;
+        pp_children pp_node wrapper fmt level nodes
+  in
+  let rec pp_ast_aux fmt root level prefix =
+    let get_node_name (an : ast_node) =
+      match an with
+      | Stmt stmt ->
+          Clang_ast_proj.get_stmt_kind_string stmt
+      | Decl decl ->
+          Clang_ast_proj.get_decl_kind_string decl
+    in
+    let should_highlight =
+      match (root, ast_node_to_highlight) with
+      | Stmt r, Stmt n ->
+          phys_equal r n
+      | Decl r, Decl n ->
+          phys_equal r n
+      | _ ->
+          false
+    in
+    let node_name =
+      let node_name = get_node_name root in
+      if should_highlight then prettifier node_name else node_name
+    in
+    let spaces = String.make (level * String.length prefix) ' ' in
+    let next_level = level + 1 in
+    Format.fprintf fmt "%s%s%s %a@\n" spaces prefix node_name pp_node_info root ;
+    match root with
+    | Stmt (DeclStmt (_, stmts, ([VarDecl _] as var_decl))) ->
+        (* handling special case of DeclStmt with VarDecl: emit the VarDecl node
+           then emit the statements in DeclStmt as children of VarDecl. This is
+           because despite being equal, the statements inside VarDecl and those
+           inside DeclStmt belong to different instances, hence they fail the
+           phys_equal check that should colour them *)
+        pp_children pp_ast_aux (fun n -> Decl n) fmt next_level var_decl ;
+        pp_stmts fmt (next_level + 1) stmts
+    | Stmt stmt ->
+        let _, stmts = Clang_ast_proj.get_stmt_tuple stmt in
+        pp_stmts fmt next_level stmts
+    | Decl decl ->
+        let decls =
+          Clang_ast_proj.get_decl_context_tuple decl
+          |> Option.map ~f:(fun (decls, _) -> decls)
+          |> Option.value ~default:[]
+        in
+        pp_decls fmt next_level decls
+  and pp_stmts fmt level stmts = pp_children pp_ast_aux (fun n -> Stmt n) fmt level stmts
+  and pp_decls fmt level decls = pp_children pp_ast_aux (fun n -> Decl n) fmt level decls in
+  pp_ast_aux fmt root 0 ""
+
+
+module EvaluationTracker = struct
+  exception Empty_stack of string
+
+  type eval_result = Eval_undefined | Eval_true | Eval_false
+
+  type content =
+    { ast_node: Ctl_parser_types.ast_node
+    ; phi: CTLTypes.t
+    ; lcxt: CLintersContext.context
+    ; eval_result: eval_result
+    ; witness: Ctl_parser_types.ast_node option }
+
+  type eval_node = {id: int; content: content}
+
+  type tree = Tree of eval_node * tree list
+
+  type ast_node_to_display =
+    (* the node can be used to describe further sub calls in the evaluation stack *)
+    | Carry_forward of Ctl_parser_types.ast_node
+    (* the node cannot be further used to describe sub calls in the evaluation stack *)
+    | Last_occurrence of Ctl_parser_types.ast_node
+
+  type t =
+    { next_id: int
+    ; eval_stack: (tree * ast_node_to_display) Stack.t
+    ; forest: tree list
+    ; breakpoint_line: int option
+    ; debugger_active: bool }
+
+  let create_content ast_node phi lcxt =
+    {ast_node; phi; eval_result= Eval_undefined; lcxt; witness= None}
+
+
+  let create source_file =
+    let breakpoint_token = "INFER_BREAKPOINT" in
+    let breakpoint_line =
+      In_channel.read_lines (SourceFile.to_abs_path source_file)
+      |> List.findi ~f:(fun _ line -> String.is_substring line ~substring:breakpoint_token)
+      |> Option.map ~f:(fun (i, _) -> i + 1)
+    in
+    {next_id= 0; eval_stack= Stack.create (); forest= []; breakpoint_line; debugger_active= false}
+
+
+  let explain t ~eval_node ~ast_node_to_display =
+    let open Ctl_parser_types in
+    let line_number an =
+      let line_of_source_range (sr : Clang_ast_t.source_range) =
+        let loc_info, _ = sr in
+        loc_info.sl_line
+      in
+      match an with
+      | Stmt stmt ->
+          let stmt_info, _ = Clang_ast_proj.get_stmt_tuple stmt in
+          line_of_source_range stmt_info.si_source_range
+      | Decl decl ->
+          let decl_info = Clang_ast_proj.get_decl_tuple decl in
+          line_of_source_range decl_info.di_source_range
+    in
+    let stop_and_explain_step () =
+      let highlight_style =
+        match eval_node.content.eval_result with
+        | Eval_undefined ->
+            ANSITerminal.[Bold]
+        | Eval_true ->
+            ANSITerminal.[Bold; green]
+        | Eval_false ->
+            ANSITerminal.[Bold; red]
+      in
+      let ast_node_to_highlight = eval_node.content.ast_node in
+      let ast_root, is_last_occurrence =
+        match ast_node_to_display with
+        | Carry_forward n ->
+            (n, false)
+        | Last_occurrence n ->
+            (n, true)
+      in
+      let witness_str =
+        match eval_node.content.witness with
+        | Some witness ->
+            "\n- witness: "
+            ^ Ctl_parser_types.ast_node_kind witness
+            ^ " "
+            ^ Ctl_parser_types.ast_node_name witness
+        | None ->
+            ""
+      in
+      let ast_str =
+        Format.asprintf "%a %s"
+          (pp_ast ~ast_node_to_highlight ~prettifier:(ANSITerminal.sprintf highlight_style "%s"))
+          ast_root witness_str
+      in
+      L.progress "@\nNode ID: %d\tEvaluation stack level: %d\tSource line-number: %s@\n"
+        eval_node.id (Stack.length t.eval_stack)
+        (Option.value_map ~default:"Unknown" ~f:string_of_int (line_number ast_node_to_highlight)) ;
+      let is_eval_result_undefined =
+        match eval_node.content.eval_result with Eval_undefined -> true | _ -> false
+      in
+      if is_last_occurrence && is_eval_result_undefined then
+        L.progress "From this step, a transition to a different part of the AST may follow.@\n" ;
+      let phi_str = Format.asprintf "%a" CTLTypes.pp_formula eval_node.content.phi in
+      L.progress "CTL Formula: %s@\n@\n" phi_str ;
+      L.progress "%s@\n" ast_str ;
+      let quit_token = "q" in
+      L.progress "Press Enter to continue or type %s to quit... @?" quit_token ;
+      match In_channel.input_line_exn In_channel.stdin |> String.lowercase with
+      | s when String.equal s quit_token ->
+          L.exit 0
+      | _ ->
+          (* Remove the line at the bottom of terminal with the debug instructions *)
+          let open ANSITerminal in
+          (* move one line up, as current line is the one generated by pressing enter *)
+          move_cursor 0 (-1) ;
+          move_bol () ;
+          (* move to the beginning of the line *)
+          erase Below
+      (* erase what follows the cursor's position *)
+    in
+    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 ->
+        L.progress "Attaching debugger at line %d" ln ;
+        stop_and_explain_step () ;
+        {t with debugger_active= true}
+    | true, _, _ ->
+        stop_and_explain_step () ; t
+    | _ ->
+        t
+
+
+  let eval_begin t content =
+    let node = {id= t.next_id; content} in
+    let create_subtree root = Tree (root, []) in
+    let subtree' = create_subtree node in
+    let ast_node_from_previous_call =
+      match Stack.top t.eval_stack with
+      | Some (_, Last_occurrence _) ->
+          content.ast_node
+      | Some (_, Carry_forward an) ->
+          an
+      | None ->
+          content.ast_node
+    in
+    let ast_node_to_display =
+      if CTLTypes.has_transition content.phi then Last_occurrence ast_node_from_previous_call
+      else Carry_forward ast_node_from_previous_call
+    in
+    Stack.push t.eval_stack (subtree', ast_node_to_display) ;
+    let t' = explain t ~eval_node:node ~ast_node_to_display in
+    {t' with next_id= t.next_id + 1}
+
+
+  let eval_end t result =
+    let result_bool = Option.is_some result in
+    let eval_result_of_bool = function true -> Eval_true | false -> Eval_false in
+    if Stack.is_empty t.eval_stack then
+      raise (Empty_stack "Unbalanced number of eval_begin/eval_end invocations") ;
+    let evaluated_tree, eval_node, ast_node_to_display =
+      match Stack.pop_exn t.eval_stack with
+      | Tree (({id= _; content} as eval_node), children), ast_node_to_display ->
+          let content' =
+            {content with eval_result= eval_result_of_bool result_bool; witness= result}
+          in
+          let eval_node' = {eval_node with content= content'} in
+          (Tree (eval_node', children), eval_node', ast_node_to_display)
+    in
+    let t' = explain t ~eval_node ~ast_node_to_display in
+    let forest' =
+      if Stack.is_empty t'.eval_stack then evaluated_tree :: t'.forest
+      else
+        let parent =
+          match Stack.pop_exn t'.eval_stack with
+          | Tree (node, children), ntd ->
+              (Tree (node, evaluated_tree :: children), ntd)
+        in
+        Stack.push t'.eval_stack parent ; t'.forest
+    in
+    {t' with forest= forest'}
+
+
+  let equal_ast_node = Poly.equal
+
+  module DottyPrinter = struct
+    let dotty_of_ctl_evaluation t =
+      let open CTLTypes in
+      let open Ctl_parser_types in
+      let buffer_content buf =
+        let result = Buffer.contents buf in
+        Buffer.reset buf ; result
+      in
+      let dotty_of_tree cluster_id tree =
+        let get_root tree = match tree with Tree (root, _) -> root in
+        let get_children tree = match tree with Tree (_, children) -> List.rev children in
+        (* shallow: emit dotty about root node and edges to its children *)
+        let shallow_dotty_of_tree tree =
+          let root_node = get_root tree in
+          let children = get_children tree in
+          let edge child_node =
+            if equal_ast_node root_node.content.ast_node child_node.content.ast_node then
+              Printf.sprintf "%d -> %d [style=dotted]" root_node.id child_node.id
+            else Printf.sprintf "%d -> %d [style=bold]" root_node.id child_node.id
+          in
+          let color =
+            match root_node.content.eval_result with
+            | Eval_true ->
+                "green"
+            | Eval_false ->
+                "red"
+            | _ ->
+                L.(die InternalError) "Tree is not fully evaluated"
+          in
+          let label =
+            let string_of_lcxt c =
+              match c.CLintersContext.et_evaluation_node with
+              | Some s ->
+                  "et_evaluation_node = " ^ s
+              | _ ->
+                  "et_evaluation_node = NONE"
+            in
+            let string_of_ast_node an =
+              match an with
+              | Stmt stmt ->
+                  Clang_ast_proj.get_stmt_kind_string stmt
+              | Decl decl ->
+                  Clang_ast_proj.get_decl_kind_string decl
+            in
+            let smart_string_of_formula phi =
+              let num_children = List.length children in
+              match phi with
+              | And _ when Int.equal num_children 2 ->
+                  "(...) AND (...)"
+              | Or _ when Int.equal num_children 2 ->
+                  "(...) OR (...)"
+              | Implies _ when Int.equal num_children 2 ->
+                  "(...) ==> (...)"
+              | Not _ ->
+                  "NOT(...)"
+              | _ ->
+                  Format.asprintf "%a" CTLTypes.pp_formula phi
+            in
+            Format.sprintf "(%d)\\n%s\\n%s\\n%s" root_node.id
+              (Escape.escape_dotty (string_of_ast_node root_node.content.ast_node))
+              (Escape.escape_dotty (string_of_lcxt root_node.content.lcxt))
+              (Escape.escape_dotty (smart_string_of_formula root_node.content.phi))
+          in
+          let edges =
+            let buf = Buffer.create 16 in
+            List.iter
+              ~f:(fun subtree -> Buffer.add_string buf (edge (get_root subtree) ^ "\n"))
+              children ;
+            buffer_content buf
+          in
+          Printf.sprintf "%d [label=\"%s\" shape=box color=%s]\n%s\n" root_node.id label color edges
+        in
+        let rec traverse buf tree =
+          Buffer.add_string buf (shallow_dotty_of_tree tree) ;
+          List.iter ~f:(traverse buf) (get_children tree)
+        in
+        let buf = Buffer.create 16 in
+        traverse buf tree ;
+        Printf.sprintf "subgraph cluster_%d {\n%s\n}" cluster_id (buffer_content buf)
+      in
+      let buf = Buffer.create 16 in
+      List.iteri
+        ~f:(fun cluster_id tree -> Buffer.add_string buf (dotty_of_tree cluster_id tree ^ "\n"))
+        (List.rev t.forest) ;
+      Printf.sprintf "digraph CTL_Evaluation {\n%s\n}\n" (buffer_content buf)
+  end
+end
diff --git a/infer/src/al/ALDebugger.mli b/infer/src/al/ALDebugger.mli
new file mode 100644
index 000000000..90e5b51f6
--- /dev/null
+++ b/infer/src/al/ALDebugger.mli
@@ -0,0 +1,48 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+module EvaluationTracker : sig
+  type eval_result = Eval_undefined | Eval_true | Eval_false
+
+  type content =
+    { ast_node: Ctl_parser_types.ast_node
+    ; phi: CTLTypes.t
+    ; lcxt: CLintersContext.context
+    ; eval_result: eval_result
+    ; witness: Ctl_parser_types.ast_node option }
+
+  type eval_node = {id: int; content: content}
+
+  type tree = Tree of eval_node * tree list
+
+  type ast_node_to_display =
+    (* the node can be used to describe further sub calls in the evaluation stack *)
+    | Carry_forward of Ctl_parser_types.ast_node
+    (* the node cannot be further used to describe sub calls in the evaluation stack *)
+    | Last_occurrence of Ctl_parser_types.ast_node
+
+  type t =
+    { next_id: int
+    ; eval_stack: (tree * ast_node_to_display) Stack.t
+    ; forest: tree list
+    ; breakpoint_line: int option
+    ; debugger_active: bool }
+
+  val create : SourceFile.t -> t
+
+  val create_content : Ctl_parser_types.ast_node -> CTLTypes.t -> CLintersContext.context -> content
+
+  val eval_begin : t -> content -> t
+
+  val eval_end : t -> Ctl_parser_types.ast_node option -> t
+
+  module DottyPrinter : sig
+    val dotty_of_ctl_evaluation : t -> string
+  end
+end
diff --git a/infer/src/al/ALIssues.ml b/infer/src/al/ALIssues.ml
index c8dd5a8ad..1c3f01f80 100644
--- a/infer/src/al/ALIssues.ml
+++ b/infer/src/al/ALIssues.ml
@@ -11,7 +11,7 @@ module L = Logging
 module MF = MarkupFormatter
 
 type linter =
-  { condition: CTL.t
+  { condition: CTLTypes.t
   ; issue_desc: CIssue.issue_desc
   ; whitelist_paths: ALVar.t list
   ; blacklist_paths: ALVar.t list }
@@ -66,7 +66,7 @@ let pp_linters fmt linters =
 (* Map a formula id to a triple (visited, parameters, definition).
    Visited is used during the expansion phase to understand if the
    formula was already expanded and, if yes we have a cyclic definifion *)
-type macros_map = (bool * ALVar.t list * CTL.t) ALVar.FormulaIdMap.t
+type macros_map = (bool * ALVar.t list * CTLTypes.t) ALVar.FormulaIdMap.t
 
 (* Map a path name to a list of paths.  *)
 type paths_map = ALVar.t list ALVar.VarMap.t
@@ -249,11 +249,12 @@ let create_parsed_linters linters_def_file checkers : linter list =
         | _ ->
             (issue, cond, wl_paths, bl_paths)
       in
-      List.fold ~f:process_linter_definitions ~init:(dummy_issue, CTL.False, [], [])
+      List.fold ~f:process_linter_definitions
+        ~init:(dummy_issue, CTLTypes.False, [], [])
         checker.definitions
     in
     L.(debug Linters Medium) "@\nMaking condition and issue desc for checker '%s'@\n" checker.id ;
-    L.(debug Linters Medium) "@\nCondition =@\n    %a@\n" CTL.Debug.pp_formula condition ;
+    L.(debug Linters Medium) "@\nCondition =@\n    %a@\n" CTLTypes.pp_formula condition ;
     let issue_type =
       let doc_url =
         Option.first_some
@@ -276,7 +277,7 @@ let rec apply_substitution f sub =
     with Not_found_s _ | Caml.Not_found -> p
   in
   let sub_list_param ps = List.map ps ~f:sub_param in
-  let open CTL in
+  let open CTLTypes in
   match f with
   | True | False ->
       f
@@ -320,7 +321,7 @@ let expand_formula phi map_ error_msg_ =
   let fail_with_circular_macro_definition name error_msg =
     L.(die ExternalError) "Macro '%s' has a circular definition.@\n Cycle:@\n%s" name error_msg
   in
-  let open CTL in
+  let open CTLTypes in
   let rec expand acc map error_msg =
     match acc with
     | True | False ->
diff --git a/infer/src/al/ALIssues.mli b/infer/src/al/ALIssues.mli
index 52d4c397f..65b73d737 100644
--- a/infer/src/al/ALIssues.mli
+++ b/infer/src/al/ALIssues.mli
@@ -10,7 +10,7 @@ open! IStd
 val issue_log : IssueLog.t ref
 
 type linter =
-  { condition: CTL.t
+  { condition: CTLTypes.t
   ; issue_desc: CIssue.issue_desc
   ; whitelist_paths: ALVar.t list
   ; blacklist_paths: ALVar.t list }
@@ -23,7 +23,7 @@ val pp_linters : Format.formatter -> linter list -> unit
    (visited, parameters, definition).
    Visited is used during the expansion phase to understand if the
    formula was already expanded and, if yes we have a cyclic definifion *)
-type macros_map = (bool * ALVar.t list * CTL.t) ALVar.FormulaIdMap.t
+type macros_map = (bool * ALVar.t list * CTLTypes.t) ALVar.FormulaIdMap.t
 
 (** Map a path name to a list of paths.  *)
 type paths_map = ALVar.t list ALVar.VarMap.t
diff --git a/infer/src/al/ALUtils.ml b/infer/src/al/ALUtils.ml
index 378fa42a7..0c8f13b3d 100644
--- a/infer/src/al/ALUtils.ml
+++ b/infer/src/al/ALUtils.ml
@@ -44,7 +44,7 @@ let tag_name_of_node an =
 
 
 let decl_ref_or_selector_name an =
-  match CTL.next_state_via_transition an CTL.PointerToDecl with
+  match CTL.next_state_via_transition an CTLTypes.PointerToDecl with
   | [(Ctl_parser_types.Decl (ObjCMethodDecl _) as decl_an)] ->
       "The selector " ^ Ctl_parser_types.ast_node_name decl_an
   | [(Ctl_parser_types.Decl _ as decl_an)] ->
@@ -62,7 +62,7 @@ let iphoneos_target_sdk_version context _ =
 
 let available_ios_sdk an =
   let open Ctl_parser_types in
-  match CTL.next_state_via_transition an CTL.PointerToDecl with
+  match CTL.next_state_via_transition an CTLTypes.PointerToDecl with
   | [Decl decl] -> (
     match CPredicates.get_available_attr_ios_sdk (Decl decl) with
     | Some version ->
diff --git a/infer/src/al/cTL.ml b/infer/src/al/CTL.ml
similarity index 64%
rename from infer/src/al/cTL.ml
rename to infer/src/al/CTL.ml
index 34f5316f5..799dca930 100644
--- a/infer/src/al/cTL.ml
+++ b/infer/src/al/CTL.ml
@@ -14,86 +14,6 @@ module L = Logging
    CTL formula which express a condition saying when the checker should
     report a problem *)
 
-(** Transition labels used for example to switch from decl to stmt *)
-type transitions =
-  | AccessorForProperty of ALVar.alexp  (** decl to decl *)
-  | Body  (** decl to stmt *)
-  | FieldName of ALVar.alexp  (** stmt to stmt, decl to decl *)
-  | Fields  (** stmt to stmt, decl to decl *)
-  | InitExpr  (** decl to stmt *)
-  | Super  (** decl to decl *)
-  | ParameterName of ALVar.alexp  (** stmt to stmt, decl to decl *)
-  | ParameterPos of ALVar.alexp  (** stmt to stmt, decl to decl *)
-  | Parameters  (** stmt to stmt, decl to decl *)
-  | Cond
-  | PointerToDecl  (** stmt to decl *)
-  | Protocol  (** decl to decl *)
-  | Sibling  (** decl to decl *)
-  | SourceExpr
-[@@deriving compare]
-
-let is_transition_to_successor trans =
-  match trans with
-  | Body
-  | InitExpr
-  | FieldName _
-  | Fields
-  | ParameterName _
-  | ParameterPos _
-  | Parameters
-  | Cond
-  | SourceExpr ->
-      true
-  | Super | PointerToDecl | Protocol | AccessorForProperty _ | Sibling ->
-      false
-
-
-(* In formulas below prefix
-   "E" means "exists a path"
-   "A" means "for all path" *)
-
-type t =
-  (* A ctl formula *)
-  | True
-  | False
-  (* not really necessary but it makes it evaluation faster *)
-  | Atomic of CPredicates.t
-  | Not of t
-  | And of t * t
-  | Or of t * t
-  | Implies of t * t
-  | InNode of ALVar.alexp list * t
-  | AX of transitions option * t
-  | EX of transitions option * t
-  | AF of transitions option * t
-  | EF of transitions option * t
-  | AG of transitions option * t
-  | EG of transitions option * t
-  | AU of transitions option * t * t
-  | EU of transitions option * t * t
-  | EH of ALVar.alexp list * t
-  | ET of ALVar.alexp list * transitions option * t
-  | InObjCClass of t * t
-[@@deriving compare]
-
-let equal = [%compare.equal: t]
-
-let has_transition phi =
-  match phi with
-  | True | False | Atomic _ | Not _ | And _ | Or _ | Implies _ | InNode _ | EH _ | InObjCClass _ ->
-      false
-  | AX (trans_opt, _)
-  | AF (trans_opt, _)
-  | AG (trans_opt, _)
-  | AU (trans_opt, _, _)
-  | EX (trans_opt, _)
-  | EF (trans_opt, _)
-  | EG (trans_opt, _)
-  | EU (trans_opt, _, _)
-  | ET (_, trans_opt, _) ->
-      Option.is_some trans_opt
-
-
 (* "set" clauses are used for defining mandatory variables that will be used
    by when reporting issues: eg for defining the condition.
 
@@ -112,9 +32,9 @@ let has_transition phi =
 *)
 
 type clause =
-  | CLet of ALVar.formula_id * ALVar.t list * t
+  | CLet of ALVar.formula_id * ALVar.t list * CTLTypes.t
   (* Let clause: let id = definifion;  *)
-  | CSet of ALVar.keyword * t
+  | CSet of ALVar.keyword * CTLTypes.t
   (* Set clause: set id = definition *)
   | CDesc of ALVar.keyword * string
   (* Description clause eg: set message = "..." *)
@@ -129,427 +49,6 @@ type al_file =
   ; global_paths: (string * ALVar.alexp list) list
   ; checkers: ctl_checker list }
 
-let equal_ast_node = Poly.equal
-
-module Debug = struct
-  let pp_transition fmt trans_opt =
-    let pp_aux fmt trans =
-      match trans with
-      | AccessorForProperty kind ->
-          Format.pp_print_string fmt ("AccessorForProperty " ^ ALVar.alexp_to_string kind)
-      | Body ->
-          Format.pp_print_string fmt "Body"
-      | FieldName name ->
-          Format.pp_print_string fmt ("FieldName " ^ ALVar.alexp_to_string name)
-      | Fields ->
-          Format.pp_print_string fmt "Fields"
-      | InitExpr ->
-          Format.pp_print_string fmt "InitExpr"
-      | Super ->
-          Format.pp_print_string fmt "Super"
-      | ParameterName name ->
-          Format.pp_print_string fmt ("ParameterName " ^ ALVar.alexp_to_string name)
-      | ParameterPos pos ->
-          Format.pp_print_string fmt ("ParameterPos " ^ ALVar.alexp_to_string pos)
-      | Parameters ->
-          Format.pp_print_string fmt "Parameters"
-      | Cond ->
-          Format.pp_print_string fmt "Cond"
-      | Protocol ->
-          Format.pp_print_string fmt "Protocol"
-      | PointerToDecl ->
-          Format.pp_print_string fmt "PointerToDecl"
-      | Sibling ->
-          Format.pp_print_string fmt "Sibling"
-      | SourceExpr ->
-          Format.pp_print_string fmt "SourceExpr"
-    in
-    match trans_opt with Some trans -> pp_aux fmt trans | None -> Format.pp_print_char fmt '_'
-
-
-  (* a flag to print more or less in the dotty graph *)
-  let full_print = true
-
-  let rec pp_formula fmt phi =
-    let nodes_to_string nl = List.map ~f:ALVar.alexp_to_string nl in
-    match phi with
-    | True ->
-        Format.pp_print_string fmt "True"
-    | False ->
-        Format.pp_print_string fmt "False"
-    | Atomic p ->
-        CPredicates.pp_predicate fmt p
-    | Not phi ->
-        if full_print then Format.fprintf fmt "NOT(%a)" pp_formula phi
-        else Format.pp_print_string fmt "NOT(...)"
-    | And (phi1, phi2) ->
-        if full_print then Format.fprintf fmt "(%a AND %a)" pp_formula phi1 pp_formula phi2
-        else Format.pp_print_string fmt "(... AND ...)"
-    | Or (phi1, phi2) ->
-        if full_print then Format.fprintf fmt "(%a OR %a)" pp_formula phi1 pp_formula phi2
-        else Format.pp_print_string fmt "(... OR ...)"
-    | Implies (phi1, phi2) ->
-        Format.fprintf fmt "(%a ==> %a)" pp_formula phi1 pp_formula phi2
-    | InNode (nl, phi) ->
-        Format.fprintf fmt "IN-NODE %a: (%a)"
-          (Pp.comma_seq Format.pp_print_string)
-          (nodes_to_string nl) pp_formula phi
-    | AX (trs, phi) ->
-        Format.fprintf fmt "AX[->%a](%a)" pp_transition trs pp_formula phi
-    | EX (trs, phi) ->
-        Format.fprintf fmt "EX[->%a](%a)" pp_transition trs pp_formula phi
-    | AF (trs, phi) ->
-        Format.fprintf fmt "AF[->%a](%a)" pp_transition trs pp_formula phi
-    | EF (trs, phi) ->
-        Format.fprintf fmt "EF[->%a](%a)" pp_transition trs pp_formula phi
-    | AG (trs, phi) ->
-        Format.fprintf fmt "AG[->%a](%a)" pp_transition trs pp_formula phi
-    | EG (trs, phi) ->
-        Format.fprintf fmt "EG[->%a](%a)" pp_transition trs pp_formula phi
-    | AU (trs, phi1, phi2) ->
-        Format.fprintf fmt "A[->%a][%a UNTIL %a]" pp_transition trs pp_formula phi1 pp_formula phi2
-    | EU (trs, phi1, phi2) ->
-        Format.fprintf fmt "E[->%a][%a UNTIL %a]" pp_transition trs pp_formula phi1 pp_formula phi2
-    | EH (arglist, phi) ->
-        Format.fprintf fmt "EH[%a](%a)"
-          (Pp.comma_seq Format.pp_print_string)
-          (nodes_to_string arglist) pp_formula phi
-    | ET (arglist, trans, phi) ->
-        Format.fprintf fmt "ET[%a][%a](%a)"
-          (Pp.comma_seq Format.pp_print_string)
-          (nodes_to_string arglist) pp_transition trans pp_formula phi
-    | InObjCClass (phi1, phi2) ->
-        if full_print then Format.fprintf fmt "InObjCClass(%a, %a)" pp_formula phi1 pp_formula phi2
-
-
-  let pp_ast ~ast_node_to_highlight ?(prettifier = Fn.id) fmt root =
-    let pp_node_info fmt an =
-      let name = Ctl_parser_types.ast_node_name an in
-      let typ = Ctl_parser_types.ast_node_type an in
-      let cast_kind = Ctl_parser_types.ast_node_cast_kind an in
-      Format.fprintf fmt " %s %s %s" name typ cast_kind
-    in
-    let rec pp_children pp_node wrapper fmt level nodes =
-      match nodes with
-      | [] ->
-          ()
-      | node :: nodes ->
-          pp_node fmt (wrapper node) level "|-" ;
-          pp_children pp_node wrapper fmt level nodes
-    in
-    let rec pp_ast_aux fmt root level prefix =
-      let get_node_name (an : ast_node) =
-        match an with
-        | Stmt stmt ->
-            Clang_ast_proj.get_stmt_kind_string stmt
-        | Decl decl ->
-            Clang_ast_proj.get_decl_kind_string decl
-      in
-      let should_highlight =
-        match (root, ast_node_to_highlight) with
-        | Stmt r, Stmt n ->
-            phys_equal r n
-        | Decl r, Decl n ->
-            phys_equal r n
-        | _ ->
-            false
-      in
-      let node_name =
-        let node_name = get_node_name root in
-        if should_highlight then prettifier node_name else node_name
-      in
-      let spaces = String.make (level * String.length prefix) ' ' in
-      let next_level = level + 1 in
-      Format.fprintf fmt "%s%s%s %a@\n" spaces prefix node_name pp_node_info root ;
-      match root with
-      | Stmt (DeclStmt (_, stmts, ([VarDecl _] as var_decl))) ->
-          (* handling special case of DeclStmt with VarDecl: emit the VarDecl node
-             then emit the statements in DeclStmt as children of VarDecl. This is
-             because despite being equal, the statements inside VarDecl and those
-             inside DeclStmt belong to different instances, hence they fail the
-             phys_equal check that should colour them *)
-          pp_children pp_ast_aux (fun n -> Decl n) fmt next_level var_decl ;
-          pp_stmts fmt (next_level + 1) stmts
-      | Stmt stmt ->
-          let _, stmts = Clang_ast_proj.get_stmt_tuple stmt in
-          pp_stmts fmt next_level stmts
-      | Decl decl ->
-          let decls =
-            Clang_ast_proj.get_decl_context_tuple decl
-            |> Option.map ~f:(fun (decls, _) -> decls)
-            |> Option.value ~default:[]
-          in
-          pp_decls fmt next_level decls
-    and pp_stmts fmt level stmts = pp_children pp_ast_aux (fun n -> Stmt n) fmt level stmts
-    and pp_decls fmt level decls = pp_children pp_ast_aux (fun n -> Decl n) fmt level decls in
-    pp_ast_aux fmt root 0 ""
-
-
-  module EvaluationTracker = struct
-    exception Empty_stack of string
-
-    type eval_result = Eval_undefined | Eval_true | Eval_false
-
-    type content =
-      { ast_node: ast_node
-      ; phi: t
-      ; lcxt: CLintersContext.context
-      ; eval_result: eval_result
-      ; witness: ast_node option }
-
-    type eval_node = {id: int; content: content}
-
-    type tree = Tree of eval_node * tree list
-
-    type ast_node_to_display =
-      (* the node can be used to describe further sub calls in the evaluation stack *)
-      | Carry_forward of ast_node
-      (* the node cannot be further used to describe sub calls in the evaluation stack *)
-      | Last_occurrence of ast_node
-
-    type t =
-      { next_id: int
-      ; eval_stack: (tree * ast_node_to_display) Stack.t
-      ; forest: tree list
-      ; breakpoint_line: int option
-      ; debugger_active: bool }
-
-    let create_content ast_node phi lcxt =
-      {ast_node; phi; eval_result= Eval_undefined; lcxt; witness= None}
-
-
-    let create source_file =
-      let breakpoint_token = "INFER_BREAKPOINT" in
-      let breakpoint_line =
-        In_channel.read_lines (SourceFile.to_abs_path source_file)
-        |> List.findi ~f:(fun _ line -> String.is_substring line ~substring:breakpoint_token)
-        |> Option.map ~f:(fun (i, _) -> i + 1)
-      in
-      {next_id= 0; eval_stack= Stack.create (); forest= []; breakpoint_line; debugger_active= false}
-
-
-    let explain t ~eval_node ~ast_node_to_display =
-      let line_number an =
-        let line_of_source_range (sr : Clang_ast_t.source_range) =
-          let loc_info, _ = sr in
-          loc_info.sl_line
-        in
-        match an with
-        | Stmt stmt ->
-            let stmt_info, _ = Clang_ast_proj.get_stmt_tuple stmt in
-            line_of_source_range stmt_info.si_source_range
-        | Decl decl ->
-            let decl_info = Clang_ast_proj.get_decl_tuple decl in
-            line_of_source_range decl_info.di_source_range
-      in
-      let stop_and_explain_step () =
-        let highlight_style =
-          match eval_node.content.eval_result with
-          | Eval_undefined ->
-              ANSITerminal.[Bold]
-          | Eval_true ->
-              ANSITerminal.[Bold; green]
-          | Eval_false ->
-              ANSITerminal.[Bold; red]
-        in
-        let ast_node_to_highlight = eval_node.content.ast_node in
-        let ast_root, is_last_occurrence =
-          match ast_node_to_display with
-          | Carry_forward n ->
-              (n, false)
-          | Last_occurrence n ->
-              (n, true)
-        in
-        let witness_str =
-          match eval_node.content.witness with
-          | Some witness ->
-              "\n- witness: "
-              ^ Ctl_parser_types.ast_node_kind witness
-              ^ " "
-              ^ Ctl_parser_types.ast_node_name witness
-          | None ->
-              ""
-        in
-        let ast_str =
-          Format.asprintf "%a %s"
-            (pp_ast ~ast_node_to_highlight ~prettifier:(ANSITerminal.sprintf highlight_style "%s"))
-            ast_root witness_str
-        in
-        L.progress "@\nNode ID: %d\tEvaluation stack level: %d\tSource line-number: %s@\n"
-          eval_node.id (Stack.length t.eval_stack)
-          (Option.value_map ~default:"Unknown" ~f:string_of_int (line_number ast_node_to_highlight)) ;
-        let is_eval_result_undefined =
-          match eval_node.content.eval_result with Eval_undefined -> true | _ -> false
-        in
-        if is_last_occurrence && is_eval_result_undefined then
-          L.progress "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
-        L.progress "CTL Formula: %s@\n@\n" phi_str ;
-        L.progress "%s@\n" ast_str ;
-        let quit_token = "q" in
-        L.progress "Press Enter to continue or type %s to quit... @?" quit_token ;
-        match In_channel.input_line_exn In_channel.stdin |> String.lowercase with
-        | s when String.equal s quit_token ->
-            L.exit 0
-        | _ ->
-            (* Remove the line at the bottom of terminal with the debug instructions *)
-            let open ANSITerminal in
-            (* move one line up, as current line is the one generated by pressing enter *)
-            move_cursor 0 (-1) ;
-            move_bol () ;
-            (* move to the beginning of the line *)
-            erase Below
-        (* erase what follows the cursor's position *)
-      in
-      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 ->
-          L.progress "Attaching debugger at line %d" ln ;
-          stop_and_explain_step () ;
-          {t with debugger_active= true}
-      | true, _, _ ->
-          stop_and_explain_step () ; t
-      | _ ->
-          t
-
-
-    let eval_begin t content =
-      let node = {id= t.next_id; content} in
-      let create_subtree root = Tree (root, []) in
-      let subtree' = create_subtree node in
-      let ast_node_from_previous_call =
-        match Stack.top t.eval_stack with
-        | Some (_, Last_occurrence _) ->
-            content.ast_node
-        | Some (_, Carry_forward an) ->
-            an
-        | None ->
-            content.ast_node
-      in
-      let ast_node_to_display =
-        if has_transition content.phi then Last_occurrence ast_node_from_previous_call
-        else Carry_forward ast_node_from_previous_call
-      in
-      Stack.push t.eval_stack (subtree', ast_node_to_display) ;
-      let t' = explain t ~eval_node:node ~ast_node_to_display in
-      {t' with next_id= t.next_id + 1}
-
-
-    let eval_end t result =
-      let result_bool = Option.is_some result in
-      let eval_result_of_bool = function true -> Eval_true | false -> Eval_false in
-      if Stack.is_empty t.eval_stack then
-        raise (Empty_stack "Unbalanced number of eval_begin/eval_end invocations") ;
-      let evaluated_tree, eval_node, ast_node_to_display =
-        match Stack.pop_exn t.eval_stack with
-        | Tree (({id= _; content} as eval_node), children), ast_node_to_display ->
-            let content' =
-              {content with eval_result= eval_result_of_bool result_bool; witness= result}
-            in
-            let eval_node' = {eval_node with content= content'} in
-            (Tree (eval_node', children), eval_node', ast_node_to_display)
-      in
-      let t' = explain t ~eval_node ~ast_node_to_display in
-      let forest' =
-        if Stack.is_empty t'.eval_stack then evaluated_tree :: t'.forest
-        else
-          let parent =
-            match Stack.pop_exn t'.eval_stack with
-            | Tree (node, children), ntd ->
-                (Tree (node, evaluated_tree :: children), ntd)
-          in
-          Stack.push t'.eval_stack parent ; t'.forest
-      in
-      {t' with forest= forest'}
-
-
-    module DottyPrinter = struct
-      let dotty_of_ctl_evaluation t =
-        let buffer_content buf =
-          let result = Buffer.contents buf in
-          Buffer.reset buf ; result
-        in
-        let dotty_of_tree cluster_id tree =
-          let get_root tree = match tree with Tree (root, _) -> root in
-          let get_children tree = match tree with Tree (_, children) -> List.rev children in
-          (* shallow: emit dotty about root node and edges to its children *)
-          let shallow_dotty_of_tree tree =
-            let root_node = get_root tree in
-            let children = get_children tree in
-            let edge child_node =
-              if equal_ast_node root_node.content.ast_node child_node.content.ast_node then
-                Printf.sprintf "%d -> %d [style=dotted]" root_node.id child_node.id
-              else Printf.sprintf "%d -> %d [style=bold]" root_node.id child_node.id
-            in
-            let color =
-              match root_node.content.eval_result with
-              | Eval_true ->
-                  "green"
-              | Eval_false ->
-                  "red"
-              | _ ->
-                  L.(die InternalError) "Tree is not fully evaluated"
-            in
-            let label =
-              let string_of_lcxt c =
-                match c.CLintersContext.et_evaluation_node with
-                | Some s ->
-                    "et_evaluation_node = " ^ s
-                | _ ->
-                    "et_evaluation_node = NONE"
-              in
-              let string_of_ast_node an =
-                match an with
-                | Stmt stmt ->
-                    Clang_ast_proj.get_stmt_kind_string stmt
-                | Decl decl ->
-                    Clang_ast_proj.get_decl_kind_string decl
-              in
-              let smart_string_of_formula phi =
-                let num_children = List.length children in
-                match phi with
-                | And _ when Int.equal num_children 2 ->
-                    "(...) AND (...)"
-                | Or _ when Int.equal num_children 2 ->
-                    "(...) OR (...)"
-                | Implies _ when Int.equal num_children 2 ->
-                    "(...) ==> (...)"
-                | Not _ ->
-                    "NOT(...)"
-                | _ ->
-                    Format.asprintf "%a" pp_formula phi
-              in
-              Format.sprintf "(%d)\\n%s\\n%s\\n%s" root_node.id
-                (Escape.escape_dotty (string_of_ast_node root_node.content.ast_node))
-                (Escape.escape_dotty (string_of_lcxt root_node.content.lcxt))
-                (Escape.escape_dotty (smart_string_of_formula root_node.content.phi))
-            in
-            let edges =
-              let buf = Buffer.create 16 in
-              List.iter
-                ~f:(fun subtree -> Buffer.add_string buf (edge (get_root subtree) ^ "\n"))
-                children ;
-              buffer_content buf
-            in
-            Printf.sprintf "%d [label=\"%s\" shape=box color=%s]\n%s\n" root_node.id label color
-              edges
-          in
-          let rec traverse buf tree =
-            Buffer.add_string buf (shallow_dotty_of_tree tree) ;
-            List.iter ~f:(traverse buf) (get_children tree)
-          in
-          let buf = Buffer.create 16 in
-          traverse buf tree ;
-          Printf.sprintf "subgraph cluster_%d {\n%s\n}" cluster_id (buffer_content buf)
-        in
-        let buf = Buffer.create 16 in
-        List.iteri
-          ~f:(fun cluster_id tree -> Buffer.add_string buf (dotty_of_tree cluster_id tree ^ "\n"))
-          (List.rev t.forest) ;
-        Printf.sprintf "digraph CTL_Evaluation {\n%s\n}\n" (buffer_content buf)
-    end
-  end
-end
-
 let print_checker c =
   L.(debug Linters Medium) "@\n-------------------- @\n" ;
   L.(debug Linters Medium) "@\nChecker name: %s@\n" c.id ;
@@ -558,10 +57,10 @@ let print_checker c =
       match d with
       | CSet (keyword, phi) ->
           let cn_str = ALVar.keyword_to_string keyword in
-          L.(debug Linters Medium) "    %s=  @\n    %a@\n@\n" cn_str Debug.pp_formula phi
+          L.(debug Linters Medium) "    %s=  @\n    %a@\n@\n" cn_str CTLTypes.pp_formula phi
       | CLet (exp, _, phi) ->
           let cn_str = ALVar.formula_id_to_string exp in
-          L.(debug Linters Medium) "    %s=  @\n    %a@\n@\n" cn_str Debug.pp_formula phi
+          L.(debug Linters Medium) "    %s=  @\n    %a@\n@\n" cn_str CTLTypes.pp_formula phi
       | CDesc (keyword, s) ->
           let cn_str = ALVar.keyword_to_string keyword in
           L.(debug Linters Medium) "    %s=  @\n    %s@\n@\n" cn_str s
@@ -580,7 +79,7 @@ let ctl_evaluation_tracker = ref None
 let create_ctl_evaluation_tracker source_file =
   match (Config.linters_developer_mode, !ctl_evaluation_tracker) with
   | true, None ->
-      ctl_evaluation_tracker := Some (Debug.EvaluationTracker.create source_file)
+      ctl_evaluation_tracker := Some (ALDebugger.EvaluationTracker.create source_file)
   | true, _ ->
       L.(die InternalError) "A CTL evaluation tracker has already been created"
   | _ ->
@@ -590,7 +89,7 @@ let create_ctl_evaluation_tracker source_file =
 let debug_create_payload ast_node phi lcxt =
   match !ctl_evaluation_tracker with
   | Some _ ->
-      Some (Debug.EvaluationTracker.create_content ast_node phi lcxt)
+      Some (ALDebugger.EvaluationTracker.create_content ast_node phi lcxt)
   | None ->
       None
 
@@ -598,7 +97,7 @@ let debug_create_payload ast_node phi lcxt =
 let debug_eval_begin payload =
   match (!ctl_evaluation_tracker, payload) with
   | Some tracker, Some payload ->
-      ctl_evaluation_tracker := Some (Debug.EvaluationTracker.eval_begin tracker payload)
+      ctl_evaluation_tracker := Some (ALDebugger.EvaluationTracker.eval_begin tracker payload)
   | _ ->
       ()
 
@@ -606,7 +105,7 @@ let debug_eval_begin payload =
 let debug_eval_end result =
   match !ctl_evaluation_tracker with
   | Some tracker ->
-      ctl_evaluation_tracker := Some (Debug.EvaluationTracker.eval_end tracker result)
+      ctl_evaluation_tracker := Some (ALDebugger.EvaluationTracker.eval_end tracker result)
   | None ->
       ()
 
@@ -618,7 +117,7 @@ let save_dotty_when_in_debug_mode source_file =
       Utils.create_dir dotty_dir ;
       let source_file_basename = Filename.basename (SourceFile.to_abs_path source_file) in
       let file = dotty_dir ^/ source_file_basename ^ ".dot" in
-      let dotty = Debug.EvaluationTracker.DottyPrinter.dotty_of_ctl_evaluation tracker in
+      let dotty = ALDebugger.EvaluationTracker.DottyPrinter.dotty_of_ctl_evaluation tracker in
       Utils.with_file_out file ~f:(fun oc -> Out_channel.output_string oc dotty)
   | _ ->
       ()
@@ -628,6 +127,7 @@ let save_dotty_when_in_debug_mode source_file =
 (* given a decl returns a stmt such that decl--->stmt via label trs *)
 let transition_decl_to_stmt d trs =
   let open Clang_ast_t in
+  let open CTLTypes in
   let temp_res =
     match (trs, d) with
     | Body, ObjCMethodDecl (_, _, omdi) ->
@@ -962,6 +462,7 @@ let transition_via_sibling node =
 
 (* given a node an returns a list of nodes an' such that an transition to an' via label trans *)
 let next_state_via_transition an trans =
+  let open CTLTypes in
   match (an, trans) with
   | Decl d, Super ->
       transition_decl_to_decl_via_super d
@@ -1285,6 +786,7 @@ and eval_Implies an lcxt f1 f2 =
    such that (an', lcxt) satifies EF phi
 *)
 and eval_EF phi an lcxt trans =
+  let open CTLTypes in
   match (trans, an) with
   | Some _, _ ->
       (* Using equivalence EF[->trans] phi = phi OR EX[->trans](EF[->trans] phi)*)
@@ -1317,7 +819,7 @@ and eval_EX phi an lcxt trans =
         choose_witness_opt (eval_formula phi node lcxt) acc )
   in
   match (witness_opt, trans) with
-  | Some _, Some trans when not (is_transition_to_successor trans) ->
+  | Some _, Some trans when not (CTLTypes.is_transition_to_successor trans) ->
       Some an (* We want to limit the witnesses to the successors of the original node. *)
   | _ ->
       witness_opt
@@ -1330,6 +832,7 @@ and eval_EX phi an lcxt trans =
    an,lcxt satifies the formula phi2 or (phi1 and EX(E(phi1 U phi2)))
 *)
 and eval_EU phi1 phi2 an lcxt trans =
+  let open CTLTypes in
   let f = Or (phi2, And (phi1, EX (trans, EU (trans, phi1, phi2)))) in
   eval_formula f an lcxt
 
@@ -1340,6 +843,7 @@ and eval_EU phi1 phi2 an lcxt trans =
    Same as EU but for the all path quantifier A
 *)
 and eval_AU phi1 phi2 an lcxt trans =
+  let open CTLTypes in
   let f = Or (phi2, And (phi1, AX (trans, AU (trans, phi1, phi2)))) in
   eval_formula f an lcxt
 
@@ -1370,6 +874,7 @@ and in_node node_type_list phi an lctx =
    the node an is in Classes and there exists a declaration d in Hierarchy(an)
    such that d,lcxt |= phi *)
 and eval_EH classes phi an lcxt =
+  let open CTLTypes in
   (* Define EH[Classes] phi = ET[Classes](EF[->Super] phi) *)
   let f = ET (classes, None, EX (Some Super, EF (Some Super, phi))) in
   eval_formula f an lcxt
@@ -1386,6 +891,7 @@ and eval_EH classes phi an lcxt =
    or l is unspecified and an,lcxt |= phi
 *)
 and eval_ET tl trs phi an lcxt =
+  let open CTLTypes in
   let f =
     match trs with
     | Some _ ->
@@ -1412,6 +918,7 @@ and eval_InObjCClass an lcxt f1 f2 =
 
 (* Formulas are evaluated on a AST node an and a linter context lcxt *)
 and eval_formula f an lcxt : Ctl_parser_types.ast_node option =
+  let open CTLTypes in
   debug_eval_begin (debug_create_payload an f lcxt) ;
   let res =
     match f with
diff --git a/infer/src/al/CTL.mli b/infer/src/al/CTL.mli
new file mode 100644
index 000000000..09d0e6c02
--- /dev/null
+++ b/infer/src/al/CTL.mli
@@ -0,0 +1,62 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+(**
+  This module defines a language to define checkers. These checkers are interpreted over the AST of
+  the program. A checker is defined by a CTL formula which expresses a condition saying when the
+  checker should report a problem.
+*)
+
+(**  "set" clauses are used for defining mandatory variables that will be used
+   by when reporting issues: eg for defining the condition.
+
+   "desc" clauses are used for defining the error message,
+   the suggestion, the severity.
+
+   "let" clauses are used to define temporary formulas which are then
+   used to abbreviate the another formula. For example
+
+   let f = a And B
+
+   set formula  = f OR f
+
+   set message = "bla"
+
+*)
+
+type clause =
+  | CLet of ALVar.formula_id * ALVar.t list * CTLTypes.t  (** Let clause: let id = definifion;  *)
+  | CSet of ALVar.keyword * CTLTypes.t  (** Set clause: set id = definition *)
+  | CDesc of ALVar.keyword * string  (** Description clause eg: set message = "..." *)
+  | CPath of [`WhitelistPath | `BlacklistPath] * ALVar.t list
+
+type ctl_checker =
+  {id: string  (** Checker's id *); definitions: clause list  (** A list of let/set definitions *)}
+
+type al_file =
+  { import_files: string list
+  ; global_macros: clause list
+  ; global_paths: (string * ALVar.alexp list) list
+  ; checkers: ctl_checker list }
+
+val print_checker : ctl_checker -> unit
+
+val eval_formula :
+     CTLTypes.t
+  -> Ctl_parser_types.ast_node
+  -> CLintersContext.context
+  -> Ctl_parser_types.ast_node option
+(** return the evaluation of the formula and a witness *)
+
+val save_dotty_when_in_debug_mode : SourceFile.t -> unit
+
+val next_state_via_transition :
+  Ctl_parser_types.ast_node -> CTLTypes.transitions -> Ctl_parser_types.ast_node list
+
+val create_ctl_evaluation_tracker : SourceFile.t -> unit
diff --git a/infer/src/al/CTLTypes.ml b/infer/src/al/CTLTypes.ml
new file mode 100644
index 000000000..695f43db6
--- /dev/null
+++ b/infer/src/al/CTLTypes.ml
@@ -0,0 +1,177 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+(** Transition labels used for example to switch from decl to stmt *)
+type transitions =
+  | AccessorForProperty of ALVar.alexp  (** decl to decl *)
+  | Body  (** decl to stmt *)
+  | FieldName of ALVar.alexp  (** stmt to stmt, decl to decl *)
+  | Fields  (** stmt to stmt, decl to decl *)
+  | InitExpr  (** decl to stmt *)
+  | Super  (** decl to decl *)
+  | ParameterName of ALVar.alexp  (** stmt to stmt, decl to decl *)
+  | ParameterPos of ALVar.alexp  (** stmt to stmt, decl to decl *)
+  | Parameters  (** stmt to stmt, decl to decl *)
+  | Cond
+  | PointerToDecl  (** stmt to decl *)
+  | Protocol  (** decl to decl *)
+  | Sibling  (** decl to decl *)
+  | SourceExpr
+[@@deriving compare]
+
+let is_transition_to_successor trans =
+  match trans with
+  | Body
+  | InitExpr
+  | FieldName _
+  | Fields
+  | ParameterName _
+  | ParameterPos _
+  | Parameters
+  | Cond
+  | SourceExpr ->
+      true
+  | Super | PointerToDecl | Protocol | AccessorForProperty _ | Sibling ->
+      false
+
+
+(* In formulas below prefix
+   "E" means "exists a path"
+   "A" means "for all path" *)
+
+type t =
+  (* A ctl formula *)
+  | True
+  | False
+  (* not really necessary but it makes it evaluation faster *)
+  | Atomic of CPredicates.t
+  | Not of t
+  | And of t * t
+  | Or of t * t
+  | Implies of t * t
+  | InNode of ALVar.alexp list * t
+  | AX of transitions option * t
+  | EX of transitions option * t
+  | AF of transitions option * t
+  | EF of transitions option * t
+  | AG of transitions option * t
+  | EG of transitions option * t
+  | AU of transitions option * t * t
+  | EU of transitions option * t * t
+  | EH of ALVar.alexp list * t
+  | ET of ALVar.alexp list * transitions option * t
+  | InObjCClass of t * t
+[@@deriving compare]
+
+let equal = [%compare.equal: t]
+
+let has_transition phi =
+  match phi with
+  | True | False | Atomic _ | Not _ | And _ | Or _ | Implies _ | InNode _ | EH _ | InObjCClass _ ->
+      false
+  | AX (trans_opt, _)
+  | AF (trans_opt, _)
+  | AG (trans_opt, _)
+  | AU (trans_opt, _, _)
+  | EX (trans_opt, _)
+  | EF (trans_opt, _)
+  | EG (trans_opt, _)
+  | EU (trans_opt, _, _)
+  | ET (_, trans_opt, _) ->
+      Option.is_some trans_opt
+
+
+let pp_transition fmt trans_opt =
+  let pp_aux fmt trans =
+    match trans with
+    | AccessorForProperty kind ->
+        Format.pp_print_string fmt ("AccessorForProperty " ^ ALVar.alexp_to_string kind)
+    | Body ->
+        Format.pp_print_string fmt "Body"
+    | FieldName name ->
+        Format.pp_print_string fmt ("FieldName " ^ ALVar.alexp_to_string name)
+    | Fields ->
+        Format.pp_print_string fmt "Fields"
+    | InitExpr ->
+        Format.pp_print_string fmt "InitExpr"
+    | Super ->
+        Format.pp_print_string fmt "Super"
+    | ParameterName name ->
+        Format.pp_print_string fmt ("ParameterName " ^ ALVar.alexp_to_string name)
+    | ParameterPos pos ->
+        Format.pp_print_string fmt ("ParameterPos " ^ ALVar.alexp_to_string pos)
+    | Parameters ->
+        Format.pp_print_string fmt "Parameters"
+    | Cond ->
+        Format.pp_print_string fmt "Cond"
+    | Protocol ->
+        Format.pp_print_string fmt "Protocol"
+    | PointerToDecl ->
+        Format.pp_print_string fmt "PointerToDecl"
+    | Sibling ->
+        Format.pp_print_string fmt "Sibling"
+    | SourceExpr ->
+        Format.pp_print_string fmt "SourceExpr"
+  in
+  match trans_opt with Some trans -> pp_aux fmt trans | None -> Format.pp_print_char fmt '_'
+
+
+(* a flag to print more or less in the dotty graph *)
+let full_print = true
+
+let rec pp_formula fmt phi =
+  let nodes_to_string nl = List.map ~f:ALVar.alexp_to_string nl in
+  match phi with
+  | True ->
+      Format.pp_print_string fmt "True"
+  | False ->
+      Format.pp_print_string fmt "False"
+  | Atomic p ->
+      CPredicates.pp_predicate fmt p
+  | Not phi ->
+      if full_print then Format.fprintf fmt "NOT(%a)" pp_formula phi
+      else Format.pp_print_string fmt "NOT(...)"
+  | And (phi1, phi2) ->
+      if full_print then Format.fprintf fmt "(%a AND %a)" pp_formula phi1 pp_formula phi2
+      else Format.pp_print_string fmt "(... AND ...)"
+  | Or (phi1, phi2) ->
+      if full_print then Format.fprintf fmt "(%a OR %a)" pp_formula phi1 pp_formula phi2
+      else Format.pp_print_string fmt "(... OR ...)"
+  | Implies (phi1, phi2) ->
+      Format.fprintf fmt "(%a ==> %a)" pp_formula phi1 pp_formula phi2
+  | InNode (nl, phi) ->
+      Format.fprintf fmt "IN-NODE %a: (%a)"
+        (Pp.comma_seq Format.pp_print_string)
+        (nodes_to_string nl) pp_formula phi
+  | AX (trs, phi) ->
+      Format.fprintf fmt "AX[->%a](%a)" pp_transition trs pp_formula phi
+  | EX (trs, phi) ->
+      Format.fprintf fmt "EX[->%a](%a)" pp_transition trs pp_formula phi
+  | AF (trs, phi) ->
+      Format.fprintf fmt "AF[->%a](%a)" pp_transition trs pp_formula phi
+  | EF (trs, phi) ->
+      Format.fprintf fmt "EF[->%a](%a)" pp_transition trs pp_formula phi
+  | AG (trs, phi) ->
+      Format.fprintf fmt "AG[->%a](%a)" pp_transition trs pp_formula phi
+  | EG (trs, phi) ->
+      Format.fprintf fmt "EG[->%a](%a)" pp_transition trs pp_formula phi
+  | AU (trs, phi1, phi2) ->
+      Format.fprintf fmt "A[->%a][%a UNTIL %a]" pp_transition trs pp_formula phi1 pp_formula phi2
+  | EU (trs, phi1, phi2) ->
+      Format.fprintf fmt "E[->%a][%a UNTIL %a]" pp_transition trs pp_formula phi1 pp_formula phi2
+  | EH (arglist, phi) ->
+      Format.fprintf fmt "EH[%a](%a)"
+        (Pp.comma_seq Format.pp_print_string)
+        (nodes_to_string arglist) pp_formula phi
+  | ET (arglist, trans, phi) ->
+      Format.fprintf fmt "ET[%a][%a](%a)"
+        (Pp.comma_seq Format.pp_print_string)
+        (nodes_to_string arglist) pp_transition trans pp_formula phi
+  | InObjCClass (phi1, phi2) ->
+      if full_print then Format.fprintf fmt "InObjCClass(%a, %a)" pp_formula phi1 pp_formula phi2
diff --git a/infer/src/al/cTL.mli b/infer/src/al/CTLTypes.mli
similarity index 59%
rename from infer/src/al/cTL.mli
rename to infer/src/al/CTLTypes.mli
index df0161622..fd9e64ae9 100644
--- a/infer/src/al/cTL.mli
+++ b/infer/src/al/CTLTypes.mli
@@ -5,15 +5,6 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open! IStd
-open Ctl_parser_types
-
-(**
-  This module defines a language to define checkers. These checkers are interpreted over the AST of
-  the program. A checker is defined by a CTL formula which expresses a condition saying when the
-  checker should report a problem.
-*)
-
 (** Transition labels used for example to switch from decl to stmt *)
 type transitions =
   | AccessorForProperty of ALVar.alexp  (** decl to decl *)
@@ -68,53 +59,12 @@ type t =
   | InObjCClass of t * t
 [@@deriving compare]
 
-(* "set" clauses are used for defining mandatory variables that will be used
-   by when reporting issues: eg for defining the condition.
-
-   "desc" clauses are used for defining the error message,
-   the suggestion, the severity.
-
-   "let" clauses are used to define temporary formulas which are then
-   used to abbreviate the another formula. For example
+val is_transition_to_successor : transitions -> bool
 
-   let f = a And B
-
-   set formula  = f OR f
-
-   set message = "bla"
-
-*)
+val has_transition : t -> bool
 
 val equal : t -> t -> bool
 
-type clause =
-  | CLet of ALVar.formula_id * ALVar.t list * t  (** Let clause: let id = definifion;  *)
-  | CSet of ALVar.keyword * t  (** Set clause: set id = definition *)
-  | CDesc of ALVar.keyword * string  (** Description clause eg: set message = "..." *)
-  | CPath of [`WhitelistPath | `BlacklistPath] * ALVar.t list
-
-type ctl_checker =
-  {id: string  (** Checker's id *); definitions: clause list  (** A list of let/set definitions *)}
-
-type al_file =
-  { import_files: string list
-  ; global_macros: clause list
-  ; global_paths: (string * ALVar.alexp list) list
-  ; checkers: ctl_checker list }
-
-val print_checker : ctl_checker -> unit
-
-val eval_formula : t -> ast_node -> CLintersContext.context -> ast_node option
-(** return the evaluation of the formula and a witness *)
-
-val save_dotty_when_in_debug_mode : SourceFile.t -> unit
-
-val next_state_via_transition : ast_node -> transitions -> ast_node list
-
-val create_ctl_evaluation_tracker : SourceFile.t -> unit
-
-module Debug : sig
-  val pp_formula : Format.formatter -> t -> unit
+val pp_transition : Format.formatter -> transitions option -> unit
 
-  val pp_transition : Format.formatter -> transitions option -> unit
-end
+val pp_formula : Format.formatter -> t -> unit
diff --git a/infer/src/al/ctl_parser.mly b/infer/src/al/ctl_parser.mly
index 1a5acd39b..e21a5fb2b 100644
--- a/infer/src/al/ctl_parser.mly
+++ b/infer/src/al/ctl_parser.mly
@@ -216,10 +216,10 @@ let_clause:
   ;
 
 atomic_formula:
-  | TRUE { L.(debug Linters Verbose) "\tParsed True@\n"; CTL.True }
-  | FALSE { L.(debug Linters Verbose) "\tParsed False@\n"; CTL.False }
+  | TRUE { L.(debug Linters Verbose) "\tParsed True@\n"; CTLTypes.True }
+  | FALSE { L.(debug Linters Verbose) "\tParsed False@\n"; CTLTypes.False }
   | identifier LEFT_PAREN actual_params RIGHT_PAREN
-    { L.(debug Linters Verbose) "\tParsed predicate@\n"; CTL.Atomic(ALVar.Formula_id $1, $3) }
+    { L.(debug Linters Verbose) "\tParsed predicate@\n"; CTLTypes.Atomic(ALVar.Formula_id $1, $3) }
   ;
 
   formula_id_def:
@@ -240,20 +240,20 @@ actual_params:
   ;
 
 transition_label:
-  | ACCESSOR_FOR_PROPERTY alexp { Some (CTL.AccessorForProperty $2) }
+  | ACCESSOR_FOR_PROPERTY alexp { Some (CTLTypes.AccessorForProperty $2) }
   | ANY { None }
-  | BODY { Some CTL.Body }
-  | COND { Some CTL.Cond }
-  | FIELDS { Some CTL.Fields }
-  | FIELD_NAME alexp { Some (CTL.FieldName $2) }
-  | INIT_EXPR { Some CTL.InitExpr }
-  | PARAMETERS { Some CTL.Parameters }
-  | PARAMETER_NAME alexp { Some (CTL.ParameterName $2) }
-  | PARAMETER_POS alexp { Some (CTL.ParameterPos $2) }
-  | POINTER_TO_DECL { Some CTL.PointerToDecl }
-  | PROTOCOL { Some CTL.Protocol }
-  | SIBLING { Some CTL.Sibling}
-  | SOURCE_EXPR { Some CTL.SourceExpr}
+  | BODY { Some CTLTypes.Body }
+  | COND { Some CTLTypes.Cond }
+  | FIELDS { Some CTLTypes.Fields }
+  | FIELD_NAME alexp { Some (CTLTypes.FieldName $2) }
+  | INIT_EXPR { Some CTLTypes.InitExpr }
+  | PARAMETERS { Some CTLTypes.Parameters }
+  | PARAMETER_NAME alexp { Some (CTLTypes.ParameterName $2) }
+  | PARAMETER_POS alexp { Some (CTLTypes.ParameterPos $2) }
+  | POINTER_TO_DECL { Some CTLTypes.PointerToDecl }
+  | PROTOCOL { Some CTLTypes.Protocol }
+  | SIBLING { Some CTLTypes.Sibling}
+  | SOURCE_EXPR { Some CTLTypes.SourceExpr}
   ;
 
 formula_EF:
@@ -268,50 +268,50 @@ when_formula:
 | INTERFACE  LEFT_SQBRACE formula RIGHT_SQBRACE
   IMPLEMENTATION LEFT_SQBRACE formula RIGHT_SQBRACE HOLDS_IN_OBJCCLASS
    { L.(debug Linters Verbose) "\tParsed HOLDS-IN-OBJC-CLASS @\n";
-        CTL.InObjCClass ($3, $7) }
+        CTLTypes.InObjCClass ($3, $7) }
 | formula HOLDS_IN_NODE node_list
-     { L.(debug Linters Verbose) "\tParsed InNode@\n"; CTL.InNode ($3, $1)}
+     { L.(debug Linters Verbose) "\tParsed InNode@\n"; CTLTypes.InNode ($3, $1)}
 ;
 
 
 formula:
   | formula_with_paren { $1 }
-  | formula_id { CTL.Atomic($1, []) }
+  | formula_id { CTLTypes.Atomic($1, []) }
   | atomic_formula { L.(debug Linters Verbose) "\tParsed atomic formula@\n"; $1 }
-  | formula EU formula { L.(debug Linters Verbose) "\tParsed EU@\n"; CTL.EU (None, $1, $3) }
-  | formula AU formula { L.(debug Linters Verbose) "\tParsed AU@\n"; CTL.AU (None,$1, $3) }
-  | formula AF { L.(debug Linters Verbose) "\tParsed AF@\n"; CTL.AF (None,$1) }
-  | formula EX { L.(debug Linters Verbose) "\tParsed EX@\n"; CTL.EX (None, $1) }
+  | formula EU formula { L.(debug Linters Verbose) "\tParsed EU@\n"; CTLTypes.EU (None, $1, $3) }
+  | formula AU formula { L.(debug Linters Verbose) "\tParsed AU@\n"; CTLTypes.AU (None,$1, $3) }
+  | formula AF { L.(debug Linters Verbose) "\tParsed AF@\n"; CTLTypes.AF (None,$1) }
+  | formula EX { L.(debug Linters Verbose) "\tParsed EX@\n"; CTLTypes.EX (None, $1) }
   | formula EX WITH_TRANSITION transition_label
-     { L.(debug Linters Verbose) "\tParsed EX WITH-TRANSITION '%a'@\n" CTL.Debug.pp_transition $4;
-       CTL.EX ($4, $1) }
-  | formula AX { L.(debug Linters Verbose) "\tParsed AX@\n"; CTL.AX (None, $1) }
+     { L.(debug Linters Verbose) "\tParsed EX WITH-TRANSITION '%a'@\n" CTLTypes.pp_transition $4;
+       CTLTypes.EX ($4, $1) }
+  | formula AX { L.(debug Linters Verbose) "\tParsed AX@\n"; CTLTypes.AX (None, $1) }
   | formula AX WITH_TRANSITION transition_label
-     { L.(debug Linters Verbose) "\tParsed AX WITH-TRANSITION '%a'@\n" CTL.Debug.pp_transition $4;
-       CTL.AX ($4, $1) }
-  | formula EG { L.(debug Linters Verbose) "\tParsed EG@\n"; CTL.EG (None, $1) }
-  | formula AG { L.(debug Linters Verbose) "\tParsed AG@\n"; CTL.AG (None, $1) }
-  | formula EH node_list { L.(debug Linters Verbose) "\tParsed EH@\n"; CTL.EH ($3, $1) }
-  | formula EF { L.(debug Linters Verbose) "\tParsed EF@\n"; CTL.EF (None, $1) }
+     { L.(debug Linters Verbose) "\tParsed AX WITH-TRANSITION '%a'@\n" CTLTypes.pp_transition $4;
+       CTLTypes.AX ($4, $1) }
+  | formula EG { L.(debug Linters Verbose) "\tParsed EG@\n"; CTLTypes.EG (None, $1) }
+  | formula AG { L.(debug Linters Verbose) "\tParsed AG@\n"; CTLTypes.AG (None, $1) }
+  | formula EH node_list { L.(debug Linters Verbose) "\tParsed EH@\n"; CTLTypes.EH ($3, $1) }
+  | formula EF { L.(debug Linters Verbose) "\tParsed EF@\n"; CTLTypes.EF (None, $1) }
   | formula EF WITH_TRANSITION transition_label
-     { L.(debug Linters Verbose) "\tParsed EF WITH-TRANSITION '%a'@\n" CTL.Debug.pp_transition $4;
-       CTL.EF($4, $1) }
+     { L.(debug Linters Verbose) "\tParsed EF WITH-TRANSITION '%a'@\n" CTLTypes.pp_transition $4;
+       CTLTypes.EF($4, $1) }
   | WHEN when_formula { $2 }
   | ET node_list WITH_TRANSITION transition_label formula_EF
-     { L.(debug Linters Verbose) "\tParsed ET with transition '%a'@\n" CTL.Debug.pp_transition $4;
-       CTL.ET ($2, $4, $5)}
+     { L.(debug Linters Verbose) "\tParsed ET with transition '%a'@\n" CTLTypes.pp_transition $4;
+       CTLTypes.ET ($2, $4, $5)}
   | EX WITH_TRANSITION transition_label formula_with_paren
-    { L.(debug Linters Verbose) "\tParsed EX with transition '%a'@\n" CTL.Debug.pp_transition $3;
-      CTL.EX ($3, $4)}
+    { L.(debug Linters Verbose) "\tParsed EX with transition '%a'@\n" CTLTypes.pp_transition $3;
+      CTLTypes.EX ($3, $4)}
   | AX WITH_TRANSITION transition_label formula_with_paren
       { L.(debug Linters Verbose)
-        "\tParsed AX with transition '%a'@\n" CTL.Debug.pp_transition $3;
-        CTL.AX ($3, $4)}
-  | formula AND formula { L.(debug Linters Verbose) "\tParsed AND@\n"; CTL.And ($1, $3) }
-  | formula OR formula { L.(debug Linters Verbose) "\tParsed OR@\n"; CTL.Or ($1, $3) }
+        "\tParsed AX with transition '%a'@\n" CTLTypes.pp_transition $3;
+        CTLTypes.AX ($3, $4)}
+  | formula AND formula { L.(debug Linters Verbose) "\tParsed AND@\n"; CTLTypes.And ($1, $3) }
+  | formula OR formula { L.(debug Linters Verbose) "\tParsed OR@\n"; CTLTypes.Or ($1, $3) }
   | formula IMPLIES formula
-      { L.(debug Linters Verbose) "\tParsed IMPLIES@\n"; CTL.Implies ($1, $3) }
-  | NOT formula { L.(debug Linters Verbose) "\tParsed NOT@\n"; CTL.Not ($2) }
+      { L.(debug Linters Verbose) "\tParsed IMPLIES@\n"; CTLTypes.Implies ($1, $3) }
+  | NOT formula { L.(debug Linters Verbose) "\tParsed NOT@\n"; CTLTypes.Not ($2) }
 ;