src/LTL/branch.mli

   1
   2 (** This module optimizes [LTL] code by suppressing all empty
   3     statements. *)
   4
   5 (* Pasted from Pottier's PP compiler *)
   6
   7 (* This module optimizes [LTL] code by suppressing all [St_skip] statements. In
   8    short, every statement whose successor is a [St_skip] statement is modified
   9    so that its successor is the successor of the [St_skip] statement, and this
  10    is repeated until no reachable [St_skip] statements remain. Unreachable
  11    [St_skip] statements remain in the graph, but will be implicitly eliminated
  12    in the translation of [LTL] to [LIN]. *)
  13
  14 val compress: Label.t -> LTL.graph -> (Label.t * LTL.graph)