package TCSLib

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type labelled_mmc_formula =
  1. | FProp of string
  2. | FVariable of string
  3. | FTT
  4. | FFF
  5. | FNeg of labelled_mmc_formula
  6. | FAnd of labelled_mmc_formula * labelled_mmc_formula
  7. | FOr of labelled_mmc_formula * labelled_mmc_formula
  8. | FDiamond of string * labelled_mmc_formula
  9. | FBox of string * labelled_mmc_formula
  10. | FMu of string * labelled_mmc_formula
  11. | FNu of string * labelled_mmc_formula
val is_closed : labelled_mmc_formula -> bool
val is_guarded : labelled_mmc_formula -> bool
val is_guarded_wrt : labelled_mmc_formula -> string -> bool
val is_uniquely_bound : labelled_mmc_formula -> bool
val make_uniquely_bound : labelled_mmc_formula -> labelled_mmc_formula
val formula_length : labelled_mmc_formula -> int
val formula_height : labelled_mmc_formula -> int
val formula_variable_occs : labelled_mmc_formula -> int * int * int
val format_formula : labelled_mmc_formula -> string
val format_formula_as_tree : labelled_mmc_formula -> string
val formula_to_positive : labelled_mmc_formula -> labelled_mmc_formula
val is_positive : labelled_mmc_formula -> bool
val guarded_transform : labelled_mmc_formula -> labelled_mmc_formula
type decomposed_labelled_mmc_formula_part =
  1. | FIntAtom of bool
  2. | FIntVariable of int
  3. | FIntBranch of bool * int * int
  4. | FIntModality of bool * int * int
  5. | FIntProp of bool * int
type mmc_proposition_data = int * int
type mmc_variable_data = bool * int * bool * int
type mmc_label_data = string
type decomposed_labelled_mmc_formula = int * decomposed_labelled_mmc_formula_part array * (string * mmc_proposition_data) array * (string * mmc_variable_data) array * mmc_label_data array
val normal_form_formula_to_decomposed_formula : labelled_mmc_formula -> decomposed_labelled_mmc_formula
val decomposed_formula_subformula_cardinality : decomposed_labelled_mmc_formula -> int
val decomposed_formula_to_formula : decomposed_labelled_mmc_formula -> int -> labelled_mmc_formula
val format_decomposed_formula : decomposed_labelled_mmc_formula -> int -> string
OCaml

Innovation. Community. Security.