### Profile

Statistics
| Branch: | Revision:

## cool / src / lib / CoAlgFormula.mli @ 40a714df

1 2 3 4fd28192 Thorsten Wißmann ```(** This module implements coalgebraic formulae ``` ``` (e.g. parsing, printing, (de-)constructing, ...). ``` ``` @author Florian Widmann ``` ``` *) ``` ```exception CoAlgException of string ``` ```type sort = int ``` e5422169 Thorsten Wißmann ```type rational = { nominator: int; denominator: int } ``` ```val rational_of_int : int -> int -> rational ``` 4fd28192 Thorsten Wißmann ```type formula = ``` ``` | TRUE ``` ``` | FALSE ``` 0247525c Thorsten Wißmann ``` | AP of string (* named atom *) ``` 4fd28192 Thorsten Wißmann ``` | NOT of formula ``` 0247525c Thorsten Wißmann ``` | AT of string * formula (* @ *) ``` 4fd28192 Thorsten Wißmann ``` | OR of formula * formula ``` ``` | AND of formula * formula ``` 0247525c Thorsten Wißmann ``` | 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 *) ``` af276a36 Thorsten Wißmann ``` | MORETHAN of int * string * formula (* diamond of GML *) ``` dbcce612 Thorsten Wißmann ``` | MAXEXCEPT of int * string * formula (* box of GML, means: ¬>_nR.¬C *) ``` c855ba91 Thorsten Wißmann ``` | ATLEASTPROB of rational * formula (* = {>= 1/2} C ---> C occurs with *) ``` e5422169 Thorsten Wißmann ``` (* probability of at least 50% *) ``` 9bae2c4f Thorsten Wißmann ``` | LESSPROBFAIL of rational * formula (* = [1/2] C = {< 1/2} ¬ C ---> C fails with *) ``` c49eea11 Thorsten Wißmann ``` (* probability of less than 50% *) ``` ``` | CONST of string (* constant functor with value string *) ``` ``` | CONSTN of string (* constant functor with value other than string *) ``` 19f5dad0 Dirk Pattinson ``` | ID of formula (* modality of the identity functor *) ``` ``` | NORM of formula * formula (* default implication *) ``` ``` | NORMN of formula * formula (* \neg NORM (\neg A, \neg B) *) ``` 4fd28192 Thorsten Wißmann ``` | CHC of formula * formula ``` ``` | FUS of bool * formula ``` d29d35f7 Christoph Egger ``` | MU of string * formula ``` ``` | NU of string * formula ``` 9a3b23cc Christoph Egger ``` | VAR of string ``` b179a57f Christoph Egger ``` | AF of formula ``` ``` | EF of formula ``` ``` | AG of formula ``` ``` | EG of formula ``` ``` | AU of formula * formula ``` ``` | EU of formula * formula ``` e30caa42 Christoph Egger ``` | AR of formula * formula ``` ``` | ER of formula * formula ``` 97d73a78 Christoph Egger ``` | AB of formula * formula ``` ``` | EB of formula * formula ``` 4fd28192 Thorsten Wißmann ca99d0c6 Thorsten Wißmann ```exception ConversionException of formula ``` 4fd28192 Thorsten Wißmann ```type sortedFormula = sort * formula ``` dbcce612 Thorsten Wißmann ```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 *) ``` 4fd28192 Thorsten Wißmann ```val isNominal : string -> bool ``` ```val sizeFormula : formula -> int ``` ```val sizeSortedFormula : sortedFormula -> int ``` ca99d0c6 Thorsten Wißmann ```val string_of_formula : formula -> string ``` 4fd28192 Thorsten Wißmann ```val exportFormula : formula -> string ``` 01b1ab69 Thorsten Wißmann ```val exportTatlFormula : formula -> string ``` 4fd28192 Thorsten Wißmann ```val exportSortedFormula : sortedFormula -> string ``` ```val exportQuery : sortedFormula list -> sortedFormula -> string ``` b59059c4 Thorsten Wißmann ```val exportQueryParsable : sortedFormula list -> sortedFormula -> string ``` 4fd28192 Thorsten Wißmann ```val importFormula : string -> formula ``` ```val importSortedFormula : string -> sortedFormula ``` ```val importQuery : string -> sortedFormula list * sortedFormula ``` 1484d8cb Christoph Egger ```val verifyFormula : formula -> unit ``` 4fd28192 Thorsten Wißmann ```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 ``` dbcce612 Thorsten Wißmann 4fd28192 Thorsten Wißmann ```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 ``` 7993e0bf Thorsten Wißmann ```val const_enforces : int list -> formula -> formula ``` ```val const_allows : int list -> formula -> formula ``` 4fd28192 Thorsten Wißmann ```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 ``` f1fa9ad5 Thorsten Wißmann ``` | HCENFORCES of int list * hcFormula ``` ``` | HCALLOWS of int list * hcFormula ``` af276a36 Thorsten Wißmann ``` | HCMORETHAN of int * string * hcFormula (* GML Diamond *) ``` ``` | HCMAXEXCEPT of int * string * hcFormula (* GML Box *) ``` 86b07be8 Thorsten Wißmann ``` | HCATLEASTPROB of rational * hcFormula ``` 9bae2c4f Thorsten Wißmann ``` | HCLESSPROBFAIL of rational * hcFormula (* the probability for failing is less than ... *) ``` c49eea11 Thorsten Wißmann ``` | HCCONST of string ``` ``` | HCCONSTN of string ``` 19f5dad0 Dirk Pattinson ``` | HCID of hcFormula ``` ``` | HCNORM of hcFormula * hcFormula ``` ``` | HCNORMN of hcFormula * hcFormula ``` 4fd28192 Thorsten Wißmann ``` | HCCHC of hcFormula * hcFormula ``` ``` | HCFUS of bool * hcFormula ``` 87d5082f Christoph Egger ``` | HCMU of string * hcFormula ``` ``` | HCNU of string * hcFormula ``` ``` | HCVAR of string ``` 4fd28192 Thorsten Wißmann ```module HcFormula : (HashConsing.S with type nde = hcFormula_node and type fml = formula) ``` ```val hc_formula : HcFormula.t -> formula -> hcFormula ``` cc07e93d Christoph Egger ```val hc_replace : HcFormula.t -> string -> hcFormula -> hcFormula -> hcFormula ``` 5e7c8aa1 Christoph Egger ```val hc_freeIn : string -> hcFormula -> bool ``` 4fd28192 Thorsten Wißmann `module HcFHt : (Hashtbl.S with type key = hcFormula)`