### Profile

Statistics
| Branch: | Revision:

## cool / src / lib / CoAlgFormula.mli @ 97d73a78

 1 ```(** This module implements coalgebraic formulae ``` ``` (e.g. parsing, printing, (de-)constructing, ...). ``` ``` @author Florian Widmann ``` ``` *) ``` ```exception CoAlgException of string ``` ```type sort = int ``` ```type rational = { nominator: int; denominator: int } ``` ```val rational_of_int : int -> int -> rational ``` ```type formula = ``` ``` | TRUE ``` ``` | FALSE ``` ``` | AP of string (* named atom *) ``` ``` | NOT of formula ``` ``` | AT of string * formula (* @ *) ``` ``` | OR of formula * formula ``` ``` | AND of formula * formula ``` ``` | EQU of formula * formula (* equivalence <=> *) ``` ``` | IMP of formula * formula (* implication <-> *) ``` ``` | EX of string * formula (* exists, diamond of K *) ``` ``` | AX of string * formula (* forall, box of K *) ``` ``` | ENFORCES of int list * formula (* CL *) ``` ``` | ALLOWS of int list * formula (* CL *) ``` ``` | MIN of int * string * formula (* some more intuitive diamond for GML *) ``` ``` | MAX of int * string * formula (* some more intuitive box for GML *) ``` ``` | MORETHAN of int * string * formula (* diamond of GML *) ``` ``` | MAXEXCEPT of int * string * formula (* box of GML, means: ¬>_nR.¬C *) ``` ``` | ATLEASTPROB of rational * formula (* = {>= 1/2} C ---> C occurs with *) ``` ``` (* probability of at least 50% *) ``` ``` | LESSPROBFAIL of rational * formula (* = [1/2] C = {< 1/2} ¬ C ---> C fails with *) ``` ``` (* probability of less than 50% *) ``` ``` | CONST of string (* constant functor with value string *) ``` ``` | CONSTN of string (* constant functor with value other than string *) ``` ``` | ID of formula (* modality of the identity functor *) ``` ``` | NORM of formula * formula (* default implication *) ``` ``` | NORMN of formula * formula (* \neg NORM (\neg A, \neg B) *) ``` ``` | CHC of formula * formula ``` ``` | FUS of bool * formula ``` ``` | MU of string * formula ``` ``` | NU of string * formula ``` ``` | VAR of string ``` ``` | AF of formula ``` ``` | EF of formula ``` ``` | AG of formula ``` ``` | EG of formula ``` ``` | AU of formula * formula ``` ``` | EU of formula * formula ``` ``` | AR of formula * formula ``` ``` | ER of formula * formula ``` ``` | AB of formula * formula ``` ``` | EB of formula * formula ``` ```exception ConversionException of formula ``` ```type sortedFormula = sort * formula ``` ```val iter : (formula -> unit) -> formula -> unit (* iterate over all sub formulas *) ``` ```val convert_post : (formula -> formula) -> formula -> formula (* run over all subformulas in post order *) ``` ```val convertToK : formula -> formula (* tries to convert a formula to a pure K formula *) ``` ```val convertToGML : formula -> formula (* tries to convert a formula to a pure GML formula *) ``` ```val isNominal : string -> bool ``` ```val sizeFormula : formula -> int ``` ```val sizeSortedFormula : sortedFormula -> int ``` ```val string_of_formula : formula -> string ``` ```val exportFormula : formula -> string ``` ```val exportTatlFormula : formula -> string ``` ```val exportSortedFormula : sortedFormula -> string ``` ```val exportQuery : sortedFormula list -> sortedFormula -> string ``` ```val exportQueryParsable : sortedFormula list -> sortedFormula -> string ``` ```val importFormula : string -> formula ``` ```val importSortedFormula : string -> sortedFormula ``` ```val importQuery : string -> sortedFormula list * sortedFormula ``` ```val verifyFormula : formula -> unit ``` ```val nnfNeg : formula -> formula ``` ```val nnf : formula -> formula ``` ```val simplify : formula -> formula ``` ```val dest_ap : formula -> string ``` ```val dest_nom : formula -> string ``` ```val dest_not : formula -> formula ``` ```val dest_at : formula -> string * formula ``` ```val dest_or : formula -> formula * formula ``` ```val dest_and : formula -> formula * formula ``` ```val dest_equ : formula -> formula * formula ``` ```val dest_imp : formula -> formula * formula ``` ```val dest_ex : formula -> string * formula ``` ```val dest_ax : formula -> string * formula ``` ```val dest_min : formula -> int * string * formula ``` ```val dest_max : formula -> int * string * formula ``` ```val dest_choice : formula -> formula * formula ``` ```val dest_fusion : formula -> bool * formula ``` ```val is_true : formula -> bool ``` ```val is_false : formula -> bool ``` ```val is_ap : formula -> bool ``` ```val is_nom : formula -> bool ``` ```val is_not : formula -> bool ``` ```val is_at : formula -> bool ``` ```val is_or : formula -> bool ``` ```val is_and : formula -> bool ``` ```val is_equ : formula -> bool ``` ```val is_imp : formula -> bool ``` ```val is_ex : formula -> bool ``` ```val is_ax : formula -> bool ``` ```val is_min : formula -> bool ``` ```val is_max : formula -> bool ``` ```val is_choice : formula -> bool ``` ```val is_fusion : formula -> bool ``` ```val const_true : formula ``` ```val const_false : formula ``` ```val const_ap : string -> formula ``` ```val const_nom : string -> formula ``` ```val const_not : formula -> formula ``` ```val const_at : string -> formula -> formula ``` ```val const_or : formula -> formula -> formula ``` ```val const_and : formula -> formula -> formula ``` ```val const_equ : formula -> formula -> formula ``` ```val const_imp : formula -> formula -> formula ``` ```val const_ex : string -> formula -> formula ``` ```val const_ax : string -> formula -> formula ``` ```val const_min : int -> string -> formula -> formula ``` ```val const_max : int -> string -> formula -> formula ``` ```val const_enforces : int list -> formula -> formula ``` ```val const_allows : int list -> formula -> formula ``` ```val const_choice : formula -> formula -> formula ``` ```val const_fusion : bool -> formula -> formula ``` ```type hcFormula = (hcFormula_node, formula) HashConsing.hash_consed ``` ```and hcFormula_node = ``` ``` | HCTRUE ``` ``` | HCFALSE ``` ``` | HCAP of string ``` ``` | HCNOT of string ``` ``` | HCAT of string * hcFormula ``` ``` | HCOR of hcFormula * hcFormula ``` ``` | HCAND of hcFormula * hcFormula ``` ``` | HCEX of string * hcFormula ``` ``` | HCAX of string * hcFormula ``` ``` | HCENFORCES of int list * hcFormula ``` ``` | HCALLOWS of int list * hcFormula ``` ``` | HCMORETHAN of int * string * hcFormula (* GML Diamond *) ``` ``` | HCMAXEXCEPT of int * string * hcFormula (* GML Box *) ``` ``` | HCATLEASTPROB of rational * hcFormula ``` ``` | HCLESSPROBFAIL of rational * hcFormula (* the probability for failing is less than ... *) ``` ``` | HCCONST of string ``` ``` | HCCONSTN of string ``` ``` | HCID of hcFormula ``` ``` | HCNORM of hcFormula * hcFormula ``` ``` | HCNORMN of hcFormula * hcFormula ``` ``` | HCCHC of hcFormula * hcFormula ``` ``` | HCFUS of bool * hcFormula ``` ``` | HCMU of string * hcFormula ``` ``` | HCNU of string * hcFormula ``` ``` | HCVAR of string ``` ```module HcFormula : (HashConsing.S with type nde = hcFormula_node and type fml = formula) ``` ```val hc_formula : HcFormula.t -> formula -> hcFormula ``` ```val hc_replace : HcFormula.t -> string -> hcFormula -> hcFormula -> hcFormula ``` ```val hc_freeIn : string -> hcFormula -> bool ``` ```module HcFHt : (Hashtbl.S with type key = hcFormula) ```