package TCSLib

  1. Overview
  2. Docs
type ctlstar_formula =
  1. | FProp of string
  2. | FTT
  3. | FFF
  4. | FNeg of ctlstar_formula
  5. | FAnd of ctlstar_formula * ctlstar_formula
  6. | FOr of ctlstar_formula * ctlstar_formula
  7. | FNext of ctlstar_formula
  8. | FExists of ctlstar_formula
  9. | FForall of ctlstar_formula
  10. | FRelease of ctlstar_formula * ctlstar_formula
  11. | FUntil of ctlstar_formula * ctlstar_formula
val is_ctl_formula : ctlstar_formula -> bool
val formula_length : ctlstar_formula -> int
val format_formula : ctlstar_formula -> string
val formula_to_positive : ctlstar_formula -> ctlstar_formula
val is_positive : ctlstar_formula -> bool
type decomposed_ctlstar_formula_part =
  1. | FIntAtom of bool
  2. | FIntProp of bool * int
  3. | FIntNext of int
  4. | FIntPath of bool * int
  5. | FIntBranch of bool * int * int
  6. | FIntFixpoint of bool * int * int
type decomposed_ctlstar_formula = int * decomposed_ctlstar_formula_part array * int array array * (string * (int * int)) array
val normal_form_formula_to_decomposed_formula : ctlstar_formula -> (ctlstar_formula -> ctlstar_formula array) -> decomposed_ctlstar_formula
val decomposed_formula_to_formula : decomposed_ctlstar_formula -> int -> ctlstar_formula
val format_decomposed_formula : decomposed_ctlstar_formula -> int -> string
type block_type =
  1. | EBlock
  2. | ABlock
type block = block_type * int list * int list
val format_block : decomposed_ctlstar_formula -> block -> string
val add_to_block : decomposed_ctlstar_formula -> block -> int list -> block
OCaml

Innovation. Community. Security.