diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt
index 716490984..4b1945f11 100644
--- a/infer/man/man1/infer-full.txt
+++ b/infer/man/man1/infer-full.txt
@@ -1948,7 +1948,15 @@ INTERNAL OPTIONS
 
        --topl-properties +path
            [EXPERIMENTAL] Specify a file containing a temporal property
-           definition (e.g., jdk.topl).
+           definition (e.g., jdk.topl).           One needs to also select one of the three implementations, by
+           enabling one of the following checkers
+           --pulse       will run pulse with updated transfer functions
+           --topl-pulse  [SLOW] uses SIL-instrumentation, runs pulse, and
+           analyzes pulse summaries
+           --topl-biabd  [SLOW] uses SIL-instrumentation, runs biabduction,
+           and analyzes biabduction summaries
+           Note that enabling topl-pulse or topl-biabd will disable the
+           first implementation using updated pulse transfer functions.
 
        --topl-properties-reset
            Set --topl-properties to the empty list.
diff --git a/infer/src/backend/InferAnalyze.ml b/infer/src/backend/InferAnalyze.ml
index 55274ab9c..4d8af69da 100644
--- a/infer/src/backend/InferAnalyze.ml
+++ b/infer/src/backend/InferAnalyze.ml
@@ -45,12 +45,12 @@ let proc_name_of_uid =
 
 let analyze_target : (TaskSchedulerTypes.target, string) Tasks.doer =
   let analyze_source_file exe_env source_file =
-    if Topl.is_active () then DB.Results_dir.init (Topl.sourcefile ()) ;
+    if Topl.is_shallow_active () then DB.Results_dir.init (Topl.sourcefile ()) ;
     DB.Results_dir.init source_file ;
     L.task_progress SourceFile.pp source_file ~f:(fun () ->
         try
           Ondemand.analyze_file exe_env source_file ;
-          if Topl.is_active () && Config.debug_mode then
+          if Topl.is_shallow_active () && Config.debug_mode then
             DotCfg.emit_frontend_cfg (Topl.sourcefile ()) (Topl.cfg ()) ;
           if Config.write_html then Printer.write_all_html_files source_file ;
           None
diff --git a/infer/src/backend/registerCheckers.ml b/infer/src/backend/registerCheckers.ml
index 4390d0c99..5023eadc0 100644
--- a/infer/src/backend/registerCheckers.ml
+++ b/infer/src/backend/registerCheckers.ml
@@ -148,7 +148,7 @@ let all_checkers =
   ; { checker= Pulse
     ; callbacks=
         (let checker =
-           if Config.is_checker_enabled ToplOnPulse then Topl.analyze_with_pulse Pulse.checker
+           if Config.is_checker_enabled ToplOnPulse then PulseToplShallow.analyze Pulse.checker
            else Pulse.checker
          in
          let pulse = interprocedural Payloads.Fields.pulse checker in
diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml
index db7576bef..bd5f5c8f4 100644
--- a/infer/src/base/Config.ml
+++ b/infer/src/base/Config.ml
@@ -2313,7 +2313,15 @@ and test_filtering =
 
 and topl_properties =
   CLOpt.mk_path_list ~default:[] ~long:"topl-properties"
-    "[EXPERIMENTAL] Specify a file containing a temporal property definition (e.g., jdk.topl)."
+    "[EXPERIMENTAL] Specify a file containing a temporal property definition (e.g., jdk.topl).\n\
+     One needs to also select one of the three implementations, by enabling one of the following \
+     checkers\n\
+     $(b,--pulse)       will run pulse with updated transfer functions\n\
+     $(b,--topl-pulse)  [SLOW] uses SIL-instrumentation, runs pulse, and analyzes pulse summaries\n\
+     $(b,--topl-biabd)  [SLOW] uses SIL-instrumentation, runs biabduction, and analyzes \
+     biabduction summaries\n\
+     Note that enabling topl-pulse or topl-biabd will disable the first implementation using \
+     updated pulse transfer functions."
 
 
 and profiler_samples =
diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml
index 0abb88836..38f198955 100644
--- a/infer/src/pulse/Pulse.ml
+++ b/infer/src/pulse/Pulse.ml
@@ -92,6 +92,26 @@ module PulseTransferFunctions = struct
         Ok exec_state
 
 
+  let topl_small_step arguments (return, _typ) exec_state_res =
+    let arguments =
+      List.map arguments ~f:(fun {ProcnameDispatcher.Call.FuncArg.arg_payload} -> fst arg_payload)
+    in
+    let return = Var.of_id return in
+    let do_astate astate =
+      let return = Option.map ~f:fst (Stack.find_opt return astate) in
+      let topl_event = PulseTopl.Call {return; arguments} in
+      AbductiveDomain.Topl.small_step topl_event astate
+    in
+    let do_one_exec_state (exec_state : Domain.t) : Domain.t =
+      match exec_state with
+      | ContinueProgram astate ->
+          ContinueProgram (do_astate astate)
+      | AbortProgram _ | LatentAbortProgram _ | ExitProgram _ ->
+          exec_state
+    in
+    Result.map ~f:(List.map ~f:do_one_exec_state) exec_state_res
+
+
   let dispatch_call ({InterproceduralAnalysis.tenv} as analysis_data) ret call_exp actuals call_loc
       flags astate =
     (* evaluate all actuals *)
@@ -132,6 +152,10 @@ module PulseTransferFunctions = struct
           PerfEvent.(log (fun logger -> log_end_event logger ())) ;
           r
     in
+    let exec_state_res =
+      if Topl.is_deep_active () then topl_small_step func_args ret exec_state_res
+      else exec_state_res
+    in
     match get_out_of_scope_object call_exp actuals flags with
     | Some pvar_typ ->
         L.d_printfln "%a is going out of scope" Pvar.pp_value (fst pvar_typ) ;
diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index 3367aa27a..22fae223c 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -81,6 +81,7 @@ module PreDomain : BaseDomainSig = PostDomain
 type t =
   { post: PostDomain.t  (** state at the current program point*)
   ; pre: PreDomain.t  (** inferred pre at the current program point *)
+  ; topl: (PulseTopl.state[@yojson.opaque])
   ; skipped_calls: SkippedCalls.t  (** set of skipped calls *)
   ; path_condition: PathCondition.t }
 [@@deriving yojson_of]
@@ -140,6 +141,7 @@ module Stack = struct
         in
         ( { post= PostDomain.update astate.post ~stack:post_stack
           ; pre
+          ; topl= astate.topl
           ; skipped_calls= astate.skipped_calls
           ; path_condition= astate.path_condition }
         , addr_hist )
@@ -288,6 +290,7 @@ module Memory = struct
         in
         ( { post= PostDomain.update astate.post ~heap:post_heap
           ; pre= PreDomain.update astate.pre ~heap:foot_heap
+          ; topl= astate.topl
           ; skipped_calls= astate.skipped_calls
           ; path_condition= astate.path_condition }
         , addr_hist_dst )
@@ -326,7 +329,11 @@ let mk_initial proc_desc =
     PreDomain.update ~stack:initial_stack ~heap:initial_heap PreDomain.empty
   in
   let post = PostDomain.update ~stack:initial_stack PostDomain.empty in
-  {pre; post; skipped_calls= SkippedCalls.empty; path_condition= PathCondition.true_}
+  { pre
+  ; post
+  ; topl= PulseTopl.start ()
+  ; skipped_calls= SkippedCalls.empty
+  ; path_condition= PathCondition.true_ }
 
 
 let add_skipped_call pname trace astate =
@@ -479,3 +486,10 @@ let summary_of_post pdesc astate =
 let get_pre {pre} = (pre :> BaseDomain.t)
 
 let get_post {post} = (post :> BaseDomain.t)
+
+module Topl = struct
+  let small_step event astate =
+    {astate with topl= PulseTopl.small_step astate.path_condition event astate.topl}
+
+  (* TODO: large_step *)
+end
diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli
index 302a0d4c5..04a5faac5 100644
--- a/infer/src/pulse/PulseAbductiveDomain.mli
+++ b/infer/src/pulse/PulseAbductiveDomain.mli
@@ -56,6 +56,7 @@ module PreDomain : BaseDomainSig
 type t = private
   { post: PostDomain.t  (** state at the current program point*)
   ; pre: PreDomain.t  (** inferred pre at the current program point *)
+  ; topl: PulseTopl.state  (** state at of the Topl monitor at the current program point *)
   ; skipped_calls: SkippedCalls.t  (** set of skipped calls *)
   ; path_condition: PathCondition.t  (** arithmetic facts *) }
 
@@ -178,3 +179,7 @@ val incorporate_new_eqs : t -> PathCondition.t * PathCondition.new_eqs -> PathCo
     e.g. [x = 0] is not compatible with [x] being allocated, and [x = y] is not compatible with [x]
     and [y] being allocated separately. In those cases, the resulting path condition is
     {!PathCondition.false_}. *)
+
+module Topl : sig
+  val small_step : PulseTopl.event -> t -> t
+end
diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml
index 9bd73c105..686ca6641 100644
--- a/infer/src/pulse/PulseInterproc.ml
+++ b/infer/src/pulse/PulseInterproc.ml
@@ -115,11 +115,12 @@ let visit call_state ~pre ~addr_callee ~addr_hist_caller =
       ; rev_subst= AddressMap.add addr_caller addr_callee call_state.rev_subst } )
 
 
-let pp f {AbductiveDomain.pre; post; path_condition; skipped_calls} =
+let pp f {AbductiveDomain.pre; post; topl; path_condition; skipped_calls} =
   F.fprintf f "COND:@\n  @[%a@]@\n" PathCondition.pp path_condition ;
   F.fprintf f "PRE:@\n  @[%a@]@\n" BaseDomain.pp (pre :> BaseDomain.t) ;
   F.fprintf f "POST:@\n  @[%a@]@\n" BaseDomain.pp (post :> BaseDomain.t) ;
-  F.fprintf f "SKIPPED_CALLS:@ @[%a@]@\n" SkippedCalls.pp skipped_calls
+  F.fprintf f "SKIPPED_CALLS:@ @[%a@]@\n" SkippedCalls.pp skipped_calls ;
+  F.fprintf f "TOPL:@\n @[%a@]@\n" PulseTopl.pp_state topl
 
 
 (* {3 reading the pre from the current state} *)
diff --git a/infer/src/pulse/PulseTopl.ml b/infer/src/pulse/PulseTopl.ml
new file mode 100644
index 000000000..bf9d22533
--- /dev/null
+++ b/infer/src/pulse/PulseTopl.ml
@@ -0,0 +1,38 @@
+(*
+ * 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
+open PulseBasicInterface
+
+type value = AbstractValue.t
+
+type event = Call of {return: value option; arguments: value list}
+
+type vertex = string
+
+type register = string
+
+type configuration = {vertex: vertex; memory: (register * value) list}
+
+(** Let P be the [path_condition] in the enclosing pulse state, and let Q be the [path_condition] in
+    the [simple_state] below. Then, the facts we know are P∧Q, and it should be that ∃V P∧Q,
+    where V are the abstract values mentioned in the pre/post-configurations of the simple state, is
+    equivalent to P. In other words, the facts in Q should not constrain program variables but may
+    constrain Topl registers. *)
+type simple_state =
+  { pre: configuration  (** at the start of the procedure *)
+  ; post: configuration  (** at the current program point *)
+  ; path_condition: PathCondition.t }
+
+(* TODO: include a hash of the automaton in a summary to avoid caching problems. *)
+type state = simple_state list
+
+let start () = (* TODO *) []
+
+let small_step _condition _event state = (* TODO *) state
+
+let pp_state _formatter _state = (* TODO *) ()
diff --git a/infer/src/pulse/PulseTopl.mli b/infer/src/pulse/PulseTopl.mli
new file mode 100644
index 000000000..20bf88513
--- /dev/null
+++ b/infer/src/pulse/PulseTopl.mli
@@ -0,0 +1,21 @@
+(*
+ * 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
+
+type value = PulseAbstractValue.t
+
+type event = Call of {return: value option; arguments: value list}
+
+type state
+
+val start : unit -> state
+(** Return the initial state of [Topl.automaton ()]. *)
+
+val small_step : PulsePathCondition.t -> event -> state -> state
+
+val pp_state : Format.formatter -> state -> unit
diff --git a/infer/src/pulse/PulseToplShallow.ml b/infer/src/pulse/PulseToplShallow.ml
new file mode 100644
index 000000000..64508f0e2
--- /dev/null
+++ b/infer/src/pulse/PulseToplShallow.ml
@@ -0,0 +1,56 @@
+(*
+ * 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
+
+let add_errors {InterproceduralAnalysis.proc_desc; err_log} (pulse_summary : PulseSummary.t) =
+  let pulse_summary =
+    let f = function PulseExecutionDomain.ContinueProgram s -> Some s | _ -> None in
+    List.filter_map ~f (pulse_summary :> PulseExecutionDomain.t list)
+  in
+  let proc_name = Procdesc.get_proc_name proc_desc in
+  if not (ToplUtils.is_synthesized proc_name) then
+    let start_to_error =
+      Topl.automaton () |> ToplAutomaton.get_start_error_pairs |> Int.Table.of_alist_exn
+    in
+    let topl_property_var = Var.of_pvar ToplUtils.topl_class_pvar in
+    let topl_state_field = HilExp.Access.FieldAccess (ToplUtils.make_field ToplName.state) in
+    let check_pre_post pre_post =
+      let open IOption.Let_syntax in
+      let path_condition = pre_post.PulseAbductiveDomain.path_condition in
+      let get_topl_state_opt pulse_state =
+        let stack = pulse_state.PulseBaseDomain.stack in
+        let heap = pulse_state.PulseBaseDomain.heap in
+        let* topl_property_addr, _ = PulseBaseStack.find_opt topl_property_var stack in
+        let* state_addr, _ =
+          PulseBaseMemory.find_edge_opt topl_property_addr topl_state_field heap
+        in
+        let* state_val, _ =
+          PulseBaseMemory.find_edge_opt state_addr HilExp.Access.Dereference heap
+        in
+        PulsePathCondition.as_int path_condition state_val
+      in
+      let* pre_topl = get_topl_state_opt (pre_post.PulseAbductiveDomain.pre :> PulseBaseDomain.t) in
+      let* post_topl =
+        get_topl_state_opt (pre_post.PulseAbductiveDomain.post :> PulseBaseDomain.t)
+      in
+      let* error_topl = Int.Table.find start_to_error pre_topl in
+      if Int.equal post_topl error_topl then Some error_topl else None
+    in
+    let errors = List.filter_map ~f:check_pre_post pulse_summary in
+    let errors = Int.Set.to_list (Int.Set.of_list errors) in
+    let loc = Procdesc.get_loc proc_desc in
+    let report error_state =
+      let m =
+        Format.asprintf "%a" ToplAutomaton.pp_message_of_state (Topl.automaton (), error_state)
+      in
+      Reporting.log_issue proc_desc err_log ToplOnPulse IssueType.topl_pulse_error ~loc m
+    in
+    List.iter ~f:report errors
+
+
+let analyze pulse analysis_data = Topl.analyze_with add_errors pulse analysis_data
diff --git a/infer/src/pulse/PulseToplShallow.mli b/infer/src/pulse/PulseToplShallow.mli
new file mode 100644
index 000000000..1610d9099
--- /dev/null
+++ b/infer/src/pulse/PulseToplShallow.mli
@@ -0,0 +1,12 @@
+(*
+ * 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
+
+val analyze : PulseSummary.t Topl.analysis_transformer
+(** Run pulse with Topl instrumentation if active. Inserts calls to the Topl automaton. Mutates the
+    arguments: it is the caller's responsibility to instrument procedures at most once. *)
diff --git a/infer/src/pulse/dune b/infer/src/pulse/dune
index 1782cb272..4a93d2976 100644
--- a/infer/src/pulse/dune
+++ b/infer/src/pulse/dune
@@ -8,7 +8,7 @@
  (public_name infer.Pulselib)
  (flags
   (:standard -open Core -open IR -open IStdlib -open IStd -open ATDGenerated
-    -open IBase -open Absint -open BO))
- (libraries core IStdlib ATDGenerated IBase IR Absint BO)
+    -open IBase -open Absint -open BO -open TOPLlib))
+ (libraries core IStdlib ATDGenerated IBase IR Absint BO TOPLlib)
  (preprocess
   (pps ppx_yojson_conv ppx_compare ppx_variants_conv)))
diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml
index a5d30c4ef..7cf680128 100644
--- a/infer/src/topl/Topl.ml
+++ b/infer/src/topl/Topl.ml
@@ -27,11 +27,20 @@ let properties = lazy (List.concat_map ~f:parse Config.topl_properties)
 
 let automaton = lazy (ToplAutomaton.make (Lazy.force properties))
 
-let is_active () = not (List.is_empty (Lazy.force properties))
+let is_shallow_requested () =
+  Config.is_checker_enabled Checker.ToplOnBiabduction
+  || Config.is_checker_enabled Checker.ToplOnPulse
+
+
+let is_shallow_active () = is_shallow_requested () && not (List.is_empty (Lazy.force properties))
+
+let is_deep_active () =
+  (not (is_shallow_requested ())) && not (List.is_empty (Lazy.force properties))
+
 
 let get_proc_desc proc_name =
   (* Avoid calling [ToplMonitor.generate] when inactive to avoid side-effects. *)
-  if is_active () then ToplMonitor.generate (Lazy.force automaton) proc_name else None
+  if is_shallow_active () then ToplMonitor.generate (Lazy.force automaton) proc_name else None
 
 
 let get_proc_attr proc_name =
@@ -227,11 +236,6 @@ let conjoin_props env post pre =
   List.fold ~init:post ~f:(Prop.prop_atom_and env) (Prop.get_pure pre)
 
 
-let message_of_state state =
-  let property, _vname = ToplAutomaton.vname (Lazy.force automaton) state in
-  Printf.sprintf "property %s reaches error" property
-
-
 (** For each (pre, post) pair of symbolic heaps and each (start, error) pair of Topl automata
     states, define
 
@@ -284,7 +288,9 @@ let add_errors_biabduction {InterproceduralAnalysis.proc_desc; tenv; err_log} bi
             let phi = conjoin_props tenv post pre_start in
             let psi = Prop.conjoin_neq tenv error_exp state_post_value phi in
             if (not (is_inconsistent tenv phi)) && is_inconsistent tenv psi then (
-              let message = message_of_state error in
+              let message =
+                Format.asprintf "%a" ToplAutomaton.pp_message_of_state (Lazy.force automaton, error)
+              in
               tt "WARN@\n" ;
               Reporting.log_issue proc_desc err_log ToplOnBiabduction IssueType.topl_biabd_error
                 ~loc message )
@@ -304,69 +310,32 @@ let add_errors_biabduction {InterproceduralAnalysis.proc_desc; tenv; err_log} bi
     List.iter ~f:handle_preposts preposts
 
 
-let add_errors_pulse {InterproceduralAnalysis.proc_desc; err_log} (pulse_summary : PulseSummary.t) =
-  let pulse_summary =
-    let f = function PulseExecutionDomain.ContinueProgram s -> Some s | _ -> None in
-    List.filter_map ~f (pulse_summary :> PulseExecutionDomain.t list)
-  in
-  let proc_name = Procdesc.get_proc_name proc_desc in
-  if not (ToplUtils.is_synthesized proc_name) then
-    let start_to_error =
-      Lazy.force automaton |> ToplAutomaton.get_start_error_pairs |> Int.Table.of_alist_exn
-    in
-    let topl_property_var = Var.of_pvar ToplUtils.topl_class_pvar in
-    let topl_state_field = HilExp.Access.FieldAccess (ToplUtils.make_field ToplName.state) in
-    let check_pre_post pre_post =
-      let open IOption.Let_syntax in
-      let path_condition = pre_post.PulseAbductiveDomain.path_condition in
-      let get_topl_state_opt pulse_state =
-        let stack = pulse_state.PulseBaseDomain.stack in
-        let heap = pulse_state.PulseBaseDomain.heap in
-        let* topl_property_addr, _ = PulseBaseStack.find_opt topl_property_var stack in
-        let* state_addr, _ =
-          PulseBaseMemory.find_edge_opt topl_property_addr topl_state_field heap
-        in
-        let* state_val, _ =
-          PulseBaseMemory.find_edge_opt state_addr HilExp.Access.Dereference heap
-        in
-        PulsePathCondition.as_int path_condition state_val
-      in
-      let* pre_topl = get_topl_state_opt (pre_post.PulseAbductiveDomain.pre :> PulseBaseDomain.t) in
-      let* post_topl =
-        get_topl_state_opt (pre_post.PulseAbductiveDomain.post :> PulseBaseDomain.t)
-      in
-      let* error_topl = Int.Table.find start_to_error pre_topl in
-      if Int.equal post_topl error_topl then Some error_topl else None
-    in
-    let errors = List.filter_map ~f:check_pre_post pulse_summary in
-    let errors = Int.Set.to_list (Int.Set.of_list errors) in
-    let loc = Procdesc.get_loc proc_desc in
-    let report error_state =
-      let m = message_of_state error_state in
-      Reporting.log_issue proc_desc err_log ToplOnPulse IssueType.topl_pulse_error ~loc m
-    in
-    List.iter ~f:report errors
-
-
 let sourcefile () =
-  if not (is_active ()) then L.die InternalError "Called Topl.sourcefile when Topl is inactive" ;
+  if not (is_shallow_active ()) then
+    L.die InternalError "Called Topl.sourcefile when Topl is inactive" ;
   ToplMonitor.sourcefile ()
 
 
 let cfg () =
-  if not (is_active ()) then L.die InternalError "Called Topl.cfg when Topl is inactive" ;
+  if not (is_shallow_active ()) then L.die InternalError "Called Topl.cfg when Topl is inactive" ;
   ToplMonitor.cfg ()
 
 
-let analyze_with analyze postprocess analysis_data =
-  if is_active () then instrument analysis_data ;
+let analyze_with postprocess analyze analysis_data =
+  if is_shallow_active () then instrument analysis_data ;
   let summary = analyze analysis_data in
-  if is_active () then Option.iter ~f:(postprocess analysis_data) summary ;
+  if is_shallow_active () then Option.iter ~f:(postprocess analysis_data) summary ;
   summary
 
 
 let analyze_with_biabduction biabduction analysis_data =
-  analyze_with biabduction add_errors_biabduction analysis_data
+  analyze_with add_errors_biabduction biabduction analysis_data
+
+
+let automaton () = Lazy.force automaton
+
+type 'summary analysis = 'summary InterproceduralAnalysis.t -> 'summary option
 
+type 'summary postprocess = 'summary InterproceduralAnalysis.t -> 'summary -> unit
 
-let analyze_with_pulse pulse analysis_data = analyze_with pulse add_errors_pulse analysis_data
+type 'summary analysis_transformer = 'summary analysis -> 'summary analysis
diff --git a/infer/src/topl/Topl.mli b/infer/src/topl/Topl.mli
index 26e3de856..33120403c 100644
--- a/infer/src/topl/Topl.mli
+++ b/infer/src/topl/Topl.mli
@@ -7,14 +7,20 @@
 
 open! IStd
 
-val is_active : unit -> bool
-(** Returns whether the TOPL analysis is active. *)
+val automaton : unit -> ToplAutomaton.t
+(** Return the automaton representing all Topl properties. *)
+
+val is_shallow_active : unit -> bool
+(** Return whether the Topl based on Sil instrumentation is active. *)
+
+val is_deep_active : unit -> bool
+(** Return whether PulseTopl is active. *)
 
 val get_proc_attr : Procname.t -> ProcAttributes.t option
 (** [get_proc_attr proc_name] returns the attributes of [get_proc_desc proc_name] *)
 
 val get_proc_desc : Procname.t -> Procdesc.t option
-(** Returns a synthesized Procdesc.t, when it corresponds to instrumentation for a TOPL property. *)
+(** Return a synthesized Procdesc.t, when it corresponds to instrumentation for a TOPL property. *)
 
 val sourcefile : unit -> SourceFile.t
 (** The (fake) sourcefile in which synthesized code resides. This function has a side-effect,
@@ -24,16 +30,16 @@ val cfg : unit -> Cfg.t
 (** The CFG of the synthesized code. This function has a side-effect, because that's how [Cfg]
     works, so do NOT call when Topl is inactive.*)
 
-val analyze_with_biabduction :
-     (BiabductionSummary.t InterproceduralAnalysis.t -> BiabductionSummary.t option)
-  -> BiabductionSummary.t InterproceduralAnalysis.t
-  -> BiabductionSummary.t option
+type 'summary analysis = 'summary InterproceduralAnalysis.t -> 'summary option
+
+type 'summary postprocess = 'summary InterproceduralAnalysis.t -> 'summary -> unit
+
+type 'summary analysis_transformer = 'summary analysis -> 'summary analysis
+
+val analyze_with : 'summary postprocess -> 'summary analysis_transformer
+(** [analyze_with analyze postprocess analysis_data] calls [analyze] and then [postprocess] on
+    [analysis_data] *)
+
+val analyze_with_biabduction : BiabductionSummary.t analysis_transformer
 (** Run biabduction with Topl instrumentation if active. Inserts calls to the TOPL automaton.
     Mutates the arguments: it is the caller's responsibility to instrument procedures at most once. *)
-
-val analyze_with_pulse :
-     (PulseSummary.t InterproceduralAnalysis.t -> PulseSummary.t option)
-  -> PulseSummary.t InterproceduralAnalysis.t
-  -> PulseSummary.t option
-(** Run pulse with Topl instrumentation if active. Inserts calls to the TOPL automaton. Mutates the
-    arguments: it is the caller's responsibility to instrument procedures at most once. *)
diff --git a/infer/src/topl/ToplAutomaton.ml b/infer/src/topl/ToplAutomaton.ml
index ab04209f9..4c68dcdb8 100644
--- a/infer/src/topl/ToplAutomaton.ml
+++ b/infer/src/topl/ToplAutomaton.ml
@@ -164,3 +164,8 @@ let get_start_error_pairs a =
   let f ~key:_ = function `Both (x, y) -> Some (x, y) | _ -> None in
   let pairs = Hashtbl.merge starts errors ~f in
   Hashtbl.data pairs
+
+
+let pp_message_of_state fmt (a, i) =
+  let property, state = vname a i in
+  Format.fprintf fmt "property %s reaches state %s" property state
diff --git a/infer/src/topl/ToplAutomaton.mli b/infer/src/topl/ToplAutomaton.mli
index 26b77eed6..6a5e25b13 100644
--- a/infer/src/topl/ToplAutomaton.mli
+++ b/infer/src/topl/ToplAutomaton.mli
@@ -23,8 +23,6 @@ open! IStd
 *)
 type t
 
-type vname = ToplAst.property_name * ToplAst.vertex
-
 type vindex = int (* from 0 to vcount()-1, inclusive *)
 
 type tindex = int (* from 0 to tcount()-1, inclusive *)
@@ -35,8 +33,6 @@ val make : ToplAst.t list -> t
 
 val outgoing : t -> vindex -> tindex list
 
-val vname : t -> vindex -> vname
-
 val is_nondet : t -> vindex -> bool
 
 val vcount : t -> int
@@ -52,6 +48,9 @@ val tcount : t -> int
 val max_args : t -> int
 
 val get_start_error_pairs : t -> (vindex * vindex) list
-(** Returns pairs [(i,j)] of vertex indices corresponding to pairs [((p, "start"), (p, "error"))] of
+(** Return pairs [(i,j)] of vertex indices corresponding to pairs [((p, "start"), (p, "error"))] of
     vertex names, where [p] ranges over property names. POST: no vertex index occurs more than once
     in the result. *)
+
+val pp_message_of_state : Format.formatter -> t * tindex -> unit
+(** Print "property P reaches state E". *)
diff --git a/infer/src/topl/dune b/infer/src/topl/dune
index d21b9f4ac..65d998b12 100644
--- a/infer/src/topl/dune
+++ b/infer/src/topl/dune
@@ -14,7 +14,7 @@
  (public_name infer.TOPLlib)
  (flags
   (:standard -open Core -open IR -open IStdlib -open IStd -open ATDGenerated
-    -open IBase -open Absint -open Biabduction -open Pulselib))
- (libraries core IStdlib ATDGenerated IBase IR Absint Biabduction Pulselib)
+    -open IBase -open Absint -open Biabduction))
+ (libraries core IStdlib ATDGenerated IBase IR Absint Biabduction)
  (preprocess
   (pps ppx_compare ppx_hash ppx_sexp_conv)))