package TCSLib

  1. Overview
  2. Docs
package TCSLib
Legend:
Library
Module
Module type
Parameter
Class
Class type
type pdl_formula =
  1. | FProp of string
  2. | FTT
  3. | FFF
  4. | FNeg of pdl_formula
  5. | FAnd of pdl_formula * pdl_formula
  6. | FOr of pdl_formula * pdl_formula
  7. | FDiamond of pdl_program * pdl_formula
  8. | FBox of pdl_program * pdl_formula
and pdl_program =
  1. | FAtom of string
  2. | FConcat of pdl_program * pdl_program
  3. | FChoice of pdl_program * pdl_program
  4. | FStar of pdl_program
  5. | FQuestion of pdl_formula
val eval_metaformula : Tcsmetaformula.formula_expr -> pdl_formula
val formula_length : pdl_formula -> int
val program_length : pdl_program -> int
val format_formula : pdl_formula -> string
val format_program : pdl_program -> string
val formula_to_positive : pdl_formula -> pdl_formula
val program_to_positive : pdl_program -> pdl_program
val is_positive : pdl_formula -> bool
val is_positive_program : pdl_program -> bool
type decomposed_pdl_formula_part =
  1. | FIntAtom of bool
  2. | FIntProp of bool * int
  3. | FIntBranch of bool * int * int
  4. | FIntModality of bool * int * int
type decomposed_pdl_program_part =
  1. | FIntPAtom of int
  2. | FIntQuestion of int
  3. | FIntConcat of int * int
  4. | FIntChoice of int * int
  5. | FIntStar of int
type decomposed_pdl_formula = int * decomposed_pdl_formula_part array * int array array * decomposed_pdl_program_part array * (string * (int * int)) array * string array
val normal_form_formula_to_decomposed_formula : pdl_formula -> (pdl_formula -> pdl_formula array) -> decomposed_pdl_formula
val get_formula_depth : decomposed_pdl_formula -> decomposed_pdl_formula_part -> int
val decomposed_formula_to_formula : decomposed_pdl_formula -> int -> pdl_formula
val decomposed_program_to_program : decomposed_pdl_formula -> int -> pdl_program
val format_decomposed_formula : decomposed_pdl_formula -> int -> string
val format_decomposed_program : decomposed_pdl_formula -> int -> string