sig
  exception No_next_frame
  type expr =
      True
    | False
    | Var of string
    | And of Ltl.expr * Ltl.expr
    | Or of Ltl.expr * Ltl.expr
    | Impl of Ltl.expr * Ltl.expr
    | Iff of Ltl.expr * Ltl.expr
    | U of Ltl.expr * Ltl.expr
    | R of Ltl.expr * Ltl.expr
    | W of Ltl.expr * Ltl.expr
    | M of Ltl.expr * Ltl.expr
    | Not of Ltl.expr
    | X of Ltl.expr
    | G of Ltl.expr
    | F of Ltl.expr
  val fmla_as_string : Ltl.expr -> string
  val to_atomics : Ltl.expr -> Ltl.expr
  val eval_fmla : Ltl.expr -> (string * bool) list list -> bool
end