### Profile

Statistics
| Branch: | Revision:

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

1 2 3 4fd28192 Thorsten Wißmann ```(** This module implements coalgebraic formulae ``` ``` (e.g. parsing, printing, (de-)constructing, ...). ``` ``` @author Florian Widmann ``` ``` *) ``` ```module HC = HashConsing ``` ```module A = AltGenlex ``` f1fa9ad5 Thorsten Wißmann ```module L = List ``` ```module Str = String ``` 4fd28192 Thorsten Wißmann ```(** A general exception for all kinds of errors ``` ``` that can happen in the tableau procedure. ``` c5c25acf Christoph Egger ``` More specific information is given in the argument. ``` 4fd28192 Thorsten Wißmann ``` *) ``` ```exception CoAlgException of string ``` ```(** Indicates the sort of a sorted formula ``` ``` *) ``` ```type sort = int ``` e5422169 Thorsten Wißmann ```type rational = { nominator: int; denominator: int } ``` 86b07be8 Thorsten Wißmann ```let string_of_rational r = ``` ``` (string_of_int r.nominator)^"/"^(string_of_int r.denominator) ``` e5422169 Thorsten Wißmann ```let rational_of_int n d = { nominator = n; denominator = d } ``` 4fd28192 Thorsten Wißmann ```(** Defines (unsorted) coalgebraic formulae. ``` ``` *) ``` ```type formula = ``` ``` | TRUE ``` ``` | FALSE ``` 69a71d22 Thorsten Wißmann ``` | AP of string (* atomic proposition *) ``` 4fd28192 Thorsten Wißmann ``` | 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 ``` f1fa9ad5 Thorsten Wißmann ``` | ENFORCES of int list * formula ``` ``` | ALLOWS of int list * formula ``` 4fd28192 Thorsten Wißmann ``` | MIN of int * string * formula ``` ``` | MAX of int * string * formula ``` af276a36 Thorsten Wißmann ``` | MORETHAN of int * string * formula (* diamond of GML *) ``` ``` | MAXEXCEPT of int * string * formula (* box of GML *) ``` e5422169 Thorsten Wißmann ``` | ATLEASTPROB of rational * formula (* = {>= 0.5} C ---> C occurs with *) ``` c5c25acf Christoph Egger ``` (* probability of at least 50% *) ``` 9bae2c4f Thorsten Wißmann ``` | LESSPROBFAIL of rational * formula (* = [1/2] C = {< 1/2} ¬ C ---> C fails with *) ``` ``` (* probability of less than 50% *) ``` c49eea11 Thorsten Wißmann ``` | 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) *) ``` d58bba0f Dirk Pattinson ``` | CHC of formula * formula (* Choice is self-dual *) ``` 4fd28192 Thorsten Wißmann ``` | 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 ``` 4fd28192 Thorsten Wißmann ca99d0c6 Thorsten Wißmann ```exception ConversionException of formula ``` 4fd28192 Thorsten Wißmann ```(** 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 ``` c5c25acf Christoph Egger ``` | TRUE ``` ``` | FALSE ``` 4fd28192 Thorsten Wißmann ``` | AP _ -> 1 ``` ``` | NOT f1 ``` ``` | AT (_, f1) -> succ (sizeFormula f1) ``` c5c25acf Christoph Egger ``` | OR (f1, f2) ``` 4fd28192 Thorsten Wißmann ``` | AND (f1, f2) ``` c5c25acf Christoph Egger ``` | EQU (f1, f2) ``` 4fd28192 Thorsten Wißmann ``` | IMP (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2) ``` ``` | EX (_, f1) ``` f1fa9ad5 Thorsten Wißmann ``` | AX (_, f1) ``` ``` | ENFORCES (_, f1) ``` ``` | ALLOWS (_, f1) -> succ (sizeFormula f1) ``` 4fd28192 Thorsten Wißmann ``` | MIN (_, _, f1) ``` af276a36 Thorsten Wißmann ``` | MAX (_, _, f1) ``` 81435cc4 Thorsten Wißmann ``` | ATLEASTPROB (_, f1) ``` 9bae2c4f Thorsten Wißmann ``` | LESSPROBFAIL (_, f1) ``` af276a36 Thorsten Wißmann ``` | MORETHAN (_, _, f1) ``` ``` | MAXEXCEPT (_, _, f1) -> succ (sizeFormula f1) ``` 19f5dad0 Dirk Pattinson ``` | ID (f1) -> succ (sizeFormula f1) ``` ``` | NORM(f1, f2) ``` ``` | NORMN(f1, f2) -> succ (sizeFormula f1 + sizeFormula f2) ``` c49eea11 Thorsten Wißmann ``` | CONST _ ``` ``` | CONSTN _ -> 1 ``` d58bba0f Dirk Pattinson ``` | CHC (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2) ``` 4fd28192 Thorsten Wißmann ``` | FUS (_, f1) -> succ (sizeFormula f1) ``` a5f60450 Christoph Egger ``` | MU (_, f1) ``` ``` | NU (_, f1) -> succ (succ (sizeFormula f1)) ``` ``` | VAR _ -> 1 ``` 8cac0897 Christoph Egger ``` | AF _ | EF _ ``` ``` | AG _ | EG _ ``` ``` | AU _ | EU _ -> ``` c5c25acf Christoph Egger ``` raise (CoAlgException ("sizeFormula: CTL should have been removed at this point")) ``` 4fd28192 Thorsten Wißmann ```(** Determines the size of a sorted formula. ``` ``` @param f A sorted formula. ``` ``` @return The size of f. ``` ``` *) ``` ```let sizeSortedFormula f = sizeFormula (snd f) ``` c49eea11 Thorsten Wißmann ```(* think of func: (formula -> unit) -> formula -> unit as identity. ``` ``` iterate over all subformulae and collect side effects. *) ``` dbcce612 Thorsten Wißmann ```let rec iter func formula = ``` ``` func formula; ``` ``` let proc = iter func in (* proc = "process" *) ``` ``` match formula with ``` 309b71a5 Christoph Egger ``` | TRUE | FALSE | AP _ | VAR _ -> () ``` c49eea11 Thorsten Wißmann ``` | CONST _ ``` ``` | CONSTN _ -> () ``` dbcce612 Thorsten Wißmann ``` | 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) ``` 9bae2c4f Thorsten Wißmann ``` | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a) ``` dbcce612 Thorsten Wißmann ``` | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a ``` 19f5dad0 Dirk Pattinson ``` | ID(a) -> proc a ``` ``` | NORM(a, b) | NORMN(a, b) -> (proc a; proc b) ``` d58bba0f Dirk Pattinson ``` | CHC (a,b) -> (proc a ; proc b) ``` dbcce612 Thorsten Wißmann ``` | FUS (_,a) -> proc a ``` 309b71a5 Christoph Egger ``` | MU (_, f) | NU (_, f) -> proc f ``` fbffb079 Christoph Egger ``` | AF f | EF f | AG f | EG f -> proc f ``` ``` | AU (f1, f2) | EU (f1, f2) -> (proc f1; proc f2) ``` dbcce612 Thorsten Wißmann ```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 *) ``` 7b944a64 Christoph Egger ``` | TRUE | FALSE | AP _ | VAR _ -> formula ``` c49eea11 Thorsten Wißmann ``` | CONST _ ``` ``` | CONSTN _ -> formula ``` dbcce612 Thorsten Wißmann ``` (* 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) ``` 81435cc4 Thorsten Wißmann ``` | ATLEASTPROB (p,a) -> ATLEASTPROB (p, c a) ``` 9bae2c4f Thorsten Wißmann ``` | LESSPROBFAIL (p,a) -> LESSPROBFAIL (p, c a) ``` dbcce612 Thorsten Wißmann ``` | MORETHAN (n,s,a) -> MORETHAN (n,s,c a) ``` ``` | MAXEXCEPT (n,s,a) -> MAXEXCEPT (n,s,c a) ``` 19f5dad0 Dirk Pattinson ``` | ID(a) -> ID (c a) ``` ``` | NORM(a, b) -> NORM(c a, c b) ``` ``` | NORMN(a, b) -> NORMN(c a, c b) ``` dbcce612 Thorsten Wißmann ``` | CHC (a,b) -> CHC (c a, c b) ``` 7b944a64 Christoph Egger ``` | 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 ``` dbcce612 Thorsten Wißmann ``` func formula ``` ```let convertToK formula = (* tries to convert a formula to a pure K formula *) ``` ``` let helper formula = match formula with ``` ca99d0c6 Thorsten Wißmann ``` | ENFORCES _ | ALLOWS _ -> raise (ConversionException formula) ``` dbcce612 Thorsten Wißmann ``` | 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) ``` ca99d0c6 Thorsten Wißmann ``` | TRUE | FALSE ``` ``` | EQU _ | IMP _ ``` ``` | AND _ | OR _ ``` ``` | AP _ | NOT _ ``` dbcce612 Thorsten Wißmann ``` | AX _ | EX _ ``` d58bba0f Dirk Pattinson ``` | CHC _ | FUS _ -> formula ``` ca99d0c6 Thorsten Wißmann ``` | _ -> raise (ConversionException formula) ``` dbcce612 Thorsten Wißmann ``` in ``` ``` convert_post helper formula ``` ```let convertToGML formula = (* tries to convert a formula to a pure GML formula *) ``` ``` let helper formula = match formula with ``` ca99d0c6 Thorsten Wißmann ``` | ENFORCES _ | ALLOWS _ -> raise (ConversionException formula) ``` dbcce612 Thorsten Wißmann ``` | MORETHAN _ | MIN _ | MAX _ | MAXEXCEPT _ -> formula ``` ca99d0c6 Thorsten Wißmann ``` | TRUE | FALSE ``` ``` | EQU _ | IMP _ ``` ``` | AND _ | OR _ ``` ``` | AP _ | NOT _ ``` d58bba0f Dirk Pattinson ``` | CHC _ | FUS _ -> formula ``` dbcce612 Thorsten Wißmann ``` | AX (r,a) -> MAXEXCEPT (0,r,a) ``` ``` | EX (r,a) -> MORETHAN (0,r,a) ``` ca99d0c6 Thorsten Wißmann ``` | _ -> raise (ConversionException formula) ``` dbcce612 Thorsten Wißmann ``` in ``` ``` convert_post helper formula ``` 17af2794 Christoph Egger ```let gensym = Stream.from (fun i -> Some (Printf.sprintf "#gensym%x#" i)) ``` c5105465 Christoph Egger ```let convertToMu formula = ``` 17af2794 Christoph Egger ``` let helper formula = ``` c5c25acf Christoph Egger ``` match formula with ``` ``` | AF f1 -> ``` dcc8167f Christoph Egger ``` MU ("#AF#", (OR (f1, (AX ("", (VAR "#AF#")))))) ``` c5c25acf Christoph Egger ``` | EF f1 -> ``` dcc8167f Christoph Egger ``` MU ("#EF#", (OR (f1, (EX ("", (VAR "#EF#")))))) ``` c5c25acf Christoph Egger ``` | AG f1 -> ``` dcc8167f Christoph Egger ``` NU ("#AG#", (AND (f1, (AX ("", (VAR "#AG#")))))) ``` c5c25acf Christoph Egger ``` | EG f1 -> ``` dcc8167f Christoph Egger ``` NU ("#EG#", (AND (f1, (EX ("", (VAR "#EG#")))))) ``` c5c25acf Christoph Egger ``` | AU (f1, f2) -> ``` dcc8167f Christoph Egger ``` MU ("#AU#", (OR (f2, (AND (f1, (AX ("", (VAR "#AU#")))))))) ``` c5c25acf Christoph Egger ``` | EU (f1, f2) -> ``` dcc8167f Christoph Egger ``` MU ("#EU#", (OR (f2, (AND (f1, (EX ("", (VAR "#EU#")))))))) ``` c5c25acf Christoph Egger ``` | _ -> formula ``` c5105465 Christoph Egger ``` in ``` ``` convert_post helper formula ``` 4fd28192 Thorsten Wißmann ```(** 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 ``` c5c25acf Christoph Egger ``` | IMP _ -> 1 ``` 4fd28192 Thorsten Wißmann ``` | 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 ``` f1fa9ad5 Thorsten Wißmann ``` | ALLOWS (s, f1) -> ``` ``` Buffer.add_string sb "<{"; ``` c16fd631 Thorsten Wißmann ``` Buffer.add_string sb ( ``` ``` match s with ``` ``` | [] -> " " ``` ``` | _ ->(Str.concat " " (L.map string_of_int s)) ``` ``` ); ``` f1fa9ad5 Thorsten Wißmann ``` Buffer.add_string sb "}>"; ``` ``` prio 4 f1 ``` ``` | ENFORCES (s, f1) -> ``` ``` Buffer.add_string sb "[{"; ``` c16fd631 Thorsten Wißmann ``` Buffer.add_string sb ( ``` ``` match s with ``` ``` | [] -> " " ``` ``` | _ ->(Str.concat " " (L.map string_of_int s)) ``` ``` ); ``` f1fa9ad5 Thorsten Wißmann ``` Buffer.add_string sb "}]"; ``` ``` prio 4 f1 ``` 86b07be8 Thorsten Wißmann ``` | ATLEASTPROB (p, f1) -> ``` ``` Buffer.add_string sb "{>="; ``` ``` Buffer.add_string sb (string_of_rational p); ``` ``` Buffer.add_string sb "}"; ``` ``` prio 4 f1 ``` 9bae2c4f Thorsten Wißmann ``` | LESSPROBFAIL (p, f1) -> ``` c855ba91 Thorsten Wißmann ``` Buffer.add_string sb "{<"; ``` 86b07be8 Thorsten Wißmann ``` Buffer.add_string sb (string_of_rational p); ``` 9bae2c4f Thorsten Wißmann ``` Buffer.add_string sb "} ~ "; ``` 86b07be8 Thorsten Wißmann ``` prio 4 f1 ``` 4fd28192 Thorsten Wißmann ``` | 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 ``` af276a36 Thorsten Wißmann ``` | 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 <= *) ``` 19f5dad0 Dirk Pattinson ``` | 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 ")" ``` 4fd28192 Thorsten Wißmann ``` | CHC (f1, f2) -> ``` ``` Buffer.add_string sb "("; ``` ``` exportFormula_buffer sb f1; ``` ``` Buffer.add_string sb " + "; ``` ``` exportFormula_buffer sb f2; ``` ``` Buffer.add_string sb ")" ``` c49eea11 Thorsten Wißmann ``` | CONST s -> Buffer.add_string sb "="; ``` ``` Buffer.add_string sb s ``` ``` | CONSTN s -> Buffer.add_string sb "~="; ``` ``` Buffer.add_string sb s ``` 4fd28192 Thorsten Wißmann ``` | FUS (first, f1) -> ``` ``` Buffer.add_string sb (if first then "[pi1]" else "[pi2]"); ``` ``` prio 4 f1 ``` 8334c748 Christoph Egger ``` | MU (s, f1) -> ``` ``` Buffer.add_string sb "μ"; ``` d29d35f7 Christoph Egger ``` Buffer.add_string sb s; ``` 8334c748 Christoph Egger ``` Buffer.add_string sb "."; ``` ``` prio 4 f1 ``` ``` | NU (s, f1) -> ``` ``` Buffer.add_string sb "ν"; ``` c5c25acf Christoph Egger ``` Buffer.add_string sb s; ``` 8334c748 Christoph Egger ``` Buffer.add_string sb "."; ``` ``` prio 4 f1 ``` ``` | VAR s -> ``` ``` Buffer.add_string sb s ``` 0aa34675 Christoph Egger ``` | AF f1 -> ``` c5c25acf Christoph Egger ``` Buffer.add_string sb "AF "; ``` ``` prio 4 f1 ``` 0aa34675 Christoph Egger ``` | EF f1 -> ``` c5c25acf Christoph Egger ``` Buffer.add_string sb "EF "; ``` ``` prio 4 f1 ``` 0aa34675 Christoph Egger ``` | AG f1 -> ``` c5c25acf Christoph Egger ``` Buffer.add_string sb "AG "; ``` ``` prio 4 f1 ``` 0aa34675 Christoph Egger ``` | EG f1 -> ``` c5c25acf Christoph Egger ``` Buffer.add_string sb "EG "; ``` ``` prio 4 f1 ``` 0aa34675 Christoph Egger ``` | AU (f1, f2) -> ``` c5c25acf Christoph Egger ``` Buffer.add_string sb "A ("; ``` ``` prio 4 f1; ``` ``` Buffer.add_string sb " U "; ``` ``` prio 4 f2; ``` ``` Buffer.add_string sb ")" ``` 0aa34675 Christoph Egger ``` | EU (f1, f2) -> ``` c5c25acf Christoph Egger ``` Buffer.add_string sb "E ("; ``` ``` prio 4 f1; ``` ``` Buffer.add_string sb " U "; ``` ``` prio 4 f2; ``` ``` Buffer.add_string sb ")" ``` 4fd28192 Thorsten Wißmann ```(** 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 ``` ca99d0c6 Thorsten Wißmann ```let string_of_formula = exportFormula ``` 01b1ab69 Thorsten Wißmann ```(** export (CL)-formula suitable for tatl-inputs *) ``` ```let rec exportTatlFormula_buffer sb f = ``` ``` let prio n lf = ``` ``` let prionr = function ``` ``` | EQU _ -> 0 ``` c5c25acf Christoph Egger ``` | IMP _ -> 1 ``` 01b1ab69 Thorsten Wißmann ``` | OR _ -> 2 ``` ``` | AND _ -> 3 ``` ``` | _ -> 4 ``` ``` in ``` ``` if prionr lf < n then begin ``` ``` Buffer.add_char sb '('; ``` 064f3099 Thorsten Wißmann ``` exportTatlFormula_buffer sb lf; ``` 01b1ab69 Thorsten Wißmann ``` Buffer.add_char sb ')' ``` ``` end ``` 064f3099 Thorsten Wißmann ``` else exportTatlFormula_buffer sb lf ``` 01b1ab69 Thorsten Wißmann ``` 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 _ ``` c49eea11 Thorsten Wißmann ``` | CONST _ ``` ``` | CONSTN _ ``` 01b1ab69 Thorsten Wißmann ``` | CHC _ ``` 86b07be8 Thorsten Wißmann ``` | ATLEASTPROB _ ``` 9bae2c4f Thorsten Wißmann ``` | LESSPROBFAIL _ ``` 19f5dad0 Dirk Pattinson ``` | ID _ ``` ``` | NORM _ ``` ``` | NORMN _ ``` 8cac0897 Christoph Egger ``` | FUS _ ``` ``` | MU _ ``` ``` | NU _ ``` ``` | VAR _ ``` ``` | AF _ ``` ``` | EF _ ``` ``` | AG _ ``` ``` | EG _ ``` ``` | AU _ ``` ``` | EU _ -> raise (CoAlgException ("export to tatl: Not connectives of CL")) ``` 01b1ab69 Thorsten Wißmann ```let exportTatlFormula f = ``` ``` let sb = Buffer.create 128 in ``` ``` exportTatlFormula_buffer sb f; ``` ``` Buffer.contents sb ``` 4fd28192 Thorsten Wißmann ```(** 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 ``` b59059c4 Thorsten Wißmann ```(** 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 ``` 4fd28192 Thorsten Wißmann 19f5dad0 Dirk Pattinson ```(* NB: True and False are the propositional constants. Lower case ``` ``` true/false are regardes as atomic propositions and we emit a warning ``` ```*) ``` c5c25acf Christoph Egger ```let lexer = A.make_lexer ``` 19f5dad0 Dirk Pattinson ``` [":";";";"|-";"(";")";"=>";"<=>";"|";"&";"~";"@";"True";"False";"true";"false";"<";">";"[";"]";"{<=";"{>=";"}";"+";"[pi1]";"[pi2]" ``` b2f18312 Christoph Egger ``` ;"[{";"}]";"<{";"}>";",";"/";"{<";"=";"=o";"O" ``` ``` ;"μ";"ν";"." ``` c5c25acf Christoph Egger ``` ;"AX";"EX";"AF";"EF";"AG";"EG";"A";"E";"U" ``` ``` ] ``` 4fd28192 Thorsten Wißmann ```let mk_exn s = CoAlgException s ``` 63710593 Christoph Egger ```(** 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) -> ``` c5c25acf Christoph Egger ``` 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]) ``` 63710593 Christoph Egger ``` | 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) -> ``` c5c25acf Christoph Egger ``` 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]) ``` 63710593 Christoph Egger ``` | FUS (_,a) -> proc a ``` ``` | MU (s, f) -> ``` c5c25acf Christoph Egger ``` 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 ``` 63710593 Christoph Egger ``` let newfree = List.filter predicate free in ``` c5c25acf Christoph Egger ``` if newfree = [] then ``` ``` ("none", []) ``` ``` else ``` ``` ("μ", newfree) ``` 63710593 Christoph Egger ``` | NU (s, f) -> ``` c5c25acf Christoph Egger ``` 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 ``` 63710593 Christoph Egger ``` let newfree = List.filter predicate free in ``` c5c25acf Christoph Egger ``` if newfree = [] then ``` ``` ("none", []) ``` ``` else ``` ``` ("ν", newfree) ``` 63710593 Christoph Egger ``` | VAR s -> ("none", [s]) ``` 939f5bab Christoph Egger ``` | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ -> ``` c5c25acf Christoph Egger ``` raise (CoAlgException ("verifyMuAltFree: CTL should have been removed at this point")) ``` 939f5bab Christoph Egger 63710593 Christoph Egger ```(** 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) -> ``` c5c25acf Christoph Egger ``` let newNeg = (s, 0) :: negations in ``` ``` verifyMuMonotone newNeg f ``` 63710593 Christoph Egger ``` | VAR s -> ``` c5c25acf Christoph Egger ``` 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")) ``` 63710593 Christoph Egger ``` | NOT a -> ``` c5c25acf Christoph Egger ``` let increment (s, n) = (s, n+1) in ``` ``` let newNeg = List.map increment negations in ``` ``` verifyMuMonotone newNeg a ``` 939f5bab Christoph Egger ``` | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ -> ``` c5c25acf Christoph Egger ``` raise (CoAlgException ("verifyMuMonotone: CTL should have been removed at this point")) ``` 63710593 Christoph Egger 26cfb2dc Christoph Egger ```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) -> ``` c5c25acf Christoph Egger ``` let newUnguard = s :: unguarded in ``` ``` verifyMuGuarded newUnguard f ``` 26cfb2dc Christoph Egger ``` | VAR s -> ``` c5c25acf Christoph Egger ``` let finder x = compare x s == 0 in ``` ``` if List.exists finder unguarded then ``` ``` raise (CoAlgException ("formula not guarded")) ``` 939f5bab Christoph Egger ``` | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ -> ``` c5c25acf Christoph Egger ``` raise (CoAlgException ("verifyMuGuarded: CTL should have been removed at this point")) ``` 63710593 Christoph Egger ```let verifyFormula formula = ``` ``` verifyMuAltFree formula; ``` ``` verifyMuMonotone [] formula; ``` 26cfb2dc Christoph Egger ``` verifyMuGuarded [] formula ``` 63710593 Christoph Egger 4fd28192 Thorsten Wißmann ```(** 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. ``` ``` *) ``` 0b908205 Christoph Egger ```let rec parse_formula (symtab: 'a list) ts = ``` 1484d8cb Christoph Egger ``` let formula = (parse_imp symtab ts) in ``` ``` let f1 = convertToMu formula in ``` 4fd28192 Thorsten Wißmann ``` match Stream.peek ts with ``` ``` | None -> f1 ``` ``` | Some (A.Kwd "<=>") -> ``` ``` Stream.junk ts; ``` 0b908205 Christoph Egger ``` let f2 = parse_formula symtab ts in ``` 4fd28192 Thorsten Wißmann ``` 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. ``` ``` *) ``` 0b908205 Christoph Egger ```and parse_imp symtab ts= ``` ``` let f1 = parse_or symtab ts in ``` 4fd28192 Thorsten Wißmann ``` match Stream.peek ts with ``` ``` | None -> f1 ``` ``` | Some (A.Kwd "=>") -> ``` ``` Stream.junk ts; ``` 0b908205 Christoph Egger ``` let f2 = parse_imp symtab ts in ``` 4fd28192 Thorsten Wißmann ``` 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. ``` ``` *) ``` 0b908205 Christoph Egger ```and parse_or symtab ts = ``` ``` let f1 = parse_and symtab ts in ``` 4fd28192 Thorsten Wißmann ``` match Stream.peek ts with ``` ``` | None -> f1 ``` ``` | Some (A.Kwd "|") -> ``` ``` Stream.junk ts; ``` 0b908205 Christoph Egger ``` let f2 = parse_or symtab ts in ``` 4fd28192 Thorsten Wißmann ``` 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. ``` ``` *) ``` 0b908205 Christoph Egger ```and parse_and symtab ts = ``` ``` let f1 = parse_cimp symtab ts in ``` 4fd28192 Thorsten Wißmann ``` match Stream.peek ts with ``` ``` | None -> f1 ``` ``` | Some (A.Kwd "&") -> ``` ``` Stream.junk ts; ``` 0b908205 Christoph Egger ``` let f2 = parse_and symtab ts in ``` 4fd28192 Thorsten Wißmann ``` 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. ``` ``` *) ``` 0b908205 Christoph Egger ```and parse_cimp symtab ts = ``` ``` let f1 = parse_rest symtab ts in ``` 19f5dad0 Dirk Pattinson ``` match Stream.peek ts with ``` ``` | None -> f1 ``` ``` | Some (A.Kwd "=o") -> ``` ``` Stream.junk ts; ``` 0b908205 Christoph Egger ``` let f2 = parse_cimp symtab ts in ``` 19f5dad0 Dirk Pattinson ``` 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. ``` ``` *) ``` 0b908205 Christoph Egger ```and parse_rest symtab ts = ``` 4fd28192 Thorsten Wißmann ``` 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 ``` e5422169 Thorsten Wißmann ``` let (s,denominator) = ``` 4fd28192 Thorsten Wißmann ``` match Stream.peek ts with ``` e5422169 Thorsten Wißmann ``` | 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 ``` 4fd28192 Thorsten Wißmann ``` | _ -> A.printError mk_exn ~ts ("role name or \"" ^ es ^ "\" expected: ") ``` ``` in ``` eda515b6 Thorsten Wißmann ``` 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: " ``` ``` ) ``` e5422169 Thorsten Wißmann ``` end; ``` 4fd28192 Thorsten Wißmann ``` let _ = ``` ``` match Stream.next ts with ``` ``` | A.Kwd c when c = es -> () ``` ``` | t -> A.printError mk_exn ~t ~ts ("\"" ^ es ^ "\" expected: ") ``` ``` in ``` e5422169 Thorsten Wißmann ``` (n, denominator, s) ``` 4fd28192 Thorsten Wißmann ``` in ``` f1fa9ad5 Thorsten Wißmann ``` let rec agentlist es = ``` e2dc68f7 Thorsten Wißmann ``` let allAgents = CoolUtils.cl_get_agents () in ``` f1fa9ad5 Thorsten Wißmann ``` match Stream.next ts with ``` e2dc68f7 Thorsten Wißmann ``` | 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: ") ``` f1fa9ad5 Thorsten Wißmann ``` | A.Kwd c when c = es -> [] ``` ``` | _ -> A.printError mk_exn ~ts ("agent name or " ^ es ^ "\" expected: ") ``` ``` in ``` 4fd28192 Thorsten Wißmann ``` match Stream.next ts with ``` 19f5dad0 Dirk Pattinson ``` | 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" ``` 4fd28192 Thorsten Wißmann ``` | A.Kwd "True" -> TRUE ``` ``` | A.Kwd "False" -> FALSE ``` c3e13ca6 Christoph Egger ``` | A.Ident s -> ``` c5c25acf Christoph Egger ``` (try ``` ``` let finder (x, _) = compare x s == 0 in ``` ``` let (_, symbol) = List.find finder symtab in ``` ``` VAR symbol ``` ``` with Not_found -> AP s) ``` 4fd28192 Thorsten Wißmann ``` | A.Kwd "~" -> ``` 0b908205 Christoph Egger ``` let f = parse_rest symtab ts in ``` 4fd28192 Thorsten Wißmann ``` 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 ``` 0b908205 Christoph Egger ``` let f = parse_rest symtab ts in ``` 4fd28192 Thorsten Wißmann ``` AT (s, f) ``` c5c25acf Christoph Egger ``` | A.Kwd "<" -> ``` e5422169 Thorsten Wißmann ``` let (_, _, s) = boxinternals true ">" in ``` 0b908205 Christoph Egger ``` let f1 = parse_rest symtab ts in ``` c5c25acf Christoph Egger ``` EX (s, f1) ``` ``` | A.Kwd "[" -> ``` e5422169 Thorsten Wißmann ``` let (_, _, s) = boxinternals true "]" in ``` 0b908205 Christoph Egger ``` let f1 = parse_rest symtab ts in ``` 4fd28192 Thorsten Wißmann ``` AX (s, f1) ``` c5c25acf Christoph Egger ``` | A.Kwd "[{" -> ``` 7aa620ce Thorsten Wißmann ``` let ls = agentlist "}]" in ``` 0b908205 Christoph Egger ``` let f1 = parse_rest symtab ts in ``` 7aa620ce Thorsten Wißmann ``` ENFORCES (ls, f1) ``` c5c25acf Christoph Egger ``` | A.Kwd "<{" -> ``` 7aa620ce Thorsten Wißmann ``` let ls = agentlist "}>" in ``` 0b908205 Christoph Egger ``` let f1 = parse_rest symtab ts in ``` 7aa620ce Thorsten Wißmann ``` ALLOWS (ls, f1) ``` c5c25acf Christoph Egger ``` | A.Kwd "{>=" -> ``` e5422169 Thorsten Wißmann ``` let (n, denom, s) = boxinternals false "}" in ``` 0b908205 Christoph Egger ``` let f1 = parse_rest symtab ts in ``` e5422169 Thorsten Wißmann ``` if (denom <> 0) ``` ``` then ATLEASTPROB (rational_of_int n denom, f1) ``` ``` else MIN (n, s, f1) ``` c5c25acf Christoph Egger ``` | A.Kwd "{<=" -> ``` e5422169 Thorsten Wißmann ``` let (n, denom, s) = boxinternals false "}" in ``` 0b908205 Christoph Egger ``` let f1 = parse_rest symtab ts in ``` e5422169 Thorsten Wißmann ``` if (denom <> 0) ``` c855ba91 Thorsten Wißmann ``` then A.printError mk_exn ~ts "Can not express {<= probability}" ``` e5422169 Thorsten Wißmann ``` else MAX (n, s, f1) ``` c5c25acf Christoph Egger ``` | A.Kwd "{<" -> ``` c855ba91 Thorsten Wißmann ``` let (n, denom, s) = boxinternals false "}" in ``` 0b908205 Christoph Egger ``` let f1 = parse_rest symtab ts in ``` c855ba91 Thorsten Wißmann ``` if (denom <> 0) ``` 9bae2c4f Thorsten Wißmann ``` then LESSPROBFAIL (rational_of_int n denom, NOT f1) ``` c855ba91 Thorsten Wißmann ``` else A.printError mk_exn ~ts "The \"Less than\" < is not implemented yet" ``` c49eea11 Thorsten Wißmann ``` | 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 ``` 4fd28192 Thorsten Wißmann ``` | A.Kwd "(" -> begin ``` 0b908205 Christoph Egger ``` let f = parse_formula symtab ts in ``` 4fd28192 Thorsten Wißmann ``` match Stream.next ts with ``` ``` | A.Kwd ")" -> f ``` ``` | A.Kwd "+" -> begin ``` 0b908205 Christoph Egger ``` let f2 = parse_formula symtab ts in ``` 4fd28192 Thorsten Wißmann ``` 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 ``` 19f5dad0 Dirk Pattinson ``` | A.Kwd "O" -> ``` 0b908205 Christoph Egger ``` let f = parse_rest symtab ts in ``` 19f5dad0 Dirk Pattinson ``` ID f ``` 4fd28192 Thorsten Wißmann ``` | A.Kwd "[pi1]" -> ``` 0b908205 Christoph Egger ``` let f = parse_rest symtab ts in ``` 4fd28192 Thorsten Wißmann ``` FUS (true, f) ``` ``` | A.Kwd "[pi2]" -> ``` 0b908205 Christoph Egger ``` let f = parse_rest symtab ts in ``` 4fd28192 Thorsten Wißmann ``` FUS (false, f) ``` 8334c748 Christoph Egger ``` | A.Kwd "μ" -> ``` ``` let (_, _, s) = boxinternals true "." in ``` c5c25acf Christoph Egger ``` let symbol = Stream.next gensym in ``` ``` let newtab = (s, symbol) :: symtab in ``` 80aa0b2f Christoph Egger ``` let f1 = parse_rest newtab ts in ``` ``` MU (symbol, f1) ``` 8334c748 Christoph Egger ``` | A.Kwd "ν" -> ``` ``` let (_, _, s) = boxinternals true "." in ``` c5c25acf Christoph Egger ``` let symbol = Stream.next gensym in ``` ``` let newtab = (s, symbol) :: symtab in ``` 80aa0b2f Christoph Egger ``` let f1 = parse_rest newtab ts in ``` ``` NU (symbol, f1) ``` 0aa34675 Christoph Egger ``` | A.Kwd "AF" -> ``` c5c25acf Christoph Egger ``` let f = parse_rest symtab ts in ``` ``` AF f ``` 0aa34675 Christoph Egger ``` | A.Kwd "EF" -> ``` c5c25acf Christoph Egger ``` let f = parse_rest symtab ts in ``` ``` EF f ``` 0aa34675 Christoph Egger ``` | A.Kwd "AG" -> ``` c5c25acf Christoph Egger ``` let f = parse_rest symtab ts in ``` ``` AG f ``` 0aa34675 Christoph Egger ``` | A.Kwd "EG" -> ``` c5c25acf Christoph Egger ``` let f = parse_rest symtab ts in ``` ``` EG f ``` 0aa34675 Christoph Egger ``` | A.Kwd "A" -> ``` c5c25acf Christoph Egger ``` 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) ``` 0aa34675 Christoph Egger ``` | A.Kwd "E" -> ``` c5c25acf Christoph Egger ``` 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) ``` 0aa34675 Christoph Egger ``` | A.Kwd "AX" -> ``` c5c25acf Christoph Egger ``` let f1 = parse_rest symtab ts in ``` ``` AX ("", f1) ``` 0aa34675 Christoph Egger ``` | A.Kwd "EX" -> ``` c5c25acf Christoph Egger ``` let f1 = parse_rest symtab ts in ``` ``` EX ("", f1) ``` ``` | t -> A.printError mk_exn ~t ~ts ``` 19f5dad0 Dirk Pattinson ``` "\"<\", \"[\", \"{>=\", \"{<=\", \"@\", \"~\", \"(\", ``` ``` \"True\", \"False\", \"=\", \"=o\", \"O\" or expected: " ``` 8334c748 Christoph Egger 4fd28192 Thorsten Wißmann ```(** 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 = ``` c5c25acf Christoph Egger ``` let nr = ``` 4fd28192 Thorsten Wißmann ``` 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: ") ``` c5c25acf Christoph Egger ``` | _ -> 0 ``` 4fd28192 Thorsten Wißmann ``` in ``` 0b908205 Christoph Egger ``` let f = parse_formula [] ts in ``` 4fd28192 Thorsten Wißmann ``` (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. ``` ``` *) ``` 0b908205 Christoph Egger ```let importFormula s = importWrapper (parse_formula []) s ``` 4fd28192 Thorsten Wißmann ```(** 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) ``` c5c25acf Christoph Egger ``` | _ -> ``` 4fd28192 Thorsten Wißmann ``` 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 ``` ff4dc786 Christoph Egger ``` | VAR _ -> f ``` 4fd28192 Thorsten Wißmann ``` | 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) ``` f1fa9ad5 Thorsten Wißmann ``` | ENFORCES (s, f1) -> ALLOWS (s, nnfNeg f1) ``` ``` | ALLOWS (s, f1) -> ENFORCES (s, nnfNeg f1) ``` af276a36 Thorsten Wißmann ``` | 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) ``` 9bae2c4f Thorsten Wißmann ``` | ATLEASTPROB (p, f1) -> LESSPROBFAIL (p, nnfNeg f1) ``` ``` | LESSPROBFAIL (p, f1) -> ATLEASTPROB (p, nnfNeg f1) ``` c49eea11 Thorsten Wißmann ``` | CONST s -> CONSTN s ``` ``` | CONSTN s -> CONST s ``` 19f5dad0 Dirk Pattinson ``` | ID (f1) -> ID (nnfNeg f1) ``` ``` | NORM(f1, f2) -> NORMN(nnfNeg f1, nnfNeg f2) ``` ``` | NORMN(f1, f2) -> NORM (nnfNeg f1, nnfNeg f2) ``` c5c25acf Christoph Egger ``` | CHC (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2) ``` 4fd28192 Thorsten Wißmann ``` | FUS (first, f1) -> FUS (first, nnfNeg f1) ``` ff4dc786 Christoph Egger ``` | MU (s, f1) -> NU(s, nnfNeg f1) ``` ``` | NU (s, f1) -> MU(s, nnfNeg f1) ``` 8cac0897 Christoph Egger ``` | AF _ ``` ``` | EF _ ``` ``` | AG _ ``` ``` | EG _ ``` ``` | AU _ ``` ``` | EU _ -> raise (CoAlgException ("nnfNeg: CTL should have been removed at this point")) ``` c5c25acf Christoph Egger 4fd28192 Thorsten Wißmann ```(** 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 _ ``` c49eea11 Thorsten Wißmann ``` | NOT (AP _) ``` ``` | CONST _ ``` ff4dc786 Christoph Egger ``` | CONSTN _ ``` ``` | VAR _ -> f ``` 4fd28192 Thorsten Wißmann ``` | 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) ``` c5c25acf Christoph Egger ``` | EX (s, f1) -> ``` 4fd28192 Thorsten Wißmann ``` 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) ``` c5c25acf Christoph Egger ``` | ENFORCES (s, f1) -> ``` f1fa9ad5 Thorsten Wißmann ``` 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) ``` 4fd28192 Thorsten Wißmann ``` | MIN (n, s, f1) -> ``` ``` if n = 0 then TRUE ``` ``` else ``` ``` let ft = nnf f1 in ``` 87926e98 Thorsten Wißmann ``` MORETHAN (n-1,s,ft) ``` 4fd28192 Thorsten Wißmann ``` | MAX (n, s, f1) -> ``` af276a36 Thorsten Wißmann ``` let ft = nnfNeg f1 in ``` ``` MAXEXCEPT (n,s, ft) ``` ``` | MORETHAN (n,s,f1) -> ``` 4fd28192 Thorsten Wißmann ``` let ft = nnf f1 in ``` af276a36 Thorsten Wißmann ``` 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) ``` 86b07be8 Thorsten Wißmann ``` | ATLEASTPROB (p, f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft == f1 then f else ATLEASTPROB (p, ft) ``` 9bae2c4f Thorsten Wißmann ``` | LESSPROBFAIL (p, f1) -> ``` 86b07be8 Thorsten Wißmann ``` let ft = nnf f1 in ``` 9bae2c4f Thorsten Wißmann ``` if ft == f1 then f else LESSPROBFAIL (p, ft) ``` 19f5dad0 Dirk Pattinson ``` | 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) ``` 4fd28192 Thorsten Wißmann ``` | 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) ``` ff4dc786 Christoph Egger ``` | 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) ``` 8cac0897 Christoph Egger ``` | AF _ ``` ``` | EF _ ``` ``` | AG _ ``` ``` | EG _ ``` ``` | AU _ ``` ``` | EU _ -> raise (CoAlgException ("nnf: CTL should have been removed at this point")) ``` 4fd28192 Thorsten Wißmann ```(** 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 _ ``` fbffb079 Christoph Egger ``` | NOT (AP _) ``` ``` | VAR _ ``` ``` | NOT (VAR _) -> f ``` 4fd28192 Thorsten Wißmann ``` | 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 ``` ``` | _, _ -> ``` c5c25acf Christoph Egger ``` if (f1 == ft1) && (f2 == ft2) then f ``` 4fd28192 Thorsten Wißmann ``` 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 ``` ``` | _, _ -> ``` c5c25acf Christoph Egger ``` if (f1 == ft1) && (f2 == ft2) then f ``` 4fd28192 Thorsten Wißmann ``` 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 ``` f1fa9ad5 Thorsten Wißmann ``` | 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 ``` 4fd28192 Thorsten Wißmann ``` | 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 ``` af276a36 Thorsten Wißmann ``` | 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) ``` 4fd28192 Thorsten Wißmann ``` | 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 ``` 9bae2c4f Thorsten Wißmann ``` | LESSPROBFAIL (p,f1) -> ``` 86b07be8 Thorsten Wißmann ``` let ft1 = simplify f1 in ``` 9bae2c4f Thorsten Wißmann ``` if (ft1 == f1) then f else LESSPROBFAIL (p,ft1) ``` 86b07be8 Thorsten Wißmann ``` | ATLEASTPROB (p,f1) -> ``` ``` let ft1 = simplify f1 in ``` ``` if (ft1 == f1) then f else ATLEASTPROB (p,ft1) ``` c49eea11 Thorsten Wißmann ``` | CONST _ ``` ``` | CONSTN _ -> f (* no simplifications possible *) ``` 19f5dad0 Dirk Pattinson ``` | 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 ``` ``` | _ -> ``` c5c25acf Christoph Egger ``` if (f1 == ft1) && (f2 == ft2) then f ``` 19f5dad0 Dirk Pattinson ``` else NORM (ft1, ft2) ``` ``` end ``` ``` | NORMN (f1, f2) -> ``` ``` let ft1 = simplify f1 in ``` ``` let ft2 = simplify f2 in ``` ``` begin ``` ``` match ft2 with ``` ``` | FALSE -> FALSE ``` ``` | _ -> ``` c5c25acf Christoph Egger ``` if (f1 == ft1) && (f2 == ft2) then f ``` 19f5dad0 Dirk Pattinson ``` else NORMN (ft1, ft2) ``` ``` end ``` 4fd28192 Thorsten Wißmann ``` | CHC (f1, f2) -> ``` ``` let ft1 = simplify f1 in ``` ``` let ft2 = simplify f2 in ``` ``` begin ``` ``` match ft1, ft2 with ``` ``` | TRUE, TRUE -> TRUE ``` ``` | FALSE, FALSE -> FALSE ``` ``` | _, _ -> ``` c5c25acf Christoph Egger ``` if (f1 == ft1) && (f2 == ft2) then f ``` 4fd28192 Thorsten Wißmann ``` 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 ``` fbffb079 Christoph Egger ``` | 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 ``` 8cac0897 Christoph Egger ``` | AF _ ``` ``` | EF _ ``` ``` | AG _ ``` ``` | EG _ ``` ``` | AU _ ``` ``` | EU _ -> ``` c5c25acf Christoph Egger ``` raise (CoAlgException ("nnf: CTL should have been removed at this point")) ``` 4fd28192 Thorsten Wißmann ```(** 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 ``` c5c25acf Christoph Egger 4fd28192 Thorsten Wißmann ```(** The constant True. ``` ``` *) ``` ```let const_true = TRUE ``` ```(** The constant False. ``` ``` *) ``` ```let const_false = FALSE ``` c5c25acf Christoph Egger 4fd28192 Thorsten Wißmann ```(** 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 ``` c5c25acf Christoph Egger 4fd28192 Thorsten Wißmann ```(** 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. ``` c5c25acf Christoph Egger ``` *) ``` 4fd28192 Thorsten Wißmann ```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) ``` 7993e0bf Thorsten Wißmann ```let const_enforces p f = ``` ``` ENFORCES (p,f) ``` ```let const_allows p f = ``` ``` ALLOWS (p,f) ``` 4fd28192 Thorsten Wißmann ```(** 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. ``` 87d5082f Christoph Egger ``` Also CTL has been replaced by the equivalent μ-Calculus ``` ``` constructs ``` 4fd28192 Thorsten Wißmann ``` *) ``` ```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 ``` 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 ``` 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 ```(** 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 ``` c49eea11 Thorsten Wißmann ``` | HCCONST s1, HCCONST s2 ``` ``` | HCCONSTN s1, HCCONSTN s2 ``` 4fd28192 Thorsten Wißmann ``` | 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 ``` bc6db513 Thorsten Wißmann ``` | HCENFORCES (s1, f1), HCENFORCES (s2, f2) ``` ``` | HCALLOWS (s1, f1), HCALLOWS (s2, f2) -> compare s1 s2 = 0 && f1 == f2 ``` af276a36 Thorsten Wißmann ``` | HCMORETHAN (n1, s1, f1), HCMORETHAN (n2, s2, f2) ``` ``` | HCMAXEXCEPT (n1, s1, f1), HCMAXEXCEPT (n2, s2, f2) -> ``` c5c25acf Christoph Egger ``` n1 = n2 && compare s1 s2 = 0 && f1 == f2 ``` 86b07be8 Thorsten Wißmann ``` | HCATLEASTPROB (p1, f1), HCATLEASTPROB (p2,f2) -> ``` ``` p1 = p2 && f1 == f2 ``` 9bae2c4f Thorsten Wißmann ``` | HCLESSPROBFAIL (p1, f1), HCLESSPROBFAIL (p2,f2) -> ``` 86b07be8 Thorsten Wißmann ``` p1 = p2 && f1 == f2 ``` 19f5dad0 Dirk Pattinson ``` | HCID f1, HCID f2 -> f1 == f2 ``` ``` | HCNORM (f1a, f1b), HCNORMN (f2a, f2b) -> f1a == f2a && f1b == f2b ``` 4fd28192 Thorsten Wißmann ``` | HCCHC (f1a, f1b), HCCHC (f2a, f2b) -> f1a == f2a && f1b == f2b ``` ``` | HCFUS (first1, f1), HCFUS (first2, f2) -> first1 = first2 && f1 == f2 ``` a7ae917b Christoph Egger ``` | 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 ``` 4fd28192 Thorsten Wißmann ```(* 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 _, _ ``` f1fa9ad5 Thorsten Wißmann ``` | HCENFORCES _, _ ``` ``` | HCALLOWS _, _ ``` af276a36 Thorsten Wißmann ``` | HCMORETHAN _, _ ``` ``` | HCMAXEXCEPT _, _ ``` 86b07be8 Thorsten Wißmann ``` | HCATLEASTPROB _, _ ``` 9bae2c4f Thorsten Wißmann ``` | HCLESSPROBFAIL _, _ ``` c49eea11 Thorsten Wißmann ``` | HCCONST _, _ ``` ``` | HCCONSTN _, _ ``` 19f5dad0 Dirk Pattinson ``` | HCID _, _ ``` ``` | HCNORM _, _ ``` ``` | HCNORMN _, _ ``` 4fd28192 Thorsten Wißmann ``` | HCCHC _, _ ``` a7ae917b Christoph Egger ``` | HCFUS _, _ ``` ``` | HCMU _, _ ``` ``` | HCNU _, _ ``` ``` | HCVAR _, _ -> false ``` 4fd28192 Thorsten Wißmann ```(** Computes the hash value of a formula node. ``` ``` @param f A formula node. ``` ``` @return The hash value of f. ``` ``` *) ``` ```let hash_hcFormula_node f = ``` 19f5dad0 Dirk Pattinson ``` let base = 23 in (* should be larger than the no of constructors *) ``` 4fd28192 Thorsten Wißmann ``` match f with ``` ``` | HCTRUE -> 0 ``` ``` | HCFALSE -> 1 ``` ``` | HCAP s ``` 508e3c33 Christoph Egger ``` | HCNOT s ``` ``` | HCVAR s -> base * Hashtbl.hash s + 1 ``` 19f5dad0 Dirk Pattinson ``` | 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 ``` c49eea11 Thorsten Wißmann ``` | HCCONST s -> Hashtbl.hash s + 16 ``` ``` | HCCONSTN s -> Hashtbl.hash s + 17 ``` 19f5dad0 Dirk Pattinson ``` | 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 ``` 508e3c33 Christoph Egger ``` | HCMU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 21 ``` ``` | HCNU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 22 ``` 4fd28192 Thorsten Wißmann ```(** 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 ``` 508e3c33 Christoph Egger ``` | HCVAR s -> VAR s ``` 4fd28192 Thorsten Wißmann ``` | 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) ``` f1fa9ad5 Thorsten Wißmann ``` | HCENFORCES (s, f1) -> ENFORCES (s, f1.HC.fml) ``` ``` | HCALLOWS (s, f1) -> ALLOWS (s, f1.HC.fml) ``` af276a36 Thorsten Wißmann ``` | HCMORETHAN (n, s, f1) -> MORETHAN (n, s, f1.HC.fml) ``` ``` | HCMAXEXCEPT (n, s, f1) -> MAXEXCEPT (n, s, f1.HC.fml) ``` 86b07be8 Thorsten Wißmann ``` | HCATLEASTPROB (p, f1) -> ATLEASTPROB (p, f1.HC.fml) ``` 9bae2c4f Thorsten Wißmann ``` | HCLESSPROBFAIL (p, f1) -> LESSPROBFAIL (p, f1.HC.fml) ``` c49eea11 Thorsten Wißmann ``` | HCCONST s -> CONST s ``` ``` | HCCONSTN s -> CONSTN s ``` 19f5dad0 Dirk Pattinson ``` | 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) ``` 4fd28192 Thorsten Wißmann ``` | HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml) ``` ``` | HCFUS (first, f1) -> FUS (first, f1.HC.fml) ``` 508e3c33 Christoph Egger ``` | HCMU (var, f1) -> MU (var, f1.HC.fml) ``` ``` | HCNU (var, f1) -> NU (var, f1.HC.fml) ``` 4fd28192 Thorsten Wißmann ```(** 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 ``` 92feed46 Christoph Egger ``` | HCVAR s -> f ``` 4fd28192 Thorsten Wißmann ``` | 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) ``` f1fa9ad5 Thorsten Wißmann ``` | HCENFORCES (s, f2) -> HCALLOWS (s, f2.HC.neg) ``` ``` | HCALLOWS (s, f2) -> HCENFORCES (s, f2.HC.neg) ``` af276a36 Thorsten Wißmann ``` | HCMORETHAN (n, s, f1) -> HCMAXEXCEPT (n, s, f1.HC.neg) ``` ``` | HCMAXEXCEPT (n, s, f1) -> HCMORETHAN (n, s, f1.HC.neg) ``` 9bae2c4f Thorsten Wißmann ``` | HCATLEASTPROB (p, f1) -> HCLESSPROBFAIL (p, f1.HC.neg) ``` ``` | HCLESSPROBFAIL (p, f1) -> HCATLEASTPROB (p, f1.HC.neg) ``` c49eea11 Thorsten Wißmann ``` | HCCONST s -> HCCONSTN s ``` ``` | HCCONSTN s -> HCCONST s ``` 19f5dad0 Dirk Pattinson ``` | 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) ``` d58bba0f Dirk Pattinson ``` | HCCHC (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg) ``` 4fd28192 Thorsten Wißmann ``` | HCFUS (first, f1) -> HCFUS (first, f1.HC.neg) ``` 92feed46 Christoph Egger ``` | HCMU (name, f1) -> HCNU (name, f1.HC.neg) ``` ``` | HCNU (name, f1) -> HCMU (name, f1.HC.neg) ``` 4fd28192 Thorsten Wißmann ```(** 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) ``` 508e3c33 Christoph Egger ``` | VAR s -> HcFormula.hashcons hcF (HCVAR s) ``` 4fd28192 Thorsten Wißmann ``` | 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 _ ``` af276a36 Thorsten Wißmann ``` | MIN _ ``` ``` | MAX _ ``` 4fd28192 Thorsten Wißmann ``` | 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)) ``` f1fa9ad5 Thorsten Wißmann ``` | 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)) ``` af276a36 Thorsten Wißmann ``` | MORETHAN (n, s, f1) -> ``` 4fd28192 Thorsten Wißmann ``` let tf1 = hc_formula hcF f1 in ``` af276a36 Thorsten Wißmann ``` HcFormula.hashcons hcF (HCMORETHAN (n, s, tf1)) ``` ``` | MAXEXCEPT (n, s, f1) -> ``` 4fd28192 Thorsten Wißmann ``` let tf1 = hc_formula hcF f1 in ``` af276a36 Thorsten Wißmann ``` HcFormula.hashcons hcF (HCMAXEXCEPT (n, s, tf1)) ``` 86b07be8 Thorsten Wißmann ``` | ATLEASTPROB (p, f1) -> ``` ``` HcFormula.hashcons hcF (HCATLEASTPROB (p, hc_formula hcF f1)) ``` 9bae2c4f Thorsten Wißmann ``` | LESSPROBFAIL (p, f1) -> ``` ``` HcFormula.hashcons hcF (HCLESSPROBFAIL (p, hc_formula hcF f1)) ``` c49eea11 Thorsten Wißmann ``` | CONST s -> ``` ``` HcFormula.hashcons hcF (HCCONST s) ``` ``` | CONSTN s -> ``` ``` HcFormula.hashcons hcF (HCCONSTN s) ``` 19f5dad0 Dirk Pattinson ``` | 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)) ``` 4fd28192 Thorsten Wißmann ``` | 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)) ``` 508e3c33 Christoph Egger ``` | MU (var, f1) -> ``` c5c25acf Christoph Egger ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCMU (var, tf1)) ``` 508e3c33 Christoph Egger ``` | NU (var, f1) -> ``` c5c25acf Christoph Egger ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCNU (var, tf1)) ``` 8cac0897 Christoph Egger ``` | AF _ ``` ``` | EF _ ``` ``` | AG _ ``` ``` | EG _ ``` ``` | AU _ ``` ``` | EU _ -> ``` c5c25acf Christoph Egger ``` raise (CoAlgException ("nnf: CTL should have been removed at this point")) ``` 4fd28192 Thorsten Wißmann cc07e93d Christoph Egger ```(* 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 -> ``` c5c25acf Christoph Egger ``` if compare s name == 0 ``` ``` then formula ``` ``` else f ``` cc07e93d Christoph Egger ``` | HCAT (s, f1) -> ``` c5c25acf Christoph Egger ``` let nf1 = func f1 in ``` ``` if nf1 == f1 then f else gennew (HCAT(s, nf1)) ``` cc07e93d Christoph Egger ``` | HCOR (f1, f2) -> ``` c5c25acf Christoph Egger ``` let nf1 = func f1 in ``` ``` let nf2 = func f2 in ``` ``` if nf1 == f1 && nf2 == f2 then f else gennew (HCOR(nf1, nf2)) ``` cc07e93d Christoph Egger ``` | HCAND (f1, f2) -> ``` c5c25acf Christoph Egger ``` let nf1 = func f1 in ``` ``` let nf2 = func f2 in ``` ``` if nf1 == f1 && nf2 == f2 then f else gennew (HCAND(nf1, nf2)) ``` cc07e93d Christoph Egger ``` | HCEX (s, f1) -> ``` c5c25acf Christoph Egger ``` let nf1 = func f1 in ``` ``` if nf1 == f1 then f else gennew (HCEX(s, nf1)) ``` cc07e93d Christoph Egger ``` | HCAX (s, f1) -> ``` ``` let nf1 = func f1 in ``` c5c25acf Christoph Egger ``` if nf1 == f1 then f else gennew (HCAX(s, nf1)) ``` cc07e93d Christoph Egger ``` | HCENFORCES (s, f1) -> ``` c5c25acf Christoph Egger ``` let nf1 = func f1 in ``` ``` if nf1 == f1 then f else gennew (HCENFORCES(s, nf1)) ``` cc07e93d Christoph Egger ``` | HCALLOWS (s, f1) -> ``` ``` let nf1 = func f1 in ``` c5c25acf Christoph Egger ``` if nf1 == f1 then f else gennew (HCALLOWS(s, nf1)) ``` cc07e93d Christoph Egger ``` | HCMORETHAN (n, s, f1) -> ``` ``` let nf1 = func f1 in ``` c5c25acf Christoph Egger ``` if nf1 == f1 then f else gennew (HCMORETHAN(n, s, nf1)) ``` cc07e93d Christoph Egger ``` | HCMAXEXCEPT (n, s, f1) -> ``` c5c25acf Christoph Egger ``` let nf1 = func f1 in ``` ``` if nf1 == f1 then f else gennew (HCMAXEXCEPT(n, s, nf1)) ``` cc07e93d Christoph Egger ``` | HCATLEASTPROB (p, f1) -> ``` ``` let nf1 = func f1 in ``` c5c25acf Christoph Egger ``` if nf1 == f1 then f else gennew (HCATLEASTPROB(p, nf1)) ``` cc07e93d Christoph Egger ``` | HCLESSPROBFAIL (p, f1) -> ``` ``` let nf1 = func f1 in ``` c5c25acf Christoph Egger ``` if nf1 == f1 then f else gennew (HCLESSPROBFAIL(p, nf1)) ``` cc07e93d Christoph Egger ``` | HCID f1 -> ``` ``` let nf1 = func f1 in ``` c5c25acf Christoph Egger ``` if nf1 == f1 then f else gennew (HCID(nf1)) ``` cc07e93d Christoph Egger ``` | HCNORM (f1, f2) -> ``` c5c25acf Christoph Egger ``` let nf1 = func f1 in ``` ``` let nf2 = func f2 in ``` ``` if nf1 == f1 && nf2 == f2 then f else gennew (HCNORM(nf1, nf2)) ``` cc07e93d Christoph Egger ``` | HCNORMN (f1, f2) -> ``` c5c25acf Christoph Egger ``` let nf1 = func f1 in ``` ``` let nf2 = func f2 in ``` ``` if nf1 == f1 && nf2 == f2 then f else gennew (HCNORMN(nf1, nf2)) ``` cc07e93d Christoph Egger ``` | HCCHC (f1, f2) -> ``` c5c25acf Christoph Egger ``` let nf1 = func f1 in ``` ``` let nf2 = func f2 in ``` ``` if nf1 == f1 && nf2 == f2 then f else gennew (HCCHC(nf1, nf2)) ``` cc07e93d Christoph Egger ``` | HCFUS (first, f1) -> ``` ``` let nf1 = func f1 in ``` c5c25acf Christoph Egger ``` if nf1 == f1 then f else gennew (HCFUS(first, nf1)) ``` cc07e93d Christoph Egger ``` | HCMU (var, f1) -> ``` c5c25acf Christoph Egger ``` if compare var name != 0 then ``` 854e1338 Christoph Egger ``` let nf1 = func f1 in ``` c5c25acf Christoph Egger ``` if nf1 == f1 then f else gennew (HCMU(var, nf1)) ``` ``` else ``` ``` f ``` cc07e93d Christoph Egger ``` | HCNU (var, f1) -> ``` c5c25acf Christoph Egger ``` if compare var name != 0 then ``` 854e1338 Christoph Egger ``` let nf1 = func f1 in ``` c5c25acf Christoph Egger ``` if nf1 == f1 then f else gennew (HCNU(var, nf1)) ``` ``` else ``` ``` f ``` cc07e93d Christoph Egger 5e7c8aa1 Christoph Egger ```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 ``` cc07e93d Christoph Egger 4fd28192 Thorsten Wißmann ```(** 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 ``` ` )`