Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgFormula.ml @ bc0691dc

History | View | Annotate | Download (73.4 KB)

1
(** This module implements coalgebraic formulae
2
    (e.g. parsing, printing, (de-)constructing, ...).
3
    @author Florian Widmann
4
 *)
5

    
6

    
7
module HC = HashConsing
8
module A = AltGenlex
9
module L = List
10
module Str = String
11

    
12

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

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

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

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

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

    
30
(** Defines (unsorted) coalgebraic formulae.
31
 *)
32
type formula =
33
  | TRUE
34
  | FALSE
35
  | AP of string (* atomic proposition *)
36
  | NOT of formula
37
  | AT of string * formula
38
  | OR of formula * formula
39
  | AND of formula * formula
40
  | EQU of formula * formula
41
  | IMP of formula * formula
42
  | EX of string * formula
43
  | AX of string * formula
44
  | ENFORCES of int list * formula
45
  | ALLOWS   of int list * formula
46
  | MIN of int * string * formula
47
  | MAX of int * string * formula
48
  | MORETHAN of int * string * formula (* diamond of GML *)
49
  | MAXEXCEPT of int * string * formula (* box of GML *)
50
  | ATLEASTPROB of rational * formula (* = {>= 0.5} C  ---> C occurs with *)
51
                                      (*  probability of at least 50% *)
52
  | LESSPROBFAIL of rational * formula (* = [1/2] C = {< 1/2} ¬ C ---> C fails with *)
53
                                        (* probability of less than 50% *)
54
  | CONST of string  (* constant functor with value string *)
55
  | CONSTN of string  (* constant functor with value other than string *)
56
  | ID of formula (* modality of the identity functor *)
57
  | NORM of formula * formula (* default implication *)
58
  | NORMN of formula * formula (* \neg NORM (\neg A, \neg B) *)
59
  | CHC of formula * formula (* Choice is self-dual *)
60
  | FUS of bool * formula
61
  | MU of string * formula
62
  | NU of string * formula
63
  | VAR of string
64
  | AF of formula
65
  | EF of formula
66
  | AG of formula
67
  | EG of formula
68
  | AU of formula * formula
69
  | EU of formula * formula
70
  | AR of formula * formula
71
  | ER of formula * formula
72
  | AB of formula * formula
73
  | EB of formula * formula
74

    
75
exception ConversionException of formula
76

    
77

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

    
82

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

    
89

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

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

    
138

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

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

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

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

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

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

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

    
482

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

    
494
let string_of_formula = exportFormula
495

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

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

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

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

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

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

    
648

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

    
659
let mk_exn s = CoAlgException s
660

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

    
725

    
726
exception NotAconjunctive of unit
727

    
728
let isMuAconjunctive (formula:formula) : bool =
729
  let module SS = Set.Make(String) in
730

    
731
  (* Accepts formula f and a set of currently bound mu variables. Returns a subset
732
   * of those, which actually occured free in the formula.
733
   * Raises an CoAlgException if the formula is determined not to be aconjunctive *)
734
  let rec verifyMuAconjunctiveInternal (formula:formula) (bound_mu_vars: SS.t) : SS.t =
735
    let proc f = verifyMuAconjunctiveInternal f bound_mu_vars in
736
    match formula with
737
    | VAR s when SS.mem s bound_mu_vars -> SS.singleton s
738
    | VAR s                             -> SS.empty
739
    (* s is now bound by a nu and shadows any privious binding s *)
740
    | NU (s, a) -> verifyMuAconjunctiveInternal a (SS.remove s bound_mu_vars)
741
    (* Bind s in the recursive call but don't return it as occuring free *)
742
    | MU (s, a) ->
743
       SS.remove s (verifyMuAconjunctiveInternal a (SS.add s bound_mu_vars))
744

    
745
    (* This is the interesting case *)
746
    | AND (a, b) ->
747
       let a_vars = proc a in
748
       let b_vars = proc b in
749

    
750
       (* If both subformulas contain free mu variables, the formula is not aconjunctive *)
751
       if not (SS.is_empty a_vars) && not (SS.is_empty b_vars) then
752
         raise (NotAconjunctive ())
753
       else
754
         SS.union a_vars b_vars (* one of them is empty anyways *)
755

    
756
    (* The other cases just pass argument and return value through *)
757
    | TRUE | FALSE | AP _
758
    | CONST _ | CONSTN _ -> SS.empty
759
    | AT (_,a) | NOT a
760
    | EX (_,a) | AX (_,a) -> proc a
761
    | OR (a,b) | EQU (a,b) | IMP (a,b) -> SS.union (proc a) (proc b)
762
    | ENFORCES (_,a) | ALLOWS   (_,a)
763
    | MIN (_,_,a)    | MAX (_,_,a)
764
    | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
765
    | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
766
    | ID(a) -> proc a
767
    | NORM(a, b) | NORMN(a, b)
768
    | CHC (a,b)  -> SS.union (proc a) (proc b)
769
    | FUS (_,a) -> proc a
770
    | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ ->
771
       raise (CoAlgException ("verifyMuAconjunctiveInternal: CTL should have been removed at this point"))
772
  in
773
  try ignore (verifyMuAconjunctiveInternal formula SS.empty); true
774
  with NotAconjunctive () -> false
775

    
776
(** Process from outside in. For every variable bound keep the tuple
777
    (name, negations). For every negation crossed map a +1 over snd on
778
    that list. For every variable met check that the matching
779
    negations is even.
780
 *)
781
let rec verifyMuMonotone negations formula =
782
  let proc = verifyMuMonotone negations in
783
  match formula with
784
  | TRUE | FALSE | AP _ -> ()
785
  | CONST _
786
  | CONSTN _ -> ()
787
  | AT (_,a)
788
  | EX (_,a) | AX (_,a) -> proc a
789
  | OR (a,b) | AND (a,b)
790
  | EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
791
  | ENFORCES (_,a) | ALLOWS   (_,a)
792
  | MIN (_,_,a)    | MAX (_,_,a)
793
  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
794
  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
795
  | ID(a) -> proc a
796
  | NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
797
  | CHC (a,b)  -> (proc a ; proc b)
798
  | FUS (_,a) -> proc a
799
  | MU (s, f)
800
  | NU (s, f) ->
801
     let newNeg = (s, 0) :: negations in
802
     verifyMuMonotone newNeg f
803
  | VAR s ->
804
     let finder (x, _) = compare x s == 0 in
805
     let (_, neg) = List.find finder negations in
806
     if ((neg land 1) != 0) then raise (CoAlgException ("formula not monotone"))
807
  | NOT a ->
808
     let increment (s, n) = (s, n+1) in
809
     let newNeg = List.map increment negations in
810
     verifyMuMonotone newNeg a
811
  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ ->
812
     raise (CoAlgException ("verifyMuMonotone: CTL should have been removed at this point"))
813

    
814
let rec verifyMuGuarded unguarded formula =
815
  let proc = verifyMuGuarded unguarded in
816
  match formula with
817
  | TRUE | FALSE | AP _ -> ()
818
  | CONST _
819
  | CONSTN _ -> ()
820
  | AT (_,a) | NOT a -> proc a
821
  | EX (_,a) | AX (_,a) -> verifyMuGuarded [] a
822
  | OR (a,b) | AND (a,b)
823
  | EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
824
  | ENFORCES (_,a) | ALLOWS   (_,a)
825
  | MIN (_,_,a)    | MAX (_,_,a)
826
  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
827
  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> verifyMuGuarded [] a
828
  | ID(a) -> verifyMuGuarded [] a
829
  | NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
830
  | CHC (a,b)  -> (proc a ; proc b)
831
  | FUS (_,a) -> proc a
832
  | MU (s, f)
833
  | NU (s, f) ->
834
     let newUnguard = s :: unguarded in
835
     verifyMuGuarded newUnguard f
836
  | VAR s ->
837
     let finder x = compare x s == 0 in
838
     if List.exists finder unguarded then
839
       raise (CoAlgException ("formula not guarded"))
840
  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ ->
841
     raise (CoAlgException ("verifyMuGuarded: CTL should have been removed at this point"))
842

    
843
let verifyFormula formula =
844
  verifyMuAltFree formula;
845
  verifyMuMonotone [] formula;
846
  verifyMuGuarded [] formula
847

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

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

    
881
(** These functions parse a token stream to obtain a formula.
882
    It is a standard recursive descent procedure.
883
    @param ts A token stream.
884
    @return The resulting (sub-)formula.
885
    @raise CoAlgException if ts does not represent a formula.
886
 *)
887
and parse_or symtab ts =
888
  let f1 = parse_and symtab ts in
889
  match Stream.peek ts with
890
  | None -> f1
891
  | Some (A.Kwd "|") ->
892
      Stream.junk ts;
893
      let f2 = parse_or symtab ts in
894
      OR (f1, f2)
895
  | _ -> f1
896

    
897
(** These functions parse a token stream to obtain a formula.
898
    It is a standard recursive descent procedure.
899
    @param ts A token stream.
900
    @return The resulting (sub-)formula.
901
    @raise CoAlgException if ts does not represent a formula.
902
 *)
903
and parse_and symtab ts =
904
  let f1 = parse_cimp symtab ts in
905
  match Stream.peek ts with
906
  | None -> f1
907
  | Some (A.Kwd "&") ->
908
      Stream.junk ts;
909
      let f2 = parse_and symtab ts in
910
      AND (f1, f2)
911
  | _ -> f1
912

    
913
(** These functions parse a token stream to obtain a formula.
914
    It is a standard recursive descent procedure.
915
    @param ts A token stream.
916
    @return The resulting (sub-)formula.
917
    @raise CoAlgException if ts does not represent a formula.
918
 *)
919
and parse_cimp symtab ts =
920
  let f1 = parse_rest symtab ts in
921
  match Stream.peek ts with
922
  | None -> f1
923
  | Some (A.Kwd "=o") ->
924
      Stream.junk ts;
925
      let f2 = parse_cimp symtab ts in
926
      NORM (f1, f2)
927
  | _ -> f1
928

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

    
1138
(** Parses a sorted formula.
1139
    @param ts A token stream.
1140
    @return A sorted formula.
1141
    @raise CoAlgException If ts does not represent a sorted formula.
1142
 *)
1143
let parse_sortedFormula ts =
1144
  let nr =
1145
    match Stream.peek ts with
1146
    | Some (A.Int n) ->
1147
        if n >= 0 then begin
1148
          Stream.junk ts;
1149
          let () =
1150
            match Stream.next ts with
1151
            | A.Kwd ":" -> ()
1152
            | t -> A.printError mk_exn ~t ~ts ("\":\" expected: ")
1153
          in
1154
          n
1155
        end else
1156
          A.printError mk_exn ~ts ("<non-negative number> expected: ")
1157
    | _ -> 0
1158
  in
1159
  let f = parse_formula [] ts in
1160
  (nr, f)
1161

    
1162
(** Parses a list of sorted formulae separated by ";".
1163
    @param ts A token stream.
1164
    @param acc The list of sorted formulae parsed so far.
1165
    @return The resulting list of sorted formula.
1166
    @raise CoAlgException if ts does not represent a list of sorted formulae.
1167
 *)
1168
let rec parse_sortedFormulaList ts acc =
1169
  let f1 = parse_sortedFormula ts in
1170
  match Stream.peek ts with
1171
  | Some (A.Kwd ";") ->
1172
      Stream.junk ts;
1173
      parse_sortedFormulaList ts (f1::acc)
1174
  | _ -> List.rev (f1::acc)
1175

    
1176
(** A common wrapper for import functions.
1177
    @param fkt An import function.
1178
    @param s A string.
1179
    @return The object imported from s using fkt.
1180
    @raise CoAlgException If ts is not empty.
1181
 *)
1182
let importWrapper fkt s =
1183
  let ts = lexer s in
1184
  try
1185
    let res = fkt ts in
1186
    let _ =
1187
      match Stream.peek ts with
1188
      | None -> ()
1189
      | Some _ -> A.printError mk_exn ~ts "EOS expected: "
1190
    in
1191
    res
1192
  with Stream.Failure -> A.printError mk_exn ~ts "unexpected EOS"
1193

    
1194
(** Parses a string to obtain a formula.
1195
    @param s A string representing a formula.
1196
    @return The resulting formula.
1197
    @raise CoAlgException if s does not represent a formula.
1198
 *)
1199
let importFormula s = importWrapper (parse_formula []) s
1200

    
1201
(** Parses a string to obtain a sorted formula.
1202
    @param s A string representing a sorted formula.
1203
    @return The sorted formula.
1204
    @raise CoAlgException If s does not represent a sorted formula.
1205
 *)
1206
let importSortedFormula s = importWrapper parse_sortedFormula s
1207

    
1208
(** Parses a string to obtain a (sorted) formula query.
1209
    @param s A string representing a formula query.
1210
    @return A pair (tbox, f) where
1211
    tbox is a list of sorted formulae representing the TBox; and
1212
    f is a sorted formula.
1213
    @raise CoAlgException if s does not represent a formula query.
1214
 *)
1215
let importQuery s =
1216
  let fkt ts =
1217
    match Stream.peek ts with
1218
    | Some (A.Kwd "|-") ->
1219
        Stream.junk ts;
1220
        let f = parse_sortedFormula ts in
1221
        ([], f)
1222
    | _ ->
1223
        let fl = parse_sortedFormulaList ts [] in
1224
        match Stream.peek ts with
1225
        | Some (A.Kwd "|-") ->
1226
            Stream.junk ts;
1227
            let f = parse_sortedFormula ts in
1228
            (fl, f)
1229
        | _ ->
1230
            if List.length fl = 1 then ([], List.hd fl)
1231
            else A.printError mk_exn ~ts "\"|-\" expected: "
1232
  in
1233
  importWrapper fkt s
1234

    
1235

    
1236
(** Converts the negation of a formula to negation normal form
1237
    by "pushing in" the negations "~".
1238
    The symbols "<=>" and "=>" are substituted by their usual definitions.
1239
    @param f A formula.
1240
    @return A formula in negation normal form and not containing "<=>" or "=>"
1241
    that is equivalent to ~f.
1242
 *)
1243

    
1244
let rec equals f_1 f_2 =
1245
  match f_1, f_2 with
1246
  | TRUE, TRUE -> true 
1247
  | FALSE, FALSE -> true
1248
  | AP s1, AP s2 -> compare s1 s2 = 0
1249
  | VAR f1, VAR f2 -> compare f1 f2 = 0
1250
  | NOT f1, NOT f2 -> equals f1 f2
1251
  | AT(s1,f1), AT(s2,f2) -> (compare s1 s2 = 0) && (equals f1 f2)
1252
  | AND(f1,g1), AND(f2,g2) -> (equals f1 f2) && (equals g1 g2)
1253
  | OR(f1,g1), OR(f2,g2) -> (equals f1 f2) && (equals g1 g2)
1254
  | EQU(f1,g1), EQU(f2,g2) -> (equals f1 f2) && (equals g1 g2) 
1255
  | IMP(f1,g1), IMP(f2,g2) -> (equals f1 f2) && (equals g1 g2)
1256
  | EX(s1,g1), EX(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2)
1257
  | AX(s1,g1), AX(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2)
1258
  | ENFORCES(s1,g1), ENFORCES(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2)
1259
  | ALLOWS(s1,g1), ALLOWS(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2)
1260
  | MIN(n1,s1,g1), MIN(n2,s2,g2) -> (compare n1 n2 = 0) && (compare s1 s2 = 0) && (equals g1 g2)
1261
  | MAX(n1,s1,g1), MAX(n2,s2,g2) -> (compare n1 n2 = 0) && (compare s1 s2 = 0) && (equals g1 g2)
1262
  | MORETHAN(n1,s1,g1), MORETHAN(n2,s2,g2) -> (compare n1 n2 = 0) && (compare s1 s2 = 0) && (equals g1 g2)
1263
  | MAXEXCEPT(n1,s1,g1), MAXEXCEPT(n2,s2,g2) -> (compare n1 n2 = 0) && (compare s1 s2 = 0) && (equals g1 g2)
1264
  | ATLEASTPROB(p1,g1), ATLEASTPROB(p2,g2) -> (compare p1 p2 = 0) && (equals g1 g2)
1265
  | LESSPROBFAIL(p1,g1), LESSPROBFAIL(p2,g2) -> (compare p1 p2 = 0) && (equals g1 g2)
1266
  | CONST s1, CONST s2 -> compare s1 s2 = 0
1267
  | CONSTN s1, CONSTN s2 -> compare s1 s2 = 0
1268
  | ID(f1), ID(f2) -> equals f1 f2
1269
  | NORM(f1,g1),NORM(f2,g2) -> (equals f1 f2) && (equals g1 g2)
1270
  | NORMN(f1,g1), NORMN(f2,g2) -> (equals f1 f2) && (equals g1 g2)
1271
  | CHC(f1,g1), CHC(f2,g2) -> (equals f1 f2) && (equals g1 g2)
1272
  | FUS(b1,g1), FUS(b2,g2) -> (compare b1 b2 = 0) && (equals g1 g2)
1273
  | MU(s1,g1), MU(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2)
1274
  | NU(s1,g1),  NU(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2)
1275
  | _ -> false
1276

    
1277

    
1278
let rec nnfNeg f =
1279
  match f with
1280
  | TRUE -> FALSE
1281
  | FALSE -> TRUE
1282
  | AP _ -> NOT f
1283
  | VAR _ -> f
1284
  | NOT f1 -> nnf f1
1285
  | AT (s, f1) -> AT (s, nnfNeg f1)
1286
  | OR (f1, f2) -> AND (nnfNeg f1, nnfNeg f2)
1287
  | AND (f1, f2) -> OR (nnfNeg f1, nnfNeg f2)
1288
  | EQU (f1, f2) -> OR (AND (nnf f1, nnfNeg f2), AND (nnf f2, nnfNeg f1))
1289
  | IMP (f1, f2) -> AND (nnf f1, nnfNeg f2)
1290
  | EX (s, f1) -> AX (s, nnfNeg f1)
1291
  | AX (s, f1) -> EX (s, nnfNeg f1)
1292
  | ENFORCES (s, f1) -> ALLOWS (s, nnfNeg f1)
1293
  | ALLOWS (s, f1) -> ENFORCES (s, nnfNeg f1)
1294
  | MIN (n, s, f1) -> if n = 0 then FALSE else MAXEXCEPT (n-1, s, nnfNeg f1)
1295
  | MAX (n, s, f1) -> MORETHAN (n, s, nnf f1)
1296
  | MORETHAN (n, s, f1) -> MAXEXCEPT (n, s, nnfNeg f1)
1297
  | MAXEXCEPT (n, s, f1) -> MORETHAN (n, s, nnfNeg f1)
1298
  | ATLEASTPROB (p, f1) -> LESSPROBFAIL (p, nnfNeg f1)
1299
  | LESSPROBFAIL (p, f1) -> ATLEASTPROB (p, nnfNeg f1)
1300
  | CONST s -> CONSTN s
1301
  | CONSTN s -> CONST s
1302
  | ID (f1) -> ID (nnfNeg f1)
1303
  | NORM(f1, f2) -> NORMN(nnfNeg f1, nnfNeg f2)
1304
  | NORMN(f1, f2) -> NORM (nnfNeg f1, nnfNeg f2)
1305
  | CHC (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2)
1306
  | FUS (first, f1) -> FUS (first, nnfNeg f1)
1307
  | MU (s, f1) -> NU(s, nnfNeg f1)
1308
  | NU (s, f1) -> MU(s, nnfNeg f1)
1309
  | AF _ | EF _
1310
  | AG _ | EG _
1311
  | AU _ | EU _
1312
  | AR _ | ER _
1313
  | AB _ | EB _ -> raise (CoAlgException ("nnfNeg: CTL should have been removed at this point"))
1314

    
1315
(** Converts a formula to negation normal form
1316
    by "pushing in" the negations "~".
1317
    The symbols "<=>" and "=>" are substituted by their usual definitions.
1318
    @param f A formula.
1319
    @return A formula in negation normal form and not containing "<=>" or "=>"
1320
    that is equivalent to f.
1321
 *)
1322
and nnf f =
1323
  match f with
1324
  | TRUE
1325
  | FALSE
1326
  | AP _
1327
  | NOT (AP _)
1328
  | CONST _
1329
  | CONSTN _
1330
  | VAR _ -> f
1331
  | NOT f1 -> nnfNeg f1
1332
  | AT (s, f1) ->
1333
      let ft1 = nnf f1 in
1334
      if ft1 == f1 then f else AT (s, ft1)
1335
  | OR (f1, f2) ->
1336
      let ft1 = nnf f1 in
1337
      let ft2 = nnf f2 in
1338
      if ft1 == f1 && ft2 == f2 then f else OR (ft1, ft2)
1339
  | AND (f1, f2) ->
1340
      let ft1 = nnf f1 in
1341
      let ft2 = nnf f2 in
1342
      if ft1 == f1 && ft2 == f2 then f else AND (ft1, ft2)
1343
  | EQU (f1, f2) -> AND (OR (nnfNeg f1, nnf f2), OR (nnfNeg f2, nnf f1))
1344
  | IMP (f1, f2) -> OR (nnfNeg f1, nnf f2)
1345
  | EX (s, f1) ->
1346
      let ft = nnf f1 in
1347
      if ft == f1 then f else EX (s, ft)
1348
  | AX (s, f1) ->
1349
      let ft = nnf f1 in
1350
      if ft == f1 then f else AX (s, ft)
1351
  | ENFORCES (s, f1) ->
1352
      let ft = nnf f1 in
1353
      if ft == f1 then f else ENFORCES (s, ft)
1354
  | ALLOWS (s, f1) ->
1355
      let ft = nnf f1 in
1356
      if ft == f1 then f else ALLOWS (s, ft)
1357
  | MIN (n, s, f1) ->
1358
      if n = 0 then TRUE
1359
      else
1360
        let ft = nnf f1 in
1361
        MORETHAN (n-1,s,ft)
1362
  | MAX (n, s, f1) ->
1363
      let ft = nnfNeg f1 in
1364
      MAXEXCEPT (n,s, ft)
1365
  | MORETHAN (n,s,f1) ->
1366
      let ft = nnf f1 in
1367
      if ft = f1 then f else MORETHAN (n,s,ft)
1368
  | MAXEXCEPT (n,s,f1) ->
1369
      let ft = nnf f1 in
1370
      if ft = f1 then f else MAXEXCEPT (n,s,ft)
1371
  | ATLEASTPROB (p, f1) ->
1372
      let ft = nnf f1 in
1373
      if ft == f1 then f else ATLEASTPROB (p, ft)
1374
  | LESSPROBFAIL (p, f1) ->
1375
      let ft = nnf f1 in
1376
      if ft == f1 then f else LESSPROBFAIL (p, ft)
1377
  | ID (f1) ->
1378
    let ft = nnf f1 in
1379
    if ft == f1 then f else ID(ft)
1380
  | NORM (f1, f2) ->
1381
      let ft1 = nnf f1 in
1382
      let ft2 = nnf f2 in
1383
      if ft1 == f1 && ft2 == f2 then f else NORM (ft1, ft2)
1384
  | NORMN (f1, f2) ->
1385
      let ft1 = nnf f1 in
1386
      let ft2 = nnf f2 in
1387
      if ft1 == f1 && ft2 == f2 then f else NORMN (ft1, ft2)
1388
  | CHC (f1, f2) ->
1389
      let ft1 = nnf f1 in
1390
      let ft2 = nnf f2 in
1391
      if ft1 == f1 && ft2 == f2 then f else CHC (ft1, ft2)
1392
  | FUS (first, f1) ->
1393
      let ft = nnf f1 in
1394
      if ft == f1 then f else FUS (first, ft)
1395
  | MU (s, f1) ->
1396
      let ft = nnf f1 in
1397
      if ft == f1 then f else MU (s, ft)
1398
  | NU (s, f1) ->
1399
      let ft = nnf f1 in
1400
      if ft == f1 then f else NU (s, ft)
1401
  | AF _ | EF _
1402
  | AG _ | EG _
1403
  | AU _ | EU _
1404
  | AR _ | ER _
1405
  | AB _ | EB _ ->
1406
            raise (CoAlgException ("nnf: CTL should have been removed at this point"))
1407

    
1408
(** Simplifies a formula.
1409
    @param f A formula which must be in negation normal form.
1410
    @return A formula in negation normal form that is equivalent to f.
1411
    @raise CoAlgException if f is not in negation normal form.
1412
 *)
1413
let rec simplify f =
1414
  match f with
1415
  | TRUE
1416
  | FALSE
1417
  | AP _
1418
  | NOT (AP _)
1419
  | VAR _
1420
  | NOT (VAR _) -> f
1421
  | AT (s, f1) ->
1422
      let ft = simplify f1 in
1423
      begin
1424
        match ft with
1425
        | FALSE -> FALSE
1426
        | TRUE -> TRUE
1427
        | AT _ -> ft
1428
        | AP s1 when s = s1 -> TRUE
1429
        | NOT (AP s1) when s = s1 -> FALSE
1430
        | _ -> if ft == f1 then f else AT (s, ft)
1431
      end
1432
  | OR (f1, f2) ->
1433
      let ft1 = simplify f1 in
1434
      let ft2 = simplify f2 in
1435
      begin
1436
        match ft1, ft2 with
1437
        | TRUE, _ -> TRUE
1438
        | FALSE, _ -> ft2
1439
        | _, TRUE -> TRUE
1440
        | _, FALSE -> ft1
1441
        | _, _ ->
1442
            if (f1 == ft1) && (f2 == ft2) then f
1443
            else OR (ft1, ft2)
1444
      end
1445
  | AND (f1, f2) ->
1446
      let ft1 = simplify f1 in
1447
      let ft2 = simplify f2 in
1448
      begin
1449
        match ft1, ft2 with
1450
        | TRUE, _ -> ft2
1451
        | FALSE, _ -> FALSE
1452
        | _, TRUE -> ft1
1453
        | _, FALSE -> FALSE
1454
        | _, _ ->
1455
            if (f1 == ft1) && (f2 == ft2) then f
1456
            else AND (ft1, ft2)
1457
      end
1458
  | NOT _
1459
  | EQU _
1460
  | IMP _ -> raise (CoAlgException "Formula is not in negation normal form.")
1461
  | EX (s, f1) ->
1462
      let ft = simplify f1 in
1463
      begin
1464
        match ft with
1465
        | FALSE -> FALSE
1466
        | _ -> if ft == f1 then f else EX (s, ft)
1467
      end
1468
  | AX (s, f1) ->
1469
      let ft = simplify f1 in
1470
      begin
1471
        match ft with
1472
        | TRUE -> TRUE
1473
        | _ -> if ft == f1 then f else AX (s, ft)
1474
      end
1475
  | ENFORCES (s, f1) ->
1476
      let ft = simplify f1 in
1477
      begin
1478
        match ft with
1479
        (* Simplification rules are checked with dirks Generic.hs
1480
        let enforce ls = M (C ls)
1481
        let allow   ls = Neg . M (C ls) . Neg
1482
        provable $ F <-> enforce [1,2] F
1483
        *)
1484
        | TRUE -> TRUE
1485
        | FALSE -> FALSE
1486
        | _ -> if ft == f1 then f else ENFORCES (s, ft)
1487
      end
1488
  | ALLOWS (s, f1) ->
1489
      let ft = simplify f1 in
1490
      begin
1491
        match ft with
1492
        (* Simplification rules are checked with dirks Generic.hs
1493
        let enforce ls = M (C ls)
1494
        let allow   ls = Neg . M (C ls) . Neg
1495
        provable $ F <-> enforce [1,2] F
1496
        *)
1497
        | TRUE -> TRUE
1498
        | FALSE -> FALSE
1499
        | _ -> if ft == f1 then f else ALLOWS (s, ft)
1500
      end
1501
  | MIN (n, s, f1) ->
1502
      if n = 0 then TRUE
1503
      else
1504
        let ft = simplify f1 in
1505
        begin
1506
          match ft with
1507
          | FALSE -> FALSE
1508
          | _ -> if ft == f1 then f else MIN (n, s, ft)
1509
        end
1510
  | MORETHAN (n,s,f1) ->
1511
      let ft = simplify f1 in
1512
      if ft == f1 then f else MORETHAN (n,s,ft)
1513
  | MAXEXCEPT (n,s,f1) ->
1514
      let ft = simplify f1 in
1515
      if ft == f1 then f else MAXEXCEPT (n,s,ft)
1516
  | MAX (n, s, f1) ->
1517
      let ft = simplify f1 in
1518
      begin
1519
        match ft with
1520
        | FALSE -> TRUE
1521
        | _ -> if ft == f1 then f else MAX (n, s, ft)
1522
      end
1523
  | LESSPROBFAIL (p,f1) ->
1524
      let ft1 = simplify f1 in
1525
      if (ft1 == f1) then f else LESSPROBFAIL (p,ft1)
1526
  | ATLEASTPROB (p,f1) ->
1527
      let ft1 = simplify f1 in
1528
      if (ft1 == f1) then f else ATLEASTPROB (p,ft1)
1529
  | CONST _
1530
  | CONSTN _ -> f (* no simplifications possible *)
1531
  | ID (f1) ->
1532
    let ft1 = simplify f1 in
1533
    begin
1534
      match ft1 with
1535
        | TRUE -> TRUE
1536
        | FALSE -> FALSE
1537
        | _ -> if (ft1 == f1) then f else ID (ft1)
1538
    end
1539
  (* todo: more simplifications for KLM? *)
1540
  | NORM (f1, f2) ->
1541
      let ft1 = simplify f1 in
1542
      let ft2 = simplify f2 in
1543
      begin
1544
        match ft2 with
1545
          | TRUE -> TRUE
1546
          | _ ->
1547
            if (f1 == ft1) && (f2 == ft2) then f
1548
            else NORM (ft1, ft2)
1549
      end
1550
  | NORMN (f1, f2) ->
1551
      let ft1 = simplify f1 in
1552
      let ft2 = simplify f2 in
1553
      begin
1554
        match ft2 with
1555
          | FALSE -> FALSE
1556
          | _ ->
1557
            if (f1 == ft1) && (f2 == ft2) then f
1558
            else NORMN (ft1, ft2)
1559
      end
1560
  | CHC (f1, f2) ->
1561
      let ft1 = simplify f1 in
1562
      let ft2 = simplify f2 in
1563
      begin
1564
        match ft1, ft2 with
1565
        | TRUE, TRUE -> TRUE
1566
        | FALSE, FALSE -> FALSE
1567
        | _, _ ->
1568
            if (f1 == ft1) && (f2 == ft2) then f
1569
            else CHC (ft1, ft2)
1570
      end
1571
  | FUS (first, f1) ->
1572
      let ft = simplify f1 in
1573
      begin
1574
        match ft with
1575
        | FALSE -> FALSE
1576
        | TRUE -> TRUE
1577
        | _ -> if ft == f1 then f else FUS (first, ft)
1578
      end
1579
  | MU (s, f1) ->
1580
      let ft = simplify f1 in
1581
      begin
1582
        match ft with
1583
        | TRUE -> TRUE
1584
        | _ -> if ft == f1 then f else MU (s, ft)
1585
      end
1586
  | NU (s, f1) ->
1587
      let ft = simplify f1 in
1588
      begin
1589
        match ft with
1590
        | TRUE -> TRUE
1591
        | _ -> if ft == f1 then f else NU (s, ft)
1592
      end
1593
  | AF _ | EF _
1594
  | AG _ | EG _
1595
  | AU _ | EU _
1596
  | AR _ | ER _
1597
  | AB _ | EB _ ->
1598
            raise (CoAlgException ("nnf: CTL should have been removed at this point"))
1599

    
1600
(** Destructs an atomic proposition.
1601
    @param f An atomic proposition.
1602
    @return The name of the atomic proposition.
1603
    @raise CoAlgException if f is not an atomic proposition.
1604
 *)
1605
let dest_ap f =
1606
  match f with
1607
  | AP s when not (isNominal s) -> s
1608
  | _ -> raise (CoAlgException "Formula is not an atomic proposition.")
1609

    
1610
(** Destructs a nominal.
1611
    @param f A nominal.
1612
    @return The name of the nominal
1613
    @raise CoAlgException if f is not a nominal.
1614
 *)
1615
let dest_nom f =
1616
  match f with
1617
  | AP s when isNominal s -> s
1618
  | _ -> raise (CoAlgException "Formula is not a nominal.")
1619

    
1620
(** Destructs a negation.
1621
    @param f A negation.
1622
    @return The immediate subformula of the negation.
1623
    @raise CoAlgException if f is not a negation.
1624
 *)
1625
let dest_not f =
1626
  match f with
1627
  | NOT f1 -> f1
1628
  | _ -> raise (CoAlgException "Formula is not a negation.")
1629

    
1630
(** Destructs an @-formula.
1631
    @param f An @-formula.
1632
    @return The name of the nominal and the immediate subformula of the @-formula.
1633
    @raise CoAlgException if f is not an @-formula.
1634
 *)
1635
let dest_at f =
1636
  match f with
1637
  | AT (s, f1) -> (s, f1)
1638
  | _ -> raise (CoAlgException "Formula is not an @-formula.")
1639

    
1640
(** Destructs an or-formula.
1641
    @param f An or-formula.
1642
    @return The two immediate subformulae of the or-formula.
1643
    @raise CoAlgException if f is not an or-formula.
1644
 *)
1645
let dest_or f =
1646
  match f with
1647
  | OR (f1, f2) -> (f1, f2)
1648
  | _ -> raise (CoAlgException "Formula is not an or-formula.")
1649

    
1650
(** Destructs an and-formula.
1651
    @param f An and-formula.
1652
    @return The two immediate subformulae of the and-formula.
1653
    @raise CoAlgException if f is not an and-formula.
1654
 *)
1655
let dest_and f =
1656
  match f with
1657
  | AND (f1, f2) -> (f1, f2)
1658
  | _ -> raise (CoAlgException "Formula is not an and-formula.")
1659

    
1660
(** Destructs an equivalence.
1661
    @param f An equivalence.
1662
    @return The two immediate subformulae of the equivalence.
1663
    @raise CoAlgException if f is not an equivalence.
1664
 *)
1665
let dest_equ f =
1666
  match f with
1667
  | EQU (f1, f2) -> (f1, f2)
1668
  | _ -> raise (CoAlgException "Formula is not an equivalence.")
1669

    
1670
(** Destructs an implication.
1671
    @param f An implication.
1672
    @return The two immediate subformulae of the implication.
1673
    @raise CoAlgException if f is not an implication.
1674
 *)
1675
let dest_imp f =
1676
  match f with
1677
  | IMP (f1, f2) -> (f1, f2)
1678
  | _ -> raise (CoAlgException "Formula is not an implication.")
1679

    
1680
(** Destructs an EX-formula.
1681
    @param f An EX-formula.
1682
    @return The role name and the immediate subformula of the EX-formula.
1683
    @raise CoAlgException if f is not an EX-formula.
1684
 *)
1685
let dest_ex f =
1686
  match f with
1687
  | EX (s, f1) -> (s, f1)
1688
  | _ -> raise (CoAlgException "Formula is not an EX-formula.")
1689

    
1690
(** Destructs an AX-formula.
1691
    @param f An AX-formula.
1692
    @return The role name and the immediate subformula of the AX-formula.
1693
    @raise CoAlgException if f is not an AX-formula.
1694
 *)
1695
let dest_ax f =
1696
  match f with
1697
  | AX (s, f1) -> (s, f1)
1698
  | _ -> raise (CoAlgException "Formula is not an AX-formula.")
1699

    
1700
(** Destructs a MIN-formula.
1701
    @param f A MIN-formula.
1702
    @return The number restriction, role name,
1703
    and the immediate subformula of the MIN-formula.
1704
    @raise CoAlgException if f is not a MIN-formula.
1705
 *)
1706
let dest_min f =
1707
  match f with
1708
  | MIN (n, s, f1) -> (n, s, f1)
1709
  | _ -> raise (CoAlgException "Formula is not a MIN-formula.")
1710

    
1711
(** Destructs a MAX-formula.
1712
    @param f A MAX-formula.
1713
    @return The number restriction, role name,
1714
    and the immediate subformula of the MAX-formula.
1715
    @raise CoAlgException if f is not a MAX-formula.
1716
 *)
1717
let dest_max f =
1718
  match f with
1719
  | MAX (n, s, f1) -> (n, s, f1)
1720
  | _ -> raise (CoAlgException "Formula is not a MAX-formula.")
1721

    
1722
(** Destructs a choice formula.
1723
    @param f A choice formula.
1724
    @return The two immediate subformulae of the choice formula.
1725
    @raise CoAlgException if f is not a choice formula.
1726
 *)
1727
let dest_choice f =
1728
  match f with
1729
  | CHC (f1, f2) -> (f1, f2)
1730
  | _ -> raise (CoAlgException "Formula is not a choice formula.")
1731

    
1732
(** Destructs a fusion formula.
1733
    @param f A fusion formula.
1734
    @return A pair (first, f1) where
1735
    first is true iff f is a first projection; and
1736
    f1 is the immediate subformulae of f.
1737
    @raise CoAlgException if f is not a fusion formula.
1738
 *)
1739
let dest_fusion f =
1740
  match f with
1741
  | FUS (first, f1) -> (first, f1)
1742
  | _ -> raise (CoAlgException "Formula is not a fusion formula.")
1743

    
1744

    
1745
(** Tests whether a formula is the constant True.
1746
    @param f A formula.
1747
    @return True iff f is the constant True.
1748
 *)
1749
let is_true f =
1750
  match f with
1751
  | TRUE -> true
1752
  | _ -> false
1753

    
1754
(** Tests whether a formula is the constant False.
1755
    @param f A formula.
1756
    @return True iff f is the constant False.
1757
 *)
1758
let is_false f =
1759
  match f with
1760
  | FALSE -> true
1761
  | _ -> false
1762

    
1763
(** Tests whether a formula is an atomic proposition.
1764
    @param f A formula.
1765
    @return True iff f is an atomic proposition.
1766
 *)
1767
let is_ap f =
1768
  match f with
1769
  | AP s when not (isNominal s) -> true
1770
  | _ -> false
1771

    
1772
(** Tests whether a formula is a nominal.
1773
    @param f A formula.
1774
    @return True iff f is a nominal.
1775
 *)
1776
let is_nom f =
1777
  match f with
1778
  | AP s when isNominal s -> true
1779
  | _ -> false
1780

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

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

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

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

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

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

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

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

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

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

    
1871
(** Tests whether a formula is a choice formula.
1872
    @param f A formula.
1873
    @return True iff f is a choice formula.
1874
 *)
1875
let is_choice f =
1876
  match f with
1877
  | CHC _ -> true
1878
  | _ -> false
1879

    
1880
(** Tests whether a formula is a fusion formula.
1881
    @param f A formula.
1882
    @return True iff f is a fusion formula.
1883
 *)
1884
let is_fusion f =
1885
  match f with
1886
  | FUS _ -> true
1887
  | _ -> false
1888

    
1889

    
1890
(** The constant True.
1891
 *)
1892
let const_true = TRUE
1893

    
1894
(** The constant False.
1895
 *)
1896
let const_false = FALSE
1897

    
1898
(** Constructs an atomic proposition.
1899
    @param s The name of the atomic proposition.
1900
    @return The atomic proposition with name s.
1901
    @raise CoAlgException if s is a nominal name.
1902
 *)
1903
let const_ap s =
1904
  if isNominal s then raise (CoAlgException "The name indicates a nominal.")
1905
  else AP s
1906

    
1907
(** Constructs a nominal.
1908
    @param s The name of the nominal.
1909
    @return A nominal with name s.
1910
    @raise CoAlgException if s is not a nominal name.
1911
 *)
1912
let const_nom s =
1913
  if isNominal s then AP s
1914
  else raise (CoAlgException "The name does not indicate a nominal.")
1915

    
1916
(** Negates a formula.
1917
    @param f A formula.
1918
    @return The negation of f.
1919
 *)
1920
let const_not f = NOT f
1921

    
1922
(** Constructs an @-formula from a name and a formula.
1923
    @param s A nominal name.
1924
    @param f A formula.
1925
    @return The formula AT (s, f).
1926
 *)
1927
let const_at s f = AT (s, f)
1928

    
1929
(** Constructs an or-formula from two formulae.
1930
    @param f1 The first formula (LHS).
1931
    @param f2 The second formula (LHS).
1932
    @return The formula f1 | f2.
1933
 *)
1934
let const_or f1 f2 = OR (f1, f2)
1935

    
1936
(** Constructs an and-formula from two formulae.
1937
    @param f1 The first formula (LHS).
1938
    @param f2 The second formula (LHS).
1939
    @return The formula f1 & f2.
1940
 *)
1941
let const_and f1 f2 = AND (f1, f2)
1942

    
1943
(** Constructs an equivalence from two formulae.
1944
    @param f1 The first formula (LHS).
1945
    @param f2 The second formula (LHS).
1946
    @return The equivalence f1 <=> f2.
1947
 *)
1948
let const_equ f1 f2 = EQU (f1, f2)
1949

    
1950
(** Constructs an implication from two formulae.
1951
    @param f1 The first formula (LHS).
1952
    @param f2 The second formula (LHS).
1953
    @return The implication f1 => f2.
1954
 *)
1955
let const_imp f1 f2 = IMP (f1, f2)
1956

    
1957
(** Constructs an EX-formula from a formula.
1958
    @param s A role name.
1959
    @param f A formula.
1960
    @return The formula EX (s, f).
1961
 *)
1962
let const_ex s f = EX (s, f)
1963

    
1964
(** Constructs an AX-formula from a formula.
1965
    @param s A role name.
1966
    @param f A formula.
1967
    @return The formula AX (s, f).
1968
 *)
1969
let const_ax s f = AX (s, f)
1970

    
1971
(** Constructs a MIN-formula from a formula.
1972
    @param n A non-negative integer.
1973
    @param s A role name.
1974
    @param f A formula.
1975
    @return The formula MIN f.
1976
    @raise CoAlgException Iff n is negative.
1977
 *)
1978
let const_min n s f =
1979
  if n < 0 then raise (CoAlgException "Negative cardinality constraint.")
1980
  else MIN (n, s, f)
1981

    
1982
(** Constructs a MAX-formula from a formula.
1983
    @param n A non-negative integer.
1984
    @param s A role name.
1985
    @param f A formula.
1986
    @return The formula MAX f.
1987
    @raise CoAlgException Iff n is negative.
1988
 *)
1989
let const_max n s f =
1990
  if n < 0 then raise (CoAlgException "Negative cardinality constraint.")
1991
  else MAX (n, s, f)
1992

    
1993
let const_enforces p f =
1994
    ENFORCES (p,f)
1995

    
1996
let const_allows p f =
1997
    ALLOWS (p,f)
1998

    
1999
(** Constructs a choice formula from two formulae.
2000
    @param f1 The first formula (LHS).
2001
    @param f2 The second formula (LHS).
2002
    @return The formula (f1 + f2).
2003
 *)
2004
let const_choice f1 f2 = CHC (f1, f2)
2005

    
2006
(** Constructs a fusion formula.
2007
    @param first True iff the result is a first projection.
2008
    @param f1 A formula.
2009
    @return The formula [pi1] f1 or [pi2] f1 (depending on first).
2010
 *)
2011
let const_fusion first f1 = FUS (first, f1)
2012

    
2013

    
2014
(** Hash-consed formulae, which are in negation normal form,
2015
    such that structural and physical equality coincide.
2016

    
2017
    Also CTL has been replaced by the equivalent μ-Calculus
2018
    constructs
2019
 *)
2020
type hcFormula = (hcFormula_node, formula) HC.hash_consed
2021
and hcFormula_node =
2022
  | HCTRUE
2023
  | HCFALSE
2024
  | HCAP of string
2025
  | HCNOT of string
2026
  | HCAT of string * hcFormula
2027
  | HCOR of hcFormula * hcFormula
2028
  | HCAND of hcFormula * hcFormula
2029
  | HCEX of string * hcFormula
2030
  | HCAX of string * hcFormula
2031
  | HCENFORCES of int list * hcFormula
2032
  | HCALLOWS of int list * hcFormula
2033
  | HCMORETHAN of int * string * hcFormula (* GML Diamond *)
2034
  | HCMAXEXCEPT of int * string * hcFormula (* GML Box *)
2035
  | HCATLEASTPROB of rational * hcFormula
2036
  | HCLESSPROBFAIL of rational * hcFormula
2037
  | HCCONST of string
2038
  | HCCONSTN of string
2039
  | HCID of hcFormula
2040
  | HCNORM of hcFormula * hcFormula
2041
  | HCNORMN of hcFormula * hcFormula
2042
  | HCCHC of hcFormula * hcFormula
2043
  | HCFUS of bool * hcFormula
2044
  | HCMU of string * hcFormula
2045
  | HCNU of string * hcFormula
2046
  | HCVAR of string
2047

    
2048
(** Determines whether two formula nodes are structurally equal.
2049
    @param f1 The first formula node.
2050
    @param f2 The second formula node.
2051
    @return True iff f1 and f2 are structurally equal.
2052
 *)
2053
let equal_hcFormula_node f1 f2 =
2054
  match f1, f2 with
2055
  | HCTRUE, HCTRUE -> true
2056
  | HCFALSE, HCFALSE -> true
2057
  | HCCONST s1, HCCONST s2
2058
  | HCCONSTN s1, HCCONSTN s2
2059
  | HCAP s1, HCAP s2
2060
  | HCNOT s1, HCNOT s2 -> compare s1 s2 = 0
2061
  | HCAT (s1, f1), HCAT (s2, f2) -> compare s1 s2 = 0 && f1 == f2
2062
  | HCOR (f1a, f1b), HCOR (f2a, f2b)
2063
  | HCAND (f1a, f1b), HCAND (f2a, f2b) -> f1a == f2a && f1b == f2b
2064
  | HCEX (s1, f1), HCEX (s2, f2)
2065
  | HCAX (s1, f1), HCAX (s2, f2) -> compare s1 s2 = 0 && f1 == f2
2066
  | HCENFORCES (s1, f1), HCENFORCES (s2, f2)
2067
  | HCALLOWS (s1, f1), HCALLOWS (s2, f2) -> compare s1 s2 = 0 && f1 == f2
2068
  | HCMORETHAN (n1, s1, f1), HCMORETHAN (n2, s2, f2)
2069
  | HCMAXEXCEPT (n1, s1, f1), HCMAXEXCEPT (n2, s2, f2) ->
2070
      n1 = n2 && compare s1 s2 = 0 && f1 == f2
2071
  | HCATLEASTPROB (p1, f1), HCATLEASTPROB (p2,f2) ->
2072
      p1 = p2 && f1 == f2
2073
  | HCLESSPROBFAIL (p1, f1), HCLESSPROBFAIL (p2,f2) ->
2074
      p1 = p2 && f1 == f2
2075
  | HCID f1, HCID f2 -> f1 == f2
2076
  | HCNORM (f1a, f1b), HCNORMN (f2a, f2b) -> f1a == f2a && f1b == f2b
2077
  | HCCHC (f1a, f1b), HCCHC (f2a, f2b) -> f1a == f2a && f1b == f2b
2078
  | HCFUS (first1, f1), HCFUS (first2, f2) -> first1 = first2 && f1 == f2
2079
  | HCMU (name1, f1), HCMU(name2, f2) -> compare name1 name2 = 0 && f1 == f2
2080
  | HCNU (name1, f1), HCNU(name2, f2) -> compare name1 name2 = 0 && f1 == f2
2081
  | HCVAR name1, HCVAR name2 -> compare name1 name2 = 0
2082
(* The rest could be shortened to | _ -> false,
2083
   but then the compiler would not warn if the formula type is extended
2084
   and this function is not updated accordingly.*)
2085
  | HCTRUE, _
2086
  | HCFALSE, _
2087
  | HCAP _, _
2088
  | HCNOT _, _
2089
  | HCAT _, _
2090
  | HCOR _, _
2091
  | HCAND _, _
2092
  | HCEX _, _
2093
  | HCAX _, _
2094
  | HCENFORCES _, _
2095
  | HCALLOWS   _, _
2096
  | HCMORETHAN _, _
2097
  | HCMAXEXCEPT _, _
2098
  | HCATLEASTPROB _, _
2099
  | HCLESSPROBFAIL _, _
2100
  | HCCONST _, _
2101
  | HCCONSTN _, _
2102
  | HCID _, _
2103
  | HCNORM _, _
2104
  | HCNORMN _, _
2105
  | HCCHC _, _
2106
  | HCFUS _, _
2107
  | HCMU _, _
2108
  | HCNU _, _
2109
  | HCVAR _, _ -> false
2110

    
2111
(** Computes the hash value of a formula node.
2112
    @param f A formula node.
2113
    @return The hash value of f.
2114
 *)
2115
let hash_hcFormula_node f =
2116
  let base = 23 in (* should be larger than the no of constructors *)
2117
  match f with
2118
  | HCTRUE -> 0
2119
  | HCFALSE -> 1
2120
  | HCAP s
2121
  | HCNOT s
2122
  | HCVAR s -> base * Hashtbl.hash s + 1
2123
  | HCAT (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 2
2124
  | HCOR (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 5
2125
  | HCAND (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 6
2126
  | HCEX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 3
2127
  | HCAX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 4
2128
  | HCMORETHAN (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 7
2129
  | HCMAXEXCEPT (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 8
2130
  | HCATLEASTPROB (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 9
2131
  | HCLESSPROBFAIL (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 10
2132
  | HCCHC (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 11
2133
  | HCFUS (first, f1) -> base * (base * (Hashtbl.hash first) + f1.HC.hkey) + 13
2134
  | HCENFORCES (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 14
2135
  | HCALLOWS   (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 15
2136
  | HCCONST s -> Hashtbl.hash s + 16
2137
  | HCCONSTN s -> Hashtbl.hash s + 17
2138
  | HCNORM (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 18
2139
  | HCNORMN (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 19
2140
  | HCID (f1) -> base * f1.HC.hkey + 20
2141
  | HCMU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 21
2142
  | HCNU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 22
2143

    
2144
(** Determines the "real" formula of a formula node.
2145
    @param f A formula node.
2146
    @return The formula (in negation normal form) which corresponds to f.
2147
 *)
2148
let toFml_hcFormula_node f =
2149
  match f with
2150
  | HCTRUE -> TRUE
2151
  | HCFALSE -> FALSE
2152
  | HCAP s -> AP s
2153
  | HCVAR s -> VAR s
2154
  | HCNOT s -> NOT (AP s)
2155
  | HCAT (s, f1) -> AT (s, f1.HC.fml)
2156
  | HCOR (f1, f2) -> OR (f1.HC.fml, f2.HC.fml)
2157
  | HCAND (f1, f2) -> AND (f1.HC.fml, f2.HC.fml)
2158
  | HCEX (s, f1) -> EX (s, f1.HC.fml)
2159
  | HCAX (s, f1) -> AX (s, f1.HC.fml)
2160
  | HCENFORCES (s, f1) -> ENFORCES (s, f1.HC.fml)
2161
  | HCALLOWS (s, f1) -> ALLOWS (s, f1.HC.fml)
2162
  | HCMORETHAN (n, s, f1) -> MORETHAN (n, s, f1.HC.fml)
2163
  | HCMAXEXCEPT (n, s, f1) -> MAXEXCEPT (n, s, f1.HC.fml)
2164
  | HCATLEASTPROB (p, f1) -> ATLEASTPROB (p, f1.HC.fml)
2165
  | HCLESSPROBFAIL (p, f1) -> LESSPROBFAIL (p, f1.HC.fml)
2166
  | HCCONST s -> CONST s
2167
  | HCCONSTN s -> CONSTN s
2168
  | HCID (f1) -> ID(f1.HC.fml)
2169
  | HCNORM (f1, f2) -> NORM(f1.HC.fml, f2.HC.fml)
2170
  | HCNORMN (f1, f2) -> NORMN(f1.HC.fml, f2.HC.fml)
2171
  | HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml)
2172
  | HCFUS (first, f1) -> FUS (first, f1.HC.fml)
2173
  | HCMU (var, f1) -> MU (var, f1.HC.fml)
2174
  | HCNU (var, f1) -> NU (var, f1.HC.fml)
2175

    
2176
(** Determines the negation (in negation normal form) of a formula node.
2177
    @param f A formula node.
2178
    @return The negation (in negation normal form) of f.
2179
 *)
2180
let negNde_hcFormula_node f =
2181
  match f with
2182
  | HCTRUE -> HCFALSE
2183
  | HCFALSE -> HCTRUE
2184
  | HCAP s -> HCNOT s
2185
  | HCNOT s -> HCAP s
2186
  | HCVAR s -> f
2187
  | HCAT (s, f1) -> HCAT (s, f1.HC.neg)
2188
  | HCOR (f1, f2) -> HCAND (f1.HC.neg, f2.HC.neg)
2189
  | HCAND (f1, f2) -> HCOR (f1.HC.neg, f2.HC.neg)
2190
  | HCEX (s, f2) -> HCAX (s, f2.HC.neg)
2191
  | HCAX (s, f2) -> HCEX (s, f2.HC.neg)
2192
  | HCENFORCES (s, f2) -> HCALLOWS (s, f2.HC.neg)
2193
  | HCALLOWS (s, f2) -> HCENFORCES (s, f2.HC.neg)
2194
  | HCMORETHAN (n, s, f1) -> HCMAXEXCEPT (n, s, f1.HC.neg)
2195
  | HCMAXEXCEPT (n, s, f1) -> HCMORETHAN (n, s, f1.HC.neg)
2196
  | HCATLEASTPROB (p, f1) -> HCLESSPROBFAIL (p, f1.HC.neg)
2197
  | HCLESSPROBFAIL (p, f1) -> HCATLEASTPROB (p, f1.HC.neg)
2198
  | HCCONST s -> HCCONSTN s
2199
  | HCCONSTN s -> HCCONST s
2200
  | HCID (f1) -> HCID(f1.HC.neg)
2201
  | HCNORM (f1, f2) -> HCNORMN(f1.HC.neg, f2.HC.neg)
2202
  | HCNORMN (f1, f2) -> HCNORM(f1.HC.neg, f2.HC.neg)
2203
  | HCCHC (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg)
2204
  | HCFUS (first, f1) -> HCFUS (first, f1.HC.neg)
2205
  | HCMU (name, f1) -> HCNU (name, f1.HC.neg)
2206
  | HCNU (name, f1) -> HCMU (name, f1.HC.neg)
2207

    
2208
(** An instantiation of hash-consing for formulae.
2209
 *)
2210
module HcFormula = HC.Make(
2211
  struct
2212
    type nde = hcFormula_node
2213
    type fml = formula
2214
    let equal (n1 : nde) n2 = equal_hcFormula_node n1 n2
2215
    let hash (n : nde) = hash_hcFormula_node n
2216
    let negNde (n : nde) = negNde_hcFormula_node n
2217
    let toFml (n : nde) = toFml_hcFormula_node n
2218
  end
2219
 )
2220

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

    
2307
(* Replace the Variable name in f with formula formula
2308
   hc_replace foo φ ψ => ψ[foo |-> φ]
2309
 *)
2310
let rec hc_replace hcF name (formula: hcFormula) (f: hcFormula) =
2311
  let func = hc_replace hcF name formula in
2312
  let gennew = HcFormula.hashcons hcF in
2313
  match f.HC.node with
2314
  | HCTRUE
2315
  | HCFALSE
2316
  | HCAP _
2317
  | HCNOT _
2318
  | HCCONST _
2319
  | HCCONSTN _ -> f
2320
  | HCVAR s ->
2321
     if compare s name == 0
2322
     then formula
2323
     else f
2324
  | HCAT (s, f1) ->
2325
     let nf1 = func f1 in
2326
     if nf1 == f1 then f else gennew (HCAT(s, nf1))
2327
  | HCOR (f1, f2) ->
2328
     let nf1 = func f1 in
2329
     let nf2 = func f2 in
2330
     if nf1 == f1 && nf2 == f2 then f else gennew (HCOR(nf1, nf2))
2331
  | HCAND (f1, f2) ->
2332
     let nf1 = func f1 in
2333
     let nf2 = func f2 in
2334
     if nf1 == f1 && nf2 == f2 then f else gennew (HCAND(nf1, nf2))
2335
  | HCEX (s, f1) ->
2336
     let nf1 = func f1 in
2337
     if nf1 == f1 then f else gennew (HCEX(s, nf1))
2338
  | HCAX (s, f1) ->
2339
     let nf1 = func f1 in
2340
     if nf1 == f1 then f else gennew (HCAX(s, nf1))
2341
  | HCENFORCES (s, f1) ->
2342
     let nf1 = func f1 in
2343
     if nf1 == f1 then f else gennew (HCENFORCES(s, nf1))
2344
  | HCALLOWS (s, f1) ->
2345
     let nf1 = func f1 in
2346
     if nf1 == f1 then f else gennew (HCALLOWS(s, nf1))
2347
  | HCMORETHAN  (n, s, f1) ->
2348
     let nf1 = func f1 in
2349
     if nf1 == f1 then f else gennew (HCMORETHAN(n, s, nf1))
2350
  | HCMAXEXCEPT  (n, s, f1) ->
2351
     let nf1 = func f1 in
2352
     if nf1 == f1 then f else gennew (HCMAXEXCEPT(n, s, nf1))
2353
  | HCATLEASTPROB (p, f1) ->
2354
     let nf1 = func f1 in
2355
     if nf1 == f1 then f else gennew (HCATLEASTPROB(p, nf1))
2356
  | HCLESSPROBFAIL (p, f1) ->
2357
     let nf1 = func f1 in
2358
     if nf1 == f1 then f else gennew (HCLESSPROBFAIL(p, nf1))
2359
  | HCID f1 ->
2360
     let nf1 = func f1 in
2361
     if nf1 == f1 then f else gennew (HCID(nf1))
2362
  | HCNORM (f1, f2) ->
2363
     let nf1 = func f1 in
2364
     let nf2 = func f2 in
2365
     if nf1 == f1 && nf2 == f2 then f else gennew (HCNORM(nf1, nf2))
2366
  | HCNORMN (f1, f2) ->
2367
     let nf1 = func f1 in
2368
     let nf2 = func f2 in
2369
     if nf1 == f1 && nf2 == f2 then f else gennew (HCNORMN(nf1, nf2))
2370
  | HCCHC (f1, f2) ->
2371
     let nf1 = func f1 in
2372
     let nf2 = func f2 in
2373
     if nf1 == f1 && nf2 == f2 then f else gennew (HCCHC(nf1, nf2))
2374
  | HCFUS (first, f1) ->
2375
     let nf1 = func f1 in
2376
     if nf1 == f1 then f else gennew (HCFUS(first, nf1))
2377
  | HCMU (var, f1) ->
2378
     if compare var name != 0 then
2379
       let nf1 = func f1 in
2380
       if nf1 == f1 then f else gennew (HCMU(var, nf1))
2381
     else
2382
       f
2383
  | HCNU (var, f1) ->
2384
     if compare var name != 0 then
2385
       let nf1 = func f1 in
2386
       if nf1 == f1 then f else gennew (HCNU(var, nf1))
2387
     else
2388
       f
2389

    
2390
let rec hc_freeIn variable (f: hcFormula) =
2391
  match f.HC.node with
2392
  | HCTRUE
2393
  | HCFALSE
2394
  | HCAP _
2395
  | HCNOT _
2396
  | HCCONST _
2397
  | HCCONSTN _ -> false
2398
  | HCVAR s ->
2399
     if compare variable s == 0
2400
     then true
2401
     else false
2402
  | HCAT (s, f1) ->
2403
     hc_freeIn variable f1
2404
  | HCOR (f1, f2)
2405
  | HCAND (f1, f2) ->
2406
     hc_freeIn variable f1 || hc_freeIn variable f2
2407
  | HCEX (_, f1)
2408
  | HCAX (_, f1)
2409
  | HCENFORCES (_, f1)
2410
  | HCALLOWS (_, f1)
2411
  | HCMORETHAN  (_, _, f1)
2412
  | HCMAXEXCEPT  (_, _, f1)
2413
  | HCATLEASTPROB (_, f1)
2414
  | HCLESSPROBFAIL (_, f1)
2415
  | HCID f1 ->
2416
     hc_freeIn variable f1
2417
  | HCNORM (f1, f2)
2418
  | HCNORMN (f1, f2)
2419
  | HCCHC (f1, f2) ->
2420
     hc_freeIn variable f1 || hc_freeIn variable f2
2421
  | HCFUS (first, f1) ->
2422
     hc_freeIn variable f1
2423
  | HCMU (var, f1)
2424
  | HCNU (var, f1) ->
2425
     (* Do we need to exclude bound variables here? *)
2426
     hc_freeIn variable f1
2427

    
2428

    
2429
(** An instantiation of a hash table (of the standard library)
2430
    for hash-consed formulae. The test for equality
2431
    and computing the hash value is done in constant time.
2432
 *)
2433
module HcFHt = Hashtbl.Make(
2434
  struct
2435
    type t = hcFormula
2436
    let equal (f1 : t) f2 = f1.HC.tag = f2.HC.tag
2437
    let hash (f : t) = f.HC.tag
2438
  end
2439
 )
2440

    
2441
(* vim: set et sw=2 sts=2 ts=8 : *)