Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgFormula.ml @ 97d73a78

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 helper formula =
247
    match formula with
248
    | AF f1 ->
249
       MU ("#AF#", (OR (f1, (AX ("", (VAR "#AF#"))))))
250
    | EF f1 ->
251
       MU ("#EF#", (OR (f1, (EX ("", (VAR "#EF#"))))))
252
    | AG f1 ->
253
       NU ("#AG#", (AND (f1, (AX ("", (VAR "#AG#"))))))
254
    | EG f1 ->
255
       NU ("#EG#", (AND (f1, (EX ("", (VAR "#EG#"))))))
256
    | AU (f1, f2) ->
257
       MU ("#AU#", (OR (f2, (AND (f1, (AX ("", (VAR "#AU#"))))))))
258
    | EU (f1, f2) ->
259
       MU ("#EU#", (OR (f2, (AND (f1, (EX ("", (VAR "#EU#"))))))))
260
    | AR (f1, f2) ->
261
       NU ("#AR#", (AND (f2, (OR (f1, (AX ("", (VAR "#AR#"))))))))
262
    | ER (f1, f2) ->
263
       NU ("#ER#", (AND (f2, (OR (f1, (EX ("", (VAR "#ER#"))))))))
264
    | AB (f1, f2) ->
265
       NOT (MU ("#AB#", (OR (f2, (AND ((NOT f1), (AX ("", (VAR "#AU#")))))))))
266
    | EB (f1, f2) ->
267
       NOT (MU ("#EB#", (OR (f2, (AND ((NOT f1), (EX ("", (VAR "#EU#")))))))))
268
    | _ -> formula
269
  in
270
  convert_post helper formula
271

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

    
481

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

    
493
let string_of_formula = exportFormula
494

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

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

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

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

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

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

    
647

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

    
658
let mk_exn s = CoAlgException s
659

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

    
724

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
1184

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
1658

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
1803

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
1927

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

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

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

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

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

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

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

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

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

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

    
2342

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