Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgFormula.ml @ e30caa42

History | View | Annotate | Download (68.5 KB)

1
(** 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
module L = List
10
module Str = String
11

    
12

    
13
(** A general exception for all kinds of errors
14
    that can happen in the tableau procedure.
15
    More specific information is given in the argument.
16
 *)
17
exception CoAlgException of string
18

    
19
(** Indicates the sort of a sorted formula
20
 *)
21
type sort = int
22

    
23
type rational = { nominator: int; denominator: int }
24

    
25
let string_of_rational r =
26
    (string_of_int r.nominator)^"/"^(string_of_int r.denominator)
27

    
28
let rational_of_int n d = { nominator = n; denominator = d }
29

    
30
(** Defines (unsorted) coalgebraic formulae.
31
 *)
32
type formula =
33
  | TRUE
34
  | FALSE
35
  | AP of string (* atomic proposition *)
36
  | 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
  | ENFORCES of int list * formula
45
  | ALLOWS   of int list * formula
46
  | MIN of int * string * formula
47
  | MAX of int * string * formula
48
  | MORETHAN of int * string * formula (* diamond of GML *)
49
  | MAXEXCEPT of int * string * formula (* box of GML *)
50
  | ATLEASTPROB of rational * formula (* = {>= 0.5} C  ---> C occurs with *)
51
                                      (*  probability of at least 50% *)
52
  | LESSPROBFAIL of rational * formula (* = [1/2] C = {< 1/2} ¬ C ---> C fails with *)
53
                                        (* probability of less than 50% *)
54
  | CONST of string  (* constant functor with value string *)
55
  | CONSTN of string  (* constant functor with value other than string *)
56
  | 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
  | CHC of formula * formula (* Choice is self-dual *)
60
  | FUS of bool * formula
61
  | MU of string * formula
62
  | NU of string * formula
63
  | VAR of string
64
  | 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
  | AR of formula * formula
71
  | ER of formula * formula
72

    
73
exception ConversionException of formula
74

    
75

    
76
(** Defines sorted coalgebraic formulae.
77
 *)
78
type sortedFormula = sort * formula
79

    
80

    
81
(** Determines whether a name indicates a nominal.
82
    @param A string s.
83
    @return True iff s contains a prime character.
84
 *)
85
let isNominal s = String.contains s '\''
86

    
87

    
88
(** Determines the size of a formula.
89
    @param f A formula.
90
    @return The size of f.
91
 *)
92
let rec sizeFormula f =
93
  match f with
94
  | TRUE
95
  | FALSE
96
  | AP _ -> 1
97
  | NOT f1
98
  | AT (_, f1) -> succ (sizeFormula f1)
99
  | OR (f1, f2)
100
  | AND (f1, f2)
101
  | EQU (f1, f2)
102
  | IMP (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
103
  | EX (_, f1)
104
  | AX (_, f1)
105
  | ENFORCES (_, f1)
106
  | ALLOWS (_, f1) -> succ (sizeFormula f1)
107
  | MIN (_, _, f1)
108
  | MAX (_, _, f1)
109
  | ATLEASTPROB (_, f1)
110
  | LESSPROBFAIL (_, f1)
111
  | MORETHAN (_, _, f1)
112
  | MAXEXCEPT (_, _, f1) -> succ (sizeFormula f1)
113
  | ID (f1) -> succ (sizeFormula f1)
114
  | NORM(f1, f2)
115
  | NORMN(f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
116
  | CONST _
117
  | CONSTN _ -> 1
118
  | CHC (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
119
  | FUS (_, f1) -> succ (sizeFormula f1)
120
  | MU (_, f1)
121
  | NU (_, f1) -> succ (succ (sizeFormula f1))
122
  | VAR _ -> 1
123
  | AF _ | EF _
124
  | AG _ | EG _
125
  | AU _ | EU _
126
  | AR _ | ER _ ->
127
            raise (CoAlgException ("sizeFormula: CTL should have been removed at this point"))
128

    
129
(** Determines the size of a sorted formula.
130
    @param f A sorted formula.
131
    @return The size of f.
132
 *)
133
let sizeSortedFormula f = sizeFormula (snd f)
134

    
135

    
136
(* think of func: (formula -> unit) -> formula -> unit as identity.
137
  iterate over all subformulae and collect side effects. *)
138
let rec iter func formula =
139
    func formula;
140
    let proc = iter func in (* proc = "process" *)
141
    match formula with
142
    | TRUE | FALSE | AP _ | VAR _ -> ()
143
    | CONST _
144
    | CONSTN _ -> ()
145
    | NOT a | AT (_,a)
146
    | EX (_,a) | AX (_,a) -> proc a
147
    | OR (a,b) | AND (a,b)
148
    | EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
149
    | ENFORCES (_,a) | ALLOWS   (_,a)
150
    | MIN (_,_,a)    | MAX (_,_,a)
151
    | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
152
    | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
153
    | ID(a) -> proc a
154
    | NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
155
    | CHC (a,b)  -> (proc a ; proc b)
156
    | FUS (_,a) -> proc a
157
    | MU (_, f) | NU (_, f) -> proc f
158
    | AF f | EF f | AG f | EG f -> proc f
159
    | AU (f1, f2) | EU (f1, f2) | AR (f1, f2) | ER (f1, f2) -> (proc f1; proc f2)
160

    
161
let rec convert_post func formula = (* run over all subformulas in post order *)
162
  let c = convert_post func in (* some shorthand *)
163
  (* replace parts of the formula *)
164
  let formula = (match formula with
165
    (* 0-ary constructors *)
166
    | TRUE | FALSE | AP _ | VAR _ -> formula
167
    | CONST _
168
    | CONSTN _ -> formula
169
    (* unary *)
170
    | NOT a -> NOT (c a)
171
    | AT (s,a) -> AT (s,c a)
172
    (* binary *)
173
    | OR (a,b) -> OR (c a, c b)
174
    | AND (a,b) -> AND (c a, c b)
175
    | EQU (a,b) -> EQU (c a, c b)
176
    | IMP (a,b) -> IMP (c a, c b)
177
    | EX (s,a) -> EX (s,c a)
178
    | AX (s,a) -> AX (s,c a)
179
    | ENFORCES (s,a) -> ENFORCES (s,c a)
180
    | ALLOWS   (s,a) -> ALLOWS   (s,c a)
181
    | MIN (n,s,a) -> MIN (n,s,c a)
182
    | MAX (n,s,a) -> MAX (n,s,c a)
183
    | ATLEASTPROB (p,a) -> ATLEASTPROB (p, c a)
184
    | LESSPROBFAIL (p,a) -> LESSPROBFAIL (p, c a)
185
    | MORETHAN (n,s,a) -> MORETHAN (n,s,c a)
186
    | MAXEXCEPT (n,s,a) -> MAXEXCEPT (n,s,c a)
187
    | ID(a) -> ID (c a)
188
    | NORM(a, b) -> NORM(c a, c b)
189
    | NORMN(a, b) -> NORMN(c a, c b)
190
    | CHC (a,b) -> CHC (c a, c b)
191
    | FUS (s,a) -> FUS (s, c a)
192
    | MU (n, f1) -> MU (n, c f1)
193
    | NU (n, f1) -> NU (n, c f1)
194
    | AF f1 -> AF (c f1)
195
    | EF f1 -> EF (c f1)
196
    | AG f1 -> AG (c f1)
197
    | EG f1 -> EG (c f1)
198
    | AU (f1, f2) -> AU (c f1, c f2)
199
    | EU (f1, f2) -> EU (c f1, c f2)
200
    | AR (f1, f2) -> AR (c f1, c f2)
201
    | ER (f1, f2) -> ER (c f1, c f2))
202
  in
203
  func formula
204

    
205
let convertToK formula = (* tries to convert a formula to a pure K formula *)
206
  let helper formula = match formula with
207
  | ENFORCES _ | ALLOWS _ -> raise (ConversionException formula)
208
  | MORETHAN (0,s,a) | MIN (1,s,a) -> EX (s,a)
209
  | MAX (0,s,a) -> AX (s, NOT a)
210
  | MAXEXCEPT (0,s,a) -> AX (s, a)
211
  | TRUE | FALSE
212
  | EQU _ | IMP _
213
  | AND _ | OR _
214
  | AP _ | NOT _
215
  | AX _ | EX _
216
  | CHC _ | FUS _ -> formula
217
  | _ -> raise (ConversionException formula)
218
  in
219
  convert_post helper formula
220

    
221
let convertToGML formula = (* tries to convert a formula to a pure GML formula *)
222
  let helper formula = match formula with
223
  | ENFORCES _ | ALLOWS _ -> raise (ConversionException formula)
224
  | MORETHAN _ | MIN _ | MAX _ | MAXEXCEPT _ -> formula
225
  | TRUE | FALSE
226
  | EQU _ | IMP _
227
  | AND _ | OR _
228
  | AP _ | NOT _
229
  | CHC _ | FUS _ -> formula
230
  | AX (r,a) -> MAXEXCEPT (0,r,a)
231
  | EX (r,a) -> MORETHAN  (0,r,a)
232
  | _ -> raise (ConversionException formula)
233
  in
234
  convert_post helper formula
235

    
236
let gensym = Stream.from (fun i -> Some (Printf.sprintf "#gensym%x#" i))
237

    
238
let convertToMu formula =
239
  let helper formula =
240
    match formula with
241
    | AF f1 ->
242
       MU ("#AF#", (OR (f1, (AX ("", (VAR "#AF#"))))))
243
    | EF f1 ->
244
       MU ("#EF#", (OR (f1, (EX ("", (VAR "#EF#"))))))
245
    | AG f1 ->
246
       NU ("#AG#", (AND (f1, (AX ("", (VAR "#AG#"))))))
247
    | EG f1 ->
248
       NU ("#EG#", (AND (f1, (EX ("", (VAR "#EG#"))))))
249
    | AU (f1, f2) ->
250
       MU ("#AU#", (OR (f2, (AND (f1, (AX ("", (VAR "#AU#"))))))))
251
    | EU (f1, f2) ->
252
       MU ("#EU#", (OR (f2, (AND (f1, (EX ("", (VAR "#EU#"))))))))
253
    | AR (f1, f2) ->
254
       NU ("#AR#", (AND (f2, (OR (f1, (AX ("", (VAR "#AR#"))))))))
255
    | ER (f1, f2) ->
256
       NU ("#ER#", (AND (f2, (OR (f1, (EX ("", (VAR "#ER#"))))))))
257

    
258
    | _ -> formula
259
  in
260
  convert_post helper formula
261

    
262
(** Appends a string representation of a formula to a string buffer.
263
    Parentheses are ommited where possible
264
    where the preference rules are defined as usual.
265
    @param sb A string buffer.
266
    @param f A formula.
267
 *)
268
let rec exportFormula_buffer sb f =
269
  let negate = function
270
    | NOT f -> f
271
    | f -> NOT f
272
  in
273
  let prio n lf =
274
    let prionr = function
275
      | EQU _ -> 0
276
      | IMP _  -> 1
277
      | OR _ -> 2
278
      | AND _ -> 3
279
      | _ -> 4
280
    in
281
    if prionr lf < n then begin
282
      Buffer.add_char sb '(';
283
      exportFormula_buffer sb lf;
284
      Buffer.add_char sb ')'
285
    end
286
    else exportFormula_buffer sb lf
287
  in
288
  match f with
289
  | TRUE -> Buffer.add_string sb "True"
290
  | FALSE -> Buffer.add_string sb "False"
291
  | AP s -> Buffer.add_string sb s
292
  | NOT f1 ->
293
      Buffer.add_string sb "~";
294
      prio 4 f1
295
  | AT (s, f1) ->
296
      Buffer.add_string sb "@ ";
297
      Buffer.add_string sb s;
298
      Buffer.add_string sb " ";
299
      prio 4 f1
300
  | OR (f1, f2) ->
301
      prio 2 f1;
302
      Buffer.add_string sb " | ";
303
      prio 2 f2
304
  | AND (f1, f2) ->
305
      prio 3 f1;
306
      Buffer.add_string sb " & ";
307
      prio 3 f2
308
  | EQU (f1, f2) ->
309
      prio 0 f1;
310
      Buffer.add_string sb " <=> ";
311
      prio 0 f2
312
  | IMP (f1, f2) ->
313
      prio 2 f1;
314
      Buffer.add_string sb " => ";
315
      prio 2 f2
316
  | EX (s, f1) ->
317
      Buffer.add_string sb "<";
318
      Buffer.add_string sb s;
319
      Buffer.add_string sb ">";
320
      prio 4 f1
321
  | AX (s, f1) ->
322
      Buffer.add_string sb "[";
323
      Buffer.add_string sb s;
324
      Buffer.add_string sb "]";
325
      prio 4 f1
326
  | ALLOWS (s, f1) ->
327
      Buffer.add_string sb "<{";
328
      Buffer.add_string sb (
329
          match s with
330
          | [] -> " "
331
          | _ ->(Str.concat " " (L.map string_of_int s))
332
      );
333
      Buffer.add_string sb "}>";
334
      prio 4 f1
335
  | ENFORCES (s, f1) ->
336
      Buffer.add_string sb "[{";
337
      Buffer.add_string sb (
338
          match s with
339
          | [] -> " "
340
          | _ ->(Str.concat " " (L.map string_of_int s))
341
      );
342
      Buffer.add_string sb "}]";
343
      prio 4 f1
344
  | ATLEASTPROB (p, f1) ->
345
      Buffer.add_string sb "{>=";
346
      Buffer.add_string sb (string_of_rational p);
347
      Buffer.add_string sb "}";
348
      prio 4 f1
349
  | LESSPROBFAIL (p, f1) ->
350
      Buffer.add_string sb "{<";
351
      Buffer.add_string sb (string_of_rational p);
352
      Buffer.add_string sb "} ~ ";
353
      prio 4 f1
354
  | MIN (n, s, f1) ->
355
      Buffer.add_string sb "{>=";
356
      Buffer.add_string sb (string_of_int n);
357
      Buffer.add_string sb " ";
358
      Buffer.add_string sb s;
359
      Buffer.add_string sb "}";
360
      prio 4 f1
361
  | MAX (n, s, f1) ->
362
      Buffer.add_string sb "{<=";
363
      Buffer.add_string sb (string_of_int n);
364
      Buffer.add_string sb " ";
365
      Buffer.add_string sb s;
366
      Buffer.add_string sb "}";
367
      prio 4 f1
368
  | MORETHAN (n, s, f1) ->
369
      Buffer.add_string sb "{>";
370
      Buffer.add_string sb (string_of_int n);
371
      Buffer.add_string sb " ";
372
      Buffer.add_string sb s;
373
      Buffer.add_string sb "}";
374
      prio 4 f1
375
  | MAXEXCEPT (n, s, f1) ->
376
      Buffer.add_string sb "{<=";
377
      Buffer.add_string sb (string_of_int n);
378
      Buffer.add_string sb " ~ ";
379
      Buffer.add_string sb s;
380
      Buffer.add_string sb "}";
381
      prio 4 f1 (* actually is prio of ~ and not of <= *)
382
  | ID (f1) ->
383
      Buffer.add_string sb "O";
384
      prio 4 f1
385
  | NORM(f1, f2) ->
386
      Buffer.add_string sb "(";
387
      exportFormula_buffer sb f1;
388
      Buffer.add_string sb " =o ";
389
      exportFormula_buffer sb f2;
390
      Buffer.add_string sb ")"
391
  | NORMN(f1, f2) ->
392
      Buffer.add_string sb "~(";
393
      exportFormula_buffer sb (negate f1);
394
      Buffer.add_string sb " =o ";
395
      exportFormula_buffer sb (negate f2);
396
      Buffer.add_string sb ")"
397
  | CHC (f1, f2) ->
398
      Buffer.add_string sb "(";
399
      exportFormula_buffer sb f1;
400
      Buffer.add_string sb " + ";
401
      exportFormula_buffer sb f2;
402
      Buffer.add_string sb ")"
403
  | CONST s -> Buffer.add_string sb "=";
404
      Buffer.add_string sb s
405
  | CONSTN s -> Buffer.add_string sb "~=";
406
      Buffer.add_string sb s
407
  | FUS (first, f1) ->
408
      Buffer.add_string sb (if first then "[pi1]" else "[pi2]");
409
      prio 4 f1
410
  | MU (s, f1) ->
411
      Buffer.add_string sb "μ";
412
      Buffer.add_string sb s;
413
      Buffer.add_string sb ".";
414
      prio 4 f1
415
  | NU (s, f1) ->
416
      Buffer.add_string sb "ν";
417
      Buffer.add_string sb s;
418
      Buffer.add_string sb ".";
419
      prio 4 f1
420
  | VAR s ->
421
     Buffer.add_string sb s
422
  | AF f1 ->
423
     Buffer.add_string sb "AF ";
424
     prio 4 f1
425
  | EF f1 ->
426
     Buffer.add_string sb "EF ";
427
     prio 4 f1
428
  | AG f1 ->
429
     Buffer.add_string sb "AG ";
430
     prio 4 f1
431
  | EG f1 ->
432
     Buffer.add_string sb "EG ";
433
     prio 4 f1
434
  | AU (f1, f2) ->
435
     Buffer.add_string sb "A (";
436
     prio 4 f1;
437
     Buffer.add_string sb " U ";
438
     prio 4 f2;
439
     Buffer.add_string sb ")"
440
  | EU (f1, f2) ->
441
     Buffer.add_string sb "E (";
442
     prio 4 f1;
443
     Buffer.add_string sb " U ";
444
     prio 4 f2;
445
     Buffer.add_string sb ")"
446
  | AR (f1, f2) ->
447
     Buffer.add_string sb "A (";
448
     prio 4 f1;
449
     Buffer.add_string sb " R ";
450
     prio 4 f2;
451
     Buffer.add_string sb ")"
452
  | ER (f1, f2) ->
453
     Buffer.add_string sb "E (";
454
     prio 4 f1;
455
     Buffer.add_string sb " R ";
456
     prio 4 f2;
457
     Buffer.add_string sb ")"
458

    
459

    
460
(** Converts a formula into a string representation.
461
    Parentheses are ommited where possible
462
    where the preference rules are defined as usual.
463
    @param f A formula.
464
    @return A string representing f.
465
 *)
466
let exportFormula f =
467
  let sb = Buffer.create 128 in
468
  exportFormula_buffer sb f;
469
  Buffer.contents sb
470

    
471
let string_of_formula = exportFormula
472

    
473
(** export (CL)-formula suitable for tatl-inputs *)
474
let rec exportTatlFormula_buffer sb f =
475
  let prio n lf =
476
    let prionr = function
477
      | EQU _ -> 0
478
      | IMP _  -> 1
479
      | OR _ -> 2
480
      | AND _ -> 3
481
      | _ -> 4
482
    in
483
    if prionr lf < n then begin
484
      Buffer.add_char sb '(';
485
      exportTatlFormula_buffer sb lf;
486
      Buffer.add_char sb ')'
487
    end
488
    else exportTatlFormula_buffer sb lf
489
  in
490
  match f with
491
  | TRUE -> Buffer.add_string sb "(p \\/ ~p)"
492
  | FALSE -> Buffer.add_string sb "(p /\\ ~p)"
493
  | AP s -> Buffer.add_string sb s
494
  | NOT f1 ->
495
      Buffer.add_string sb "~";
496
      prio 4 f1
497
  | OR (f1, f2) ->
498
      prio 2 f1;
499
      Buffer.add_string sb " \\/ ";
500
      prio 2 f2
501
  | AND (f1, f2) ->
502
      prio 3 f1;
503
      Buffer.add_string sb " /\\ ";
504
      prio 3 f2
505
  | EQU (f1, f2) ->
506
      prio 0 (AND (IMP (f1,f2), IMP (f2,f1)))
507
  | IMP (f1, f2) ->
508
      prio 2 f1;
509
      Buffer.add_string sb " -> ";
510
      prio 2 f2
511
  | ALLOWS (s, f1) ->
512
      Buffer.add_string sb "<<";
513
      Buffer.add_string sb (
514
          match s with
515
          | [] -> " "
516
          | _ ->(Str.concat "," (L.map string_of_int s))
517
      );
518
      Buffer.add_string sb ">>X ";
519
      prio 4 f1
520
  | ENFORCES (s, f1) ->
521
      Buffer.add_string sb "~<<";
522
      Buffer.add_string sb (
523
          match s with
524
          | [] -> " "
525
          | _ ->(Str.concat "," (L.map string_of_int s))
526
      );
527
      Buffer.add_string sb ">>X ~ ";
528
      prio 4 f1
529
  | EX _
530
  | AX _
531
  | MIN _
532
  | MAX _
533
  | MORETHAN _
534
  | MAXEXCEPT _
535
  | AT _
536
  | CONST _
537
  | CONSTN _
538
  | CHC _
539
  | ATLEASTPROB _
540
  | LESSPROBFAIL _
541
  | ID _
542
  | NORM _
543
  | NORMN _
544
  | FUS _
545
  | MU _
546
  | NU _
547
  | VAR _
548
  | AF _
549
  | EF _
550
  | AG _
551
  | EG _
552
  | AU _
553
  | EU _
554
  | AR _
555
  | ER _ -> raise (CoAlgException ("export to tatl: Not connectives of CL"))
556

    
557
let exportTatlFormula f =
558
  let sb = Buffer.create 128 in
559
  exportTatlFormula_buffer sb f;
560
  Buffer.contents sb
561

    
562
(** Appends a string representation of a sorted formula to a string buffer.
563
    Parentheses are ommited where possible
564
    where the preference rules are defined as usual.
565
    @param sb A string buffer.
566
    @param (s, f) A sorted formula.
567
 *)
568
let rec exportSortedFormula_buffer sb (s, f) =
569
  Buffer.add_string sb (string_of_int s);
570
  Buffer.add_string sb ": ";
571
  exportFormula_buffer sb f
572

    
573
(** Converts a sorted formula into a string representation.
574
    Parentheses are ommited where possible
575
    where the preference rules are defined as usual.
576
    @param f A sorted formula.
577
    @return A string representing f.
578
 *)
579
let exportSortedFormula f =
580
  let sb = Buffer.create 128 in
581
  exportSortedFormula_buffer sb f;
582
  Buffer.contents sb
583

    
584
(** Converts a (sorted) formula query into a string representation.
585
    @param tbox A list of sorted formulae representing a TBox.
586
    @param f A sorted formula.
587
    @return A string representing tbox |- f.
588
 *)
589
let exportQuery tbox f =
590
  let sb = Buffer.create 1000 in
591
  let rec expFl = function
592
    | [] -> ()
593
    | h::tl ->
594
        exportSortedFormula_buffer sb h;
595
        if tl <> [] then Buffer.add_string sb "; " else ();
596
        expFl tl
597
  in
598
  expFl tbox;
599
  Buffer.add_string sb "  |-  ";
600
  exportSortedFormula_buffer sb f;
601
  Buffer.contents sb
602

    
603
(** Converts a (sorted) formula query into a string representation. Such that
604
    coalg can read it again using importQuery
605
    @param tbox A list of sorted formulae representing a TBox.
606
    @param f A sorted formula.
607
    @return A string representing tbox |- f.
608
 *)
609
let exportQueryParsable tbox (_,f) =
610
  let sb = Buffer.create 1000 in
611
  let rec expFl = function
612
    | [] -> ()
613
    | (_,h)::tl ->
614
        exportFormula_buffer sb h;
615
        if tl <> [] then Buffer.add_string sb "; " else ();
616
        expFl tl
617
  in
618
  expFl tbox;
619
  Buffer.add_string sb "  |-  ";
620
  exportFormula_buffer sb f;
621
  Buffer.contents sb
622

    
623

    
624
(* NB: True and False are the propositional constants. Lower case
625
   true/false are regardes as atomic propositions and we emit a warning
626
*)
627
let lexer = A.make_lexer
628
    [":";";";"|-";"(";")";"=>";"<=>";"|";"&";"~";"@";"True";"False";"true";"false";"<";">";"[";"]";"{<=";"{>=";"}";"+";"[pi1]";"[pi2]"
629
     ;"[{";"}]";"<{";"}>";",";"/";"{<";"=";"=o";"O"
630
     ;"μ";"ν";"."
631
     ;"AX";"EX";"AF";"EF";"AG";"EG";"A";"E";"U";"R";"B"
632
    ]
633

    
634
let mk_exn s = CoAlgException s
635

    
636
(** Process from inside out. cons all variables seen, remove them when
637
    binding fixpoint is found. Fixpoint type may only change if last
638
    (inner) fixpoint didn't include any free variables.
639
 *)
640
let rec verifyMuAltFree formula =
641
  let proc = verifyMuAltFree in
642
  match formula with
643
  | TRUE | FALSE | AP _ -> ("none", [])
644
  | CONST _
645
  | CONSTN _ -> ("none", [])
646
  | AT (_,a) | NOT a
647
  | EX (_,a) | AX (_,a) -> proc a
648
  | OR (a,b) | AND (a,b)
649
  | EQU (a,b) | IMP (a,b) ->
650
     let (atype, afree) = proc a
651
     and (btype, bfree) = proc b in
652
     if (compare atype "μ" == 0 && compare btype "ν" == 0) ||
653
          (compare atype "ν" == 0 && compare btype "μ" == 0) then
654
       raise (CoAlgException ("formula not alternation-free"));
655
     if compare atype "none" == 0 then
656
       (btype, List.flatten [afree; bfree])
657
     else
658
       (atype, List.flatten [afree; bfree])
659
  | ENFORCES (_,a) | ALLOWS   (_,a)
660
  | MIN (_,_,a)    | MAX (_,_,a)
661
  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
662
  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
663
  | ID(a) -> proc a
664
  | NORM(a, b) | NORMN(a, b)
665
  | CHC (a,b)  ->
666
     let (atype, afree) = proc a
667
     and (btype, bfree) = proc b in
668
     if (compare atype "μ" == 0 && compare btype "ν" == 0) ||
669
          (compare atype "ν" == 0 && compare btype "μ" == 0) then
670
       raise (CoAlgException ("formula not alternation-free"));
671
     if compare atype "none" == 0 then
672
       (btype, List.flatten [afree; bfree])
673
     else
674
       (atype, List.flatten [afree; bfree])
675
  | FUS (_,a) -> proc a
676
  | MU (s, f) ->
677
     let (fptype, free) = proc f in
678
     (if (compare fptype "ν" == 0) then
679
        raise (CoAlgException ("formula not alternation-free")));
680
     let predicate x = compare x s != 0 in
681
     let newfree = List.filter predicate free in
682
     if newfree = [] then
683
       ("none", [])
684
     else
685
       ("μ", newfree)
686
  | NU (s, f) ->
687
     let (fptype, free) = proc f in
688
     (if (compare fptype "μ" == 0) then
689
        raise (CoAlgException ("formula not alternation-free")));
690
     let predicate x = compare x s != 0 in
691
     let newfree = List.filter predicate free in
692
     if newfree = [] then
693
       ("none", [])
694
     else
695
       ("ν", newfree)
696
  | VAR s -> ("none", [s])
697
  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ ->
698
     raise (CoAlgException ("verifyMuAltFree: CTL should have been removed at this point"))
699

    
700

    
701
(** Process from outside in. For every variable bound keep the tuple
702
    (name, negations). For every negation crossed map a +1 over snd on
703
    that list. For every variable met check that the matching
704
    negations is even.
705
 *)
706
let rec verifyMuMonotone negations formula =
707
  let proc = verifyMuMonotone negations in
708
  match formula with
709
  | TRUE | FALSE | AP _ -> ()
710
  | CONST _
711
  | CONSTN _ -> ()
712
  | AT (_,a)
713
  | EX (_,a) | AX (_,a) -> proc a
714
  | OR (a,b) | AND (a,b)
715
  | EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
716
  | ENFORCES (_,a) | ALLOWS   (_,a)
717
  | MIN (_,_,a)    | MAX (_,_,a)
718
  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
719
  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
720
  | ID(a) -> proc a
721
  | NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
722
  | CHC (a,b)  -> (proc a ; proc b)
723
  | FUS (_,a) -> proc a
724
  | MU (s, f)
725
  | NU (s, f) ->
726
     let newNeg = (s, 0) :: negations in
727
     verifyMuMonotone newNeg f
728
  | VAR s ->
729
     let finder (x, _) = compare x s == 0 in
730
     let (_, neg) = List.find finder negations in
731
     if ((neg land 1) != 0) then raise (CoAlgException ("formula not monotone"))
732
  | NOT a ->
733
     let increment (s, n) = (s, n+1) in
734
     let newNeg = List.map increment negations in
735
     verifyMuMonotone newNeg a
736
  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ ->
737
     raise (CoAlgException ("verifyMuMonotone: CTL should have been removed at this point"))
738

    
739
let rec verifyMuGuarded unguarded formula =
740
  let proc = verifyMuGuarded unguarded in
741
  match formula with
742
  | TRUE | FALSE | AP _ -> ()
743
  | CONST _
744
  | CONSTN _ -> ()
745
  | AT (_,a) | NOT a -> proc a
746
  | EX (_,a) | AX (_,a) -> verifyMuGuarded [] a
747
  | OR (a,b) | AND (a,b)
748
  | EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
749
  | ENFORCES (_,a) | ALLOWS   (_,a)
750
  | MIN (_,_,a)    | MAX (_,_,a)
751
  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
752
  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
753
  | ID(a) -> proc a
754
  | NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
755
  | CHC (a,b)  -> (proc a ; proc b)
756
  | FUS (_,a) -> proc a
757
  | MU (s, f)
758
  | NU (s, f) ->
759
     let newUnguard = s :: unguarded in
760
     verifyMuGuarded newUnguard f
761
  | VAR s ->
762
     let finder x = compare x s == 0 in
763
     if List.exists finder unguarded then
764
       raise (CoAlgException ("formula not guarded"))
765
  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ ->
766
     raise (CoAlgException ("verifyMuGuarded: CTL should have been removed at this point"))
767

    
768
let verifyFormula formula =
769
  verifyMuAltFree formula;
770
  verifyMuMonotone [] formula;
771
  verifyMuGuarded [] formula
772

    
773
(** These functions parse a token stream to obtain a formula.
774
    It is a standard recursive descent procedure.
775
    @param ts A token stream.
776
    @return The resulting (sub-)formula.
777
    @raise CoAlgException if ts does not represent a formula.
778
 *)
779
let rec parse_formula (symtab: 'a list) ts =
780
  let formula = (parse_imp symtab ts) in
781
  let f1 = convertToMu formula in
782
  match Stream.peek ts with
783
  | None -> f1
784
  | Some (A.Kwd "<=>") ->
785
      Stream.junk ts;
786
      let f2 = parse_formula symtab ts in
787
      EQU (f1, f2)
788
  | _ -> f1
789

    
790
(** These functions parse a token stream to obtain a formula.
791
    It is a standard recursive descent procedure.
792
    @param ts A token stream.
793
    @return The resulting (sub-)formula.
794
    @raise CoAlgException if ts does not represent a formula.
795
 *)
796
and parse_imp symtab ts=
797
  let f1 = parse_or symtab ts in
798
  match Stream.peek ts with
799
  | None -> f1
800
  | Some (A.Kwd "=>") ->
801
      Stream.junk ts;
802
      let f2 = parse_imp symtab ts in
803
      IMP (f1, f2)
804
  | _ -> f1
805

    
806
(** These functions parse a token stream to obtain a formula.
807
    It is a standard recursive descent procedure.
808
    @param ts A token stream.
809
    @return The resulting (sub-)formula.
810
    @raise CoAlgException if ts does not represent a formula.
811
 *)
812
and parse_or symtab ts =
813
  let f1 = parse_and symtab ts in
814
  match Stream.peek ts with
815
  | None -> f1
816
  | Some (A.Kwd "|") ->
817
      Stream.junk ts;
818
      let f2 = parse_or symtab ts in
819
      OR (f1, f2)
820
  | _ -> f1
821

    
822
(** These functions parse a token stream to obtain a formula.
823
    It is a standard recursive descent procedure.
824
    @param ts A token stream.
825
    @return The resulting (sub-)formula.
826
    @raise CoAlgException if ts does not represent a formula.
827
 *)
828
and parse_and symtab ts =
829
  let f1 = parse_cimp symtab ts in
830
  match Stream.peek ts with
831
  | None -> f1
832
  | Some (A.Kwd "&") ->
833
      Stream.junk ts;
834
      let f2 = parse_and symtab ts in
835
      AND (f1, f2)
836
  | _ -> f1
837

    
838
(** These functions parse a token stream to obtain a formula.
839
    It is a standard recursive descent procedure.
840
    @param ts A token stream.
841
    @return The resulting (sub-)formula.
842
    @raise CoAlgException if ts does not represent a formula.
843
 *)
844
and parse_cimp symtab ts =
845
  let f1 = parse_rest symtab ts in
846
  match Stream.peek ts with
847
  | None -> f1
848
  | Some (A.Kwd "=o") ->
849
      Stream.junk ts;
850
      let f2 = parse_cimp symtab ts in
851
      NORM (f1, f2)
852
  | _ -> f1
853

    
854
(** These functions parse a token stream to obtain a formula.
855
    It is a standard recursive descent procedure.
856
    @param ts A token stream.
857
    @return The resulting (sub-)formula.
858
    @raise CoAlgException if ts does not represent a formula.
859
 *)
860
and parse_rest symtab ts =
861
  let boxinternals noNo es =
862
    let n =
863
      if noNo then 0
864
      else
865
        match Stream.next ts with
866
        | A.Int n when n >= 0 -> n
867
        | t -> A.printError mk_exn ~t ~ts "<non-negative number> expected: "
868
    in
869
    let (s,denominator) =
870
      match Stream.peek ts with
871
      | Some (A.Ident s1) -> Stream.junk ts; (s1,0)
872
      | Some (A.Kwd c) when c = es -> ("", 0)
873
      | Some (A.Kwd "/") -> begin
874
            Stream.junk ts;
875
            match Stream.next ts with
876
            | A.Int denom when denom > 0 -> ("", denom)
877
            | t -> A.printError mk_exn ~t ~ts "<positive number> (the denominator) expected: "
878
        end
879
      | _ -> A.printError mk_exn ~ts ("role name or \"" ^ es ^ "\" expected: ")
880
    in
881
    if (denominator < n) then begin
882
       let explanation =
883
        ("nominator="^(string_of_int n)^" but denominator="^(string_of_int denominator))
884
       in
885
       A.printError mk_exn ~ts ("Nominator must not be larger than the denominator "
886
                               ^"("^explanation^") at: "
887
                               )
888
    end;
889
    let _ =
890
      match Stream.next ts with
891
      | A.Kwd c when c = es -> ()
892
      | t -> A.printError mk_exn ~t ~ts ("\"" ^ es ^ "\" expected: ")
893
    in
894
    (n, denominator, s)
895
  in
896
  let rec agentlist es =
897
    let allAgents = CoolUtils.cl_get_agents () in
898
    match Stream.next ts with
899
    | A.Int n -> if CoolUtils.TArray.elem n allAgents
900
                 then n::(agentlist es)
901
                 else A.printError mk_exn ~ts ("agent name \"" ^ (string_of_int n) ^ "\" unknonwn, see --agents: ")
902
    | A.Kwd c when c = es -> []
903
    | _ -> A.printError mk_exn ~ts ("agent name or " ^ es ^ "\" expected: ")
904
  in
905
  match Stream.next ts with
906
  | A.Kwd "true" ->
907
    print_endline "*** Warning: \"true\" used as propositional variable.";
908
    AP "true"
909
  | A.Kwd "false" ->
910
    print_endline "*** Warning: \"false\" used as propositional variable.";
911
    AP "false"
912
  | A.Kwd "True" -> TRUE
913
  | A.Kwd "False" -> FALSE
914
  | A.Ident s ->
915
      (try
916
          let finder (x, _) = compare x s == 0 in
917
          let (_, symbol) = List.find finder symtab in
918
          VAR symbol
919
        with Not_found -> AP s)
920
  | A.Kwd "~" ->
921
      let f = parse_rest symtab ts in
922
      NOT f
923
  | A.Kwd "@" ->
924
      let s =
925
        match Stream.next ts with
926
        | A.Ident s when isNominal s -> s
927
        | t -> A.printError mk_exn ~t ~ts ("nominal expected: ")
928
      in
929
      let f = parse_rest symtab ts in
930
      AT (s, f)
931
  | A.Kwd "<" ->
932
      let (_, _, s) = boxinternals true ">" in
933
      let f1 = parse_rest symtab ts in
934
      EX (s, f1)
935
  | A.Kwd "[" ->
936
      let (_, _, s) = boxinternals true "]" in
937
      let f1 = parse_rest symtab ts in
938
      AX (s, f1)
939
  | A.Kwd "[{" ->
940
      let ls = agentlist "}]" in
941
      let f1 = parse_rest symtab ts in
942
      ENFORCES (ls, f1)
943
  | A.Kwd "<{" ->
944
      let ls = agentlist "}>" in
945
      let f1 = parse_rest symtab ts in
946
      ALLOWS (ls, f1)
947
  | A.Kwd "{>=" ->
948
      let (n, denom, s) = boxinternals false "}" in
949
      let f1 = parse_rest symtab ts in
950
      if (denom <> 0)
951
      then ATLEASTPROB (rational_of_int n denom, f1)
952
      else MIN (n, s, f1)
953
  | A.Kwd "{<=" ->
954
      let (n, denom, s) = boxinternals false "}" in
955
      let f1 = parse_rest symtab ts in
956
      if (denom <> 0)
957
      then A.printError mk_exn ~ts "Can not express {<= probability}"
958
      else MAX (n, s, f1)
959
  | A.Kwd "{<" ->
960
      let (n, denom, s) = boxinternals false "}" in
961
      let f1 = parse_rest symtab ts in
962
      if (denom <> 0)
963
      then LESSPROBFAIL (rational_of_int n denom, NOT f1)
964
      else A.printError mk_exn ~ts "The \"Less than\" < is not implemented yet"
965
  | A.Kwd "=" -> begin
966
          match Stream.next ts with
967
          (* | A.Int s *)
968
          | A.Kwd s
969
          | A.Ident s -> CONST s
970
          | _ -> A.printError mk_exn ~ts "constant = expects an identifier afterwards"
971
    end
972
  | A.Kwd "(" -> begin
973
      let f = parse_formula symtab ts in
974
      match Stream.next ts with
975
      | A.Kwd ")" -> f
976
      | A.Kwd "+" -> begin
977
          let f2 = parse_formula symtab ts in
978
          match Stream.next ts with
979
          | A.Kwd ")" -> CHC (f, f2)
980
          | t -> A.printError mk_exn ~t ~ts "\")\" expected: "
981
        end
982
      | t -> A.printError mk_exn ~t ~ts "\")\" or \"+\" expected: "
983
    end
984
  | A.Kwd "O" ->
985
    let f = parse_rest symtab ts in
986
      ID f
987
  | A.Kwd "[pi1]" ->
988
      let f = parse_rest symtab ts in
989
      FUS (true, f)
990
  | A.Kwd "[pi2]" ->
991
      let f = parse_rest symtab ts in
992
      FUS (false, f)
993
  | A.Kwd "μ" ->
994
      let (_, _, s) = boxinternals true "." in
995
      let symbol = Stream.next gensym in
996
      let newtab = (s, symbol) :: symtab in
997
      let f1 = parse_rest newtab ts in
998
      MU (symbol, f1)
999
  | A.Kwd "ν" ->
1000
      let (_, _, s) = boxinternals true "." in
1001
      let symbol = Stream.next gensym in
1002
      let newtab = (s, symbol) :: symtab in
1003
      let f1 = parse_rest newtab ts in
1004
      NU (symbol, f1)
1005
  | A.Kwd "AF" ->
1006
      let f = parse_rest symtab ts in
1007
      AF f
1008
  | A.Kwd "EF" ->
1009
      let f = parse_rest symtab ts in
1010
      EF f
1011
  | A.Kwd "AG" ->
1012
      let f = parse_rest symtab ts in
1013
      AG f
1014
  | A.Kwd "EG" ->
1015
      let f = parse_rest symtab ts in
1016
      EG f
1017
  | A.Kwd "A" ->
1018
     assert (Stream.next ts = A.Kwd "(");
1019
     let f1 = parse_formula symtab ts in begin
1020
       match Stream.next ts with
1021
       | A.Kwd "U" ->
1022
         let f2 = parse_formula symtab ts in
1023
         assert (Stream.next ts = A.Kwd ")");
1024
         AU (f1, f2)
1025
       | A.Kwd "R" ->
1026
         let f2 = parse_formula symtab ts in
1027
         assert (Stream.next ts = A.Kwd ")");
1028
         AR (f1, f2)
1029
       | A.Kwd "B" ->
1030
         let f2 = parse_formula symtab ts in
1031
         assert (Stream.next ts = A.Kwd ")");
1032
         AR (f2, f1)
1033
       | t -> A.printError mk_exn ~t ~ts "one of \"U\" \"R\" \"B\" expected: "
1034
     end
1035
  | A.Kwd "E" ->
1036
     assert (Stream.next ts = A.Kwd "(");
1037
     let f1 = parse_formula symtab ts in begin
1038
       match Stream.next ts with
1039
       | A.Kwd "U" ->
1040
         let f2 = parse_formula symtab ts in
1041
         assert (Stream.next ts = A.Kwd ")");
1042
         EU (f1, f2)
1043
       | A.Kwd "R" ->
1044
         let f2 = parse_formula symtab ts in
1045
         assert (Stream.next ts = A.Kwd ")");
1046
         ER (f1, f2)
1047
       | A.Kwd "B" ->
1048
         let f2 = parse_formula symtab ts in
1049
         assert (Stream.next ts = A.Kwd ")");
1050
         ER (f2, f1)
1051
       | t -> A.printError mk_exn ~t ~ts "one of \"U\" \"R\" \"B\" expected: "
1052
     end
1053
  | A.Kwd "AX" ->
1054
     let f1 = parse_rest symtab ts in
1055
     AX ("", f1)
1056
  | A.Kwd "EX" ->
1057
     let f1 = parse_rest symtab ts in
1058
     EX ("", f1)
1059
  | t -> A.printError mk_exn ~t ~ts
1060
      "\"<\", \"[\", \"{>=\", \"{<=\", \"@\", \"~\", \"(\",
1061
      \"True\", \"False\", \"=\", \"=o\", \"O\" or <ident> expected: "
1062

    
1063
(** Parses a sorted formula.
1064
    @param ts A token stream.
1065
    @return A sorted formula.
1066
    @raise CoAlgException If ts does not represent a sorted formula.
1067
 *)
1068
let parse_sortedFormula ts =
1069
  let nr =
1070
    match Stream.peek ts with
1071
    | Some (A.Int n) ->
1072
        if n >= 0 then begin
1073
          Stream.junk ts;
1074
          let () =
1075
            match Stream.next ts with
1076
            | A.Kwd ":" -> ()
1077
            | t -> A.printError mk_exn ~t ~ts ("\":\" expected: ")
1078
          in
1079
          n
1080
        end else
1081
          A.printError mk_exn ~ts ("<non-negative number> expected: ")
1082
    | _ -> 0
1083
  in
1084
  let f = parse_formula [] ts in
1085
  (nr, f)
1086

    
1087
(** Parses a list of sorted formulae separated by ";".
1088
    @param ts A token stream.
1089
    @param acc The list of sorted formulae parsed so far.
1090
    @return The resulting list of sorted formula.
1091
    @raise CoAlgException if ts does not represent a list of sorted formulae.
1092
 *)
1093
let rec parse_sortedFormulaList ts acc =
1094
  let f1 = parse_sortedFormula ts in
1095
  match Stream.peek ts with
1096
  | Some (A.Kwd ";") ->
1097
      Stream.junk ts;
1098
      parse_sortedFormulaList ts (f1::acc)
1099
  | _ -> List.rev (f1::acc)
1100

    
1101
(** A common wrapper for import functions.
1102
    @param fkt An import function.
1103
    @param s A string.
1104
    @return The object imported from s using fkt.
1105
    @raise CoAlgException If ts is not empty.
1106
 *)
1107
let importWrapper fkt s =
1108
  let ts = lexer s in
1109
  try
1110
    let res = fkt ts in
1111
    let _ =
1112
      match Stream.peek ts with
1113
      | None -> ()
1114
      | Some _ -> A.printError mk_exn ~ts "EOS expected: "
1115
    in
1116
    res
1117
  with Stream.Failure -> A.printError mk_exn ~ts "unexpected EOS"
1118

    
1119
(** Parses a string to obtain a formula.
1120
    @param s A string representing a formula.
1121
    @return The resulting formula.
1122
    @raise CoAlgException if s does not represent a formula.
1123
 *)
1124
let importFormula s = importWrapper (parse_formula []) s
1125

    
1126
(** Parses a string to obtain a sorted formula.
1127
    @param s A string representing a sorted formula.
1128
    @return The sorted formula.
1129
    @raise CoAlgException If s does not represent a sorted formula.
1130
 *)
1131
let importSortedFormula s = importWrapper parse_sortedFormula s
1132

    
1133
(** Parses a string to obtain a (sorted) formula query.
1134
    @param s A string representing a formula query.
1135
    @return A pair (tbox, f) where
1136
    tbox is a list of sorted formulae representing the TBox; and
1137
    f is a sorted formula.
1138
    @raise CoAlgException if s does not represent a formula query.
1139
 *)
1140
let importQuery s =
1141
  let fkt ts =
1142
    match Stream.peek ts with
1143
    | Some (A.Kwd "|-") ->
1144
        Stream.junk ts;
1145
        let f = parse_sortedFormula ts in
1146
        ([], f)
1147
    | _ ->
1148
        let fl = parse_sortedFormulaList ts [] in
1149
        match Stream.peek ts with
1150
        | Some (A.Kwd "|-") ->
1151
            Stream.junk ts;
1152
            let f = parse_sortedFormula ts in
1153
            (fl, f)
1154
        | _ ->
1155
            if List.length fl = 1 then ([], List.hd fl)
1156
            else A.printError mk_exn ~ts "\"|-\" expected: "
1157
  in
1158
  importWrapper fkt s
1159

    
1160

    
1161
(** Converts the negation of a formula to negation normal form
1162
    by "pushing in" the negations "~".
1163
    The symbols "<=>" and "=>" are substituted by their usual definitions.
1164
    @param f A formula.
1165
    @return A formula in negation normal form and not containing "<=>" or "=>"
1166
    that is equivalent to ~f.
1167
 *)
1168
let rec nnfNeg f =
1169
  match f with
1170
  | TRUE -> FALSE
1171
  | FALSE -> TRUE
1172
  | AP _ -> NOT f
1173
  | VAR _ -> f
1174
  | NOT f1 -> nnf f1
1175
  | AT (s, f1) -> AT (s, nnfNeg f1)
1176
  | OR (f1, f2) -> AND (nnfNeg f1, nnfNeg f2)
1177
  | AND (f1, f2) -> OR (nnfNeg f1, nnfNeg f2)
1178
  | EQU (f1, f2) -> OR (AND (nnf f1, nnfNeg f2), AND (nnf f2, nnfNeg f1))
1179
  | IMP (f1, f2) -> AND (nnf f1, nnfNeg f2)
1180
  | EX (s, f1) -> AX (s, nnfNeg f1)
1181
  | AX (s, f1) -> EX (s, nnfNeg f1)
1182
  | ENFORCES (s, f1) -> ALLOWS (s, nnfNeg f1)
1183
  | ALLOWS (s, f1) -> ENFORCES (s, nnfNeg f1)
1184
  | MIN (n, s, f1) -> if n = 0 then FALSE else MAXEXCEPT (n-1, s, nnfNeg f1)
1185
  | MAX (n, s, f1) -> MORETHAN (n, s, nnf f1)
1186
  | MORETHAN (n, s, f1) -> MAXEXCEPT (n, s, nnfNeg f1)
1187
  | MAXEXCEPT (n, s, f1) -> MORETHAN (n, s, nnfNeg f1)
1188
  | ATLEASTPROB (p, f1) -> LESSPROBFAIL (p, nnfNeg f1)
1189
  | LESSPROBFAIL (p, f1) -> ATLEASTPROB (p, nnfNeg f1)
1190
  | CONST s -> CONSTN s
1191
  | CONSTN s -> CONST s
1192
  | ID (f1) -> ID (nnfNeg f1)
1193
  | NORM(f1, f2) -> NORMN(nnfNeg f1, nnfNeg f2)
1194
  | NORMN(f1, f2) -> NORM (nnfNeg f1, nnfNeg f2)
1195
  | CHC (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2)
1196
  | FUS (first, f1) -> FUS (first, nnfNeg f1)
1197
  | MU (s, f1) -> NU(s, nnfNeg f1)
1198
  | NU (s, f1) -> MU(s, nnfNeg f1)
1199
  | AF _
1200
  | EF _
1201
  | AG _
1202
  | EG _
1203
  | AU _
1204
  | EU _
1205
  | AR _
1206
  | ER _ -> raise (CoAlgException ("nnfNeg: CTL should have been removed at this point"))
1207

    
1208
(** Converts a formula to negation normal form
1209
    by "pushing in" the negations "~".
1210
    The symbols "<=>" and "=>" are substituted by their usual definitions.
1211
    @param f A formula.
1212
    @return A formula in negation normal form and not containing "<=>" or "=>"
1213
    that is equivalent to f.
1214
 *)
1215
and nnf f =
1216
  match f with
1217
  | TRUE
1218
  | FALSE
1219
  | AP _
1220
  | NOT (AP _)
1221
  | CONST _
1222
  | CONSTN _
1223
  | VAR _ -> f
1224
  | NOT f1 -> nnfNeg f1
1225
  | AT (s, f1) ->
1226
      let ft1 = nnf f1 in
1227
      if ft1 == f1 then f else AT (s, ft1)
1228
  | OR (f1, f2) ->
1229
      let ft1 = nnf f1 in
1230
      let ft2 = nnf f2 in
1231
      if ft1 == f1 && ft2 == f2 then f else OR (ft1, ft2)
1232
  | AND (f1, f2) ->
1233
      let ft1 = nnf f1 in
1234
      let ft2 = nnf f2 in
1235
      if ft1 == f1 && ft2 == f2 then f else AND (ft1, ft2)
1236
  | EQU (f1, f2) -> AND (OR (nnfNeg f1, nnf f2), OR (nnfNeg f2, nnf f1))
1237
  | IMP (f1, f2) -> OR (nnfNeg f1, nnf f2)
1238
  | EX (s, f1) ->
1239
      let ft = nnf f1 in
1240
      if ft == f1 then f else EX (s, ft)
1241
  | AX (s, f1) ->
1242
      let ft = nnf f1 in
1243
      if ft == f1 then f else AX (s, ft)
1244
  | ENFORCES (s, f1) ->
1245
      let ft = nnf f1 in
1246
      if ft == f1 then f else ENFORCES (s, ft)
1247
  | ALLOWS (s, f1) ->
1248
      let ft = nnf f1 in
1249
      if ft == f1 then f else ALLOWS (s, ft)
1250
  | MIN (n, s, f1) ->
1251
      if n = 0 then TRUE
1252
      else
1253
        let ft = nnf f1 in
1254
        MORETHAN (n-1,s,ft)
1255
  | MAX (n, s, f1) ->
1256
      let ft = nnfNeg f1 in
1257
      MAXEXCEPT (n,s, ft)
1258
  | MORETHAN (n,s,f1) ->
1259
      let ft = nnf f1 in
1260
      if ft = f1 then f else MORETHAN (n,s,ft)
1261
  | MAXEXCEPT (n,s,f1) ->
1262
      let ft = nnf f1 in
1263
      if ft = f1 then f else MAXEXCEPT (n,s,ft)
1264
  | ATLEASTPROB (p, f1) ->
1265
      let ft = nnf f1 in
1266
      if ft == f1 then f else ATLEASTPROB (p, ft)
1267
  | LESSPROBFAIL (p, f1) ->
1268
      let ft = nnf f1 in
1269
      if ft == f1 then f else LESSPROBFAIL (p, ft)
1270
  | ID (f1) ->
1271
    let ft = nnf f1 in
1272
    if ft == f1 then f else ID(ft)
1273
  | NORM (f1, f2) ->
1274
      let ft1 = nnf f1 in
1275
      let ft2 = nnf f2 in
1276
      if ft1 == f1 && ft2 == f2 then f else NORM (ft1, ft2)
1277
  | NORMN (f1, f2) ->
1278
      let ft1 = nnf f1 in
1279
      let ft2 = nnf f2 in
1280
      if ft1 == f1 && ft2 == f2 then f else NORMN (ft1, ft2)
1281
  | CHC (f1, f2) ->
1282
      let ft1 = nnf f1 in
1283
      let ft2 = nnf f2 in
1284
      if ft1 == f1 && ft2 == f2 then f else CHC (ft1, ft2)
1285
  | FUS (first, f1) ->
1286
      let ft = nnf f1 in
1287
      if ft == f1 then f else FUS (first, ft)
1288
  | MU (s, f1) ->
1289
      let ft = nnf f1 in
1290
      if ft == f1 then f else MU (s, ft)
1291
  | NU (s, f1) ->
1292
      let ft = nnf f1 in
1293
      if ft == f1 then f else NU (s, ft)
1294
  | AF _
1295
  | EF _
1296
  | AG _
1297
  | EG _
1298
  | AU _
1299
  | EU _
1300
  | AR _
1301
  | ER _ -> raise (CoAlgException ("nnf: CTL should have been removed at this point"))
1302

    
1303
(** Simplifies a formula.
1304
    @param f A formula which must be in negation normal form.
1305
    @return A formula in negation normal form that is equivalent to f.
1306
    @raise CoAlgException if f is not in negation normal form.
1307
 *)
1308
let rec simplify f =
1309
  match f with
1310
  | TRUE
1311
  | FALSE
1312
  | AP _
1313
  | NOT (AP _)
1314
  | VAR _
1315
  | NOT (VAR _) -> f
1316
  | AT (s, f1) ->
1317
      let ft = simplify f1 in
1318
      begin
1319
        match ft with
1320
        | FALSE -> FALSE
1321
        | TRUE -> TRUE
1322
        | AT _ -> ft
1323
        | AP s1 when s = s1 -> TRUE
1324
        | NOT (AP s1) when s = s1 -> FALSE
1325
        | _ -> if ft == f1 then f else AT (s, ft)
1326
      end
1327
  | OR (f1, f2) ->
1328
      let ft1 = simplify f1 in
1329
      let ft2 = simplify f2 in
1330
      begin
1331
        match ft1, ft2 with
1332
        | TRUE, _ -> TRUE
1333
        | FALSE, _ -> ft2
1334
        | _, TRUE -> TRUE
1335
        | _, FALSE -> ft1
1336
        | _, _ ->
1337
            if (f1 == ft1) && (f2 == ft2) then f
1338
            else OR (ft1, ft2)
1339
      end
1340
  | AND (f1, f2) ->
1341
      let ft1 = simplify f1 in
1342
      let ft2 = simplify f2 in
1343
      begin
1344
        match ft1, ft2 with
1345
        | TRUE, _ -> ft2
1346
        | FALSE, _ -> FALSE
1347
        | _, TRUE -> ft1
1348
        | _, FALSE -> FALSE
1349
        | _, _ ->
1350
            if (f1 == ft1) && (f2 == ft2) then f
1351
            else AND (ft1, ft2)
1352
      end
1353
  | NOT _
1354
  | EQU _
1355
  | IMP _ -> raise (CoAlgException "Formula is not in negation normal form.")
1356
  | EX (s, f1) ->
1357
      let ft = simplify f1 in
1358
      begin
1359
        match ft with
1360
        | FALSE -> FALSE
1361
        | _ -> if ft == f1 then f else EX (s, ft)
1362
      end
1363
  | AX (s, f1) ->
1364
      let ft = simplify f1 in
1365
      begin
1366
        match ft with
1367
        | TRUE -> TRUE
1368
        | _ -> if ft == f1 then f else AX (s, ft)
1369
      end
1370
  | ENFORCES (s, f1) ->
1371
      let ft = simplify f1 in
1372
      begin
1373
        match ft with
1374
        (* Simplification rules are checked with dirks Generic.hs
1375
        let enforce ls = M (C ls)
1376
        let allow   ls = Neg . M (C ls) . Neg
1377
        provable $ F <-> enforce [1,2] F
1378
        *)
1379
        | TRUE -> TRUE
1380
        | FALSE -> FALSE
1381
        | _ -> if ft == f1 then f else ENFORCES (s, ft)
1382
      end
1383
  | ALLOWS (s, f1) ->
1384
      let ft = simplify f1 in
1385
      begin
1386
        match ft with
1387
        (* Simplification rules are checked with dirks Generic.hs
1388
        let enforce ls = M (C ls)
1389
        let allow   ls = Neg . M (C ls) . Neg
1390
        provable $ F <-> enforce [1,2] F
1391
        *)
1392
        | TRUE -> TRUE
1393
        | FALSE -> FALSE
1394
        | _ -> if ft == f1 then f else ALLOWS (s, ft)
1395
      end
1396
  | MIN (n, s, f1) ->
1397
      if n = 0 then TRUE
1398
      else
1399
        let ft = simplify f1 in
1400
        begin
1401
          match ft with
1402
          | FALSE -> FALSE
1403
          | _ -> if ft == f1 then f else MIN (n, s, ft)
1404
        end
1405
  | MORETHAN (n,s,f1) ->
1406
      let ft = simplify f1 in
1407
      if ft == f1 then f else MORETHAN (n,s,ft)
1408
  | MAXEXCEPT (n,s,f1) ->
1409
      let ft = simplify f1 in
1410
      if ft == f1 then f else MAXEXCEPT (n,s,ft)
1411
  | MAX (n, s, f1) ->
1412
      let ft = simplify f1 in
1413
      begin
1414
        match ft with
1415
        | FALSE -> TRUE
1416
        | _ -> if ft == f1 then f else MAX (n, s, ft)
1417
      end
1418
  | LESSPROBFAIL (p,f1) ->
1419
      let ft1 = simplify f1 in
1420
      if (ft1 == f1) then f else LESSPROBFAIL (p,ft1)
1421
  | ATLEASTPROB (p,f1) ->
1422
      let ft1 = simplify f1 in
1423
      if (ft1 == f1) then f else ATLEASTPROB (p,ft1)
1424
  | CONST _
1425
  | CONSTN _ -> f (* no simplifications possible *)
1426
  | ID (f1) ->
1427
    let ft1 = simplify f1 in
1428
    begin
1429
      match ft1 with
1430
        | TRUE -> TRUE
1431
        | FALSE -> FALSE
1432
        | _ -> if (ft1 == f1) then f else ID (ft1)
1433
    end
1434
  (* todo: more simplifications for KLM? *)
1435
  | NORM (f1, f2) ->
1436
      let ft1 = simplify f1 in
1437
      let ft2 = simplify f2 in
1438
      begin
1439
        match ft2 with
1440
          | TRUE -> TRUE
1441
          | _ ->
1442
            if (f1 == ft1) && (f2 == ft2) then f
1443
            else NORM (ft1, ft2)
1444
      end
1445
  | NORMN (f1, f2) ->
1446
      let ft1 = simplify f1 in
1447
      let ft2 = simplify f2 in
1448
      begin
1449
        match ft2 with
1450
          | FALSE -> FALSE
1451
          | _ ->
1452
            if (f1 == ft1) && (f2 == ft2) then f
1453
            else NORMN (ft1, ft2)
1454
      end
1455
  | CHC (f1, f2) ->
1456
      let ft1 = simplify f1 in
1457
      let ft2 = simplify f2 in
1458
      begin
1459
        match ft1, ft2 with
1460
        | TRUE, TRUE -> TRUE
1461
        | FALSE, FALSE -> FALSE
1462
        | _, _ ->
1463
            if (f1 == ft1) && (f2 == ft2) then f
1464
            else CHC (ft1, ft2)
1465
      end
1466
  | FUS (first, f1) ->
1467
      let ft = simplify f1 in
1468
      begin
1469
        match ft with
1470
        | FALSE -> FALSE
1471
        | TRUE -> TRUE
1472
        | _ -> if ft == f1 then f else FUS (first, ft)
1473
      end
1474
  | MU (s, f1) ->
1475
      let ft = simplify f1 in
1476
      begin
1477
        match ft with
1478
        | TRUE -> TRUE
1479
        | _ -> if ft == f1 then f else MU (s, ft)
1480
      end
1481
  | NU (s, f1) ->
1482
      let ft = simplify f1 in
1483
      begin
1484
        match ft with
1485
        | TRUE -> TRUE
1486
        | _ -> if ft == f1 then f else NU (s, ft)
1487
      end
1488
  | AF _
1489
  | EF _
1490
  | AG _
1491
  | EG _
1492
  | AU _
1493
  | EU _
1494
  | AR _
1495
  | ER _ ->
1496
     raise (CoAlgException ("nnf: CTL should have been removed at this point"))
1497

    
1498
(** Destructs an atomic proposition.
1499
    @param f An atomic proposition.
1500
    @return The name of the atomic proposition.
1501
    @raise CoAlgException if f is not an atomic proposition.
1502
 *)
1503
let dest_ap f =
1504
  match f with
1505
  | AP s when not (isNominal s) -> s
1506
  | _ -> raise (CoAlgException "Formula is not an atomic proposition.")
1507

    
1508
(** Destructs a nominal.
1509
    @param f A nominal.
1510
    @return The name of the nominal
1511
    @raise CoAlgException if f is not a nominal.
1512
 *)
1513
let dest_nom f =
1514
  match f with
1515
  | AP s when isNominal s -> s
1516
  | _ -> raise (CoAlgException "Formula is not a nominal.")
1517

    
1518
(** Destructs a negation.
1519
    @param f A negation.
1520
    @return The immediate subformula of the negation.
1521
    @raise CoAlgException if f is not a negation.
1522
 *)
1523
let dest_not f =
1524
  match f with
1525
  | NOT f1 -> f1
1526
  | _ -> raise (CoAlgException "Formula is not a negation.")
1527

    
1528
(** Destructs an @-formula.
1529
    @param f An @-formula.
1530
    @return The name of the nominal and the immediate subformula of the @-formula.
1531
    @raise CoAlgException if f is not an @-formula.
1532
 *)
1533
let dest_at f =
1534
  match f with
1535
  | AT (s, f1) -> (s, f1)
1536
  | _ -> raise (CoAlgException "Formula is not an @-formula.")
1537

    
1538
(** Destructs an or-formula.
1539
    @param f An or-formula.
1540
    @return The two immediate subformulae of the or-formula.
1541
    @raise CoAlgException if f is not an or-formula.
1542
 *)
1543
let dest_or f =
1544
  match f with
1545
  | OR (f1, f2) -> (f1, f2)
1546
  | _ -> raise (CoAlgException "Formula is not an or-formula.")
1547

    
1548
(** Destructs an and-formula.
1549
    @param f An and-formula.
1550
    @return The two immediate subformulae of the and-formula.
1551
    @raise CoAlgException if f is not an and-formula.
1552
 *)
1553
let dest_and f =
1554
  match f with
1555
  | AND (f1, f2) -> (f1, f2)
1556
  | _ -> raise (CoAlgException "Formula is not an and-formula.")
1557

    
1558
(** Destructs an equivalence.
1559
    @param f An equivalence.
1560
    @return The two immediate subformulae of the equivalence.
1561
    @raise CoAlgException if f is not an equivalence.
1562
 *)
1563
let dest_equ f =
1564
  match f with
1565
  | EQU (f1, f2) -> (f1, f2)
1566
  | _ -> raise (CoAlgException "Formula is not an equivalence.")
1567

    
1568
(** Destructs an implication.
1569
    @param f An implication.
1570
    @return The two immediate subformulae of the implication.
1571
    @raise CoAlgException if f is not an implication.
1572
 *)
1573
let dest_imp f =
1574
  match f with
1575
  | IMP (f1, f2) -> (f1, f2)
1576
  | _ -> raise (CoAlgException "Formula is not an implication.")
1577

    
1578
(** Destructs an EX-formula.
1579
    @param f An EX-formula.
1580
    @return The role name and the immediate subformula of the EX-formula.
1581
    @raise CoAlgException if f is not an EX-formula.
1582
 *)
1583
let dest_ex f =
1584
  match f with
1585
  | EX (s, f1) -> (s, f1)
1586
  | _ -> raise (CoAlgException "Formula is not an EX-formula.")
1587

    
1588
(** Destructs an AX-formula.
1589
    @param f An AX-formula.
1590
    @return The role name and the immediate subformula of the AX-formula.
1591
    @raise CoAlgException if f is not an AX-formula.
1592
 *)
1593
let dest_ax f =
1594
  match f with
1595
  | AX (s, f1) -> (s, f1)
1596
  | _ -> raise (CoAlgException "Formula is not an AX-formula.")
1597

    
1598
(** Destructs a MIN-formula.
1599
    @param f A MIN-formula.
1600
    @return The number restriction, role name,
1601
    and the immediate subformula of the MIN-formula.
1602
    @raise CoAlgException if f is not a MIN-formula.
1603
 *)
1604
let dest_min f =
1605
  match f with
1606
  | MIN (n, s, f1) -> (n, s, f1)
1607
  | _ -> raise (CoAlgException "Formula is not a MIN-formula.")
1608

    
1609
(** Destructs a MAX-formula.
1610
    @param f A MAX-formula.
1611
    @return The number restriction, role name,
1612
    and the immediate subformula of the MAX-formula.
1613
    @raise CoAlgException if f is not a MAX-formula.
1614
 *)
1615
let dest_max f =
1616
  match f with
1617
  | MAX (n, s, f1) -> (n, s, f1)
1618
  | _ -> raise (CoAlgException "Formula is not a MAX-formula.")
1619

    
1620
(** Destructs a choice formula.
1621
    @param f A choice formula.
1622
    @return The two immediate subformulae of the choice formula.
1623
    @raise CoAlgException if f is not a choice formula.
1624
 *)
1625
let dest_choice f =
1626
  match f with
1627
  | CHC (f1, f2) -> (f1, f2)
1628
  | _ -> raise (CoAlgException "Formula is not a choice formula.")
1629

    
1630
(** Destructs a fusion formula.
1631
    @param f A fusion formula.
1632
    @return A pair (first, f1) where
1633
    first is true iff f is a first projection; and
1634
    f1 is the immediate subformulae of f.
1635
    @raise CoAlgException if f is not a fusion formula.
1636
 *)
1637
let dest_fusion f =
1638
  match f with
1639
  | FUS (first, f1) -> (first, f1)
1640
  | _ -> raise (CoAlgException "Formula is not a fusion formula.")
1641

    
1642

    
1643
(** Tests whether a formula is the constant True.
1644
    @param f A formula.
1645
    @return True iff f is the constant True.
1646
 *)
1647
let is_true f =
1648
  match f with
1649
  | TRUE -> true
1650
  | _ -> false
1651

    
1652
(** Tests whether a formula is the constant False.
1653
    @param f A formula.
1654
    @return True iff f is the constant False.
1655
 *)
1656
let is_false f =
1657
  match f with
1658
  | FALSE -> true
1659
  | _ -> false
1660

    
1661
(** Tests whether a formula is an atomic proposition.
1662
    @param f A formula.
1663
    @return True iff f is an atomic proposition.
1664
 *)
1665
let is_ap f =
1666
  match f with
1667
  | AP s when not (isNominal s) -> true
1668
  | _ -> false
1669

    
1670
(** Tests whether a formula is a nominal.
1671
    @param f A formula.
1672
    @return True iff f is a nominal.
1673
 *)
1674
let is_nom f =
1675
  match f with
1676
  | AP s when isNominal s -> true
1677
  | _ -> false
1678

    
1679
(** Tests whether a formula is a negation.
1680
    @param f A formula.
1681
    @return True iff f is a negation.
1682
 *)
1683
let is_not f =
1684
  match f with
1685
  | NOT _ -> true
1686
  | _ -> false
1687

    
1688
(** Tests whether a formula is an @-formula.
1689
    @param f A formula.
1690
    @return True iff f is an @-formula.
1691
 *)
1692
let is_at f =
1693
  match f with
1694
  | AT _ -> true
1695
  | _ -> false
1696

    
1697
(** Tests whether a formula is an or-formula.
1698
    @param f A formula.
1699
    @return True iff f is an or-formula.
1700
 *)
1701
let is_or f =
1702
  match f with
1703
  | OR _ -> true
1704
  | _ -> false
1705

    
1706
(** Tests whether a formula is an and-formula.
1707
    @param f A formula.
1708
    @return True iff f is an and-formula.
1709
 *)
1710
let is_and f =
1711
  match f with
1712
  | AND _ -> true
1713
  | _ -> false
1714

    
1715
(** Tests whether a formula is an equivalence.
1716
    @param f A formula.
1717
    @return True iff f is an equivalence.
1718
 *)
1719
let is_equ f =
1720
  match f with
1721
  | EQU _ -> true
1722
  | _ -> false
1723

    
1724
(** Tests whether a formula is an implication.
1725
    @param f A formula.
1726
    @return True iff f is an implication.
1727
 *)
1728
let is_imp f =
1729
  match f with
1730
  | IMP _ -> true
1731
  | _ -> false
1732

    
1733
(** Tests whether a formula is an EX-formula.
1734
    @param f A formula.
1735
    @return True iff f is an EX-formula.
1736
 *)
1737
let is_ex f =
1738
  match f with
1739
  | EX _ -> true
1740
  | _ -> false
1741

    
1742
(** Tests whether a formula is an AX-formula.
1743
    @param f A formula.
1744
    @return True iff f is an AX-formula.
1745
 *)
1746
let is_ax f =
1747
  match f with
1748
  | AX _ -> true
1749
  | _ -> false
1750

    
1751
(** Tests whether a formula is a MIN-formula.
1752
    @param f A formula.
1753
    @return True iff f is a MIN-formula.
1754
 *)
1755
let is_min f =
1756
  match f with
1757
  | MIN _ -> true
1758
  | _ -> false
1759

    
1760
(** Tests whether a formula is a MAX-formula.
1761
    @param f A formula.
1762
    @return True iff f is a MAX-formula.
1763
 *)
1764
let is_max f =
1765
  match f with
1766
  | MAX _ -> true
1767
  | _ -> false
1768

    
1769
(** Tests whether a formula is a choice formula.
1770
    @param f A formula.
1771
    @return True iff f is a choice formula.
1772
 *)
1773
let is_choice f =
1774
  match f with
1775
  | CHC _ -> true
1776
  | _ -> false
1777

    
1778
(** Tests whether a formula is a fusion formula.
1779
    @param f A formula.
1780
    @return True iff f is a fusion formula.
1781
 *)
1782
let is_fusion f =
1783
  match f with
1784
  | FUS _ -> true
1785
  | _ -> false
1786

    
1787

    
1788
(** The constant True.
1789
 *)
1790
let const_true = TRUE
1791

    
1792
(** The constant False.
1793
 *)
1794
let const_false = FALSE
1795

    
1796
(** Constructs an atomic proposition.
1797
    @param s The name of the atomic proposition.
1798
    @return The atomic proposition with name s.
1799
    @raise CoAlgException if s is a nominal name.
1800
 *)
1801
let const_ap s =
1802
  if isNominal s then raise (CoAlgException "The name indicates a nominal.")
1803
  else AP s
1804

    
1805
(** Constructs a nominal.
1806
    @param s The name of the nominal.
1807
    @return A nominal with name s.
1808
    @raise CoAlgException if s is not a nominal name.
1809
 *)
1810
let const_nom s =
1811
  if isNominal s then AP s
1812
  else raise (CoAlgException "The name does not indicate a nominal.")
1813

    
1814
(** Negates a formula.
1815
    @param f A formula.
1816
    @return The negation of f.
1817
 *)
1818
let const_not f = NOT f
1819

    
1820
(** Constructs an @-formula from a name and a formula.
1821
    @param s A nominal name.
1822
    @param f A formula.
1823
    @return The formula AT (s, f).
1824
 *)
1825
let const_at s f = AT (s, f)
1826

    
1827
(** Constructs an or-formula from two formulae.
1828
    @param f1 The first formula (LHS).
1829
    @param f2 The second formula (LHS).
1830
    @return The formula f1 | f2.
1831
 *)
1832
let const_or f1 f2 = OR (f1, f2)
1833

    
1834
(** Constructs an and-formula from two formulae.
1835
    @param f1 The first formula (LHS).
1836
    @param f2 The second formula (LHS).
1837
    @return The formula f1 & f2.
1838
 *)
1839
let const_and f1 f2 = AND (f1, f2)
1840

    
1841
(** Constructs an equivalence from two formulae.
1842
    @param f1 The first formula (LHS).
1843
    @param f2 The second formula (LHS).
1844
    @return The equivalence f1 <=> f2.
1845
 *)
1846
let const_equ f1 f2 = EQU (f1, f2)
1847

    
1848
(** Constructs an implication from two formulae.
1849
    @param f1 The first formula (LHS).
1850
    @param f2 The second formula (LHS).
1851
    @return The implication f1 => f2.
1852
 *)
1853
let const_imp f1 f2 = IMP (f1, f2)
1854

    
1855
(** Constructs an EX-formula from a formula.
1856
    @param s A role name.
1857
    @param f A formula.
1858
    @return The formula EX (s, f).
1859
 *)
1860
let const_ex s f = EX (s, f)
1861

    
1862
(** Constructs an AX-formula from a formula.
1863
    @param s A role name.
1864
    @param f A formula.
1865
    @return The formula AX (s, f).
1866
 *)
1867
let const_ax s f = AX (s, f)
1868

    
1869
(** Constructs a MIN-formula from a formula.
1870
    @param n A non-negative integer.
1871
    @param s A role name.
1872
    @param f A formula.
1873
    @return The formula MIN f.
1874
    @raise CoAlgException Iff n is negative.
1875
 *)
1876
let const_min n s f =
1877
  if n < 0 then raise (CoAlgException "Negative cardinality constraint.")
1878
  else MIN (n, s, f)
1879

    
1880
(** Constructs a MAX-formula from a formula.
1881
    @param n A non-negative integer.
1882
    @param s A role name.
1883
    @param f A formula.
1884
    @return The formula MAX f.
1885
    @raise CoAlgException Iff n is negative.
1886
 *)
1887
let const_max n s f =
1888
  if n < 0 then raise (CoAlgException "Negative cardinality constraint.")
1889
  else MAX (n, s, f)
1890

    
1891
let const_enforces p f =
1892
    ENFORCES (p,f)
1893

    
1894
let const_allows p f =
1895
    ALLOWS (p,f)
1896

    
1897
(** Constructs a choice formula from two formulae.
1898
    @param f1 The first formula (LHS).
1899
    @param f2 The second formula (LHS).
1900
    @return The formula (f1 + f2).
1901
 *)
1902
let const_choice f1 f2 = CHC (f1, f2)
1903

    
1904
(** Constructs a fusion formula.
1905
    @param first True iff the result is a first projection.
1906
    @param f1 A formula.
1907
    @return The formula [pi1] f1 or [pi2] f1 (depending on first).
1908
 *)
1909
let const_fusion first f1 = FUS (first, f1)
1910

    
1911

    
1912
(** Hash-consed formulae, which are in negation normal form,
1913
    such that structural and physical equality coincide.
1914

    
1915
    Also CTL has been replaced by the equivalent μ-Calculus
1916
    constructs
1917
 *)
1918
type hcFormula = (hcFormula_node, formula) HC.hash_consed
1919
and hcFormula_node =
1920
  | HCTRUE
1921
  | HCFALSE
1922
  | HCAP of string
1923
  | HCNOT of string
1924
  | HCAT of string * hcFormula
1925
  | HCOR of hcFormula * hcFormula
1926
  | HCAND of hcFormula * hcFormula
1927
  | HCEX of string * hcFormula
1928
  | HCAX of string * hcFormula
1929
  | HCENFORCES of int list * hcFormula
1930
  | HCALLOWS of int list * hcFormula
1931
  | HCMORETHAN of int * string * hcFormula (* GML Diamond *)
1932
  | HCMAXEXCEPT of int * string * hcFormula (* GML Box *)
1933
  | HCATLEASTPROB of rational * hcFormula
1934
  | HCLESSPROBFAIL of rational * hcFormula
1935
  | HCCONST of string
1936
  | HCCONSTN of string
1937
  | HCID of hcFormula
1938
  | HCNORM of hcFormula * hcFormula
1939
  | HCNORMN of hcFormula * hcFormula
1940
  | HCCHC of hcFormula * hcFormula
1941
  | HCFUS of bool * hcFormula
1942
  | HCMU of string * hcFormula
1943
  | HCNU of string * hcFormula
1944
  | HCVAR of string
1945

    
1946
(** Determines whether two formula nodes are structurally equal.
1947
    @param f1 The first formula node.
1948
    @param f2 The second formula node.
1949
    @return True iff f1 and f2 are structurally equal.
1950
 *)
1951
let equal_hcFormula_node f1 f2 =
1952
  match f1, f2 with
1953
  | HCTRUE, HCTRUE -> true
1954
  | HCFALSE, HCFALSE -> true
1955
  | HCCONST s1, HCCONST s2
1956
  | HCCONSTN s1, HCCONSTN s2
1957
  | HCAP s1, HCAP s2
1958
  | HCNOT s1, HCNOT s2 -> compare s1 s2 = 0
1959
  | HCAT (s1, f1), HCAT (s2, f2) -> compare s1 s2 = 0 && f1 == f2
1960
  | HCOR (f1a, f1b), HCOR (f2a, f2b)
1961
  | HCAND (f1a, f1b), HCAND (f2a, f2b) -> f1a == f2a && f1b == f2b
1962
  | HCEX (s1, f1), HCEX (s2, f2)
1963
  | HCAX (s1, f1), HCAX (s2, f2) -> compare s1 s2 = 0 && f1 == f2
1964
  | HCENFORCES (s1, f1), HCENFORCES (s2, f2)
1965
  | HCALLOWS (s1, f1), HCALLOWS (s2, f2) -> compare s1 s2 = 0 && f1 == f2
1966
  | HCMORETHAN (n1, s1, f1), HCMORETHAN (n2, s2, f2)
1967
  | HCMAXEXCEPT (n1, s1, f1), HCMAXEXCEPT (n2, s2, f2) ->
1968
      n1 = n2 && compare s1 s2 = 0 && f1 == f2
1969
  | HCATLEASTPROB (p1, f1), HCATLEASTPROB (p2,f2) ->
1970
      p1 = p2 && f1 == f2
1971
  | HCLESSPROBFAIL (p1, f1), HCLESSPROBFAIL (p2,f2) ->
1972
      p1 = p2 && f1 == f2
1973
  | HCID f1, HCID f2 -> f1 == f2
1974
  | HCNORM (f1a, f1b), HCNORMN (f2a, f2b) -> f1a == f2a && f1b == f2b
1975
  | HCCHC (f1a, f1b), HCCHC (f2a, f2b) -> f1a == f2a && f1b == f2b
1976
  | HCFUS (first1, f1), HCFUS (first2, f2) -> first1 = first2 && f1 == f2
1977
  | HCMU (name1, f1), HCMU(name2, f2) -> compare name1 name2 = 0 && f1 == f2
1978
  | HCNU (name1, f1), HCNU(name2, f2) -> compare name1 name2 = 0 && f1 == f2
1979
  | HCVAR name1, HCVAR name2 -> compare name1 name2 = 0
1980
(* The rest could be shortened to | _ -> false,
1981
   but then the compiler would not warn if the formula type is extended
1982
   and this function is not updated accordingly.*)
1983
  | HCTRUE, _
1984
  | HCFALSE, _
1985
  | HCAP _, _
1986
  | HCNOT _, _
1987
  | HCAT _, _
1988
  | HCOR _, _
1989
  | HCAND _, _
1990
  | HCEX _, _
1991
  | HCAX _, _
1992
  | HCENFORCES _, _
1993
  | HCALLOWS   _, _
1994
  | HCMORETHAN _, _
1995
  | HCMAXEXCEPT _, _
1996
  | HCATLEASTPROB _, _
1997
  | HCLESSPROBFAIL _, _
1998
  | HCCONST _, _
1999
  | HCCONSTN _, _
2000
  | HCID _, _
2001
  | HCNORM _, _
2002
  | HCNORMN _, _
2003
  | HCCHC _, _
2004
  | HCFUS _, _
2005
  | HCMU _, _
2006
  | HCNU _, _
2007
  | HCVAR _, _ -> false
2008

    
2009
(** Computes the hash value of a formula node.
2010
    @param f A formula node.
2011
    @return The hash value of f.
2012
 *)
2013
let hash_hcFormula_node f =
2014
  let base = 23 in (* should be larger than the no of constructors *)
2015
  match f with
2016
  | HCTRUE -> 0
2017
  | HCFALSE -> 1
2018
  | HCAP s
2019
  | HCNOT s
2020
  | HCVAR s -> base * Hashtbl.hash s + 1
2021
  | HCAT (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 2
2022
  | HCOR (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 5
2023
  | HCAND (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 6
2024
  | HCEX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 3
2025
  | HCAX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 4
2026
  | HCMORETHAN (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 7
2027
  | HCMAXEXCEPT (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 8
2028
  | HCATLEASTPROB (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 9
2029
  | HCLESSPROBFAIL (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 10
2030
  | HCCHC (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 11
2031
  | HCFUS (first, f1) -> base * (base * (Hashtbl.hash first) + f1.HC.hkey) + 13
2032
  | HCENFORCES (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 14
2033
  | HCALLOWS   (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 15
2034
  | HCCONST s -> Hashtbl.hash s + 16
2035
  | HCCONSTN s -> Hashtbl.hash s + 17
2036
  | HCNORM (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 18
2037
  | HCNORMN (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 19
2038
  | HCID (f1) -> base * f1.HC.hkey + 20
2039
  | HCMU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 21
2040
  | HCNU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 22
2041

    
2042
(** Determines the "real" formula of a formula node.
2043
    @param f A formula node.
2044
    @return The formula (in negation normal form) which corresponds to f.
2045
 *)
2046
let toFml_hcFormula_node f =
2047
  match f with
2048
  | HCTRUE -> TRUE
2049
  | HCFALSE -> FALSE
2050
  | HCAP s -> AP s
2051
  | HCVAR s -> VAR s
2052
  | HCNOT s -> NOT (AP s)
2053
  | HCAT (s, f1) -> AT (s, f1.HC.fml)
2054
  | HCOR (f1, f2) -> OR (f1.HC.fml, f2.HC.fml)
2055
  | HCAND (f1, f2) -> AND (f1.HC.fml, f2.HC.fml)
2056
  | HCEX (s, f1) -> EX (s, f1.HC.fml)
2057
  | HCAX (s, f1) -> AX (s, f1.HC.fml)
2058
  | HCENFORCES (s, f1) -> ENFORCES (s, f1.HC.fml)
2059
  | HCALLOWS (s, f1) -> ALLOWS (s, f1.HC.fml)
2060
  | HCMORETHAN (n, s, f1) -> MORETHAN (n, s, f1.HC.fml)
2061
  | HCMAXEXCEPT (n, s, f1) -> MAXEXCEPT (n, s, f1.HC.fml)
2062
  | HCATLEASTPROB (p, f1) -> ATLEASTPROB (p, f1.HC.fml)
2063
  | HCLESSPROBFAIL (p, f1) -> LESSPROBFAIL (p, f1.HC.fml)
2064
  | HCCONST s -> CONST s
2065
  | HCCONSTN s -> CONSTN s
2066
  | HCID (f1) -> ID(f1.HC.fml)
2067
  | HCNORM (f1, f2) -> NORM(f1.HC.fml, f2.HC.fml)
2068
  | HCNORMN (f1, f2) -> NORMN(f1.HC.fml, f2.HC.fml)
2069
  | HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml)
2070
  | HCFUS (first, f1) -> FUS (first, f1.HC.fml)
2071
  | HCMU (var, f1) -> MU (var, f1.HC.fml)
2072
  | HCNU (var, f1) -> NU (var, f1.HC.fml)
2073

    
2074
(** Determines the negation (in negation normal form) of a formula node.
2075
    @param f A formula node.
2076
    @return The negation (in negation normal form) of f.
2077
 *)
2078
let negNde_hcFormula_node f =
2079
  match f with
2080
  | HCTRUE -> HCFALSE
2081
  | HCFALSE -> HCTRUE
2082
  | HCAP s -> HCNOT s
2083
  | HCNOT s -> HCAP s
2084
  | HCVAR s -> f
2085
  | HCAT (s, f1) -> HCAT (s, f1.HC.neg)
2086
  | HCOR (f1, f2) -> HCAND (f1.HC.neg, f2.HC.neg)
2087
  | HCAND (f1, f2) -> HCOR (f1.HC.neg, f2.HC.neg)
2088
  | HCEX (s, f2) -> HCAX (s, f2.HC.neg)
2089
  | HCAX (s, f2) -> HCEX (s, f2.HC.neg)
2090
  | HCENFORCES (s, f2) -> HCALLOWS (s, f2.HC.neg)
2091
  | HCALLOWS (s, f2) -> HCENFORCES (s, f2.HC.neg)
2092
  | HCMORETHAN (n, s, f1) -> HCMAXEXCEPT (n, s, f1.HC.neg)
2093
  | HCMAXEXCEPT (n, s, f1) -> HCMORETHAN (n, s, f1.HC.neg)
2094
  | HCATLEASTPROB (p, f1) -> HCLESSPROBFAIL (p, f1.HC.neg)
2095
  | HCLESSPROBFAIL (p, f1) -> HCATLEASTPROB (p, f1.HC.neg)
2096
  | HCCONST s -> HCCONSTN s
2097
  | HCCONSTN s -> HCCONST s
2098
  | HCID (f1) -> HCID(f1.HC.neg)
2099
  | HCNORM (f1, f2) -> HCNORMN(f1.HC.neg, f2.HC.neg)
2100
  | HCNORMN (f1, f2) -> HCNORM(f1.HC.neg, f2.HC.neg)
2101
  | HCCHC (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg)
2102
  | HCFUS (first, f1) -> HCFUS (first, f1.HC.neg)
2103
  | HCMU (name, f1) -> HCNU (name, f1.HC.neg)
2104
  | HCNU (name, f1) -> HCMU (name, f1.HC.neg)
2105

    
2106
(** An instantiation of hash-consing for formulae.
2107
 *)
2108
module HcFormula = HC.Make(
2109
  struct
2110
    type nde = hcFormula_node
2111
    type fml = formula
2112
    let equal (n1 : nde) n2 = equal_hcFormula_node n1 n2
2113
    let hash (n : nde) = hash_hcFormula_node n
2114
    let negNde (n : nde) = negNde_hcFormula_node n
2115
    let toFml (n : nde) = toFml_hcFormula_node n
2116
  end
2117
 )
2118

    
2119
(** Converts a formula into its hash-consed version.
2120
    @param hcF A hash-cons table for formulae.
2121
    @param f A formula in negation normal form.
2122
    @return The hash-consed version of f.
2123
    @raise CoAlgException if f is not in negation normal form.
2124
*)
2125
let rec hc_formula hcF f =
2126
  match f with
2127
  | TRUE -> HcFormula.hashcons hcF HCTRUE
2128
  | FALSE -> HcFormula.hashcons hcF HCFALSE
2129
  | AP s -> HcFormula.hashcons hcF (HCAP s)
2130
  | VAR s -> HcFormula.hashcons hcF (HCVAR s)
2131
  | NOT (AP s) -> HcFormula.hashcons hcF (HCNOT s)
2132
  | AT (s, f1) ->
2133
      let tf1 = hc_formula hcF f1 in
2134
      HcFormula.hashcons hcF (HCAT (s, tf1))
2135
  | OR (f1, f2) ->
2136
      let tf1 = hc_formula hcF f1 in
2137
      let tf2 = hc_formula hcF f2 in
2138
      HcFormula.hashcons hcF (HCOR (tf1, tf2))
2139
  | AND (f1, f2) ->
2140
      let tf1 = hc_formula hcF f1 in
2141
      let tf2 = hc_formula hcF f2 in
2142
      HcFormula.hashcons hcF (HCAND (tf1, tf2))
2143
  | NOT _
2144
  | EQU _
2145
  | MIN _
2146
  | MAX _
2147
  | IMP _ -> raise (CoAlgException "Formula is not in negation normal form.")
2148
  | EX (s, f1) ->
2149
      let tf1 = hc_formula hcF f1 in
2150
      HcFormula.hashcons hcF (HCEX (s, tf1))
2151
  | AX (s, f1) ->
2152
      let tf1 = hc_formula hcF f1 in
2153
      HcFormula.hashcons hcF (HCAX (s, tf1))
2154
  | ENFORCES (s, f1) ->
2155
      let tf1 = hc_formula hcF f1 in
2156
      HcFormula.hashcons hcF (HCENFORCES (s, tf1))
2157
  | ALLOWS (s, f1) ->
2158
      let tf1 = hc_formula hcF f1 in
2159
      HcFormula.hashcons hcF (HCALLOWS (s, tf1))
2160
  | MORETHAN  (n, s, f1) ->
2161
      let tf1 = hc_formula hcF f1 in
2162
      HcFormula.hashcons hcF (HCMORETHAN (n, s, tf1))
2163
  | MAXEXCEPT  (n, s, f1) ->
2164
      let tf1 = hc_formula hcF f1 in
2165
      HcFormula.hashcons hcF (HCMAXEXCEPT (n, s, tf1))
2166
  | ATLEASTPROB (p, f1) ->
2167
      HcFormula.hashcons hcF (HCATLEASTPROB (p, hc_formula hcF f1))
2168
  | LESSPROBFAIL (p, f1) ->
2169
      HcFormula.hashcons hcF (HCLESSPROBFAIL (p, hc_formula hcF f1))
2170
  | CONST s ->
2171
      HcFormula.hashcons hcF (HCCONST s)
2172
  | CONSTN s ->
2173
      HcFormula.hashcons hcF (HCCONSTN s)
2174
  | ID f1 ->
2175
    let tf1 = hc_formula hcF f1 in
2176
      HcFormula.hashcons hcF (HCID tf1)
2177
  | NORM (f1, f2) ->
2178
      let tf1 = hc_formula hcF f1 in
2179
      let tf2 = hc_formula hcF f2 in
2180
      HcFormula.hashcons hcF (HCNORM (tf1, tf2))
2181
  | NORMN (f1, f2) ->
2182
      let tf1 = hc_formula hcF f1 in
2183
      let tf2 = hc_formula hcF f2 in
2184
      HcFormula.hashcons hcF (HCNORMN (tf1, tf2))
2185
  | CHC (f1, f2) ->
2186
      let tf1 = hc_formula hcF f1 in
2187
      let tf2 = hc_formula hcF f2 in
2188
      HcFormula.hashcons hcF (HCCHC (tf1, tf2))
2189
  | FUS (first, f1) ->
2190
      let tf1 = hc_formula hcF f1 in
2191
      HcFormula.hashcons hcF (HCFUS (first, tf1))
2192
  | MU (var, f1) ->
2193
     let tf1 = hc_formula hcF f1 in
2194
     HcFormula.hashcons hcF (HCMU (var, tf1))
2195
  | NU (var, f1) ->
2196
     let tf1 = hc_formula hcF f1 in
2197
     HcFormula.hashcons hcF (HCNU (var, tf1))
2198
  | AF _
2199
  | EF _
2200
  | AG _
2201
  | EG _
2202
  | AU _
2203
  | EU _
2204
  | AR _
2205
  | ER _ ->
2206
     raise (CoAlgException ("nnf: CTL should have been removed at this point"))
2207

    
2208
(* Replace the Variable name in f with formula formula
2209
   hc_replace foo φ ψ => ψ[foo |-> φ]
2210
 *)
2211
let rec hc_replace hcF name (formula: hcFormula) (f: hcFormula) =
2212
  let func = hc_replace hcF name formula in
2213
  let gennew = HcFormula.hashcons hcF in
2214
  match f.HC.node with
2215
  | HCTRUE
2216
  | HCFALSE
2217
  | HCAP _
2218
  | HCNOT _
2219
  | HCCONST _
2220
  | HCCONSTN _ -> f
2221
  | HCVAR s ->
2222
     if compare s name == 0
2223
     then formula
2224
     else f
2225
  | HCAT (s, f1) ->
2226
     let nf1 = func f1 in
2227
     if nf1 == f1 then f else gennew (HCAT(s, nf1))
2228
  | HCOR (f1, f2) ->
2229
     let nf1 = func f1 in
2230
     let nf2 = func f2 in
2231
     if nf1 == f1 && nf2 == f2 then f else gennew (HCOR(nf1, nf2))
2232
  | HCAND (f1, f2) ->
2233
     let nf1 = func f1 in
2234
     let nf2 = func f2 in
2235
     if nf1 == f1 && nf2 == f2 then f else gennew (HCAND(nf1, nf2))
2236
  | HCEX (s, f1) ->
2237
     let nf1 = func f1 in
2238
     if nf1 == f1 then f else gennew (HCEX(s, nf1))
2239
  | HCAX (s, f1) ->
2240
     let nf1 = func f1 in
2241
     if nf1 == f1 then f else gennew (HCAX(s, nf1))
2242
  | HCENFORCES (s, f1) ->
2243
     let nf1 = func f1 in
2244
     if nf1 == f1 then f else gennew (HCENFORCES(s, nf1))
2245
  | HCALLOWS (s, f1) ->
2246
     let nf1 = func f1 in
2247
     if nf1 == f1 then f else gennew (HCALLOWS(s, nf1))
2248
  | HCMORETHAN  (n, s, f1) ->
2249
     let nf1 = func f1 in
2250
     if nf1 == f1 then f else gennew (HCMORETHAN(n, s, nf1))
2251
  | HCMAXEXCEPT  (n, s, f1) ->
2252
     let nf1 = func f1 in
2253
     if nf1 == f1 then f else gennew (HCMAXEXCEPT(n, s, nf1))
2254
  | HCATLEASTPROB (p, f1) ->
2255
     let nf1 = func f1 in
2256
     if nf1 == f1 then f else gennew (HCATLEASTPROB(p, nf1))
2257
  | HCLESSPROBFAIL (p, f1) ->
2258
     let nf1 = func f1 in
2259
     if nf1 == f1 then f else gennew (HCLESSPROBFAIL(p, nf1))
2260
  | HCID f1 ->
2261
     let nf1 = func f1 in
2262
     if nf1 == f1 then f else gennew (HCID(nf1))
2263
  | HCNORM (f1, f2) ->
2264
     let nf1 = func f1 in
2265
     let nf2 = func f2 in
2266
     if nf1 == f1 && nf2 == f2 then f else gennew (HCNORM(nf1, nf2))
2267
  | HCNORMN (f1, f2) ->
2268
     let nf1 = func f1 in
2269
     let nf2 = func f2 in
2270
     if nf1 == f1 && nf2 == f2 then f else gennew (HCNORMN(nf1, nf2))
2271
  | HCCHC (f1, f2) ->
2272
     let nf1 = func f1 in
2273
     let nf2 = func f2 in
2274
     if nf1 == f1 && nf2 == f2 then f else gennew (HCCHC(nf1, nf2))
2275
  | HCFUS (first, f1) ->
2276
     let nf1 = func f1 in
2277
     if nf1 == f1 then f else gennew (HCFUS(first, nf1))
2278
  | HCMU (var, f1) ->
2279
     if compare var name != 0 then
2280
       let nf1 = func f1 in
2281
       if nf1 == f1 then f else gennew (HCMU(var, nf1))
2282
     else
2283
       f
2284
  | HCNU (var, f1) ->
2285
     if compare var name != 0 then
2286
       let nf1 = func f1 in
2287
       if nf1 == f1 then f else gennew (HCNU(var, nf1))
2288
     else
2289
       f
2290

    
2291
let rec hc_freeIn variable (f: hcFormula) =
2292
  match f.HC.node with
2293
  | HCTRUE
2294
  | HCFALSE
2295
  | HCAP _
2296
  | HCNOT _
2297
  | HCCONST _
2298
  | HCCONSTN _ -> false
2299
  | HCVAR s ->
2300
     if compare variable s == 0
2301
     then true
2302
     else false
2303
  | HCAT (s, f1) ->
2304
     hc_freeIn variable f1
2305
  | HCOR (f1, f2)
2306
  | HCAND (f1, f2) ->
2307
     hc_freeIn variable f1 || hc_freeIn variable f2
2308
  | HCEX (_, f1)
2309
  | HCAX (_, f1)
2310
  | HCENFORCES (_, f1)
2311
  | HCALLOWS (_, f1)
2312
  | HCMORETHAN  (_, _, f1)
2313
  | HCMAXEXCEPT  (_, _, f1)
2314
  | HCATLEASTPROB (_, f1)
2315
  | HCLESSPROBFAIL (_, f1)
2316
  | HCID f1 ->
2317
     hc_freeIn variable f1
2318
  | HCNORM (f1, f2)
2319
  | HCNORMN (f1, f2)
2320
  | HCCHC (f1, f2) ->
2321
     hc_freeIn variable f1 || hc_freeIn variable f2
2322
  | HCFUS (first, f1) ->
2323
     hc_freeIn variable f1
2324
  | HCMU (var, f1)
2325
  | HCNU (var, f1) ->
2326
     (* Do we need to exclude bound variables here? *)
2327
     hc_freeIn variable f1
2328

    
2329

    
2330
(** An instantiation of a hash table (of the standard library)
2331
    for hash-consed formulae. The test for equality
2332
    and computing the hash value is done in constant time.
2333
 *)
2334
module HcFHt = Hashtbl.Make(
2335
  struct
2336
    type t = hcFormula
2337
    let equal (f1 : t) f2 = f1.HC.tag = f2.HC.tag
2338
    let hash (f : t) = f.HC.tag
2339
  end
2340
 )