Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgFormula.ml @ 15537461

History | View | Annotate | Download (71.3 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

    
76
(** Defines (unsorted) coalgebraic axioms for the TBox.
77
 *)
78
type axiom =
79
  | DEFINITION of formula * formula
80
  | INCLUSION of formula * formula
81

    
82
exception ConversionException of formula
83

    
84
(** Defines sorted coalgebraic formulae.
85
 *)
86
type sortedFormula = sort * formula
87

    
88

    
89
(** Defines sorted coalgebraic axioms.
90
 *)
91
type sortedAxiom = sort * axiom
92

    
93
(** Determines whether a name indicates a nominal.
94
    @param A string s.
95
    @return True iff s contains a prime character.
96
 *)
97
let isNominal s = String.contains s '\''
98

    
99

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

    
142
(** Determines the size of a sorted formula.
143
    @param f A sorted formula.
144
    @return The size of f.
145
 *)
146
let sizeSortedFormula f = sizeFormula (snd f)
147

    
148

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

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

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

    
238
let convertToGML formula = (* tries to convert a formula to a pure GML formula *)
239
  let helper formula = match formula with
240
  | ENFORCES _ | ALLOWS _ -> raise (ConversionException formula)
241
  | MORETHAN _ | MIN _ | MAX _ | MAXEXCEPT _ -> formula
242
  | TRUE | FALSE
243
  | EQU _ | IMP _
244
  | AND _ | OR _
245
  | AP _ | NOT _
246
  | CHC _ | FUS _ -> formula
247
  | AX (r,a) -> MAXEXCEPT (0,r,a)
248
  | EX (r,a) -> MORETHAN  (0,r,a)
249
  | _ -> raise (ConversionException formula)
250
  in
251
  convert_post helper formula
252

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

    
255
let convertToMu formula =
256
  let name = Stream.next gensym in
257
  let helper formula =
258
    match formula with
259
    | AF f1 ->
260
       MU (name, (OR (f1, (AX ("", (VAR name))))))
261
    | EF f1 ->
262
       MU (name, (OR (f1, (EX ("", (VAR name))))))
263
    | AG f1 ->
264
       NU (name, (AND (f1, (AX ("", (VAR name))))))
265
    | EG f1 ->
266
       NU (name, (AND (f1, (EX ("", (VAR name))))))
267
    | AU (f1, f2) ->
268
       MU (name, (OR (f2, (AND (f1, (AX ("", (VAR name))))))))
269
    | EU (f1, f2) ->
270
       MU (name, (OR (f2, (AND (f1, (EX ("", (VAR name))))))))
271
    | AR (f1, f2) ->
272
       NU (name, (AND (f2, (OR (f1, (AX ("", (VAR name))))))))
273
    | ER (f1, f2) ->
274
       NU (name, (AND (f2, (OR (f1, (EX ("", (VAR name))))))))
275
    | AB (f1, f2) ->
276
       NOT (MU (name, (OR (f2, (AND ((NOT f1), (EX ("", (VAR name)))))))))
277
    | EB (f1, f2) ->
278
       NOT (MU (name, (OR (f2, (AND ((NOT f1), (AX ("", (VAR name)))))))))
279
    | _ -> formula
280
  in
281
  convert_post helper formula
282

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

    
492

    
493
(** Converts a formula into a string representation.
494
    Parentheses are ommited where possible
495
    where the preference rules are defined as usual.
496
    @param f A formula.
497
    @return A string representing f.
498
 *)
499
let exportFormula f =
500
  let sb = Buffer.create 128 in
501
  exportFormula_buffer sb f;
502
  Buffer.contents sb
503

    
504
let string_of_formula = exportFormula
505

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

    
592
let exportTatlFormula f =
593
  let sb = Buffer.create 128 in
594
  exportTatlFormula_buffer sb f;
595
  Buffer.contents sb
596

    
597
(** Appends a string representation of a sorted formula to a string buffer.
598
    Parentheses are ommited where possible
599
    where the preference rules are defined as usual.
600
    @param sb A string buffer.
601
    @param (s, f) A sorted formula.
602
 *)
603
let rec exportSortedFormula_buffer sb (s, f) =
604
  Buffer.add_string sb (string_of_int s);
605
  Buffer.add_string sb ": ";
606
  exportFormula_buffer sb f
607

    
608
(** Converts a sorted formula into a string representation.
609
    Parentheses are ommited where possible
610
    where the preference rules are defined as usual.
611
    @param f A sorted formula.
612
    @return A string representing f.
613
 *)
614
let exportSortedFormula f =
615
  let sb = Buffer.create 128 in
616
  exportSortedFormula_buffer sb f;
617
  Buffer.contents sb
618

    
619
(** Converts a (sorted) formula query into a string representation.
620
    @param tbox A list of sorted formulae representing a TBox.
621
    @param f A sorted formula.
622
    @return A string representing tbox |- f.
623
 *)
624
let exportQuery tbox f =
625
  let sb = Buffer.create 1000 in
626
  let rec expFl = function
627
    | [] -> ()
628
    | h::tl ->
629
        exportSortedFormula_buffer sb h;
630
        if tl <> [] then Buffer.add_string sb "; " else ();
631
        expFl tl
632
  in
633
  expFl tbox;
634
  Buffer.add_string sb "  |-  ";
635
  exportSortedFormula_buffer sb f;
636
  Buffer.contents sb
637

    
638
(** Converts a (sorted) formula query into a string representation. Such that
639
    coalg can read it again using importQuery
640
    @param tbox A list of sorted formulae representing a TBox.
641
    @param f A sorted formula.
642
    @return A string representing tbox |- f.
643
 *)
644
let exportQueryParsable tbox (_,f) =
645
  let sb = Buffer.create 1000 in
646
  let rec expFl = function
647
    | [] -> ()
648
    | (_,h)::tl ->
649
        exportFormula_buffer sb h;
650
        if tl <> [] then Buffer.add_string sb "; " else ();
651
        expFl tl
652
  in
653
  expFl tbox;
654
  Buffer.add_string sb "  |-  ";
655
  exportFormula_buffer sb f;
656
  Buffer.contents sb
657

    
658

    
659
(* NB: True and False are the propositional constants. Lower case
660
   true/false are regardes as atomic propositions and we emit a warning
661
*)
662
let lexer = A.make_lexer
663
    [":";";";"|-";"(";")";"=>";"<=>";"|";"&";"~";"@";"True";"False";"true";"false";"<";">";"[";"]";"{<=";"{>=";"}";"+";"[pi1]";"[pi2]"
664
     ;"[{";"}]";"<{";"}>";",";"/";"{<";"=";"=o";"O";":=";"[="
665
     ;"μ";"ν";"."
666
     ;"AX";"EX";"AF";"EF";"AG";"EG";"A";"E";"U";"R";"B"
667
    ]
668

    
669
let mk_exn s = CoAlgException s
670

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

    
735

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

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

    
803
let verifyFormula formula =
804
  verifyMuAltFree formula;
805
  verifyMuMonotone [] formula;
806
  verifyMuGuarded [] formula
807

    
808
(** These functions parse a token stream to obtain a formula.
809
    It is a standard recursive descent procedure.
810
    @param ts A token stream.
811
    @return The resulting (sub-)formula.
812
    @raise CoAlgException if ts does not represent a formula.
813
 *)
814
let rec parse_formula (symtab: 'a list) ts =
815
  let formula = (parse_imp symtab ts) in
816
  let f1 = convertToMu formula in
817
  match Stream.peek ts with
818
  | None -> f1
819
  | Some (A.Kwd "<=>") ->
820
      Stream.junk ts;
821
      let f2 = parse_formula symtab ts in
822
      EQU (f1, f2)
823
  | _ -> f1
824

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

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

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

    
873
(** These functions parse a token stream to obtain a formula.
874
    It is a standard recursive descent procedure.
875
    @param ts A token stream.
876
    @return The resulting (sub-)formula.
877
    @raise CoAlgException if ts does not represent a formula.
878
 *)
879
and parse_cimp symtab ts =
880
  let f1 = parse_rest symtab ts in
881
  match Stream.peek ts with
882
  | None -> f1
883
  | Some (A.Kwd "=o") ->
884
      Stream.junk ts;
885
      let f2 = parse_cimp symtab ts in
886
      NORM (f1, f2)
887
  | _ -> f1
888

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

    
1098
(** Parses a sorted formula.
1099
    @param ts A token stream.
1100
    @return A sorted formula.
1101
    @raise CoAlgException If ts does not represent a sorted formula.
1102
 *)
1103
let parse_sortedFormula ts =
1104
  let nr =
1105
    match Stream.peek ts with
1106
    | Some (A.Int n) ->
1107
        if n >= 0 then begin
1108
          Stream.junk ts;
1109
          let () =
1110
            match Stream.next ts with
1111
            | A.Kwd ":" -> ()
1112
            | t -> A.printError mk_exn ~t ~ts ("\":\" expected: ")
1113
          in
1114
          n
1115
        end else
1116
          A.printError mk_exn ~ts ("<non-negative number> expected: ")
1117
    | _ -> 0
1118
  in
1119
  let f = parse_formula [] ts in
1120
  (nr, f)
1121

    
1122
(** Parses a list of sorted formulae separated by ";".
1123
    @param ts A token stream.
1124
    @param acc The list of sorted formulae parsed so far.
1125
    @return The resulting list of sorted formula.
1126
    @raise CoAlgException if ts does not represent a list of sorted formulae.
1127
 *)
1128
let rec parse_sortedFormulaList ts acc =
1129
  let f1 = parse_sortedFormula ts in
1130
  match Stream.peek ts with
1131
  | Some (A.Kwd ";") ->
1132
      Stream.junk ts;
1133
      parse_sortedFormulaList ts (f1::acc)
1134
  | _ -> List.rev (f1::acc)
1135

    
1136
(** A common wrapper for import functions.
1137
    @param fkt An import function.
1138
    @param s A string.
1139
    @return The object imported from s using fkt.
1140
    @raise CoAlgException If ts is not empty.
1141
 *)
1142
let importWrapper fkt s =
1143
  let ts = lexer s in
1144
  try
1145
    let res = fkt ts in
1146
    let _ =
1147
      match Stream.peek ts with
1148
      | None -> ()
1149
      | Some _ -> A.printError mk_exn ~ts "EOS expected: "
1150
    in
1151
    res
1152
  with Stream.Failure -> A.printError mk_exn ~ts "unexpected EOS"
1153

    
1154
(** Parses a string to obtain a formula.
1155
    @param s A string representing a formula.
1156
    @return The resulting formula.
1157
    @raise CoAlgException if s does not represent a formula.
1158
 *)
1159
let importFormula s = importWrapper (parse_formula []) s
1160

    
1161
(** Parses a string to obtain a sorted formula.
1162
    @param s A string representing a sorted formula.
1163
    @return The sorted formula.
1164
    @raise CoAlgException If s does not represent a sorted formula.
1165
 *)
1166
let importSortedFormula s = importWrapper parse_sortedFormula s
1167

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

    
1195

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

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

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

    
1525
let exportSortedAxiom = function
1526
  | (s, INCLUSION(f1, f2)) -> (string_of_int s) ^ ": " ^ (exportFormula f1) ^ " [= " ^ (exportFormula f2)
1527
  | (s, DEFINITION(f1, f2)) -> (string_of_int s) ^ ": " ^ (exportFormula f1) ^ " := " ^ (exportFormula f2)
1528

    
1529

    
1530
(** Destructs a nominal.
1531
    @param s the input stream
1532
    @return (tbox, query) in simplifyed nnf
1533
*)
1534
let importAxiomQuery s =
1535
  let fkt ts =
1536
    let rec parse_sortedAxiomList ts acc =
1537
      let nr = 
1538
        match Stream.peek ts with
1539
        | Some (A.Int n) ->
1540
            if n >= 0 then begin
1541
              Stream.junk ts;
1542
              let () =
1543
                match Stream.next ts with
1544
                | A.Kwd ":" -> ()
1545
                | t -> A.printError mk_exn ~t ~ts ("\":\" expected: ")
1546
              in
1547
              n
1548
            end else
1549
              A.printError mk_exn ~ts ("<non-negative number> expected: ")
1550
        | _ -> 0 
1551
      in
1552
      let f1 = simplify (nnf (parse_formula [] ts)) in
1553
      let f = match Stream.peek ts with
1554
      | Some (A.Kwd ":=") ->
1555
        Stream.junk ts;
1556
        (nr, DEFINITION(f1, simplify (nnf (parse_formula [] ts))))
1557
      | Some (A.Kwd "[=") ->
1558
        Stream.junk ts;
1559
        (nr, INCLUSION(f1, simplify (nnf (parse_formula [] ts))))
1560
      | _ -> raise (CoAlgException "Exception parse_sortedAxiomList")
1561
      in
1562
      match Stream.peek ts with
1563
      | Some (A.Kwd ";") ->
1564
        Stream.junk ts;
1565
        parse_sortedAxiomList ts (f::acc)
1566
      | _ -> List.rev (f :: acc)
1567
    in
1568
    match Stream.peek ts with
1569
    | Some (A.Kwd "|-") ->
1570
      Stream.junk ts;
1571
      ([], parse_sortedAxiomList ts [])
1572
    | _ ->
1573
      let fl = parse_sortedAxiomList ts [] in
1574
      if Stream.peek ts = Some (A.Kwd "|-")
1575
      then begin
1576
        Stream.junk ts;
1577
        (fl, parse_sortedAxiomList ts [])
1578
      end else ([], fl)
1579
  in
1580
  importWrapper fkt s
1581

    
1582
(** Destructs an atomic proposition.
1583
    @param f An atomic proposition.
1584
    @return The name of the atomic proposition.
1585
    @raise CoAlgException if f is not an atomic proposition.
1586
 *)
1587
let dest_ap f =
1588
  match f with
1589
  | AP s when not (isNominal s) -> s
1590
  | _ -> raise (CoAlgException "Formula is not an atomic proposition.")
1591

    
1592
(** Destructs a nominal.
1593
    @param f A nominal.
1594
    @return The name of the nominal
1595
    @raise CoAlgException if f is not a nominal.
1596
 *)
1597
let dest_nom f =
1598
  match f with
1599
  | AP s when isNominal s -> s
1600
  | _ -> raise (CoAlgException "Formula is not a nominal.")
1601

    
1602
(** Destructs a negation.
1603
    @param f A negation.
1604
    @return The immediate subformula of the negation.
1605
    @raise CoAlgException if f is not a negation.
1606
 *)
1607
let dest_not f =
1608
  match f with
1609
  | NOT f1 -> f1
1610
  | _ -> raise (CoAlgException "Formula is not a negation.")
1611

    
1612
(** Destructs an @-formula.
1613
    @param f An @-formula.
1614
    @return The name of the nominal and the immediate subformula of the @-formula.
1615
    @raise CoAlgException if f is not an @-formula.
1616
 *)
1617
let dest_at f =
1618
  match f with
1619
  | AT (s, f1) -> (s, f1)
1620
  | _ -> raise (CoAlgException "Formula is not an @-formula.")
1621

    
1622
(** Destructs an or-formula.
1623
    @param f An or-formula.
1624
    @return The two immediate subformulae of the or-formula.
1625
    @raise CoAlgException if f is not an or-formula.
1626
 *)
1627
let dest_or f =
1628
  match f with
1629
  | OR (f1, f2) -> (f1, f2)
1630
  | _ -> raise (CoAlgException "Formula is not an or-formula.")
1631

    
1632
(** Destructs an and-formula.
1633
    @param f An and-formula.
1634
    @return The two immediate subformulae of the and-formula.
1635
    @raise CoAlgException if f is not an and-formula.
1636
 *)
1637
let dest_and f =
1638
  match f with
1639
  | AND (f1, f2) -> (f1, f2)
1640
  | _ -> raise (CoAlgException "Formula is not an and-formula.")
1641

    
1642
(** Destructs an equivalence.
1643
    @param f An equivalence.
1644
    @return The two immediate subformulae of the equivalence.
1645
    @raise CoAlgException if f is not an equivalence.
1646
 *)
1647
let dest_equ f =
1648
  match f with
1649
  | EQU (f1, f2) -> (f1, f2)
1650
  | _ -> raise (CoAlgException "Formula is not an equivalence.")
1651

    
1652
(** Destructs an implication.
1653
    @param f An implication.
1654
    @return The two immediate subformulae of the implication.
1655
    @raise CoAlgException if f is not an implication.
1656
 *)
1657
let dest_imp f =
1658
  match f with
1659
  | IMP (f1, f2) -> (f1, f2)
1660
  | _ -> raise (CoAlgException "Formula is not an implication.")
1661

    
1662
(** Destructs an EX-formula.
1663
    @param f An EX-formula.
1664
    @return The role name and the immediate subformula of the EX-formula.
1665
    @raise CoAlgException if f is not an EX-formula.
1666
 *)
1667
let dest_ex f =
1668
  match f with
1669
  | EX (s, f1) -> (s, f1)
1670
  | _ -> raise (CoAlgException "Formula is not an EX-formula.")
1671

    
1672
(** Destructs an AX-formula.
1673
    @param f An AX-formula.
1674
    @return The role name and the immediate subformula of the AX-formula.
1675
    @raise CoAlgException if f is not an AX-formula.
1676
 *)
1677
let dest_ax f =
1678
  match f with
1679
  | AX (s, f1) -> (s, f1)
1680
  | _ -> raise (CoAlgException "Formula is not an AX-formula.")
1681

    
1682
(** Destructs a MIN-formula.
1683
    @param f A MIN-formula.
1684
    @return The number restriction, role name,
1685
    and the immediate subformula of the MIN-formula.
1686
    @raise CoAlgException if f is not a MIN-formula.
1687
 *)
1688
let dest_min f =
1689
  match f with
1690
  | MIN (n, s, f1) -> (n, s, f1)
1691
  | _ -> raise (CoAlgException "Formula is not a MIN-formula.")
1692

    
1693
(** Destructs a MAX-formula.
1694
    @param f A MAX-formula.
1695
    @return The number restriction, role name,
1696
    and the immediate subformula of the MAX-formula.
1697
    @raise CoAlgException if f is not a MAX-formula.
1698
 *)
1699
let dest_max f =
1700
  match f with
1701
  | MAX (n, s, f1) -> (n, s, f1)
1702
  | _ -> raise (CoAlgException "Formula is not a MAX-formula.")
1703

    
1704
(** Destructs a choice formula.
1705
    @param f A choice formula.
1706
    @return The two immediate subformulae of the choice formula.
1707
    @raise CoAlgException if f is not a choice formula.
1708
 *)
1709
let dest_choice f =
1710
  match f with
1711
  | CHC (f1, f2) -> (f1, f2)
1712
  | _ -> raise (CoAlgException "Formula is not a choice formula.")
1713

    
1714
(** Destructs a fusion formula.
1715
    @param f A fusion formula.
1716
    @return A pair (first, f1) where
1717
    first is true iff f is a first projection; and
1718
    f1 is the immediate subformulae of f.
1719
    @raise CoAlgException if f is not a fusion formula.
1720
 *)
1721
let dest_fusion f =
1722
  match f with
1723
  | FUS (first, f1) -> (first, f1)
1724
  | _ -> raise (CoAlgException "Formula is not a fusion formula.")
1725

    
1726

    
1727
(** Tests whether a formula is the constant True.
1728
    @param f A formula.
1729
    @return True iff f is the constant True.
1730
 *)
1731
let is_true f =
1732
  match f with
1733
  | TRUE -> true
1734
  | _ -> false
1735

    
1736
(** Tests whether a formula is the constant False.
1737
    @param f A formula.
1738
    @return True iff f is the constant False.
1739
 *)
1740
let is_false f =
1741
  match f with
1742
  | FALSE -> true
1743
  | _ -> false
1744

    
1745
(** Tests whether a formula is an atomic proposition.
1746
    @param f A formula.
1747
    @return True iff f is an atomic proposition.
1748
 *)
1749
let is_ap f =
1750
  match f with
1751
  | AP s when not (isNominal s) -> true
1752
  | _ -> false
1753

    
1754
(** Tests whether a formula is a nominal.
1755
    @param f A formula.
1756
    @return True iff f is a nominal.
1757
 *)
1758
let is_nom f =
1759
  match f with
1760
  | AP s when isNominal s -> true
1761
  | _ -> false
1762

    
1763
(** Tests whether a formula is a negation.
1764
    @param f A formula.
1765
    @return True iff f is a negation.
1766
 *)
1767
let is_not f =
1768
  match f with
1769
  | NOT _ -> true
1770
  | _ -> false
1771

    
1772
(** Tests whether a formula is an @-formula.
1773
    @param f A formula.
1774
    @return True iff f is an @-formula.
1775
 *)
1776
let is_at f =
1777
  match f with
1778
  | AT _ -> true
1779
  | _ -> false
1780

    
1781
(** Tests whether a formula is an or-formula.
1782
    @param f A formula.
1783
    @return True iff f is an or-formula.
1784
 *)
1785
let is_or f =
1786
  match f with
1787
  | OR _ -> true
1788
  | _ -> false
1789

    
1790
(** Tests whether a formula is an and-formula.
1791
    @param f A formula.
1792
    @return True iff f is an and-formula.
1793
 *)
1794
let is_and f =
1795
  match f with
1796
  | AND _ -> true
1797
  | _ -> false
1798

    
1799
(** Tests whether a formula is an equivalence.
1800
    @param f A formula.
1801
    @return True iff f is an equivalence.
1802
 *)
1803
let is_equ f =
1804
  match f with
1805
  | EQU _ -> true
1806
  | _ -> false
1807

    
1808
(** Tests whether a formula is an implication.
1809
    @param f A formula.
1810
    @return True iff f is an implication.
1811
 *)
1812
let is_imp f =
1813
  match f with
1814
  | IMP _ -> true
1815
  | _ -> false
1816

    
1817
(** Tests whether a formula is an EX-formula.
1818
    @param f A formula.
1819
    @return True iff f is an EX-formula.
1820
 *)
1821
let is_ex f =
1822
  match f with
1823
  | EX _ -> true
1824
  | _ -> false
1825

    
1826
(** Tests whether a formula is an AX-formula.
1827
    @param f A formula.
1828
    @return True iff f is an AX-formula.
1829
 *)
1830
let is_ax f =
1831
  match f with
1832
  | AX _ -> true
1833
  | _ -> false
1834

    
1835
(** Tests whether a formula is a MIN-formula.
1836
    @param f A formula.
1837
    @return True iff f is a MIN-formula.
1838
 *)
1839
let is_min f =
1840
  match f with
1841
  | MIN _ -> true
1842
  | _ -> false
1843

    
1844
(** Tests whether a formula is a MAX-formula.
1845
    @param f A formula.
1846
    @return True iff f is a MAX-formula.
1847
 *)
1848
let is_max f =
1849
  match f with
1850
  | MAX _ -> true
1851
  | _ -> false
1852

    
1853
(** Tests whether a formula is a choice formula.
1854
    @param f A formula.
1855
    @return True iff f is a choice formula.
1856
 *)
1857
let is_choice f =
1858
  match f with
1859
  | CHC _ -> true
1860
  | _ -> false
1861

    
1862
(** Tests whether a formula is a fusion formula.
1863
    @param f A formula.
1864
    @return True iff f is a fusion formula.
1865
 *)
1866
let is_fusion f =
1867
  match f with
1868
  | FUS _ -> true
1869
  | _ -> false
1870

    
1871

    
1872
(** The constant True.
1873
 *)
1874
let const_true = TRUE
1875

    
1876
(** The constant False.
1877
 *)
1878
let const_false = FALSE
1879

    
1880
(** Constructs an atomic proposition.
1881
    @param s The name of the atomic proposition.
1882
    @return The atomic proposition with name s.
1883
    @raise CoAlgException if s is a nominal name.
1884
 *)
1885
let const_ap s =
1886
  if isNominal s then raise (CoAlgException "The name indicates a nominal.")
1887
  else AP s
1888

    
1889
(** Constructs a nominal.
1890
    @param s The name of the nominal.
1891
    @return A nominal with name s.
1892
    @raise CoAlgException if s is not a nominal name.
1893
 *)
1894
let const_nom s =
1895
  if isNominal s then AP s
1896
  else raise (CoAlgException "The name does not indicate a nominal.")
1897

    
1898
(** Negates a formula.
1899
    @param f A formula.
1900
    @return The negation of f.
1901
 *)
1902
let const_not f = NOT f
1903

    
1904
(** Constructs an @-formula from a name and a formula.
1905
    @param s A nominal name.
1906
    @param f A formula.
1907
    @return The formula AT (s, f).
1908
 *)
1909
let const_at s f = AT (s, f)
1910

    
1911
(** Constructs an or-formula from two formulae.
1912
    @param f1 The first formula (LHS).
1913
    @param f2 The second formula (LHS).
1914
    @return The formula f1 | f2.
1915
 *)
1916
let const_or f1 f2 = OR (f1, f2)
1917

    
1918
(** Constructs an and-formula from two formulae.
1919
    @param f1 The first formula (LHS).
1920
    @param f2 The second formula (LHS).
1921
    @return The formula f1 & f2.
1922
 *)
1923
let const_and f1 f2 = AND (f1, f2)
1924

    
1925
(** Constructs an equivalence from two formulae.
1926
    @param f1 The first formula (LHS).
1927
    @param f2 The second formula (LHS).
1928
    @return The equivalence f1 <=> f2.
1929
 *)
1930
let const_equ f1 f2 = EQU (f1, f2)
1931

    
1932
(** Constructs an implication from two formulae.
1933
    @param f1 The first formula (LHS).
1934
    @param f2 The second formula (LHS).
1935
    @return The implication f1 => f2.
1936
 *)
1937
let const_imp f1 f2 = IMP (f1, f2)
1938

    
1939
(** Constructs an EX-formula from a formula.
1940
    @param s A role name.
1941
    @param f A formula.
1942
    @return The formula EX (s, f).
1943
 *)
1944
let const_ex s f = EX (s, f)
1945

    
1946
(** Constructs an AX-formula from a formula.
1947
    @param s A role name.
1948
    @param f A formula.
1949
    @return The formula AX (s, f).
1950
 *)
1951
let const_ax s f = AX (s, f)
1952

    
1953
(** Constructs a MIN-formula from a formula.
1954
    @param n A non-negative integer.
1955
    @param s A role name.
1956
    @param f A formula.
1957
    @return The formula MIN f.
1958
    @raise CoAlgException Iff n is negative.
1959
 *)
1960
let const_min n s f =
1961
  if n < 0 then raise (CoAlgException "Negative cardinality constraint.")
1962
  else MIN (n, s, f)
1963

    
1964
(** Constructs a MAX-formula from a formula.
1965
    @param n A non-negative integer.
1966
    @param s A role name.
1967
    @param f A formula.
1968
    @return The formula MAX f.
1969
    @raise CoAlgException Iff n is negative.
1970
 *)
1971
let const_max n s f =
1972
  if n < 0 then raise (CoAlgException "Negative cardinality constraint.")
1973
  else MAX (n, s, f)
1974

    
1975
let const_enforces p f =
1976
    ENFORCES (p,f)
1977

    
1978
let const_allows p f =
1979
    ALLOWS (p,f)
1980

    
1981
(** Constructs a choice formula from two formulae.
1982
    @param f1 The first formula (LHS).
1983
    @param f2 The second formula (LHS).
1984
    @return The formula (f1 + f2).
1985
 *)
1986
let const_choice f1 f2 = CHC (f1, f2)
1987

    
1988
(** Constructs a fusion formula.
1989
    @param first True iff the result is a first projection.
1990
    @param f1 A formula.
1991
    @return The formula [pi1] f1 or [pi2] f1 (depending on first).
1992
 *)
1993
let const_fusion first f1 = FUS (first, f1)
1994

    
1995

    
1996
(** Hash-consed formulae, which are in negation normal form,
1997
    such that structural and physical equality coincide.
1998

    
1999
    Also CTL has been replaced by the equivalent μ-Calculus
2000
    constructs
2001
 *)
2002
type hcFormula = (hcFormula_node, formula) HC.hash_consed
2003
and hcFormula_node =
2004
  | HCTRUE
2005
  | HCFALSE
2006
  | HCAP of string
2007
  | HCNOT of string
2008
  | HCAT of string * hcFormula
2009
  | HCOR of hcFormula * hcFormula
2010
  | HCAND of hcFormula * hcFormula
2011
  | HCEX of string * hcFormula
2012
  | HCAX of string * hcFormula
2013
  | HCENFORCES of int list * hcFormula
2014
  | HCALLOWS of int list * hcFormula
2015
  | HCMORETHAN of int * string * hcFormula (* GML Diamond *)
2016
  | HCMAXEXCEPT of int * string * hcFormula (* GML Box *)
2017
  | HCATLEASTPROB of rational * hcFormula
2018
  | HCLESSPROBFAIL of rational * hcFormula
2019
  | HCCONST of string
2020
  | HCCONSTN of string
2021
  | HCID of hcFormula
2022
  | HCNORM of hcFormula * hcFormula
2023
  | HCNORMN of hcFormula * hcFormula
2024
  | HCCHC of hcFormula * hcFormula
2025
  | HCFUS of bool * hcFormula
2026
  | HCMU of string * hcFormula
2027
  | HCNU of string * hcFormula
2028
  | HCVAR of string
2029

    
2030
(** Determines whether two formula nodes are structurally equal.
2031
    @param f1 The first formula node.
2032
    @param f2 The second formula node.
2033
    @return True iff f1 and f2 are structurally equal.
2034
 *)
2035
let equal_hcFormula_node f1 f2 =
2036
  match f1, f2 with
2037
  | HCTRUE, HCTRUE -> true
2038
  | HCFALSE, HCFALSE -> true
2039
  | HCCONST s1, HCCONST s2
2040
  | HCCONSTN s1, HCCONSTN s2
2041
  | HCAP s1, HCAP s2
2042
  | HCNOT s1, HCNOT s2 -> compare s1 s2 = 0
2043
  | HCAT (s1, f1), HCAT (s2, f2) -> compare s1 s2 = 0 && f1 == f2
2044
  | HCOR (f1a, f1b), HCOR (f2a, f2b)
2045
  | HCAND (f1a, f1b), HCAND (f2a, f2b) -> f1a == f2a && f1b == f2b
2046
  | HCEX (s1, f1), HCEX (s2, f2)
2047
  | HCAX (s1, f1), HCAX (s2, f2) -> compare s1 s2 = 0 && f1 == f2
2048
  | HCENFORCES (s1, f1), HCENFORCES (s2, f2)
2049
  | HCALLOWS (s1, f1), HCALLOWS (s2, f2) -> compare s1 s2 = 0 && f1 == f2
2050
  | HCMORETHAN (n1, s1, f1), HCMORETHAN (n2, s2, f2)
2051
  | HCMAXEXCEPT (n1, s1, f1), HCMAXEXCEPT (n2, s2, f2) ->
2052
      n1 = n2 && compare s1 s2 = 0 && f1 == f2
2053
  | HCATLEASTPROB (p1, f1), HCATLEASTPROB (p2,f2) ->
2054
      p1 = p2 && f1 == f2
2055
  | HCLESSPROBFAIL (p1, f1), HCLESSPROBFAIL (p2,f2) ->
2056
      p1 = p2 && f1 == f2
2057
  | HCID f1, HCID f2 -> f1 == f2
2058
  | HCNORM (f1a, f1b), HCNORMN (f2a, f2b) -> f1a == f2a && f1b == f2b
2059
  | HCCHC (f1a, f1b), HCCHC (f2a, f2b) -> f1a == f2a && f1b == f2b
2060
  | HCFUS (first1, f1), HCFUS (first2, f2) -> first1 = first2 && f1 == f2
2061
  | HCMU (name1, f1), HCMU(name2, f2) -> compare name1 name2 = 0 && f1 == f2
2062
  | HCNU (name1, f1), HCNU(name2, f2) -> compare name1 name2 = 0 && f1 == f2
2063
  | HCVAR name1, HCVAR name2 -> compare name1 name2 = 0
2064
(* The rest could be shortened to | _ -> false,
2065
   but then the compiler would not warn if the formula type is extended
2066
   and this function is not updated accordingly.*)
2067
  | HCTRUE, _
2068
  | HCFALSE, _
2069
  | HCAP _, _
2070
  | HCNOT _, _
2071
  | HCAT _, _
2072
  | HCOR _, _
2073
  | HCAND _, _
2074
  | HCEX _, _
2075
  | HCAX _, _
2076
  | HCENFORCES _, _
2077
  | HCALLOWS   _, _
2078
  | HCMORETHAN _, _
2079
  | HCMAXEXCEPT _, _
2080
  | HCATLEASTPROB _, _
2081
  | HCLESSPROBFAIL _, _
2082
  | HCCONST _, _
2083
  | HCCONSTN _, _
2084
  | HCID _, _
2085
  | HCNORM _, _
2086
  | HCNORMN _, _
2087
  | HCCHC _, _
2088
  | HCFUS _, _
2089
  | HCMU _, _
2090
  | HCNU _, _
2091
  | HCVAR _, _ -> false
2092

    
2093
(** Computes the hash value of a formula node.
2094
    @param f A formula node.
2095
    @return The hash value of f.
2096
 *)
2097
let hash_hcFormula_node f =
2098
  let base = 23 in (* should be larger than the no of constructors *)
2099
  match f with
2100
  | HCTRUE -> 0
2101
  | HCFALSE -> 1
2102
  | HCAP s
2103
  | HCNOT s
2104
  | HCVAR s -> base * Hashtbl.hash s + 1
2105
  | HCAT (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 2
2106
  | HCOR (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 5
2107
  | HCAND (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 6
2108
  | HCEX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 3
2109
  | HCAX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 4
2110
  | HCMORETHAN (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 7
2111
  | HCMAXEXCEPT (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 8
2112
  | HCATLEASTPROB (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 9
2113
  | HCLESSPROBFAIL (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 10
2114
  | HCCHC (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 11
2115
  | HCFUS (first, f1) -> base * (base * (Hashtbl.hash first) + f1.HC.hkey) + 13
2116
  | HCENFORCES (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 14
2117
  | HCALLOWS   (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 15
2118
  | HCCONST s -> Hashtbl.hash s + 16
2119
  | HCCONSTN s -> Hashtbl.hash s + 17
2120
  | HCNORM (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 18
2121
  | HCNORMN (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 19
2122
  | HCID (f1) -> base * f1.HC.hkey + 20
2123
  | HCMU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 21
2124
  | HCNU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 22
2125

    
2126
(** Determines the "real" formula of a formula node.
2127
    @param f A formula node.
2128
    @return The formula (in negation normal form) which corresponds to f.
2129
 *)
2130
let toFml_hcFormula_node f =
2131
  match f with
2132
  | HCTRUE -> TRUE
2133
  | HCFALSE -> FALSE
2134
  | HCAP s -> AP s
2135
  | HCVAR s -> VAR s
2136
  | HCNOT s -> NOT (AP s)
2137
  | HCAT (s, f1) -> AT (s, f1.HC.fml)
2138
  | HCOR (f1, f2) -> OR (f1.HC.fml, f2.HC.fml)
2139
  | HCAND (f1, f2) -> AND (f1.HC.fml, f2.HC.fml)
2140
  | HCEX (s, f1) -> EX (s, f1.HC.fml)
2141
  | HCAX (s, f1) -> AX (s, f1.HC.fml)
2142
  | HCENFORCES (s, f1) -> ENFORCES (s, f1.HC.fml)
2143
  | HCALLOWS (s, f1) -> ALLOWS (s, f1.HC.fml)
2144
  | HCMORETHAN (n, s, f1) -> MORETHAN (n, s, f1.HC.fml)
2145
  | HCMAXEXCEPT (n, s, f1) -> MAXEXCEPT (n, s, f1.HC.fml)
2146
  | HCATLEASTPROB (p, f1) -> ATLEASTPROB (p, f1.HC.fml)
2147
  | HCLESSPROBFAIL (p, f1) -> LESSPROBFAIL (p, f1.HC.fml)
2148
  | HCCONST s -> CONST s
2149
  | HCCONSTN s -> CONSTN s
2150
  | HCID (f1) -> ID(f1.HC.fml)
2151
  | HCNORM (f1, f2) -> NORM(f1.HC.fml, f2.HC.fml)
2152
  | HCNORMN (f1, f2) -> NORMN(f1.HC.fml, f2.HC.fml)
2153
  | HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml)
2154
  | HCFUS (first, f1) -> FUS (first, f1.HC.fml)
2155
  | HCMU (var, f1) -> MU (var, f1.HC.fml)
2156
  | HCNU (var, f1) -> NU (var, f1.HC.fml)
2157

    
2158
(** Determines the negation (in negation normal form) of a formula node.
2159
    @param f A formula node.
2160
    @return The negation (in negation normal form) of f.
2161
 *)
2162
let negNde_hcFormula_node f =
2163
  match f with
2164
  | HCTRUE -> HCFALSE
2165
  | HCFALSE -> HCTRUE
2166
  | HCAP s -> HCNOT s
2167
  | HCNOT s -> HCAP s
2168
  | HCVAR s -> f
2169
  | HCAT (s, f1) -> HCAT (s, f1.HC.neg)
2170
  | HCOR (f1, f2) -> HCAND (f1.HC.neg, f2.HC.neg)
2171
  | HCAND (f1, f2) -> HCOR (f1.HC.neg, f2.HC.neg)
2172
  | HCEX (s, f2) -> HCAX (s, f2.HC.neg)
2173
  | HCAX (s, f2) -> HCEX (s, f2.HC.neg)
2174
  | HCENFORCES (s, f2) -> HCALLOWS (s, f2.HC.neg)
2175
  | HCALLOWS (s, f2) -> HCENFORCES (s, f2.HC.neg)
2176
  | HCMORETHAN (n, s, f1) -> HCMAXEXCEPT (n, s, f1.HC.neg)
2177
  | HCMAXEXCEPT (n, s, f1) -> HCMORETHAN (n, s, f1.HC.neg)
2178
  | HCATLEASTPROB (p, f1) -> HCLESSPROBFAIL (p, f1.HC.neg)
2179
  | HCLESSPROBFAIL (p, f1) -> HCATLEASTPROB (p, f1.HC.neg)
2180
  | HCCONST s -> HCCONSTN s
2181
  | HCCONSTN s -> HCCONST s
2182
  | HCID (f1) -> HCID(f1.HC.neg)
2183
  | HCNORM (f1, f2) -> HCNORMN(f1.HC.neg, f2.HC.neg)
2184
  | HCNORMN (f1, f2) -> HCNORM(f1.HC.neg, f2.HC.neg)
2185
  | HCCHC (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg)
2186
  | HCFUS (first, f1) -> HCFUS (first, f1.HC.neg)
2187
  | HCMU (name, f1) -> HCNU (name, f1.HC.neg)
2188
  | HCNU (name, f1) -> HCMU (name, f1.HC.neg)
2189

    
2190
(** An instantiation of hash-consing for formulae.
2191
 *)
2192
module HcFormula = HC.Make(
2193
  struct
2194
    type nde = hcFormula_node
2195
    type fml = formula
2196
    let equal (n1 : nde) n2 = equal_hcFormula_node n1 n2
2197
    let hash (n : nde) = hash_hcFormula_node n
2198
    let negNde (n : nde) = negNde_hcFormula_node n
2199
    let toFml (n : nde) = toFml_hcFormula_node n
2200
  end
2201
 )
2202

    
2203
(** Converts a formula into its hash-consed version.
2204
    @param hcF A hash-cons table for formulae.
2205
    @param f A formula in negation normal form.
2206
    @return The hash-consed version of f.
2207
    @raise CoAlgException if f is not in negation normal form.
2208
*)
2209
let rec hc_formula hcF f =
2210
  match f with
2211
  | TRUE -> HcFormula.hashcons hcF HCTRUE
2212
  | FALSE -> HcFormula.hashcons hcF HCFALSE
2213
  | AP s -> HcFormula.hashcons hcF (HCAP s)
2214
  | VAR s -> HcFormula.hashcons hcF (HCVAR s)
2215
  | NOT (AP s) -> HcFormula.hashcons hcF (HCNOT s)
2216
  | AT (s, f1) ->
2217
      let tf1 = hc_formula hcF f1 in
2218
      HcFormula.hashcons hcF (HCAT (s, tf1))
2219
  | OR (f1, f2) ->
2220
      let tf1 = hc_formula hcF f1 in
2221
      let tf2 = hc_formula hcF f2 in
2222
      HcFormula.hashcons hcF (HCOR (tf1, tf2))
2223
  | AND (f1, f2) ->
2224
      let tf1 = hc_formula hcF f1 in
2225
      let tf2 = hc_formula hcF f2 in
2226
      HcFormula.hashcons hcF (HCAND (tf1, tf2))
2227
  | NOT _
2228
  | EQU _
2229
  | MIN _
2230
  | MAX _
2231
  | IMP _ -> raise (CoAlgException "Formula is not in negation normal form.")
2232
  | EX (s, f1) ->
2233
      let tf1 = hc_formula hcF f1 in
2234
      HcFormula.hashcons hcF (HCEX (s, tf1))
2235
  | AX (s, f1) ->
2236
      let tf1 = hc_formula hcF f1 in
2237
      HcFormula.hashcons hcF (HCAX (s, tf1))
2238
  | ENFORCES (s, f1) ->
2239
      let tf1 = hc_formula hcF f1 in
2240
      HcFormula.hashcons hcF (HCENFORCES (s, tf1))
2241
  | ALLOWS (s, f1) ->
2242
      let tf1 = hc_formula hcF f1 in
2243
      HcFormula.hashcons hcF (HCALLOWS (s, tf1))
2244
  | MORETHAN  (n, s, f1) ->
2245
      let tf1 = hc_formula hcF f1 in
2246
      HcFormula.hashcons hcF (HCMORETHAN (n, s, tf1))
2247
  | MAXEXCEPT  (n, s, f1) ->
2248
      let tf1 = hc_formula hcF f1 in
2249
      HcFormula.hashcons hcF (HCMAXEXCEPT (n, s, tf1))
2250
  | ATLEASTPROB (p, f1) ->
2251
      HcFormula.hashcons hcF (HCATLEASTPROB (p, hc_formula hcF f1))
2252
  | LESSPROBFAIL (p, f1) ->
2253
      HcFormula.hashcons hcF (HCLESSPROBFAIL (p, hc_formula hcF f1))
2254
  | CONST s ->
2255
      HcFormula.hashcons hcF (HCCONST s)
2256
  | CONSTN s ->
2257
      HcFormula.hashcons hcF (HCCONSTN s)
2258
  | ID f1 ->
2259
    let tf1 = hc_formula hcF f1 in
2260
      HcFormula.hashcons hcF (HCID tf1)
2261
  | NORM (f1, f2) ->
2262
      let tf1 = hc_formula hcF f1 in
2263
      let tf2 = hc_formula hcF f2 in
2264
      HcFormula.hashcons hcF (HCNORM (tf1, tf2))
2265
  | NORMN (f1, f2) ->
2266
      let tf1 = hc_formula hcF f1 in
2267
      let tf2 = hc_formula hcF f2 in
2268
      HcFormula.hashcons hcF (HCNORMN (tf1, tf2))
2269
  | CHC (f1, f2) ->
2270
      let tf1 = hc_formula hcF f1 in
2271
      let tf2 = hc_formula hcF f2 in
2272
      HcFormula.hashcons hcF (HCCHC (tf1, tf2))
2273
  | FUS (first, f1) ->
2274
      let tf1 = hc_formula hcF f1 in
2275
      HcFormula.hashcons hcF (HCFUS (first, tf1))
2276
  | MU (var, f1) ->
2277
     let tf1 = hc_formula hcF f1 in
2278
     HcFormula.hashcons hcF (HCMU (var, tf1))
2279
  | NU (var, f1) ->
2280
     let tf1 = hc_formula hcF f1 in
2281
     HcFormula.hashcons hcF (HCNU (var, tf1))
2282
  | AF _ | EF _
2283
  | AG _ | EG _
2284
  | AU _ | EU _
2285
  | AR _ | ER _
2286
  | AB _ | EB _ ->
2287
     raise (CoAlgException ("nnf: CTL should have been removed at this point"))
2288

    
2289
(* Replace the Variable name in f with formula formula
2290
   hc_replace foo φ ψ => ψ[foo |-> φ]
2291
 *)
2292
let rec hc_replace hcF name (formula: hcFormula) (f: hcFormula) =
2293
  let func = hc_replace hcF name formula in
2294
  let gennew = HcFormula.hashcons hcF in
2295
  match f.HC.node with
2296
  | HCTRUE
2297
  | HCFALSE
2298
  | HCAP _
2299
  | HCNOT _
2300
  | HCCONST _
2301
  | HCCONSTN _ -> f
2302
  | HCVAR s ->
2303
     if compare s name == 0
2304
     then formula
2305
     else f
2306
  | HCAT (s, f1) ->
2307
     let nf1 = func f1 in
2308
     if nf1 == f1 then f else gennew (HCAT(s, nf1))
2309
  | HCOR (f1, f2) ->
2310
     let nf1 = func f1 in
2311
     let nf2 = func f2 in
2312
     if nf1 == f1 && nf2 == f2 then f else gennew (HCOR(nf1, nf2))
2313
  | HCAND (f1, f2) ->
2314
     let nf1 = func f1 in
2315
     let nf2 = func f2 in
2316
     if nf1 == f1 && nf2 == f2 then f else gennew (HCAND(nf1, nf2))
2317
  | HCEX (s, f1) ->
2318
     let nf1 = func f1 in
2319
     if nf1 == f1 then f else gennew (HCEX(s, nf1))
2320
  | HCAX (s, f1) ->
2321
     let nf1 = func f1 in
2322
     if nf1 == f1 then f else gennew (HCAX(s, nf1))
2323
  | HCENFORCES (s, f1) ->
2324
     let nf1 = func f1 in
2325
     if nf1 == f1 then f else gennew (HCENFORCES(s, nf1))
2326
  | HCALLOWS (s, f1) ->
2327
     let nf1 = func f1 in
2328
     if nf1 == f1 then f else gennew (HCALLOWS(s, nf1))
2329
  | HCMORETHAN  (n, s, f1) ->
2330
     let nf1 = func f1 in
2331
     if nf1 == f1 then f else gennew (HCMORETHAN(n, s, nf1))
2332
  | HCMAXEXCEPT  (n, s, f1) ->
2333
     let nf1 = func f1 in
2334
     if nf1 == f1 then f else gennew (HCMAXEXCEPT(n, s, nf1))
2335
  | HCATLEASTPROB (p, f1) ->
2336
     let nf1 = func f1 in
2337
     if nf1 == f1 then f else gennew (HCATLEASTPROB(p, nf1))
2338
  | HCLESSPROBFAIL (p, f1) ->
2339
     let nf1 = func f1 in
2340
     if nf1 == f1 then f else gennew (HCLESSPROBFAIL(p, nf1))
2341
  | HCID f1 ->
2342
     let nf1 = func f1 in
2343
     if nf1 == f1 then f else gennew (HCID(nf1))
2344
  | HCNORM (f1, f2) ->
2345
     let nf1 = func f1 in
2346
     let nf2 = func f2 in
2347
     if nf1 == f1 && nf2 == f2 then f else gennew (HCNORM(nf1, nf2))
2348
  | HCNORMN (f1, f2) ->
2349
     let nf1 = func f1 in
2350
     let nf2 = func f2 in
2351
     if nf1 == f1 && nf2 == f2 then f else gennew (HCNORMN(nf1, nf2))
2352
  | HCCHC (f1, f2) ->
2353
     let nf1 = func f1 in
2354
     let nf2 = func f2 in
2355
     if nf1 == f1 && nf2 == f2 then f else gennew (HCCHC(nf1, nf2))
2356
  | HCFUS (first, f1) ->
2357
     let nf1 = func f1 in
2358
     if nf1 == f1 then f else gennew (HCFUS(first, nf1))
2359
  | HCMU (var, f1) ->
2360
     if compare var name != 0 then
2361
       let nf1 = func f1 in
2362
       if nf1 == f1 then f else gennew (HCMU(var, nf1))
2363
     else
2364
       f
2365
  | HCNU (var, f1) ->
2366
     if compare var name != 0 then
2367
       let nf1 = func f1 in
2368
       if nf1 == f1 then f else gennew (HCNU(var, nf1))
2369
     else
2370
       f
2371

    
2372
let rec hc_freeIn variable (f: hcFormula) =
2373
  match f.HC.node with
2374
  | HCTRUE
2375
  | HCFALSE
2376
  | HCAP _
2377
  | HCNOT _
2378
  | HCCONST _
2379
  | HCCONSTN _ -> false
2380
  | HCVAR s ->
2381
     if compare variable s == 0
2382
     then true
2383
     else false
2384
  | HCAT (s, f1) ->
2385
     hc_freeIn variable f1
2386
  | HCOR (f1, f2)
2387
  | HCAND (f1, f2) ->
2388
     hc_freeIn variable f1 || hc_freeIn variable f2
2389
  | HCEX (_, f1)
2390
  | HCAX (_, f1)
2391
  | HCENFORCES (_, f1)
2392
  | HCALLOWS (_, f1)
2393
  | HCMORETHAN  (_, _, f1)
2394
  | HCMAXEXCEPT  (_, _, f1)
2395
  | HCATLEASTPROB (_, f1)
2396
  | HCLESSPROBFAIL (_, f1)
2397
  | HCID f1 ->
2398
     hc_freeIn variable f1
2399
  | HCNORM (f1, f2)
2400
  | HCNORMN (f1, f2)
2401
  | HCCHC (f1, f2) ->
2402
     hc_freeIn variable f1 || hc_freeIn variable f2
2403
  | HCFUS (first, f1) ->
2404
     hc_freeIn variable f1
2405
  | HCMU (var, f1)
2406
  | HCNU (var, f1) ->
2407
     (* Do we need to exclude bound variables here? *)
2408
     hc_freeIn variable f1
2409

    
2410

    
2411
(** An instantiation of a hash table (of the standard library)
2412
    for hash-consed formulae. The test for equality
2413
    and computing the hash value is done in constant time.
2414
 *)
2415
module HcFHt = Hashtbl.Make(
2416
  struct
2417
    type t = hcFormula
2418
    let equal (f1 : t) f2 = f1.HC.tag = f2.HC.tag
2419
    let hash (f : t) = f.HC.tag
2420
  end
2421
 )