TCSLib 0.3 · OCaml Package

type ctlstar_formula =

| FProp of string
| FTT
| FFF
| FNeg of ctlstar_formula
| FAnd of ctlstar_formula * ctlstar_formula
| FOr of ctlstar_formula * ctlstar_formula
| FNext of ctlstar_formula
| FExists of ctlstar_formula
| FForall of ctlstar_formula
| FRelease of ctlstar_formula * ctlstar_formula
| FUntil of ctlstar_formula * ctlstar_formula

val eval_metaformula : Tcsmetaformula.formula_expr -> 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 =

| FIntAtom of bool
| FIntProp of bool * int
| FIntNext of int
| FIntPath of bool * int
| FIntBranch of bool * int * int
| 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 sort_decomposed_formula : 
  decomposed_ctlstar_formula ->
  (decomposed_ctlstar_formula ->
    decomposed_ctlstar_formula_part ->
    decomposed_ctlstar_formula_part ->
    int) ->
  decomposed_ctlstar_formula

val get_formula_depth : 
  decomposed_ctlstar_formula ->
  decomposed_ctlstar_formula_part ->
  int

val decomposed_formula_to_formula : 
  decomposed_ctlstar_formula ->
  int ->
  ctlstar_formula

val format_decomposed_formula : decomposed_ctlstar_formula -> int -> string

type block_type =

| EBlock
| 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

val ctlstar_formula_link_map : ctlstar_formula -> ctlstar_formula array

package TCSLib