Module Tcsltmcformula

type ltmc_formula =
  1. | FProp of string
  2. | FVariable of string
  3. | FTT
  4. | FFF
  5. | FNeg of ltmc_formula
  6. | FAnd of ltmc_formula * ltmc_formula
  7. | FOr of ltmc_formula * ltmc_formula
  8. | FNext of ltmc_formula
  9. | FMu of string * ltmc_formula
  10. | FNu of string * ltmc_formula
val is_closed : ltmc_formula -> bool
val is_guarded : ltmc_formula -> bool
val is_guarded_wrt : ltmc_formula -> string -> bool
val is_uniquely_bound : ltmc_formula -> bool
val make_uniquely_bound : ltmc_formula -> ltmc_formula
val eval_metaformula : Tcsmetaformula.formula_expr -> ltmc_formula
val formula_length : ltmc_formula -> int
val format_formula : ltmc_formula -> string
val formula_to_positive : ltmc_formula -> ltmc_formula
val is_positive : ltmc_formula -> bool
val guarded_transform : ltmc_formula -> ltmc_formula
type decomposed_ltmc_formula_part =
  1. | FIntAtom of bool
  2. | FIntVariable of int
  3. | FIntBranch of bool * int * int
  4. | FIntNext of int
  5. | FIntProp of bool * int
type ltmc_proposition_data = int * int
type ltmc_variable_data = bool * int * bool * int
type decomposed_ltmc_formula = int * decomposed_ltmc_formula_part array * (string * ltmc_proposition_data) array * (string * ltmc_variable_data) array
val normal_form_formula_to_decomposed_formula : ltmc_formula -> decomposed_ltmc_formula
val decomposed_formula_subformula_cardinality : decomposed_ltmc_formula -> int
val get_formula_depth : decomposed_ltmc_formula -> decomposed_ltmc_formula_part -> int
val decomposed_formula_to_formula : decomposed_ltmc_formula -> int -> ltmc_formula
val format_decomposed_formula : decomposed_ltmc_formula -> int -> string