Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgFormula.ml @ 2a36974b

History | View | Annotate | Download (69.2 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
  | AB of formula * formula
73
  | EB of formula * formula
74

    
75
exception ConversionException of formula
76

    
77

    
78
(** Defines sorted coalgebraic formulae.
79
 *)
80
type sortedFormula = sort * formula
81

    
82

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

    
89

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

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

    
138

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

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

    
212
let convertToK formula = (* tries to convert a formula to a pure K formula *)
213
  let helper formula = match formula with
214
  | ENFORCES _ | ALLOWS _ -> raise (ConversionException formula)
215
  | MORETHAN (0,s,a) | MIN (1,s,a) -> EX (s,a)
216
  | MAX (0,s,a) -> AX (s, NOT a)
217
  | MAXEXCEPT (0,s,a) -> AX (s, a)
218
  | TRUE | FALSE
219
  | EQU _ | IMP _
220
  | AND _ | OR _
221
  | AP _ | NOT _
222
  | AX _ | EX _
223
  | CHC _ | FUS _ -> formula
224
  | _ -> raise (ConversionException formula)
225
  in
226
  convert_post helper formula
227

    
228
let convertToGML formula = (* tries to convert a formula to a pure GML formula *)
229
  let helper formula = match formula with
230
  | ENFORCES _ | ALLOWS _ -> raise (ConversionException formula)
231
  | MORETHAN _ | MIN _ | MAX _ | MAXEXCEPT _ -> formula
232
  | TRUE | FALSE
233
  | EQU _ | IMP _
234
  | AND _ | OR _
235
  | AP _ | NOT _
236
  | CHC _ | FUS _ -> formula
237
  | AX (r,a) -> MAXEXCEPT (0,r,a)
238
  | EX (r,a) -> MORETHAN  (0,r,a)
239
  | _ -> raise (ConversionException formula)
240
  in
241
  convert_post helper formula
242

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

    
245
let convertToMu formula =
246
  let name = Stream.next gensym in
247
  let helper formula =
248
    match formula with
249
    | AF f1 ->
250
       MU (name, (OR (f1, (AX ("", (VAR name))))))
251
    | EF f1 ->
252
       MU (name, (OR (f1, (EX ("", (VAR name))))))
253
    | AG f1 ->
254
       NU (name, (AND (f1, (AX ("", (VAR name))))))
255
    | EG f1 ->
256
       NU (name, (AND (f1, (EX ("", (VAR name))))))
257
    | AU (f1, f2) ->
258
       MU (name, (OR (f2, (AND (f1, (AX ("", (VAR name))))))))
259
    | EU (f1, f2) ->
260
       MU (name, (OR (f2, (AND (f1, (EX ("", (VAR name))))))))
261
    | AR (f1, f2) ->
262
       NU (name, (AND (f2, (OR (f1, (AX ("", (VAR name))))))))
263
    | ER (f1, f2) ->
264
       NU (name, (AND (f2, (OR (f1, (EX ("", (VAR name))))))))
265
    | AB (f1, f2) ->
266
       NOT (MU (name, (OR (f2, (AND ((NOT f1), (EX ("", (VAR name)))))))))
267
    | EB (f1, f2) ->
268
       NOT (MU (name, (OR (f2, (AND ((NOT f1), (AX ("", (VAR name)))))))))
269
    | _ -> formula
270
  in
271
  convert_post helper formula
272

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

    
482

    
483
(** Converts a formula into a string representation.
484
    Parentheses are ommited where possible
485
    where the preference rules are defined as usual.
486
    @param f A formula.
487
    @return A string representing f.
488
 *)
489
let exportFormula f =
490
  let sb = Buffer.create 128 in
491
  exportFormula_buffer sb f;
492
  Buffer.contents sb
493

    
494
let string_of_formula = exportFormula
495

    
496
(** export (CL)-formula suitable for tatl-inputs *)
497
let rec exportTatlFormula_buffer sb f =
498
  let prio n lf =
499
    let prionr = function
500
      | EQU _ -> 0
501
      | IMP _  -> 1
502
      | OR _ -> 2
503
      | AND _ -> 3
504
      | _ -> 4
505
    in
506
    if prionr lf < n then begin
507
      Buffer.add_char sb '(';
508
      exportTatlFormula_buffer sb lf;
509
      Buffer.add_char sb ')'
510
    end
511
    else exportTatlFormula_buffer sb lf
512
  in
513
  match f with
514
  | TRUE -> Buffer.add_string sb "(p \\/ ~p)"
515
  | FALSE -> Buffer.add_string sb "(p /\\ ~p)"
516
  | AP s -> Buffer.add_string sb s
517
  | NOT f1 ->
518
      Buffer.add_string sb "~";
519
      prio 4 f1
520
  | OR (f1, f2) ->
521
      prio 2 f1;
522
      Buffer.add_string sb " \\/ ";
523
      prio 2 f2
524
  | AND (f1, f2) ->
525
      prio 3 f1;
526
      Buffer.add_string sb " /\\ ";
527
      prio 3 f2
528
  | EQU (f1, f2) ->
529
      prio 0 (AND (IMP (f1,f2), IMP (f2,f1)))
530
  | IMP (f1, f2) ->
531
      prio 2 f1;
532
      Buffer.add_string sb " -> ";
533
      prio 2 f2
534
  | ALLOWS (s, f1) ->
535
      Buffer.add_string sb "<<";
536
      Buffer.add_string sb (
537
          match s with
538
          | [] -> " "
539
          | _ ->(Str.concat "," (L.map string_of_int s))
540
      );
541
      Buffer.add_string sb ">>X ";
542
      prio 4 f1
543
  | ENFORCES (s, f1) ->
544
      Buffer.add_string sb "~<<";
545
      Buffer.add_string sb (
546
          match s with
547
          | [] -> " "
548
          | _ ->(Str.concat "," (L.map string_of_int s))
549
      );
550
      Buffer.add_string sb ">>X ~ ";
551
      prio 4 f1
552
  | EX _
553
  | AX _
554
  | MIN _
555
  | MAX _
556
  | MORETHAN _
557
  | MAXEXCEPT _
558
  | AT _
559
  | CONST _
560
  | CONSTN _
561
  | CHC _
562
  | ATLEASTPROB _
563
  | LESSPROBFAIL _
564
  | ID _
565
  | NORM _
566
  | NORMN _
567
  | FUS _
568
  | MU _
569
  | NU _
570
  | VAR _
571
  | AF _
572
  | EF _
573
  | AG _
574
  | EG _
575
  | AU _
576
  | EU _
577
  | AR _
578
  | ER _
579
  | AB _
580
  | EB _ -> raise (CoAlgException ("export to tatl: Not connectives of CL"))
581

    
582
let exportTatlFormula f =
583
  let sb = Buffer.create 128 in
584
  exportTatlFormula_buffer sb f;
585
  Buffer.contents sb
586

    
587
(** Appends a string representation of a sorted formula to a string buffer.
588
    Parentheses are ommited where possible
589
    where the preference rules are defined as usual.
590
    @param sb A string buffer.
591
    @param (s, f) A sorted formula.
592
 *)
593
let rec exportSortedFormula_buffer sb (s, f) =
594
  Buffer.add_string sb (string_of_int s);
595
  Buffer.add_string sb ": ";
596
  exportFormula_buffer sb f
597

    
598
(** Converts a sorted formula into a string representation.
599
    Parentheses are ommited where possible
600
    where the preference rules are defined as usual.
601
    @param f A sorted formula.
602
    @return A string representing f.
603
 *)
604
let exportSortedFormula f =
605
  let sb = Buffer.create 128 in
606
  exportSortedFormula_buffer sb f;
607
  Buffer.contents sb
608

    
609
(** Converts a (sorted) formula query into a string representation.
610
    @param tbox A list of sorted formulae representing a TBox.
611
    @param f A sorted formula.
612
    @return A string representing tbox |- f.
613
 *)
614
let exportQuery tbox f =
615
  let sb = Buffer.create 1000 in
616
  let rec expFl = function
617
    | [] -> ()
618
    | h::tl ->
619
        exportSortedFormula_buffer sb h;
620
        if tl <> [] then Buffer.add_string sb "; " else ();
621
        expFl tl
622
  in
623
  expFl tbox;
624
  Buffer.add_string sb "  |-  ";
625
  exportSortedFormula_buffer sb f;
626
  Buffer.contents sb
627

    
628
(** Converts a (sorted) formula query into a string representation. Such that
629
    coalg can read it again using importQuery
630
    @param tbox A list of sorted formulae representing a TBox.
631
    @param f A sorted formula.
632
    @return A string representing tbox |- f.
633
 *)
634
let exportQueryParsable tbox (_,f) =
635
  let sb = Buffer.create 1000 in
636
  let rec expFl = function
637
    | [] -> ()
638
    | (_,h)::tl ->
639
        exportFormula_buffer sb h;
640
        if tl <> [] then Buffer.add_string sb "; " else ();
641
        expFl tl
642
  in
643
  expFl tbox;
644
  Buffer.add_string sb "  |-  ";
645
  exportFormula_buffer sb f;
646
  Buffer.contents sb
647

    
648

    
649
(* NB: True and False are the propositional constants. Lower case
650
   true/false are regardes as atomic propositions and we emit a warning
651
*)
652
let lexer = A.make_lexer
653
    [":";";";"|-";"(";")";"=>";"<=>";"|";"&";"~";"@";"True";"False";"true";"false";"<";">";"[";"]";"{<=";"{>=";"}";"+";"[pi1]";"[pi2]"
654
     ;"[{";"}]";"<{";"}>";",";"/";"{<";"=";"=o";"O"
655
     ;"μ";"ν";"."
656
     ;"AX";"EX";"AF";"EF";"AG";"EG";"A";"E";"U";"R";"B"
657
    ]
658

    
659
let mk_exn s = CoAlgException s
660

    
661
(** Process from inside out. cons all variables seen, remove them when
662
    binding fixpoint is found. Fixpoint type may only change if last
663
    (inner) fixpoint didn't include any free variables.
664
 *)
665
let rec verifyMuAltFree formula =
666
  let proc = verifyMuAltFree in
667
  match formula with
668
  | TRUE | FALSE | AP _ -> ("none", [])
669
  | CONST _
670
  | CONSTN _ -> ("none", [])
671
  | AT (_,a) | NOT a
672
  | EX (_,a) | AX (_,a) -> proc a
673
  | OR (a,b) | AND (a,b)
674
  | EQU (a,b) | IMP (a,b) ->
675
     let (atype, afree) = proc a
676
     and (btype, bfree) = proc b in
677
     if (compare atype "μ" == 0 && compare btype "ν" == 0) ||
678
          (compare atype "ν" == 0 && compare btype "μ" == 0) then
679
       raise (CoAlgException ("formula not alternation-free"));
680
     if compare atype "none" == 0 then
681
       (btype, List.flatten [afree; bfree])
682
     else
683
       (atype, List.flatten [afree; bfree])
684
  | ENFORCES (_,a) | ALLOWS   (_,a)
685
  | MIN (_,_,a)    | MAX (_,_,a)
686
  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
687
  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
688
  | ID(a) -> proc a
689
  | NORM(a, b) | NORMN(a, b)
690
  | CHC (a,b)  ->
691
     let (atype, afree) = proc a
692
     and (btype, bfree) = proc b in
693
     if (compare atype "μ" == 0 && compare btype "ν" == 0) ||
694
          (compare atype "ν" == 0 && compare btype "μ" == 0) then
695
       raise (CoAlgException ("formula not alternation-free"));
696
     if compare atype "none" == 0 then
697
       (btype, List.flatten [afree; bfree])
698
     else
699
       (atype, List.flatten [afree; bfree])
700
  | FUS (_,a) -> proc a
701
  | MU (s, f) ->
702
     let (fptype, free) = proc f in
703
     (if (compare fptype "ν" == 0) then
704
        raise (CoAlgException ("formula not alternation-free")));
705
     let predicate x = compare x s != 0 in
706
     let newfree = List.filter predicate free in
707
     if newfree = [] then
708
       ("none", [])
709
     else
710
       ("μ", newfree)
711
  | NU (s, f) ->
712
     let (fptype, free) = proc f in
713
     (if (compare fptype "μ" == 0) then
714
        raise (CoAlgException ("formula not alternation-free")));
715
     let predicate x = compare x s != 0 in
716
     let newfree = List.filter predicate free in
717
     if newfree = [] then
718
       ("none", [])
719
     else
720
       ("ν", newfree)
721
  | VAR s -> ("none", [s])
722
  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ ->
723
     raise (CoAlgException ("verifyMuAltFree: CTL should have been removed at this point"))
724

    
725

    
726
(** Process from outside in. For every variable bound keep the tuple
727
    (name, negations). For every negation crossed map a +1 over snd on
728
    that list. For every variable met check that the matching
729
    negations is even.
730
 *)
731
let rec verifyMuMonotone negations formula =
732
  let proc = verifyMuMonotone negations in
733
  match formula with
734
  | TRUE | FALSE | AP _ -> ()
735
  | CONST _
736
  | CONSTN _ -> ()
737
  | AT (_,a)
738
  | EX (_,a) | AX (_,a) -> proc a
739
  | OR (a,b) | AND (a,b)
740
  | EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
741
  | ENFORCES (_,a) | ALLOWS   (_,a)
742
  | MIN (_,_,a)    | MAX (_,_,a)
743
  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
744
  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
745
  | ID(a) -> proc a
746
  | NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
747
  | CHC (a,b)  -> (proc a ; proc b)
748
  | FUS (_,a) -> proc a
749
  | MU (s, f)
750
  | NU (s, f) ->
751
     let newNeg = (s, 0) :: negations in
752
     verifyMuMonotone newNeg f
753
  | VAR s ->
754
     let finder (x, _) = compare x s == 0 in
755
     let (_, neg) = List.find finder negations in
756
     if ((neg land 1) != 0) then raise (CoAlgException ("formula not monotone"))
757
  | NOT a ->
758
     let increment (s, n) = (s, n+1) in
759
     let newNeg = List.map increment negations in
760
     verifyMuMonotone newNeg a
761
  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ ->
762
     raise (CoAlgException ("verifyMuMonotone: CTL should have been removed at this point"))
763

    
764
let rec verifyMuGuarded unguarded formula =
765
  let proc = verifyMuGuarded unguarded in
766
  match formula with
767
  | TRUE | FALSE | AP _ -> ()
768
  | CONST _
769
  | CONSTN _ -> ()
770
  | AT (_,a) | NOT a -> proc a
771
  | EX (_,a) | AX (_,a) -> verifyMuGuarded [] a
772
  | OR (a,b) | AND (a,b)
773
  | EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
774
  | ENFORCES (_,a) | ALLOWS   (_,a)
775
  | MIN (_,_,a)    | MAX (_,_,a)
776
  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
777
  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
778
  | ID(a) -> proc a
779
  | NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
780
  | CHC (a,b)  -> (proc a ; proc b)
781
  | FUS (_,a) -> proc a
782
  | MU (s, f)
783
  | NU (s, f) ->
784
     let newUnguard = s :: unguarded in
785
     verifyMuGuarded newUnguard f
786
  | VAR s ->
787
     let finder x = compare x s == 0 in
788
     if List.exists finder unguarded then
789
       raise (CoAlgException ("formula not guarded"))
790
  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ ->
791
     raise (CoAlgException ("verifyMuGuarded: CTL should have been removed at this point"))
792

    
793
let verifyFormula formula =
794
  verifyMuAltFree formula;
795
  verifyMuMonotone [] formula;
796
  verifyMuGuarded [] formula
797

    
798
(** These functions parse a token stream to obtain a formula.
799
    It is a standard recursive descent procedure.
800
    @param ts A token stream.
801
    @return The resulting (sub-)formula.
802
    @raise CoAlgException if ts does not represent a formula.
803
 *)
804
let rec parse_formula (symtab: 'a list) ts =
805
  let formula = (parse_imp symtab ts) in
806
  let f1 = convertToMu formula in
807
  match Stream.peek ts with
808
  | None -> f1
809
  | Some (A.Kwd "<=>") ->
810
      Stream.junk ts;
811
      let f2 = parse_formula symtab ts in
812
      EQU (f1, f2)
813
  | _ -> f1
814

    
815
(** These functions parse a token stream to obtain a formula.
816
    It is a standard recursive descent procedure.
817
    @param ts A token stream.
818
    @return The resulting (sub-)formula.
819
    @raise CoAlgException if ts does not represent a formula.
820
 *)
821
and parse_imp symtab ts=
822
  let f1 = parse_or symtab ts in
823
  match Stream.peek ts with
824
  | None -> f1
825
  | Some (A.Kwd "=>") ->
826
      Stream.junk ts;
827
      let f2 = parse_imp symtab ts in
828
      IMP (f1, f2)
829
  | _ -> f1
830

    
831
(** These functions parse a token stream to obtain a formula.
832
    It is a standard recursive descent procedure.
833
    @param ts A token stream.
834
    @return The resulting (sub-)formula.
835
    @raise CoAlgException if ts does not represent a formula.
836
 *)
837
and parse_or symtab ts =
838
  let f1 = parse_and symtab ts in
839
  match Stream.peek ts with
840
  | None -> f1
841
  | Some (A.Kwd "|") ->
842
      Stream.junk ts;
843
      let f2 = parse_or symtab ts in
844
      OR (f1, f2)
845
  | _ -> f1
846

    
847
(** These functions parse a token stream to obtain a formula.
848
    It is a standard recursive descent procedure.
849
    @param ts A token stream.
850
    @return The resulting (sub-)formula.
851
    @raise CoAlgException if ts does not represent a formula.
852
 *)
853
and parse_and symtab ts =
854
  let f1 = parse_cimp symtab ts in
855
  match Stream.peek ts with
856
  | None -> f1
857
  | Some (A.Kwd "&") ->
858
      Stream.junk ts;
859
      let f2 = parse_and symtab ts in
860
      AND (f1, f2)
861
  | _ -> f1
862

    
863
(** These functions parse a token stream to obtain a formula.
864
    It is a standard recursive descent procedure.
865
    @param ts A token stream.
866
    @return The resulting (sub-)formula.
867
    @raise CoAlgException if ts does not represent a formula.
868
 *)
869
and parse_cimp symtab ts =
870
  let f1 = parse_rest symtab ts in
871
  match Stream.peek ts with
872
  | None -> f1
873
  | Some (A.Kwd "=o") ->
874
      Stream.junk ts;
875
      let f2 = parse_cimp symtab ts in
876
      NORM (f1, f2)
877
  | _ -> f1
878

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

    
1088
(** Parses a sorted formula.
1089
    @param ts A token stream.
1090
    @return A sorted formula.
1091
    @raise CoAlgException If ts does not represent a sorted formula.
1092
 *)
1093
let parse_sortedFormula ts =
1094
  let nr =
1095
    match Stream.peek ts with
1096
    | Some (A.Int n) ->
1097
        if n >= 0 then begin
1098
          Stream.junk ts;
1099
          let () =
1100
            match Stream.next ts with
1101
            | A.Kwd ":" -> ()
1102
            | t -> A.printError mk_exn ~t ~ts ("\":\" expected: ")
1103
          in
1104
          n
1105
        end else
1106
          A.printError mk_exn ~ts ("<non-negative number> expected: ")
1107
    | _ -> 0
1108
  in
1109
  let f = parse_formula [] ts in
1110
  (nr, f)
1111

    
1112
(** Parses a list of sorted formulae separated by ";".
1113
    @param ts A token stream.
1114
    @param acc The list of sorted formulae parsed so far.
1115
    @return The resulting list of sorted formula.
1116
    @raise CoAlgException if ts does not represent a list of sorted formulae.
1117
 *)
1118
let rec parse_sortedFormulaList ts acc =
1119
  let f1 = parse_sortedFormula ts in
1120
  match Stream.peek ts with
1121
  | Some (A.Kwd ";") ->
1122
      Stream.junk ts;
1123
      parse_sortedFormulaList ts (f1::acc)
1124
  | _ -> List.rev (f1::acc)
1125

    
1126
(** A common wrapper for import functions.
1127
    @param fkt An import function.
1128
    @param s A string.
1129
    @return The object imported from s using fkt.
1130
    @raise CoAlgException If ts is not empty.
1131
 *)
1132
let importWrapper fkt s =
1133
  let ts = lexer s in
1134
  try
1135
    let res = fkt ts in
1136
    let _ =
1137
      match Stream.peek ts with
1138
      | None -> ()
1139
      | Some _ -> A.printError mk_exn ~ts "EOS expected: "
1140
    in
1141
    res
1142
  with Stream.Failure -> A.printError mk_exn ~ts "unexpected EOS"
1143

    
1144
(** Parses a string to obtain a formula.
1145
    @param s A string representing a formula.
1146
    @return The resulting formula.
1147
    @raise CoAlgException if s does not represent a formula.
1148
 *)
1149
let importFormula s = importWrapper (parse_formula []) s
1150

    
1151
(** Parses a string to obtain a sorted formula.
1152
    @param s A string representing a sorted formula.
1153
    @return The sorted formula.
1154
    @raise CoAlgException If s does not represent a sorted formula.
1155
 *)
1156
let importSortedFormula s = importWrapper parse_sortedFormula s
1157

    
1158
(** Parses a string to obtain a (sorted) formula query.
1159
    @param s A string representing a formula query.
1160
    @return A pair (tbox, f) where
1161
    tbox is a list of sorted formulae representing the TBox; and
1162
    f is a sorted formula.
1163
    @raise CoAlgException if s does not represent a formula query.
1164
 *)
1165
let importQuery s =
1166
  let fkt ts =
1167
    match Stream.peek ts with
1168
    | Some (A.Kwd "|-") ->
1169
        Stream.junk ts;
1170
        let f = parse_sortedFormula ts in
1171
        ([], f)
1172
    | _ ->
1173
        let fl = parse_sortedFormulaList ts [] in
1174
        match Stream.peek ts with
1175
        | Some (A.Kwd "|-") ->
1176
            Stream.junk ts;
1177
            let f = parse_sortedFormula ts in
1178
            (fl, f)
1179
        | _ ->
1180
            if List.length fl = 1 then ([], List.hd fl)
1181
            else A.printError mk_exn ~ts "\"|-\" expected: "
1182
  in
1183
  importWrapper fkt s
1184

    
1185

    
1186
(** Converts the negation of a formula to negation normal form
1187
    by "pushing in" the negations "~".
1188
    The symbols "<=>" and "=>" are substituted by their usual definitions.
1189
    @param f A formula.
1190
    @return A formula in negation normal form and not containing "<=>" or "=>"
1191
    that is equivalent to ~f.
1192
 *)
1193
let rec nnfNeg f =
1194
  match f with
1195
  | TRUE -> FALSE
1196
  | FALSE -> TRUE
1197
  | AP _ -> NOT f
1198
  | VAR _ -> f
1199
  | NOT f1 -> nnf f1
1200
  | AT (s, f1) -> AT (s, nnfNeg f1)
1201
  | OR (f1, f2) -> AND (nnfNeg f1, nnfNeg f2)
1202
  | AND (f1, f2) -> OR (nnfNeg f1, nnfNeg f2)
1203
  | EQU (f1, f2) -> OR (AND (nnf f1, nnfNeg f2), AND (nnf f2, nnfNeg f1))
1204
  | IMP (f1, f2) -> AND (nnf f1, nnfNeg f2)
1205
  | EX (s, f1) -> AX (s, nnfNeg f1)
1206
  | AX (s, f1) -> EX (s, nnfNeg f1)
1207
  | ENFORCES (s, f1) -> ALLOWS (s, nnfNeg f1)
1208
  | ALLOWS (s, f1) -> ENFORCES (s, nnfNeg f1)
1209
  | MIN (n, s, f1) -> if n = 0 then FALSE else MAXEXCEPT (n-1, s, nnfNeg f1)
1210
  | MAX (n, s, f1) -> MORETHAN (n, s, nnf f1)
1211
  | MORETHAN (n, s, f1) -> MAXEXCEPT (n, s, nnfNeg f1)
1212
  | MAXEXCEPT (n, s, f1) -> MORETHAN (n, s, nnfNeg f1)
1213
  | ATLEASTPROB (p, f1) -> LESSPROBFAIL (p, nnfNeg f1)
1214
  | LESSPROBFAIL (p, f1) -> ATLEASTPROB (p, nnfNeg f1)
1215
  | CONST s -> CONSTN s
1216
  | CONSTN s -> CONST s
1217
  | ID (f1) -> ID (nnfNeg f1)
1218
  | NORM(f1, f2) -> NORMN(nnfNeg f1, nnfNeg f2)
1219
  | NORMN(f1, f2) -> NORM (nnfNeg f1, nnfNeg f2)
1220
  | CHC (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2)
1221
  | FUS (first, f1) -> FUS (first, nnfNeg f1)
1222
  | MU (s, f1) -> NU(s, nnfNeg f1)
1223
  | NU (s, f1) -> MU(s, nnfNeg f1)
1224
  | AF _ | EF _
1225
  | AG _ | EG _
1226
  | AU _ | EU _
1227
  | AR _ | ER _
1228
  | AB _ | EB _ -> raise (CoAlgException ("nnfNeg: CTL should have been removed at this point"))
1229

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

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

    
1515
(** Destructs an atomic proposition.
1516
    @param f An atomic proposition.
1517
    @return The name of the atomic proposition.
1518
    @raise CoAlgException if f is not an atomic proposition.
1519
 *)
1520
let dest_ap f =
1521
  match f with
1522
  | AP s when not (isNominal s) -> s
1523
  | _ -> raise (CoAlgException "Formula is not an atomic proposition.")
1524

    
1525
(** Destructs a nominal.
1526
    @param f A nominal.
1527
    @return The name of the nominal
1528
    @raise CoAlgException if f is not a nominal.
1529
 *)
1530
let dest_nom f =
1531
  match f with
1532
  | AP s when isNominal s -> s
1533
  | _ -> raise (CoAlgException "Formula is not a nominal.")
1534

    
1535
(** Destructs a negation.
1536
    @param f A negation.
1537
    @return The immediate subformula of the negation.
1538
    @raise CoAlgException if f is not a negation.
1539
 *)
1540
let dest_not f =
1541
  match f with
1542
  | NOT f1 -> f1
1543
  | _ -> raise (CoAlgException "Formula is not a negation.")
1544

    
1545
(** Destructs an @-formula.
1546
    @param f An @-formula.
1547
    @return The name of the nominal and the immediate subformula of the @-formula.
1548
    @raise CoAlgException if f is not an @-formula.
1549
 *)
1550
let dest_at f =
1551
  match f with
1552
  | AT (s, f1) -> (s, f1)
1553
  | _ -> raise (CoAlgException "Formula is not an @-formula.")
1554

    
1555
(** Destructs an or-formula.
1556
    @param f An or-formula.
1557
    @return The two immediate subformulae of the or-formula.
1558
    @raise CoAlgException if f is not an or-formula.
1559
 *)
1560
let dest_or f =
1561
  match f with
1562
  | OR (f1, f2) -> (f1, f2)
1563
  | _ -> raise (CoAlgException "Formula is not an or-formula.")
1564

    
1565
(** Destructs an and-formula.
1566
    @param f An and-formula.
1567
    @return The two immediate subformulae of the and-formula.
1568
    @raise CoAlgException if f is not an and-formula.
1569
 *)
1570
let dest_and f =
1571
  match f with
1572
  | AND (f1, f2) -> (f1, f2)
1573
  | _ -> raise (CoAlgException "Formula is not an and-formula.")
1574

    
1575
(** Destructs an equivalence.
1576
    @param f An equivalence.
1577
    @return The two immediate subformulae of the equivalence.
1578
    @raise CoAlgException if f is not an equivalence.
1579
 *)
1580
let dest_equ f =
1581
  match f with
1582
  | EQU (f1, f2) -> (f1, f2)
1583
  | _ -> raise (CoAlgException "Formula is not an equivalence.")
1584

    
1585
(** Destructs an implication.
1586
    @param f An implication.
1587
    @return The two immediate subformulae of the implication.
1588
    @raise CoAlgException if f is not an implication.
1589
 *)
1590
let dest_imp f =
1591
  match f with
1592
  | IMP (f1, f2) -> (f1, f2)
1593
  | _ -> raise (CoAlgException "Formula is not an implication.")
1594

    
1595
(** Destructs an EX-formula.
1596
    @param f An EX-formula.
1597
    @return The role name and the immediate subformula of the EX-formula.
1598
    @raise CoAlgException if f is not an EX-formula.
1599
 *)
1600
let dest_ex f =
1601
  match f with
1602
  | EX (s, f1) -> (s, f1)
1603
  | _ -> raise (CoAlgException "Formula is not an EX-formula.")
1604

    
1605
(** Destructs an AX-formula.
1606
    @param f An AX-formula.
1607
    @return The role name and the immediate subformula of the AX-formula.
1608
    @raise CoAlgException if f is not an AX-formula.
1609
 *)
1610
let dest_ax f =
1611
  match f with
1612
  | AX (s, f1) -> (s, f1)
1613
  | _ -> raise (CoAlgException "Formula is not an AX-formula.")
1614

    
1615
(** Destructs a MIN-formula.
1616
    @param f A MIN-formula.
1617
    @return The number restriction, role name,
1618
    and the immediate subformula of the MIN-formula.
1619
    @raise CoAlgException if f is not a MIN-formula.
1620
 *)
1621
let dest_min f =
1622
  match f with
1623
  | MIN (n, s, f1) -> (n, s, f1)
1624
  | _ -> raise (CoAlgException "Formula is not a MIN-formula.")
1625

    
1626
(** Destructs a MAX-formula.
1627
    @param f A MAX-formula.
1628
    @return The number restriction, role name,
1629
    and the immediate subformula of the MAX-formula.
1630
    @raise CoAlgException if f is not a MAX-formula.
1631
 *)
1632
let dest_max f =
1633
  match f with
1634
  | MAX (n, s, f1) -> (n, s, f1)
1635
  | _ -> raise (CoAlgException "Formula is not a MAX-formula.")
1636

    
1637
(** Destructs a choice formula.
1638
    @param f A choice formula.
1639
    @return The two immediate subformulae of the choice formula.
1640
    @raise CoAlgException if f is not a choice formula.
1641
 *)
1642
let dest_choice f =
1643
  match f with
1644
  | CHC (f1, f2) -> (f1, f2)
1645
  | _ -> raise (CoAlgException "Formula is not a choice formula.")
1646

    
1647
(** Destructs a fusion formula.
1648
    @param f A fusion formula.
1649
    @return A pair (first, f1) where
1650
    first is true iff f is a first projection; and
1651
    f1 is the immediate subformulae of f.
1652
    @raise CoAlgException if f is not a fusion formula.
1653
 *)
1654
let dest_fusion f =
1655
  match f with
1656
  | FUS (first, f1) -> (first, f1)
1657
  | _ -> raise (CoAlgException "Formula is not a fusion formula.")
1658

    
1659

    
1660
(** Tests whether a formula is the constant True.
1661
    @param f A formula.
1662
    @return True iff f is the constant True.
1663
 *)
1664
let is_true f =
1665
  match f with
1666
  | TRUE -> true
1667
  | _ -> false
1668

    
1669
(** Tests whether a formula is the constant False.
1670
    @param f A formula.
1671
    @return True iff f is the constant False.
1672
 *)
1673
let is_false f =
1674
  match f with
1675
  | FALSE -> true
1676
  | _ -> false
1677

    
1678
(** Tests whether a formula is an atomic proposition.
1679
    @param f A formula.
1680
    @return True iff f is an atomic proposition.
1681
 *)
1682
let is_ap f =
1683
  match f with
1684
  | AP s when not (isNominal s) -> true
1685
  | _ -> false
1686

    
1687
(** Tests whether a formula is a nominal.
1688
    @param f A formula.
1689
    @return True iff f is a nominal.
1690
 *)
1691
let is_nom f =
1692
  match f with
1693
  | AP s when isNominal s -> true
1694
  | _ -> false
1695

    
1696
(** Tests whether a formula is a negation.
1697
    @param f A formula.
1698
    @return True iff f is a negation.
1699
 *)
1700
let is_not f =
1701
  match f with
1702
  | NOT _ -> true
1703
  | _ -> false
1704

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

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

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

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

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

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

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

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

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

    
1786
(** Tests whether a formula is a choice formula.
1787
    @param f A formula.
1788
    @return True iff f is a choice formula.
1789
 *)
1790
let is_choice f =
1791
  match f with
1792
  | CHC _ -> true
1793
  | _ -> false
1794

    
1795
(** Tests whether a formula is a fusion formula.
1796
    @param f A formula.
1797
    @return True iff f is a fusion formula.
1798
 *)
1799
let is_fusion f =
1800
  match f with
1801
  | FUS _ -> true
1802
  | _ -> false
1803

    
1804

    
1805
(** The constant True.
1806
 *)
1807
let const_true = TRUE
1808

    
1809
(** The constant False.
1810
 *)
1811
let const_false = FALSE
1812

    
1813
(** Constructs an atomic proposition.
1814
    @param s The name of the atomic proposition.
1815
    @return The atomic proposition with name s.
1816
    @raise CoAlgException if s is a nominal name.
1817
 *)
1818
let const_ap s =
1819
  if isNominal s then raise (CoAlgException "The name indicates a nominal.")
1820
  else AP s
1821

    
1822
(** Constructs a nominal.
1823
    @param s The name of the nominal.
1824
    @return A nominal with name s.
1825
    @raise CoAlgException if s is not a nominal name.
1826
 *)
1827
let const_nom s =
1828
  if isNominal s then AP s
1829
  else raise (CoAlgException "The name does not indicate a nominal.")
1830

    
1831
(** Negates a formula.
1832
    @param f A formula.
1833
    @return The negation of f.
1834
 *)
1835
let const_not f = NOT f
1836

    
1837
(** Constructs an @-formula from a name and a formula.
1838
    @param s A nominal name.
1839
    @param f A formula.
1840
    @return The formula AT (s, f).
1841
 *)
1842
let const_at s f = AT (s, f)
1843

    
1844
(** Constructs an or-formula from two formulae.
1845
    @param f1 The first formula (LHS).
1846
    @param f2 The second formula (LHS).
1847
    @return The formula f1 | f2.
1848
 *)
1849
let const_or f1 f2 = OR (f1, f2)
1850

    
1851
(** Constructs an and-formula from two formulae.
1852
    @param f1 The first formula (LHS).
1853
    @param f2 The second formula (LHS).
1854
    @return The formula f1 & f2.
1855
 *)
1856
let const_and f1 f2 = AND (f1, f2)
1857

    
1858
(** Constructs an equivalence from two formulae.
1859
    @param f1 The first formula (LHS).
1860
    @param f2 The second formula (LHS).
1861
    @return The equivalence f1 <=> f2.
1862
 *)
1863
let const_equ f1 f2 = EQU (f1, f2)
1864

    
1865
(** Constructs an implication from two formulae.
1866
    @param f1 The first formula (LHS).
1867
    @param f2 The second formula (LHS).
1868
    @return The implication f1 => f2.
1869
 *)
1870
let const_imp f1 f2 = IMP (f1, f2)
1871

    
1872
(** Constructs an EX-formula from a formula.
1873
    @param s A role name.
1874
    @param f A formula.
1875
    @return The formula EX (s, f).
1876
 *)
1877
let const_ex s f = EX (s, f)
1878

    
1879
(** Constructs an AX-formula from a formula.
1880
    @param s A role name.
1881
    @param f A formula.
1882
    @return The formula AX (s, f).
1883
 *)
1884
let const_ax s f = AX (s, f)
1885

    
1886
(** Constructs a MIN-formula from a formula.
1887
    @param n A non-negative integer.
1888
    @param s A role name.
1889
    @param f A formula.
1890
    @return The formula MIN f.
1891
    @raise CoAlgException Iff n is negative.
1892
 *)
1893
let const_min n s f =
1894
  if n < 0 then raise (CoAlgException "Negative cardinality constraint.")
1895
  else MIN (n, s, f)
1896

    
1897
(** Constructs a MAX-formula from a formula.
1898
    @param n A non-negative integer.
1899
    @param s A role name.
1900
    @param f A formula.
1901
    @return The formula MAX f.
1902
    @raise CoAlgException Iff n is negative.
1903
 *)
1904
let const_max n s f =
1905
  if n < 0 then raise (CoAlgException "Negative cardinality constraint.")
1906
  else MAX (n, s, f)
1907

    
1908
let const_enforces p f =
1909
    ENFORCES (p,f)
1910

    
1911
let const_allows p f =
1912
    ALLOWS (p,f)
1913

    
1914
(** Constructs a choice formula from two formulae.
1915
    @param f1 The first formula (LHS).
1916
    @param f2 The second formula (LHS).
1917
    @return The formula (f1 + f2).
1918
 *)
1919
let const_choice f1 f2 = CHC (f1, f2)
1920

    
1921
(** Constructs a fusion formula.
1922
    @param first True iff the result is a first projection.
1923
    @param f1 A formula.
1924
    @return The formula [pi1] f1 or [pi2] f1 (depending on first).
1925
 *)
1926
let const_fusion first f1 = FUS (first, f1)
1927

    
1928

    
1929
(** Hash-consed formulae, which are in negation normal form,
1930
    such that structural and physical equality coincide.
1931

    
1932
    Also CTL has been replaced by the equivalent μ-Calculus
1933
    constructs
1934
 *)
1935
type hcFormula = (hcFormula_node, formula) HC.hash_consed
1936
and hcFormula_node =
1937
  | HCTRUE
1938
  | HCFALSE
1939
  | HCAP of string
1940
  | HCNOT of string
1941
  | HCAT of string * hcFormula
1942
  | HCOR of hcFormula * hcFormula
1943
  | HCAND of hcFormula * hcFormula
1944
  | HCEX of string * hcFormula
1945
  | HCAX of string * hcFormula
1946
  | HCENFORCES of int list * hcFormula
1947
  | HCALLOWS of int list * hcFormula
1948
  | HCMORETHAN of int * string * hcFormula (* GML Diamond *)
1949
  | HCMAXEXCEPT of int * string * hcFormula (* GML Box *)
1950
  | HCATLEASTPROB of rational * hcFormula
1951
  | HCLESSPROBFAIL of rational * hcFormula
1952
  | HCCONST of string
1953
  | HCCONSTN of string
1954
  | HCID of hcFormula
1955
  | HCNORM of hcFormula * hcFormula
1956
  | HCNORMN of hcFormula * hcFormula
1957
  | HCCHC of hcFormula * hcFormula
1958
  | HCFUS of bool * hcFormula
1959
  | HCMU of string * hcFormula
1960
  | HCNU of string * hcFormula
1961
  | HCVAR of string
1962

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

    
2026
(** Computes the hash value of a formula node.
2027
    @param f A formula node.
2028
    @return The hash value of f.
2029
 *)
2030
let hash_hcFormula_node f =
2031
  let base = 23 in (* should be larger than the no of constructors *)
2032
  match f with
2033
  | HCTRUE -> 0
2034
  | HCFALSE -> 1
2035
  | HCAP s
2036
  | HCNOT s
2037
  | HCVAR s -> base * Hashtbl.hash s + 1
2038
  | HCAT (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 2
2039
  | HCOR (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 5
2040
  | HCAND (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 6
2041
  | HCEX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 3
2042
  | HCAX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 4
2043
  | HCMORETHAN (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 7
2044
  | HCMAXEXCEPT (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 8
2045
  | HCATLEASTPROB (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 9
2046
  | HCLESSPROBFAIL (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 10
2047
  | HCCHC (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 11
2048
  | HCFUS (first, f1) -> base * (base * (Hashtbl.hash first) + f1.HC.hkey) + 13
2049
  | HCENFORCES (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 14
2050
  | HCALLOWS   (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 15
2051
  | HCCONST s -> Hashtbl.hash s + 16
2052
  | HCCONSTN s -> Hashtbl.hash s + 17
2053
  | HCNORM (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 18
2054
  | HCNORMN (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 19
2055
  | HCID (f1) -> base * f1.HC.hkey + 20
2056
  | HCMU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 21
2057
  | HCNU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 22
2058

    
2059
(** Determines the "real" formula of a formula node.
2060
    @param f A formula node.
2061
    @return The formula (in negation normal form) which corresponds to f.
2062
 *)
2063
let toFml_hcFormula_node f =
2064
  match f with
2065
  | HCTRUE -> TRUE
2066
  | HCFALSE -> FALSE
2067
  | HCAP s -> AP s
2068
  | HCVAR s -> VAR s
2069
  | HCNOT s -> NOT (AP s)
2070
  | HCAT (s, f1) -> AT (s, f1.HC.fml)
2071
  | HCOR (f1, f2) -> OR (f1.HC.fml, f2.HC.fml)
2072
  | HCAND (f1, f2) -> AND (f1.HC.fml, f2.HC.fml)
2073
  | HCEX (s, f1) -> EX (s, f1.HC.fml)
2074
  | HCAX (s, f1) -> AX (s, f1.HC.fml)
2075
  | HCENFORCES (s, f1) -> ENFORCES (s, f1.HC.fml)
2076
  | HCALLOWS (s, f1) -> ALLOWS (s, f1.HC.fml)
2077
  | HCMORETHAN (n, s, f1) -> MORETHAN (n, s, f1.HC.fml)
2078
  | HCMAXEXCEPT (n, s, f1) -> MAXEXCEPT (n, s, f1.HC.fml)
2079
  | HCATLEASTPROB (p, f1) -> ATLEASTPROB (p, f1.HC.fml)
2080
  | HCLESSPROBFAIL (p, f1) -> LESSPROBFAIL (p, f1.HC.fml)
2081
  | HCCONST s -> CONST s
2082
  | HCCONSTN s -> CONSTN s
2083
  | HCID (f1) -> ID(f1.HC.fml)
2084
  | HCNORM (f1, f2) -> NORM(f1.HC.fml, f2.HC.fml)
2085
  | HCNORMN (f1, f2) -> NORMN(f1.HC.fml, f2.HC.fml)
2086
  | HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml)
2087
  | HCFUS (first, f1) -> FUS (first, f1.HC.fml)
2088
  | HCMU (var, f1) -> MU (var, f1.HC.fml)
2089
  | HCNU (var, f1) -> NU (var, f1.HC.fml)
2090

    
2091
(** Determines the negation (in negation normal form) of a formula node.
2092
    @param f A formula node.
2093
    @return The negation (in negation normal form) of f.
2094
 *)
2095
let negNde_hcFormula_node f =
2096
  match f with
2097
  | HCTRUE -> HCFALSE
2098
  | HCFALSE -> HCTRUE
2099
  | HCAP s -> HCNOT s
2100
  | HCNOT s -> HCAP s
2101
  | HCVAR s -> f
2102
  | HCAT (s, f1) -> HCAT (s, f1.HC.neg)
2103
  | HCOR (f1, f2) -> HCAND (f1.HC.neg, f2.HC.neg)
2104
  | HCAND (f1, f2) -> HCOR (f1.HC.neg, f2.HC.neg)
2105
  | HCEX (s, f2) -> HCAX (s, f2.HC.neg)
2106
  | HCAX (s, f2) -> HCEX (s, f2.HC.neg)
2107
  | HCENFORCES (s, f2) -> HCALLOWS (s, f2.HC.neg)
2108
  | HCALLOWS (s, f2) -> HCENFORCES (s, f2.HC.neg)
2109
  | HCMORETHAN (n, s, f1) -> HCMAXEXCEPT (n, s, f1.HC.neg)
2110
  | HCMAXEXCEPT (n, s, f1) -> HCMORETHAN (n, s, f1.HC.neg)
2111
  | HCATLEASTPROB (p, f1) -> HCLESSPROBFAIL (p, f1.HC.neg)
2112
  | HCLESSPROBFAIL (p, f1) -> HCATLEASTPROB (p, f1.HC.neg)
2113
  | HCCONST s -> HCCONSTN s
2114
  | HCCONSTN s -> HCCONST s
2115
  | HCID (f1) -> HCID(f1.HC.neg)
2116
  | HCNORM (f1, f2) -> HCNORMN(f1.HC.neg, f2.HC.neg)
2117
  | HCNORMN (f1, f2) -> HCNORM(f1.HC.neg, f2.HC.neg)
2118
  | HCCHC (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg)
2119
  | HCFUS (first, f1) -> HCFUS (first, f1.HC.neg)
2120
  | HCMU (name, f1) -> HCNU (name, f1.HC.neg)
2121
  | HCNU (name, f1) -> HCMU (name, f1.HC.neg)
2122

    
2123
(** An instantiation of hash-consing for formulae.
2124
 *)
2125
module HcFormula = HC.Make(
2126
  struct
2127
    type nde = hcFormula_node
2128
    type fml = formula
2129
    let equal (n1 : nde) n2 = equal_hcFormula_node n1 n2
2130
    let hash (n : nde) = hash_hcFormula_node n
2131
    let negNde (n : nde) = negNde_hcFormula_node n
2132
    let toFml (n : nde) = toFml_hcFormula_node n
2133
  end
2134
 )
2135

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

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

    
2305
let rec hc_freeIn variable (f: hcFormula) =
2306
  match f.HC.node with
2307
  | HCTRUE
2308
  | HCFALSE
2309
  | HCAP _
2310
  | HCNOT _
2311
  | HCCONST _
2312
  | HCCONSTN _ -> false
2313
  | HCVAR s ->
2314
     if compare variable s == 0
2315
     then true
2316
     else false
2317
  | HCAT (s, f1) ->
2318
     hc_freeIn variable f1
2319
  | HCOR (f1, f2)
2320
  | HCAND (f1, f2) ->
2321
     hc_freeIn variable f1 || hc_freeIn variable f2
2322
  | HCEX (_, f1)
2323
  | HCAX (_, f1)
2324
  | HCENFORCES (_, f1)
2325
  | HCALLOWS (_, f1)
2326
  | HCMORETHAN  (_, _, f1)
2327
  | HCMAXEXCEPT  (_, _, f1)
2328
  | HCATLEASTPROB (_, f1)
2329
  | HCLESSPROBFAIL (_, f1)
2330
  | HCID f1 ->
2331
     hc_freeIn variable f1
2332
  | HCNORM (f1, f2)
2333
  | HCNORMN (f1, f2)
2334
  | HCCHC (f1, f2) ->
2335
     hc_freeIn variable f1 || hc_freeIn variable f2
2336
  | HCFUS (first, f1) ->
2337
     hc_freeIn variable f1
2338
  | HCMU (var, f1)
2339
  | HCNU (var, f1) ->
2340
     (* Do we need to exclude bound variables here? *)
2341
     hc_freeIn variable f1
2342

    
2343

    
2344
(** An instantiation of a hash table (of the standard library)
2345
    for hash-consed formulae. The test for equality
2346
    and computing the hash value is done in constant time.
2347
 *)
2348
module HcFHt = Hashtbl.Make(
2349
  struct
2350
    type t = hcFormula
2351
    let equal (f1 : t) f2 = f1.HC.tag = f2.HC.tag
2352
    let hash (f : t) = f.HC.tag
2353
  end
2354
 )