### Profile

Statistics
| Branch: | Revision:

## cool / src / lib / CoAlgFormula.ml @ de84f40d

 1 ```(** This module implements coalgebraic formulae ``` ``` (e.g. parsing, printing, (de-)constructing, ...). ``` ``` @author Florian Widmann ``` ``` *) ``` ```module HC = HashConsing ``` ```module A = AltGenlex ``` ```module L = List ``` ```module Str = String ``` ```(** A general exception for all kinds of errors ``` ``` that can happen in the tableau procedure. ``` ``` More specific information is given in the argument. ``` ``` *) ``` ```exception CoAlgException of string ``` ```(** Indicates the sort of a sorted formula ``` ``` *) ``` ```type sort = int ``` ```type rational = { nominator: int; denominator: int } ``` ```let string_of_rational r = ``` ``` (string_of_int r.nominator)^"/"^(string_of_int r.denominator) ``` ```let rational_of_int n d = { nominator = n; denominator = d } ``` ```(** Defines (unsorted) coalgebraic formulae. ``` ``` *) ``` ```type formula = ``` ``` | TRUE ``` ``` | FALSE ``` ``` | AP of string (* atomic proposition *) ``` ``` | NOT of formula ``` ``` | AT of string * formula ``` ``` | OR of formula * formula ``` ``` | AND of formula * formula ``` ``` | EQU of formula * formula ``` ``` | IMP of formula * formula ``` ``` | EX of string * formula ``` ``` | AX of string * formula ``` ``` | ENFORCES of int list * formula ``` ``` | ALLOWS of int list * formula ``` ``` | MIN of int * string * formula ``` ``` | MAX of int * string * formula ``` ``` | MORETHAN of int * string * formula (* diamond of GML *) ``` ``` | MAXEXCEPT of int * string * formula (* box of GML *) ``` ``` | ATLEASTPROB of rational * formula (* = {>= 0.5} 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 (* Choice is self-dual *) ``` ``` | 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 ``` ```exception ConversionException of formula ``` ```(** Defines sorted coalgebraic formulae. ``` ``` *) ``` ```type sortedFormula = sort * formula ``` ```(** Determines whether a name indicates a nominal. ``` ``` @param A string s. ``` ``` @return True iff s contains a prime character. ``` ``` *) ``` ```let isNominal s = String.contains s '\'' ``` ```(** Determines the size of a formula. ``` ``` @param f A formula. ``` ``` @return The size of f. ``` ``` *) ``` ```let rec sizeFormula f = ``` ``` match f with ``` ``` | TRUE ``` ``` | FALSE ``` ``` | AP _ -> 1 ``` ``` | NOT f1 ``` ``` | AT (_, f1) -> succ (sizeFormula f1) ``` ``` | OR (f1, f2) ``` ``` | AND (f1, f2) ``` ``` | EQU (f1, f2) ``` ``` | IMP (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2) ``` ``` | EX (_, f1) ``` ``` | AX (_, f1) ``` ``` | ENFORCES (_, f1) ``` ``` | ALLOWS (_, f1) -> succ (sizeFormula f1) ``` ``` | MIN (_, _, f1) ``` ``` | MAX (_, _, f1) ``` ``` | ATLEASTPROB (_, f1) ``` ``` | LESSPROBFAIL (_, f1) ``` ``` | MORETHAN (_, _, f1) ``` ``` | MAXEXCEPT (_, _, f1) -> succ (sizeFormula f1) ``` ``` | ID (f1) -> succ (sizeFormula f1) ``` ``` | NORM(f1, f2) ``` ``` | NORMN(f1, f2) -> succ (sizeFormula f1 + sizeFormula f2) ``` ``` | CONST _ ``` ``` | CONSTN _ -> 1 ``` ``` | CHC (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2) ``` ``` | FUS (_, f1) -> succ (sizeFormula f1) ``` ``` | MU (_, f1) ``` ``` | NU (_, f1) -> succ (succ (sizeFormula f1)) ``` ``` | VAR _ -> 1 ``` ``` | AF _ | EF _ ``` ``` | AG _ | EG _ ``` ``` | AU _ | EU _ -> ``` ``` raise (CoAlgException ("sizeFormula: CTL should have been removed at this point")) ``` ```(** Determines the size of a sorted formula. ``` ``` @param f A sorted formula. ``` ``` @return The size of f. ``` ``` *) ``` ```let sizeSortedFormula f = sizeFormula (snd f) ``` ```(* think of func: (formula -> unit) -> formula -> unit as identity. ``` ``` iterate over all subformulae and collect side effects. *) ``` ```let rec iter func formula = ``` ``` func formula; ``` ``` let proc = iter func in (* proc = "process" *) ``` ``` match formula with ``` ``` | TRUE | FALSE | AP _ | VAR _ -> () ``` ``` | CONST _ ``` ``` | CONSTN _ -> () ``` ``` | NOT a | AT (_,a) ``` ``` | EX (_,a) | AX (_,a) -> proc a ``` ``` | OR (a,b) | AND (a,b) ``` ``` | EQU (a,b) | IMP (a,b) -> (proc a ; proc b) ``` ``` | ENFORCES (_,a) | ALLOWS (_,a) ``` ``` | MIN (_,_,a) | MAX (_,_,a) ``` ``` | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a) ``` ``` | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a ``` ``` | ID(a) -> proc a ``` ``` | NORM(a, b) | NORMN(a, b) -> (proc a; proc b) ``` ``` | CHC (a,b) -> (proc a ; proc b) ``` ``` | FUS (_,a) -> proc a ``` ``` | MU (_, f) | NU (_, f) -> proc f ``` ``` | AF f | EF f | AG f | EG f -> proc f ``` ``` | AU (f1, f2) | EU (f1, f2) -> (proc f1; proc f2) ``` ```let rec convert_post func formula = (* run over all subformulas in post order *) ``` ``` let c = convert_post func in (* some shorthand *) ``` ``` (* replace parts of the formula *) ``` ``` let formula = (match formula with ``` ``` (* 0-ary constructors *) ``` ``` | TRUE | FALSE | AP _ | VAR _ -> formula ``` ``` | CONST _ ``` ``` | CONSTN _ -> formula ``` ``` (* unary *) ``` ``` | NOT a -> NOT (c a) ``` ``` | AT (s,a) -> AT (s,c a) ``` ``` (* binary *) ``` ``` | OR (a,b) -> OR (c a, c b) ``` ``` | AND (a,b) -> AND (c a, c b) ``` ``` | EQU (a,b) -> EQU (c a, c b) ``` ``` | IMP (a,b) -> IMP (c a, c b) ``` ``` | EX (s,a) -> EX (s,c a) ``` ``` | AX (s,a) -> AX (s,c a) ``` ``` | ENFORCES (s,a) -> ENFORCES (s,c a) ``` ``` | ALLOWS (s,a) -> ALLOWS (s,c a) ``` ``` | MIN (n,s,a) -> MIN (n,s,c a) ``` ``` | MAX (n,s,a) -> MAX (n,s,c a) ``` ``` | ATLEASTPROB (p,a) -> ATLEASTPROB (p, c a) ``` ``` | LESSPROBFAIL (p,a) -> LESSPROBFAIL (p, c a) ``` ``` | MORETHAN (n,s,a) -> MORETHAN (n,s,c a) ``` ``` | MAXEXCEPT (n,s,a) -> MAXEXCEPT (n,s,c a) ``` ``` | ID(a) -> ID (c a) ``` ``` | NORM(a, b) -> NORM(c a, c b) ``` ``` | NORMN(a, b) -> NORMN(c a, c b) ``` ``` | CHC (a,b) -> CHC (c a, c b) ``` ``` | FUS (s,a) -> FUS (s, c a) ``` ``` | MU (n, f1) -> MU (n, c f1) ``` ``` | NU (n, f1) -> NU (n, c f1) ``` ``` | AF f1 -> AF (c f1) ``` ``` | EF f1 -> EF (c f1) ``` ``` | AG f1 -> AG (c f1) ``` ``` | EG f1 -> EG (c f1) ``` ``` | AU (f1, f2) -> AU (c f1, c f2) ``` ``` | EU (f1, f2) -> AU (c f1, c f2))in ``` ``` func formula ``` ```let convertToK formula = (* tries to convert a formula to a pure K formula *) ``` ``` let helper formula = match formula with ``` ``` | ENFORCES _ | ALLOWS _ -> raise (ConversionException formula) ``` ``` | MORETHAN (0,s,a) | MIN (1,s,a) -> EX (s,a) ``` ``` | MAX (0,s,a) -> AX (s, NOT a) ``` ``` | MAXEXCEPT (0,s,a) -> AX (s, a) ``` ``` | TRUE | FALSE ``` ``` | EQU _ | IMP _ ``` ``` | AND _ | OR _ ``` ``` | AP _ | NOT _ ``` ``` | AX _ | EX _ ``` ``` | CHC _ | FUS _ -> formula ``` ``` | _ -> raise (ConversionException formula) ``` ``` in ``` ``` convert_post helper formula ``` ```let convertToGML formula = (* tries to convert a formula to a pure GML formula *) ``` ``` let helper formula = match formula with ``` ``` | ENFORCES _ | ALLOWS _ -> raise (ConversionException formula) ``` ``` | MORETHAN _ | MIN _ | MAX _ | MAXEXCEPT _ -> formula ``` ``` | TRUE | FALSE ``` ``` | EQU _ | IMP _ ``` ``` | AND _ | OR _ ``` ``` | AP _ | NOT _ ``` ``` | CHC _ | FUS _ -> formula ``` ``` | AX (r,a) -> MAXEXCEPT (0,r,a) ``` ``` | EX (r,a) -> MORETHAN (0,r,a) ``` ``` | _ -> raise (ConversionException formula) ``` ``` in ``` ``` convert_post helper formula ``` ```let gensym = Stream.from (fun i -> Some (Printf.sprintf "#gensym%x#" i)) ``` ```let convertToMu formula = ``` ``` let helper formula = ``` ``` match formula with ``` ``` | AF f1 -> ``` ``` MU ("#AF#", (OR (f1, (AX ("", (VAR "#AF#")))))) ``` ``` | EF f1 -> ``` ``` MU ("#EF#", (OR (f1, (EX ("", (VAR "#EF#")))))) ``` ``` | AG f1 -> ``` ``` NU ("#AG#", (AND (f1, (AX ("", (VAR "#AG#")))))) ``` ``` | EG f1 -> ``` ``` NU ("#EG#", (AND (f1, (EX ("", (VAR "#EG#")))))) ``` ``` | AU (f1, f2) -> ``` ``` MU ("#AU#", (OR (f2, (AND (f1, (AX ("", (VAR "#AU#")))))))) ``` ``` | EU (f1, f2) -> ``` ``` MU ("#EU#", (OR (f2, (AND (f1, (EX ("", (VAR "#EU#")))))))) ``` ``` | _ -> formula ``` ``` in ``` ``` convert_post helper formula ``` ```(** Appends a string representation of a formula to a string buffer. ``` ``` Parentheses are ommited where possible ``` ``` where the preference rules are defined as usual. ``` ``` @param sb A string buffer. ``` ``` @param f A formula. ``` ``` *) ``` ```let rec exportFormula_buffer sb f = ``` ``` let negate = function ``` ``` | NOT f -> f ``` ``` | f -> NOT f ``` ``` in ``` ``` let prio n lf = ``` ``` let prionr = function ``` ``` | EQU _ -> 0 ``` ``` | IMP _ -> 1 ``` ``` | OR _ -> 2 ``` ``` | AND _ -> 3 ``` ``` | _ -> 4 ``` ``` in ``` ``` if prionr lf < n then begin ``` ``` Buffer.add_char sb '('; ``` ``` exportFormula_buffer sb lf; ``` ``` Buffer.add_char sb ')' ``` ``` end ``` ``` else exportFormula_buffer sb lf ``` ``` in ``` ``` match f with ``` ``` | TRUE -> Buffer.add_string sb "True" ``` ``` | FALSE -> Buffer.add_string sb "False" ``` ``` | AP s -> Buffer.add_string sb s ``` ``` | NOT f1 -> ``` ``` Buffer.add_string sb "~"; ``` ``` prio 4 f1 ``` ``` | AT (s, f1) -> ``` ``` Buffer.add_string sb "@ "; ``` ``` Buffer.add_string sb s; ``` ``` Buffer.add_string sb " "; ``` ``` prio 4 f1 ``` ``` | OR (f1, f2) -> ``` ``` prio 2 f1; ``` ``` Buffer.add_string sb " | "; ``` ``` prio 2 f2 ``` ``` | AND (f1, f2) -> ``` ``` prio 3 f1; ``` ``` Buffer.add_string sb " & "; ``` ``` prio 3 f2 ``` ``` | EQU (f1, f2) -> ``` ``` prio 0 f1; ``` ``` Buffer.add_string sb " <=> "; ``` ``` prio 0 f2 ``` ``` | IMP (f1, f2) -> ``` ``` prio 2 f1; ``` ``` Buffer.add_string sb " => "; ``` ``` prio 2 f2 ``` ``` | EX (s, f1) -> ``` ``` Buffer.add_string sb "<"; ``` ``` Buffer.add_string sb s; ``` ``` Buffer.add_string sb ">"; ``` ``` prio 4 f1 ``` ``` | AX (s, f1) -> ``` ``` Buffer.add_string sb "["; ``` ``` Buffer.add_string sb s; ``` ``` Buffer.add_string sb "]"; ``` ``` prio 4 f1 ``` ``` | ALLOWS (s, f1) -> ``` ``` Buffer.add_string sb "<{"; ``` ``` Buffer.add_string sb ( ``` ``` match s with ``` ``` | [] -> " " ``` ``` | _ ->(Str.concat " " (L.map string_of_int s)) ``` ``` ); ``` ``` Buffer.add_string sb "}>"; ``` ``` prio 4 f1 ``` ``` | ENFORCES (s, f1) -> ``` ``` Buffer.add_string sb "[{"; ``` ``` Buffer.add_string sb ( ``` ``` match s with ``` ``` | [] -> " " ``` ``` | _ ->(Str.concat " " (L.map string_of_int s)) ``` ``` ); ``` ``` Buffer.add_string sb "}]"; ``` ``` prio 4 f1 ``` ``` | ATLEASTPROB (p, f1) -> ``` ``` Buffer.add_string sb "{>="; ``` ``` Buffer.add_string sb (string_of_rational p); ``` ``` Buffer.add_string sb "}"; ``` ``` prio 4 f1 ``` ``` | LESSPROBFAIL (p, f1) -> ``` ``` Buffer.add_string sb "{<"; ``` ``` Buffer.add_string sb (string_of_rational p); ``` ``` Buffer.add_string sb "} ~ "; ``` ``` prio 4 f1 ``` ``` | MIN (n, s, f1) -> ``` ``` Buffer.add_string sb "{>="; ``` ``` Buffer.add_string sb (string_of_int n); ``` ``` Buffer.add_string sb " "; ``` ``` Buffer.add_string sb s; ``` ``` Buffer.add_string sb "}"; ``` ``` prio 4 f1 ``` ``` | MAX (n, s, f1) -> ``` ``` Buffer.add_string sb "{<="; ``` ``` Buffer.add_string sb (string_of_int n); ``` ``` Buffer.add_string sb " "; ``` ``` Buffer.add_string sb s; ``` ``` Buffer.add_string sb "}"; ``` ``` prio 4 f1 ``` ``` | MORETHAN (n, s, f1) -> ``` ``` Buffer.add_string sb "{>"; ``` ``` Buffer.add_string sb (string_of_int n); ``` ``` Buffer.add_string sb " "; ``` ``` Buffer.add_string sb s; ``` ``` Buffer.add_string sb "}"; ``` ``` prio 4 f1 ``` ``` | MAXEXCEPT (n, s, f1) -> ``` ``` Buffer.add_string sb "{<="; ``` ``` Buffer.add_string sb (string_of_int n); ``` ``` Buffer.add_string sb " ~ "; ``` ``` Buffer.add_string sb s; ``` ``` Buffer.add_string sb "}"; ``` ``` prio 4 f1 (* actually is prio of ~ and not of <= *) ``` ``` | ID (f1) -> ``` ``` Buffer.add_string sb "O"; ``` ``` prio 4 f1 ``` ``` | NORM(f1, f2) -> ``` ``` Buffer.add_string sb "("; ``` ``` exportFormula_buffer sb f1; ``` ``` Buffer.add_string sb " =o "; ``` ``` exportFormula_buffer sb f2; ``` ``` Buffer.add_string sb ")" ``` ``` | NORMN(f1, f2) -> ``` ``` Buffer.add_string sb "~("; ``` ``` exportFormula_buffer sb (negate f1); ``` ``` Buffer.add_string sb " =o "; ``` ``` exportFormula_buffer sb (negate f2); ``` ``` Buffer.add_string sb ")" ``` ``` | CHC (f1, f2) -> ``` ``` Buffer.add_string sb "("; ``` ``` exportFormula_buffer sb f1; ``` ``` Buffer.add_string sb " + "; ``` ``` exportFormula_buffer sb f2; ``` ``` Buffer.add_string sb ")" ``` ``` | CONST s -> Buffer.add_string sb "="; ``` ``` Buffer.add_string sb s ``` ``` | CONSTN s -> Buffer.add_string sb "~="; ``` ``` Buffer.add_string sb s ``` ``` | FUS (first, f1) -> ``` ``` Buffer.add_string sb (if first then "[pi1]" else "[pi2]"); ``` ``` prio 4 f1 ``` ``` | MU (s, f1) -> ``` ``` Buffer.add_string sb "μ"; ``` ``` Buffer.add_string sb s; ``` ``` Buffer.add_string sb "."; ``` ``` prio 4 f1 ``` ``` | NU (s, f1) -> ``` ``` Buffer.add_string sb "ν"; ``` ``` Buffer.add_string sb s; ``` ``` Buffer.add_string sb "."; ``` ``` prio 4 f1 ``` ``` | VAR s -> ``` ``` Buffer.add_string sb s ``` ``` | AF f1 -> ``` ``` Buffer.add_string sb "AF "; ``` ``` prio 4 f1 ``` ``` | EF f1 -> ``` ``` Buffer.add_string sb "EF "; ``` ``` prio 4 f1 ``` ``` | AG f1 -> ``` ``` Buffer.add_string sb "AG "; ``` ``` prio 4 f1 ``` ``` | EG f1 -> ``` ``` Buffer.add_string sb "EG "; ``` ``` prio 4 f1 ``` ``` | AU (f1, f2) -> ``` ``` Buffer.add_string sb "A ("; ``` ``` prio 4 f1; ``` ``` Buffer.add_string sb " U "; ``` ``` prio 4 f2; ``` ``` Buffer.add_string sb ")" ``` ``` | EU (f1, f2) -> ``` ``` Buffer.add_string sb "E ("; ``` ``` prio 4 f1; ``` ``` Buffer.add_string sb " U "; ``` ``` prio 4 f2; ``` ``` Buffer.add_string sb ")" ``` ```(** Converts a formula into a string representation. ``` ``` Parentheses are ommited where possible ``` ``` where the preference rules are defined as usual. ``` ``` @param f A formula. ``` ``` @return A string representing f. ``` ``` *) ``` ```let exportFormula f = ``` ``` let sb = Buffer.create 128 in ``` ``` exportFormula_buffer sb f; ``` ``` Buffer.contents sb ``` ```let string_of_formula = exportFormula ``` ```(** export (CL)-formula suitable for tatl-inputs *) ``` ```let rec exportTatlFormula_buffer sb f = ``` ``` let prio n lf = ``` ``` let prionr = function ``` ``` | EQU _ -> 0 ``` ``` | IMP _ -> 1 ``` ``` | OR _ -> 2 ``` ``` | AND _ -> 3 ``` ``` | _ -> 4 ``` ``` in ``` ``` if prionr lf < n then begin ``` ``` Buffer.add_char sb '('; ``` ``` exportTatlFormula_buffer sb lf; ``` ``` Buffer.add_char sb ')' ``` ``` end ``` ``` else exportTatlFormula_buffer sb lf ``` ``` in ``` ``` match f with ``` ``` | TRUE -> Buffer.add_string sb "(p \\/ ~p)" ``` ``` | FALSE -> Buffer.add_string sb "(p /\\ ~p)" ``` ``` | AP s -> Buffer.add_string sb s ``` ``` | NOT f1 -> ``` ``` Buffer.add_string sb "~"; ``` ``` prio 4 f1 ``` ``` | OR (f1, f2) -> ``` ``` prio 2 f1; ``` ``` Buffer.add_string sb " \\/ "; ``` ``` prio 2 f2 ``` ``` | AND (f1, f2) -> ``` ``` prio 3 f1; ``` ``` Buffer.add_string sb " /\\ "; ``` ``` prio 3 f2 ``` ``` | EQU (f1, f2) -> ``` ``` prio 0 (AND (IMP (f1,f2), IMP (f2,f1))) ``` ``` | IMP (f1, f2) -> ``` ``` prio 2 f1; ``` ``` Buffer.add_string sb " -> "; ``` ``` prio 2 f2 ``` ``` | ALLOWS (s, f1) -> ``` ``` Buffer.add_string sb "<<"; ``` ``` Buffer.add_string sb ( ``` ``` match s with ``` ``` | [] -> " " ``` ``` | _ ->(Str.concat "," (L.map string_of_int s)) ``` ``` ); ``` ``` Buffer.add_string sb ">>X "; ``` ``` prio 4 f1 ``` ``` | ENFORCES (s, f1) -> ``` ``` Buffer.add_string sb "~<<"; ``` ``` Buffer.add_string sb ( ``` ``` match s with ``` ``` | [] -> " " ``` ``` | _ ->(Str.concat "," (L.map string_of_int s)) ``` ``` ); ``` ``` Buffer.add_string sb ">>X ~ "; ``` ``` prio 4 f1 ``` ``` | EX _ ``` ``` | AX _ ``` ``` | MIN _ ``` ``` | MAX _ ``` ``` | MORETHAN _ ``` ``` | MAXEXCEPT _ ``` ``` | AT _ ``` ``` | CONST _ ``` ``` | CONSTN _ ``` ``` | CHC _ ``` ``` | ATLEASTPROB _ ``` ``` | LESSPROBFAIL _ ``` ``` | ID _ ``` ``` | NORM _ ``` ``` | NORMN _ ``` ``` | FUS _ ``` ``` | MU _ ``` ``` | NU _ ``` ``` | VAR _ ``` ``` | AF _ ``` ``` | EF _ ``` ``` | AG _ ``` ``` | EG _ ``` ``` | AU _ ``` ``` | EU _ -> raise (CoAlgException ("export to tatl: Not connectives of CL")) ``` ```let exportTatlFormula f = ``` ``` let sb = Buffer.create 128 in ``` ``` exportTatlFormula_buffer sb f; ``` ``` Buffer.contents sb ``` ```(** Appends a string representation of a sorted formula to a string buffer. ``` ``` Parentheses are ommited where possible ``` ``` where the preference rules are defined as usual. ``` ``` @param sb A string buffer. ``` ``` @param (s, f) A sorted formula. ``` ``` *) ``` ```let rec exportSortedFormula_buffer sb (s, f) = ``` ``` Buffer.add_string sb (string_of_int s); ``` ``` Buffer.add_string sb ": "; ``` ``` exportFormula_buffer sb f ``` ```(** Converts a sorted formula into a string representation. ``` ``` Parentheses are ommited where possible ``` ``` where the preference rules are defined as usual. ``` ``` @param f A sorted formula. ``` ``` @return A string representing f. ``` ``` *) ``` ```let exportSortedFormula f = ``` ``` let sb = Buffer.create 128 in ``` ``` exportSortedFormula_buffer sb f; ``` ``` Buffer.contents sb ``` ```(** Converts a (sorted) formula query into a string representation. ``` ``` @param tbox A list of sorted formulae representing a TBox. ``` ``` @param f A sorted formula. ``` ``` @return A string representing tbox |- f. ``` ``` *) ``` ```let exportQuery tbox f = ``` ``` let sb = Buffer.create 1000 in ``` ``` let rec expFl = function ``` ``` | [] -> () ``` ``` | h::tl -> ``` ``` exportSortedFormula_buffer sb h; ``` ``` if tl <> [] then Buffer.add_string sb "; " else (); ``` ``` expFl tl ``` ``` in ``` ``` expFl tbox; ``` ``` Buffer.add_string sb " |- "; ``` ``` exportSortedFormula_buffer sb f; ``` ``` Buffer.contents sb ``` ```(** Converts a (sorted) formula query into a string representation. Such that ``` ``` coalg can read it again using importQuery ``` ``` @param tbox A list of sorted formulae representing a TBox. ``` ``` @param f A sorted formula. ``` ``` @return A string representing tbox |- f. ``` ``` *) ``` ```let exportQueryParsable tbox (_,f) = ``` ``` let sb = Buffer.create 1000 in ``` ``` let rec expFl = function ``` ``` | [] -> () ``` ``` | (_,h)::tl -> ``` ``` exportFormula_buffer sb h; ``` ``` if tl <> [] then Buffer.add_string sb "; " else (); ``` ``` expFl tl ``` ``` in ``` ``` expFl tbox; ``` ``` Buffer.add_string sb " |- "; ``` ``` exportFormula_buffer sb f; ``` ``` Buffer.contents sb ``` ```(* NB: True and False are the propositional constants. Lower case ``` ``` true/false are regardes as atomic propositions and we emit a warning ``` ```*) ``` ```let lexer = A.make_lexer ``` ``` [":";";";"|-";"(";")";"=>";"<=>";"|";"&";"~";"@";"True";"False";"true";"false";"<";">";"[";"]";"{<=";"{>=";"}";"+";"[pi1]";"[pi2]" ``` ``` ;"[{";"}]";"<{";"}>";",";"/";"{<";"=";"=o";"O" ``` ``` ;"μ";"ν";"." ``` ``` ;"AX";"EX";"AF";"EF";"AG";"EG";"A";"E";"U" ``` ``` ] ``` ```let mk_exn s = CoAlgException s ``` ```(** Process from inside out. cons all variables seen, remove them when ``` ``` binding fixpoint is found. Fixpoint type may only change if last ``` ``` (inner) fixpoint didn't include any free variables. ``` ``` *) ``` ```let rec verifyMuAltFree formula = ``` ``` let proc = verifyMuAltFree in ``` ``` match formula with ``` ``` | TRUE | FALSE | AP _ -> ("none", []) ``` ``` | CONST _ ``` ``` | CONSTN _ -> ("none", []) ``` ``` | AT (_,a) | NOT a ``` ``` | EX (_,a) | AX (_,a) -> proc a ``` ``` | OR (a,b) | AND (a,b) ``` ``` | EQU (a,b) | IMP (a,b) -> ``` ``` let (atype, afree) = proc a ``` ``` and (btype, bfree) = proc b in ``` ``` if (compare atype "μ" == 0 && compare btype "ν" == 0) || ``` ``` (compare atype "ν" == 0 && compare btype "μ" == 0) then ``` ``` raise (CoAlgException ("formula not alternation-free")); ``` ``` if compare atype "none" == 0 then ``` ``` (btype, List.flatten [afree; bfree]) ``` ``` else ``` ``` (atype, List.flatten [afree; bfree]) ``` ``` | ENFORCES (_,a) | ALLOWS (_,a) ``` ``` | MIN (_,_,a) | MAX (_,_,a) ``` ``` | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a) ``` ``` | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a ``` ``` | ID(a) -> proc a ``` ``` | NORM(a, b) | NORMN(a, b) ``` ``` | CHC (a,b) -> ``` ``` let (atype, afree) = proc a ``` ``` and (btype, bfree) = proc b in ``` ``` if (compare atype "μ" == 0 && compare btype "ν" == 0) || ``` ``` (compare atype "ν" == 0 && compare btype "μ" == 0) then ``` ``` raise (CoAlgException ("formula not alternation-free")); ``` ``` if compare atype "none" == 0 then ``` ``` (btype, List.flatten [afree; bfree]) ``` ``` else ``` ``` (atype, List.flatten [afree; bfree]) ``` ``` | FUS (_,a) -> proc a ``` ``` | MU (s, f) -> ``` ``` let (fptype, free) = proc f in ``` ``` (if (compare fptype "ν" == 0) then ``` ``` raise (CoAlgException ("formula not alternation-free"))); ``` ``` let predicate x = compare x s != 0 in ``` ``` let newfree = List.filter predicate free in ``` ``` if newfree = [] then ``` ``` ("none", []) ``` ``` else ``` ``` ("μ", newfree) ``` ``` | NU (s, f) -> ``` ``` let (fptype, free) = proc f in ``` ``` (if (compare fptype "μ" == 0) then ``` ``` raise (CoAlgException ("formula not alternation-free"))); ``` ``` let predicate x = compare x s != 0 in ``` ``` let newfree = List.filter predicate free in ``` ``` if newfree = [] then ``` ``` ("none", []) ``` ``` else ``` ``` ("ν", newfree) ``` ``` | VAR s -> ("none", [s]) ``` ``` | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ -> ``` ``` raise (CoAlgException ("verifyMuAltFree: CTL should have been removed at this point")) ``` ```(** Process from outside in. For every variable bound keep the tuple ``` ``` (name, negations). For every negation crossed map a +1 over snd on ``` ``` that list. For every variable met check that the matching ``` ``` negations is even. ``` ``` *) ``` ```let rec verifyMuMonotone negations formula = ``` ``` let proc = verifyMuMonotone negations in ``` ``` match formula with ``` ``` | TRUE | FALSE | AP _ -> () ``` ``` | CONST _ ``` ``` | CONSTN _ -> () ``` ``` | AT (_,a) ``` ``` | EX (_,a) | AX (_,a) -> proc a ``` ``` | OR (a,b) | AND (a,b) ``` ``` | EQU (a,b) | IMP (a,b) -> (proc a ; proc b) ``` ``` | ENFORCES (_,a) | ALLOWS (_,a) ``` ``` | MIN (_,_,a) | MAX (_,_,a) ``` ``` | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a) ``` ``` | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a ``` ``` | ID(a) -> proc a ``` ``` | NORM(a, b) | NORMN(a, b) -> (proc a; proc b) ``` ``` | CHC (a,b) -> (proc a ; proc b) ``` ``` | FUS (_,a) -> proc a ``` ``` | MU (s, f) ``` ``` | NU (s, f) -> ``` ``` let newNeg = (s, 0) :: negations in ``` ``` verifyMuMonotone newNeg f ``` ``` | VAR s -> ``` ``` let finder (x, _) = compare x s == 0 in ``` ``` let (_, neg) = List.find finder negations in ``` ``` if ((neg land 1) != 0) then raise (CoAlgException ("formula not monotone")) ``` ``` | NOT a -> ``` ``` let increment (s, n) = (s, n+1) in ``` ``` let newNeg = List.map increment negations in ``` ``` verifyMuMonotone newNeg a ``` ``` | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ -> ``` ``` raise (CoAlgException ("verifyMuMonotone: CTL should have been removed at this point")) ``` ```let rec verifyMuGuarded unguarded formula = ``` ``` let proc = verifyMuGuarded unguarded in ``` ``` match formula with ``` ``` | TRUE | FALSE | AP _ -> () ``` ``` | CONST _ ``` ``` | CONSTN _ -> () ``` ``` | AT (_,a) | NOT a -> proc a ``` ``` | EX (_,a) | AX (_,a) -> verifyMuGuarded [] a ``` ``` | OR (a,b) | AND (a,b) ``` ``` | EQU (a,b) | IMP (a,b) -> (proc a ; proc b) ``` ``` | ENFORCES (_,a) | ALLOWS (_,a) ``` ``` | MIN (_,_,a) | MAX (_,_,a) ``` ``` | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a) ``` ``` | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a ``` ``` | ID(a) -> proc a ``` ``` | NORM(a, b) | NORMN(a, b) -> (proc a; proc b) ``` ``` | CHC (a,b) -> (proc a ; proc b) ``` ``` | FUS (_,a) -> proc a ``` ``` | MU (s, f) ``` ``` | NU (s, f) -> ``` ``` let newUnguard = s :: unguarded in ``` ``` verifyMuGuarded newUnguard f ``` ``` | VAR s -> ``` ``` let finder x = compare x s == 0 in ``` ``` if List.exists finder unguarded then ``` ``` raise (CoAlgException ("formula not guarded")) ``` ``` | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ -> ``` ``` raise (CoAlgException ("verifyMuGuarded: CTL should have been removed at this point")) ``` ```let verifyFormula formula = ``` ``` verifyMuAltFree formula; ``` ``` verifyMuMonotone [] formula; ``` ``` verifyMuGuarded [] formula ``` ```(** These functions parse a token stream to obtain a formula. ``` ``` It is a standard recursive descent procedure. ``` ``` @param ts A token stream. ``` ``` @return The resulting (sub-)formula. ``` ``` @raise CoAlgException if ts does not represent a formula. ``` ``` *) ``` ```let rec parse_formula (symtab: 'a list) ts = ``` ``` let formula = (parse_imp symtab ts) in ``` ``` let f1 = convertToMu formula in ``` ``` match Stream.peek ts with ``` ``` | None -> f1 ``` ``` | Some (A.Kwd "<=>") -> ``` ``` Stream.junk ts; ``` ``` let f2 = parse_formula symtab ts in ``` ``` EQU (f1, f2) ``` ``` | _ -> f1 ``` ```(** These functions parse a token stream to obtain a formula. ``` ``` It is a standard recursive descent procedure. ``` ``` @param ts A token stream. ``` ``` @return The resulting (sub-)formula. ``` ``` @raise CoAlgException if ts does not represent a formula. ``` ``` *) ``` ```and parse_imp symtab ts= ``` ``` let f1 = parse_or symtab ts in ``` ``` match Stream.peek ts with ``` ``` | None -> f1 ``` ``` | Some (A.Kwd "=>") -> ``` ``` Stream.junk ts; ``` ``` let f2 = parse_imp symtab ts in ``` ``` IMP (f1, f2) ``` ``` | _ -> f1 ``` ```(** These functions parse a token stream to obtain a formula. ``` ``` It is a standard recursive descent procedure. ``` ``` @param ts A token stream. ``` ``` @return The resulting (sub-)formula. ``` ``` @raise CoAlgException if ts does not represent a formula. ``` ``` *) ``` ```and parse_or symtab ts = ``` ``` let f1 = parse_and symtab ts in ``` ``` match Stream.peek ts with ``` ``` | None -> f1 ``` ``` | Some (A.Kwd "|") -> ``` ``` Stream.junk ts; ``` ``` let f2 = parse_or symtab ts in ``` ``` OR (f1, f2) ``` ``` | _ -> f1 ``` ```(** These functions parse a token stream to obtain a formula. ``` ``` It is a standard recursive descent procedure. ``` ``` @param ts A token stream. ``` ``` @return The resulting (sub-)formula. ``` ``` @raise CoAlgException if ts does not represent a formula. ``` ``` *) ``` ```and parse_and symtab ts = ``` ``` let f1 = parse_cimp symtab ts in ``` ``` match Stream.peek ts with ``` ``` | None -> f1 ``` ``` | Some (A.Kwd "&") -> ``` ``` Stream.junk ts; ``` ``` let f2 = parse_and symtab ts in ``` ``` AND (f1, f2) ``` ``` | _ -> f1 ``` ```(** These functions parse a token stream to obtain a formula. ``` ``` It is a standard recursive descent procedure. ``` ``` @param ts A token stream. ``` ``` @return The resulting (sub-)formula. ``` ``` @raise CoAlgException if ts does not represent a formula. ``` ``` *) ``` ```and parse_cimp symtab ts = ``` ``` let f1 = parse_rest symtab ts in ``` ``` match Stream.peek ts with ``` ``` | None -> f1 ``` ``` | Some (A.Kwd "=o") -> ``` ``` Stream.junk ts; ``` ``` let f2 = parse_cimp symtab ts in ``` ``` NORM (f1, f2) ``` ``` | _ -> f1 ``` ```(** These functions parse a token stream to obtain a formula. ``` ``` It is a standard recursive descent procedure. ``` ``` @param ts A token stream. ``` ``` @return The resulting (sub-)formula. ``` ``` @raise CoAlgException if ts does not represent a formula. ``` ``` *) ``` ```and parse_rest symtab ts = ``` ``` let boxinternals noNo es = ``` ``` let n = ``` ``` if noNo then 0 ``` ``` else ``` ``` match Stream.next ts with ``` ``` | A.Int n when n >= 0 -> n ``` ``` | t -> A.printError mk_exn ~t ~ts " expected: " ``` ``` in ``` ``` let (s,denominator) = ``` ``` match Stream.peek ts with ``` ``` | Some (A.Ident s1) -> Stream.junk ts; (s1,0) ``` ``` | Some (A.Kwd c) when c = es -> ("", 0) ``` ``` | Some (A.Kwd "/") -> begin ``` ``` Stream.junk ts; ``` ``` match Stream.next ts with ``` ``` | A.Int denom when denom > 0 -> ("", denom) ``` ``` | t -> A.printError mk_exn ~t ~ts " (the denominator) expected: " ``` ``` end ``` ``` | _ -> A.printError mk_exn ~ts ("role name or \"" ^ es ^ "\" expected: ") ``` ``` in ``` ``` if (denominator < n) then begin ``` ``` let explanation = ``` ``` ("nominator="^(string_of_int n)^" but denominator="^(string_of_int denominator)) ``` ``` in ``` ``` A.printError mk_exn ~ts ("Nominator must not be larger than the denominator " ``` ``` ^"("^explanation^") at: " ``` ``` ) ``` ``` end; ``` ``` let _ = ``` ``` match Stream.next ts with ``` ``` | A.Kwd c when c = es -> () ``` ``` | t -> A.printError mk_exn ~t ~ts ("\"" ^ es ^ "\" expected: ") ``` ``` in ``` ``` (n, denominator, s) ``` ``` in ``` ``` let rec agentlist es = ``` ``` let allAgents = CoolUtils.cl_get_agents () in ``` ``` match Stream.next ts with ``` ``` | A.Int n -> if CoolUtils.TArray.elem n allAgents ``` ``` then n::(agentlist es) ``` ``` else A.printError mk_exn ~ts ("agent name \"" ^ (string_of_int n) ^ "\" unknonwn, see --agents: ") ``` ``` | A.Kwd c when c = es -> [] ``` ``` | _ -> A.printError mk_exn ~ts ("agent name or " ^ es ^ "\" expected: ") ``` ``` in ``` ``` match Stream.next ts with ``` ``` | A.Kwd "true" -> ``` ``` print_endline "*** Warning: \"true\" used as propositional variable."; ``` ``` AP "true" ``` ``` | A.Kwd "false" -> ``` ``` print_endline "*** Warning: \"false\" used as propositional variable."; ``` ``` AP "false" ``` ``` | A.Kwd "True" -> TRUE ``` ``` | A.Kwd "False" -> FALSE ``` ``` | A.Ident s -> ``` ``` (try ``` ``` let finder (x, _) = compare x s == 0 in ``` ``` let (_, symbol) = List.find finder symtab in ``` ``` VAR symbol ``` ``` with Not_found -> AP s) ``` ``` | A.Kwd "~" -> ``` ``` let f = parse_rest symtab ts in ``` ``` NOT f ``` ``` | A.Kwd "@" -> ``` ``` let s = ``` ``` match Stream.next ts with ``` ``` | A.Ident s when isNominal s -> s ``` ``` | t -> A.printError mk_exn ~t ~ts ("nominal expected: ") ``` ``` in ``` ``` let f = parse_rest symtab ts in ``` ``` AT (s, f) ``` ``` | A.Kwd "<" -> ``` ``` let (_, _, s) = boxinternals true ">" in ``` ``` let f1 = parse_rest symtab ts in ``` ``` EX (s, f1) ``` ``` | A.Kwd "[" -> ``` ``` let (_, _, s) = boxinternals true "]" in ``` ``` let f1 = parse_rest symtab ts in ``` ``` AX (s, f1) ``` ``` | A.Kwd "[{" -> ``` ``` let ls = agentlist "}]" in ``` ``` let f1 = parse_rest symtab ts in ``` ``` ENFORCES (ls, f1) ``` ``` | A.Kwd "<{" -> ``` ``` let ls = agentlist "}>" in ``` ``` let f1 = parse_rest symtab ts in ``` ``` ALLOWS (ls, f1) ``` ``` | A.Kwd "{>=" -> ``` ``` let (n, denom, s) = boxinternals false "}" in ``` ``` let f1 = parse_rest symtab ts in ``` ``` if (denom <> 0) ``` ``` then ATLEASTPROB (rational_of_int n denom, f1) ``` ``` else MIN (n, s, f1) ``` ``` | A.Kwd "{<=" -> ``` ``` let (n, denom, s) = boxinternals false "}" in ``` ``` let f1 = parse_rest symtab ts in ``` ``` if (denom <> 0) ``` ``` then A.printError mk_exn ~ts "Can not express {<= probability}" ``` ``` else MAX (n, s, f1) ``` ``` | A.Kwd "{<" -> ``` ``` let (n, denom, s) = boxinternals false "}" in ``` ``` let f1 = parse_rest symtab ts in ``` ``` if (denom <> 0) ``` ``` then LESSPROBFAIL (rational_of_int n denom, NOT f1) ``` ``` else A.printError mk_exn ~ts "The \"Less than\" < is not implemented yet" ``` ``` | A.Kwd "=" -> begin ``` ``` match Stream.next ts with ``` ``` (* | A.Int s *) ``` ``` | A.Kwd s ``` ``` | A.Ident s -> CONST s ``` ``` | _ -> A.printError mk_exn ~ts "constant = expects an identifier afterwards" ``` ``` end ``` ``` | A.Kwd "(" -> begin ``` ``` let f = parse_formula symtab ts in ``` ``` match Stream.next ts with ``` ``` | A.Kwd ")" -> f ``` ``` | A.Kwd "+" -> begin ``` ``` let f2 = parse_formula symtab ts in ``` ``` match Stream.next ts with ``` ``` | A.Kwd ")" -> CHC (f, f2) ``` ``` | t -> A.printError mk_exn ~t ~ts "\")\" expected: " ``` ``` end ``` ``` | t -> A.printError mk_exn ~t ~ts "\")\" or \"+\" expected: " ``` ``` end ``` ``` | A.Kwd "O" -> ``` ``` let f = parse_rest symtab ts in ``` ``` ID f ``` ``` | A.Kwd "[pi1]" -> ``` ``` let f = parse_rest symtab ts in ``` ``` FUS (true, f) ``` ``` | A.Kwd "[pi2]" -> ``` ``` let f = parse_rest symtab ts in ``` ``` FUS (false, f) ``` ``` | A.Kwd "μ" -> ``` ``` let (_, _, s) = boxinternals true "." in ``` ``` let symbol = Stream.next gensym in ``` ``` let newtab = (s, symbol) :: symtab in ``` ``` let f1 = parse_rest newtab ts in ``` ``` MU (symbol, f1) ``` ``` | A.Kwd "ν" -> ``` ``` let (_, _, s) = boxinternals true "." in ``` ``` let symbol = Stream.next gensym in ``` ``` let newtab = (s, symbol) :: symtab in ``` ``` let f1 = parse_rest newtab ts in ``` ``` NU (symbol, f1) ``` ``` | A.Kwd "AF" -> ``` ``` let f = parse_rest symtab ts in ``` ``` AF f ``` ``` | A.Kwd "EF" -> ``` ``` let f = parse_rest symtab ts in ``` ``` EF f ``` ``` | A.Kwd "AG" -> ``` ``` let f = parse_rest symtab ts in ``` ``` AG f ``` ``` | A.Kwd "EG" -> ``` ``` let f = parse_rest symtab ts in ``` ``` EG f ``` ``` | A.Kwd "A" -> ``` ``` assert (Stream.next ts = A.Kwd "("); ``` ``` let f1 = parse_formula symtab ts in ``` ``` assert (Stream.next ts = A.Kwd "U"); ``` ``` let f2 = parse_formula symtab ts in ``` ``` assert (Stream.next ts = A.Kwd ")"); ``` ``` AU (f1, f2) ``` ``` | A.Kwd "E" -> ``` ``` assert (Stream.next ts = A.Kwd "("); ``` ``` let f1 = parse_formula symtab ts in ``` ``` assert (Stream.next ts = A.Kwd "U"); ``` ``` let f2 = parse_formula symtab ts in ``` ``` assert (Stream.next ts = A.Kwd ")"); ``` ``` EU (f1, f2) ``` ``` | A.Kwd "AX" -> ``` ``` let f1 = parse_rest symtab ts in ``` ``` AX ("", f1) ``` ``` | A.Kwd "EX" -> ``` ``` let f1 = parse_rest symtab ts in ``` ``` EX ("", f1) ``` ``` | t -> A.printError mk_exn ~t ~ts ``` ``` "\"<\", \"[\", \"{>=\", \"{<=\", \"@\", \"~\", \"(\", ``` ``` \"True\", \"False\", \"=\", \"=o\", \"O\" or expected: " ``` ```(** Parses a sorted formula. ``` ``` @param ts A token stream. ``` ``` @return A sorted formula. ``` ``` @raise CoAlgException If ts does not represent a sorted formula. ``` ``` *) ``` ```let parse_sortedFormula ts = ``` ``` let nr = ``` ``` match Stream.peek ts with ``` ``` | Some (A.Int n) -> ``` ``` if n >= 0 then begin ``` ``` Stream.junk ts; ``` ``` let () = ``` ``` match Stream.next ts with ``` ``` | A.Kwd ":" -> () ``` ``` | t -> A.printError mk_exn ~t ~ts ("\":\" expected: ") ``` ``` in ``` ``` n ``` ``` end else ``` ``` A.printError mk_exn ~ts (" expected: ") ``` ``` | _ -> 0 ``` ``` in ``` ``` let f = parse_formula [] ts in ``` ``` (nr, f) ``` ```(** Parses a list of sorted formulae separated by ";". ``` ``` @param ts A token stream. ``` ``` @param acc The list of sorted formulae parsed so far. ``` ``` @return The resulting list of sorted formula. ``` ``` @raise CoAlgException if ts does not represent a list of sorted formulae. ``` ``` *) ``` ```let rec parse_sortedFormulaList ts acc = ``` ``` let f1 = parse_sortedFormula ts in ``` ``` match Stream.peek ts with ``` ``` | Some (A.Kwd ";") -> ``` ``` Stream.junk ts; ``` ``` parse_sortedFormulaList ts (f1::acc) ``` ``` | _ -> List.rev (f1::acc) ``` ```(** A common wrapper for import functions. ``` ``` @param fkt An import function. ``` ``` @param s A string. ``` ``` @return The object imported from s using fkt. ``` ``` @raise CoAlgException If ts is not empty. ``` ``` *) ``` ```let importWrapper fkt s = ``` ``` let ts = lexer s in ``` ``` try ``` ``` let res = fkt ts in ``` ``` let _ = ``` ``` match Stream.peek ts with ``` ``` | None -> () ``` ``` | Some _ -> A.printError mk_exn ~ts "EOS expected: " ``` ``` in ``` ``` res ``` ``` with Stream.Failure -> A.printError mk_exn ~ts "unexpected EOS" ``` ```(** Parses a string to obtain a formula. ``` ``` @param s A string representing a formula. ``` ``` @return The resulting formula. ``` ``` @raise CoAlgException if s does not represent a formula. ``` ``` *) ``` ```let importFormula s = importWrapper (parse_formula []) s ``` ```(** Parses a string to obtain a sorted formula. ``` ``` @param s A string representing a sorted formula. ``` ``` @return The sorted formula. ``` ``` @raise CoAlgException If s does not represent a sorted formula. ``` ``` *) ``` ```let importSortedFormula s = importWrapper parse_sortedFormula s ``` ```(** Parses a string to obtain a (sorted) formula query. ``` ``` @param s A string representing a formula query. ``` ``` @return A pair (tbox, f) where ``` ``` tbox is a list of sorted formulae representing the TBox; and ``` ``` f is a sorted formula. ``` ``` @raise CoAlgException if s does not represent a formula query. ``` ``` *) ``` ```let importQuery s = ``` ``` let fkt ts = ``` ``` match Stream.peek ts with ``` ``` | Some (A.Kwd "|-") -> ``` ``` Stream.junk ts; ``` ``` let f = parse_sortedFormula ts in ``` ``` ([], f) ``` ``` | _ -> ``` ``` let fl = parse_sortedFormulaList ts [] in ``` ``` match Stream.peek ts with ``` ``` | Some (A.Kwd "|-") -> ``` ``` Stream.junk ts; ``` ``` let f = parse_sortedFormula ts in ``` ``` (fl, f) ``` ``` | _ -> ``` ``` if List.length fl = 1 then ([], List.hd fl) ``` ``` else A.printError mk_exn ~ts "\"|-\" expected: " ``` ``` in ``` ``` importWrapper fkt s ``` ```(** Converts the negation of a formula to negation normal form ``` ``` by "pushing in" the negations "~". ``` ``` The symbols "<=>" and "=>" are substituted by their usual definitions. ``` ``` @param f A formula. ``` ``` @return A formula in negation normal form and not containing "<=>" or "=>" ``` ``` that is equivalent to ~f. ``` ``` *) ``` ```let rec nnfNeg f = ``` ``` match f with ``` ``` | TRUE -> FALSE ``` ``` | FALSE -> TRUE ``` ``` | AP _ -> NOT f ``` ``` | VAR _ -> f ``` ``` | NOT f1 -> nnf f1 ``` ``` | AT (s, f1) -> AT (s, nnfNeg f1) ``` ``` | OR (f1, f2) -> AND (nnfNeg f1, nnfNeg f2) ``` ``` | AND (f1, f2) -> OR (nnfNeg f1, nnfNeg f2) ``` ``` | EQU (f1, f2) -> OR (AND (nnf f1, nnfNeg f2), AND (nnf f2, nnfNeg f1)) ``` ``` | IMP (f1, f2) -> AND (nnf f1, nnfNeg f2) ``` ``` | EX (s, f1) -> AX (s, nnfNeg f1) ``` ``` | AX (s, f1) -> EX (s, nnfNeg f1) ``` ``` | ENFORCES (s, f1) -> ALLOWS (s, nnfNeg f1) ``` ``` | ALLOWS (s, f1) -> ENFORCES (s, nnfNeg f1) ``` ``` | MIN (n, s, f1) -> if n = 0 then FALSE else MAXEXCEPT (n-1, s, nnfNeg f1) ``` ``` | MAX (n, s, f1) -> MORETHAN (n, s, nnf f1) ``` ``` | MORETHAN (n, s, f1) -> MAXEXCEPT (n, s, nnfNeg f1) ``` ``` | MAXEXCEPT (n, s, f1) -> MORETHAN (n, s, nnfNeg f1) ``` ``` | ATLEASTPROB (p, f1) -> LESSPROBFAIL (p, nnfNeg f1) ``` ``` | LESSPROBFAIL (p, f1) -> ATLEASTPROB (p, nnfNeg f1) ``` ``` | CONST s -> CONSTN s ``` ``` | CONSTN s -> CONST s ``` ``` | ID (f1) -> ID (nnfNeg f1) ``` ``` | NORM(f1, f2) -> NORMN(nnfNeg f1, nnfNeg f2) ``` ``` | NORMN(f1, f2) -> NORM (nnfNeg f1, nnfNeg f2) ``` ``` | CHC (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2) ``` ``` | FUS (first, f1) -> FUS (first, nnfNeg f1) ``` ``` | MU (s, f1) -> NU(s, nnfNeg f1) ``` ``` | NU (s, f1) -> MU(s, nnfNeg f1) ``` ``` | AF _ ``` ``` | EF _ ``` ``` | AG _ ``` ``` | EG _ ``` ``` | AU _ ``` ``` | EU _ -> raise (CoAlgException ("nnfNeg: CTL should have been removed at this point")) ``` ```(** Converts a formula to negation normal form ``` ``` by "pushing in" the negations "~". ``` ``` The symbols "<=>" and "=>" are substituted by their usual definitions. ``` ``` @param f A formula. ``` ``` @return A formula in negation normal form and not containing "<=>" or "=>" ``` ``` that is equivalent to f. ``` ``` *) ``` ```and nnf f = ``` ``` match f with ``` ``` | TRUE ``` ``` | FALSE ``` ``` | AP _ ``` ``` | NOT (AP _) ``` ``` | CONST _ ``` ``` | CONSTN _ ``` ``` | VAR _ -> f ``` ``` | NOT f1 -> nnfNeg f1 ``` ``` | AT (s, f1) -> ``` ``` let ft1 = nnf f1 in ``` ``` if ft1 == f1 then f else AT (s, ft1) ``` ``` | OR (f1, f2) -> ``` ``` let ft1 = nnf f1 in ``` ``` let ft2 = nnf f2 in ``` ``` if ft1 == f1 && ft2 == f2 then f else OR (ft1, ft2) ``` ``` | AND (f1, f2) -> ``` ``` let ft1 = nnf f1 in ``` ``` let ft2 = nnf f2 in ``` ``` if ft1 == f1 && ft2 == f2 then f else AND (ft1, ft2) ``` ``` | EQU (f1, f2) -> AND (OR (nnfNeg f1, nnf f2), OR (nnfNeg f2, nnf f1)) ``` ``` | IMP (f1, f2) -> OR (nnfNeg f1, nnf f2) ``` ``` | EX (s, f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft == f1 then f else EX (s, ft) ``` ``` | AX (s, f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft == f1 then f else AX (s, ft) ``` ``` | ENFORCES (s, f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft == f1 then f else ENFORCES (s, ft) ``` ``` | ALLOWS (s, f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft == f1 then f else ALLOWS (s, ft) ``` ``` | MIN (n, s, f1) -> ``` ``` if n = 0 then TRUE ``` ``` else ``` ``` let ft = nnf f1 in ``` ``` MORETHAN (n-1,s,ft) ``` ``` | MAX (n, s, f1) -> ``` ``` let ft = nnfNeg f1 in ``` ``` MAXEXCEPT (n,s, ft) ``` ``` | MORETHAN (n,s,f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft = f1 then f else MORETHAN (n,s,ft) ``` ``` | MAXEXCEPT (n,s,f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft = f1 then f else MAXEXCEPT (n,s,ft) ``` ``` | ATLEASTPROB (p, f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft == f1 then f else ATLEASTPROB (p, ft) ``` ``` | LESSPROBFAIL (p, f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft == f1 then f else LESSPROBFAIL (p, ft) ``` ``` | ID (f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft == f1 then f else ID(ft) ``` ``` | NORM (f1, f2) -> ``` ``` let ft1 = nnf f1 in ``` ``` let ft2 = nnf f2 in ``` ``` if ft1 == f1 && ft2 == f2 then f else NORM (ft1, ft2) ``` ``` | NORMN (f1, f2) -> ``` ``` let ft1 = nnf f1 in ``` ``` let ft2 = nnf f2 in ``` ``` if ft1 == f1 && ft2 == f2 then f else NORMN (ft1, ft2) ``` ``` | CHC (f1, f2) -> ``` ``` let ft1 = nnf f1 in ``` ``` let ft2 = nnf f2 in ``` ``` if ft1 == f1 && ft2 == f2 then f else CHC (ft1, ft2) ``` ``` | FUS (first, f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft == f1 then f else FUS (first, ft) ``` ``` | MU (s, f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft == f1 then f else MU (s, ft) ``` ``` | NU (s, f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft == f1 then f else NU (s, ft) ``` ``` | AF _ ``` ``` | EF _ ``` ``` | AG _ ``` ``` | EG _ ``` ``` | AU _ ``` ``` | EU _ -> raise (CoAlgException ("nnf: CTL should have been removed at this point")) ``` ```(** Simplifies a formula. ``` ``` @param f A formula which must be in negation normal form. ``` ``` @return A formula in negation normal form that is equivalent to f. ``` ``` @raise CoAlgException if f is not in negation normal form. ``` ``` *) ``` ```let rec simplify f = ``` ``` match f with ``` ``` | TRUE ``` ``` | FALSE ``` ``` | AP _ ``` ``` | NOT (AP _) ``` ``` | VAR _ ``` ``` | NOT (VAR _) -> f ``` ``` | AT (s, f1) -> ``` ``` let ft = simplify f1 in ``` ``` begin ``` ``` match ft with ``` ``` | FALSE -> FALSE ``` ``` | TRUE -> TRUE ``` ``` | AT _ -> ft ``` ``` | AP s1 when s = s1 -> TRUE ``` ``` | NOT (AP s1) when s = s1 -> FALSE ``` ``` | _ -> if ft == f1 then f else AT (s, ft) ``` ``` end ``` ``` | OR (f1, f2) -> ``` ``` let ft1 = simplify f1 in ``` ``` let ft2 = simplify f2 in ``` ``` begin ``` ``` match ft1, ft2 with ``` ``` | TRUE, _ -> TRUE ``` ``` | FALSE, _ -> ft2 ``` ``` | _, TRUE -> TRUE ``` ``` | _, FALSE -> ft1 ``` ``` | _, _ -> ``` ``` if (f1 == ft1) && (f2 == ft2) then f ``` ``` else OR (ft1, ft2) ``` ``` end ``` ``` | AND (f1, f2) -> ``` ``` let ft1 = simplify f1 in ``` ``` let ft2 = simplify f2 in ``` ``` begin ``` ``` match ft1, ft2 with ``` ``` | TRUE, _ -> ft2 ``` ``` | FALSE, _ -> FALSE ``` ``` | _, TRUE -> ft1 ``` ``` | _, FALSE -> FALSE ``` ``` | _, _ -> ``` ``` if (f1 == ft1) && (f2 == ft2) then f ``` ``` else AND (ft1, ft2) ``` ``` end ``` ``` | NOT _ ``` ``` | EQU _ ``` ``` | IMP _ -> raise (CoAlgException "Formula is not in negation normal form.") ``` ``` | EX (s, f1) -> ``` ``` let ft = simplify f1 in ``` ``` begin ``` ``` match ft with ``` ``` | FALSE -> FALSE ``` ``` | _ -> if ft == f1 then f else EX (s, ft) ``` ``` end ``` ``` | AX (s, f1) -> ``` ``` let ft = simplify f1 in ``` ``` begin ``` ``` match ft with ``` ``` | TRUE -> TRUE ``` ``` | _ -> if ft == f1 then f else AX (s, ft) ``` ``` end ``` ``` | ENFORCES (s, f1) -> ``` ``` let ft = simplify f1 in ``` ``` begin ``` ``` match ft with ``` ``` (* Simplification rules are checked with dirks Generic.hs ``` ``` let enforce ls = M (C ls) ``` ``` let allow ls = Neg . M (C ls) . Neg ``` ``` provable \$ F <-> enforce [1,2] F ``` ``` *) ``` ``` | TRUE -> TRUE ``` ``` | FALSE -> FALSE ``` ``` | _ -> if ft == f1 then f else ENFORCES (s, ft) ``` ``` end ``` ``` | ALLOWS (s, f1) -> ``` ``` let ft = simplify f1 in ``` ``` begin ``` ``` match ft with ``` ``` (* Simplification rules are checked with dirks Generic.hs ``` ``` let enforce ls = M (C ls) ``` ``` let allow ls = Neg . M (C ls) . Neg ``` ``` provable \$ F <-> enforce [1,2] F ``` ``` *) ``` ``` | TRUE -> TRUE ``` ``` | FALSE -> FALSE ``` ``` | _ -> if ft == f1 then f else ALLOWS (s, ft) ``` ``` end ``` ``` | MIN (n, s, f1) -> ``` ``` if n = 0 then TRUE ``` ``` else ``` ``` let ft = simplify f1 in ``` ``` begin ``` ``` match ft with ``` ``` | FALSE -> FALSE ``` ``` | _ -> if ft == f1 then f else MIN (n, s, ft) ``` ``` end ``` ``` | MORETHAN (n,s,f1) -> ``` ``` let ft = simplify f1 in ``` ``` if ft == f1 then f else MORETHAN (n,s,ft) ``` ``` | MAXEXCEPT (n,s,f1) -> ``` ``` let ft = simplify f1 in ``` ``` if ft == f1 then f else MAXEXCEPT (n,s,ft) ``` ``` | MAX (n, s, f1) -> ``` ``` let ft = simplify f1 in ``` ``` begin ``` ``` match ft with ``` ``` | FALSE -> TRUE ``` ``` | _ -> if ft == f1 then f else MAX (n, s, ft) ``` ``` end ``` ``` | LESSPROBFAIL (p,f1) -> ``` ``` let ft1 = simplify f1 in ``` ``` if (ft1 == f1) then f else LESSPROBFAIL (p,ft1) ``` ``` | ATLEASTPROB (p,f1) -> ``` ``` let ft1 = simplify f1 in ``` ``` if (ft1 == f1) then f else ATLEASTPROB (p,ft1) ``` ``` | CONST _ ``` ``` | CONSTN _ -> f (* no simplifications possible *) ``` ``` | ID (f1) -> ``` ``` let ft1 = simplify f1 in ``` ``` begin ``` ``` match ft1 with ``` ``` | TRUE -> TRUE ``` ``` | FALSE -> FALSE ``` ``` | _ -> if (ft1 == f1) then f else ID (ft1) ``` ``` end ``` ``` (* todo: more simplifications for KLM? *) ``` ``` | NORM (f1, f2) -> ``` ``` let ft1 = simplify f1 in ``` ``` let ft2 = simplify f2 in ``` ``` begin ``` ``` match ft2 with ``` ``` | TRUE -> TRUE ``` ``` | _ -> ``` ``` if (f1 == ft1) && (f2 == ft2) then f ``` ``` else NORM (ft1, ft2) ``` ``` end ``` ``` | NORMN (f1, f2) -> ``` ``` let ft1 = simplify f1 in ``` ``` let ft2 = simplify f2 in ``` ``` begin ``` ``` match ft2 with ``` ``` | FALSE -> FALSE ``` ``` | _ -> ``` ``` if (f1 == ft1) && (f2 == ft2) then f ``` ``` else NORMN (ft1, ft2) ``` ``` end ``` ``` | CHC (f1, f2) -> ``` ``` let ft1 = simplify f1 in ``` ``` let ft2 = simplify f2 in ``` ``` begin ``` ``` match ft1, ft2 with ``` ``` | TRUE, TRUE -> TRUE ``` ``` | FALSE, FALSE -> FALSE ``` ``` | _, _ -> ``` ``` if (f1 == ft1) && (f2 == ft2) then f ``` ``` else CHC (ft1, ft2) ``` ``` end ``` ``` | FUS (first, f1) -> ``` ``` let ft = simplify f1 in ``` ``` begin ``` ``` match ft with ``` ``` | FALSE -> FALSE ``` ``` | TRUE -> TRUE ``` ``` | _ -> if ft == f1 then f else FUS (first, ft) ``` ``` end ``` ``` | MU (s, f1) -> ``` ``` let ft = simplify f1 in ``` ``` begin ``` ``` match ft with ``` ``` | TRUE -> TRUE ``` ``` | _ -> if ft == f1 then f else MU (s, ft) ``` ``` end ``` ``` | NU (s, f1) -> ``` ``` let ft = simplify f1 in ``` ``` begin ``` ``` match ft with ``` ``` | TRUE -> TRUE ``` ``` | _ -> if ft == f1 then f else NU (s, ft) ``` ``` end ``` ``` | AF _ ``` ``` | EF _ ``` ``` | AG _ ``` ``` | EG _ ``` ``` | AU _ ``` ``` | EU _ -> ``` ``` raise (CoAlgException ("nnf: CTL should have been removed at this point")) ``` ```(** Destructs an atomic proposition. ``` ``` @param f An atomic proposition. ``` ``` @return The name of the atomic proposition. ``` ``` @raise CoAlgException if f is not an atomic proposition. ``` ``` *) ``` ```let dest_ap f = ``` ``` match f with ``` ``` | AP s when not (isNominal s) -> s ``` ``` | _ -> raise (CoAlgException "Formula is not an atomic proposition.") ``` ```(** Destructs a nominal. ``` ``` @param f A nominal. ``` ``` @return The name of the nominal ``` ``` @raise CoAlgException if f is not a nominal. ``` ``` *) ``` ```let dest_nom f = ``` ``` match f with ``` ``` | AP s when isNominal s -> s ``` ``` | _ -> raise (CoAlgException "Formula is not a nominal.") ``` ```(** Destructs a negation. ``` ``` @param f A negation. ``` ``` @return The immediate subformula of the negation. ``` ``` @raise CoAlgException if f is not a negation. ``` ``` *) ``` ```let dest_not f = ``` ``` match f with ``` ``` | NOT f1 -> f1 ``` ``` | _ -> raise (CoAlgException "Formula is not a negation.") ``` ```(** Destructs an @-formula. ``` ``` @param f An @-formula. ``` ``` @return The name of the nominal and the immediate subformula of the @-formula. ``` ``` @raise CoAlgException if f is not an @-formula. ``` ``` *) ``` ```let dest_at f = ``` ``` match f with ``` ``` | AT (s, f1) -> (s, f1) ``` ``` | _ -> raise (CoAlgException "Formula is not an @-formula.") ``` ```(** Destructs an or-formula. ``` ``` @param f An or-formula. ``` ``` @return The two immediate subformulae of the or-formula. ``` ``` @raise CoAlgException if f is not an or-formula. ``` ``` *) ``` ```let dest_or f = ``` ``` match f with ``` ``` | OR (f1, f2) -> (f1, f2) ``` ``` | _ -> raise (CoAlgException "Formula is not an or-formula.") ``` ```(** Destructs an and-formula. ``` ``` @param f An and-formula. ``` ``` @return The two immediate subformulae of the and-formula. ``` ``` @raise CoAlgException if f is not an and-formula. ``` ``` *) ``` ```let dest_and f = ``` ``` match f with ``` ``` | AND (f1, f2) -> (f1, f2) ``` ``` | _ -> raise (CoAlgException "Formula is not an and-formula.") ``` ```(** Destructs an equivalence. ``` ``` @param f An equivalence. ``` ``` @return The two immediate subformulae of the equivalence. ``` ``` @raise CoAlgException if f is not an equivalence. ``` ``` *) ``` ```let dest_equ f = ``` ``` match f with ``` ``` | EQU (f1, f2) -> (f1, f2) ``` ``` | _ -> raise (CoAlgException "Formula is not an equivalence.") ``` ```(** Destructs an implication. ``` ``` @param f An implication. ``` ``` @return The two immediate subformulae of the implication. ``` ``` @raise CoAlgException if f is not an implication. ``` ``` *) ``` ```let dest_imp f = ``` ``` match f with ``` ``` | IMP (f1, f2) -> (f1, f2) ``` ``` | _ -> raise (CoAlgException "Formula is not an implication.") ``` ```(** Destructs an EX-formula. ``` ``` @param f An EX-formula. ``` ``` @return The role name and the immediate subformula of the EX-formula. ``` ``` @raise CoAlgException if f is not an EX-formula. ``` ``` *) ``` ```let dest_ex f = ``` ``` match f with ``` ``` | EX (s, f1) -> (s, f1) ``` ``` | _ -> raise (CoAlgException "Formula is not an EX-formula.") ``` ```(** Destructs an AX-formula. ``` ``` @param f An AX-formula. ``` ``` @return The role name and the immediate subformula of the AX-formula. ``` ``` @raise CoAlgException if f is not an AX-formula. ``` ``` *) ``` ```let dest_ax f = ``` ``` match f with ``` ``` | AX (s, f1) -> (s, f1) ``` ``` | _ -> raise (CoAlgException "Formula is not an AX-formula.") ``` ```(** Destructs a MIN-formula. ``` ``` @param f A MIN-formula. ``` ``` @return The number restriction, role name, ``` ``` and the immediate subformula of the MIN-formula. ``` ``` @raise CoAlgException if f is not a MIN-formula. ``` ``` *) ``` ```let dest_min f = ``` ``` match f with ``` ``` | MIN (n, s, f1) -> (n, s, f1) ``` ``` | _ -> raise (CoAlgException "Formula is not a MIN-formula.") ``` ```(** Destructs a MAX-formula. ``` ``` @param f A MAX-formula. ``` ``` @return The number restriction, role name, ``` ``` and the immediate subformula of the MAX-formula. ``` ``` @raise CoAlgException if f is not a MAX-formula. ``` ``` *) ``` ```let dest_max f = ``` ``` match f with ``` ``` | MAX (n, s, f1) -> (n, s, f1) ``` ``` | _ -> raise (CoAlgException "Formula is not a MAX-formula.") ``` ```(** Destructs a choice formula. ``` ``` @param f A choice formula. ``` ``` @return The two immediate subformulae of the choice formula. ``` ``` @raise CoAlgException if f is not a choice formula. ``` ``` *) ``` ```let dest_choice f = ``` ``` match f with ``` ``` | CHC (f1, f2) -> (f1, f2) ``` ``` | _ -> raise (CoAlgException "Formula is not a choice formula.") ``` ```(** Destructs a fusion formula. ``` ``` @param f A fusion formula. ``` ``` @return A pair (first, f1) where ``` ``` first is true iff f is a first projection; and ``` ``` f1 is the immediate subformulae of f. ``` ``` @raise CoAlgException if f is not a fusion formula. ``` ``` *) ``` ```let dest_fusion f = ``` ``` match f with ``` ``` | FUS (first, f1) -> (first, f1) ``` ``` | _ -> raise (CoAlgException "Formula is not a fusion formula.") ``` ```(** Tests whether a formula is the constant True. ``` ``` @param f A formula. ``` ``` @return True iff f is the constant True. ``` ``` *) ``` ```let is_true f = ``` ``` match f with ``` ``` | TRUE -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is the constant False. ``` ``` @param f A formula. ``` ``` @return True iff f is the constant False. ``` ``` *) ``` ```let is_false f = ``` ``` match f with ``` ``` | FALSE -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is an atomic proposition. ``` ``` @param f A formula. ``` ``` @return True iff f is an atomic proposition. ``` ``` *) ``` ```let is_ap f = ``` ``` match f with ``` ``` | AP s when not (isNominal s) -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is a nominal. ``` ``` @param f A formula. ``` ``` @return True iff f is a nominal. ``` ``` *) ``` ```let is_nom f = ``` ``` match f with ``` ``` | AP s when isNominal s -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is a negation. ``` ``` @param f A formula. ``` ``` @return True iff f is a negation. ``` ``` *) ``` ```let is_not f = ``` ``` match f with ``` ``` | NOT _ -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is an @-formula. ``` ``` @param f A formula. ``` ``` @return True iff f is an @-formula. ``` ``` *) ``` ```let is_at f = ``` ``` match f with ``` ``` | AT _ -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is an or-formula. ``` ``` @param f A formula. ``` ``` @return True iff f is an or-formula. ``` ``` *) ``` ```let is_or f = ``` ``` match f with ``` ``` | OR _ -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is an and-formula. ``` ``` @param f A formula. ``` ``` @return True iff f is an and-formula. ``` ``` *) ``` ```let is_and f = ``` ``` match f with ``` ``` | AND _ -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is an equivalence. ``` ``` @param f A formula. ``` ``` @return True iff f is an equivalence. ``` ``` *) ``` ```let is_equ f = ``` ``` match f with ``` ``` | EQU _ -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is an implication. ``` ``` @param f A formula. ``` ``` @return True iff f is an implication. ``` ``` *) ``` ```let is_imp f = ``` ``` match f with ``` ``` | IMP _ -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is an EX-formula. ``` ``` @param f A formula. ``` ``` @return True iff f is an EX-formula. ``` ``` *) ``` ```let is_ex f = ``` ``` match f with ``` ``` | EX _ -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is an AX-formula. ``` ``` @param f A formula. ``` ``` @return True iff f is an AX-formula. ``` ``` *) ``` ```let is_ax f = ``` ``` match f with ``` ``` | AX _ -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is a MIN-formula. ``` ``` @param f A formula. ``` ``` @return True iff f is a MIN-formula. ``` ``` *) ``` ```let is_min f = ``` ``` match f with ``` ``` | MIN _ -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is a MAX-formula. ``` ``` @param f A formula. ``` ``` @return True iff f is a MAX-formula. ``` ``` *) ``` ```let is_max f = ``` ``` match f with ``` ``` | MAX _ -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is a choice formula. ``` ``` @param f A formula. ``` ``` @return True iff f is a choice formula. ``` ``` *) ``` ```let is_choice f = ``` ``` match f with ``` ``` | CHC _ -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is a fusion formula. ``` ``` @param f A formula. ``` ``` @return True iff f is a fusion formula. ``` ``` *) ``` ```let is_fusion f = ``` ``` match f with ``` ``` | FUS _ -> true ``` ``` | _ -> false ``` ```(** The constant True. ``` ``` *) ``` ```let const_true = TRUE ``` ```(** The constant False. ``` ``` *) ``` ```let const_false = FALSE ``` ```(** Constructs an atomic proposition. ``` ``` @param s The name of the atomic proposition. ``` ``` @return The atomic proposition with name s. ``` ``` @raise CoAlgException if s is a nominal name. ``` ``` *) ``` ```let const_ap s = ``` ``` if isNominal s then raise (CoAlgException "The name indicates a nominal.") ``` ``` else AP s ``` ```(** Constructs a nominal. ``` ``` @param s The name of the nominal. ``` ``` @return A nominal with name s. ``` ``` @raise CoAlgException if s is not a nominal name. ``` ``` *) ``` ```let const_nom s = ``` ``` if isNominal s then AP s ``` ``` else raise (CoAlgException "The name does not indicate a nominal.") ``` ```(** Negates a formula. ``` ``` @param f A formula. ``` ``` @return The negation of f. ``` ``` *) ``` ```let const_not f = NOT f ``` ```(** Constructs an @-formula from a name and a formula. ``` ``` @param s A nominal name. ``` ``` @param f A formula. ``` ``` @return The formula AT (s, f). ``` ``` *) ``` ```let const_at s f = AT (s, f) ``` ```(** Constructs an or-formula from two formulae. ``` ``` @param f1 The first formula (LHS). ``` ``` @param f2 The second formula (LHS). ``` ``` @return The formula f1 | f2. ``` ``` *) ``` ```let const_or f1 f2 = OR (f1, f2) ``` ```(** Constructs an and-formula from two formulae. ``` ``` @param f1 The first formula (LHS). ``` ``` @param f2 The second formula (LHS). ``` ``` @return The formula f1 & f2. ``` ``` *) ``` ```let const_and f1 f2 = AND (f1, f2) ``` ```(** Constructs an equivalence from two formulae. ``` ``` @param f1 The first formula (LHS). ``` ``` @param f2 The second formula (LHS). ``` ``` @return The equivalence f1 <=> f2. ``` ``` *) ``` ```let const_equ f1 f2 = EQU (f1, f2) ``` ```(** Constructs an implication from two formulae. ``` ``` @param f1 The first formula (LHS). ``` ``` @param f2 The second formula (LHS). ``` ``` @return The implication f1 => f2. ``` ``` *) ``` ```let const_imp f1 f2 = IMP (f1, f2) ``` ```(** Constructs an EX-formula from a formula. ``` ``` @param s A role name. ``` ``` @param f A formula. ``` ``` @return The formula EX (s, f). ``` ``` *) ``` ```let const_ex s f = EX (s, f) ``` ```(** Constructs an AX-formula from a formula. ``` ``` @param s A role name. ``` ``` @param f A formula. ``` ``` @return The formula AX (s, f). ``` ``` *) ``` ```let const_ax s f = AX (s, f) ``` ```(** Constructs a MIN-formula from a formula. ``` ``` @param n A non-negative integer. ``` ``` @param s A role name. ``` ``` @param f A formula. ``` ``` @return The formula MIN f. ``` ``` @raise CoAlgException Iff n is negative. ``` ``` *) ``` ```let const_min n s f = ``` ``` if n < 0 then raise (CoAlgException "Negative cardinality constraint.") ``` ``` else MIN (n, s, f) ``` ```(** Constructs a MAX-formula from a formula. ``` ``` @param n A non-negative integer. ``` ``` @param s A role name. ``` ``` @param f A formula. ``` ``` @return The formula MAX f. ``` ``` @raise CoAlgException Iff n is negative. ``` ``` *) ``` ```let const_max n s f = ``` ``` if n < 0 then raise (CoAlgException "Negative cardinality constraint.") ``` ``` else MAX (n, s, f) ``` ```let const_enforces p f = ``` ``` ENFORCES (p,f) ``` ```let const_allows p f = ``` ``` ALLOWS (p,f) ``` ```(** Constructs a choice formula from two formulae. ``` ``` @param f1 The first formula (LHS). ``` ``` @param f2 The second formula (LHS). ``` ``` @return The formula (f1 + f2). ``` ``` *) ``` ```let const_choice f1 f2 = CHC (f1, f2) ``` ```(** Constructs a fusion formula. ``` ``` @param first True iff the result is a first projection. ``` ``` @param f1 A formula. ``` ``` @return The formula [pi1] f1 or [pi2] f1 (depending on first). ``` ``` *) ``` ```let const_fusion first f1 = FUS (first, f1) ``` ```(** Hash-consed formulae, which are in negation normal form, ``` ``` such that structural and physical equality coincide. ``` ``` Also CTL has been replaced by the equivalent μ-Calculus ``` ``` constructs ``` ``` *) ``` ```type hcFormula = (hcFormula_node, formula) HC.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 ``` ``` | 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 ``` ```(** Determines whether two formula nodes are structurally equal. ``` ``` @param f1 The first formula node. ``` ``` @param f2 The second formula node. ``` ``` @return True iff f1 and f2 are structurally equal. ``` ``` *) ``` ```let equal_hcFormula_node f1 f2 = ``` ``` match f1, f2 with ``` ``` | HCTRUE, HCTRUE -> true ``` ``` | HCFALSE, HCFALSE -> true ``` ``` | HCCONST s1, HCCONST s2 ``` ``` | HCCONSTN s1, HCCONSTN s2 ``` ``` | HCAP s1, HCAP s2 ``` ``` | HCNOT s1, HCNOT s2 -> compare s1 s2 = 0 ``` ``` | HCAT (s1, f1), HCAT (s2, f2) -> compare s1 s2 = 0 && f1 == f2 ``` ``` | HCOR (f1a, f1b), HCOR (f2a, f2b) ``` ``` | HCAND (f1a, f1b), HCAND (f2a, f2b) -> f1a == f2a && f1b == f2b ``` ``` | HCEX (s1, f1), HCEX (s2, f2) ``` ``` | HCAX (s1, f1), HCAX (s2, f2) -> compare s1 s2 = 0 && f1 == f2 ``` ``` | HCENFORCES (s1, f1), HCENFORCES (s2, f2) ``` ``` | HCALLOWS (s1, f1), HCALLOWS (s2, f2) -> compare s1 s2 = 0 && f1 == f2 ``` ``` | HCMORETHAN (n1, s1, f1), HCMORETHAN (n2, s2, f2) ``` ``` | HCMAXEXCEPT (n1, s1, f1), HCMAXEXCEPT (n2, s2, f2) -> ``` ``` n1 = n2 && compare s1 s2 = 0 && f1 == f2 ``` ``` | HCATLEASTPROB (p1, f1), HCATLEASTPROB (p2,f2) -> ``` ``` p1 = p2 && f1 == f2 ``` ``` | HCLESSPROBFAIL (p1, f1), HCLESSPROBFAIL (p2,f2) -> ``` ``` p1 = p2 && f1 == f2 ``` ``` | HCID f1, HCID f2 -> f1 == f2 ``` ``` | HCNORM (f1a, f1b), HCNORMN (f2a, f2b) -> f1a == f2a && f1b == f2b ``` ``` | HCCHC (f1a, f1b), HCCHC (f2a, f2b) -> f1a == f2a && f1b == f2b ``` ``` | HCFUS (first1, f1), HCFUS (first2, f2) -> first1 = first2 && f1 == f2 ``` ``` | HCMU (name1, f1), HCMU(name2, f2) -> compare name1 name2 = 0 && f1 == f2 ``` ``` | HCNU (name1, f1), HCNU(name2, f2) -> compare name1 name2 = 0 && f1 == f2 ``` ``` | HCVAR name1, HCVAR name2 -> compare name1 name2 = 0 ``` ```(* The rest could be shortened to | _ -> false, ``` ``` but then the compiler would not warn if the formula type is extended ``` ``` and this function is not updated accordingly.*) ``` ``` | HCTRUE, _ ``` ``` | HCFALSE, _ ``` ``` | HCAP _, _ ``` ``` | HCNOT _, _ ``` ``` | HCAT _, _ ``` ``` | HCOR _, _ ``` ``` | HCAND _, _ ``` ``` | HCEX _, _ ``` ``` | HCAX _, _ ``` ``` | HCENFORCES _, _ ``` ``` | HCALLOWS _, _ ``` ``` | HCMORETHAN _, _ ``` ``` | HCMAXEXCEPT _, _ ``` ``` | HCATLEASTPROB _, _ ``` ``` | HCLESSPROBFAIL _, _ ``` ``` | HCCONST _, _ ``` ``` | HCCONSTN _, _ ``` ``` | HCID _, _ ``` ``` | HCNORM _, _ ``` ``` | HCNORMN _, _ ``` ``` | HCCHC _, _ ``` ``` | HCFUS _, _ ``` ``` | HCMU _, _ ``` ``` | HCNU _, _ ``` ``` | HCVAR _, _ -> false ``` ```(** Computes the hash value of a formula node. ``` ``` @param f A formula node. ``` ``` @return The hash value of f. ``` ``` *) ``` ```let hash_hcFormula_node f = ``` ``` let base = 23 in (* should be larger than the no of constructors *) ``` ``` match f with ``` ``` | HCTRUE -> 0 ``` ``` | HCFALSE -> 1 ``` ``` | HCAP s ``` ``` | HCNOT s ``` ``` | HCVAR s -> base * Hashtbl.hash s + 1 ``` ``` | HCAT (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 2 ``` ``` | HCOR (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 5 ``` ``` | HCAND (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 6 ``` ``` | HCEX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 3 ``` ``` | HCAX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 4 ``` ``` | HCMORETHAN (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 7 ``` ``` | HCMAXEXCEPT (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 8 ``` ``` | HCATLEASTPROB (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 9 ``` ``` | HCLESSPROBFAIL (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 10 ``` ``` | HCCHC (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 11 ``` ``` | HCFUS (first, f1) -> base * (base * (Hashtbl.hash first) + f1.HC.hkey) + 13 ``` ``` | HCENFORCES (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 14 ``` ``` | HCALLOWS (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 15 ``` ``` | HCCONST s -> Hashtbl.hash s + 16 ``` ``` | HCCONSTN s -> Hashtbl.hash s + 17 ``` ``` | HCNORM (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 18 ``` ``` | HCNORMN (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 19 ``` ``` | HCID (f1) -> base * f1.HC.hkey + 20 ``` ``` | HCMU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 21 ``` ``` | HCNU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 22 ``` ```(** Determines the "real" formula of a formula node. ``` ``` @param f A formula node. ``` ``` @return The formula (in negation normal form) which corresponds to f. ``` ``` *) ``` ```let toFml_hcFormula_node f = ``` ``` match f with ``` ``` | HCTRUE -> TRUE ``` ``` | HCFALSE -> FALSE ``` ``` | HCAP s -> AP s ``` ``` | HCVAR s -> VAR s ``` ``` | HCNOT s -> NOT (AP s) ``` ``` | HCAT (s, f1) -> AT (s, f1.HC.fml) ``` ``` | HCOR (f1, f2) -> OR (f1.HC.fml, f2.HC.fml) ``` ``` | HCAND (f1, f2) -> AND (f1.HC.fml, f2.HC.fml) ``` ``` | HCEX (s, f1) -> EX (s, f1.HC.fml) ``` ``` | HCAX (s, f1) -> AX (s, f1.HC.fml) ``` ``` | HCENFORCES (s, f1) -> ENFORCES (s, f1.HC.fml) ``` ``` | HCALLOWS (s, f1) -> ALLOWS (s, f1.HC.fml) ``` ``` | HCMORETHAN (n, s, f1) -> MORETHAN (n, s, f1.HC.fml) ``` ``` | HCMAXEXCEPT (n, s, f1) -> MAXEXCEPT (n, s, f1.HC.fml) ``` ``` | HCATLEASTPROB (p, f1) -> ATLEASTPROB (p, f1.HC.fml) ``` ``` | HCLESSPROBFAIL (p, f1) -> LESSPROBFAIL (p, f1.HC.fml) ``` ``` | HCCONST s -> CONST s ``` ``` | HCCONSTN s -> CONSTN s ``` ``` | HCID (f1) -> ID(f1.HC.fml) ``` ``` | HCNORM (f1, f2) -> NORM(f1.HC.fml, f2.HC.fml) ``` ``` | HCNORMN (f1, f2) -> NORMN(f1.HC.fml, f2.HC.fml) ``` ``` | HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml) ``` ``` | HCFUS (first, f1) -> FUS (first, f1.HC.fml) ``` ``` | HCMU (var, f1) -> MU (var, f1.HC.fml) ``` ``` | HCNU (var, f1) -> NU (var, f1.HC.fml) ``` ```(** Determines the negation (in negation normal form) of a formula node. ``` ``` @param f A formula node. ``` ``` @return The negation (in negation normal form) of f. ``` ``` *) ``` ```let negNde_hcFormula_node f = ``` ``` match f with ``` ``` | HCTRUE -> HCFALSE ``` ``` | HCFALSE -> HCTRUE ``` ``` | HCAP s -> HCNOT s ``` ``` | HCNOT s -> HCAP s ``` ``` | HCVAR s -> f ``` ``` | HCAT (s, f1) -> HCAT (s, f1.HC.neg) ``` ``` | HCOR (f1, f2) -> HCAND (f1.HC.neg, f2.HC.neg) ``` ``` | HCAND (f1, f2) -> HCOR (f1.HC.neg, f2.HC.neg) ``` ``` | HCEX (s, f2) -> HCAX (s, f2.HC.neg) ``` ``` | HCAX (s, f2) -> HCEX (s, f2.HC.neg) ``` ``` | HCENFORCES (s, f2) -> HCALLOWS (s, f2.HC.neg) ``` ``` | HCALLOWS (s, f2) -> HCENFORCES (s, f2.HC.neg) ``` ``` | HCMORETHAN (n, s, f1) -> HCMAXEXCEPT (n, s, f1.HC.neg) ``` ``` | HCMAXEXCEPT (n, s, f1) -> HCMORETHAN (n, s, f1.HC.neg) ``` ``` | HCATLEASTPROB (p, f1) -> HCLESSPROBFAIL (p, f1.HC.neg) ``` ``` | HCLESSPROBFAIL (p, f1) -> HCATLEASTPROB (p, f1.HC.neg) ``` ``` | HCCONST s -> HCCONSTN s ``` ``` | HCCONSTN s -> HCCONST s ``` ``` | HCID (f1) -> HCID(f1.HC.neg) ``` ``` | HCNORM (f1, f2) -> HCNORMN(f1.HC.neg, f2.HC.neg) ``` ``` | HCNORMN (f1, f2) -> HCNORM(f1.HC.neg, f2.HC.neg) ``` ``` | HCCHC (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg) ``` ``` | HCFUS (first, f1) -> HCFUS (first, f1.HC.neg) ``` ``` | HCMU (name, f1) -> HCNU (name, f1.HC.neg) ``` ``` | HCNU (name, f1) -> HCMU (name, f1.HC.neg) ``` ```(** An instantiation of hash-consing for formulae. ``` ``` *) ``` ```module HcFormula = HC.Make( ``` ``` struct ``` ``` type nde = hcFormula_node ``` ``` type fml = formula ``` ``` let equal (n1 : nde) n2 = equal_hcFormula_node n1 n2 ``` ``` let hash (n : nde) = hash_hcFormula_node n ``` ``` let negNde (n : nde) = negNde_hcFormula_node n ``` ``` let toFml (n : nde) = toFml_hcFormula_node n ``` ``` end ``` ``` ) ``` ```(** Converts a formula into its hash-consed version. ``` ``` @param hcF A hash-cons table for formulae. ``` ``` @param f A formula in negation normal form. ``` ``` @return The hash-consed version of f. ``` ``` @raise CoAlgException if f is not in negation normal form. ``` ```*) ``` ```let rec hc_formula hcF f = ``` ``` match f with ``` ``` | TRUE -> HcFormula.hashcons hcF HCTRUE ``` ``` | FALSE -> HcFormula.hashcons hcF HCFALSE ``` ``` | AP s -> HcFormula.hashcons hcF (HCAP s) ``` ``` | VAR s -> HcFormula.hashcons hcF (HCVAR s) ``` ``` | NOT (AP s) -> HcFormula.hashcons hcF (HCNOT s) ``` ``` | AT (s, f1) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCAT (s, tf1)) ``` ``` | OR (f1, f2) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` let tf2 = hc_formula hcF f2 in ``` ``` HcFormula.hashcons hcF (HCOR (tf1, tf2)) ``` ``` | AND (f1, f2) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` let tf2 = hc_formula hcF f2 in ``` ``` HcFormula.hashcons hcF (HCAND (tf1, tf2)) ``` ``` | NOT _ ``` ``` | EQU _ ``` ``` | MIN _ ``` ``` | MAX _ ``` ``` | IMP _ -> raise (CoAlgException "Formula is not in negation normal form.") ``` ``` | EX (s, f1) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCEX (s, tf1)) ``` ``` | AX (s, f1) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCAX (s, tf1)) ``` ``` | ENFORCES (s, f1) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCENFORCES (s, tf1)) ``` ``` | ALLOWS (s, f1) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCALLOWS (s, tf1)) ``` ``` | MORETHAN (n, s, f1) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCMORETHAN (n, s, tf1)) ``` ``` | MAXEXCEPT (n, s, f1) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCMAXEXCEPT (n, s, tf1)) ``` ``` | ATLEASTPROB (p, f1) -> ``` ``` HcFormula.hashcons hcF (HCATLEASTPROB (p, hc_formula hcF f1)) ``` ``` | LESSPROBFAIL (p, f1) -> ``` ``` HcFormula.hashcons hcF (HCLESSPROBFAIL (p, hc_formula hcF f1)) ``` ``` | CONST s -> ``` ``` HcFormula.hashcons hcF (HCCONST s) ``` ``` | CONSTN s -> ``` ``` HcFormula.hashcons hcF (HCCONSTN s) ``` ``` | ID f1 -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCID tf1) ``` ``` | NORM (f1, f2) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` let tf2 = hc_formula hcF f2 in ``` ``` HcFormula.hashcons hcF (HCNORM (tf1, tf2)) ``` ``` | NORMN (f1, f2) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` let tf2 = hc_formula hcF f2 in ``` ``` HcFormula.hashcons hcF (HCNORMN (tf1, tf2)) ``` ``` | CHC (f1, f2) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` let tf2 = hc_formula hcF f2 in ``` ``` HcFormula.hashcons hcF (HCCHC (tf1, tf2)) ``` ``` | FUS (first, f1) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCFUS (first, tf1)) ``` ``` | MU (var, f1) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCMU (var, tf1)) ``` ``` | NU (var, f1) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCNU (var, tf1)) ``` ``` | AF _ ``` ``` | EF _ ``` ``` | AG _ ``` ``` | EG _ ``` ``` | AU _ ``` ``` | EU _ -> ``` ``` raise (CoAlgException ("nnf: CTL should have been removed at this point")) ``` ```(* Replace the Variable name in f with formula formula ``` ``` hc_replace foo φ ψ => ψ[foo |-> φ] ``` ``` *) ``` ```let rec hc_replace hcF name (formula: hcFormula) (f: hcFormula) = ``` ``` let func = hc_replace hcF name formula in ``` ``` let gennew = HcFormula.hashcons hcF in ``` ``` match f.HC.node with ``` ``` | HCTRUE ``` ``` | HCFALSE ``` ``` | HCAP _ ``` ``` | HCNOT _ ``` ``` | HCCONST _ ``` ``` | HCCONSTN _ -> f ``` ``` | HCVAR s -> ``` ``` if compare s name == 0 ``` ``` then formula ``` ``` else f ``` ``` | HCAT (s, f1) -> ``` ``` let nf1 = func f1 in ``` ``` if nf1 == f1 then f else gennew (HCAT(s, nf1)) ``` ``` | HCOR (f1, f2) -> ``` ``` let nf1 = func f1 in ``` ``` let nf2 = func f2 in ``` ``` if nf1 == f1 && nf2 == f2 then f else gennew (HCOR(nf1, nf2)) ``` ``` | HCAND (f1, f2) -> ``` ``` let nf1 = func f1 in ``` ``` let nf2 = func f2 in ``` ``` if nf1 == f1 && nf2 == f2 then f else gennew (HCAND(nf1, nf2)) ``` ``` | HCEX (s, f1) -> ``` ``` let nf1 = func f1 in ``` ``` if nf1 == f1 then f else gennew (HCEX(s, nf1)) ``` ``` | HCAX (s, f1) -> ``` ``` let nf1 = func f1 in ``` ``` if nf1 == f1 then f else gennew (HCAX(s, nf1)) ``` ``` | HCENFORCES (s, f1) -> ``` ``` let nf1 = func f1 in ``` ``` if nf1 == f1 then f else gennew (HCENFORCES(s, nf1)) ``` ``` | HCALLOWS (s, f1) -> ``` ``` let nf1 = func f1 in ``` ``` if nf1 == f1 then f else gennew (HCALLOWS(s, nf1)) ``` ``` | HCMORETHAN (n, s, f1) -> ``` ``` let nf1 = func f1 in ``` ``` if nf1 == f1 then f else gennew (HCMORETHAN(n, s, nf1)) ``` ``` | HCMAXEXCEPT (n, s, f1) -> ``` ``` let nf1 = func f1 in ``` ``` if nf1 == f1 then f else gennew (HCMAXEXCEPT(n, s, nf1)) ``` ``` | HCATLEASTPROB (p, f1) -> ``` ``` let nf1 = func f1 in ``` ``` if nf1 == f1 then f else gennew (HCATLEASTPROB(p, nf1)) ``` ``` | HCLESSPROBFAIL (p, f1) -> ``` ``` let nf1 = func f1 in ``` ``` if nf1 == f1 then f else gennew (HCLESSPROBFAIL(p, nf1)) ``` ``` | HCID f1 -> ``` ``` let nf1 = func f1 in ``` ``` if nf1 == f1 then f else gennew (HCID(nf1)) ``` ``` | HCNORM (f1, f2) -> ``` ``` let nf1 = func f1 in ``` ``` let nf2 = func f2 in ``` ``` if nf1 == f1 && nf2 == f2 then f else gennew (HCNORM(nf1, nf2)) ``` ``` | HCNORMN (f1, f2) -> ``` ``` let nf1 = func f1 in ``` ``` let nf2 = func f2 in ``` ``` if nf1 == f1 && nf2 == f2 then f else gennew (HCNORMN(nf1, nf2)) ``` ``` | HCCHC (f1, f2) -> ``` ``` let nf1 = func f1 in ``` ``` let nf2 = func f2 in ``` ``` if nf1 == f1 && nf2 == f2 then f else gennew (HCCHC(nf1, nf2)) ``` ``` | HCFUS (first, f1) -> ``` ``` let nf1 = func f1 in ``` ``` if nf1 == f1 then f else gennew (HCFUS(first, nf1)) ``` ``` | HCMU (var, f1) -> ``` ``` if compare var name != 0 then ``` ``` let nf1 = func f1 in ``` ``` if nf1 == f1 then f else gennew (HCMU(var, nf1)) ``` ``` else ``` ``` f ``` ``` | HCNU (var, f1) -> ``` ``` if compare var name != 0 then ``` ``` let nf1 = func f1 in ``` ``` if nf1 == f1 then f else gennew (HCNU(var, nf1)) ``` ``` else ``` ``` f ``` ```let rec hc_freeIn variable (f: hcFormula) = ``` ``` match f.HC.node with ``` ``` | HCTRUE ``` ``` | HCFALSE ``` ``` | HCAP _ ``` ``` | HCNOT _ ``` ``` | HCCONST _ ``` ``` | HCCONSTN _ -> false ``` ``` | HCVAR s -> ``` ``` if compare variable s == 0 ``` ``` then true ``` ``` else false ``` ``` | HCAT (s, f1) -> ``` ``` hc_freeIn variable f1 ``` ``` | HCOR (f1, f2) ``` ``` | HCAND (f1, f2) -> ``` ``` hc_freeIn variable f1 || hc_freeIn variable f2 ``` ``` | HCEX (_, f1) ``` ``` | HCAX (_, f1) ``` ``` | HCENFORCES (_, f1) ``` ``` | HCALLOWS (_, f1) ``` ``` | HCMORETHAN (_, _, f1) ``` ``` | HCMAXEXCEPT (_, _, f1) ``` ``` | HCATLEASTPROB (_, f1) ``` ``` | HCLESSPROBFAIL (_, f1) ``` ``` | HCID f1 -> ``` ``` hc_freeIn variable f1 ``` ``` | HCNORM (f1, f2) ``` ``` | HCNORMN (f1, f2) ``` ``` | HCCHC (f1, f2) -> ``` ``` hc_freeIn variable f1 || hc_freeIn variable f2 ``` ``` | HCFUS (first, f1) -> ``` ``` hc_freeIn variable f1 ``` ``` | HCMU (var, f1) ``` ``` | HCNU (var, f1) -> ``` ``` (* Do we need to exclude bound variables here? *) ``` ``` hc_freeIn variable f1 ``` ```(** An instantiation of a hash table (of the standard library) ``` ``` for hash-consed formulae. The test for equality ``` ``` and computing the hash value is done in constant time. ``` ``` *) ``` ```module HcFHt = Hashtbl.Make( ``` ``` struct ``` ``` type t = hcFormula ``` ``` let equal (f1 : t) f2 = f1.HC.tag = f2.HC.tag ``` ``` let hash (f : t) = f.HC.tag ``` ``` end ``` ``` ) ```