sig
  type formula =
      LNext of Ltlast.formula
    | LUntil of Ltlast.formula * Ltlast.formula
    | LFatally of Ltlast.formula
    | LGlobally of Ltlast.formula
    | LRelease of Ltlast.formula * Ltlast.formula
    | LNot of Ltlast.formula
    | LAnd of Ltlast.formula * Ltlast.formula
    | LOr of Ltlast.formula * Ltlast.formula
    | LImplies of Ltlast.formula * Ltlast.formula
    | LIff of Ltlast.formula * Ltlast.formula
    | LTrue
    | LFalse
    | LCall of string
    | LReturn of string
    | LCallOrReturn of string
    | LIdent of string
end