Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgFormula.ml @ de84f40d

History | View | Annotate | Download (66.9 KB)

1 4fd28192 Thorsten Wißmann
(** This module implements coalgebraic formulae
2
    (e.g. parsing, printing, (de-)constructing, ...).
3
    @author Florian Widmann
4
 *)
5
6
7
module HC = HashConsing
8
module A = AltGenlex
9 f1fa9ad5 Thorsten Wißmann
module L = List
10
module Str = String
11 4fd28192 Thorsten Wißmann
12
13
(** A general exception for all kinds of errors
14
    that can happen in the tableau procedure.
15 c5c25acf Christoph Egger
    More specific information is given in the argument.
16 4fd28192 Thorsten Wißmann
 *)
17
exception CoAlgException of string
18
19
(** Indicates the sort of a sorted formula
20
 *)
21
type sort = int
22
23 e5422169 Thorsten Wißmann
type rational = { nominator: int; denominator: int }
24
25 86b07be8 Thorsten Wißmann
let string_of_rational r =
26
    (string_of_int r.nominator)^"/"^(string_of_int r.denominator)
27
28 e5422169 Thorsten Wißmann
let rational_of_int n d = { nominator = n; denominator = d }
29
30 4fd28192 Thorsten Wißmann
(** Defines (unsorted) coalgebraic formulae.
31
 *)
32
type formula =
33
  | TRUE
34
  | FALSE
35 69a71d22 Thorsten Wißmann
  | AP of string (* atomic proposition *)
36 4fd28192 Thorsten Wißmann
  | NOT of formula
37
  | AT of string * formula
38
  | OR of formula * formula
39
  | AND of formula * formula
40
  | EQU of formula * formula
41
  | IMP of formula * formula
42
  | EX of string * formula
43
  | AX of string * formula
44 f1fa9ad5 Thorsten Wißmann
  | ENFORCES of int list * formula
45
  | ALLOWS   of int list * formula
46 4fd28192 Thorsten Wißmann
  | MIN of int * string * formula
47
  | MAX of int * string * formula
48 af276a36 Thorsten Wißmann
  | MORETHAN of int * string * formula (* diamond of GML *)
49
  | MAXEXCEPT of int * string * formula (* box of GML *)
50 e5422169 Thorsten Wißmann
  | ATLEASTPROB of rational * formula (* = {>= 0.5} C  ---> C occurs with *)
51 c5c25acf Christoph Egger
                                      (*  probability of at least 50% *)
52 9bae2c4f Thorsten Wißmann
  | LESSPROBFAIL of rational * formula (* = [1/2] C = {< 1/2} ¬ C ---> C fails with *)
53
                                        (* probability of less than 50% *)
54 c49eea11 Thorsten Wißmann
  | CONST of string  (* constant functor with value string *)
55
  | CONSTN of string  (* constant functor with value other than string *)
56 19f5dad0 Dirk Pattinson
  | ID of formula (* modality of the identity functor *)
57
  | NORM of formula * formula (* default implication *)
58
  | NORMN of formula * formula (* \neg NORM (\neg A, \neg B) *)
59 d58bba0f Dirk Pattinson
  | CHC of formula * formula (* Choice is self-dual *)
60 4fd28192 Thorsten Wißmann
  | FUS of bool * formula
61 d29d35f7 Christoph Egger
  | MU of string * formula
62
  | NU of string * formula
63 9a3b23cc Christoph Egger
  | VAR of string
64 b179a57f Christoph Egger
  | AF of formula
65
  | EF of formula
66
  | AG of formula
67
  | EG of formula
68
  | AU of formula * formula
69
  | EU of formula * formula
70 4fd28192 Thorsten Wißmann
71 ca99d0c6 Thorsten Wißmann
exception ConversionException of formula
72
73
74 4fd28192 Thorsten Wißmann
(** Defines sorted coalgebraic formulae.
75
 *)
76
type sortedFormula = sort * formula
77
78
79
(** Determines whether a name indicates a nominal.
80
    @param A string s.
81
    @return True iff s contains a prime character.
82
 *)
83
let isNominal s = String.contains s '\''
84
85
86
(** Determines the size of a formula.
87
    @param f A formula.
88
    @return The size of f.
89
 *)
90
let rec sizeFormula f =
91
  match f with
92 c5c25acf Christoph Egger
  | TRUE
93
  | FALSE
94 4fd28192 Thorsten Wißmann
  | AP _ -> 1
95
  | NOT f1
96
  | AT (_, f1) -> succ (sizeFormula f1)
97 c5c25acf Christoph Egger
  | OR (f1, f2)
98 4fd28192 Thorsten Wißmann
  | AND (f1, f2)
99 c5c25acf Christoph Egger
  | EQU (f1, f2)
100 4fd28192 Thorsten Wißmann
  | IMP (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
101
  | EX (_, f1)
102 f1fa9ad5 Thorsten Wißmann
  | AX (_, f1)
103
  | ENFORCES (_, f1)
104
  | ALLOWS (_, f1) -> succ (sizeFormula f1)
105 4fd28192 Thorsten Wißmann
  | MIN (_, _, f1)
106 af276a36 Thorsten Wißmann
  | MAX (_, _, f1)
107 81435cc4 Thorsten Wißmann
  | ATLEASTPROB (_, f1)
108 9bae2c4f Thorsten Wißmann
  | LESSPROBFAIL (_, f1)
109 af276a36 Thorsten Wißmann
  | MORETHAN (_, _, f1)
110
  | MAXEXCEPT (_, _, f1) -> succ (sizeFormula f1)
111 19f5dad0 Dirk Pattinson
  | ID (f1) -> succ (sizeFormula f1)
112
  | NORM(f1, f2)
113
  | NORMN(f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
114 c49eea11 Thorsten Wißmann
  | CONST _
115
  | CONSTN _ -> 1
116 d58bba0f Dirk Pattinson
  | CHC (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
117 4fd28192 Thorsten Wißmann
  | FUS (_, f1) -> succ (sizeFormula f1)
118 a5f60450 Christoph Egger
  | MU (_, f1)
119
  | NU (_, f1) -> succ (succ (sizeFormula f1))
120
  | VAR _ -> 1
121 8cac0897 Christoph Egger
  | AF _ | EF _
122
  | AG _ | EG _
123
  | AU _ | EU _ ->
124 c5c25acf Christoph Egger
            raise (CoAlgException ("sizeFormula: CTL should have been removed at this point"))
125 4fd28192 Thorsten Wißmann
126
(** Determines the size of a sorted formula.
127
    @param f A sorted formula.
128
    @return The size of f.
129
 *)
130
let sizeSortedFormula f = sizeFormula (snd f)
131
132
133 c49eea11 Thorsten Wißmann
(* think of func: (formula -> unit) -> formula -> unit as identity.
134
  iterate over all subformulae and collect side effects. *)
135 dbcce612 Thorsten Wißmann
let rec iter func formula =
136
    func formula;
137
    let proc = iter func in (* proc = "process" *)
138
    match formula with
139 309b71a5 Christoph Egger
    | TRUE | FALSE | AP _ | VAR _ -> ()
140 c49eea11 Thorsten Wißmann
    | CONST _
141
    | CONSTN _ -> ()
142 dbcce612 Thorsten Wißmann
    | NOT a | AT (_,a)
143
    | EX (_,a) | AX (_,a) -> proc a
144
    | OR (a,b) | AND (a,b)
145
    | EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
146
    | ENFORCES (_,a) | ALLOWS   (_,a)
147
    | MIN (_,_,a)    | MAX (_,_,a)
148 9bae2c4f Thorsten Wißmann
    | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
149 dbcce612 Thorsten Wißmann
    | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
150 19f5dad0 Dirk Pattinson
    | ID(a) -> proc a
151
    | NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
152 d58bba0f Dirk Pattinson
    | CHC (a,b)  -> (proc a ; proc b)
153 dbcce612 Thorsten Wißmann
    | FUS (_,a) -> proc a
154 309b71a5 Christoph Egger
    | MU (_, f) | NU (_, f) -> proc f
155 fbffb079 Christoph Egger
    | AF f | EF f | AG f | EG f -> proc f
156
    | AU (f1, f2) | EU (f1, f2) -> (proc f1; proc f2)
157 dbcce612 Thorsten Wißmann
158
let rec convert_post func formula = (* run over all subformulas in post order *)
159
  let c = convert_post func in (* some shorthand *)
160
  (* replace parts of the formula *)
161
  let formula = (match formula with
162
  (* 0-ary constructors *)
163 7b944a64 Christoph Egger
  | TRUE | FALSE | AP _ | VAR _ -> formula
164 c49eea11 Thorsten Wißmann
  | CONST _
165
  | CONSTN _ -> formula
166 dbcce612 Thorsten Wißmann
  (* unary *)
167
  | NOT a -> NOT (c a)
168
  | AT (s,a) -> AT (s,c a)
169
  (* binary *)
170
  | OR (a,b) -> OR (c a, c b)
171
  | AND (a,b) -> AND (c a, c b)
172
  | EQU (a,b) -> EQU (c a, c b)
173
  | IMP (a,b) -> IMP (c a, c b)
174
  | EX (s,a) -> EX (s,c a)
175
  | AX (s,a) -> AX (s,c a)
176
  | ENFORCES (s,a) -> ENFORCES (s,c a)
177
  | ALLOWS   (s,a) -> ALLOWS   (s,c a)
178
  | MIN (n,s,a) -> MIN (n,s,c a)
179
  | MAX (n,s,a) -> MAX (n,s,c a)
180 81435cc4 Thorsten Wißmann
  | ATLEASTPROB (p,a) -> ATLEASTPROB (p, c a)
181 9bae2c4f Thorsten Wißmann
  | LESSPROBFAIL (p,a) -> LESSPROBFAIL (p, c a)
182 dbcce612 Thorsten Wißmann
  | MORETHAN (n,s,a) -> MORETHAN (n,s,c a)
183
  | MAXEXCEPT (n,s,a) -> MAXEXCEPT (n,s,c a)
184 19f5dad0 Dirk Pattinson
  | ID(a) -> ID (c a)
185
  | NORM(a, b) -> NORM(c a, c b)
186
  | NORMN(a, b) -> NORMN(c a, c b)
187 dbcce612 Thorsten Wißmann
  | CHC (a,b) -> CHC (c a, c b)
188 7b944a64 Christoph Egger
  | FUS (s,a) -> FUS (s, c a)
189
  | MU (n, f1) -> MU (n, c f1)
190
  | NU (n, f1) -> NU (n, c f1)
191
  | AF f1 -> AF (c f1)
192
  | EF f1 -> EF (c f1)
193
  | AG f1 -> AG (c f1)
194
  | EG f1 -> EG (c f1)
195
  | AU (f1, f2) -> AU (c f1, c f2)
196
  | EU (f1, f2) -> AU (c f1, c f2))in
197 dbcce612 Thorsten Wißmann
  func formula
198
199
let convertToK formula = (* tries to convert a formula to a pure K formula *)
200
  let helper formula = match formula with
201 ca99d0c6 Thorsten Wißmann
  | ENFORCES _ | ALLOWS _ -> raise (ConversionException formula)
202 dbcce612 Thorsten Wißmann
  | MORETHAN (0,s,a) | MIN (1,s,a) -> EX (s,a)
203
  | MAX (0,s,a) -> AX (s, NOT a)
204
  | MAXEXCEPT (0,s,a) -> AX (s, a)
205 ca99d0c6 Thorsten Wißmann
  | TRUE | FALSE
206
  | EQU _ | IMP _
207
  | AND _ | OR _
208
  | AP _ | NOT _
209 dbcce612 Thorsten Wißmann
  | AX _ | EX _
210 d58bba0f Dirk Pattinson
  | CHC _ | FUS _ -> formula
211 ca99d0c6 Thorsten Wißmann
  | _ -> raise (ConversionException formula)
212 dbcce612 Thorsten Wißmann
  in
213
  convert_post helper formula
214
215
let convertToGML formula = (* tries to convert a formula to a pure GML formula *)
216
  let helper formula = match formula with
217 ca99d0c6 Thorsten Wißmann
  | ENFORCES _ | ALLOWS _ -> raise (ConversionException formula)
218 dbcce612 Thorsten Wißmann
  | MORETHAN _ | MIN _ | MAX _ | MAXEXCEPT _ -> formula
219 ca99d0c6 Thorsten Wißmann
  | TRUE | FALSE
220
  | EQU _ | IMP _
221
  | AND _ | OR _
222
  | AP _ | NOT _
223 d58bba0f Dirk Pattinson
  | CHC _ | FUS _ -> formula
224 dbcce612 Thorsten Wißmann
  | AX (r,a) -> MAXEXCEPT (0,r,a)
225
  | EX (r,a) -> MORETHAN  (0,r,a)
226 ca99d0c6 Thorsten Wißmann
  | _ -> raise (ConversionException formula)
227 dbcce612 Thorsten Wißmann
  in
228
  convert_post helper formula
229
230 17af2794 Christoph Egger
let gensym = Stream.from (fun i -> Some (Printf.sprintf "#gensym%x#" i))
231
232 c5105465 Christoph Egger
let convertToMu formula =
233 17af2794 Christoph Egger
  let helper formula =
234 c5c25acf Christoph Egger
    match formula with
235
    | AF f1 ->
236 dcc8167f Christoph Egger
       MU ("#AF#", (OR (f1, (AX ("", (VAR "#AF#"))))))
237 c5c25acf Christoph Egger
    | EF f1 ->
238 dcc8167f Christoph Egger
       MU ("#EF#", (OR (f1, (EX ("", (VAR "#EF#"))))))
239 c5c25acf Christoph Egger
    | AG f1 ->
240 dcc8167f Christoph Egger
       NU ("#AG#", (AND (f1, (AX ("", (VAR "#AG#"))))))
241 c5c25acf Christoph Egger
    | EG f1 ->
242 dcc8167f Christoph Egger
       NU ("#EG#", (AND (f1, (EX ("", (VAR "#EG#"))))))
243 c5c25acf Christoph Egger
    | AU (f1, f2) ->
244 dcc8167f Christoph Egger
       MU ("#AU#", (OR (f2, (AND (f1, (AX ("", (VAR "#AU#"))))))))
245 c5c25acf Christoph Egger
    | EU (f1, f2) ->
246 dcc8167f Christoph Egger
       MU ("#EU#", (OR (f2, (AND (f1, (EX ("", (VAR "#EU#"))))))))
247 c5c25acf Christoph Egger
    | _ -> formula
248 c5105465 Christoph Egger
  in
249
  convert_post helper formula
250
251 4fd28192 Thorsten Wißmann
(** Appends a string representation of a formula to a string buffer.
252
    Parentheses are ommited where possible
253
    where the preference rules are defined as usual.
254
    @param sb A string buffer.
255
    @param f A formula.
256
 *)
257
let rec exportFormula_buffer sb f =
258
  let negate = function
259
    | NOT f -> f
260
    | f -> NOT f
261
  in
262
  let prio n lf =
263
    let prionr = function
264
      | EQU _ -> 0
265 c5c25acf Christoph Egger
      | IMP _  -> 1
266 4fd28192 Thorsten Wißmann
      | OR _ -> 2
267
      | AND _ -> 3
268
      | _ -> 4
269
    in
270
    if prionr lf < n then begin
271
      Buffer.add_char sb '(';
272
      exportFormula_buffer sb lf;
273
      Buffer.add_char sb ')'
274
    end
275
    else exportFormula_buffer sb lf
276
  in
277
  match f with
278
  | TRUE -> Buffer.add_string sb "True"
279
  | FALSE -> Buffer.add_string sb "False"
280
  | AP s -> Buffer.add_string sb s
281
  | NOT f1 ->
282
      Buffer.add_string sb "~";
283
      prio 4 f1
284
  | AT (s, f1) ->
285
      Buffer.add_string sb "@ ";
286
      Buffer.add_string sb s;
287
      Buffer.add_string sb " ";
288
      prio 4 f1
289
  | OR (f1, f2) ->
290
      prio 2 f1;
291
      Buffer.add_string sb " | ";
292
      prio 2 f2
293
  | AND (f1, f2) ->
294
      prio 3 f1;
295
      Buffer.add_string sb " & ";
296
      prio 3 f2
297
  | EQU (f1, f2) ->
298
      prio 0 f1;
299
      Buffer.add_string sb " <=> ";
300
      prio 0 f2
301
  | IMP (f1, f2) ->
302
      prio 2 f1;
303
      Buffer.add_string sb " => ";
304
      prio 2 f2
305
  | EX (s, f1) ->
306
      Buffer.add_string sb "<";
307
      Buffer.add_string sb s;
308
      Buffer.add_string sb ">";
309
      prio 4 f1
310
  | AX (s, f1) ->
311
      Buffer.add_string sb "[";
312
      Buffer.add_string sb s;
313
      Buffer.add_string sb "]";
314
      prio 4 f1
315 f1fa9ad5 Thorsten Wißmann
  | ALLOWS (s, f1) ->
316
      Buffer.add_string sb "<{";
317 c16fd631 Thorsten Wißmann
      Buffer.add_string sb (
318
          match s with
319
          | [] -> " "
320
          | _ ->(Str.concat " " (L.map string_of_int s))
321
      );
322 f1fa9ad5 Thorsten Wißmann
      Buffer.add_string sb "}>";
323
      prio 4 f1
324
  | ENFORCES (s, f1) ->
325
      Buffer.add_string sb "[{";
326 c16fd631 Thorsten Wißmann
      Buffer.add_string sb (
327
          match s with
328
          | [] -> " "
329
          | _ ->(Str.concat " " (L.map string_of_int s))
330
      );
331 f1fa9ad5 Thorsten Wißmann
      Buffer.add_string sb "}]";
332
      prio 4 f1
333 86b07be8 Thorsten Wißmann
  | ATLEASTPROB (p, f1) ->
334
      Buffer.add_string sb "{>=";
335
      Buffer.add_string sb (string_of_rational p);
336
      Buffer.add_string sb "}";
337
      prio 4 f1
338 9bae2c4f Thorsten Wißmann
  | LESSPROBFAIL (p, f1) ->
339 c855ba91 Thorsten Wißmann
      Buffer.add_string sb "{<";
340 86b07be8 Thorsten Wißmann
      Buffer.add_string sb (string_of_rational p);
341 9bae2c4f Thorsten Wißmann
      Buffer.add_string sb "} ~ ";
342 86b07be8 Thorsten Wißmann
      prio 4 f1
343 4fd28192 Thorsten Wißmann
  | MIN (n, s, f1) ->
344
      Buffer.add_string sb "{>=";
345
      Buffer.add_string sb (string_of_int n);
346
      Buffer.add_string sb " ";
347
      Buffer.add_string sb s;
348
      Buffer.add_string sb "}";
349
      prio 4 f1
350
  | MAX (n, s, f1) ->
351
      Buffer.add_string sb "{<=";
352
      Buffer.add_string sb (string_of_int n);
353
      Buffer.add_string sb " ";
354
      Buffer.add_string sb s;
355
      Buffer.add_string sb "}";
356
      prio 4 f1
357 af276a36 Thorsten Wißmann
  | MORETHAN (n, s, f1) ->
358
      Buffer.add_string sb "{>";
359
      Buffer.add_string sb (string_of_int n);
360
      Buffer.add_string sb " ";
361
      Buffer.add_string sb s;
362
      Buffer.add_string sb "}";
363
      prio 4 f1
364
  | MAXEXCEPT (n, s, f1) ->
365
      Buffer.add_string sb "{<=";
366
      Buffer.add_string sb (string_of_int n);
367
      Buffer.add_string sb " ~ ";
368
      Buffer.add_string sb s;
369
      Buffer.add_string sb "}";
370
      prio 4 f1 (* actually is prio of ~ and not of <= *)
371 19f5dad0 Dirk Pattinson
  | ID (f1) ->
372
      Buffer.add_string sb "O";
373
      prio 4 f1
374
  | NORM(f1, f2) ->
375
      Buffer.add_string sb "(";
376
      exportFormula_buffer sb f1;
377
      Buffer.add_string sb " =o ";
378
      exportFormula_buffer sb f2;
379
      Buffer.add_string sb ")"
380
  | NORMN(f1, f2) ->
381
      Buffer.add_string sb "~(";
382
      exportFormula_buffer sb (negate f1);
383
      Buffer.add_string sb " =o ";
384
      exportFormula_buffer sb (negate f2);
385
      Buffer.add_string sb ")"
386 4fd28192 Thorsten Wißmann
  | CHC (f1, f2) ->
387
      Buffer.add_string sb "(";
388
      exportFormula_buffer sb f1;
389
      Buffer.add_string sb " + ";
390
      exportFormula_buffer sb f2;
391
      Buffer.add_string sb ")"
392 c49eea11 Thorsten Wißmann
  | CONST s -> Buffer.add_string sb "=";
393
      Buffer.add_string sb s
394
  | CONSTN s -> Buffer.add_string sb "~=";
395
      Buffer.add_string sb s
396 4fd28192 Thorsten Wißmann
  | FUS (first, f1) ->
397
      Buffer.add_string sb (if first then "[pi1]" else "[pi2]");
398
      prio 4 f1
399 8334c748 Christoph Egger
  | MU (s, f1) ->
400
      Buffer.add_string sb "μ";
401 d29d35f7 Christoph Egger
      Buffer.add_string sb s;
402 8334c748 Christoph Egger
      Buffer.add_string sb ".";
403
      prio 4 f1
404
  | NU (s, f1) ->
405
      Buffer.add_string sb "ν";
406 c5c25acf Christoph Egger
      Buffer.add_string sb s;
407 8334c748 Christoph Egger
      Buffer.add_string sb ".";
408
      prio 4 f1
409
  | VAR s ->
410
     Buffer.add_string sb s
411 0aa34675 Christoph Egger
  | AF f1 ->
412 c5c25acf Christoph Egger
     Buffer.add_string sb "AF ";
413
     prio 4 f1
414 0aa34675 Christoph Egger
  | EF f1 ->
415 c5c25acf Christoph Egger
     Buffer.add_string sb "EF ";
416
     prio 4 f1
417 0aa34675 Christoph Egger
  | AG f1 ->
418 c5c25acf Christoph Egger
     Buffer.add_string sb "AG ";
419
     prio 4 f1
420 0aa34675 Christoph Egger
  | EG f1 ->
421 c5c25acf Christoph Egger
     Buffer.add_string sb "EG ";
422
     prio 4 f1
423 0aa34675 Christoph Egger
  | AU (f1, f2) ->
424 c5c25acf Christoph Egger
     Buffer.add_string sb "A (";
425
     prio 4 f1;
426
     Buffer.add_string sb " U ";
427
     prio 4 f2;
428
     Buffer.add_string sb ")"
429 0aa34675 Christoph Egger
  | EU (f1, f2) ->
430 c5c25acf Christoph Egger
     Buffer.add_string sb "E (";
431
     prio 4 f1;
432
     Buffer.add_string sb " U ";
433
     prio 4 f2;
434
     Buffer.add_string sb ")"
435 4fd28192 Thorsten Wißmann
436
(** Converts a formula into a string representation.
437
    Parentheses are ommited where possible
438
    where the preference rules are defined as usual.
439
    @param f A formula.
440
    @return A string representing f.
441
 *)
442
let exportFormula f =
443
  let sb = Buffer.create 128 in
444
  exportFormula_buffer sb f;
445
  Buffer.contents sb
446
447 ca99d0c6 Thorsten Wißmann
let string_of_formula = exportFormula
448
449 01b1ab69 Thorsten Wißmann
(** export (CL)-formula suitable for tatl-inputs *)
450
let rec exportTatlFormula_buffer sb f =
451
  let prio n lf =
452
    let prionr = function
453
      | EQU _ -> 0
454 c5c25acf Christoph Egger
      | IMP _  -> 1
455 01b1ab69 Thorsten Wißmann
      | OR _ -> 2
456
      | AND _ -> 3
457
      | _ -> 4
458
    in
459
    if prionr lf < n then begin
460
      Buffer.add_char sb '(';
461 064f3099 Thorsten Wißmann
      exportTatlFormula_buffer sb lf;
462 01b1ab69 Thorsten Wißmann
      Buffer.add_char sb ')'
463
    end
464 064f3099 Thorsten Wißmann
    else exportTatlFormula_buffer sb lf
465 01b1ab69 Thorsten Wißmann
  in
466
  match f with
467
  | TRUE -> Buffer.add_string sb "(p \\/ ~p)"
468
  | FALSE -> Buffer.add_string sb "(p /\\ ~p)"
469
  | AP s -> Buffer.add_string sb s
470
  | NOT f1 ->
471
      Buffer.add_string sb "~";
472
      prio 4 f1
473
  | OR (f1, f2) ->
474
      prio 2 f1;
475
      Buffer.add_string sb " \\/ ";
476
      prio 2 f2
477
  | AND (f1, f2) ->
478
      prio 3 f1;
479
      Buffer.add_string sb " /\\ ";
480
      prio 3 f2
481
  | EQU (f1, f2) ->
482
      prio 0 (AND (IMP (f1,f2), IMP (f2,f1)))
483
  | IMP (f1, f2) ->
484
      prio 2 f1;
485
      Buffer.add_string sb " -> ";
486
      prio 2 f2
487
  | ALLOWS (s, f1) ->
488
      Buffer.add_string sb "<<";
489
      Buffer.add_string sb (
490
          match s with
491
          | [] -> " "
492
          | _ ->(Str.concat "," (L.map string_of_int s))
493
      );
494
      Buffer.add_string sb ">>X ";
495
      prio 4 f1
496
  | ENFORCES (s, f1) ->
497
      Buffer.add_string sb "~<<";
498
      Buffer.add_string sb (
499
          match s with
500
          | [] -> " "
501
          | _ ->(Str.concat "," (L.map string_of_int s))
502
      );
503
      Buffer.add_string sb ">>X ~ ";
504
      prio 4 f1
505
  | EX _
506
  | AX _
507
  | MIN _
508
  | MAX _
509
  | MORETHAN _
510
  | MAXEXCEPT _
511
  | AT _
512 c49eea11 Thorsten Wißmann
  | CONST _
513
  | CONSTN _
514 01b1ab69 Thorsten Wißmann
  | CHC _
515 86b07be8 Thorsten Wißmann
  | ATLEASTPROB _
516 9bae2c4f Thorsten Wißmann
  | LESSPROBFAIL _
517 19f5dad0 Dirk Pattinson
  | ID _
518
  | NORM _
519
  | NORMN _
520 8cac0897 Christoph Egger
  | FUS _
521
  | MU _
522
  | NU _
523
  | VAR _
524
  | AF _
525
  | EF _
526
  | AG _
527
  | EG _
528
  | AU _
529
  | EU _ -> raise (CoAlgException ("export to tatl: Not connectives of CL"))
530 01b1ab69 Thorsten Wißmann
531
let exportTatlFormula f =
532
  let sb = Buffer.create 128 in
533
  exportTatlFormula_buffer sb f;
534
  Buffer.contents sb
535
536 4fd28192 Thorsten Wißmann
(** Appends a string representation of a sorted formula to a string buffer.
537
    Parentheses are ommited where possible
538
    where the preference rules are defined as usual.
539
    @param sb A string buffer.
540
    @param (s, f) A sorted formula.
541
 *)
542
let rec exportSortedFormula_buffer sb (s, f) =
543
  Buffer.add_string sb (string_of_int s);
544
  Buffer.add_string sb ": ";
545
  exportFormula_buffer sb f
546
547
(** Converts a sorted formula into a string representation.
548
    Parentheses are ommited where possible
549
    where the preference rules are defined as usual.
550
    @param f A sorted formula.
551
    @return A string representing f.
552
 *)
553
let exportSortedFormula f =
554
  let sb = Buffer.create 128 in
555
  exportSortedFormula_buffer sb f;
556
  Buffer.contents sb
557
558
(** Converts a (sorted) formula query into a string representation.
559
    @param tbox A list of sorted formulae representing a TBox.
560
    @param f A sorted formula.
561
    @return A string representing tbox |- f.
562
 *)
563
let exportQuery tbox f =
564
  let sb = Buffer.create 1000 in
565
  let rec expFl = function
566
    | [] -> ()
567
    | h::tl ->
568
        exportSortedFormula_buffer sb h;
569
        if tl <> [] then Buffer.add_string sb "; " else ();
570
        expFl tl
571
  in
572
  expFl tbox;
573
  Buffer.add_string sb "  |-  ";
574
  exportSortedFormula_buffer sb f;
575
  Buffer.contents sb
576
577 b59059c4 Thorsten Wißmann
(** Converts a (sorted) formula query into a string representation. Such that
578
    coalg can read it again using importQuery
579
    @param tbox A list of sorted formulae representing a TBox.
580
    @param f A sorted formula.
581
    @return A string representing tbox |- f.
582
 *)
583
let exportQueryParsable tbox (_,f) =
584
  let sb = Buffer.create 1000 in
585
  let rec expFl = function
586
    | [] -> ()
587
    | (_,h)::tl ->
588
        exportFormula_buffer sb h;
589
        if tl <> [] then Buffer.add_string sb "; " else ();
590
        expFl tl
591
  in
592
  expFl tbox;
593
  Buffer.add_string sb "  |-  ";
594
  exportFormula_buffer sb f;
595
  Buffer.contents sb
596
597 4fd28192 Thorsten Wißmann
598 19f5dad0 Dirk Pattinson
(* NB: True and False are the propositional constants. Lower case
599
   true/false are regardes as atomic propositions and we emit a warning
600
*)
601 c5c25acf Christoph Egger
let lexer = A.make_lexer
602 19f5dad0 Dirk Pattinson
    [":";";";"|-";"(";")";"=>";"<=>";"|";"&";"~";"@";"True";"False";"true";"false";"<";">";"[";"]";"{<=";"{>=";"}";"+";"[pi1]";"[pi2]"
603 b2f18312 Christoph Egger
     ;"[{";"}]";"<{";"}>";",";"/";"{<";"=";"=o";"O"
604
     ;"μ";"ν";"."
605 c5c25acf Christoph Egger
     ;"AX";"EX";"AF";"EF";"AG";"EG";"A";"E";"U"
606
    ]
607 4fd28192 Thorsten Wißmann
608
let mk_exn s = CoAlgException s
609
610 63710593 Christoph Egger
(** Process from inside out. cons all variables seen, remove them when
611
    binding fixpoint is found. Fixpoint type may only change if last
612
    (inner) fixpoint didn't include any free variables.
613
 *)
614
let rec verifyMuAltFree formula =
615
  let proc = verifyMuAltFree in
616
  match formula with
617
  | TRUE | FALSE | AP _ -> ("none", [])
618
  | CONST _
619
  | CONSTN _ -> ("none", [])
620
  | AT (_,a) | NOT a
621
  | EX (_,a) | AX (_,a) -> proc a
622
  | OR (a,b) | AND (a,b)
623
  | EQU (a,b) | IMP (a,b) ->
624 c5c25acf Christoph Egger
     let (atype, afree) = proc a
625
     and (btype, bfree) = proc b in
626
     if (compare atype "μ" == 0 && compare btype "ν" == 0) ||
627
          (compare atype "ν" == 0 && compare btype "μ" == 0) then
628
       raise (CoAlgException ("formula not alternation-free"));
629
     if compare atype "none" == 0 then
630
       (btype, List.flatten [afree; bfree])
631
     else
632
       (atype, List.flatten [afree; bfree])
633 63710593 Christoph Egger
  | ENFORCES (_,a) | ALLOWS   (_,a)
634
  | MIN (_,_,a)    | MAX (_,_,a)
635
  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
636
  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
637
  | ID(a) -> proc a
638
  | NORM(a, b) | NORMN(a, b)
639
  | CHC (a,b)  ->
640 c5c25acf Christoph Egger
     let (atype, afree) = proc a
641
     and (btype, bfree) = proc b in
642
     if (compare atype "μ" == 0 && compare btype "ν" == 0) ||
643
          (compare atype "ν" == 0 && compare btype "μ" == 0) then
644
       raise (CoAlgException ("formula not alternation-free"));
645
     if compare atype "none" == 0 then
646
       (btype, List.flatten [afree; bfree])
647
     else
648
       (atype, List.flatten [afree; bfree])
649 63710593 Christoph Egger
  | FUS (_,a) -> proc a
650
  | MU (s, f) ->
651 c5c25acf Christoph Egger
     let (fptype, free) = proc f in
652
     (if (compare fptype "ν" == 0) then
653
        raise (CoAlgException ("formula not alternation-free")));
654
     let predicate x = compare x s != 0 in
655 63710593 Christoph Egger
     let newfree = List.filter predicate free in
656 c5c25acf Christoph Egger
     if newfree = [] then
657
       ("none", [])
658
     else
659
       ("μ", newfree)
660 63710593 Christoph Egger
  | NU (s, f) ->
661 c5c25acf Christoph Egger
     let (fptype, free) = proc f in
662
     (if (compare fptype "μ" == 0) then
663
        raise (CoAlgException ("formula not alternation-free")));
664
     let predicate x = compare x s != 0 in
665 63710593 Christoph Egger
     let newfree = List.filter predicate free in
666 c5c25acf Christoph Egger
     if newfree = [] then
667
       ("none", [])
668
     else
669
       ("ν", newfree)
670 63710593 Christoph Egger
  | VAR s -> ("none", [s])
671 939f5bab Christoph Egger
  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ ->
672 c5c25acf Christoph Egger
     raise (CoAlgException ("verifyMuAltFree: CTL should have been removed at this point"))
673 939f5bab Christoph Egger
674 63710593 Christoph Egger
675
(** Process from outside in. For every variable bound keep the tuple
676
    (name, negations). For every negation crossed map a +1 over snd on
677
    that list. For every variable met check that the matching
678
    negations is even.
679
 *)
680
let rec verifyMuMonotone negations formula =
681
  let proc = verifyMuMonotone negations in
682
  match formula with
683
  | TRUE | FALSE | AP _ -> ()
684
  | CONST _
685
  | CONSTN _ -> ()
686
  | AT (_,a)
687
  | EX (_,a) | AX (_,a) -> proc a
688
  | OR (a,b) | AND (a,b)
689
  | EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
690
  | ENFORCES (_,a) | ALLOWS   (_,a)
691
  | MIN (_,_,a)    | MAX (_,_,a)
692
  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
693
  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
694
  | ID(a) -> proc a
695
  | NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
696
  | CHC (a,b)  -> (proc a ; proc b)
697
  | FUS (_,a) -> proc a
698
  | MU (s, f)
699
  | NU (s, f) ->
700 c5c25acf Christoph Egger
     let newNeg = (s, 0) :: negations in
701
     verifyMuMonotone newNeg f
702 63710593 Christoph Egger
  | VAR s ->
703 c5c25acf Christoph Egger
     let finder (x, _) = compare x s == 0 in
704
     let (_, neg) = List.find finder negations in
705
     if ((neg land 1) != 0) then raise (CoAlgException ("formula not monotone"))
706 63710593 Christoph Egger
  | NOT a ->
707 c5c25acf Christoph Egger
     let increment (s, n) = (s, n+1) in
708
     let newNeg = List.map increment negations in
709
     verifyMuMonotone newNeg a
710 939f5bab Christoph Egger
  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ ->
711 c5c25acf Christoph Egger
     raise (CoAlgException ("verifyMuMonotone: CTL should have been removed at this point"))
712 63710593 Christoph Egger
713 26cfb2dc Christoph Egger
let rec verifyMuGuarded unguarded formula =
714
  let proc = verifyMuGuarded unguarded in
715
  match formula with
716
  | TRUE | FALSE | AP _ -> ()
717
  | CONST _
718
  | CONSTN _ -> ()
719
  | AT (_,a) | NOT a -> proc a
720
  | EX (_,a) | AX (_,a) -> verifyMuGuarded [] a
721
  | OR (a,b) | AND (a,b)
722
  | EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
723
  | ENFORCES (_,a) | ALLOWS   (_,a)
724
  | MIN (_,_,a)    | MAX (_,_,a)
725
  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
726
  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
727
  | ID(a) -> proc a
728
  | NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
729
  | CHC (a,b)  -> (proc a ; proc b)
730
  | FUS (_,a) -> proc a
731
  | MU (s, f)
732
  | NU (s, f) ->
733 c5c25acf Christoph Egger
     let newUnguard = s :: unguarded in
734
     verifyMuGuarded newUnguard f
735 26cfb2dc Christoph Egger
  | VAR s ->
736 c5c25acf Christoph Egger
     let finder x = compare x s == 0 in
737
     if List.exists finder unguarded then
738
       raise (CoAlgException ("formula not guarded"))
739 939f5bab Christoph Egger
  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ ->
740 c5c25acf Christoph Egger
     raise (CoAlgException ("verifyMuGuarded: CTL should have been removed at this point"))
741 63710593 Christoph Egger
742
let verifyFormula formula =
743
  verifyMuAltFree formula;
744
  verifyMuMonotone [] formula;
745 26cfb2dc Christoph Egger
  verifyMuGuarded [] formula
746 63710593 Christoph Egger
747 4fd28192 Thorsten Wißmann
(** These functions parse a token stream to obtain a formula.
748
    It is a standard recursive descent procedure.
749
    @param ts A token stream.
750
    @return The resulting (sub-)formula.
751
    @raise CoAlgException if ts does not represent a formula.
752
 *)
753 0b908205 Christoph Egger
let rec parse_formula (symtab: 'a list) ts =
754 1484d8cb Christoph Egger
  let formula = (parse_imp symtab ts) in
755
  let f1 = convertToMu formula in
756 4fd28192 Thorsten Wißmann
  match Stream.peek ts with
757
  | None -> f1
758
  | Some (A.Kwd "<=>") ->
759
      Stream.junk ts;
760 0b908205 Christoph Egger
      let f2 = parse_formula symtab ts in
761 4fd28192 Thorsten Wißmann
      EQU (f1, f2)
762
  | _ -> f1
763
764
(** These functions parse a token stream to obtain a formula.
765
    It is a standard recursive descent procedure.
766
    @param ts A token stream.
767
    @return The resulting (sub-)formula.
768
    @raise CoAlgException if ts does not represent a formula.
769
 *)
770 0b908205 Christoph Egger
and parse_imp symtab ts=
771
  let f1 = parse_or symtab ts in
772 4fd28192 Thorsten Wißmann
  match Stream.peek ts with
773
  | None -> f1
774
  | Some (A.Kwd "=>") ->
775
      Stream.junk ts;
776 0b908205 Christoph Egger
      let f2 = parse_imp symtab ts in
777 4fd28192 Thorsten Wißmann
      IMP (f1, f2)
778
  | _ -> f1
779
780
(** These functions parse a token stream to obtain a formula.
781
    It is a standard recursive descent procedure.
782
    @param ts A token stream.
783
    @return The resulting (sub-)formula.
784
    @raise CoAlgException if ts does not represent a formula.
785
 *)
786 0b908205 Christoph Egger
and parse_or symtab ts =
787
  let f1 = parse_and symtab ts in
788 4fd28192 Thorsten Wißmann
  match Stream.peek ts with
789
  | None -> f1
790
  | Some (A.Kwd "|") ->
791
      Stream.junk ts;
792 0b908205 Christoph Egger
      let f2 = parse_or symtab ts in
793 4fd28192 Thorsten Wißmann
      OR (f1, f2)
794
  | _ -> f1
795
796
(** These functions parse a token stream to obtain a formula.
797
    It is a standard recursive descent procedure.
798
    @param ts A token stream.
799
    @return The resulting (sub-)formula.
800
    @raise CoAlgException if ts does not represent a formula.
801
 *)
802 0b908205 Christoph Egger
and parse_and symtab ts =
803
  let f1 = parse_cimp symtab ts in
804 4fd28192 Thorsten Wißmann
  match Stream.peek ts with
805
  | None -> f1
806
  | Some (A.Kwd "&") ->
807
      Stream.junk ts;
808 0b908205 Christoph Egger
      let f2 = parse_and symtab ts in
809 4fd28192 Thorsten Wißmann
      AND (f1, f2)
810
  | _ -> f1
811
812
(** These functions parse a token stream to obtain a formula.
813
    It is a standard recursive descent procedure.
814
    @param ts A token stream.
815
    @return The resulting (sub-)formula.
816
    @raise CoAlgException if ts does not represent a formula.
817
 *)
818 0b908205 Christoph Egger
and parse_cimp symtab ts =
819
  let f1 = parse_rest symtab ts in
820 19f5dad0 Dirk Pattinson
  match Stream.peek ts with
821
  | None -> f1
822
  | Some (A.Kwd "=o") ->
823
      Stream.junk ts;
824 0b908205 Christoph Egger
      let f2 = parse_cimp symtab ts in
825 19f5dad0 Dirk Pattinson
      NORM (f1, f2)
826
  | _ -> f1
827
828
(** These functions parse a token stream to obtain a formula.
829
    It is a standard recursive descent procedure.
830
    @param ts A token stream.
831
    @return The resulting (sub-)formula.
832
    @raise CoAlgException if ts does not represent a formula.
833
 *)
834 0b908205 Christoph Egger
and parse_rest symtab ts =
835 4fd28192 Thorsten Wißmann
  let boxinternals noNo es =
836
    let n =
837
      if noNo then 0
838
      else
839
        match Stream.next ts with
840
        | A.Int n when n >= 0 -> n
841
        | t -> A.printError mk_exn ~t ~ts "<non-negative number> expected: "
842
    in
843 e5422169 Thorsten Wißmann
    let (s,denominator) =
844 4fd28192 Thorsten Wißmann
      match Stream.peek ts with
845 e5422169 Thorsten Wißmann
      | Some (A.Ident s1) -> Stream.junk ts; (s1,0)
846
      | Some (A.Kwd c) when c = es -> ("", 0)
847
      | Some (A.Kwd "/") -> begin
848
            Stream.junk ts;
849
            match Stream.next ts with
850
            | A.Int denom when denom > 0 -> ("", denom)
851
            | t -> A.printError mk_exn ~t ~ts "<positive number> (the denominator) expected: "
852
        end
853 4fd28192 Thorsten Wißmann
      | _ -> A.printError mk_exn ~ts ("role name or \"" ^ es ^ "\" expected: ")
854
    in
855 eda515b6 Thorsten Wißmann
    if (denominator < n) then begin
856
       let explanation =
857
        ("nominator="^(string_of_int n)^" but denominator="^(string_of_int denominator))
858
       in
859
       A.printError mk_exn ~ts ("Nominator must not be larger than the denominator "
860
                               ^"("^explanation^") at: "
861
                               )
862 e5422169 Thorsten Wißmann
    end;
863 4fd28192 Thorsten Wißmann
    let _ =
864
      match Stream.next ts with
865
      | A.Kwd c when c = es -> ()
866
      | t -> A.printError mk_exn ~t ~ts ("\"" ^ es ^ "\" expected: ")
867
    in
868 e5422169 Thorsten Wißmann
    (n, denominator, s)
869 4fd28192 Thorsten Wißmann
  in
870 f1fa9ad5 Thorsten Wißmann
  let rec agentlist es =
871 e2dc68f7 Thorsten Wißmann
    let allAgents = CoolUtils.cl_get_agents () in
872 f1fa9ad5 Thorsten Wißmann
    match Stream.next ts with
873 e2dc68f7 Thorsten Wißmann
    | A.Int n -> if CoolUtils.TArray.elem n allAgents
874
                 then n::(agentlist es)
875
                 else A.printError mk_exn ~ts ("agent name \"" ^ (string_of_int n) ^ "\" unknonwn, see --agents: ")
876 f1fa9ad5 Thorsten Wißmann
    | A.Kwd c when c = es -> []
877
    | _ -> A.printError mk_exn ~ts ("agent name or " ^ es ^ "\" expected: ")
878
  in
879 4fd28192 Thorsten Wißmann
  match Stream.next ts with
880 19f5dad0 Dirk Pattinson
  | A.Kwd "true" ->
881
    print_endline "*** Warning: \"true\" used as propositional variable.";
882
    AP "true"
883
  | A.Kwd "false" ->
884
    print_endline "*** Warning: \"false\" used as propositional variable.";
885
    AP "false"
886 4fd28192 Thorsten Wißmann
  | A.Kwd "True" -> TRUE
887
  | A.Kwd "False" -> FALSE
888 c3e13ca6 Christoph Egger
  | A.Ident s ->
889 c5c25acf Christoph Egger
      (try
890
          let finder (x, _) = compare x s == 0 in
891
          let (_, symbol) = List.find finder symtab in
892
          VAR symbol
893
        with Not_found -> AP s)
894 4fd28192 Thorsten Wißmann
  | A.Kwd "~" ->
895 0b908205 Christoph Egger
      let f = parse_rest symtab ts in
896 4fd28192 Thorsten Wißmann
      NOT f
897
  | A.Kwd "@" ->
898
      let s =
899
        match Stream.next ts with
900
        | A.Ident s when isNominal s -> s
901
        | t -> A.printError mk_exn ~t ~ts ("nominal expected: ")
902
      in
903 0b908205 Christoph Egger
      let f = parse_rest symtab ts in
904 4fd28192 Thorsten Wißmann
      AT (s, f)
905 c5c25acf Christoph Egger
  | A.Kwd "<" ->
906 e5422169 Thorsten Wißmann
      let (_, _, s) = boxinternals true ">" in
907 0b908205 Christoph Egger
      let f1 = parse_rest symtab ts in
908 c5c25acf Christoph Egger
      EX (s, f1)
909
  | A.Kwd "[" ->
910 e5422169 Thorsten Wißmann
      let (_, _, s) = boxinternals true "]" in
911 0b908205 Christoph Egger
      let f1 = parse_rest symtab ts in
912 4fd28192 Thorsten Wißmann
      AX (s, f1)
913 c5c25acf Christoph Egger
  | A.Kwd "[{" ->
914 7aa620ce Thorsten Wißmann
      let ls = agentlist "}]" in
915 0b908205 Christoph Egger
      let f1 = parse_rest symtab ts in
916 7aa620ce Thorsten Wißmann
      ENFORCES (ls, f1)
917 c5c25acf Christoph Egger
  | A.Kwd "<{" ->
918 7aa620ce Thorsten Wißmann
      let ls = agentlist "}>" in
919 0b908205 Christoph Egger
      let f1 = parse_rest symtab ts in
920 7aa620ce Thorsten Wißmann
      ALLOWS (ls, f1)
921 c5c25acf Christoph Egger
  | A.Kwd "{>=" ->
922 e5422169 Thorsten Wißmann
      let (n, denom, s) = boxinternals false "}" in
923 0b908205 Christoph Egger
      let f1 = parse_rest symtab ts in
924 e5422169 Thorsten Wißmann
      if (denom <> 0)
925
      then ATLEASTPROB (rational_of_int n denom, f1)
926
      else MIN (n, s, f1)
927 c5c25acf Christoph Egger
  | A.Kwd "{<=" ->
928 e5422169 Thorsten Wißmann
      let (n, denom, s) = boxinternals false "}" in
929 0b908205 Christoph Egger
      let f1 = parse_rest symtab ts in
930 e5422169 Thorsten Wißmann
      if (denom <> 0)
931 c855ba91 Thorsten Wißmann
      then A.printError mk_exn ~ts "Can not express {<= probability}"
932 e5422169 Thorsten Wißmann
      else MAX (n, s, f1)
933 c5c25acf Christoph Egger
  | A.Kwd "{<" ->
934 c855ba91 Thorsten Wißmann
      let (n, denom, s) = boxinternals false "}" in
935 0b908205 Christoph Egger
      let f1 = parse_rest symtab ts in
936 c855ba91 Thorsten Wißmann
      if (denom <> 0)
937 9bae2c4f Thorsten Wißmann
      then LESSPROBFAIL (rational_of_int n denom, NOT f1)
938 c855ba91 Thorsten Wißmann
      else A.printError mk_exn ~ts "The \"Less than\" < is not implemented yet"
939 c49eea11 Thorsten Wißmann
  | A.Kwd "=" -> begin
940
          match Stream.next ts with
941
          (* | A.Int s *)
942
          | A.Kwd s
943
          | A.Ident s -> CONST s
944
          | _ -> A.printError mk_exn ~ts "constant = expects an identifier afterwards"
945
    end
946 4fd28192 Thorsten Wißmann
  | A.Kwd "(" -> begin
947 0b908205 Christoph Egger
      let f = parse_formula symtab ts in
948 4fd28192 Thorsten Wißmann
      match Stream.next ts with
949
      | A.Kwd ")" -> f
950
      | A.Kwd "+" -> begin
951 0b908205 Christoph Egger
          let f2 = parse_formula symtab ts in
952 4fd28192 Thorsten Wißmann
          match Stream.next ts with
953
          | A.Kwd ")" -> CHC (f, f2)
954
          | t -> A.printError mk_exn ~t ~ts "\")\" expected: "
955
        end
956
      | t -> A.printError mk_exn ~t ~ts "\")\" or \"+\" expected: "
957
    end
958 19f5dad0 Dirk Pattinson
  | A.Kwd "O" ->
959 0b908205 Christoph Egger
    let f = parse_rest symtab ts in
960 19f5dad0 Dirk Pattinson
      ID f
961 4fd28192 Thorsten Wißmann
  | A.Kwd "[pi1]" ->
962 0b908205 Christoph Egger
      let f = parse_rest symtab ts in
963 4fd28192 Thorsten Wißmann
      FUS (true, f)
964
  | A.Kwd "[pi2]" ->
965 0b908205 Christoph Egger
      let f = parse_rest symtab ts in
966 4fd28192 Thorsten Wißmann
      FUS (false, f)
967 8334c748 Christoph Egger
  | A.Kwd "μ" ->
968
      let (_, _, s) = boxinternals true "." in
969 c5c25acf Christoph Egger
      let symbol = Stream.next gensym in
970
      let newtab = (s, symbol) :: symtab in
971 80aa0b2f Christoph Egger
      let f1 = parse_rest newtab ts in
972
      MU (symbol, f1)
973 8334c748 Christoph Egger
  | A.Kwd "ν" ->
974
      let (_, _, s) = boxinternals true "." in
975 c5c25acf Christoph Egger
      let symbol = Stream.next gensym in
976
      let newtab = (s, symbol) :: symtab in
977 80aa0b2f Christoph Egger
      let f1 = parse_rest newtab ts in
978
      NU (symbol, f1)
979 0aa34675 Christoph Egger
  | A.Kwd "AF" ->
980 c5c25acf Christoph Egger
      let f = parse_rest symtab ts in
981
      AF f
982 0aa34675 Christoph Egger
  | A.Kwd "EF" ->
983 c5c25acf Christoph Egger
      let f = parse_rest symtab ts in
984
      EF f
985 0aa34675 Christoph Egger
  | A.Kwd "AG" ->
986 c5c25acf Christoph Egger
      let f = parse_rest symtab ts in
987
      AG f
988 0aa34675 Christoph Egger
  | A.Kwd "EG" ->
989 c5c25acf Christoph Egger
      let f = parse_rest symtab ts in
990
      EG f
991 0aa34675 Christoph Egger
  | A.Kwd "A" ->
992 c5c25acf Christoph Egger
     assert (Stream.next ts = A.Kwd "(");
993
     let f1 = parse_formula symtab ts in
994
     assert (Stream.next ts = A.Kwd "U");
995
     let f2 = parse_formula symtab ts in
996
     assert (Stream.next ts = A.Kwd ")");
997
     AU (f1, f2)
998 0aa34675 Christoph Egger
  | A.Kwd "E" ->
999 c5c25acf Christoph Egger
     assert (Stream.next ts = A.Kwd "(");
1000
     let f1 = parse_formula symtab ts in
1001
     assert (Stream.next ts = A.Kwd "U");
1002
     let f2 = parse_formula symtab ts in
1003
     assert (Stream.next ts = A.Kwd ")");
1004
     EU (f1, f2)
1005 0aa34675 Christoph Egger
  | A.Kwd "AX" ->
1006 c5c25acf Christoph Egger
     let f1 = parse_rest symtab ts in
1007
     AX ("", f1)
1008 0aa34675 Christoph Egger
  | A.Kwd "EX" ->
1009 c5c25acf Christoph Egger
     let f1 = parse_rest symtab ts in
1010
     EX ("", f1)
1011
  | t -> A.printError mk_exn ~t ~ts
1012 19f5dad0 Dirk Pattinson
      "\"<\", \"[\", \"{>=\", \"{<=\", \"@\", \"~\", \"(\",
1013
      \"True\", \"False\", \"=\", \"=o\", \"O\" or <ident> expected: "
1014 8334c748 Christoph Egger
1015 4fd28192 Thorsten Wißmann
(** Parses a sorted formula.
1016
    @param ts A token stream.
1017
    @return A sorted formula.
1018
    @raise CoAlgException If ts does not represent a sorted formula.
1019
 *)
1020
let parse_sortedFormula ts =
1021 c5c25acf Christoph Egger
  let nr =
1022 4fd28192 Thorsten Wißmann
    match Stream.peek ts with
1023
    | Some (A.Int n) ->
1024
        if n >= 0 then begin
1025
          Stream.junk ts;
1026
          let () =
1027
            match Stream.next ts with
1028
            | A.Kwd ":" -> ()
1029
            | t -> A.printError mk_exn ~t ~ts ("\":\" expected: ")
1030
          in
1031
          n
1032
        end else
1033
          A.printError mk_exn ~ts ("<non-negative number> expected: ")
1034 c5c25acf Christoph Egger
    | _ -> 0
1035 4fd28192 Thorsten Wißmann
  in
1036 0b908205 Christoph Egger
  let f = parse_formula [] ts in
1037 4fd28192 Thorsten Wißmann
  (nr, f)
1038
1039
(** Parses a list of sorted formulae separated by ";".
1040
    @param ts A token stream.
1041
    @param acc The list of sorted formulae parsed so far.
1042
    @return The resulting list of sorted formula.
1043
    @raise CoAlgException if ts does not represent a list of sorted formulae.
1044
 *)
1045
let rec parse_sortedFormulaList ts acc =
1046
  let f1 = parse_sortedFormula ts in
1047
  match Stream.peek ts with
1048
  | Some (A.Kwd ";") ->
1049
      Stream.junk ts;
1050
      parse_sortedFormulaList ts (f1::acc)
1051
  | _ -> List.rev (f1::acc)
1052
1053
(** A common wrapper for import functions.
1054
    @param fkt An import function.
1055
    @param s A string.
1056
    @return The object imported from s using fkt.
1057
    @raise CoAlgException If ts is not empty.
1058
 *)
1059
let importWrapper fkt s =
1060
  let ts = lexer s in
1061
  try
1062
    let res = fkt ts in
1063
    let _ =
1064
      match Stream.peek ts with
1065
      | None -> ()
1066
      | Some _ -> A.printError mk_exn ~ts "EOS expected: "
1067
    in
1068
    res
1069
  with Stream.Failure -> A.printError mk_exn ~ts "unexpected EOS"
1070
1071
(** Parses a string to obtain a formula.
1072
    @param s A string representing a formula.
1073
    @return The resulting formula.
1074
    @raise CoAlgException if s does not represent a formula.
1075
 *)
1076 0b908205 Christoph Egger
let importFormula s = importWrapper (parse_formula []) s
1077 4fd28192 Thorsten Wißmann
1078
(** Parses a string to obtain a sorted formula.
1079
    @param s A string representing a sorted formula.
1080
    @return The sorted formula.
1081
    @raise CoAlgException If s does not represent a sorted formula.
1082
 *)
1083
let importSortedFormula s = importWrapper parse_sortedFormula s
1084
1085
(** Parses a string to obtain a (sorted) formula query.
1086
    @param s A string representing a formula query.
1087
    @return A pair (tbox, f) where
1088
    tbox is a list of sorted formulae representing the TBox; and
1089
    f is a sorted formula.
1090
    @raise CoAlgException if s does not represent a formula query.
1091
 *)
1092
let importQuery s =
1093
  let fkt ts =
1094
    match Stream.peek ts with
1095
    | Some (A.Kwd "|-") ->
1096
        Stream.junk ts;
1097
        let f = parse_sortedFormula ts in
1098
        ([], f)
1099
    | _ ->
1100
        let fl = parse_sortedFormulaList ts [] in
1101
        match Stream.peek ts with
1102
        | Some (A.Kwd "|-") ->
1103
            Stream.junk ts;
1104
            let f = parse_sortedFormula ts in
1105
            (fl, f)
1106 c5c25acf Christoph Egger
        | _ ->
1107 4fd28192 Thorsten Wißmann
            if List.length fl = 1 then ([], List.hd fl)
1108
            else A.printError mk_exn ~ts "\"|-\" expected: "
1109
  in
1110
  importWrapper fkt s
1111
1112
1113
(** Converts the negation of a formula to negation normal form
1114
    by "pushing in" the negations "~".
1115
    The symbols "<=>" and "=>" are substituted by their usual definitions.
1116
    @param f A formula.
1117
    @return A formula in negation normal form and not containing "<=>" or "=>"
1118
    that is equivalent to ~f.
1119
 *)
1120
let rec nnfNeg f =
1121
  match f with
1122
  | TRUE -> FALSE
1123
  | FALSE -> TRUE
1124
  | AP _ -> NOT f
1125 ff4dc786 Christoph Egger
  | VAR _ -> f
1126 4fd28192 Thorsten Wißmann
  | NOT f1 -> nnf f1
1127
  | AT (s, f1) -> AT (s, nnfNeg f1)
1128
  | OR (f1, f2) -> AND (nnfNeg f1, nnfNeg f2)
1129
  | AND (f1, f2) -> OR (nnfNeg f1, nnfNeg f2)
1130
  | EQU (f1, f2) -> OR (AND (nnf f1, nnfNeg f2), AND (nnf f2, nnfNeg f1))
1131
  | IMP (f1, f2) -> AND (nnf f1, nnfNeg f2)
1132
  | EX (s, f1) -> AX (s, nnfNeg f1)
1133
  | AX (s, f1) -> EX (s, nnfNeg f1)
1134 f1fa9ad5 Thorsten Wißmann
  | ENFORCES (s, f1) -> ALLOWS (s, nnfNeg f1)
1135
  | ALLOWS (s, f1) -> ENFORCES (s, nnfNeg f1)
1136 af276a36 Thorsten Wißmann
  | MIN (n, s, f1) -> if n = 0 then FALSE else MAXEXCEPT (n-1, s, nnfNeg f1)
1137
  | MAX (n, s, f1) -> MORETHAN (n, s, nnf f1)
1138
  | MORETHAN (n, s, f1) -> MAXEXCEPT (n, s, nnfNeg f1)
1139
  | MAXEXCEPT (n, s, f1) -> MORETHAN (n, s, nnfNeg f1)
1140 9bae2c4f Thorsten Wißmann
  | ATLEASTPROB (p, f1) -> LESSPROBFAIL (p, nnfNeg f1)
1141
  | LESSPROBFAIL (p, f1) -> ATLEASTPROB (p, nnfNeg f1)
1142 c49eea11 Thorsten Wißmann
  | CONST s -> CONSTN s
1143
  | CONSTN s -> CONST s
1144 19f5dad0 Dirk Pattinson
  | ID (f1) -> ID (nnfNeg f1)
1145
  | NORM(f1, f2) -> NORMN(nnfNeg f1, nnfNeg f2)
1146
  | NORMN(f1, f2) -> NORM (nnfNeg f1, nnfNeg f2)
1147 c5c25acf Christoph Egger
  | CHC (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2)
1148 4fd28192 Thorsten Wißmann
  | FUS (first, f1) -> FUS (first, nnfNeg f1)
1149 ff4dc786 Christoph Egger
  | MU (s, f1) -> NU(s, nnfNeg f1)
1150
  | NU (s, f1) -> MU(s, nnfNeg f1)
1151 8cac0897 Christoph Egger
  | AF _
1152
  | EF _
1153
  | AG _
1154
  | EG _
1155
  | AU _
1156
  | EU _ -> raise (CoAlgException ("nnfNeg: CTL should have been removed at this point"))
1157 c5c25acf Christoph Egger
1158 4fd28192 Thorsten Wißmann
(** Converts a formula to negation normal form
1159
    by "pushing in" the negations "~".
1160
    The symbols "<=>" and "=>" are substituted by their usual definitions.
1161
    @param f A formula.
1162
    @return A formula in negation normal form and not containing "<=>" or "=>"
1163
    that is equivalent to f.
1164
 *)
1165
and nnf f =
1166
  match f with
1167
  | TRUE
1168
  | FALSE
1169
  | AP _
1170 c49eea11 Thorsten Wißmann
  | NOT (AP _)
1171
  | CONST _
1172 ff4dc786 Christoph Egger
  | CONSTN _
1173
  | VAR _ -> f
1174 4fd28192 Thorsten Wißmann
  | NOT f1 -> nnfNeg f1
1175
  | AT (s, f1) ->
1176
      let ft1 = nnf f1 in
1177
      if ft1 == f1 then f else AT (s, ft1)
1178
  | OR (f1, f2) ->
1179
      let ft1 = nnf f1 in
1180
      let ft2 = nnf f2 in
1181
      if ft1 == f1 && ft2 == f2 then f else OR (ft1, ft2)
1182
  | AND (f1, f2) ->
1183
      let ft1 = nnf f1 in
1184
      let ft2 = nnf f2 in
1185
      if ft1 == f1 && ft2 == f2 then f else AND (ft1, ft2)
1186
  | EQU (f1, f2) -> AND (OR (nnfNeg f1, nnf f2), OR (nnfNeg f2, nnf f1))
1187
  | IMP (f1, f2) -> OR (nnfNeg f1, nnf f2)
1188 c5c25acf Christoph Egger
  | EX (s, f1) ->
1189 4fd28192 Thorsten Wißmann
      let ft = nnf f1 in
1190
      if ft == f1 then f else EX (s, ft)
1191
  | AX (s, f1) ->
1192
      let ft = nnf f1 in
1193
      if ft == f1 then f else AX (s, ft)
1194 c5c25acf Christoph Egger
  | ENFORCES (s, f1) ->
1195 f1fa9ad5 Thorsten Wißmann
      let ft = nnf f1 in
1196
      if ft == f1 then f else ENFORCES (s, ft)
1197
  | ALLOWS (s, f1) ->
1198
      let ft = nnf f1 in
1199
      if ft == f1 then f else ALLOWS (s, ft)
1200 4fd28192 Thorsten Wißmann
  | MIN (n, s, f1) ->
1201
      if n = 0 then TRUE
1202
      else
1203
        let ft = nnf f1 in
1204 87926e98 Thorsten Wißmann
        MORETHAN (n-1,s,ft)
1205 4fd28192 Thorsten Wißmann
  | MAX (n, s, f1) ->
1206 af276a36 Thorsten Wißmann
      let ft = nnfNeg f1 in
1207
      MAXEXCEPT (n,s, ft)
1208
  | MORETHAN (n,s,f1) ->
1209 4fd28192 Thorsten Wißmann
      let ft = nnf f1 in
1210 af276a36 Thorsten Wißmann
      if ft = f1 then f else MORETHAN (n,s,ft)
1211
  | MAXEXCEPT (n,s,f1) ->
1212
      let ft = nnf f1 in
1213
      if ft = f1 then f else MAXEXCEPT (n,s,ft)
1214 86b07be8 Thorsten Wißmann
  | ATLEASTPROB (p, f1) ->
1215
      let ft = nnf f1 in
1216
      if ft == f1 then f else ATLEASTPROB (p, ft)
1217 9bae2c4f Thorsten Wißmann
  | LESSPROBFAIL (p, f1) ->
1218 86b07be8 Thorsten Wißmann
      let ft = nnf f1 in
1219 9bae2c4f Thorsten Wißmann
      if ft == f1 then f else LESSPROBFAIL (p, ft)
1220 19f5dad0 Dirk Pattinson
  | ID (f1) ->
1221
    let ft = nnf f1 in
1222
    if ft == f1 then f else ID(ft)
1223
  | NORM (f1, f2) ->
1224
      let ft1 = nnf f1 in
1225
      let ft2 = nnf f2 in
1226
      if ft1 == f1 && ft2 == f2 then f else NORM (ft1, ft2)
1227
  | NORMN (f1, f2) ->
1228
      let ft1 = nnf f1 in
1229
      let ft2 = nnf f2 in
1230
      if ft1 == f1 && ft2 == f2 then f else NORMN (ft1, ft2)
1231 4fd28192 Thorsten Wißmann
  | CHC (f1, f2) ->
1232
      let ft1 = nnf f1 in
1233
      let ft2 = nnf f2 in
1234
      if ft1 == f1 && ft2 == f2 then f else CHC (ft1, ft2)
1235
  | FUS (first, f1) ->
1236
      let ft = nnf f1 in
1237
      if ft == f1 then f else FUS (first, ft)
1238 ff4dc786 Christoph Egger
  | MU (s, f1) ->
1239
      let ft = nnf f1 in
1240
      if ft == f1 then f else MU (s, ft)
1241
  | NU (s, f1) ->
1242
      let ft = nnf f1 in
1243
      if ft == f1 then f else NU (s, ft)
1244 8cac0897 Christoph Egger
  | AF _
1245
  | EF _
1246
  | AG _
1247
  | EG _
1248
  | AU _
1249
  | EU _ -> raise (CoAlgException ("nnf: CTL should have been removed at this point"))
1250 4fd28192 Thorsten Wißmann
1251
(** Simplifies a formula.
1252
    @param f A formula which must be in negation normal form.
1253
    @return A formula in negation normal form that is equivalent to f.
1254
    @raise CoAlgException if f is not in negation normal form.
1255
 *)
1256
let rec simplify f =
1257
  match f with
1258
  | TRUE
1259
  | FALSE
1260
  | AP _
1261 fbffb079 Christoph Egger
  | NOT (AP _)
1262
  | VAR _
1263
  | NOT (VAR _) -> f
1264 4fd28192 Thorsten Wißmann
  | AT (s, f1) ->
1265
      let ft = simplify f1 in
1266
      begin
1267
        match ft with
1268
        | FALSE -> FALSE
1269
        | TRUE -> TRUE
1270
        | AT _ -> ft
1271
        | AP s1 when s = s1 -> TRUE
1272
        | NOT (AP s1) when s = s1 -> FALSE
1273
        | _ -> if ft == f1 then f else AT (s, ft)
1274
      end
1275
  | OR (f1, f2) ->
1276
      let ft1 = simplify f1 in
1277
      let ft2 = simplify f2 in
1278
      begin
1279
        match ft1, ft2 with
1280
        | TRUE, _ -> TRUE
1281
        | FALSE, _ -> ft2
1282
        | _, TRUE -> TRUE
1283
        | _, FALSE -> ft1
1284
        | _, _ ->
1285 c5c25acf Christoph Egger
            if (f1 == ft1) && (f2 == ft2) then f
1286 4fd28192 Thorsten Wißmann
            else OR (ft1, ft2)
1287
      end
1288
  | AND (f1, f2) ->
1289
      let ft1 = simplify f1 in
1290
      let ft2 = simplify f2 in
1291
      begin
1292
        match ft1, ft2 with
1293
        | TRUE, _ -> ft2
1294
        | FALSE, _ -> FALSE
1295
        | _, TRUE -> ft1
1296
        | _, FALSE -> FALSE
1297
        | _, _ ->
1298 c5c25acf Christoph Egger
            if (f1 == ft1) && (f2 == ft2) then f
1299 4fd28192 Thorsten Wißmann
            else AND (ft1, ft2)
1300
      end
1301
  | NOT _
1302
  | EQU _
1303
  | IMP _ -> raise (CoAlgException "Formula is not in negation normal form.")
1304
  | EX (s, f1) ->
1305
      let ft = simplify f1 in
1306
      begin
1307
        match ft with
1308
        | FALSE -> FALSE
1309
        | _ -> if ft == f1 then f else EX (s, ft)
1310
      end
1311
  | AX (s, f1) ->
1312
      let ft = simplify f1 in
1313
      begin
1314
        match ft with
1315
        | TRUE -> TRUE
1316
        | _ -> if ft == f1 then f else AX (s, ft)
1317
      end
1318 f1fa9ad5 Thorsten Wißmann
  | ENFORCES (s, f1) ->
1319
      let ft = simplify f1 in
1320
      begin
1321
        match ft with
1322
        (* Simplification rules are checked with dirks Generic.hs
1323
        let enforce ls = M (C ls)
1324
        let allow   ls = Neg . M (C ls) . Neg
1325
        provable $ F <-> enforce [1,2] F
1326
        *)
1327
        | TRUE -> TRUE
1328
        | FALSE -> FALSE
1329
        | _ -> if ft == f1 then f else ENFORCES (s, ft)
1330
      end
1331
  | ALLOWS (s, f1) ->
1332
      let ft = simplify f1 in
1333
      begin
1334
        match ft with
1335
        (* Simplification rules are checked with dirks Generic.hs
1336
        let enforce ls = M (C ls)
1337
        let allow   ls = Neg . M (C ls) . Neg
1338
        provable $ F <-> enforce [1,2] F
1339
        *)
1340
        | TRUE -> TRUE
1341
        | FALSE -> FALSE
1342
        | _ -> if ft == f1 then f else ALLOWS (s, ft)
1343
      end
1344 4fd28192 Thorsten Wißmann
  | MIN (n, s, f1) ->
1345
      if n = 0 then TRUE
1346
      else
1347
        let ft = simplify f1 in
1348
        begin
1349
          match ft with
1350
          | FALSE -> FALSE
1351
          | _ -> if ft == f1 then f else MIN (n, s, ft)
1352
        end
1353 af276a36 Thorsten Wißmann
  | MORETHAN (n,s,f1) ->
1354
      let ft = simplify f1 in
1355
      if ft == f1 then f else MORETHAN (n,s,ft)
1356
  | MAXEXCEPT (n,s,f1) ->
1357
      let ft = simplify f1 in
1358
      if ft == f1 then f else MAXEXCEPT (n,s,ft)
1359 4fd28192 Thorsten Wißmann
  | MAX (n, s, f1) ->
1360
      let ft = simplify f1 in
1361
      begin
1362
        match ft with
1363
        | FALSE -> TRUE
1364
        | _ -> if ft == f1 then f else MAX (n, s, ft)
1365
      end
1366 9bae2c4f Thorsten Wißmann
  | LESSPROBFAIL (p,f1) ->
1367 86b07be8 Thorsten Wißmann
      let ft1 = simplify f1 in
1368 9bae2c4f Thorsten Wißmann
      if (ft1 == f1) then f else LESSPROBFAIL (p,ft1)
1369 86b07be8 Thorsten Wißmann
  | ATLEASTPROB (p,f1) ->
1370
      let ft1 = simplify f1 in
1371
      if (ft1 == f1) then f else ATLEASTPROB (p,ft1)
1372 c49eea11 Thorsten Wißmann
  | CONST _
1373
  | CONSTN _ -> f (* no simplifications possible *)
1374 19f5dad0 Dirk Pattinson
  | ID (f1) ->
1375
    let ft1 = simplify f1 in
1376
    begin
1377
      match ft1 with
1378
        | TRUE -> TRUE
1379
        | FALSE -> FALSE
1380
        | _ -> if (ft1 == f1) then f else ID (ft1)
1381
    end
1382
  (* todo: more simplifications for KLM? *)
1383
  | NORM (f1, f2) ->
1384
      let ft1 = simplify f1 in
1385
      let ft2 = simplify f2 in
1386
      begin
1387
        match ft2 with
1388
          | TRUE -> TRUE
1389
          | _ ->
1390 c5c25acf Christoph Egger
            if (f1 == ft1) && (f2 == ft2) then f
1391 19f5dad0 Dirk Pattinson
            else NORM (ft1, ft2)
1392
      end
1393
  | NORMN (f1, f2) ->
1394
      let ft1 = simplify f1 in
1395
      let ft2 = simplify f2 in
1396
      begin
1397
        match ft2 with
1398
          | FALSE -> FALSE
1399
          | _ ->
1400 c5c25acf Christoph Egger
            if (f1 == ft1) && (f2 == ft2) then f
1401 19f5dad0 Dirk Pattinson
            else NORMN (ft1, ft2)
1402
      end
1403 4fd28192 Thorsten Wißmann
  | CHC (f1, f2) ->
1404
      let ft1 = simplify f1 in
1405
      let ft2 = simplify f2 in
1406
      begin
1407
        match ft1, ft2 with
1408
        | TRUE, TRUE -> TRUE
1409
        | FALSE, FALSE -> FALSE
1410
        | _, _ ->
1411 c5c25acf Christoph Egger
            if (f1 == ft1) && (f2 == ft2) then f
1412 4fd28192 Thorsten Wißmann
            else CHC (ft1, ft2)
1413
      end
1414
  | FUS (first, f1) ->
1415
      let ft = simplify f1 in
1416
      begin
1417
        match ft with
1418
        | FALSE -> FALSE
1419
        | TRUE -> TRUE
1420
        | _ -> if ft == f1 then f else FUS (first, ft)
1421
      end
1422 fbffb079 Christoph Egger
  | MU (s, f1) ->
1423
      let ft = simplify f1 in
1424
      begin
1425
        match ft with
1426
        | TRUE -> TRUE
1427
        | _ -> if ft == f1 then f else MU (s, ft)
1428
      end
1429
  | NU (s, f1) ->
1430
      let ft = simplify f1 in
1431
      begin
1432
        match ft with
1433
        | TRUE -> TRUE
1434
        | _ -> if ft == f1 then f else NU (s, ft)
1435
      end
1436 8cac0897 Christoph Egger
  | AF _
1437
  | EF _
1438
  | AG _
1439
  | EG _
1440
  | AU _
1441
  | EU _ ->
1442 c5c25acf Christoph Egger
     raise (CoAlgException ("nnf: CTL should have been removed at this point"))
1443 4fd28192 Thorsten Wißmann
1444
(** Destructs an atomic proposition.
1445
    @param f An atomic proposition.
1446
    @return The name of the atomic proposition.
1447
    @raise CoAlgException if f is not an atomic proposition.
1448
 *)
1449
let dest_ap f =
1450
  match f with
1451
  | AP s when not (isNominal s) -> s
1452
  | _ -> raise (CoAlgException "Formula is not an atomic proposition.")
1453
1454
(** Destructs a nominal.
1455
    @param f A nominal.
1456
    @return The name of the nominal
1457
    @raise CoAlgException if f is not a nominal.
1458
 *)
1459
let dest_nom f =
1460
  match f with
1461
  | AP s when isNominal s -> s
1462
  | _ -> raise (CoAlgException "Formula is not a nominal.")
1463
1464
(** Destructs a negation.
1465
    @param f A negation.
1466
    @return The immediate subformula of the negation.
1467
    @raise CoAlgException if f is not a negation.
1468
 *)
1469
let dest_not f =
1470
  match f with
1471
  | NOT f1 -> f1
1472
  | _ -> raise (CoAlgException "Formula is not a negation.")
1473
1474
(** Destructs an @-formula.
1475
    @param f An @-formula.
1476
    @return The name of the nominal and the immediate subformula of the @-formula.
1477
    @raise CoAlgException if f is not an @-formula.
1478
 *)
1479
let dest_at f =
1480
  match f with
1481
  | AT (s, f1) -> (s, f1)
1482
  | _ -> raise (CoAlgException "Formula is not an @-formula.")
1483
1484
(** Destructs an or-formula.
1485
    @param f An or-formula.
1486
    @return The two immediate subformulae of the or-formula.
1487
    @raise CoAlgException if f is not an or-formula.
1488
 *)
1489
let dest_or f =
1490
  match f with
1491
  | OR (f1, f2) -> (f1, f2)
1492
  | _ -> raise (CoAlgException "Formula is not an or-formula.")
1493
1494
(** Destructs an and-formula.
1495
    @param f An and-formula.
1496
    @return The two immediate subformulae of the and-formula.
1497
    @raise CoAlgException if f is not an and-formula.
1498
 *)
1499
let dest_and f =
1500
  match f with
1501
  | AND (f1, f2) -> (f1, f2)
1502
  | _ -> raise (CoAlgException "Formula is not an and-formula.")
1503
1504
(** Destructs an equivalence.
1505
    @param f An equivalence.
1506
    @return The two immediate subformulae of the equivalence.
1507
    @raise CoAlgException if f is not an equivalence.
1508
 *)
1509
let dest_equ f =
1510
  match f with
1511
  | EQU (f1, f2) -> (f1, f2)
1512
  | _ -> raise (CoAlgException "Formula is not an equivalence.")
1513
1514
(** Destructs an implication.
1515
    @param f An implication.
1516
    @return The two immediate subformulae of the implication.
1517
    @raise CoAlgException if f is not an implication.
1518
 *)
1519
let dest_imp f =
1520
  match f with
1521
  | IMP (f1, f2) -> (f1, f2)
1522
  | _ -> raise (CoAlgException "Formula is not an implication.")
1523
1524
(** Destructs an EX-formula.
1525
    @param f An EX-formula.
1526
    @return The role name and the immediate subformula of the EX-formula.
1527
    @raise CoAlgException if f is not an EX-formula.
1528
 *)
1529
let dest_ex f =
1530
  match f with
1531
  | EX (s, f1) -> (s, f1)
1532
  | _ -> raise (CoAlgException "Formula is not an EX-formula.")
1533
1534
(** Destructs an AX-formula.
1535
    @param f An AX-formula.
1536
    @return The role name and the immediate subformula of the AX-formula.
1537
    @raise CoAlgException if f is not an AX-formula.
1538
 *)
1539
let dest_ax f =
1540
  match f with
1541
  | AX (s, f1) -> (s, f1)
1542
  | _ -> raise (CoAlgException "Formula is not an AX-formula.")
1543
1544
(** Destructs a MIN-formula.
1545
    @param f A MIN-formula.
1546
    @return The number restriction, role name,
1547
    and the immediate subformula of the MIN-formula.
1548
    @raise CoAlgException if f is not a MIN-formula.
1549
 *)
1550
let dest_min f =
1551
  match f with
1552
  | MIN (n, s, f1) -> (n, s, f1)
1553
  | _ -> raise (CoAlgException "Formula is not a MIN-formula.")
1554
1555
(** Destructs a MAX-formula.
1556
    @param f A MAX-formula.
1557
    @return The number restriction, role name,
1558
    and the immediate subformula of the MAX-formula.
1559
    @raise CoAlgException if f is not a MAX-formula.
1560
 *)
1561
let dest_max f =
1562
  match f with
1563
  | MAX (n, s, f1) -> (n, s, f1)
1564
  | _ -> raise (CoAlgException "Formula is not a MAX-formula.")
1565
1566
(** Destructs a choice formula.
1567
    @param f A choice formula.
1568
    @return The two immediate subformulae of the choice formula.
1569
    @raise CoAlgException if f is not a choice formula.
1570
 *)
1571
let dest_choice f =
1572
  match f with
1573
  | CHC (f1, f2) -> (f1, f2)
1574
  | _ -> raise (CoAlgException "Formula is not a choice formula.")
1575
1576
(** Destructs a fusion formula.
1577
    @param f A fusion formula.
1578
    @return A pair (first, f1) where
1579
    first is true iff f is a first projection; and
1580
    f1 is the immediate subformulae of f.
1581
    @raise CoAlgException if f is not a fusion formula.
1582
 *)
1583
let dest_fusion f =
1584
  match f with
1585
  | FUS (first, f1) -> (first, f1)
1586
  | _ -> raise (CoAlgException "Formula is not a fusion formula.")
1587
1588
1589
(** Tests whether a formula is the constant True.
1590
    @param f A formula.
1591
    @return True iff f is the constant True.
1592
 *)
1593
let is_true f =
1594
  match f with
1595
  | TRUE -> true
1596
  | _ -> false
1597
1598
(** Tests whether a formula is the constant False.
1599
    @param f A formula.
1600
    @return True iff f is the constant False.
1601
 *)
1602
let is_false f =
1603
  match f with
1604
  | FALSE -> true
1605
  | _ -> false
1606
1607
(** Tests whether a formula is an atomic proposition.
1608
    @param f A formula.
1609
    @return True iff f is an atomic proposition.
1610
 *)
1611
let is_ap f =
1612
  match f with
1613
  | AP s when not (isNominal s) -> true
1614
  | _ -> false
1615
1616
(** Tests whether a formula is a nominal.
1617
    @param f A formula.
1618
    @return True iff f is a nominal.
1619
 *)
1620
let is_nom f =
1621
  match f with
1622
  | AP s when isNominal s -> true
1623
  | _ -> false
1624
1625
(** Tests whether a formula is a negation.
1626
    @param f A formula.
1627
    @return True iff f is a negation.
1628
 *)
1629
let is_not f =
1630
  match f with
1631
  | NOT _ -> true
1632
  | _ -> false
1633
1634
(** Tests whether a formula is an @-formula.
1635
    @param f A formula.
1636
    @return True iff f is an @-formula.
1637
 *)
1638
let is_at f =
1639
  match f with
1640
  | AT _ -> true
1641
  | _ -> false
1642
1643
(** Tests whether a formula is an or-formula.
1644
    @param f A formula.
1645
    @return True iff f is an or-formula.
1646
 *)
1647
let is_or f =
1648
  match f with
1649
  | OR _ -> true
1650
  | _ -> false
1651
1652
(** Tests whether a formula is an and-formula.
1653
    @param f A formula.
1654
    @return True iff f is an and-formula.
1655
 *)
1656
let is_and f =
1657
  match f with
1658
  | AND _ -> true
1659
  | _ -> false
1660
1661
(** Tests whether a formula is an equivalence.
1662
    @param f A formula.
1663
    @return True iff f is an equivalence.
1664
 *)
1665
let is_equ f =
1666
  match f with
1667
  | EQU _ -> true
1668
  | _ -> false
1669
1670
(** Tests whether a formula is an implication.
1671
    @param f A formula.
1672
    @return True iff f is an implication.
1673
 *)
1674
let is_imp f =
1675
  match f with
1676
  | IMP _ -> true
1677
  | _ -> false
1678
1679
(** Tests whether a formula is an EX-formula.
1680
    @param f A formula.
1681
    @return True iff f is an EX-formula.
1682
 *)
1683
let is_ex f =
1684
  match f with
1685
  | EX _ -> true
1686
  | _ -> false
1687
1688
(** Tests whether a formula is an AX-formula.
1689
    @param f A formula.
1690
    @return True iff f is an AX-formula.
1691
 *)
1692
let is_ax f =
1693
  match f with
1694
  | AX _ -> true
1695
  | _ -> false
1696
1697
(** Tests whether a formula is a MIN-formula.
1698
    @param f A formula.
1699
    @return True iff f is a MIN-formula.
1700
 *)
1701
let is_min f =
1702
  match f with
1703
  | MIN _ -> true
1704
  | _ -> false
1705
1706
(** Tests whether a formula is a MAX-formula.
1707
    @param f A formula.
1708
    @return True iff f is a MAX-formula.
1709
 *)
1710
let is_max f =
1711
  match f with
1712
  | MAX _ -> true
1713
  | _ -> false
1714
1715
(** Tests whether a formula is a choice formula.
1716
    @param f A formula.
1717
    @return True iff f is a choice formula.
1718
 *)
1719
let is_choice f =
1720
  match f with
1721
  | CHC _ -> true
1722
  | _ -> false
1723
1724
(** Tests whether a formula is a fusion formula.
1725
    @param f A formula.
1726
    @return True iff f is a fusion formula.
1727
 *)
1728
let is_fusion f =
1729
  match f with
1730
  | FUS _ -> true
1731
  | _ -> false
1732
1733 c5c25acf Christoph Egger
1734 4fd28192 Thorsten Wißmann
(** The constant True.
1735
 *)
1736
let const_true = TRUE
1737
1738
(** The constant False.
1739
 *)
1740
let const_false = FALSE
1741 c5c25acf Christoph Egger
1742 4fd28192 Thorsten Wißmann
(** Constructs an atomic proposition.
1743
    @param s The name of the atomic proposition.
1744
    @return The atomic proposition with name s.
1745
    @raise CoAlgException if s is a nominal name.
1746
 *)
1747
let const_ap s =
1748
  if isNominal s then raise (CoAlgException "The name indicates a nominal.")
1749
  else AP s
1750
1751
(** Constructs a nominal.
1752
    @param s The name of the nominal.
1753
    @return A nominal with name s.
1754
    @raise CoAlgException if s is not a nominal name.
1755
 *)
1756
let const_nom s =
1757
  if isNominal s then AP s
1758
  else raise (CoAlgException "The name does not indicate a nominal.")
1759
1760
(** Negates a formula.
1761
    @param f A formula.
1762
    @return The negation of f.
1763
 *)
1764
let const_not f = NOT f
1765 c5c25acf Christoph Egger
1766 4fd28192 Thorsten Wißmann
(** Constructs an @-formula from a name and a formula.
1767
    @param s A nominal name.
1768
    @param f A formula.
1769
    @return The formula AT (s, f).
1770
 *)
1771
let const_at s f = AT (s, f)
1772
1773
(** Constructs an or-formula from two formulae.
1774
    @param f1 The first formula (LHS).
1775
    @param f2 The second formula (LHS).
1776
    @return The formula f1 | f2.
1777
 *)
1778
let const_or f1 f2 = OR (f1, f2)
1779
1780
(** Constructs an and-formula from two formulae.
1781
    @param f1 The first formula (LHS).
1782
    @param f2 The second formula (LHS).
1783
    @return The formula f1 & f2.
1784 c5c25acf Christoph Egger
 *)
1785 4fd28192 Thorsten Wißmann
let const_and f1 f2 = AND (f1, f2)
1786
1787
(** Constructs an equivalence from two formulae.
1788
    @param f1 The first formula (LHS).
1789
    @param f2 The second formula (LHS).
1790
    @return The equivalence f1 <=> f2.
1791
 *)
1792
let const_equ f1 f2 = EQU (f1, f2)
1793
1794
(** Constructs an implication from two formulae.
1795
    @param f1 The first formula (LHS).
1796
    @param f2 The second formula (LHS).
1797
    @return The implication f1 => f2.
1798
 *)
1799
let const_imp f1 f2 = IMP (f1, f2)
1800
1801
(** Constructs an EX-formula from a formula.
1802
    @param s A role name.
1803
    @param f A formula.
1804
    @return The formula EX (s, f).
1805
 *)
1806
let const_ex s f = EX (s, f)
1807
1808
(** Constructs an AX-formula from a formula.
1809
    @param s A role name.
1810
    @param f A formula.
1811
    @return The formula AX (s, f).
1812
 *)
1813
let const_ax s f = AX (s, f)
1814
1815
(** Constructs a MIN-formula from a formula.
1816
    @param n A non-negative integer.
1817
    @param s A role name.
1818
    @param f A formula.
1819
    @return The formula MIN f.
1820
    @raise CoAlgException Iff n is negative.
1821
 *)
1822
let const_min n s f =
1823
  if n < 0 then raise (CoAlgException "Negative cardinality constraint.")
1824
  else MIN (n, s, f)
1825
1826
(** Constructs a MAX-formula from a formula.
1827
    @param n A non-negative integer.
1828
    @param s A role name.
1829
    @param f A formula.
1830
    @return The formula MAX f.
1831
    @raise CoAlgException Iff n is negative.
1832
 *)
1833
let const_max n s f =
1834
  if n < 0 then raise (CoAlgException "Negative cardinality constraint.")
1835
  else MAX (n, s, f)
1836
1837 7993e0bf Thorsten Wißmann
let const_enforces p f =
1838
    ENFORCES (p,f)
1839
1840
let const_allows p f =
1841
    ALLOWS (p,f)
1842
1843 4fd28192 Thorsten Wißmann
(** Constructs a choice formula from two formulae.
1844
    @param f1 The first formula (LHS).
1845
    @param f2 The second formula (LHS).
1846
    @return The formula (f1 + f2).
1847
 *)
1848
let const_choice f1 f2 = CHC (f1, f2)
1849
1850
(** Constructs a fusion formula.
1851
    @param first True iff the result is a first projection.
1852
    @param f1 A formula.
1853
    @return The formula [pi1] f1 or [pi2] f1 (depending on first).
1854
 *)
1855
let const_fusion first f1 = FUS (first, f1)
1856
1857
1858
(** Hash-consed formulae, which are in negation normal form,
1859
    such that structural and physical equality coincide.
1860 87d5082f Christoph Egger
1861
    Also CTL has been replaced by the equivalent μ-Calculus
1862
    constructs
1863 4fd28192 Thorsten Wißmann
 *)
1864
type hcFormula = (hcFormula_node, formula) HC.hash_consed
1865
and hcFormula_node =
1866
  | HCTRUE
1867
  | HCFALSE
1868
  | HCAP of string
1869
  | HCNOT of string
1870
  | HCAT of string * hcFormula
1871
  | HCOR of hcFormula * hcFormula
1872
  | HCAND of hcFormula * hcFormula
1873
  | HCEX of string * hcFormula
1874
  | HCAX of string * hcFormula
1875 f1fa9ad5 Thorsten Wißmann
  | HCENFORCES of int list * hcFormula
1876
  | HCALLOWS of int list * hcFormula
1877 af276a36 Thorsten Wißmann
  | HCMORETHAN of int * string * hcFormula (* GML Diamond *)
1878
  | HCMAXEXCEPT of int * string * hcFormula (* GML Box *)
1879 86b07be8 Thorsten Wißmann
  | HCATLEASTPROB of rational * hcFormula
1880 9bae2c4f Thorsten Wißmann
  | HCLESSPROBFAIL of rational * hcFormula
1881 c49eea11 Thorsten Wißmann
  | HCCONST of string
1882
  | HCCONSTN of string
1883 19f5dad0 Dirk Pattinson
  | HCID of hcFormula
1884
  | HCNORM of hcFormula * hcFormula
1885
  | HCNORMN of hcFormula * hcFormula
1886 4fd28192 Thorsten Wißmann
  | HCCHC of hcFormula * hcFormula
1887
  | HCFUS of bool * hcFormula
1888 87d5082f Christoph Egger
  | HCMU of string * hcFormula
1889
  | HCNU of string * hcFormula
1890
  | HCVAR of string
1891 4fd28192 Thorsten Wißmann
1892
(** Determines whether two formula nodes are structurally equal.
1893
    @param f1 The first formula node.
1894
    @param f2 The second formula node.
1895
    @return True iff f1 and f2 are structurally equal.
1896
 *)
1897
let equal_hcFormula_node f1 f2 =
1898
  match f1, f2 with
1899
  | HCTRUE, HCTRUE -> true
1900
  | HCFALSE, HCFALSE -> true
1901 c49eea11 Thorsten Wißmann
  | HCCONST s1, HCCONST s2
1902
  | HCCONSTN s1, HCCONSTN s2
1903 4fd28192 Thorsten Wißmann
  | HCAP s1, HCAP s2
1904
  | HCNOT s1, HCNOT s2 -> compare s1 s2 = 0
1905
  | HCAT (s1, f1), HCAT (s2, f2) -> compare s1 s2 = 0 && f1 == f2
1906
  | HCOR (f1a, f1b), HCOR (f2a, f2b)
1907
  | HCAND (f1a, f1b), HCAND (f2a, f2b) -> f1a == f2a && f1b == f2b
1908
  | HCEX (s1, f1), HCEX (s2, f2)
1909
  | HCAX (s1, f1), HCAX (s2, f2) -> compare s1 s2 = 0 && f1 == f2
1910 bc6db513 Thorsten Wißmann
  | HCENFORCES (s1, f1), HCENFORCES (s2, f2)
1911
  | HCALLOWS (s1, f1), HCALLOWS (s2, f2) -> compare s1 s2 = 0 && f1 == f2
1912 af276a36 Thorsten Wißmann
  | HCMORETHAN (n1, s1, f1), HCMORETHAN (n2, s2, f2)
1913
  | HCMAXEXCEPT (n1, s1, f1), HCMAXEXCEPT (n2, s2, f2) ->
1914 c5c25acf Christoph Egger
      n1 = n2 && compare s1 s2 = 0 && f1 == f2
1915 86b07be8 Thorsten Wißmann
  | HCATLEASTPROB (p1, f1), HCATLEASTPROB (p2,f2) ->
1916
      p1 = p2 && f1 == f2
1917 9bae2c4f Thorsten Wißmann
  | HCLESSPROBFAIL (p1, f1), HCLESSPROBFAIL (p2,f2) ->
1918 86b07be8 Thorsten Wißmann
      p1 = p2 && f1 == f2
1919 19f5dad0 Dirk Pattinson
  | HCID f1, HCID f2 -> f1 == f2
1920
  | HCNORM (f1a, f1b), HCNORMN (f2a, f2b) -> f1a == f2a && f1b == f2b
1921 4fd28192 Thorsten Wißmann
  | HCCHC (f1a, f1b), HCCHC (f2a, f2b) -> f1a == f2a && f1b == f2b
1922
  | HCFUS (first1, f1), HCFUS (first2, f2) -> first1 = first2 && f1 == f2
1923 a7ae917b Christoph Egger
  | HCMU (name1, f1), HCMU(name2, f2) -> compare name1 name2 = 0 && f1 == f2
1924
  | HCNU (name1, f1), HCNU(name2, f2) -> compare name1 name2 = 0 && f1 == f2
1925
  | HCVAR name1, HCVAR name2 -> compare name1 name2 = 0
1926 4fd28192 Thorsten Wißmann
(* The rest could be shortened to | _ -> false,
1927
   but then the compiler would not warn if the formula type is extended
1928
   and this function is not updated accordingly.*)
1929
  | HCTRUE, _
1930
  | HCFALSE, _
1931
  | HCAP _, _
1932
  | HCNOT _, _
1933
  | HCAT _, _
1934
  | HCOR _, _
1935
  | HCAND _, _
1936
  | HCEX _, _
1937
  | HCAX _, _
1938 f1fa9ad5 Thorsten Wißmann
  | HCENFORCES _, _
1939
  | HCALLOWS   _, _
1940 af276a36 Thorsten Wißmann
  | HCMORETHAN _, _
1941
  | HCMAXEXCEPT _, _
1942 86b07be8 Thorsten Wißmann
  | HCATLEASTPROB _, _
1943 9bae2c4f Thorsten Wißmann
  | HCLESSPROBFAIL _, _
1944 c49eea11 Thorsten Wißmann
  | HCCONST _, _
1945
  | HCCONSTN _, _
1946 19f5dad0 Dirk Pattinson
  | HCID _, _
1947
  | HCNORM _, _
1948
  | HCNORMN _, _
1949 4fd28192 Thorsten Wißmann
  | HCCHC _, _
1950 a7ae917b Christoph Egger
  | HCFUS _, _
1951
  | HCMU _, _
1952
  | HCNU _, _
1953
  | HCVAR _, _ -> false
1954 4fd28192 Thorsten Wißmann
1955
(** Computes the hash value of a formula node.
1956
    @param f A formula node.
1957
    @return The hash value of f.
1958
 *)
1959
let hash_hcFormula_node f =
1960 19f5dad0 Dirk Pattinson
  let base = 23 in (* should be larger than the no of constructors *)
1961 4fd28192 Thorsten Wißmann
  match f with
1962
  | HCTRUE -> 0
1963
  | HCFALSE -> 1
1964
  | HCAP s
1965 508e3c33 Christoph Egger
  | HCNOT s
1966
  | HCVAR s -> base * Hashtbl.hash s + 1
1967 19f5dad0 Dirk Pattinson
  | HCAT (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 2
1968
  | HCOR (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 5
1969
  | HCAND (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 6
1970
  | HCEX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 3
1971
  | HCAX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 4
1972
  | HCMORETHAN (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 7
1973
  | HCMAXEXCEPT (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 8
1974
  | HCATLEASTPROB (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 9
1975
  | HCLESSPROBFAIL (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 10
1976
  | HCCHC (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 11
1977
  | HCFUS (first, f1) -> base * (base * (Hashtbl.hash first) + f1.HC.hkey) + 13
1978
  | HCENFORCES (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 14
1979
  | HCALLOWS   (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 15
1980 c49eea11 Thorsten Wißmann
  | HCCONST s -> Hashtbl.hash s + 16
1981
  | HCCONSTN s -> Hashtbl.hash s + 17
1982 19f5dad0 Dirk Pattinson
  | HCNORM (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 18
1983
  | HCNORMN (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 19
1984
  | HCID (f1) -> base * f1.HC.hkey + 20
1985 508e3c33 Christoph Egger
  | HCMU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 21
1986
  | HCNU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 22
1987 4fd28192 Thorsten Wißmann
1988
(** Determines the "real" formula of a formula node.
1989
    @param f A formula node.
1990
    @return The formula (in negation normal form) which corresponds to f.
1991
 *)
1992
let toFml_hcFormula_node f =
1993
  match f with
1994
  | HCTRUE -> TRUE
1995
  | HCFALSE -> FALSE
1996
  | HCAP s -> AP s
1997 508e3c33 Christoph Egger
  | HCVAR s -> VAR s
1998 4fd28192 Thorsten Wißmann
  | HCNOT s -> NOT (AP s)
1999
  | HCAT (s, f1) -> AT (s, f1.HC.fml)
2000
  | HCOR (f1, f2) -> OR (f1.HC.fml, f2.HC.fml)
2001
  | HCAND (f1, f2) -> AND (f1.HC.fml, f2.HC.fml)
2002
  | HCEX (s, f1) -> EX (s, f1.HC.fml)
2003
  | HCAX (s, f1) -> AX (s, f1.HC.fml)
2004 f1fa9ad5 Thorsten Wißmann
  | HCENFORCES (s, f1) -> ENFORCES (s, f1.HC.fml)
2005
  | HCALLOWS (s, f1) -> ALLOWS (s, f1.HC.fml)
2006 af276a36 Thorsten Wißmann
  | HCMORETHAN (n, s, f1) -> MORETHAN (n, s, f1.HC.fml)
2007
  | HCMAXEXCEPT (n, s, f1) -> MAXEXCEPT (n, s, f1.HC.fml)
2008 86b07be8 Thorsten Wißmann
  | HCATLEASTPROB (p, f1) -> ATLEASTPROB (p, f1.HC.fml)
2009 9bae2c4f Thorsten Wißmann
  | HCLESSPROBFAIL (p, f1) -> LESSPROBFAIL (p, f1.HC.fml)
2010 c49eea11 Thorsten Wißmann
  | HCCONST s -> CONST s
2011
  | HCCONSTN s -> CONSTN s
2012 19f5dad0 Dirk Pattinson
  | HCID (f1) -> ID(f1.HC.fml)
2013
  | HCNORM (f1, f2) -> NORM(f1.HC.fml, f2.HC.fml)
2014
  | HCNORMN (f1, f2) -> NORMN(f1.HC.fml, f2.HC.fml)
2015 4fd28192 Thorsten Wißmann
  | HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml)
2016
  | HCFUS (first, f1) -> FUS (first, f1.HC.fml)
2017 508e3c33 Christoph Egger
  | HCMU (var, f1) -> MU (var, f1.HC.fml)
2018
  | HCNU (var, f1) -> NU (var, f1.HC.fml)
2019 4fd28192 Thorsten Wißmann
2020
(** Determines the negation (in negation normal form) of a formula node.
2021
    @param f A formula node.
2022
    @return The negation (in negation normal form) of f.
2023
 *)
2024
let negNde_hcFormula_node f =
2025
  match f with
2026
  | HCTRUE -> HCFALSE
2027
  | HCFALSE -> HCTRUE
2028
  | HCAP s -> HCNOT s
2029
  | HCNOT s -> HCAP s
2030 92feed46 Christoph Egger
  | HCVAR s -> f
2031 4fd28192 Thorsten Wißmann
  | HCAT (s, f1) -> HCAT (s, f1.HC.neg)
2032
  | HCOR (f1, f2) -> HCAND (f1.HC.neg, f2.HC.neg)
2033
  | HCAND (f1, f2) -> HCOR (f1.HC.neg, f2.HC.neg)
2034
  | HCEX (s, f2) -> HCAX (s, f2.HC.neg)
2035
  | HCAX (s, f2) -> HCEX (s, f2.HC.neg)
2036 f1fa9ad5 Thorsten Wißmann
  | HCENFORCES (s, f2) -> HCALLOWS (s, f2.HC.neg)
2037
  | HCALLOWS (s, f2) -> HCENFORCES (s, f2.HC.neg)
2038 af276a36 Thorsten Wißmann
  | HCMORETHAN (n, s, f1) -> HCMAXEXCEPT (n, s, f1.HC.neg)
2039
  | HCMAXEXCEPT (n, s, f1) -> HCMORETHAN (n, s, f1.HC.neg)
2040 9bae2c4f Thorsten Wißmann
  | HCATLEASTPROB (p, f1) -> HCLESSPROBFAIL (p, f1.HC.neg)
2041
  | HCLESSPROBFAIL (p, f1) -> HCATLEASTPROB (p, f1.HC.neg)
2042 c49eea11 Thorsten Wißmann
  | HCCONST s -> HCCONSTN s
2043
  | HCCONSTN s -> HCCONST s
2044 19f5dad0 Dirk Pattinson
  | HCID (f1) -> HCID(f1.HC.neg)
2045
  | HCNORM (f1, f2) -> HCNORMN(f1.HC.neg, f2.HC.neg)
2046
  | HCNORMN (f1, f2) -> HCNORM(f1.HC.neg, f2.HC.neg)
2047 d58bba0f Dirk Pattinson
  | HCCHC (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg)
2048 4fd28192 Thorsten Wißmann
  | HCFUS (first, f1) -> HCFUS (first, f1.HC.neg)
2049 92feed46 Christoph Egger
  | HCMU (name, f1) -> HCNU (name, f1.HC.neg)
2050
  | HCNU (name, f1) -> HCMU (name, f1.HC.neg)
2051 4fd28192 Thorsten Wißmann
2052
(** An instantiation of hash-consing for formulae.
2053
 *)
2054
module HcFormula = HC.Make(
2055
  struct
2056
    type nde = hcFormula_node
2057
    type fml = formula
2058
    let equal (n1 : nde) n2 = equal_hcFormula_node n1 n2
2059
    let hash (n : nde) = hash_hcFormula_node n
2060
    let negNde (n : nde) = negNde_hcFormula_node n
2061
    let toFml (n : nde) = toFml_hcFormula_node n
2062
  end
2063
 )
2064
2065
(** Converts a formula into its hash-consed version.
2066
    @param hcF A hash-cons table for formulae.
2067
    @param f A formula in negation normal form.
2068
    @return The hash-consed version of f.
2069
    @raise CoAlgException if f is not in negation normal form.
2070
*)
2071
let rec hc_formula hcF f =
2072
  match f with
2073
  | TRUE -> HcFormula.hashcons hcF HCTRUE
2074
  | FALSE -> HcFormula.hashcons hcF HCFALSE
2075
  | AP s -> HcFormula.hashcons hcF (HCAP s)
2076 508e3c33 Christoph Egger
  | VAR s -> HcFormula.hashcons hcF (HCVAR s)
2077 4fd28192 Thorsten Wißmann
  | NOT (AP s) -> HcFormula.hashcons hcF (HCNOT s)
2078
  | AT (s, f1) ->
2079
      let tf1 = hc_formula hcF f1 in
2080
      HcFormula.hashcons hcF (HCAT (s, tf1))
2081
  | OR (f1, f2) ->
2082
      let tf1 = hc_formula hcF f1 in
2083
      let tf2 = hc_formula hcF f2 in
2084
      HcFormula.hashcons hcF (HCOR (tf1, tf2))
2085
  | AND (f1, f2) ->
2086
      let tf1 = hc_formula hcF f1 in
2087
      let tf2 = hc_formula hcF f2 in
2088
      HcFormula.hashcons hcF (HCAND (tf1, tf2))
2089
  | NOT _
2090
  | EQU _
2091 af276a36 Thorsten Wißmann
  | MIN _
2092
  | MAX _
2093 4fd28192 Thorsten Wißmann
  | IMP _ -> raise (CoAlgException "Formula is not in negation normal form.")
2094
  | EX (s, f1) ->
2095
      let tf1 = hc_formula hcF f1 in
2096
      HcFormula.hashcons hcF (HCEX (s, tf1))
2097
  | AX (s, f1) ->
2098
      let tf1 = hc_formula hcF f1 in
2099
      HcFormula.hashcons hcF (HCAX (s, tf1))
2100 f1fa9ad5 Thorsten Wißmann
  | ENFORCES (s, f1) ->
2101
      let tf1 = hc_formula hcF f1 in
2102
      HcFormula.hashcons hcF (HCENFORCES (s, tf1))
2103
  | ALLOWS (s, f1) ->
2104
      let tf1 = hc_formula hcF f1 in
2105
      HcFormula.hashcons hcF (HCALLOWS (s, tf1))
2106 af276a36 Thorsten Wißmann
  | MORETHAN  (n, s, f1) ->
2107 4fd28192 Thorsten Wißmann
      let tf1 = hc_formula hcF f1 in
2108 af276a36 Thorsten Wißmann
      HcFormula.hashcons hcF (HCMORETHAN (n, s, tf1))
2109
  | MAXEXCEPT  (n, s, f1) ->
2110 4fd28192 Thorsten Wißmann
      let tf1 = hc_formula hcF f1 in
2111 af276a36 Thorsten Wißmann
      HcFormula.hashcons hcF (HCMAXEXCEPT (n, s, tf1))
2112 86b07be8 Thorsten Wißmann
  | ATLEASTPROB (p, f1) ->
2113
      HcFormula.hashcons hcF (HCATLEASTPROB (p, hc_formula hcF f1))
2114 9bae2c4f Thorsten Wißmann
  | LESSPROBFAIL (p, f1) ->
2115
      HcFormula.hashcons hcF (HCLESSPROBFAIL (p, hc_formula hcF f1))
2116 c49eea11 Thorsten Wißmann
  | CONST s ->
2117
      HcFormula.hashcons hcF (HCCONST s)
2118
  | CONSTN s ->
2119
      HcFormula.hashcons hcF (HCCONSTN s)
2120 19f5dad0 Dirk Pattinson
  | ID f1 ->
2121
    let tf1 = hc_formula hcF f1 in
2122
      HcFormula.hashcons hcF (HCID tf1)
2123
  | NORM (f1, f2) ->
2124
      let tf1 = hc_formula hcF f1 in
2125
      let tf2 = hc_formula hcF f2 in
2126
      HcFormula.hashcons hcF (HCNORM (tf1, tf2))
2127
  | NORMN (f1, f2) ->
2128
      let tf1 = hc_formula hcF f1 in
2129
      let tf2 = hc_formula hcF f2 in
2130
      HcFormula.hashcons hcF (HCNORMN (tf1, tf2))
2131 4fd28192 Thorsten Wißmann
  | CHC (f1, f2) ->
2132
      let tf1 = hc_formula hcF f1 in
2133
      let tf2 = hc_formula hcF f2 in
2134
      HcFormula.hashcons hcF (HCCHC (tf1, tf2))
2135
  | FUS (first, f1) ->
2136
      let tf1 = hc_formula hcF f1 in
2137
      HcFormula.hashcons hcF (HCFUS (first, tf1))
2138 508e3c33 Christoph Egger
  | MU (var, f1) ->
2139 c5c25acf Christoph Egger
     let tf1 = hc_formula hcF f1 in
2140
     HcFormula.hashcons hcF (HCMU (var, tf1))
2141 508e3c33 Christoph Egger
  | NU (var, f1) ->
2142 c5c25acf Christoph Egger
     let tf1 = hc_formula hcF f1 in
2143
     HcFormula.hashcons hcF (HCNU (var, tf1))
2144 8cac0897 Christoph Egger
  | AF _
2145
  | EF _
2146
  | AG _
2147
  | EG _
2148
  | AU _
2149
  | EU _ ->
2150 c5c25acf Christoph Egger
     raise (CoAlgException ("nnf: CTL should have been removed at this point"))
2151 4fd28192 Thorsten Wißmann
2152 cc07e93d Christoph Egger
(* Replace the Variable name in f with formula formula
2153
   hc_replace foo φ ψ => ψ[foo |-> φ]
2154
 *)
2155
let rec hc_replace hcF name (formula: hcFormula) (f: hcFormula) =
2156
  let func = hc_replace hcF name formula in
2157
  let gennew = HcFormula.hashcons hcF in
2158
  match f.HC.node with
2159
  | HCTRUE
2160
  | HCFALSE
2161
  | HCAP _
2162
  | HCNOT _
2163
  | HCCONST _
2164
  | HCCONSTN _ -> f
2165
  | HCVAR s ->
2166 c5c25acf Christoph Egger
     if compare s name == 0
2167
     then formula
2168
     else f
2169 cc07e93d Christoph Egger
  | HCAT (s, f1) ->
2170 c5c25acf Christoph Egger
     let nf1 = func f1 in
2171
     if nf1 == f1 then f else gennew (HCAT(s, nf1))
2172 cc07e93d Christoph Egger
  | HCOR (f1, f2) ->
2173 c5c25acf Christoph Egger
     let nf1 = func f1 in
2174
     let nf2 = func f2 in
2175
     if nf1 == f1 && nf2 == f2 then f else gennew (HCOR(nf1, nf2))
2176 cc07e93d Christoph Egger
  | HCAND (f1, f2) ->
2177 c5c25acf Christoph Egger
     let nf1 = func f1 in
2178
     let nf2 = func f2 in
2179
     if nf1 == f1 && nf2 == f2 then f else gennew (HCAND(nf1, nf2))
2180 cc07e93d Christoph Egger
  | HCEX (s, f1) ->
2181 c5c25acf Christoph Egger
     let nf1 = func f1 in
2182
     if nf1 == f1 then f else gennew (HCEX(s, nf1))
2183 cc07e93d Christoph Egger
  | HCAX (s, f1) ->
2184
     let nf1 = func f1 in
2185 c5c25acf Christoph Egger
     if nf1 == f1 then f else gennew (HCAX(s, nf1))
2186 cc07e93d Christoph Egger
  | HCENFORCES (s, f1) ->
2187 c5c25acf Christoph Egger
     let nf1 = func f1 in
2188
     if nf1 == f1 then f else gennew (HCENFORCES(s, nf1))
2189 cc07e93d Christoph Egger
  | HCALLOWS (s, f1) ->
2190
     let nf1 = func f1 in
2191 c5c25acf Christoph Egger
     if nf1 == f1 then f else gennew (HCALLOWS(s, nf1))
2192 cc07e93d Christoph Egger
  | HCMORETHAN  (n, s, f1) ->
2193
     let nf1 = func f1 in
2194 c5c25acf Christoph Egger
     if nf1 == f1 then f else gennew (HCMORETHAN(n, s, nf1))
2195 cc07e93d Christoph Egger
  | HCMAXEXCEPT  (n, s, f1) ->
2196 c5c25acf Christoph Egger
     let nf1 = func f1 in
2197
     if nf1 == f1 then f else gennew (HCMAXEXCEPT(n, s, nf1))
2198 cc07e93d Christoph Egger
  | HCATLEASTPROB (p, f1) ->
2199
     let nf1 = func f1 in
2200 c5c25acf Christoph Egger
     if nf1 == f1 then f else gennew (HCATLEASTPROB(p, nf1))
2201 cc07e93d Christoph Egger
  | HCLESSPROBFAIL (p, f1) ->
2202
     let nf1 = func f1 in
2203 c5c25acf Christoph Egger
     if nf1 == f1 then f else gennew (HCLESSPROBFAIL(p, nf1))
2204 cc07e93d Christoph Egger
  | HCID f1 ->
2205
     let nf1 = func f1 in
2206 c5c25acf Christoph Egger
     if nf1 == f1 then f else gennew (HCID(nf1))
2207 cc07e93d Christoph Egger
  | HCNORM (f1, f2) ->
2208 c5c25acf Christoph Egger
     let nf1 = func f1 in
2209
     let nf2 = func f2 in
2210
     if nf1 == f1 && nf2 == f2 then f else gennew (HCNORM(nf1, nf2))
2211 cc07e93d Christoph Egger
  | HCNORMN (f1, f2) ->
2212 c5c25acf Christoph Egger
     let nf1 = func f1 in
2213
     let nf2 = func f2 in
2214
     if nf1 == f1 && nf2 == f2 then f else gennew (HCNORMN(nf1, nf2))
2215 cc07e93d Christoph Egger
  | HCCHC (f1, f2) ->
2216 c5c25acf Christoph Egger
     let nf1 = func f1 in
2217
     let nf2 = func f2 in
2218
     if nf1 == f1 && nf2 == f2 then f else gennew (HCCHC(nf1, nf2))
2219 cc07e93d Christoph Egger
  | HCFUS (first, f1) ->
2220
     let nf1 = func f1 in
2221 c5c25acf Christoph Egger
     if nf1 == f1 then f else gennew (HCFUS(first, nf1))
2222 cc07e93d Christoph Egger
  | HCMU (var, f1) ->
2223 c5c25acf Christoph Egger
     if compare var name != 0 then
2224 854e1338 Christoph Egger
       let nf1 = func f1 in
2225 c5c25acf Christoph Egger
       if nf1 == f1 then f else gennew (HCMU(var, nf1))
2226
     else
2227
       f
2228 cc07e93d Christoph Egger
  | HCNU (var, f1) ->
2229 c5c25acf Christoph Egger
     if compare var name != 0 then
2230 854e1338 Christoph Egger
       let nf1 = func f1 in
2231 c5c25acf Christoph Egger
       if nf1 == f1 then f else gennew (HCNU(var, nf1))
2232
     else
2233
       f
2234 cc07e93d Christoph Egger
2235 5e7c8aa1 Christoph Egger
let rec hc_freeIn variable (f: hcFormula) =
2236
  match f.HC.node with
2237
  | HCTRUE
2238
  | HCFALSE
2239
  | HCAP _
2240
  | HCNOT _
2241
  | HCCONST _
2242
  | HCCONSTN _ -> false
2243
  | HCVAR s ->
2244
     if compare variable s == 0
2245
     then true
2246
     else false
2247
  | HCAT (s, f1) ->
2248
     hc_freeIn variable f1
2249
  | HCOR (f1, f2)
2250
  | HCAND (f1, f2) ->
2251
     hc_freeIn variable f1 || hc_freeIn variable f2
2252
  | HCEX (_, f1)
2253
  | HCAX (_, f1)
2254
  | HCENFORCES (_, f1)
2255
  | HCALLOWS (_, f1)
2256
  | HCMORETHAN  (_, _, f1)
2257
  | HCMAXEXCEPT  (_, _, f1)
2258
  | HCATLEASTPROB (_, f1)
2259
  | HCLESSPROBFAIL (_, f1)
2260
  | HCID f1 ->
2261
     hc_freeIn variable f1
2262
  | HCNORM (f1, f2)
2263
  | HCNORMN (f1, f2)
2264
  | HCCHC (f1, f2) ->
2265
     hc_freeIn variable f1 || hc_freeIn variable f2
2266
  | HCFUS (first, f1) ->
2267
     hc_freeIn variable f1
2268
  | HCMU (var, f1)
2269
  | HCNU (var, f1) ->
2270
     (* Do we need to exclude bound variables here? *)
2271
     hc_freeIn variable f1
2272
2273 cc07e93d Christoph Egger
2274 4fd28192 Thorsten Wißmann
(** An instantiation of a hash table (of the standard library)
2275
    for hash-consed formulae. The test for equality
2276
    and computing the hash value is done in constant time.
2277
 *)
2278
module HcFHt = Hashtbl.Make(
2279
  struct
2280
    type t = hcFormula
2281
    let equal (f1 : t) f2 = f1.HC.tag = f2.HC.tag
2282
    let hash (f : t) = f.HC.tag
2283
  end
2284
 )