package TCSLib

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type ltl_formula =
  1. | FProp of string
  2. | FTT
  3. | FFF
  4. | FNeg of ltl_formula
  5. | FAnd of ltl_formula * ltl_formula
  6. | FOr of ltl_formula * ltl_formula
  7. | FNext of ltl_formula
  8. | FRelease of ltl_formula * ltl_formula
  9. | FUntil of ltl_formula * ltl_formula
val eval_metaformula : Tcsmetaformula.formula_expr -> ltl_formula
val formula_length : ltl_formula -> int
val format_formula : ltl_formula -> string
val formula_to_positive : ltl_formula -> ltl_formula
val is_positive : ltl_formula -> bool
type decomposed_ltl_formula_part =
  1. | FIntAtom of bool
  2. | FIntProp of bool * int
  3. | FIntNext of int
  4. | FIntBranch of bool * int * int
  5. | FIntFixpoint of bool * int * int
type decomposed_ltl_formula = int * decomposed_ltl_formula_part array * int array array * (string * (int * int)) array
val normal_form_formula_to_decomposed_formula : ltl_formula -> (ltl_formula -> ltl_formula array) -> decomposed_ltl_formula
val get_formula_depth : decomposed_ltl_formula -> decomposed_ltl_formula_part -> int
val decomposed_formula_to_formula : decomposed_ltl_formula -> int -> ltl_formula
val format_decomposed_formula : decomposed_ltl_formula -> int -> string
OCaml

Innovation. Community. Security.