Module Tcsmmcformula

type mmc_formula =
  1. | FProp of string
  2. | FVariable of string
  3. | FTT
  4. | FFF
  5. | FNeg of mmc_formula
  6. | FAnd of mmc_formula * mmc_formula
  7. | FOr of mmc_formula * mmc_formula
  8. | FDiamond of mmc_formula
  9. | FBox of mmc_formula
  10. | FMu of string * mmc_formula
  11. | FNu of string * mmc_formula
val is_closed : mmc_formula -> bool
val is_guarded : mmc_formula -> bool
val is_guarded_wrt : mmc_formula -> string -> bool
val is_uniquely_bound : mmc_formula -> bool
val make_uniquely_bound : mmc_formula -> mmc_formula
val eval_metaformula : Tcsmetaformula.formula_expr -> mmc_formula
val formula_length : mmc_formula -> int
val formula_height : mmc_formula -> int
val formula_variable_occs : mmc_formula -> int * int * int
val format_formula : mmc_formula -> string
val format_formula_as_tree : mmc_formula -> string
val formula_to_positive : mmc_formula -> mmc_formula
val is_positive : mmc_formula -> bool
val guarded_transform : mmc_formula -> mmc_formula
val guarded_kupferman_vardi_wolper_transform : mmc_formula -> mmc_formula
type decomposed_mmc_formula_part =
  1. | FIntAtom of bool
  2. | FIntVariable of int
  3. | FIntBranch of bool * int * int
  4. | FIntModality of bool * int
  5. | FIntProp of bool * int
type mmc_proposition_data = int * int
type mmc_variable_data = bool * int * bool * int
type decomposed_mmc_formula = int * decomposed_mmc_formula_part array * (string * mmc_proposition_data) array * (string * mmc_variable_data) array
val normal_form_formula_to_decomposed_formula : mmc_formula -> decomposed_mmc_formula
val decomposed_formula_subformula_cardinality : decomposed_mmc_formula -> int
val get_formula_depth : decomposed_mmc_formula -> decomposed_mmc_formula_part -> int
val decomposed_formula_to_formula : decomposed_mmc_formula -> int -> mmc_formula
val format_decomposed_formula : decomposed_mmc_formula -> int -> string