Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgFormula.ml @ 1d36cd07

History | View | Annotate | Download (74.2 KB)

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

    
6

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

    
12

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

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

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

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

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

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

    
75
exception ConversionException of formula
76

    
77

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

    
82

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

    
89

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

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

    
138
let depthFormula form = 
139
  let rec depth f =
140
    match f with
141
      | TRUE
142
      | FALSE
143
      | AP _ -> 0
144
      | NOT f1
145
      | AT (_, f1) -> (depth f1)
146
      | OR (f1, f2)
147
      | AND (f1, f2)
148
      | EQU (f1, f2)
149
      | IMP (f1, f2) -> (max (depth f1)(depth f2))
150
      | EX (_, f1)
151
      | AX (_, f1)
152
      | ENFORCES (_, f1)
153
      | ALLOWS (_, f1) -> succ ((depth f1))
154
      | MIN (_, _, f1)
155
      | MAX (_, _, f1)
156
      | ATLEASTPROB (_, f1)
157
      | LESSPROBFAIL (_, f1)
158
      | MORETHAN (_, _, f1)
159
      | MAXEXCEPT (_, _, f1) -> succ ((depth f1))
160
      | ID (f1) -> succ ((depth f1))
161
      | NORM(f1, f2)
162
      | NORMN(f1, f2) -> succ ((max (depth f1) (depth f2))) 
163
      | CONST _
164
      | CONSTN _ -> 1
165
      | CHC (f1, f2) -> succ ((max (depth f1) (depth f2))) 
166
      | FUS (_, f1) -> succ (depth f1)
167
      | MU (_, f1)
168
      | NU (_, f1) -> depth f1
169
      | VAR _ -> 0
170
  in
171
  depth form
172

    
173

    
174
(* think of func: (formula -> unit) -> formula -> unit as identity.
175
  iterate over all subformulae and collect side effects. *)
176
let rec iter func formula =
177
    func formula;
178
    let proc = iter func in (* proc = "process" *)
179
    match formula with
180
    | TRUE | FALSE | AP _ | VAR _ -> ()
181
    | CONST _
182
    | CONSTN _ -> ()
183
    | NOT a | AT (_,a)
184
    | EX (_,a) | AX (_,a) -> proc a
185
    | OR (a,b) | AND (a,b)
186
    | EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
187
    | ENFORCES (_,a) | ALLOWS   (_,a)
188
    | MIN (_,_,a)    | MAX (_,_,a)
189
    | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
190
    | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
191
    | ID(a) -> proc a
192
    | NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
193
    | CHC (a,b)  -> (proc a ; proc b)
194
    | FUS (_,a) -> proc a
195
    | MU (_, f) | NU (_, f) -> proc f
196
    | AF f | EF f | AG f | EG f -> proc f
197
    | AU (f1, f2) | EU (f1, f2)
198
    | AR (f1, f2) | ER (f1, f2)
199
    | AB (f1, f2) | EB (f1, f2) -> (proc f1; proc f2)
200

    
201
let rec convert_post func formula = (* run over all subformulas in post order *)
202
  let c = convert_post func in (* some shorthand *)
203
  (* replace parts of the formula *)
204
  let formula = (match formula with
205
    (* 0-ary constructors *)
206
    | TRUE | FALSE | AP _ | VAR _ -> formula
207
    | CONST _
208
    | CONSTN _ -> formula
209
    (* unary *)
210
    | NOT a -> NOT (c a)
211
    | AT (s,a) -> AT (s,c a)
212
    (* binary *)
213
    | OR (a,b) -> OR (c a, c b)
214
    | AND (a,b) -> AND (c a, c b)
215
    | EQU (a,b) -> EQU (c a, c b)
216
    | IMP (a,b) -> IMP (c a, c b)
217
    | EX (s,a) -> EX (s,c a)
218
    | AX (s,a) -> AX (s,c a)
219
    | ENFORCES (s,a) -> ENFORCES (s,c a)
220
    | ALLOWS   (s,a) -> ALLOWS   (s,c a)
221
    | MIN (n,s,a) -> MIN (n,s,c a)
222
    | MAX (n,s,a) -> MAX (n,s,c a)
223
    | ATLEASTPROB (p,a) -> ATLEASTPROB (p, c a)
224
    | LESSPROBFAIL (p,a) -> LESSPROBFAIL (p, c a)
225
    | MORETHAN (n,s,a) -> MORETHAN (n,s,c a)
226
    | MAXEXCEPT (n,s,a) -> MAXEXCEPT (n,s,c a)
227
    | ID(a) -> ID (c a)
228
    | NORM(a, b) -> NORM(c a, c b)
229
    | NORMN(a, b) -> NORMN(c a, c b)
230
    | CHC (a,b) -> CHC (c a, c b)
231
    | FUS (s,a) -> FUS (s, c a)
232
    | MU (n, f1) -> MU (n, c f1)
233
    | NU (n, f1) -> NU (n, c f1)
234
    | AF f1 -> AF (c f1)
235
    | EF f1 -> EF (c f1)
236
    | AG f1 -> AG (c f1)
237
    | EG f1 -> EG (c f1)
238
    | AU (f1, f2) -> AU (c f1, c f2)
239
    | EU (f1, f2) -> EU (c f1, c f2)
240
    | AR (f1, f2) -> AR (c f1, c f2)
241
    | ER (f1, f2) -> ER (c f1, c f2)
242
    | AB (f1, f2) -> AB (c f1, c f2)
243
    | EB (f1, f2) -> EB (c f1, c f2))
244
  in
245
  func formula
246

    
247
let convertToK formula = (* tries to convert a formula to a pure K formula *)
248
  let helper formula = match formula with
249
  | ENFORCES _ | ALLOWS _ -> raise (ConversionException formula)
250
  | MORETHAN (0,s,a) | MIN (1,s,a) -> EX (s,a)
251
  | MAX (0,s,a) -> AX (s, NOT a)
252
  | MAXEXCEPT (0,s,a) -> AX (s, a)
253
  | TRUE | FALSE
254
  | EQU _ | IMP _
255
  | AND _ | OR _
256
  | AP _ | NOT _
257
  | AX _ | EX _
258
  | CHC _ | FUS _ -> formula
259
  | _ -> raise (ConversionException formula)
260
  in
261
  convert_post helper formula
262

    
263
let convertToGML formula = (* tries to convert a formula to a pure GML formula *)
264
  let helper formula = match formula with
265
  | ENFORCES _ | ALLOWS _ -> raise (ConversionException formula)
266
  | MORETHAN _ | MIN _ | MAX _ | MAXEXCEPT _ -> formula
267
  | TRUE | FALSE
268
  | EQU _ | IMP _
269
  | AND _ | OR _
270
  | AP _ | NOT _
271
  | CHC _ | FUS _ -> formula
272
  | AX (r,a) -> MAXEXCEPT (0,r,a)
273
  | EX (r,a) -> MORETHAN  (0,r,a)
274
  | _ -> raise (ConversionException formula)
275
  in
276
  convert_post helper formula
277

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

    
280
let convertToMu formula =
281
  let name = Stream.next gensym in
282
  let helper formula =
283
    match formula with
284
    | AF f1 ->
285
       MU (name, (OR (f1, (AX ("", (VAR name))))))
286
    | EF f1 ->
287
       MU (name, (OR (f1, (EX ("", (VAR name))))))
288
    | AG f1 ->
289
       NU (name, (AND (f1, (AX ("", (VAR name))))))
290
    | EG f1 ->
291
       NU (name, (AND (f1, (EX ("", (VAR name))))))
292
    | AU (f1, f2) ->
293
       MU (name, (OR (f2, (AND (f1, (AX ("", (VAR name))))))))
294
    | EU (f1, f2) ->
295
       MU (name, (OR (f2, (AND (f1, (EX ("", (VAR name))))))))
296
    | AR (f1, f2) ->
297
       NU (name, (AND (f2, (OR (f1, (AX ("", (VAR name))))))))
298
    | ER (f1, f2) ->
299
       NU (name, (AND (f2, (OR (f1, (EX ("", (VAR name))))))))
300
    | AB (f1, f2) ->
301
       NOT (MU (name, (OR (f2, (AND ((NOT f1), (EX ("", (VAR name)))))))))
302
    | EB (f1, f2) ->
303
       NOT (MU (name, (OR (f2, (AND ((NOT f1), (AX ("", (VAR name)))))))))
304
    | _ -> formula
305
  in
306
  convert_post helper formula
307

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

    
517

    
518
(** Converts a formula into a string representation.
519
    Parentheses are ommited where possible
520
    where the preference rules are defined as usual.
521
    @param f A formula.
522
    @return A string representing f.
523
 *)
524
let exportFormula f =
525
  let sb = Buffer.create 128 in
526
  exportFormula_buffer sb f;
527
  Buffer.contents sb
528

    
529
let string_of_formula = exportFormula
530

    
531
(** export (CL)-formula suitable for tatl-inputs *)
532
let rec exportTatlFormula_buffer sb f =
533
  let prio n lf =
534
    let prionr = function
535
      | EQU _ -> 0
536
      | IMP _  -> 1
537
      | OR _ -> 2
538
      | AND _ -> 3
539
      | _ -> 4
540
    in
541
    if prionr lf < n then begin
542
      Buffer.add_char sb '(';
543
      exportTatlFormula_buffer sb lf;
544
      Buffer.add_char sb ')'
545
    end
546
    else exportTatlFormula_buffer sb lf
547
  in
548
  match f with
549
  | TRUE -> Buffer.add_string sb "(p \\/ ~p)"
550
  | FALSE -> Buffer.add_string sb "(p /\\ ~p)"
551
  | AP s -> Buffer.add_string sb s
552
  | NOT f1 ->
553
      Buffer.add_string sb "~";
554
      prio 4 f1
555
  | OR (f1, f2) ->
556
      prio 2 f1;
557
      Buffer.add_string sb " \\/ ";
558
      prio 2 f2
559
  | AND (f1, f2) ->
560
      prio 3 f1;
561
      Buffer.add_string sb " /\\ ";
562
      prio 3 f2
563
  | EQU (f1, f2) ->
564
      prio 0 (AND (IMP (f1,f2), IMP (f2,f1)))
565
  | IMP (f1, f2) ->
566
      prio 2 f1;
567
      Buffer.add_string sb " -> ";
568
      prio 2 f2
569
  | ALLOWS (s, f1) ->
570
      Buffer.add_string sb "<<";
571
      Buffer.add_string sb (
572
          match s with
573
          | [] -> " "
574
          | _ ->(Str.concat "," (L.map string_of_int s))
575
      );
576
      Buffer.add_string sb ">>X ";
577
      prio 4 f1
578
  | ENFORCES (s, f1) ->
579
      Buffer.add_string sb "~<<";
580
      Buffer.add_string sb (
581
          match s with
582
          | [] -> " "
583
          | _ ->(Str.concat "," (L.map string_of_int s))
584
      );
585
      Buffer.add_string sb ">>X ~ ";
586
      prio 4 f1
587
  | EX _
588
  | AX _
589
  | MIN _
590
  | MAX _
591
  | MORETHAN _
592
  | MAXEXCEPT _
593
  | AT _
594
  | CONST _
595
  | CONSTN _
596
  | CHC _
597
  | ATLEASTPROB _
598
  | LESSPROBFAIL _
599
  | ID _
600
  | NORM _
601
  | NORMN _
602
  | FUS _
603
  | MU _
604
  | NU _
605
  | VAR _
606
  | AF _
607
  | EF _
608
  | AG _
609
  | EG _
610
  | AU _
611
  | EU _
612
  | AR _
613
  | ER _
614
  | AB _
615
  | EB _ -> raise (CoAlgException ("export to tatl: Not connectives of CL"))
616

    
617
let exportTatlFormula f =
618
  let sb = Buffer.create 128 in
619
  exportTatlFormula_buffer sb f;
620
  Buffer.contents sb
621

    
622
(** Appends a string representation of a sorted formula to a string buffer.
623
    Parentheses are ommited where possible
624
    where the preference rules are defined as usual.
625
    @param sb A string buffer.
626
    @param (s, f) A sorted formula.
627
 *)
628
let rec exportSortedFormula_buffer sb (s, f) =
629
  Buffer.add_string sb (string_of_int s);
630
  Buffer.add_string sb ": ";
631
  exportFormula_buffer sb f
632

    
633
(** Converts a sorted formula into a string representation.
634
    Parentheses are ommited where possible
635
    where the preference rules are defined as usual.
636
    @param f A sorted formula.
637
    @return A string representing f.
638
 *)
639
let exportSortedFormula f =
640
  let sb = Buffer.create 128 in
641
  exportSortedFormula_buffer sb f;
642
  Buffer.contents sb
643

    
644
(** Converts a (sorted) formula query into a string representation.
645
    @param tbox A list of sorted formulae representing a TBox.
646
    @param f A sorted formula.
647
    @return A string representing tbox |- f.
648
 *)
649
let exportQuery tbox f =
650
  let sb = Buffer.create 1000 in
651
  let rec expFl = function
652
    | [] -> ()
653
    | h::tl ->
654
        exportSortedFormula_buffer sb h;
655
        if tl <> [] then Buffer.add_string sb "; " else ();
656
        expFl tl
657
  in
658
  expFl tbox;
659
  Buffer.add_string sb "  |-  ";
660
  exportSortedFormula_buffer sb f;
661
  Buffer.contents sb
662

    
663
(** Converts a (sorted) formula query into a string representation. Such that
664
    coalg can read it again using importQuery
665
    @param tbox A list of sorted formulae representing a TBox.
666
    @param f A sorted formula.
667
    @return A string representing tbox |- f.
668
 *)
669
let exportQueryParsable tbox (_,f) =
670
  let sb = Buffer.create 1000 in
671
  let rec expFl = function
672
    | [] -> ()
673
    | (_,h)::tl ->
674
        exportFormula_buffer sb h;
675
        if tl <> [] then Buffer.add_string sb "; " else ();
676
        expFl tl
677
  in
678
  expFl tbox;
679
  Buffer.add_string sb "  |-  ";
680
  exportFormula_buffer sb f;
681
  Buffer.contents sb
682

    
683

    
684
(* NB: True and False are the propositional constants. Lower case
685
   true/false are regardes as atomic propositions and we emit a warning
686
*)
687
let lexer = A.make_lexer
688
    [":";";";"|-";"(";")";"=>";"<=>";"|";"&";"~";"@";"True";"False";"true";"false";"<";">";"[";"]";"{<=";"{>=";"}";"+";"[pi1]";"[pi2]"
689
     ;"[{";"}]";"<{";"}>";",";"/";"{<";"=";"=o";"O"
690
     ;"μ";"µ";"ν";"."
691
     ;"AX";"EX";"AF";"EF";"AG";"EG";"A";"E";"U";"R";"B"
692
    ]
693

    
694
let mk_exn s = CoAlgException s
695

    
696
(** Process from inside out. cons all variables seen, remove them when
697
    binding fixpoint is found. Fixpoint type may only change if last
698
    (inner) fixpoint didn't include any free variables.
699
 *)
700
let rec verifyMuAltFree formula =
701
  let proc = verifyMuAltFree in
702
  match formula with
703
  | TRUE | FALSE | AP _ -> ("none", [])
704
  | CONST _
705
  | CONSTN _ -> ("none", [])
706
  | AT (_,a) | NOT a
707
  | EX (_,a) | AX (_,a) -> proc a
708
  | OR (a,b) | AND (a,b)
709
  | EQU (a,b) | IMP (a,b) ->
710
     let (atype, afree) = proc a
711
     and (btype, bfree) = proc b in
712
     if (compare atype "μ" == 0 && compare btype "ν" == 0) ||
713
          (compare atype "ν" == 0 && compare btype "μ" == 0) then
714
       raise (CoAlgException ("formula not alternation-free"));
715
     if compare atype "none" == 0 then
716
       (btype, List.flatten [afree; bfree])
717
     else
718
       (atype, List.flatten [afree; bfree])
719
  | ENFORCES (_,a) | ALLOWS   (_,a)
720
  | MIN (_,_,a)    | MAX (_,_,a)
721
  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
722
  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
723
  | ID(a) -> proc a
724
  | NORM(a, b) | NORMN(a, b)
725
  | CHC (a,b)  ->
726
     let (atype, afree) = proc a
727
     and (btype, bfree) = proc b in
728
     if (compare atype "μ" == 0 && compare btype "ν" == 0) ||
729
          (compare atype "ν" == 0 && compare btype "μ" == 0) then
730
       raise (CoAlgException ("formula not alternation-free"));
731
     if compare atype "none" == 0 then
732
       (btype, List.flatten [afree; bfree])
733
     else
734
       (atype, List.flatten [afree; bfree])
735
  | FUS (_,a) -> proc a
736
  | MU (s, f) ->
737
     let (fptype, free) = proc f in
738
     (if (compare fptype "ν" == 0) then
739
        raise (CoAlgException ("formula not alternation-free")));
740
     let predicate x = compare x s != 0 in
741
     let newfree = List.filter predicate free in
742
     if newfree = [] then
743
       ("none", [])
744
     else
745
       ("μ", newfree)
746
  | NU (s, f) ->
747
     let (fptype, free) = proc f in
748
     (if (compare fptype "μ" == 0) then
749
        raise (CoAlgException ("formula not alternation-free")));
750
     let predicate x = compare x s != 0 in
751
     let newfree = List.filter predicate free in
752
     if newfree = [] then
753
       ("none", [])
754
     else
755
       ("ν", newfree)
756
  | VAR s -> ("none", [s])
757
  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ ->
758
     raise (CoAlgException ("verifyMuAltFree: CTL should have been removed at this point"))
759

    
760

    
761
exception NotAconjunctive of unit
762

    
763
let isMuAconjunctive (formula:formula) : bool =
764
  let module SS = Set.Make(String) in
765

    
766
  (* Accepts formula f and a set of currently bound mu variables. Returns a subset
767
   * of those, which actually occured free in the formula.
768
   * Raises an CoAlgException if the formula is determined not to be aconjunctive *)
769
  let rec verifyMuAconjunctiveInternal (formula:formula) (bound_mu_vars: SS.t) : SS.t =
770
    let proc f = verifyMuAconjunctiveInternal f bound_mu_vars in
771
    match formula with
772
    | VAR s when SS.mem s bound_mu_vars -> SS.singleton s
773
    | VAR s                             -> SS.empty
774
    (* s is now bound by a nu and shadows any privious binding s *)
775
    | NU (s, a) -> verifyMuAconjunctiveInternal a (SS.remove s bound_mu_vars)
776
    (* Bind s in the recursive call but don't return it as occuring free *)
777
    | MU (s, a) ->
778
       SS.remove s (verifyMuAconjunctiveInternal a (SS.add s bound_mu_vars))
779

    
780
    (* This is the interesting case *)
781
    | AND (a, b) ->
782
       let a_vars = proc a in
783
       let b_vars = proc b in
784

    
785
       (* If both subformulas contain free mu variables, the formula is not aconjunctive *)
786
       if not (SS.is_empty a_vars) && not (SS.is_empty b_vars) then
787
         raise (NotAconjunctive ())
788
       else
789
         SS.union a_vars b_vars (* one of them is empty anyways *)
790

    
791
    (* The other cases just pass argument and return value through *)
792
    | TRUE | FALSE | AP _
793
    | CONST _ | CONSTN _ -> SS.empty
794
    | AT (_,a) | NOT a
795
    | EX (_,a) | AX (_,a) -> proc a
796
    | OR (a,b) | EQU (a,b) | IMP (a,b) -> SS.union (proc a) (proc b)
797
    | ENFORCES (_,a) | ALLOWS   (_,a)
798
    | MIN (_,_,a)    | MAX (_,_,a)
799
    | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
800
    | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
801
    | ID(a) -> proc a
802
    | NORM(a, b) | NORMN(a, b)
803
    | CHC (a,b)  -> SS.union (proc a) (proc b)
804
    | FUS (_,a) -> proc a
805
    | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ ->
806
       raise (CoAlgException ("verifyMuAconjunctiveInternal: CTL should have been removed at this point"))
807
  in
808
  try ignore (verifyMuAconjunctiveInternal formula SS.empty); true
809
  with NotAconjunctive () -> false
810

    
811
(** Process from outside in. For every variable bound keep the tuple
812
    (name, negations). For every negation crossed map a +1 over snd on
813
    that list. For every variable met check that the matching
814
    negations is even.
815
 *)
816
let rec verifyMuMonotone negations formula =
817
  let proc = verifyMuMonotone negations in
818
  match formula with
819
  | TRUE | FALSE | AP _ -> ()
820
  | CONST _
821
  | CONSTN _ -> ()
822
  | AT (_,a)
823
  | EX (_,a) | AX (_,a) -> proc a
824
  | OR (a,b) | AND (a,b)
825
  | EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
826
  | ENFORCES (_,a) | ALLOWS   (_,a)
827
  | MIN (_,_,a)    | MAX (_,_,a)
828
  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
829
  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
830
  | ID(a) -> proc a
831
  | NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
832
  | CHC (a,b)  -> (proc a ; proc b)
833
  | FUS (_,a) -> proc a
834
  | MU (s, f)
835
  | NU (s, f) ->
836
     let newNeg = (s, 0) :: negations in
837
     verifyMuMonotone newNeg f
838
  | VAR s ->
839
     let finder (x, _) = compare x s == 0 in
840
     let (_, neg) = List.find finder negations in
841
     if ((neg land 1) != 0) then raise (CoAlgException ("formula not monotone"))
842
  | NOT a ->
843
     let increment (s, n) = (s, n+1) in
844
     let newNeg = List.map increment negations in
845
     verifyMuMonotone newNeg a
846
  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ ->
847
     raise (CoAlgException ("verifyMuMonotone: CTL should have been removed at this point"))
848

    
849
let rec verifyMuGuarded unguarded formula =
850
  let proc = verifyMuGuarded unguarded in
851
  match formula with
852
  | TRUE | FALSE | AP _ -> ()
853
  | CONST _
854
  | CONSTN _ -> ()
855
  | AT (_,a) | NOT a -> proc a
856
  | EX (_,a) | AX (_,a) -> verifyMuGuarded [] a
857
  | OR (a,b) | AND (a,b)
858
  | EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
859
  | ENFORCES (_,a) | ALLOWS   (_,a)
860
  | MIN (_,_,a)    | MAX (_,_,a)
861
  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
862
  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> verifyMuGuarded [] a
863
  | ID(a) -> verifyMuGuarded [] a
864
  | NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
865
  | CHC (a,b)  -> (proc a ; proc b)
866
  | FUS (_,a) -> proc a
867
  | MU (s, f)
868
  | NU (s, f) ->
869
     let newUnguard = s :: unguarded in
870
     verifyMuGuarded newUnguard f
871
  | VAR s ->
872
     let finder x = compare x s == 0 in
873
     if List.exists finder unguarded then
874
       raise (CoAlgException ("formula not guarded"))
875
  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ ->
876
     raise (CoAlgException ("verifyMuGuarded: CTL should have been removed at this point"))
877

    
878
let verifyFormula formula =
879
  verifyMuAltFree formula;
880
  verifyMuMonotone [] formula;
881
  verifyMuGuarded [] formula
882

    
883
(** These functions parse a token stream to obtain a formula.
884
    It is a standard recursive descent procedure.
885
    @param ts A token stream.
886
    @return The resulting (sub-)formula.
887
    @raise CoAlgException if ts does not represent a formula.
888
 *)
889
let rec parse_formula (symtab: 'a list) ts =
890
  let formula = (parse_imp symtab ts) in
891
  let f1 = convertToMu formula in
892
  match Stream.peek ts with
893
  | None -> f1
894
  | Some (A.Kwd "<=>") ->
895
      Stream.junk ts;
896
      let f2 = parse_formula symtab ts in
897
      EQU (f1, f2)
898
  | _ -> f1
899

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

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

    
932
(** These functions parse a token stream to obtain a formula.
933
    It is a standard recursive descent procedure.
934
    @param ts A token stream.
935
    @return The resulting (sub-)formula.
936
    @raise CoAlgException if ts does not represent a formula.
937
 *)
938
and parse_and symtab ts =
939
  let f1 = parse_cimp symtab ts in
940
  match Stream.peek ts with
941
  | None -> f1
942
  | Some (A.Kwd "&") ->
943
      Stream.junk ts;
944
      let f2 = parse_and symtab ts in
945
      AND (f1, f2)
946
  | _ -> f1
947

    
948
(** These functions parse a token stream to obtain a formula.
949
    It is a standard recursive descent procedure.
950
    @param ts A token stream.
951
    @return The resulting (sub-)formula.
952
    @raise CoAlgException if ts does not represent a formula.
953
 *)
954
and parse_cimp symtab ts =
955
  let f1 = parse_rest symtab ts in
956
  match Stream.peek ts with
957
  | None -> f1
958
  | Some (A.Kwd "=o") ->
959
      Stream.junk ts;
960
      let f2 = parse_cimp symtab ts in
961
      NORM (f1, f2)
962
  | _ -> f1
963

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

    
1173
(** Parses a sorted formula.
1174
    @param ts A token stream.
1175
    @return A sorted formula.
1176
    @raise CoAlgException If ts does not represent a sorted formula.
1177
 *)
1178
let parse_sortedFormula ts =
1179
  let nr =
1180
    match Stream.peek ts with
1181
    | Some (A.Int n) ->
1182
        if n >= 0 then begin
1183
          Stream.junk ts;
1184
          let () =
1185
            match Stream.next ts with
1186
            | A.Kwd ":" -> ()
1187
            | t -> A.printError mk_exn ~t ~ts ("\":\" expected: ")
1188
          in
1189
          n
1190
        end else
1191
          A.printError mk_exn ~ts ("<non-negative number> expected: ")
1192
    | _ -> 0
1193
  in
1194
  let f = parse_formula [] ts in
1195
  (nr, f)
1196

    
1197
(** Parses a list of sorted formulae separated by ";".
1198
    @param ts A token stream.
1199
    @param acc The list of sorted formulae parsed so far.
1200
    @return The resulting list of sorted formula.
1201
    @raise CoAlgException if ts does not represent a list of sorted formulae.
1202
 *)
1203
let rec parse_sortedFormulaList ts acc =
1204
  let f1 = parse_sortedFormula ts in
1205
  match Stream.peek ts with
1206
  | Some (A.Kwd ";") ->
1207
      Stream.junk ts;
1208
      parse_sortedFormulaList ts (f1::acc)
1209
  | _ -> List.rev (f1::acc)
1210

    
1211
(** A common wrapper for import functions.
1212
    @param fkt An import function.
1213
    @param s A string.
1214
    @return The object imported from s using fkt.
1215
    @raise CoAlgException If ts is not empty.
1216
 *)
1217
let importWrapper fkt s =
1218
  let ts = lexer s in
1219
  try
1220
    let res = fkt ts in
1221
    let _ =
1222
      match Stream.peek ts with
1223
      | None -> ()
1224
      | Some _ -> A.printError mk_exn ~ts "EOS expected: "
1225
    in
1226
    res
1227
  with Stream.Failure -> A.printError mk_exn ~ts "unexpected EOS"
1228

    
1229
(** Parses a string to obtain a formula.
1230
    @param s A string representing a formula.
1231
    @return The resulting formula.
1232
    @raise CoAlgException if s does not represent a formula.
1233
 *)
1234
let importFormula s = importWrapper (parse_formula []) s
1235

    
1236
(** Parses a string to obtain a sorted formula.
1237
    @param s A string representing a sorted formula.
1238
    @return The sorted formula.
1239
    @raise CoAlgException If s does not represent a sorted formula.
1240
 *)
1241
let importSortedFormula s = importWrapper parse_sortedFormula s
1242

    
1243
(** Parses a string to obtain a (sorted) formula query.
1244
    @param s A string representing a formula query.
1245
    @return A pair (tbox, f) where
1246
    tbox is a list of sorted formulae representing the TBox; and
1247
    f is a sorted formula.
1248
    @raise CoAlgException if s does not represent a formula query.
1249
 *)
1250
let importQuery s =
1251
  let fkt ts =
1252
    match Stream.peek ts with
1253
    | Some (A.Kwd "|-") ->
1254
        Stream.junk ts;
1255
        let f = parse_sortedFormula ts in
1256
        ([], f)
1257
    | _ ->
1258
        let fl = parse_sortedFormulaList ts [] in
1259
        match Stream.peek ts with
1260
        | Some (A.Kwd "|-") ->
1261
            Stream.junk ts;
1262
            let f = parse_sortedFormula ts in
1263
            (fl, f)
1264
        | _ ->
1265
            if List.length fl = 1 then ([], List.hd fl)
1266
            else A.printError mk_exn ~ts "\"|-\" expected: "
1267
  in
1268
  importWrapper fkt s
1269

    
1270

    
1271
(** Converts the negation of a formula to negation normal form
1272
    by "pushing in" the negations "~".
1273
    The symbols "<=>" and "=>" are substituted by their usual definitions.
1274
    @param f A formula.
1275
    @return A formula in negation normal form and not containing "<=>" or "=>"
1276
    that is equivalent to ~f.
1277
 *)
1278

    
1279
let rec equals f_1 f_2 =
1280
  match f_1, f_2 with
1281
  | TRUE, TRUE -> true 
1282
  | FALSE, FALSE -> true
1283
  | AP s1, AP s2 -> compare s1 s2 = 0
1284
  | VAR f1, VAR f2 -> compare f1 f2 = 0
1285
  | NOT f1, NOT f2 -> equals f1 f2
1286
  | AT(s1,f1), AT(s2,f2) -> (compare s1 s2 = 0) && (equals f1 f2)
1287
  | AND(f1,g1), AND(f2,g2) -> (equals f1 f2) && (equals g1 g2)
1288
  | OR(f1,g1), OR(f2,g2) -> (equals f1 f2) && (equals g1 g2)
1289
  | EQU(f1,g1), EQU(f2,g2) -> (equals f1 f2) && (equals g1 g2) 
1290
  | IMP(f1,g1), IMP(f2,g2) -> (equals f1 f2) && (equals g1 g2)
1291
  | EX(s1,g1), EX(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2)
1292
  | AX(s1,g1), AX(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2)
1293
  | ENFORCES(s1,g1), ENFORCES(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2)
1294
  | ALLOWS(s1,g1), ALLOWS(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2)
1295
  | MIN(n1,s1,g1), MIN(n2,s2,g2) -> (compare n1 n2 = 0) && (compare s1 s2 = 0) && (equals g1 g2)
1296
  | MAX(n1,s1,g1), MAX(n2,s2,g2) -> (compare n1 n2 = 0) && (compare s1 s2 = 0) && (equals g1 g2)
1297
  | MORETHAN(n1,s1,g1), MORETHAN(n2,s2,g2) -> (compare n1 n2 = 0) && (compare s1 s2 = 0) && (equals g1 g2)
1298
  | MAXEXCEPT(n1,s1,g1), MAXEXCEPT(n2,s2,g2) -> (compare n1 n2 = 0) && (compare s1 s2 = 0) && (equals g1 g2)
1299
  | ATLEASTPROB(p1,g1), ATLEASTPROB(p2,g2) -> (compare p1 p2 = 0) && (equals g1 g2)
1300
  | LESSPROBFAIL(p1,g1), LESSPROBFAIL(p2,g2) -> (compare p1 p2 = 0) && (equals g1 g2)
1301
  | CONST s1, CONST s2 -> compare s1 s2 = 0
1302
  | CONSTN s1, CONSTN s2 -> compare s1 s2 = 0
1303
  | ID(f1), ID(f2) -> equals f1 f2
1304
  | NORM(f1,g1),NORM(f2,g2) -> (equals f1 f2) && (equals g1 g2)
1305
  | NORMN(f1,g1), NORMN(f2,g2) -> (equals f1 f2) && (equals g1 g2)
1306
  | CHC(f1,g1), CHC(f2,g2) -> (equals f1 f2) && (equals g1 g2)
1307
  | FUS(b1,g1), FUS(b2,g2) -> (compare b1 b2 = 0) && (equals g1 g2)
1308
  | MU(s1,g1), MU(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2)
1309
  | NU(s1,g1),  NU(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2)
1310
  | _ -> false
1311

    
1312

    
1313
let rec nnfNeg f =
1314
  match f with
1315
  | TRUE -> FALSE
1316
  | FALSE -> TRUE
1317
  | AP _ -> NOT f
1318
  | VAR _ -> f
1319
  | NOT f1 -> nnf f1
1320
  | AT (s, f1) -> AT (s, nnfNeg f1)
1321
  | OR (f1, f2) -> AND (nnfNeg f1, nnfNeg f2)
1322
  | AND (f1, f2) -> OR (nnfNeg f1, nnfNeg f2)
1323
  | EQU (f1, f2) -> OR (AND (nnf f1, nnfNeg f2), AND (nnf f2, nnfNeg f1))
1324
  | IMP (f1, f2) -> AND (nnf f1, nnfNeg f2)
1325
  | EX (s, f1) -> AX (s, nnfNeg f1)
1326
  | AX (s, f1) -> EX (s, nnfNeg f1)
1327
  | ENFORCES (s, f1) -> ALLOWS (s, nnfNeg f1)
1328
  | ALLOWS (s, f1) -> ENFORCES (s, nnfNeg f1)
1329
  | MIN (n, s, f1) -> if n = 0 then FALSE else MAXEXCEPT (n-1, s, nnfNeg f1)
1330
  | MAX (n, s, f1) -> MORETHAN (n, s, nnf f1)
1331
  | MORETHAN (n, s, f1) -> MAXEXCEPT (n, s, nnfNeg f1)
1332
  | MAXEXCEPT (n, s, f1) -> MORETHAN (n, s, nnfNeg f1)
1333
  | ATLEASTPROB (p, f1) -> LESSPROBFAIL (p, nnfNeg f1)
1334
  | LESSPROBFAIL (p, f1) -> ATLEASTPROB (p, nnfNeg f1)
1335
  | CONST s -> CONSTN s
1336
  | CONSTN s -> CONST s
1337
  | ID (f1) -> ID (nnfNeg f1)
1338
  | NORM(f1, f2) -> NORMN(nnfNeg f1, nnfNeg f2)
1339
  | NORMN(f1, f2) -> NORM (nnfNeg f1, nnfNeg f2)
1340
  | CHC (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2)
1341
  | FUS (first, f1) -> FUS (first, nnfNeg f1)
1342
  | MU (s, f1) -> NU(s, nnfNeg f1)
1343
  | NU (s, f1) -> MU(s, nnfNeg f1)
1344
  | AF _ | EF _
1345
  | AG _ | EG _
1346
  | AU _ | EU _
1347
  | AR _ | ER _
1348
  | AB _ | EB _ -> raise (CoAlgException ("nnfNeg: CTL should have been removed at this point"))
1349

    
1350
(** Converts a formula to negation normal form
1351
    by "pushing in" the negations "~".
1352
    The symbols "<=>" and "=>" are substituted by their usual definitions.
1353
    @param f A formula.
1354
    @return A formula in negation normal form and not containing "<=>" or "=>"
1355
    that is equivalent to f.
1356
 *)
1357
and nnf f =
1358
  match f with
1359
  | TRUE
1360
  | FALSE
1361
  | AP _
1362
  | NOT (AP _)
1363
  | CONST _
1364
  | CONSTN _
1365
  | VAR _ -> f
1366
  | NOT f1 -> nnfNeg f1
1367
  | AT (s, f1) ->
1368
      let ft1 = nnf f1 in
1369
      if ft1 == f1 then f else AT (s, ft1)
1370
  | OR (f1, f2) ->
1371
      let ft1 = nnf f1 in
1372
      let ft2 = nnf f2 in
1373
      if ft1 == f1 && ft2 == f2 then f else OR (ft1, ft2)
1374
  | AND (f1, f2) ->
1375
      let ft1 = nnf f1 in
1376
      let ft2 = nnf f2 in
1377
      if ft1 == f1 && ft2 == f2 then f else AND (ft1, ft2)
1378
  | EQU (f1, f2) -> AND (OR (nnfNeg f1, nnf f2), OR (nnfNeg f2, nnf f1))
1379
  | IMP (f1, f2) -> OR (nnfNeg f1, nnf f2)
1380
  | EX (s, f1) ->
1381
      let ft = nnf f1 in
1382
      if ft == f1 then f else EX (s, ft)
1383
  | AX (s, f1) ->
1384
      let ft = nnf f1 in
1385
      if ft == f1 then f else AX (s, ft)
1386
  | ENFORCES (s, f1) ->
1387
      let ft = nnf f1 in
1388
      if ft == f1 then f else ENFORCES (s, ft)
1389
  | ALLOWS (s, f1) ->
1390
      let ft = nnf f1 in
1391
      if ft == f1 then f else ALLOWS (s, ft)
1392
  | MIN (n, s, f1) ->
1393
      if n = 0 then TRUE
1394
      else
1395
        let ft = nnf f1 in
1396
        MORETHAN (n-1,s,ft)
1397
  | MAX (n, s, f1) ->
1398
      let ft = nnfNeg f1 in
1399
      MAXEXCEPT (n,s, ft)
1400
  | MORETHAN (n,s,f1) ->
1401
      let ft = nnf f1 in
1402
      if ft = f1 then f else MORETHAN (n,s,ft)
1403
  | MAXEXCEPT (n,s,f1) ->
1404
      let ft = nnf f1 in
1405
      if ft = f1 then f else MAXEXCEPT (n,s,ft)
1406
  | ATLEASTPROB (p, f1) ->
1407
      let ft = nnf f1 in
1408
      if ft == f1 then f else ATLEASTPROB (p, ft)
1409
  | LESSPROBFAIL (p, f1) ->
1410
      let ft = nnf f1 in
1411
      if ft == f1 then f else LESSPROBFAIL (p, ft)
1412
  | ID (f1) ->
1413
    let ft = nnf f1 in
1414
    if ft == f1 then f else ID(ft)
1415
  | NORM (f1, f2) ->
1416
      let ft1 = nnf f1 in
1417
      let ft2 = nnf f2 in
1418
      if ft1 == f1 && ft2 == f2 then f else NORM (ft1, ft2)
1419
  | NORMN (f1, f2) ->
1420
      let ft1 = nnf f1 in
1421
      let ft2 = nnf f2 in
1422
      if ft1 == f1 && ft2 == f2 then f else NORMN (ft1, ft2)
1423
  | CHC (f1, f2) ->
1424
      let ft1 = nnf f1 in
1425
      let ft2 = nnf f2 in
1426
      if ft1 == f1 && ft2 == f2 then f else CHC (ft1, ft2)
1427
  | FUS (first, f1) ->
1428
      let ft = nnf f1 in
1429
      if ft == f1 then f else FUS (first, ft)
1430
  | MU (s, f1) ->
1431
      let ft = nnf f1 in
1432
      if ft == f1 then f else MU (s, ft)
1433
  | NU (s, f1) ->
1434
      let ft = nnf f1 in
1435
      if ft == f1 then f else NU (s, ft)
1436
  | AF _ | EF _
1437
  | AG _ | EG _
1438
  | AU _ | EU _
1439
  | AR _ | ER _
1440
  | AB _ | EB _ ->
1441
            raise (CoAlgException ("nnf: CTL should have been removed at this point"))
1442

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

    
1635
(** Destructs an atomic proposition.
1636
    @param f An atomic proposition.
1637
    @return The name of the atomic proposition.
1638
    @raise CoAlgException if f is not an atomic proposition.
1639
 *)
1640
let dest_ap f =
1641
  match f with
1642
  | AP s when not (isNominal s) -> s
1643
  | _ -> raise (CoAlgException "Formula is not an atomic proposition.")
1644

    
1645
(** Destructs a nominal.
1646
    @param f A nominal.
1647
    @return The name of the nominal
1648
    @raise CoAlgException if f is not a nominal.
1649
 *)
1650
let dest_nom f =
1651
  match f with
1652
  | AP s when isNominal s -> s
1653
  | _ -> raise (CoAlgException "Formula is not a nominal.")
1654

    
1655
(** Destructs a negation.
1656
    @param f A negation.
1657
    @return The immediate subformula of the negation.
1658
    @raise CoAlgException if f is not a negation.
1659
 *)
1660
let dest_not f =
1661
  match f with
1662
  | NOT f1 -> f1
1663
  | _ -> raise (CoAlgException "Formula is not a negation.")
1664

    
1665
(** Destructs an @-formula.
1666
    @param f An @-formula.
1667
    @return The name of the nominal and the immediate subformula of the @-formula.
1668
    @raise CoAlgException if f is not an @-formula.
1669
 *)
1670
let dest_at f =
1671
  match f with
1672
  | AT (s, f1) -> (s, f1)
1673
  | _ -> raise (CoAlgException "Formula is not an @-formula.")
1674

    
1675
(** Destructs an or-formula.
1676
    @param f An or-formula.
1677
    @return The two immediate subformulae of the or-formula.
1678
    @raise CoAlgException if f is not an or-formula.
1679
 *)
1680
let dest_or f =
1681
  match f with
1682
  | OR (f1, f2) -> (f1, f2)
1683
  | _ -> raise (CoAlgException "Formula is not an or-formula.")
1684

    
1685
(** Destructs an and-formula.
1686
    @param f An and-formula.
1687
    @return The two immediate subformulae of the and-formula.
1688
    @raise CoAlgException if f is not an and-formula.
1689
 *)
1690
let dest_and f =
1691
  match f with
1692
  | AND (f1, f2) -> (f1, f2)
1693
  | _ -> raise (CoAlgException "Formula is not an and-formula.")
1694

    
1695
(** Destructs an equivalence.
1696
    @param f An equivalence.
1697
    @return The two immediate subformulae of the equivalence.
1698
    @raise CoAlgException if f is not an equivalence.
1699
 *)
1700
let dest_equ f =
1701
  match f with
1702
  | EQU (f1, f2) -> (f1, f2)
1703
  | _ -> raise (CoAlgException "Formula is not an equivalence.")
1704

    
1705
(** Destructs an implication.
1706
    @param f An implication.
1707
    @return The two immediate subformulae of the implication.
1708
    @raise CoAlgException if f is not an implication.
1709
 *)
1710
let dest_imp f =
1711
  match f with
1712
  | IMP (f1, f2) -> (f1, f2)
1713
  | _ -> raise (CoAlgException "Formula is not an implication.")
1714

    
1715
(** Destructs an EX-formula.
1716
    @param f An EX-formula.
1717
    @return The role name and the immediate subformula of the EX-formula.
1718
    @raise CoAlgException if f is not an EX-formula.
1719
 *)
1720
let dest_ex f =
1721
  match f with
1722
  | EX (s, f1) -> (s, f1)
1723
  | _ -> raise (CoAlgException "Formula is not an EX-formula.")
1724

    
1725
(** Destructs an AX-formula.
1726
    @param f An AX-formula.
1727
    @return The role name and the immediate subformula of the AX-formula.
1728
    @raise CoAlgException if f is not an AX-formula.
1729
 *)
1730
let dest_ax f =
1731
  match f with
1732
  | AX (s, f1) -> (s, f1)
1733
  | _ -> raise (CoAlgException "Formula is not an AX-formula.")
1734

    
1735
(** Destructs a MIN-formula.
1736
    @param f A MIN-formula.
1737
    @return The number restriction, role name,
1738
    and the immediate subformula of the MIN-formula.
1739
    @raise CoAlgException if f is not a MIN-formula.
1740
 *)
1741
let dest_min f =
1742
  match f with
1743
  | MIN (n, s, f1) -> (n, s, f1)
1744
  | _ -> raise (CoAlgException "Formula is not a MIN-formula.")
1745

    
1746
(** Destructs a MAX-formula.
1747
    @param f A MAX-formula.
1748
    @return The number restriction, role name,
1749
    and the immediate subformula of the MAX-formula.
1750
    @raise CoAlgException if f is not a MAX-formula.
1751
 *)
1752
let dest_max f =
1753
  match f with
1754
  | MAX (n, s, f1) -> (n, s, f1)
1755
  | _ -> raise (CoAlgException "Formula is not a MAX-formula.")
1756

    
1757
(** Destructs a choice formula.
1758
    @param f A choice formula.
1759
    @return The two immediate subformulae of the choice formula.
1760
    @raise CoAlgException if f is not a choice formula.
1761
 *)
1762
let dest_choice f =
1763
  match f with
1764
  | CHC (f1, f2) -> (f1, f2)
1765
  | _ -> raise (CoAlgException "Formula is not a choice formula.")
1766

    
1767
(** Destructs a fusion formula.
1768
    @param f A fusion formula.
1769
    @return A pair (first, f1) where
1770
    first is true iff f is a first projection; and
1771
    f1 is the immediate subformulae of f.
1772
    @raise CoAlgException if f is not a fusion formula.
1773
 *)
1774
let dest_fusion f =
1775
  match f with
1776
  | FUS (first, f1) -> (first, f1)
1777
  | _ -> raise (CoAlgException "Formula is not a fusion formula.")
1778

    
1779

    
1780
(** Tests whether a formula is the constant True.
1781
    @param f A formula.
1782
    @return True iff f is the constant True.
1783
 *)
1784
let is_true f =
1785
  match f with
1786
  | TRUE -> true
1787
  | _ -> false
1788

    
1789
(** Tests whether a formula is the constant False.
1790
    @param f A formula.
1791
    @return True iff f is the constant False.
1792
 *)
1793
let is_false f =
1794
  match f with
1795
  | FALSE -> true
1796
  | _ -> false
1797

    
1798
(** Tests whether a formula is an atomic proposition.
1799
    @param f A formula.
1800
    @return True iff f is an atomic proposition.
1801
 *)
1802
let is_ap f =
1803
  match f with
1804
  | AP s when not (isNominal s) -> true
1805
  | _ -> false
1806

    
1807
(** Tests whether a formula is a nominal.
1808
    @param f A formula.
1809
    @return True iff f is a nominal.
1810
 *)
1811
let is_nom f =
1812
  match f with
1813
  | AP s when isNominal s -> true
1814
  | _ -> false
1815

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

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

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

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

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

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

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

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

    
1888
(** Tests whether a formula is a MIN-formula.
1889
    @param f A formula.
1890
    @return True iff f is a MIN-formula.
1891
 *)
1892
let is_min f =
1893
  match f with
1894
  | MIN _ -> true
1895
  | _ -> false
1896

    
1897
(** Tests whether a formula is a MAX-formula.
1898
    @param f A formula.
1899
    @return True iff f is a MAX-formula.
1900
 *)
1901
let is_max f =
1902
  match f with
1903
  | MAX _ -> true
1904
  | _ -> false
1905

    
1906
(** Tests whether a formula is a choice formula.
1907
    @param f A formula.
1908
    @return True iff f is a choice formula.
1909
 *)
1910
let is_choice f =
1911
  match f with
1912
  | CHC _ -> true
1913
  | _ -> false
1914

    
1915
(** Tests whether a formula is a fusion formula.
1916
    @param f A formula.
1917
    @return True iff f is a fusion formula.
1918
 *)
1919
let is_fusion f =
1920
  match f with
1921
  | FUS _ -> true
1922
  | _ -> false
1923

    
1924

    
1925
(** The constant True.
1926
 *)
1927
let const_true = TRUE
1928

    
1929
(** The constant False.
1930
 *)
1931
let const_false = FALSE
1932

    
1933
(** Constructs an atomic proposition.
1934
    @param s The name of the atomic proposition.
1935
    @return The atomic proposition with name s.
1936
    @raise CoAlgException if s is a nominal name.
1937
 *)
1938
let const_ap s =
1939
  if isNominal s then raise (CoAlgException "The name indicates a nominal.")
1940
  else AP s
1941

    
1942
(** Constructs a nominal.
1943
    @param s The name of the nominal.
1944
    @return A nominal with name s.
1945
    @raise CoAlgException if s is not a nominal name.
1946
 *)
1947
let const_nom s =
1948
  if isNominal s then AP s
1949
  else raise (CoAlgException "The name does not indicate a nominal.")
1950

    
1951
(** Negates a formula.
1952
    @param f A formula.
1953
    @return The negation of f.
1954
 *)
1955
let const_not f = NOT f
1956

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

    
1964
(** Constructs an or-formula from two formulae.
1965
    @param f1 The first formula (LHS).
1966
    @param f2 The second formula (LHS).
1967
    @return The formula f1 | f2.
1968
 *)
1969
let const_or f1 f2 = OR (f1, f2)
1970

    
1971
(** Constructs an and-formula from two formulae.
1972
    @param f1 The first formula (LHS).
1973
    @param f2 The second formula (LHS).
1974
    @return The formula f1 & f2.
1975
 *)
1976
let const_and f1 f2 = AND (f1, f2)
1977

    
1978
(** Constructs an equivalence from two formulae.
1979
    @param f1 The first formula (LHS).
1980
    @param f2 The second formula (LHS).
1981
    @return The equivalence f1 <=> f2.
1982
 *)
1983
let const_equ f1 f2 = EQU (f1, f2)
1984

    
1985
(** Constructs an implication from two formulae.
1986
    @param f1 The first formula (LHS).
1987
    @param f2 The second formula (LHS).
1988
    @return The implication f1 => f2.
1989
 *)
1990
let const_imp f1 f2 = IMP (f1, f2)
1991

    
1992
(** Constructs an EX-formula from a formula.
1993
    @param s A role name.
1994
    @param f A formula.
1995
    @return The formula EX (s, f).
1996
 *)
1997
let const_ex s f = EX (s, f)
1998

    
1999
(** Constructs an AX-formula from a formula.
2000
    @param s A role name.
2001
    @param f A formula.
2002
    @return The formula AX (s, f).
2003
 *)
2004
let const_ax s f = AX (s, f)
2005

    
2006
(** Constructs a MIN-formula from a formula.
2007
    @param n A non-negative integer.
2008
    @param s A role name.
2009
    @param f A formula.
2010
    @return The formula MIN f.
2011
    @raise CoAlgException Iff n is negative.
2012
 *)
2013
let const_min n s f =
2014
  if n < 0 then raise (CoAlgException "Negative cardinality constraint.")
2015
  else MIN (n, s, f)
2016

    
2017
(** Constructs a MAX-formula from a formula.
2018
    @param n A non-negative integer.
2019
    @param s A role name.
2020
    @param f A formula.
2021
    @return The formula MAX f.
2022
    @raise CoAlgException Iff n is negative.
2023
 *)
2024
let const_max n s f =
2025
  if n < 0 then raise (CoAlgException "Negative cardinality constraint.")
2026
  else MAX (n, s, f)
2027

    
2028
let const_enforces p f =
2029
    ENFORCES (p,f)
2030

    
2031
let const_allows p f =
2032
    ALLOWS (p,f)
2033

    
2034
(** Constructs a choice formula from two formulae.
2035
    @param f1 The first formula (LHS).
2036
    @param f2 The second formula (LHS).
2037
    @return The formula (f1 + f2).
2038
 *)
2039
let const_choice f1 f2 = CHC (f1, f2)
2040

    
2041
(** Constructs a fusion formula.
2042
    @param first True iff the result is a first projection.
2043
    @param f1 A formula.
2044
    @return The formula [pi1] f1 or [pi2] f1 (depending on first).
2045
 *)
2046
let const_fusion first f1 = FUS (first, f1)
2047

    
2048

    
2049
(** Hash-consed formulae, which are in negation normal form,
2050
    such that structural and physical equality coincide.
2051

    
2052
    Also CTL has been replaced by the equivalent μ-Calculus
2053
    constructs
2054
 *)
2055
type hcFormula = (hcFormula_node, formula) HC.hash_consed
2056
and hcFormula_node =
2057
  | HCTRUE
2058
  | HCFALSE
2059
  | HCAP of string
2060
  | HCNOT of string
2061
  | HCAT of string * hcFormula
2062
  | HCOR of hcFormula * hcFormula
2063
  | HCAND of hcFormula * hcFormula
2064
  | HCEX of string * hcFormula
2065
  | HCAX of string * hcFormula
2066
  | HCENFORCES of int list * hcFormula
2067
  | HCALLOWS of int list * hcFormula
2068
  | HCMORETHAN of int * string * hcFormula (* GML Diamond *)
2069
  | HCMAXEXCEPT of int * string * hcFormula (* GML Box *)
2070
  | HCATLEASTPROB of rational * hcFormula
2071
  | HCLESSPROBFAIL of rational * hcFormula
2072
  | HCCONST of string
2073
  | HCCONSTN of string
2074
  | HCID of hcFormula
2075
  | HCNORM of hcFormula * hcFormula
2076
  | HCNORMN of hcFormula * hcFormula
2077
  | HCCHC of hcFormula * hcFormula
2078
  | HCFUS of bool * hcFormula
2079
  | HCMU of string * hcFormula
2080
  | HCNU of string * hcFormula
2081
  | HCVAR of string
2082

    
2083
(** Determines whether two formula nodes are structurally equal.
2084
    @param f1 The first formula node.
2085
    @param f2 The second formula node.
2086
    @return True iff f1 and f2 are structurally equal.
2087
 *)
2088
let equal_hcFormula_node f1 f2 =
2089
  match f1, f2 with
2090
  | HCTRUE, HCTRUE -> true
2091
  | HCFALSE, HCFALSE -> true
2092
  | HCCONST s1, HCCONST s2
2093
  | HCCONSTN s1, HCCONSTN s2
2094
  | HCAP s1, HCAP s2
2095
  | HCNOT s1, HCNOT s2 -> compare s1 s2 = 0
2096
  | HCAT (s1, f1), HCAT (s2, f2) -> compare s1 s2 = 0 && f1 == f2
2097
  | HCOR (f1a, f1b), HCOR (f2a, f2b)
2098
  | HCAND (f1a, f1b), HCAND (f2a, f2b) -> f1a == f2a && f1b == f2b
2099
  | HCEX (s1, f1), HCEX (s2, f2)
2100
  | HCAX (s1, f1), HCAX (s2, f2) -> compare s1 s2 = 0 && f1 == f2
2101
  | HCENFORCES (s1, f1), HCENFORCES (s2, f2)
2102
  | HCALLOWS (s1, f1), HCALLOWS (s2, f2) -> compare s1 s2 = 0 && f1 == f2
2103
  | HCMORETHAN (n1, s1, f1), HCMORETHAN (n2, s2, f2)
2104
  | HCMAXEXCEPT (n1, s1, f1), HCMAXEXCEPT (n2, s2, f2) ->
2105
      n1 = n2 && compare s1 s2 = 0 && f1 == f2
2106
  | HCATLEASTPROB (p1, f1), HCATLEASTPROB (p2,f2) ->
2107
      p1 = p2 && f1 == f2
2108
  | HCLESSPROBFAIL (p1, f1), HCLESSPROBFAIL (p2,f2) ->
2109
      p1 = p2 && f1 == f2
2110
  | HCID f1, HCID f2 -> f1 == f2
2111
  | HCNORM (f1a, f1b), HCNORMN (f2a, f2b) -> f1a == f2a && f1b == f2b
2112
  | HCCHC (f1a, f1b), HCCHC (f2a, f2b) -> f1a == f2a && f1b == f2b
2113
  | HCFUS (first1, f1), HCFUS (first2, f2) -> first1 = first2 && f1 == f2
2114
  | HCMU (name1, f1), HCMU(name2, f2) -> compare name1 name2 = 0 && f1 == f2
2115
  | HCNU (name1, f1), HCNU(name2, f2) -> compare name1 name2 = 0 && f1 == f2
2116
  | HCVAR name1, HCVAR name2 -> compare name1 name2 = 0
2117
(* The rest could be shortened to | _ -> false,
2118
   but then the compiler would not warn if the formula type is extended
2119
   and this function is not updated accordingly.*)
2120
  | HCTRUE, _
2121
  | HCFALSE, _
2122
  | HCAP _, _
2123
  | HCNOT _, _
2124
  | HCAT _, _
2125
  | HCOR _, _
2126
  | HCAND _, _
2127
  | HCEX _, _
2128
  | HCAX _, _
2129
  | HCENFORCES _, _
2130
  | HCALLOWS   _, _
2131
  | HCMORETHAN _, _
2132
  | HCMAXEXCEPT _, _
2133
  | HCATLEASTPROB _, _
2134
  | HCLESSPROBFAIL _, _
2135
  | HCCONST _, _
2136
  | HCCONSTN _, _
2137
  | HCID _, _
2138
  | HCNORM _, _
2139
  | HCNORMN _, _
2140
  | HCCHC _, _
2141
  | HCFUS _, _
2142
  | HCMU _, _
2143
  | HCNU _, _
2144
  | HCVAR _, _ -> false
2145

    
2146
(** Computes the hash value of a formula node.
2147
    @param f A formula node.
2148
    @return The hash value of f.
2149
 *)
2150
let hash_hcFormula_node f =
2151
  let base = 23 in (* should be larger than the no of constructors *)
2152
  match f with
2153
  | HCTRUE -> 0
2154
  | HCFALSE -> 1
2155
  | HCAP s
2156
  | HCNOT s
2157
  | HCVAR s -> base * Hashtbl.hash s + 1
2158
  | HCAT (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 2
2159
  | HCOR (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 5
2160
  | HCAND (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 6
2161
  | HCEX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 3
2162
  | HCAX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 4
2163
  | HCMORETHAN (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 7
2164
  | HCMAXEXCEPT (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 8
2165
  | HCATLEASTPROB (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 9
2166
  | HCLESSPROBFAIL (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 10
2167
  | HCCHC (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 11
2168
  | HCFUS (first, f1) -> base * (base * (Hashtbl.hash first) + f1.HC.hkey) + 13
2169
  | HCENFORCES (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 14
2170
  | HCALLOWS   (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 15
2171
  | HCCONST s -> Hashtbl.hash s + 16
2172
  | HCCONSTN s -> Hashtbl.hash s + 17
2173
  | HCNORM (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 18
2174
  | HCNORMN (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 19
2175
  | HCID (f1) -> base * f1.HC.hkey + 20
2176
  | HCMU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 21
2177
  | HCNU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 22
2178

    
2179
(** Determines the "real" formula of a formula node.
2180
    @param f A formula node.
2181
    @return The formula (in negation normal form) which corresponds to f.
2182
 *)
2183
let toFml_hcFormula_node f =
2184
  match f with
2185
  | HCTRUE -> TRUE
2186
  | HCFALSE -> FALSE
2187
  | HCAP s -> AP s
2188
  | HCVAR s -> VAR s
2189
  | HCNOT s -> NOT (AP s)
2190
  | HCAT (s, f1) -> AT (s, f1.HC.fml)
2191
  | HCOR (f1, f2) -> OR (f1.HC.fml, f2.HC.fml)
2192
  | HCAND (f1, f2) -> AND (f1.HC.fml, f2.HC.fml)
2193
  | HCEX (s, f1) -> EX (s, f1.HC.fml)
2194
  | HCAX (s, f1) -> AX (s, f1.HC.fml)
2195
  | HCENFORCES (s, f1) -> ENFORCES (s, f1.HC.fml)
2196
  | HCALLOWS (s, f1) -> ALLOWS (s, f1.HC.fml)
2197
  | HCMORETHAN (n, s, f1) -> MORETHAN (n, s, f1.HC.fml)
2198
  | HCMAXEXCEPT (n, s, f1) -> MAXEXCEPT (n, s, f1.HC.fml)
2199
  | HCATLEASTPROB (p, f1) -> ATLEASTPROB (p, f1.HC.fml)
2200
  | HCLESSPROBFAIL (p, f1) -> LESSPROBFAIL (p, f1.HC.fml)
2201
  | HCCONST s -> CONST s
2202
  | HCCONSTN s -> CONSTN s
2203
  | HCID (f1) -> ID(f1.HC.fml)
2204
  | HCNORM (f1, f2) -> NORM(f1.HC.fml, f2.HC.fml)
2205
  | HCNORMN (f1, f2) -> NORMN(f1.HC.fml, f2.HC.fml)
2206
  | HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml)
2207
  | HCFUS (first, f1) -> FUS (first, f1.HC.fml)
2208
  | HCMU (var, f1) -> MU (var, f1.HC.fml)
2209
  | HCNU (var, f1) -> NU (var, f1.HC.fml)
2210

    
2211
(** Determines the negation (in negation normal form) of a formula node.
2212
    @param f A formula node.
2213
    @return The negation (in negation normal form) of f.
2214
 *)
2215
let negNde_hcFormula_node f =
2216
  match f with
2217
  | HCTRUE -> HCFALSE
2218
  | HCFALSE -> HCTRUE
2219
  | HCAP s -> HCNOT s
2220
  | HCNOT s -> HCAP s
2221
  | HCVAR s -> f
2222
  | HCAT (s, f1) -> HCAT (s, f1.HC.neg)
2223
  | HCOR (f1, f2) -> HCAND (f1.HC.neg, f2.HC.neg)
2224
  | HCAND (f1, f2) -> HCOR (f1.HC.neg, f2.HC.neg)
2225
  | HCEX (s, f2) -> HCAX (s, f2.HC.neg)
2226
  | HCAX (s, f2) -> HCEX (s, f2.HC.neg)
2227
  | HCENFORCES (s, f2) -> HCALLOWS (s, f2.HC.neg)
2228
  | HCALLOWS (s, f2) -> HCENFORCES (s, f2.HC.neg)
2229
  | HCMORETHAN (n, s, f1) -> HCMAXEXCEPT (n, s, f1.HC.neg)
2230
  | HCMAXEXCEPT (n, s, f1) -> HCMORETHAN (n, s, f1.HC.neg)
2231
  | HCATLEASTPROB (p, f1) -> HCLESSPROBFAIL (p, f1.HC.neg)
2232
  | HCLESSPROBFAIL (p, f1) -> HCATLEASTPROB (p, f1.HC.neg)
2233
  | HCCONST s -> HCCONSTN s
2234
  | HCCONSTN s -> HCCONST s
2235
  | HCID (f1) -> HCID(f1.HC.neg)
2236
  | HCNORM (f1, f2) -> HCNORMN(f1.HC.neg, f2.HC.neg)
2237
  | HCNORMN (f1, f2) -> HCNORM(f1.HC.neg, f2.HC.neg)
2238
  | HCCHC (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg)
2239
  | HCFUS (first, f1) -> HCFUS (first, f1.HC.neg)
2240
  | HCMU (name, f1) -> HCNU (name, f1.HC.neg)
2241
  | HCNU (name, f1) -> HCMU (name, f1.HC.neg)
2242

    
2243
(** An instantiation of hash-consing for formulae.
2244
 *)
2245
module HcFormula = HC.Make(
2246
  struct
2247
    type nde = hcFormula_node
2248
    type fml = formula
2249
    let equal (n1 : nde) n2 = equal_hcFormula_node n1 n2
2250
    let hash (n : nde) = hash_hcFormula_node n
2251
    let negNde (n : nde) = negNde_hcFormula_node n
2252
    let toFml (n : nde) = toFml_hcFormula_node n
2253
  end
2254
 )
2255

    
2256
(** Converts a formula into its hash-consed version.
2257
    @param hcF A hash-cons table for formulae.
2258
    @param f A formula in negation normal form.
2259
    @return The hash-consed version of f.
2260
    @raise CoAlgException if f is not in negation normal form.
2261
*)
2262
let rec hc_formula hcF f =
2263
  match f with
2264
  | TRUE -> HcFormula.hashcons hcF HCTRUE
2265
  | FALSE -> HcFormula.hashcons hcF HCFALSE
2266
  | AP s -> HcFormula.hashcons hcF (HCAP s)
2267
  | VAR s -> HcFormula.hashcons hcF (HCVAR s)
2268
  | NOT (AP s) -> HcFormula.hashcons hcF (HCNOT s)
2269
  | AT (s, f1) ->
2270
      let tf1 = hc_formula hcF f1 in
2271
      HcFormula.hashcons hcF (HCAT (s, tf1))
2272
  | OR (f1, f2) ->
2273
      let tf1 = hc_formula hcF f1 in
2274
      let tf2 = hc_formula hcF f2 in
2275
      HcFormula.hashcons hcF (HCOR (tf1, tf2))
2276
  | AND (f1, f2) ->
2277
      let tf1 = hc_formula hcF f1 in
2278
      let tf2 = hc_formula hcF f2 in
2279
      HcFormula.hashcons hcF (HCAND (tf1, tf2))
2280
  | NOT _
2281
  | EQU _
2282
  | MIN _
2283
  | MAX _
2284
  | IMP _ -> raise (CoAlgException "Formula is not in negation normal form.")
2285
  | EX (s, f1) ->
2286
      let tf1 = hc_formula hcF f1 in
2287
      HcFormula.hashcons hcF (HCEX (s, tf1))
2288
  | AX (s, f1) ->
2289
      let tf1 = hc_formula hcF f1 in
2290
      HcFormula.hashcons hcF (HCAX (s, tf1))
2291
  | ENFORCES (s, f1) ->
2292
      let tf1 = hc_formula hcF f1 in
2293
      HcFormula.hashcons hcF (HCENFORCES (s, tf1))
2294
  | ALLOWS (s, f1) ->
2295
      let tf1 = hc_formula hcF f1 in
2296
      HcFormula.hashcons hcF (HCALLOWS (s, tf1))
2297
  | MORETHAN  (n, s, f1) ->
2298
      let tf1 = hc_formula hcF f1 in
2299
      HcFormula.hashcons hcF (HCMORETHAN (n, s, tf1))
2300
  | MAXEXCEPT  (n, s, f1) ->
2301
      let tf1 = hc_formula hcF f1 in
2302
      HcFormula.hashcons hcF (HCMAXEXCEPT (n, s, tf1))
2303
  | ATLEASTPROB (p, f1) ->
2304
      HcFormula.hashcons hcF (HCATLEASTPROB (p, hc_formula hcF f1))
2305
  | LESSPROBFAIL (p, f1) ->
2306
      HcFormula.hashcons hcF (HCLESSPROBFAIL (p, hc_formula hcF f1))
2307
  | CONST s ->
2308
      HcFormula.hashcons hcF (HCCONST s)
2309
  | CONSTN s ->
2310
      HcFormula.hashcons hcF (HCCONSTN s)
2311
  | ID f1 ->
2312
    let tf1 = hc_formula hcF f1 in
2313
      HcFormula.hashcons hcF (HCID tf1)
2314
  | NORM (f1, f2) ->
2315
      let tf1 = hc_formula hcF f1 in
2316
      let tf2 = hc_formula hcF f2 in
2317
      HcFormula.hashcons hcF (HCNORM (tf1, tf2))
2318
  | NORMN (f1, f2) ->
2319
      let tf1 = hc_formula hcF f1 in
2320
      let tf2 = hc_formula hcF f2 in
2321
      HcFormula.hashcons hcF (HCNORMN (tf1, tf2))
2322
  | CHC (f1, f2) ->
2323
      let tf1 = hc_formula hcF f1 in
2324
      let tf2 = hc_formula hcF f2 in
2325
      HcFormula.hashcons hcF (HCCHC (tf1, tf2))
2326
  | FUS (first, f1) ->
2327
      let tf1 = hc_formula hcF f1 in
2328
      HcFormula.hashcons hcF (HCFUS (first, tf1))
2329
  | MU (var, f1) ->
2330
     let tf1 = hc_formula hcF f1 in
2331
     HcFormula.hashcons hcF (HCMU (var, tf1))
2332
  | NU (var, f1) ->
2333
     let tf1 = hc_formula hcF f1 in
2334
     HcFormula.hashcons hcF (HCNU (var, tf1))
2335
  | AF _ | EF _
2336
  | AG _ | EG _
2337
  | AU _ | EU _
2338
  | AR _ | ER _
2339
  | AB _ | EB _ ->
2340
     raise (CoAlgException ("nnf: CTL should have been removed at this point"))
2341

    
2342
(* Replace the Variable name in f with formula formula
2343
   hc_replace foo φ ψ => ψ[foo |-> φ]
2344
 *)
2345
let rec hc_replace hcF name (formula: hcFormula) (f: hcFormula) =
2346
  let func = hc_replace hcF name formula in
2347
  let gennew = HcFormula.hashcons hcF in
2348
  match f.HC.node with
2349
  | HCTRUE
2350
  | HCFALSE
2351
  | HCAP _
2352
  | HCNOT _
2353
  | HCCONST _
2354
  | HCCONSTN _ -> f
2355
  | HCVAR s ->
2356
     if compare s name == 0
2357
     then formula
2358
     else f
2359
  | HCAT (s, f1) ->
2360
     let nf1 = func f1 in
2361
     if nf1 == f1 then f else gennew (HCAT(s, nf1))
2362
  | HCOR (f1, f2) ->
2363
     let nf1 = func f1 in
2364
     let nf2 = func f2 in
2365
     if nf1 == f1 && nf2 == f2 then f else gennew (HCOR(nf1, nf2))
2366
  | HCAND (f1, f2) ->
2367
     let nf1 = func f1 in
2368
     let nf2 = func f2 in
2369
     if nf1 == f1 && nf2 == f2 then f else gennew (HCAND(nf1, nf2))
2370
  | HCEX (s, f1) ->
2371
     let nf1 = func f1 in
2372
     if nf1 == f1 then f else gennew (HCEX(s, nf1))
2373
  | HCAX (s, f1) ->
2374
     let nf1 = func f1 in
2375
     if nf1 == f1 then f else gennew (HCAX(s, nf1))
2376
  | HCENFORCES (s, f1) ->
2377
     let nf1 = func f1 in
2378
     if nf1 == f1 then f else gennew (HCENFORCES(s, nf1))
2379
  | HCALLOWS (s, f1) ->
2380
     let nf1 = func f1 in
2381
     if nf1 == f1 then f else gennew (HCALLOWS(s, nf1))
2382
  | HCMORETHAN  (n, s, f1) ->
2383
     let nf1 = func f1 in
2384
     if nf1 == f1 then f else gennew (HCMORETHAN(n, s, nf1))
2385
  | HCMAXEXCEPT  (n, s, f1) ->
2386
     let nf1 = func f1 in
2387
     if nf1 == f1 then f else gennew (HCMAXEXCEPT(n, s, nf1))
2388
  | HCATLEASTPROB (p, f1) ->
2389
     let nf1 = func f1 in
2390
     if nf1 == f1 then f else gennew (HCATLEASTPROB(p, nf1))
2391
  | HCLESSPROBFAIL (p, f1) ->
2392
     let nf1 = func f1 in
2393
     if nf1 == f1 then f else gennew (HCLESSPROBFAIL(p, nf1))
2394
  | HCID f1 ->
2395
     let nf1 = func f1 in
2396
     if nf1 == f1 then f else gennew (HCID(nf1))
2397
  | HCNORM (f1, f2) ->
2398
     let nf1 = func f1 in
2399
     let nf2 = func f2 in
2400
     if nf1 == f1 && nf2 == f2 then f else gennew (HCNORM(nf1, nf2))
2401
  | HCNORMN (f1, f2) ->
2402
     let nf1 = func f1 in
2403
     let nf2 = func f2 in
2404
     if nf1 == f1 && nf2 == f2 then f else gennew (HCNORMN(nf1, nf2))
2405
  | HCCHC (f1, f2) ->
2406
     let nf1 = func f1 in
2407
     let nf2 = func f2 in
2408
     if nf1 == f1 && nf2 == f2 then f else gennew (HCCHC(nf1, nf2))
2409
  | HCFUS (first, f1) ->
2410
     let nf1 = func f1 in
2411
     if nf1 == f1 then f else gennew (HCFUS(first, nf1))
2412
  | HCMU (var, f1) ->
2413
     if compare var name != 0 then
2414
       let nf1 = func f1 in
2415
       if nf1 == f1 then f else gennew (HCMU(var, nf1))
2416
     else
2417
       f
2418
  | HCNU (var, f1) ->
2419
     if compare var name != 0 then
2420
       let nf1 = func f1 in
2421
       if nf1 == f1 then f else gennew (HCNU(var, nf1))
2422
     else
2423
       f
2424

    
2425
let rec hc_freeIn variable (f: hcFormula) =
2426
  match f.HC.node with
2427
  | HCTRUE
2428
  | HCFALSE
2429
  | HCAP _
2430
  | HCNOT _
2431
  | HCCONST _
2432
  | HCCONSTN _ -> false
2433
  | HCVAR s ->
2434
     if compare variable s == 0
2435
     then true
2436
     else false
2437
  | HCAT (s, f1) ->
2438
     hc_freeIn variable f1
2439
  | HCOR (f1, f2)
2440
  | HCAND (f1, f2) ->
2441
     hc_freeIn variable f1 || hc_freeIn variable f2
2442
  | HCEX (_, f1)
2443
  | HCAX (_, f1)
2444
  | HCENFORCES (_, f1)
2445
  | HCALLOWS (_, f1)
2446
  | HCMORETHAN  (_, _, f1)
2447
  | HCMAXEXCEPT  (_, _, f1)
2448
  | HCATLEASTPROB (_, f1)
2449
  | HCLESSPROBFAIL (_, f1)
2450
  | HCID f1 ->
2451
     hc_freeIn variable f1
2452
  | HCNORM (f1, f2)
2453
  | HCNORMN (f1, f2)
2454
  | HCCHC (f1, f2) ->
2455
     hc_freeIn variable f1 || hc_freeIn variable f2
2456
  | HCFUS (first, f1) ->
2457
     hc_freeIn variable f1
2458
  | HCMU (var, f1)
2459
  | HCNU (var, f1) ->
2460
     (* Do we need to exclude bound variables here? *)
2461
     hc_freeIn variable f1
2462

    
2463

    
2464
(** An instantiation of a hash table (of the standard library)
2465
    for hash-consed formulae. The test for equality
2466
    and computing the hash value is done in constant time.
2467
 *)
2468
module HcFHt = Hashtbl.Make(
2469
  struct
2470
    type t = hcFormula
2471
    let equal (f1 : t) f2 = f1.HC.tag = f2.HC.tag
2472
    let hash (f : t) = f.HC.tag
2473
  end
2474
 )
2475

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