Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgFormula.ml @ 40a714df

History | View | Annotate | Download (69.2 KB)

1 4fd28192 Thorsten Wißmann
(** 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 f1fa9ad5 Thorsten Wißmann
module L = List
10
module Str = String
11 4fd28192 Thorsten Wißmann
12
13
(** A general exception for all kinds of errors
14
    that can happen in the tableau procedure.
15 c5c25acf Christoph Egger
    More specific information is given in the argument.
16 4fd28192 Thorsten Wißmann
 *)
17
exception CoAlgException of string
18
19
(** Indicates the sort of a sorted formula
20
 *)
21
type sort = int
22
23 e5422169 Thorsten Wißmann
type rational = { nominator: int; denominator: int }
24
25 86b07be8 Thorsten Wißmann
let string_of_rational r =
26
    (string_of_int r.nominator)^"/"^(string_of_int r.denominator)
27
28 e5422169 Thorsten Wißmann
let rational_of_int n d = { nominator = n; denominator = d }
29
30 4fd28192 Thorsten Wißmann
(** Defines (unsorted) coalgebraic formulae.
31
 *)
32
type formula =
33
  | TRUE
34
  | FALSE
35 69a71d22 Thorsten Wißmann
  | AP of string (* atomic proposition *)
36 4fd28192 Thorsten Wißmann
  | 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 f1fa9ad5 Thorsten Wißmann
  | ENFORCES of int list * formula
45
  | ALLOWS   of int list * formula
46 4fd28192 Thorsten Wißmann
  | MIN of int * string * formula
47
  | MAX of int * string * formula
48 af276a36 Thorsten Wißmann
  | MORETHAN of int * string * formula (* diamond of GML *)
49
  | MAXEXCEPT of int * string * formula (* box of GML *)
50 e5422169 Thorsten Wißmann
  | ATLEASTPROB of rational * formula (* = {>= 0.5} C  ---> C occurs with *)
51 c5c25acf Christoph Egger
                                      (*  probability of at least 50% *)
52 9bae2c4f Thorsten Wißmann
  | LESSPROBFAIL of rational * formula (* = [1/2] C = {< 1/2} ¬ C ---> C fails with *)
53
                                        (* probability of less than 50% *)
54 c49eea11 Thorsten Wißmann
  | CONST of string  (* constant functor with value string *)
55
  | CONSTN of string  (* constant functor with value other than string *)
56 19f5dad0 Dirk Pattinson
  | 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 d58bba0f Dirk Pattinson
  | CHC of formula * formula (* Choice is self-dual *)
60 4fd28192 Thorsten Wißmann
  | FUS of bool * formula
61 d29d35f7 Christoph Egger
  | MU of string * formula
62
  | NU of string * formula
63 9a3b23cc Christoph Egger
  | VAR of string
64 b179a57f Christoph Egger
  | 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 e30caa42 Christoph Egger
  | AR of formula * formula
71
  | ER of formula * formula
72 97d73a78 Christoph Egger
  | AB of formula * formula
73
  | EB of formula * formula
74 4fd28192 Thorsten Wißmann
75 ca99d0c6 Thorsten Wißmann
exception ConversionException of formula
76
77
78 4fd28192 Thorsten Wißmann
(** 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 c5c25acf Christoph Egger
  | TRUE
97
  | FALSE
98 4fd28192 Thorsten Wißmann
  | AP _ -> 1
99
  | NOT f1
100
  | AT (_, f1) -> succ (sizeFormula f1)
101 c5c25acf Christoph Egger
  | OR (f1, f2)
102 4fd28192 Thorsten Wißmann
  | AND (f1, f2)
103 c5c25acf Christoph Egger
  | EQU (f1, f2)
104 4fd28192 Thorsten Wißmann
  | IMP (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
105
  | EX (_, f1)
106 f1fa9ad5 Thorsten Wißmann
  | AX (_, f1)
107
  | ENFORCES (_, f1)
108
  | ALLOWS (_, f1) -> succ (sizeFormula f1)
109 4fd28192 Thorsten Wißmann
  | MIN (_, _, f1)
110 af276a36 Thorsten Wißmann
  | MAX (_, _, f1)
111 81435cc4 Thorsten Wißmann
  | ATLEASTPROB (_, f1)
112 9bae2c4f Thorsten Wißmann
  | LESSPROBFAIL (_, f1)
113 af276a36 Thorsten Wißmann
  | MORETHAN (_, _, f1)
114
  | MAXEXCEPT (_, _, f1) -> succ (sizeFormula f1)
115 19f5dad0 Dirk Pattinson
  | ID (f1) -> succ (sizeFormula f1)
116
  | NORM(f1, f2)
117
  | NORMN(f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
118 c49eea11 Thorsten Wißmann
  | CONST _
119
  | CONSTN _ -> 1
120 d58bba0f Dirk Pattinson
  | CHC (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
121 4fd28192 Thorsten Wißmann
  | FUS (_, f1) -> succ (sizeFormula f1)
122 a5f60450 Christoph Egger
  | MU (_, f1)
123
  | NU (_, f1) -> succ (succ (sizeFormula f1))
124
  | VAR _ -> 1
125 8cac0897 Christoph Egger
  | AF _ | EF _
126
  | AG _ | EG _
127 e30caa42 Christoph Egger
  | AU _ | EU _
128 97d73a78 Christoph Egger
  | AR _ | ER _
129
  | AB _ | EB _ ->
130 c5c25acf Christoph Egger
            raise (CoAlgException ("sizeFormula: CTL should have been removed at this point"))
131 4fd28192 Thorsten Wißmann
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 c49eea11 Thorsten Wißmann
(* think of func: (formula -> unit) -> formula -> unit as identity.
140
  iterate over all subformulae and collect side effects. *)
141 dbcce612 Thorsten Wißmann
let rec iter func formula =
142
    func formula;
143
    let proc = iter func in (* proc = "process" *)
144
    match formula with
145 309b71a5 Christoph Egger
    | TRUE | FALSE | AP _ | VAR _ -> ()
146 c49eea11 Thorsten Wißmann
    | CONST _
147
    | CONSTN _ -> ()
148 dbcce612 Thorsten Wißmann
    | 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 9bae2c4f Thorsten Wißmann
    | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
155 dbcce612 Thorsten Wißmann
    | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
156 19f5dad0 Dirk Pattinson
    | ID(a) -> proc a
157
    | NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
158 d58bba0f Dirk Pattinson
    | CHC (a,b)  -> (proc a ; proc b)
159 dbcce612 Thorsten Wißmann
    | FUS (_,a) -> proc a
160 309b71a5 Christoph Egger
    | MU (_, f) | NU (_, f) -> proc f
161 fbffb079 Christoph Egger
    | AF f | EF f | AG f | EG f -> proc f
162 97d73a78 Christoph Egger
    | 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 dbcce612 Thorsten Wißmann
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 e30caa42 Christoph Egger
    (* 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 97d73a78 Christoph Egger
    | 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 e30caa42 Christoph Egger
  in
210 dbcce612 Thorsten Wißmann
  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 ca99d0c6 Thorsten Wißmann
  | ENFORCES _ | ALLOWS _ -> raise (ConversionException formula)
215 dbcce612 Thorsten Wißmann
  | 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 ca99d0c6 Thorsten Wißmann
  | TRUE | FALSE
219
  | EQU _ | IMP _
220
  | AND _ | OR _
221
  | AP _ | NOT _
222 dbcce612 Thorsten Wißmann
  | AX _ | EX _
223 d58bba0f Dirk Pattinson
  | CHC _ | FUS _ -> formula
224 ca99d0c6 Thorsten Wißmann
  | _ -> raise (ConversionException formula)
225 dbcce612 Thorsten Wißmann
  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 ca99d0c6 Thorsten Wißmann
  | ENFORCES _ | ALLOWS _ -> raise (ConversionException formula)
231 dbcce612 Thorsten Wißmann
  | MORETHAN _ | MIN _ | MAX _ | MAXEXCEPT _ -> formula
232 ca99d0c6 Thorsten Wißmann
  | TRUE | FALSE
233
  | EQU _ | IMP _
234
  | AND _ | OR _
235
  | AP _ | NOT _
236 d58bba0f Dirk Pattinson
  | CHC _ | FUS _ -> formula
237 dbcce612 Thorsten Wißmann
  | AX (r,a) -> MAXEXCEPT (0,r,a)
238
  | EX (r,a) -> MORETHAN  (0,r,a)
239 ca99d0c6 Thorsten Wißmann
  | _ -> raise (ConversionException formula)
240 dbcce612 Thorsten Wißmann
  in
241
  convert_post helper formula
242
243 17af2794 Christoph Egger
let gensym = Stream.from (fun i -> Some (Printf.sprintf "#gensym%x#" i))
244
245 c5105465 Christoph Egger
let convertToMu formula =
246 17af2794 Christoph Egger
  let helper formula =
247 c5c25acf Christoph Egger
    match formula with
248
    | AF f1 ->
249 dcc8167f Christoph Egger
       MU ("#AF#", (OR (f1, (AX ("", (VAR "#AF#"))))))
250 c5c25acf Christoph Egger
    | EF f1 ->
251 dcc8167f Christoph Egger
       MU ("#EF#", (OR (f1, (EX ("", (VAR "#EF#"))))))
252 c5c25acf Christoph Egger
    | AG f1 ->
253 dcc8167f Christoph Egger
       NU ("#AG#", (AND (f1, (AX ("", (VAR "#AG#"))))))
254 c5c25acf Christoph Egger
    | EG f1 ->
255 dcc8167f Christoph Egger
       NU ("#EG#", (AND (f1, (EX ("", (VAR "#EG#"))))))
256 c5c25acf Christoph Egger
    | AU (f1, f2) ->
257 dcc8167f Christoph Egger
       MU ("#AU#", (OR (f2, (AND (f1, (AX ("", (VAR "#AU#"))))))))
258 c5c25acf Christoph Egger
    | EU (f1, f2) ->
259 dcc8167f Christoph Egger
       MU ("#EU#", (OR (f2, (AND (f1, (EX ("", (VAR "#EU#"))))))))
260 e30caa42 Christoph Egger
    | AR (f1, f2) ->
261
       NU ("#AR#", (AND (f2, (OR (f1, (AX ("", (VAR "#AR#"))))))))
262
    | ER (f1, f2) ->
263
       NU ("#ER#", (AND (f2, (OR (f1, (EX ("", (VAR "#ER#"))))))))
264 97d73a78 Christoph Egger
    | AB (f1, f2) ->
265 435390a8 Christoph Egger
       NOT (MU ("#AB#", (OR (f2, (AND ((NOT f1), (EX ("", (VAR "#AB#")))))))))
266 97d73a78 Christoph Egger
    | EB (f1, f2) ->
267 435390a8 Christoph Egger
       NOT (MU ("#EB#", (OR (f2, (AND ((NOT f1), (AX ("", (VAR "#EB#")))))))))
268 c5c25acf Christoph Egger
    | _ -> formula
269 c5105465 Christoph Egger
  in
270
  convert_post helper formula
271
272 4fd28192 Thorsten Wißmann
(** Appends a string representation of a formula to a string buffer.
273
    Parentheses are ommited where possible
274
    where the preference rules are defined as usual.
275
    @param sb A string buffer.
276
    @param f A formula.
277
 *)
278
let rec exportFormula_buffer sb f =
279
  let negate = function
280
    | NOT f -> f
281
    | f -> NOT f
282
  in
283
  let prio n lf =
284
    let prionr = function
285
      | EQU _ -> 0
286 c5c25acf Christoph Egger
      | IMP _  -> 1
287 4fd28192 Thorsten Wißmann
      | OR _ -> 2
288
      | AND _ -> 3
289
      | _ -> 4
290
    in
291
    if prionr lf < n then begin
292
      Buffer.add_char sb '(';
293
      exportFormula_buffer sb lf;
294
      Buffer.add_char sb ')'
295
    end
296
    else exportFormula_buffer sb lf
297
  in
298
  match f with
299
  | TRUE -> Buffer.add_string sb "True"
300
  | FALSE -> Buffer.add_string sb "False"
301
  | AP s -> Buffer.add_string sb s
302
  | NOT f1 ->
303
      Buffer.add_string sb "~";
304
      prio 4 f1
305
  | AT (s, f1) ->
306
      Buffer.add_string sb "@ ";
307
      Buffer.add_string sb s;
308
      Buffer.add_string sb " ";
309
      prio 4 f1
310
  | OR (f1, f2) ->
311
      prio 2 f1;
312
      Buffer.add_string sb " | ";
313
      prio 2 f2
314
  | AND (f1, f2) ->
315
      prio 3 f1;
316
      Buffer.add_string sb " & ";
317
      prio 3 f2
318
  | EQU (f1, f2) ->
319
      prio 0 f1;
320
      Buffer.add_string sb " <=> ";
321
      prio 0 f2
322
  | IMP (f1, f2) ->
323
      prio 2 f1;
324
      Buffer.add_string sb " => ";
325
      prio 2 f2
326
  | EX (s, f1) ->
327
      Buffer.add_string sb "<";
328
      Buffer.add_string sb s;
329
      Buffer.add_string sb ">";
330
      prio 4 f1
331
  | AX (s, f1) ->
332
      Buffer.add_string sb "[";
333
      Buffer.add_string sb s;
334
      Buffer.add_string sb "]";
335
      prio 4 f1
336 f1fa9ad5 Thorsten Wißmann
  | ALLOWS (s, f1) ->
337
      Buffer.add_string sb "<{";
338 c16fd631 Thorsten Wißmann
      Buffer.add_string sb (
339
          match s with
340
          | [] -> " "
341
          | _ ->(Str.concat " " (L.map string_of_int s))
342
      );
343 f1fa9ad5 Thorsten Wißmann
      Buffer.add_string sb "}>";
344
      prio 4 f1
345
  | ENFORCES (s, f1) ->
346
      Buffer.add_string sb "[{";
347 c16fd631 Thorsten Wißmann
      Buffer.add_string sb (
348
          match s with
349
          | [] -> " "
350
          | _ ->(Str.concat " " (L.map string_of_int s))
351
      );
352 f1fa9ad5 Thorsten Wißmann
      Buffer.add_string sb "}]";
353
      prio 4 f1
354 86b07be8 Thorsten Wißmann
  | ATLEASTPROB (p, f1) ->
355
      Buffer.add_string sb "{>=";
356
      Buffer.add_string sb (string_of_rational p);
357
      Buffer.add_string sb "}";
358
      prio 4 f1
359 9bae2c4f Thorsten Wißmann
  | LESSPROBFAIL (p, f1) ->
360 c855ba91 Thorsten Wißmann
      Buffer.add_string sb "{<";
361 86b07be8 Thorsten Wißmann
      Buffer.add_string sb (string_of_rational p);
362 9bae2c4f Thorsten Wißmann
      Buffer.add_string sb "} ~ ";
363 86b07be8 Thorsten Wißmann
      prio 4 f1
364 4fd28192 Thorsten Wißmann
  | MIN (n, s, f1) ->
365
      Buffer.add_string sb "{>=";
366
      Buffer.add_string sb (string_of_int n);
367
      Buffer.add_string sb " ";
368
      Buffer.add_string sb s;
369
      Buffer.add_string sb "}";
370
      prio 4 f1
371
  | MAX (n, s, f1) ->
372
      Buffer.add_string sb "{<=";
373
      Buffer.add_string sb (string_of_int n);
374
      Buffer.add_string sb " ";
375
      Buffer.add_string sb s;
376
      Buffer.add_string sb "}";
377
      prio 4 f1
378 af276a36 Thorsten Wißmann
  | MORETHAN (n, s, f1) ->
379
      Buffer.add_string sb "{>";
380
      Buffer.add_string sb (string_of_int n);
381
      Buffer.add_string sb " ";
382
      Buffer.add_string sb s;
383
      Buffer.add_string sb "}";
384
      prio 4 f1
385
  | MAXEXCEPT (n, s, f1) ->
386
      Buffer.add_string sb "{<=";
387
      Buffer.add_string sb (string_of_int n);
388
      Buffer.add_string sb " ~ ";
389
      Buffer.add_string sb s;
390
      Buffer.add_string sb "}";
391
      prio 4 f1 (* actually is prio of ~ and not of <= *)
392 19f5dad0 Dirk Pattinson
  | ID (f1) ->
393
      Buffer.add_string sb "O";
394
      prio 4 f1
395
  | NORM(f1, f2) ->
396
      Buffer.add_string sb "(";
397
      exportFormula_buffer sb f1;
398
      Buffer.add_string sb " =o ";
399
      exportFormula_buffer sb f2;
400
      Buffer.add_string sb ")"
401
  | NORMN(f1, f2) ->
402
      Buffer.add_string sb "~(";
403
      exportFormula_buffer sb (negate f1);
404
      Buffer.add_string sb " =o ";
405
      exportFormula_buffer sb (negate f2);
406
      Buffer.add_string sb ")"
407 4fd28192 Thorsten Wißmann
  | CHC (f1, f2) ->
408
      Buffer.add_string sb "(";
409
      exportFormula_buffer sb f1;
410
      Buffer.add_string sb " + ";
411
      exportFormula_buffer sb f2;
412
      Buffer.add_string sb ")"
413 c49eea11 Thorsten Wißmann
  | CONST s -> Buffer.add_string sb "=";
414
      Buffer.add_string sb s
415
  | CONSTN s -> Buffer.add_string sb "~=";
416
      Buffer.add_string sb s
417 4fd28192 Thorsten Wißmann
  | FUS (first, f1) ->
418
      Buffer.add_string sb (if first then "[pi1]" else "[pi2]");
419
      prio 4 f1
420 8334c748 Christoph Egger
  | MU (s, f1) ->
421
      Buffer.add_string sb "μ";
422 d29d35f7 Christoph Egger
      Buffer.add_string sb s;
423 8334c748 Christoph Egger
      Buffer.add_string sb ".";
424
      prio 4 f1
425
  | NU (s, f1) ->
426
      Buffer.add_string sb "ν";
427 c5c25acf Christoph Egger
      Buffer.add_string sb s;
428 8334c748 Christoph Egger
      Buffer.add_string sb ".";
429
      prio 4 f1
430
  | VAR s ->
431
     Buffer.add_string sb s
432 0aa34675 Christoph Egger
  | AF f1 ->
433 c5c25acf Christoph Egger
     Buffer.add_string sb "AF ";
434
     prio 4 f1
435 0aa34675 Christoph Egger
  | EF f1 ->
436 c5c25acf Christoph Egger
     Buffer.add_string sb "EF ";
437
     prio 4 f1
438 0aa34675 Christoph Egger
  | AG f1 ->
439 c5c25acf Christoph Egger
     Buffer.add_string sb "AG ";
440
     prio 4 f1
441 0aa34675 Christoph Egger
  | EG f1 ->
442 c5c25acf Christoph Egger
     Buffer.add_string sb "EG ";
443
     prio 4 f1
444 0aa34675 Christoph Egger
  | AU (f1, f2) ->
445 c5c25acf Christoph Egger
     Buffer.add_string sb "A (";
446
     prio 4 f1;
447
     Buffer.add_string sb " U ";
448
     prio 4 f2;
449
     Buffer.add_string sb ")"
450 0aa34675 Christoph Egger
  | EU (f1, f2) ->
451 c5c25acf Christoph Egger
     Buffer.add_string sb "E (";
452
     prio 4 f1;
453
     Buffer.add_string sb " U ";
454
     prio 4 f2;
455
     Buffer.add_string sb ")"
456 e30caa42 Christoph Egger
  | AR (f1, f2) ->
457
     Buffer.add_string sb "A (";
458
     prio 4 f1;
459
     Buffer.add_string sb " R ";
460
     prio 4 f2;
461
     Buffer.add_string sb ")"
462
  | ER (f1, f2) ->
463
     Buffer.add_string sb "E (";
464
     prio 4 f1;
465
     Buffer.add_string sb " R ";
466
     prio 4 f2;
467
     Buffer.add_string sb ")"
468 97d73a78 Christoph Egger
  | AB (f1, f2) ->
469
     Buffer.add_string sb "A (";
470
     prio 4 f1;
471
     Buffer.add_string sb " B ";
472
     prio 4 f2;
473
     Buffer.add_string sb ")"
474
  | EB (f1, f2) ->
475
     Buffer.add_string sb "E (";
476
     prio 4 f1;
477
     Buffer.add_string sb " B ";
478
     prio 4 f2;
479
     Buffer.add_string sb ")"
480 e30caa42 Christoph Egger
481 4fd28192 Thorsten Wißmann
482
(** Converts a formula into a string representation.
483
    Parentheses are ommited where possible
484
    where the preference rules are defined as usual.
485
    @param f A formula.
486
    @return A string representing f.
487
 *)
488
let exportFormula f =
489
  let sb = Buffer.create 128 in
490
  exportFormula_buffer sb f;
491
  Buffer.contents sb
492
493 ca99d0c6 Thorsten Wißmann
let string_of_formula = exportFormula
494
495 01b1ab69 Thorsten Wißmann
(** export (CL)-formula suitable for tatl-inputs *)
496
let rec exportTatlFormula_buffer sb f =
497
  let prio n lf =
498
    let prionr = function
499
      | EQU _ -> 0
500 c5c25acf Christoph Egger
      | IMP _  -> 1
501 01b1ab69 Thorsten Wißmann
      | OR _ -> 2
502
      | AND _ -> 3
503
      | _ -> 4
504
    in
505
    if prionr lf < n then begin
506
      Buffer.add_char sb '(';
507 064f3099 Thorsten Wißmann
      exportTatlFormula_buffer sb lf;
508 01b1ab69 Thorsten Wißmann
      Buffer.add_char sb ')'
509
    end
510 064f3099 Thorsten Wißmann
    else exportTatlFormula_buffer sb lf
511 01b1ab69 Thorsten Wißmann
  in
512
  match f with
513
  | TRUE -> Buffer.add_string sb "(p \\/ ~p)"
514
  | FALSE -> Buffer.add_string sb "(p /\\ ~p)"
515
  | AP s -> Buffer.add_string sb s
516
  | NOT f1 ->
517
      Buffer.add_string sb "~";
518
      prio 4 f1
519
  | OR (f1, f2) ->
520
      prio 2 f1;
521
      Buffer.add_string sb " \\/ ";
522
      prio 2 f2
523
  | AND (f1, f2) ->
524
      prio 3 f1;
525
      Buffer.add_string sb " /\\ ";
526
      prio 3 f2
527
  | EQU (f1, f2) ->
528
      prio 0 (AND (IMP (f1,f2), IMP (f2,f1)))
529
  | IMP (f1, f2) ->
530
      prio 2 f1;
531
      Buffer.add_string sb " -> ";
532
      prio 2 f2
533
  | ALLOWS (s, f1) ->
534
      Buffer.add_string sb "<<";
535
      Buffer.add_string sb (
536
          match s with
537
          | [] -> " "
538
          | _ ->(Str.concat "," (L.map string_of_int s))
539
      );
540
      Buffer.add_string sb ">>X ";
541
      prio 4 f1
542
  | ENFORCES (s, f1) ->
543
      Buffer.add_string sb "~<<";
544
      Buffer.add_string sb (
545
          match s with
546
          | [] -> " "
547
          | _ ->(Str.concat "," (L.map string_of_int s))
548
      );
549
      Buffer.add_string sb ">>X ~ ";
550
      prio 4 f1
551
  | EX _
552
  | AX _
553
  | MIN _
554
  | MAX _
555
  | MORETHAN _
556
  | MAXEXCEPT _
557
  | AT _
558 c49eea11 Thorsten Wißmann
  | CONST _
559
  | CONSTN _
560 01b1ab69 Thorsten Wißmann
  | CHC _
561 86b07be8 Thorsten Wißmann
  | ATLEASTPROB _
562 9bae2c4f Thorsten Wißmann
  | LESSPROBFAIL _
563 19f5dad0 Dirk Pattinson
  | ID _
564
  | NORM _
565
  | NORMN _
566 8cac0897 Christoph Egger
  | FUS _
567
  | MU _
568
  | NU _
569
  | VAR _
570
  | AF _
571
  | EF _
572
  | AG _
573
  | EG _
574
  | AU _
575 e30caa42 Christoph Egger
  | EU _
576
  | AR _
577 97d73a78 Christoph Egger
  | ER _
578
  | AB _
579
  | EB _ -> raise (CoAlgException ("export to tatl: Not connectives of CL"))
580 01b1ab69 Thorsten Wißmann
581
let exportTatlFormula f =
582
  let sb = Buffer.create 128 in
583
  exportTatlFormula_buffer sb f;
584
  Buffer.contents sb
585
586 4fd28192 Thorsten Wißmann
(** Appends a string representation of a sorted formula to a string buffer.
587
    Parentheses are ommited where possible
588
    where the preference rules are defined as usual.
589
    @param sb A string buffer.
590
    @param (s, f) A sorted formula.
591
 *)
592
let rec exportSortedFormula_buffer sb (s, f) =
593
  Buffer.add_string sb (string_of_int s);
594
  Buffer.add_string sb ": ";
595
  exportFormula_buffer sb f
596
597
(** Converts a sorted formula into a string representation.
598
    Parentheses are ommited where possible
599
    where the preference rules are defined as usual.
600
    @param f A sorted formula.
601
    @return A string representing f.
602
 *)
603
let exportSortedFormula f =
604
  let sb = Buffer.create 128 in
605
  exportSortedFormula_buffer sb f;
606
  Buffer.contents sb
607
608
(** Converts a (sorted) formula query into a string representation.
609
    @param tbox A list of sorted formulae representing a TBox.
610
    @param f A sorted formula.
611
    @return A string representing tbox |- f.
612
 *)
613
let exportQuery tbox f =
614
  let sb = Buffer.create 1000 in
615
  let rec expFl = function
616
    | [] -> ()
617
    | h::tl ->
618
        exportSortedFormula_buffer sb h;
619
        if tl <> [] then Buffer.add_string sb "; " else ();
620
        expFl tl
621
  in
622
  expFl tbox;
623
  Buffer.add_string sb "  |-  ";
624
  exportSortedFormula_buffer sb f;
625
  Buffer.contents sb
626
627 b59059c4 Thorsten Wißmann
(** Converts a (sorted) formula query into a string representation. Such that
628
    coalg can read it again using importQuery
629
    @param tbox A list of sorted formulae representing a TBox.
630
    @param f A sorted formula.
631
    @return A string representing tbox |- f.
632
 *)
633
let exportQueryParsable tbox (_,f) =
634
  let sb = Buffer.create 1000 in
635
  let rec expFl = function
636
    | [] -> ()
637
    | (_,h)::tl ->
638
        exportFormula_buffer sb h;
639
        if tl <> [] then Buffer.add_string sb "; " else ();
640
        expFl tl
641
  in
642
  expFl tbox;
643
  Buffer.add_string sb "  |-  ";
644
  exportFormula_buffer sb f;
645
  Buffer.contents sb
646
647 4fd28192 Thorsten Wißmann
648 19f5dad0 Dirk Pattinson
(* NB: True and False are the propositional constants. Lower case
649
   true/false are regardes as atomic propositions and we emit a warning
650
*)
651 c5c25acf Christoph Egger
let lexer = A.make_lexer
652 19f5dad0 Dirk Pattinson
    [":";";";"|-";"(";")";"=>";"<=>";"|";"&";"~";"@";"True";"False";"true";"false";"<";">";"[";"]";"{<=";"{>=";"}";"+";"[pi1]";"[pi2]"
653 b2f18312 Christoph Egger
     ;"[{";"}]";"<{";"}>";",";"/";"{<";"=";"=o";"O"
654
     ;"μ";"ν";"."
655 e30caa42 Christoph Egger
     ;"AX";"EX";"AF";"EF";"AG";"EG";"A";"E";"U";"R";"B"
656 c5c25acf Christoph Egger
    ]
657 4fd28192 Thorsten Wißmann
658
let mk_exn s = CoAlgException s
659
660 63710593 Christoph Egger
(** Process from inside out. cons all variables seen, remove them when
661
    binding fixpoint is found. Fixpoint type may only change if last
662
    (inner) fixpoint didn't include any free variables.
663
 *)
664
let rec verifyMuAltFree formula =
665
  let proc = verifyMuAltFree in
666
  match formula with
667
  | TRUE | FALSE | AP _ -> ("none", [])
668
  | CONST _
669
  | CONSTN _ -> ("none", [])
670
  | AT (_,a) | NOT a
671
  | EX (_,a) | AX (_,a) -> proc a
672
  | OR (a,b) | AND (a,b)
673
  | EQU (a,b) | IMP (a,b) ->
674 c5c25acf Christoph Egger
     let (atype, afree) = proc a
675
     and (btype, bfree) = proc b in
676
     if (compare atype "μ" == 0 && compare btype "ν" == 0) ||
677
          (compare atype "ν" == 0 && compare btype "μ" == 0) then
678
       raise (CoAlgException ("formula not alternation-free"));
679
     if compare atype "none" == 0 then
680
       (btype, List.flatten [afree; bfree])
681
     else
682
       (atype, List.flatten [afree; bfree])
683 63710593 Christoph Egger
  | ENFORCES (_,a) | ALLOWS   (_,a)
684
  | MIN (_,_,a)    | MAX (_,_,a)
685
  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
686
  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
687
  | ID(a) -> proc a
688
  | NORM(a, b) | NORMN(a, b)
689
  | CHC (a,b)  ->
690 c5c25acf Christoph Egger
     let (atype, afree) = proc a
691
     and (btype, bfree) = proc b in
692
     if (compare atype "μ" == 0 && compare btype "ν" == 0) ||
693
          (compare atype "ν" == 0 && compare btype "μ" == 0) then
694
       raise (CoAlgException ("formula not alternation-free"));
695
     if compare atype "none" == 0 then
696
       (btype, List.flatten [afree; bfree])
697
     else
698
       (atype, List.flatten [afree; bfree])
699 63710593 Christoph Egger
  | FUS (_,a) -> proc a
700
  | MU (s, f) ->
701 c5c25acf Christoph Egger
     let (fptype, free) = proc f in
702
     (if (compare fptype "ν" == 0) then
703
        raise (CoAlgException ("formula not alternation-free")));
704
     let predicate x = compare x s != 0 in
705 63710593 Christoph Egger
     let newfree = List.filter predicate free in
706 c5c25acf Christoph Egger
     if newfree = [] then
707
       ("none", [])
708
     else
709
       ("μ", newfree)
710 63710593 Christoph Egger
  | NU (s, f) ->
711 c5c25acf Christoph Egger
     let (fptype, free) = proc f in
712
     (if (compare fptype "μ" == 0) then
713
        raise (CoAlgException ("formula not alternation-free")));
714
     let predicate x = compare x s != 0 in
715 63710593 Christoph Egger
     let newfree = List.filter predicate free in
716 c5c25acf Christoph Egger
     if newfree = [] then
717
       ("none", [])
718
     else
719
       ("ν", newfree)
720 63710593 Christoph Egger
  | VAR s -> ("none", [s])
721 97d73a78 Christoph Egger
  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ ->
722 c5c25acf Christoph Egger
     raise (CoAlgException ("verifyMuAltFree: CTL should have been removed at this point"))
723 939f5bab Christoph Egger
724 63710593 Christoph Egger
725
(** Process from outside in. For every variable bound keep the tuple
726
    (name, negations). For every negation crossed map a +1 over snd on
727
    that list. For every variable met check that the matching
728
    negations is even.
729
 *)
730
let rec verifyMuMonotone negations formula =
731
  let proc = verifyMuMonotone negations in
732
  match formula with
733
  | TRUE | FALSE | AP _ -> ()
734
  | CONST _
735
  | CONSTN _ -> ()
736
  | AT (_,a)
737
  | EX (_,a) | AX (_,a) -> proc a
738
  | OR (a,b) | AND (a,b)
739
  | EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
740
  | ENFORCES (_,a) | ALLOWS   (_,a)
741
  | MIN (_,_,a)    | MAX (_,_,a)
742
  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
743
  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
744
  | ID(a) -> proc a
745
  | NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
746
  | CHC (a,b)  -> (proc a ; proc b)
747
  | FUS (_,a) -> proc a
748
  | MU (s, f)
749
  | NU (s, f) ->
750 c5c25acf Christoph Egger
     let newNeg = (s, 0) :: negations in
751
     verifyMuMonotone newNeg f
752 63710593 Christoph Egger
  | VAR s ->
753 c5c25acf Christoph Egger
     let finder (x, _) = compare x s == 0 in
754
     let (_, neg) = List.find finder negations in
755
     if ((neg land 1) != 0) then raise (CoAlgException ("formula not monotone"))
756 63710593 Christoph Egger
  | NOT a ->
757 c5c25acf Christoph Egger
     let increment (s, n) = (s, n+1) in
758
     let newNeg = List.map increment negations in
759
     verifyMuMonotone newNeg a
760 97d73a78 Christoph Egger
  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ ->
761 c5c25acf Christoph Egger
     raise (CoAlgException ("verifyMuMonotone: CTL should have been removed at this point"))
762 63710593 Christoph Egger
763 26cfb2dc Christoph Egger
let rec verifyMuGuarded unguarded formula =
764
  let proc = verifyMuGuarded unguarded in
765
  match formula with
766
  | TRUE | FALSE | AP _ -> ()
767
  | CONST _
768
  | CONSTN _ -> ()
769
  | AT (_,a) | NOT a -> proc a
770
  | EX (_,a) | AX (_,a) -> verifyMuGuarded [] a
771
  | OR (a,b) | AND (a,b)
772
  | EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
773
  | ENFORCES (_,a) | ALLOWS   (_,a)
774
  | MIN (_,_,a)    | MAX (_,_,a)
775
  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
776
  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
777
  | ID(a) -> proc a
778
  | NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
779
  | CHC (a,b)  -> (proc a ; proc b)
780
  | FUS (_,a) -> proc a
781
  | MU (s, f)
782
  | NU (s, f) ->
783 c5c25acf Christoph Egger
     let newUnguard = s :: unguarded in
784
     verifyMuGuarded newUnguard f
785 26cfb2dc Christoph Egger
  | VAR s ->
786 c5c25acf Christoph Egger
     let finder x = compare x s == 0 in
787
     if List.exists finder unguarded then
788
       raise (CoAlgException ("formula not guarded"))
789 97d73a78 Christoph Egger
  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ ->
790 c5c25acf Christoph Egger
     raise (CoAlgException ("verifyMuGuarded: CTL should have been removed at this point"))
791 63710593 Christoph Egger
792
let verifyFormula formula =
793
  verifyMuAltFree formula;
794
  verifyMuMonotone [] formula;
795 26cfb2dc Christoph Egger
  verifyMuGuarded [] formula
796 63710593 Christoph Egger
797 4fd28192 Thorsten Wißmann
(** These functions parse a token stream to obtain a formula.
798
    It is a standard recursive descent procedure.
799
    @param ts A token stream.
800
    @return The resulting (sub-)formula.
801
    @raise CoAlgException if ts does not represent a formula.
802
 *)
803 0b908205 Christoph Egger
let rec parse_formula (symtab: 'a list) ts =
804 1484d8cb Christoph Egger
  let formula = (parse_imp symtab ts) in
805
  let f1 = convertToMu formula in
806 4fd28192 Thorsten Wißmann
  match Stream.peek ts with
807
  | None -> f1
808
  | Some (A.Kwd "<=>") ->
809
      Stream.junk ts;
810 0b908205 Christoph Egger
      let f2 = parse_formula symtab ts in
811 4fd28192 Thorsten Wißmann
      EQU (f1, f2)
812
  | _ -> f1
813
814
(** These functions parse a token stream to obtain a formula.
815
    It is a standard recursive descent procedure.
816
    @param ts A token stream.
817
    @return The resulting (sub-)formula.
818
    @raise CoAlgException if ts does not represent a formula.
819
 *)
820 0b908205 Christoph Egger
and parse_imp symtab ts=
821
  let f1 = parse_or symtab ts in
822 4fd28192 Thorsten Wißmann
  match Stream.peek ts with
823
  | None -> f1
824
  | Some (A.Kwd "=>") ->
825
      Stream.junk ts;
826 0b908205 Christoph Egger
      let f2 = parse_imp symtab ts in
827 4fd28192 Thorsten Wißmann
      IMP (f1, f2)
828
  | _ -> f1
829
830
(** These functions parse a token stream to obtain a formula.
831
    It is a standard recursive descent procedure.
832
    @param ts A token stream.
833
    @return The resulting (sub-)formula.
834
    @raise CoAlgException if ts does not represent a formula.
835
 *)
836 0b908205 Christoph Egger
and parse_or symtab ts =
837
  let f1 = parse_and symtab ts in
838 4fd28192 Thorsten Wißmann
  match Stream.peek ts with
839
  | None -> f1
840
  | Some (A.Kwd "|") ->
841
      Stream.junk ts;
842 0b908205 Christoph Egger
      let f2 = parse_or symtab ts in
843 4fd28192 Thorsten Wißmann
      OR (f1, f2)
844
  | _ -> f1
845
846
(** These functions parse a token stream to obtain a formula.
847
    It is a standard recursive descent procedure.
848
    @param ts A token stream.
849
    @return The resulting (sub-)formula.
850
    @raise CoAlgException if ts does not represent a formula.
851
 *)
852 0b908205 Christoph Egger
and parse_and symtab ts =
853
  let f1 = parse_cimp symtab ts in
854 4fd28192 Thorsten Wißmann
  match Stream.peek ts with
855
  | None -> f1
856
  | Some (A.Kwd "&") ->
857
      Stream.junk ts;
858 0b908205 Christoph Egger
      let f2 = parse_and symtab ts in
859 4fd28192 Thorsten Wißmann
      AND (f1, f2)
860
  | _ -> f1
861
862
(** These functions parse a token stream to obtain a formula.
863
    It is a standard recursive descent procedure.
864
    @param ts A token stream.
865
    @return The resulting (sub-)formula.
866
    @raise CoAlgException if ts does not represent a formula.
867
 *)
868 0b908205 Christoph Egger
and parse_cimp symtab ts =
869
  let f1 = parse_rest symtab ts in
870 19f5dad0 Dirk Pattinson
  match Stream.peek ts with
871
  | None -> f1
872
  | Some (A.Kwd "=o") ->
873
      Stream.junk ts;
874 0b908205 Christoph Egger
      let f2 = parse_cimp symtab ts in
875 19f5dad0 Dirk Pattinson
      NORM (f1, f2)
876
  | _ -> f1
877
878
(** These functions parse a token stream to obtain a formula.
879
    It is a standard recursive descent procedure.
880
    @param ts A token stream.
881
    @return The resulting (sub-)formula.
882
    @raise CoAlgException if ts does not represent a formula.
883
 *)
884 0b908205 Christoph Egger
and parse_rest symtab ts =
885 4fd28192 Thorsten Wißmann
  let boxinternals noNo es =
886
    let n =
887
      if noNo then 0
888
      else
889
        match Stream.next ts with
890
        | A.Int n when n >= 0 -> n
891
        | t -> A.printError mk_exn ~t ~ts "<non-negative number> expected: "
892
    in
893 e5422169 Thorsten Wißmann
    let (s,denominator) =
894 4fd28192 Thorsten Wißmann
      match Stream.peek ts with
895 e5422169 Thorsten Wißmann
      | Some (A.Ident s1) -> Stream.junk ts; (s1,0)
896
      | Some (A.Kwd c) when c = es -> ("", 0)
897
      | Some (A.Kwd "/") -> begin
898
            Stream.junk ts;
899
            match Stream.next ts with
900
            | A.Int denom when denom > 0 -> ("", denom)
901
            | t -> A.printError mk_exn ~t ~ts "<positive number> (the denominator) expected: "
902
        end
903 4fd28192 Thorsten Wißmann
      | _ -> A.printError mk_exn ~ts ("role name or \"" ^ es ^ "\" expected: ")
904
    in
905 eda515b6 Thorsten Wißmann
    if (denominator < n) then begin
906
       let explanation =
907
        ("nominator="^(string_of_int n)^" but denominator="^(string_of_int denominator))
908
       in
909
       A.printError mk_exn ~ts ("Nominator must not be larger than the denominator "
910
                               ^"("^explanation^") at: "
911
                               )
912 e5422169 Thorsten Wißmann
    end;
913 4fd28192 Thorsten Wißmann
    let _ =
914
      match Stream.next ts with
915
      | A.Kwd c when c = es -> ()
916
      | t -> A.printError mk_exn ~t ~ts ("\"" ^ es ^ "\" expected: ")
917
    in
918 e5422169 Thorsten Wißmann
    (n, denominator, s)
919 4fd28192 Thorsten Wißmann
  in
920 f1fa9ad5 Thorsten Wißmann
  let rec agentlist es =
921 e2dc68f7 Thorsten Wißmann
    let allAgents = CoolUtils.cl_get_agents () in
922 f1fa9ad5 Thorsten Wißmann
    match Stream.next ts with
923 e2dc68f7 Thorsten Wißmann
    | A.Int n -> if CoolUtils.TArray.elem n allAgents
924
                 then n::(agentlist es)
925
                 else A.printError mk_exn ~ts ("agent name \"" ^ (string_of_int n) ^ "\" unknonwn, see --agents: ")
926 f1fa9ad5 Thorsten Wißmann
    | A.Kwd c when c = es -> []
927
    | _ -> A.printError mk_exn ~ts ("agent name or " ^ es ^ "\" expected: ")
928
  in
929 4fd28192 Thorsten Wißmann
  match Stream.next ts with
930 19f5dad0 Dirk Pattinson
  | A.Kwd "true" ->
931
    print_endline "*** Warning: \"true\" used as propositional variable.";
932
    AP "true"
933
  | A.Kwd "false" ->
934
    print_endline "*** Warning: \"false\" used as propositional variable.";
935
    AP "false"
936 4fd28192 Thorsten Wißmann
  | A.Kwd "True" -> TRUE
937
  | A.Kwd "False" -> FALSE
938 c3e13ca6 Christoph Egger
  | A.Ident s ->
939 c5c25acf Christoph Egger
      (try
940
          let finder (x, _) = compare x s == 0 in
941
          let (_, symbol) = List.find finder symtab in
942
          VAR symbol
943
        with Not_found -> AP s)
944 4fd28192 Thorsten Wißmann
  | A.Kwd "~" ->
945 0b908205 Christoph Egger
      let f = parse_rest symtab ts in
946 4fd28192 Thorsten Wißmann
      NOT f
947
  | A.Kwd "@" ->
948
      let s =
949
        match Stream.next ts with
950
        | A.Ident s when isNominal s -> s
951
        | t -> A.printError mk_exn ~t ~ts ("nominal expected: ")
952
      in
953 0b908205 Christoph Egger
      let f = parse_rest symtab ts in
954 4fd28192 Thorsten Wißmann
      AT (s, f)
955 c5c25acf Christoph Egger
  | A.Kwd "<" ->
956 e5422169 Thorsten Wißmann
      let (_, _, s) = boxinternals true ">" in
957 0b908205 Christoph Egger
      let f1 = parse_rest symtab ts in
958 c5c25acf Christoph Egger
      EX (s, f1)
959
  | A.Kwd "[" ->
960 e5422169 Thorsten Wißmann
      let (_, _, s) = boxinternals true "]" in
961 0b908205 Christoph Egger
      let f1 = parse_rest symtab ts in
962 4fd28192 Thorsten Wißmann
      AX (s, f1)
963 c5c25acf Christoph Egger
  | A.Kwd "[{" ->
964 7aa620ce Thorsten Wißmann
      let ls = agentlist "}]" in
965 0b908205 Christoph Egger
      let f1 = parse_rest symtab ts in
966 7aa620ce Thorsten Wißmann
      ENFORCES (ls, f1)
967 c5c25acf Christoph Egger
  | A.Kwd "<{" ->
968 7aa620ce Thorsten Wißmann
      let ls = agentlist "}>" in
969 0b908205 Christoph Egger
      let f1 = parse_rest symtab ts in
970 7aa620ce Thorsten Wißmann
      ALLOWS (ls, f1)
971 c5c25acf Christoph Egger
  | A.Kwd "{>=" ->
972 e5422169 Thorsten Wißmann
      let (n, denom, s) = boxinternals false "}" in
973 0b908205 Christoph Egger
      let f1 = parse_rest symtab ts in
974 e5422169 Thorsten Wißmann
      if (denom <> 0)
975
      then ATLEASTPROB (rational_of_int n denom, f1)
976
      else MIN (n, s, f1)
977 c5c25acf Christoph Egger
  | A.Kwd "{<=" ->
978 e5422169 Thorsten Wißmann
      let (n, denom, s) = boxinternals false "}" in
979 0b908205 Christoph Egger
      let f1 = parse_rest symtab ts in
980 e5422169 Thorsten Wißmann
      if (denom <> 0)
981 c855ba91 Thorsten Wißmann
      then A.printError mk_exn ~ts "Can not express {<= probability}"
982 e5422169 Thorsten Wißmann
      else MAX (n, s, f1)
983 c5c25acf Christoph Egger
  | A.Kwd "{<" ->
984 c855ba91 Thorsten Wißmann
      let (n, denom, s) = boxinternals false "}" in
985 0b908205 Christoph Egger
      let f1 = parse_rest symtab ts in
986 c855ba91 Thorsten Wißmann
      if (denom <> 0)
987 9bae2c4f Thorsten Wißmann
      then LESSPROBFAIL (rational_of_int n denom, NOT f1)
988 c855ba91 Thorsten Wißmann
      else A.printError mk_exn ~ts "The \"Less than\" < is not implemented yet"
989 c49eea11 Thorsten Wißmann
  | A.Kwd "=" -> begin
990
          match Stream.next ts with
991
          (* | A.Int s *)
992
          | A.Kwd s
993
          | A.Ident s -> CONST s
994
          | _ -> A.printError mk_exn ~ts "constant = expects an identifier afterwards"
995
    end
996 4fd28192 Thorsten Wißmann
  | A.Kwd "(" -> begin
997 0b908205 Christoph Egger
      let f = parse_formula symtab ts in
998 4fd28192 Thorsten Wißmann
      match Stream.next ts with
999
      | A.Kwd ")" -> f
1000
      | A.Kwd "+" -> begin
1001 0b908205 Christoph Egger
          let f2 = parse_formula symtab ts in
1002 4fd28192 Thorsten Wißmann
          match Stream.next ts with
1003
          | A.Kwd ")" -> CHC (f, f2)
1004
          | t -> A.printError mk_exn ~t ~ts "\")\" expected: "
1005
        end
1006
      | t -> A.printError mk_exn ~t ~ts "\")\" or \"+\" expected: "
1007
    end
1008 19f5dad0 Dirk Pattinson
  | A.Kwd "O" ->
1009 0b908205 Christoph Egger
    let f = parse_rest symtab ts in
1010 19f5dad0 Dirk Pattinson
      ID f
1011 4fd28192 Thorsten Wißmann
  | A.Kwd "[pi1]" ->
1012 0b908205 Christoph Egger
      let f = parse_rest symtab ts in
1013 4fd28192 Thorsten Wißmann
      FUS (true, f)
1014
  | A.Kwd "[pi2]" ->
1015 0b908205 Christoph Egger
      let f = parse_rest symtab ts in
1016 4fd28192 Thorsten Wißmann
      FUS (false, f)
1017 8334c748 Christoph Egger
  | A.Kwd "μ" ->
1018
      let (_, _, s) = boxinternals true "." in
1019 c5c25acf Christoph Egger
      let symbol = Stream.next gensym in
1020
      let newtab = (s, symbol) :: symtab in
1021 80aa0b2f Christoph Egger
      let f1 = parse_rest newtab ts in
1022
      MU (symbol, f1)
1023 8334c748 Christoph Egger
  | A.Kwd "ν" ->
1024
      let (_, _, s) = boxinternals true "." in
1025 c5c25acf Christoph Egger
      let symbol = Stream.next gensym in
1026
      let newtab = (s, symbol) :: symtab in
1027 80aa0b2f Christoph Egger
      let f1 = parse_rest newtab ts in
1028
      NU (symbol, f1)
1029 0aa34675 Christoph Egger
  | A.Kwd "AF" ->
1030 c5c25acf Christoph Egger
      let f = parse_rest symtab ts in
1031
      AF f
1032 0aa34675 Christoph Egger
  | A.Kwd "EF" ->
1033 c5c25acf Christoph Egger
      let f = parse_rest symtab ts in
1034
      EF f
1035 0aa34675 Christoph Egger
  | A.Kwd "AG" ->
1036 c5c25acf Christoph Egger
      let f = parse_rest symtab ts in
1037
      AG f
1038 0aa34675 Christoph Egger
  | A.Kwd "EG" ->
1039 c5c25acf Christoph Egger
      let f = parse_rest symtab ts in
1040
      EG f
1041 0aa34675 Christoph Egger
  | A.Kwd "A" ->
1042 c5c25acf Christoph Egger
     assert (Stream.next ts = A.Kwd "(");
1043 e30caa42 Christoph Egger
     let f1 = parse_formula symtab ts in begin
1044
       match Stream.next ts with
1045
       | A.Kwd "U" ->
1046
         let f2 = parse_formula symtab ts in
1047
         assert (Stream.next ts = A.Kwd ")");
1048
         AU (f1, f2)
1049
       | A.Kwd "R" ->
1050
         let f2 = parse_formula symtab ts in
1051
         assert (Stream.next ts = A.Kwd ")");
1052
         AR (f1, f2)
1053
       | A.Kwd "B" ->
1054
         let f2 = parse_formula symtab ts in
1055
         assert (Stream.next ts = A.Kwd ")");
1056 97d73a78 Christoph Egger
         AB (f1, f2)
1057 e30caa42 Christoph Egger
       | t -> A.printError mk_exn ~t ~ts "one of \"U\" \"R\" \"B\" expected: "
1058
     end
1059 0aa34675 Christoph Egger
  | A.Kwd "E" ->
1060 c5c25acf Christoph Egger
     assert (Stream.next ts = A.Kwd "(");
1061 e30caa42 Christoph Egger
     let f1 = parse_formula symtab ts in begin
1062
       match Stream.next ts with
1063
       | A.Kwd "U" ->
1064
         let f2 = parse_formula symtab ts in
1065
         assert (Stream.next ts = A.Kwd ")");
1066
         EU (f1, f2)
1067
       | A.Kwd "R" ->
1068
         let f2 = parse_formula symtab ts in
1069
         assert (Stream.next ts = A.Kwd ")");
1070
         ER (f1, f2)
1071
       | A.Kwd "B" ->
1072
         let f2 = parse_formula symtab ts in
1073
         assert (Stream.next ts = A.Kwd ")");
1074 97d73a78 Christoph Egger
         EB (f1, f2)
1075 e30caa42 Christoph Egger
       | t -> A.printError mk_exn ~t ~ts "one of \"U\" \"R\" \"B\" expected: "
1076
     end
1077 0aa34675 Christoph Egger
  | A.Kwd "AX" ->
1078 c5c25acf Christoph Egger
     let f1 = parse_rest symtab ts in
1079
     AX ("", f1)
1080 0aa34675 Christoph Egger
  | A.Kwd "EX" ->
1081 c5c25acf Christoph Egger
     let f1 = parse_rest symtab ts in
1082
     EX ("", f1)
1083
  | t -> A.printError mk_exn ~t ~ts
1084 19f5dad0 Dirk Pattinson
      "\"<\", \"[\", \"{>=\", \"{<=\", \"@\", \"~\", \"(\",
1085
      \"True\", \"False\", \"=\", \"=o\", \"O\" or <ident> expected: "
1086 8334c748 Christoph Egger
1087 4fd28192 Thorsten Wißmann
(** Parses a sorted formula.
1088
    @param ts A token stream.
1089
    @return A sorted formula.
1090
    @raise CoAlgException If ts does not represent a sorted formula.
1091
 *)
1092
let parse_sortedFormula ts =
1093 c5c25acf Christoph Egger
  let nr =
1094 4fd28192 Thorsten Wißmann
    match Stream.peek ts with
1095
    | Some (A.Int n) ->
1096
        if n >= 0 then begin
1097
          Stream.junk ts;
1098
          let () =
1099
            match Stream.next ts with
1100
            | A.Kwd ":" -> ()
1101
            | t -> A.printError mk_exn ~t ~ts ("\":\" expected: ")
1102
          in
1103
          n
1104
        end else
1105
          A.printError mk_exn ~ts ("<non-negative number> expected: ")
1106 c5c25acf Christoph Egger
    | _ -> 0
1107 4fd28192 Thorsten Wißmann
  in
1108 0b908205 Christoph Egger
  let f = parse_formula [] ts in
1109 4fd28192 Thorsten Wißmann
  (nr, f)
1110
1111
(** Parses a list of sorted formulae separated by ";".
1112
    @param ts A token stream.
1113
    @param acc The list of sorted formulae parsed so far.
1114
    @return The resulting list of sorted formula.
1115
    @raise CoAlgException if ts does not represent a list of sorted formulae.
1116
 *)
1117
let rec parse_sortedFormulaList ts acc =
1118
  let f1 = parse_sortedFormula ts in
1119
  match Stream.peek ts with
1120
  | Some (A.Kwd ";") ->
1121
      Stream.junk ts;
1122
      parse_sortedFormulaList ts (f1::acc)
1123
  | _ -> List.rev (f1::acc)
1124
1125
(** A common wrapper for import functions.
1126
    @param fkt An import function.
1127
    @param s A string.
1128
    @return The object imported from s using fkt.
1129
    @raise CoAlgException If ts is not empty.
1130
 *)
1131
let importWrapper fkt s =
1132
  let ts = lexer s in
1133
  try
1134
    let res = fkt ts in
1135
    let _ =
1136
      match Stream.peek ts with
1137
      | None -> ()
1138
      | Some _ -> A.printError mk_exn ~ts "EOS expected: "
1139
    in
1140
    res
1141
  with Stream.Failure -> A.printError mk_exn ~ts "unexpected EOS"
1142
1143
(** Parses a string to obtain a formula.
1144
    @param s A string representing a formula.
1145
    @return The resulting formula.
1146
    @raise CoAlgException if s does not represent a formula.
1147
 *)
1148 0b908205 Christoph Egger
let importFormula s = importWrapper (parse_formula []) s
1149 4fd28192 Thorsten Wißmann
1150
(** Parses a string to obtain a sorted formula.
1151
    @param s A string representing a sorted formula.
1152
    @return The sorted formula.
1153
    @raise CoAlgException If s does not represent a sorted formula.
1154
 *)
1155
let importSortedFormula s = importWrapper parse_sortedFormula s
1156
1157
(** Parses a string to obtain a (sorted) formula query.
1158
    @param s A string representing a formula query.
1159
    @return A pair (tbox, f) where
1160
    tbox is a list of sorted formulae representing the TBox; and
1161
    f is a sorted formula.
1162
    @raise CoAlgException if s does not represent a formula query.
1163
 *)
1164
let importQuery s =
1165
  let fkt ts =
1166
    match Stream.peek ts with
1167
    | Some (A.Kwd "|-") ->
1168
        Stream.junk ts;
1169
        let f = parse_sortedFormula ts in
1170
        ([], f)
1171
    | _ ->
1172
        let fl = parse_sortedFormulaList ts [] in
1173
        match Stream.peek ts with
1174
        | Some (A.Kwd "|-") ->
1175
            Stream.junk ts;
1176
            let f = parse_sortedFormula ts in
1177
            (fl, f)
1178 c5c25acf Christoph Egger
        | _ ->
1179 4fd28192 Thorsten Wißmann
            if List.length fl = 1 then ([], List.hd fl)
1180
            else A.printError mk_exn ~ts "\"|-\" expected: "
1181
  in
1182
  importWrapper fkt s
1183
1184
1185
(** Converts the negation of a formula to negation normal form
1186
    by "pushing in" the negations "~".
1187
    The symbols "<=>" and "=>" are substituted by their usual definitions.
1188
    @param f A formula.
1189
    @return A formula in negation normal form and not containing "<=>" or "=>"
1190
    that is equivalent to ~f.
1191
 *)
1192
let rec nnfNeg f =
1193
  match f with
1194
  | TRUE -> FALSE
1195
  | FALSE -> TRUE
1196
  | AP _ -> NOT f
1197 ff4dc786 Christoph Egger
  | VAR _ -> f
1198 4fd28192 Thorsten Wißmann
  | NOT f1 -> nnf f1
1199
  | AT (s, f1) -> AT (s, nnfNeg f1)
1200
  | OR (f1, f2) -> AND (nnfNeg f1, nnfNeg f2)
1201
  | AND (f1, f2) -> OR (nnfNeg f1, nnfNeg f2)
1202
  | EQU (f1, f2) -> OR (AND (nnf f1, nnfNeg f2), AND (nnf f2, nnfNeg f1))
1203
  | IMP (f1, f2) -> AND (nnf f1, nnfNeg f2)
1204
  | EX (s, f1) -> AX (s, nnfNeg f1)
1205
  | AX (s, f1) -> EX (s, nnfNeg f1)
1206 f1fa9ad5 Thorsten Wißmann
  | ENFORCES (s, f1) -> ALLOWS (s, nnfNeg f1)
1207
  | ALLOWS (s, f1) -> ENFORCES (s, nnfNeg f1)
1208 af276a36 Thorsten Wißmann
  | MIN (n, s, f1) -> if n = 0 then FALSE else MAXEXCEPT (n-1, s, nnfNeg f1)
1209
  | MAX (n, s, f1) -> MORETHAN (n, s, nnf f1)
1210
  | MORETHAN (n, s, f1) -> MAXEXCEPT (n, s, nnfNeg f1)
1211
  | MAXEXCEPT (n, s, f1) -> MORETHAN (n, s, nnfNeg f1)
1212 9bae2c4f Thorsten Wißmann
  | ATLEASTPROB (p, f1) -> LESSPROBFAIL (p, nnfNeg f1)
1213
  | LESSPROBFAIL (p, f1) -> ATLEASTPROB (p, nnfNeg f1)
1214 c49eea11 Thorsten Wißmann
  | CONST s -> CONSTN s
1215
  | CONSTN s -> CONST s
1216 19f5dad0 Dirk Pattinson
  | ID (f1) -> ID (nnfNeg f1)
1217
  | NORM(f1, f2) -> NORMN(nnfNeg f1, nnfNeg f2)
1218
  | NORMN(f1, f2) -> NORM (nnfNeg f1, nnfNeg f2)
1219 c5c25acf Christoph Egger
  | CHC (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2)
1220 4fd28192 Thorsten Wißmann
  | FUS (first, f1) -> FUS (first, nnfNeg f1)
1221 ff4dc786 Christoph Egger
  | MU (s, f1) -> NU(s, nnfNeg f1)
1222
  | NU (s, f1) -> MU(s, nnfNeg f1)
1223 97d73a78 Christoph Egger
  | AF _ | EF _
1224
  | AG _ | EG _
1225
  | AU _ | EU _
1226
  | AR _ | ER _
1227
  | AB _ | EB _ -> raise (CoAlgException ("nnfNeg: CTL should have been removed at this point"))
1228 c5c25acf Christoph Egger
1229 4fd28192 Thorsten Wißmann
(** Converts a formula to negation normal form
1230
    by "pushing in" the negations "~".
1231
    The symbols "<=>" and "=>" are substituted by their usual definitions.
1232
    @param f A formula.
1233
    @return A formula in negation normal form and not containing "<=>" or "=>"
1234
    that is equivalent to f.
1235
 *)
1236
and nnf f =
1237
  match f with
1238
  | TRUE
1239
  | FALSE
1240
  | AP _
1241 c49eea11 Thorsten Wißmann
  | NOT (AP _)
1242
  | CONST _
1243 ff4dc786 Christoph Egger
  | CONSTN _
1244
  | VAR _ -> f
1245 4fd28192 Thorsten Wißmann
  | NOT f1 -> nnfNeg f1
1246
  | AT (s, f1) ->
1247
      let ft1 = nnf f1 in
1248
      if ft1 == f1 then f else AT (s, ft1)
1249
  | OR (f1, f2) ->
1250
      let ft1 = nnf f1 in
1251
      let ft2 = nnf f2 in
1252
      if ft1 == f1 && ft2 == f2 then f else OR (ft1, ft2)
1253
  | AND (f1, f2) ->
1254
      let ft1 = nnf f1 in
1255
      let ft2 = nnf f2 in
1256
      if ft1 == f1 && ft2 == f2 then f else AND (ft1, ft2)
1257
  | EQU (f1, f2) -> AND (OR (nnfNeg f1, nnf f2), OR (nnfNeg f2, nnf f1))
1258
  | IMP (f1, f2) -> OR (nnfNeg f1, nnf f2)
1259 c5c25acf Christoph Egger
  | EX (s, f1) ->
1260 4fd28192 Thorsten Wißmann
      let ft = nnf f1 in
1261
      if ft == f1 then f else EX (s, ft)
1262
  | AX (s, f1) ->
1263
      let ft = nnf f1 in
1264
      if ft == f1 then f else AX (s, ft)
1265 c5c25acf Christoph Egger
  | ENFORCES (s, f1) ->
1266 f1fa9ad5 Thorsten Wißmann
      let ft = nnf f1 in
1267
      if ft == f1 then f else ENFORCES (s, ft)
1268
  | ALLOWS (s, f1) ->
1269
      let ft = nnf f1 in
1270
      if ft == f1 then f else ALLOWS (s, ft)
1271 4fd28192 Thorsten Wißmann
  | MIN (n, s, f1) ->
1272
      if n = 0 then TRUE
1273
      else
1274
        let ft = nnf f1 in
1275 87926e98 Thorsten Wißmann
        MORETHAN (n-1,s,ft)
1276 4fd28192 Thorsten Wißmann
  | MAX (n, s, f1) ->
1277 af276a36 Thorsten Wißmann
      let ft = nnfNeg f1 in
1278
      MAXEXCEPT (n,s, ft)
1279
  | MORETHAN (n,s,f1) ->
1280 4fd28192 Thorsten Wißmann
      let ft = nnf f1 in
1281 af276a36 Thorsten Wißmann
      if ft = f1 then f else MORETHAN (n,s,ft)
1282
  | MAXEXCEPT (n,s,f1) ->
1283
      let ft = nnf f1 in
1284
      if ft = f1 then f else MAXEXCEPT (n,s,ft)
1285 86b07be8 Thorsten Wißmann
  | ATLEASTPROB (p, f1) ->
1286
      let ft = nnf f1 in
1287
      if ft == f1 then f else ATLEASTPROB (p, ft)
1288 9bae2c4f Thorsten Wißmann
  | LESSPROBFAIL (p, f1) ->
1289 86b07be8 Thorsten Wißmann
      let ft = nnf f1 in
1290 9bae2c4f Thorsten Wißmann
      if ft == f1 then f else LESSPROBFAIL (p, ft)
1291 19f5dad0 Dirk Pattinson
  | ID (f1) ->
1292
    let ft = nnf f1 in
1293
    if ft == f1 then f else ID(ft)
1294
  | NORM (f1, f2) ->
1295
      let ft1 = nnf f1 in
1296
      let ft2 = nnf f2 in
1297
      if ft1 == f1 && ft2 == f2 then f else NORM (ft1, ft2)
1298
  | NORMN (f1, f2) ->
1299
      let ft1 = nnf f1 in
1300
      let ft2 = nnf f2 in
1301
      if ft1 == f1 && ft2 == f2 then f else NORMN (ft1, ft2)
1302 4fd28192 Thorsten Wißmann
  | CHC (f1, f2) ->
1303
      let ft1 = nnf f1 in
1304
      let ft2 = nnf f2 in
1305
      if ft1 == f1 && ft2 == f2 then f else CHC (ft1, ft2)
1306
  | FUS (first, f1) ->
1307
      let ft = nnf f1 in
1308
      if ft == f1 then f else FUS (first, ft)
1309 ff4dc786 Christoph Egger
  | MU (s, f1) ->
1310
      let ft = nnf f1 in
1311
      if ft == f1 then f else MU (s, ft)
1312
  | NU (s, f1) ->
1313
      let ft = nnf f1 in
1314
      if ft == f1 then f else NU (s, ft)
1315 97d73a78 Christoph Egger
  | AF _ | EF _
1316
  | AG _ | EG _
1317
  | AU _ | EU _
1318
  | AR _ | ER _
1319
  | AB _ | EB _ ->
1320
            raise (CoAlgException ("nnf: CTL should have been removed at this point"))
1321 4fd28192 Thorsten Wißmann
1322
(** Simplifies a formula.
1323
    @param f A formula which must be in negation normal form.
1324
    @return A formula in negation normal form that is equivalent to f.
1325
    @raise CoAlgException if f is not in negation normal form.
1326
 *)
1327
let rec simplify f =
1328
  match f with
1329
  | TRUE
1330
  | FALSE
1331
  | AP _
1332 fbffb079 Christoph Egger
  | NOT (AP _)
1333
  | VAR _
1334
  | NOT (VAR _) -> f
1335 4fd28192 Thorsten Wißmann
  | AT (s, f1) ->
1336
      let ft = simplify f1 in
1337
      begin
1338
        match ft with
1339
        | FALSE -> FALSE
1340
        | TRUE -> TRUE
1341
        | AT _ -> ft
1342
        | AP s1 when s = s1 -> TRUE
1343
        | NOT (AP s1) when s = s1 -> FALSE
1344
        | _ -> if ft == f1 then f else AT (s, ft)
1345
      end
1346
  | OR (f1, f2) ->
1347
      let ft1 = simplify f1 in
1348
      let ft2 = simplify f2 in
1349
      begin
1350
        match ft1, ft2 with
1351
        | TRUE, _ -> TRUE
1352
        | FALSE, _ -> ft2
1353
        | _, TRUE -> TRUE
1354
        | _, FALSE -> ft1
1355
        | _, _ ->
1356 c5c25acf Christoph Egger
            if (f1 == ft1) && (f2 == ft2) then f
1357 4fd28192 Thorsten Wißmann
            else OR (ft1, ft2)
1358
      end
1359
  | AND (f1, f2) ->
1360
      let ft1 = simplify f1 in
1361
      let ft2 = simplify f2 in
1362
      begin
1363
        match ft1, ft2 with
1364
        | TRUE, _ -> ft2
1365
        | FALSE, _ -> FALSE
1366
        | _, TRUE -> ft1
1367
        | _, FALSE -> FALSE
1368
        | _, _ ->
1369 c5c25acf Christoph Egger
            if (f1 == ft1) && (f2 == ft2) then f
1370 4fd28192 Thorsten Wißmann
            else AND (ft1, ft2)
1371
      end
1372
  | NOT _
1373
  | EQU _
1374
  | IMP _ -> raise (CoAlgException "Formula is not in negation normal form.")
1375
  | EX (s, f1) ->
1376
      let ft = simplify f1 in
1377
      begin
1378
        match ft with
1379
        | FALSE -> FALSE
1380
        | _ -> if ft == f1 then f else EX (s, ft)
1381
      end
1382
  | AX (s, f1) ->
1383
      let ft = simplify f1 in
1384
      begin
1385
        match ft with
1386
        | TRUE -> TRUE
1387
        | _ -> if ft == f1 then f else AX (s, ft)
1388
      end
1389 f1fa9ad5 Thorsten Wißmann
  | ENFORCES (s, f1) ->
1390
      let ft = simplify f1 in
1391
      begin
1392
        match ft with
1393
        (* Simplification rules are checked with dirks Generic.hs
1394
        let enforce ls = M (C ls)
1395
        let allow   ls = Neg . M (C ls) . Neg
1396
        provable $ F <-> enforce [1,2] F
1397
        *)
1398
        | TRUE -> TRUE
1399
        | FALSE -> FALSE
1400
        | _ -> if ft == f1 then f else ENFORCES (s, ft)
1401
      end
1402
  | ALLOWS (s, f1) ->
1403
      let ft = simplify f1 in
1404
      begin
1405
        match ft with
1406
        (* Simplification rules are checked with dirks Generic.hs
1407
        let enforce ls = M (C ls)
1408
        let allow   ls = Neg . M (C ls) . Neg
1409
        provable $ F <-> enforce [1,2] F
1410
        *)
1411
        | TRUE -> TRUE
1412
        | FALSE -> FALSE
1413
        | _ -> if ft == f1 then f else ALLOWS (s, ft)
1414
      end
1415 4fd28192 Thorsten Wißmann
  | MIN (n, s, f1) ->
1416
      if n = 0 then TRUE
1417
      else
1418
        let ft = simplify f1 in
1419
        begin
1420
          match ft with
1421
          | FALSE -> FALSE
1422
          | _ -> if ft == f1 then f else MIN (n, s, ft)
1423
        end
1424 af276a36 Thorsten Wißmann
  | MORETHAN (n,s,f1) ->
1425
      let ft = simplify f1 in
1426
      if ft == f1 then f else MORETHAN (n,s,ft)
1427
  | MAXEXCEPT (n,s,f1) ->
1428
      let ft = simplify f1 in
1429
      if ft == f1 then f else MAXEXCEPT (n,s,ft)
1430 4fd28192 Thorsten Wißmann
  | MAX (n, s, f1) ->
1431
      let ft = simplify f1 in
1432
      begin
1433
        match ft with
1434
        | FALSE -> TRUE
1435
        | _ -> if ft == f1 then f else MAX (n, s, ft)
1436
      end
1437 9bae2c4f Thorsten Wißmann
  | LESSPROBFAIL (p,f1) ->
1438 86b07be8 Thorsten Wißmann
      let ft1 = simplify f1 in
1439 9bae2c4f Thorsten Wißmann
      if (ft1 == f1) then f else LESSPROBFAIL (p,ft1)
1440 86b07be8 Thorsten Wißmann
  | ATLEASTPROB (p,f1) ->
1441
      let ft1 = simplify f1 in
1442
      if (ft1 == f1) then f else ATLEASTPROB (p,ft1)
1443 c49eea11 Thorsten Wißmann
  | CONST _
1444
  | CONSTN _ -> f (* no simplifications possible *)
1445 19f5dad0 Dirk Pattinson
  | ID (f1) ->
1446
    let ft1 = simplify f1 in
1447
    begin
1448
      match ft1 with
1449
        | TRUE -> TRUE
1450
        | FALSE -> FALSE
1451
        | _ -> if (ft1 == f1) then f else ID (ft1)
1452
    end
1453
  (* todo: more simplifications for KLM? *)
1454
  | NORM (f1, f2) ->
1455
      let ft1 = simplify f1 in
1456
      let ft2 = simplify f2 in
1457
      begin
1458
        match ft2 with
1459
          | TRUE -> TRUE
1460
          | _ ->
1461 c5c25acf Christoph Egger
            if (f1 == ft1) && (f2 == ft2) then f
1462 19f5dad0 Dirk Pattinson
            else NORM (ft1, ft2)
1463
      end
1464
  | NORMN (f1, f2) ->
1465
      let ft1 = simplify f1 in
1466
      let ft2 = simplify f2 in
1467
      begin
1468
        match ft2 with
1469
          | FALSE -> FALSE
1470
          | _ ->
1471 c5c25acf Christoph Egger
            if (f1 == ft1) && (f2 == ft2) then f
1472 19f5dad0 Dirk Pattinson
            else NORMN (ft1, ft2)
1473
      end
1474 4fd28192 Thorsten Wißmann
  | CHC (f1, f2) ->
1475
      let ft1 = simplify f1 in
1476
      let ft2 = simplify f2 in
1477
      begin
1478
        match ft1, ft2 with
1479
        | TRUE, TRUE -> TRUE
1480
        | FALSE, FALSE -> FALSE
1481
        | _, _ ->
1482 c5c25acf Christoph Egger
            if (f1 == ft1) && (f2 == ft2) then f
1483 4fd28192 Thorsten Wißmann
            else CHC (ft1, ft2)
1484
      end
1485
  | FUS (first, f1) ->
1486
      let ft = simplify f1 in
1487
      begin
1488
        match ft with
1489
        | FALSE -> FALSE
1490
        | TRUE -> TRUE
1491
        | _ -> if ft == f1 then f else FUS (first, ft)
1492
      end
1493 fbffb079 Christoph Egger
  | MU (s, f1) ->
1494
      let ft = simplify f1 in
1495
      begin
1496
        match ft with
1497
        | TRUE -> TRUE
1498
        | _ -> if ft == f1 then f else MU (s, ft)
1499
      end
1500
  | NU (s, f1) ->
1501
      let ft = simplify f1 in
1502
      begin
1503
        match ft with
1504
        | TRUE -> TRUE
1505
        | _ -> if ft == f1 then f else NU (s, ft)
1506
      end
1507 97d73a78 Christoph Egger
  | AF _ | EF _
1508
  | AG _ | EG _
1509
  | AU _ | EU _
1510
  | AR _ | ER _
1511
  | AB _ | EB _ ->
1512
            raise (CoAlgException ("nnf: CTL should have been removed at this point"))
1513 4fd28192 Thorsten Wißmann
1514
(** Destructs an atomic proposition.
1515
    @param f An atomic proposition.
1516
    @return The name of the atomic proposition.
1517
    @raise CoAlgException if f is not an atomic proposition.
1518
 *)
1519
let dest_ap f =
1520
  match f with
1521
  | AP s when not (isNominal s) -> s
1522
  | _ -> raise (CoAlgException "Formula is not an atomic proposition.")
1523
1524
(** Destructs a nominal.
1525
    @param f A nominal.
1526
    @return The name of the nominal
1527
    @raise CoAlgException if f is not a nominal.
1528
 *)
1529
let dest_nom f =
1530
  match f with
1531
  | AP s when isNominal s -> s
1532
  | _ -> raise (CoAlgException "Formula is not a nominal.")
1533
1534
(** Destructs a negation.
1535
    @param f A negation.
1536
    @return The immediate subformula of the negation.
1537
    @raise CoAlgException if f is not a negation.
1538
 *)
1539
let dest_not f =
1540
  match f with
1541
  | NOT f1 -> f1
1542
  | _ -> raise (CoAlgException "Formula is not a negation.")
1543
1544
(** Destructs an @-formula.
1545
    @param f An @-formula.
1546
    @return The name of the nominal and the immediate subformula of the @-formula.
1547
    @raise CoAlgException if f is not an @-formula.
1548
 *)
1549
let dest_at f =
1550
  match f with
1551
  | AT (s, f1) -> (s, f1)
1552
  | _ -> raise (CoAlgException "Formula is not an @-formula.")
1553
1554
(** Destructs an or-formula.
1555
    @param f An or-formula.
1556
    @return The two immediate subformulae of the or-formula.
1557
    @raise CoAlgException if f is not an or-formula.
1558
 *)
1559
let dest_or f =
1560
  match f with
1561
  | OR (f1, f2) -> (f1, f2)
1562
  | _ -> raise (CoAlgException "Formula is not an or-formula.")
1563
1564
(** Destructs an and-formula.
1565
    @param f An and-formula.
1566
    @return The two immediate subformulae of the and-formula.
1567
    @raise CoAlgException if f is not an and-formula.
1568
 *)
1569
let dest_and f =
1570
  match f with
1571
  | AND (f1, f2) -> (f1, f2)
1572
  | _ -> raise (CoAlgException "Formula is not an and-formula.")
1573
1574
(** Destructs an equivalence.
1575
    @param f An equivalence.
1576
    @return The two immediate subformulae of the equivalence.
1577
    @raise CoAlgException if f is not an equivalence.
1578
 *)
1579
let dest_equ f =
1580
  match f with
1581
  | EQU (f1, f2) -> (f1, f2)
1582
  | _ -> raise (CoAlgException "Formula is not an equivalence.")
1583
1584
(** Destructs an implication.
1585
    @param f An implication.
1586
    @return The two immediate subformulae of the implication.
1587
    @raise CoAlgException if f is not an implication.
1588
 *)
1589
let dest_imp f =
1590
  match f with
1591
  | IMP (f1, f2) -> (f1, f2)
1592
  | _ -> raise (CoAlgException "Formula is not an implication.")
1593
1594
(** Destructs an EX-formula.
1595
    @param f An EX-formula.
1596
    @return The role name and the immediate subformula of the EX-formula.
1597
    @raise CoAlgException if f is not an EX-formula.
1598
 *)
1599
let dest_ex f =
1600
  match f with
1601
  | EX (s, f1) -> (s, f1)
1602
  | _ -> raise (CoAlgException "Formula is not an EX-formula.")
1603
1604
(** Destructs an AX-formula.
1605
    @param f An AX-formula.
1606
    @return The role name and the immediate subformula of the AX-formula.
1607
    @raise CoAlgException if f is not an AX-formula.
1608
 *)
1609
let dest_ax f =
1610
  match f with
1611
  | AX (s, f1) -> (s, f1)
1612
  | _ -> raise (CoAlgException "Formula is not an AX-formula.")
1613
1614
(** Destructs a MIN-formula.
1615
    @param f A MIN-formula.
1616
    @return The number restriction, role name,
1617
    and the immediate subformula of the MIN-formula.
1618
    @raise CoAlgException if f is not a MIN-formula.
1619
 *)
1620
let dest_min f =
1621
  match f with
1622
  | MIN (n, s, f1) -> (n, s, f1)
1623
  | _ -> raise (CoAlgException "Formula is not a MIN-formula.")
1624
1625
(** Destructs a MAX-formula.
1626
    @param f A MAX-formula.
1627
    @return The number restriction, role name,
1628
    and the immediate subformula of the MAX-formula.
1629
    @raise CoAlgException if f is not a MAX-formula.
1630
 *)
1631
let dest_max f =
1632
  match f with
1633
  | MAX (n, s, f1) -> (n, s, f1)
1634
  | _ -> raise (CoAlgException "Formula is not a MAX-formula.")
1635
1636
(** Destructs a choice formula.
1637
    @param f A choice formula.
1638
    @return The two immediate subformulae of the choice formula.
1639
    @raise CoAlgException if f is not a choice formula.
1640
 *)
1641
let dest_choice f =
1642
  match f with
1643
  | CHC (f1, f2) -> (f1, f2)
1644
  | _ -> raise (CoAlgException "Formula is not a choice formula.")
1645
1646
(** Destructs a fusion formula.
1647
    @param f A fusion formula.
1648
    @return A pair (first, f1) where
1649
    first is true iff f is a first projection; and
1650
    f1 is the immediate subformulae of f.
1651
    @raise CoAlgException if f is not a fusion formula.
1652
 *)
1653
let dest_fusion f =
1654
  match f with
1655
  | FUS (first, f1) -> (first, f1)
1656
  | _ -> raise (CoAlgException "Formula is not a fusion formula.")
1657
1658
1659
(** Tests whether a formula is the constant True.
1660
    @param f A formula.
1661
    @return True iff f is the constant True.
1662
 *)
1663
let is_true f =
1664
  match f with
1665
  | TRUE -> true
1666
  | _ -> false
1667
1668
(** Tests whether a formula is the constant False.
1669
    @param f A formula.
1670
    @return True iff f is the constant False.
1671
 *)
1672
let is_false f =
1673
  match f with
1674
  | FALSE -> true
1675
  | _ -> false
1676
1677
(** Tests whether a formula is an atomic proposition.
1678
    @param f A formula.
1679
    @return True iff f is an atomic proposition.
1680
 *)
1681
let is_ap f =
1682
  match f with
1683
  | AP s when not (isNominal s) -> true
1684
  | _ -> false
1685
1686
(** Tests whether a formula is a nominal.
1687
    @param f A formula.
1688
    @return True iff f is a nominal.
1689
 *)
1690
let is_nom f =
1691
  match f with
1692
  | AP s when isNominal s -> true
1693
  | _ -> false
1694
1695
(** Tests whether a formula is a negation.
1696
    @param f A formula.
1697
    @return True iff f is a negation.
1698
 *)
1699
let is_not f =
1700
  match f with
1701
  | NOT _ -> true
1702
  | _ -> false
1703
1704
(** Tests whether a formula is an @-formula.
1705
    @param f A formula.
1706
    @return True iff f is an @-formula.
1707
 *)
1708
let is_at f =
1709
  match f with
1710
  | AT _ -> true
1711
  | _ -> false
1712
1713
(** Tests whether a formula is an or-formula.
1714
    @param f A formula.
1715
    @return True iff f is an or-formula.
1716
 *)
1717
let is_or f =
1718
  match f with
1719
  | OR _ -> true
1720
  | _ -> false
1721
1722
(** Tests whether a formula is an and-formula.
1723
    @param f A formula.
1724
    @return True iff f is an and-formula.
1725
 *)
1726
let is_and f =
1727
  match f with
1728
  | AND _ -> true
1729
  | _ -> false
1730
1731
(** Tests whether a formula is an equivalence.
1732
    @param f A formula.
1733
    @return True iff f is an equivalence.
1734
 *)
1735
let is_equ f =
1736
  match f with
1737
  | EQU _ -> true
1738
  | _ -> false
1739
1740
(** Tests whether a formula is an implication.
1741
    @param f A formula.
1742
    @return True iff f is an implication.
1743
 *)
1744
let is_imp f =
1745
  match f with
1746
  | IMP _ -> true
1747
  | _ -> false
1748
1749
(** Tests whether a formula is an EX-formula.
1750
    @param f A formula.
1751
    @return True iff f is an EX-formula.
1752
 *)
1753
let is_ex f =
1754
  match f with
1755
  | EX _ -> true
1756
  | _ -> false
1757
1758
(** Tests whether a formula is an AX-formula.
1759
    @param f A formula.
1760
    @return True iff f is an AX-formula.
1761
 *)
1762
let is_ax f =
1763
  match f with
1764
  | AX _ -> true
1765
  | _ -> false
1766
1767
(** Tests whether a formula is a MIN-formula.
1768
    @param f A formula.
1769
    @return True iff f is a MIN-formula.
1770
 *)
1771
let is_min f =
1772
  match f with
1773
  | MIN _ -> true
1774
  | _ -> false
1775
1776
(** Tests whether a formula is a MAX-formula.
1777
    @param f A formula.
1778
    @return True iff f is a MAX-formula.
1779
 *)
1780
let is_max f =
1781
  match f with
1782
  | MAX _ -> true
1783
  | _ -> false
1784
1785
(** Tests whether a formula is a choice formula.
1786
    @param f A formula.
1787
    @return True iff f is a choice formula.
1788
 *)
1789
let is_choice f =
1790
  match f with
1791
  | CHC _ -> true
1792
  | _ -> false
1793
1794
(** Tests whether a formula is a fusion formula.
1795
    @param f A formula.
1796
    @return True iff f is a fusion formula.
1797
 *)
1798
let is_fusion f =
1799
  match f with
1800
  | FUS _ -> true
1801
  | _ -> false
1802
1803 c5c25acf Christoph Egger
1804 4fd28192 Thorsten Wißmann
(** The constant True.
1805
 *)
1806
let const_true = TRUE
1807
1808
(** The constant False.
1809
 *)
1810
let const_false = FALSE
1811 c5c25acf Christoph Egger
1812 4fd28192 Thorsten Wißmann
(** Constructs an atomic proposition.
1813
    @param s The name of the atomic proposition.
1814
    @return The atomic proposition with name s.
1815
    @raise CoAlgException if s is a nominal name.
1816
 *)
1817
let const_ap s =
1818
  if isNominal s then raise (CoAlgException "The name indicates a nominal.")
1819
  else AP s
1820
1821
(** Constructs a nominal.
1822
    @param s The name of the nominal.
1823
    @return A nominal with name s.
1824
    @raise CoAlgException if s is not a nominal name.
1825
 *)
1826
let const_nom s =
1827
  if isNominal s then AP s
1828
  else raise (CoAlgException "The name does not indicate a nominal.")
1829
1830
(** Negates a formula.
1831
    @param f A formula.
1832
    @return The negation of f.
1833
 *)
1834
let const_not f = NOT f
1835 c5c25acf Christoph Egger
1836 4fd28192 Thorsten Wißmann
(** Constructs an @-formula from a name and a formula.
1837
    @param s A nominal name.
1838
    @param f A formula.
1839
    @return The formula AT (s, f).
1840
 *)
1841
let const_at s f = AT (s, f)
1842
1843
(** Constructs an or-formula from two formulae.
1844
    @param f1 The first formula (LHS).
1845
    @param f2 The second formula (LHS).
1846
    @return The formula f1 | f2.
1847
 *)
1848
let const_or f1 f2 = OR (f1, f2)
1849
1850
(** Constructs an and-formula from two formulae.
1851
    @param f1 The first formula (LHS).
1852
    @param f2 The second formula (LHS).
1853
    @return The formula f1 & f2.
1854 c5c25acf Christoph Egger
 *)
1855 4fd28192 Thorsten Wißmann
let const_and f1 f2 = AND (f1, f2)
1856
1857
(** Constructs an equivalence from two formulae.
1858
    @param f1 The first formula (LHS).
1859
    @param f2 The second formula (LHS).
1860
    @return The equivalence f1 <=> f2.
1861
 *)
1862
let const_equ f1 f2 = EQU (f1, f2)
1863
1864
(** Constructs an implication from two formulae.
1865
    @param f1 The first formula (LHS).
1866
    @param f2 The second formula (LHS).
1867
    @return The implication f1 => f2.
1868
 *)
1869
let const_imp f1 f2 = IMP (f1, f2)
1870
1871
(** Constructs an EX-formula from a formula.
1872
    @param s A role name.
1873
    @param f A formula.
1874
    @return The formula EX (s, f).
1875
 *)
1876
let const_ex s f = EX (s, f)
1877
1878
(** Constructs an AX-formula from a formula.
1879
    @param s A role name.
1880
    @param f A formula.
1881
    @return The formula AX (s, f).
1882
 *)
1883
let const_ax s f = AX (s, f)
1884
1885
(** Constructs a MIN-formula from a formula.
1886
    @param n A non-negative integer.
1887
    @param s A role name.
1888
    @param f A formula.
1889
    @return The formula MIN f.
1890
    @raise CoAlgException Iff n is negative.
1891
 *)
1892
let const_min n s f =
1893
  if n < 0 then raise (CoAlgException "Negative cardinality constraint.")
1894
  else MIN (n, s, f)
1895
1896
(** Constructs a MAX-formula from a formula.
1897
    @param n A non-negative integer.
1898
    @param s A role name.
1899
    @param f A formula.
1900
    @return The formula MAX f.
1901
    @raise CoAlgException Iff n is negative.
1902
 *)
1903
let const_max n s f =
1904
  if n < 0 then raise (CoAlgException "Negative cardinality constraint.")
1905
  else MAX (n, s, f)
1906
1907 7993e0bf Thorsten Wißmann
let const_enforces p f =
1908
    ENFORCES (p,f)
1909
1910
let const_allows p f =
1911
    ALLOWS (p,f)
1912
1913 4fd28192 Thorsten Wißmann
(** Constructs a choice formula from two formulae.
1914
    @param f1 The first formula (LHS).
1915
    @param f2 The second formula (LHS).
1916
    @return The formula (f1 + f2).
1917
 *)
1918
let const_choice f1 f2 = CHC (f1, f2)
1919
1920
(** Constructs a fusion formula.
1921
    @param first True iff the result is a first projection.
1922
    @param f1 A formula.
1923
    @return The formula [pi1] f1 or [pi2] f1 (depending on first).
1924
 *)
1925
let const_fusion first f1 = FUS (first, f1)
1926
1927
1928
(** Hash-consed formulae, which are in negation normal form,
1929
    such that structural and physical equality coincide.
1930 87d5082f Christoph Egger
1931
    Also CTL has been replaced by the equivalent μ-Calculus
1932
    constructs
1933 4fd28192 Thorsten Wißmann
 *)
1934
type hcFormula = (hcFormula_node, formula) HC.hash_consed
1935
and hcFormula_node =
1936
  | HCTRUE
1937
  | HCFALSE
1938
  | HCAP of string
1939
  | HCNOT of string
1940
  | HCAT of string * hcFormula
1941
  | HCOR of hcFormula * hcFormula
1942
  | HCAND of hcFormula * hcFormula
1943
  | HCEX of string * hcFormula
1944
  | HCAX of string * hcFormula
1945 f1fa9ad5 Thorsten Wißmann
  | HCENFORCES of int list * hcFormula
1946
  | HCALLOWS of int list * hcFormula
1947 af276a36 Thorsten Wißmann
  | HCMORETHAN of int * string * hcFormula (* GML Diamond *)
1948
  | HCMAXEXCEPT of int * string * hcFormula (* GML Box *)
1949 86b07be8 Thorsten Wißmann
  | HCATLEASTPROB of rational * hcFormula
1950 9bae2c4f Thorsten Wißmann
  | HCLESSPROBFAIL of rational * hcFormula
1951 c49eea11 Thorsten Wißmann
  | HCCONST of string
1952
  | HCCONSTN of string
1953 19f5dad0 Dirk Pattinson
  | HCID of hcFormula
1954
  | HCNORM of hcFormula * hcFormula
1955
  | HCNORMN of hcFormula * hcFormula
1956 4fd28192 Thorsten Wißmann
  | HCCHC of hcFormula * hcFormula
1957
  | HCFUS of bool * hcFormula
1958 87d5082f Christoph Egger
  | HCMU of string * hcFormula
1959
  | HCNU of string * hcFormula
1960
  | HCVAR of string
1961 4fd28192 Thorsten Wißmann
1962
(** Determines whether two formula nodes are structurally equal.
1963
    @param f1 The first formula node.
1964
    @param f2 The second formula node.
1965
    @return True iff f1 and f2 are structurally equal.
1966
 *)
1967
let equal_hcFormula_node f1 f2 =
1968
  match f1, f2 with
1969
  | HCTRUE, HCTRUE -> true
1970
  | HCFALSE, HCFALSE -> true
1971 c49eea11 Thorsten Wißmann
  | HCCONST s1, HCCONST s2
1972
  | HCCONSTN s1, HCCONSTN s2
1973 4fd28192 Thorsten Wißmann
  | HCAP s1, HCAP s2
1974
  | HCNOT s1, HCNOT s2 -> compare s1 s2 = 0
1975
  | HCAT (s1, f1), HCAT (s2, f2) -> compare s1 s2 = 0 && f1 == f2
1976
  | HCOR (f1a, f1b), HCOR (f2a, f2b)
1977
  | HCAND (f1a, f1b), HCAND (f2a, f2b) -> f1a == f2a && f1b == f2b
1978
  | HCEX (s1, f1), HCEX (s2, f2)
1979
  | HCAX (s1, f1), HCAX (s2, f2) -> compare s1 s2 = 0 && f1 == f2
1980 bc6db513 Thorsten Wißmann
  | HCENFORCES (s1, f1), HCENFORCES (s2, f2)
1981
  | HCALLOWS (s1, f1), HCALLOWS (s2, f2) -> compare s1 s2 = 0 && f1 == f2
1982 af276a36 Thorsten Wißmann
  | HCMORETHAN (n1, s1, f1), HCMORETHAN (n2, s2, f2)
1983
  | HCMAXEXCEPT (n1, s1, f1), HCMAXEXCEPT (n2, s2, f2) ->
1984 c5c25acf Christoph Egger
      n1 = n2 && compare s1 s2 = 0 && f1 == f2
1985 86b07be8 Thorsten Wißmann
  | HCATLEASTPROB (p1, f1), HCATLEASTPROB (p2,f2) ->
1986
      p1 = p2 && f1 == f2
1987 9bae2c4f Thorsten Wißmann
  | HCLESSPROBFAIL (p1, f1), HCLESSPROBFAIL (p2,f2) ->
1988 86b07be8 Thorsten Wißmann
      p1 = p2 && f1 == f2
1989 19f5dad0 Dirk Pattinson
  | HCID f1, HCID f2 -> f1 == f2
1990
  | HCNORM (f1a, f1b), HCNORMN (f2a, f2b) -> f1a == f2a && f1b == f2b
1991 4fd28192 Thorsten Wißmann
  | HCCHC (f1a, f1b), HCCHC (f2a, f2b) -> f1a == f2a && f1b == f2b
1992
  | HCFUS (first1, f1), HCFUS (first2, f2) -> first1 = first2 && f1 == f2
1993 a7ae917b Christoph Egger
  | HCMU (name1, f1), HCMU(name2, f2) -> compare name1 name2 = 0 && f1 == f2
1994
  | HCNU (name1, f1), HCNU(name2, f2) -> compare name1 name2 = 0 && f1 == f2
1995
  | HCVAR name1, HCVAR name2 -> compare name1 name2 = 0
1996 4fd28192 Thorsten Wißmann
(* The rest could be shortened to | _ -> false,
1997
   but then the compiler would not warn if the formula type is extended
1998
   and this function is not updated accordingly.*)
1999
  | HCTRUE, _
2000
  | HCFALSE, _
2001
  | HCAP _, _
2002
  | HCNOT _, _
2003
  | HCAT _, _
2004
  | HCOR _, _
2005
  | HCAND _, _
2006
  | HCEX _, _
2007
  | HCAX _, _
2008 f1fa9ad5 Thorsten Wißmann
  | HCENFORCES _, _
2009
  | HCALLOWS   _, _
2010 af276a36 Thorsten Wißmann
  | HCMORETHAN _, _
2011
  | HCMAXEXCEPT _, _
2012 86b07be8 Thorsten Wißmann
  | HCATLEASTPROB _, _
2013 9bae2c4f Thorsten Wißmann
  | HCLESSPROBFAIL _, _
2014 c49eea11 Thorsten Wißmann
  | HCCONST _, _
2015
  | HCCONSTN _, _
2016 19f5dad0 Dirk Pattinson
  | HCID _, _
2017
  | HCNORM _, _
2018
  | HCNORMN _, _
2019 4fd28192 Thorsten Wißmann
  | HCCHC _, _
2020 a7ae917b Christoph Egger
  | HCFUS _, _
2021
  | HCMU _, _
2022
  | HCNU _, _
2023
  | HCVAR _, _ -> false
2024 4fd28192 Thorsten Wißmann
2025
(** Computes the hash value of a formula node.
2026
    @param f A formula node.
2027
    @return The hash value of f.
2028
 *)
2029
let hash_hcFormula_node f =
2030 19f5dad0 Dirk Pattinson
  let base = 23 in (* should be larger than the no of constructors *)
2031 4fd28192 Thorsten Wißmann
  match f with
2032
  | HCTRUE -> 0
2033
  | HCFALSE -> 1
2034
  | HCAP s
2035 508e3c33 Christoph Egger
  | HCNOT s
2036
  | HCVAR s -> base * Hashtbl.hash s + 1
2037 19f5dad0 Dirk Pattinson
  | HCAT (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 2
2038
  | HCOR (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 5
2039
  | HCAND (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 6
2040
  | HCEX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 3
2041
  | HCAX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 4
2042
  | HCMORETHAN (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 7
2043
  | HCMAXEXCEPT (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 8
2044
  | HCATLEASTPROB (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 9
2045
  | HCLESSPROBFAIL (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 10
2046
  | HCCHC (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 11
2047
  | HCFUS (first, f1) -> base * (base * (Hashtbl.hash first) + f1.HC.hkey) + 13
2048
  | HCENFORCES (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 14
2049
  | HCALLOWS   (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 15
2050 c49eea11 Thorsten Wißmann
  | HCCONST s -> Hashtbl.hash s + 16
2051
  | HCCONSTN s -> Hashtbl.hash s + 17
2052 19f5dad0 Dirk Pattinson
  | HCNORM (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 18
2053
  | HCNORMN (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 19
2054
  | HCID (f1) -> base * f1.HC.hkey + 20
2055 508e3c33 Christoph Egger
  | HCMU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 21
2056
  | HCNU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 22
2057 4fd28192 Thorsten Wißmann
2058
(** Determines the "real" formula of a formula node.
2059
    @param f A formula node.
2060
    @return The formula (in negation normal form) which corresponds to f.
2061
 *)
2062
let toFml_hcFormula_node f =
2063
  match f with
2064
  | HCTRUE -> TRUE
2065
  | HCFALSE -> FALSE
2066
  | HCAP s -> AP s
2067 508e3c33 Christoph Egger
  | HCVAR s -> VAR s
2068 4fd28192 Thorsten Wißmann
  | HCNOT s -> NOT (AP s)
2069
  | HCAT (s, f1) -> AT (s, f1.HC.fml)
2070
  | HCOR (f1, f2) -> OR (f1.HC.fml, f2.HC.fml)
2071
  | HCAND (f1, f2) -> AND (f1.HC.fml, f2.HC.fml)
2072
  | HCEX (s, f1) -> EX (s, f1.HC.fml)
2073
  | HCAX (s, f1) -> AX (s, f1.HC.fml)
2074 f1fa9ad5 Thorsten Wißmann
  | HCENFORCES (s, f1) -> ENFORCES (s, f1.HC.fml)
2075
  | HCALLOWS (s, f1) -> ALLOWS (s, f1.HC.fml)
2076 af276a36 Thorsten Wißmann
  | HCMORETHAN (n, s, f1) -> MORETHAN (n, s, f1.HC.fml)
2077
  | HCMAXEXCEPT (n, s, f1) -> MAXEXCEPT (n, s, f1.HC.fml)
2078 86b07be8 Thorsten Wißmann
  | HCATLEASTPROB (p, f1) -> ATLEASTPROB (p, f1.HC.fml)
2079 9bae2c4f Thorsten Wißmann
  | HCLESSPROBFAIL (p, f1) -> LESSPROBFAIL (p, f1.HC.fml)
2080 c49eea11 Thorsten Wißmann
  | HCCONST s -> CONST s
2081
  | HCCONSTN s -> CONSTN s
2082 19f5dad0 Dirk Pattinson
  | HCID (f1) -> ID(f1.HC.fml)
2083
  | HCNORM (f1, f2) -> NORM(f1.HC.fml, f2.HC.fml)
2084
  | HCNORMN (f1, f2) -> NORMN(f1.HC.fml, f2.HC.fml)
2085 4fd28192 Thorsten Wißmann
  | HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml)
2086
  | HCFUS (first, f1) -> FUS (first, f1.HC.fml)
2087 508e3c33 Christoph Egger
  | HCMU (var, f1) -> MU (var, f1.HC.fml)
2088
  | HCNU (var, f1) -> NU (var, f1.HC.fml)
2089 4fd28192 Thorsten Wißmann
2090
(** Determines the negation (in negation normal form) of a formula node.
2091
    @param f A formula node.
2092
    @return The negation (in negation normal form) of f.
2093
 *)
2094
let negNde_hcFormula_node f =
2095
  match f with
2096
  | HCTRUE -> HCFALSE
2097
  | HCFALSE -> HCTRUE
2098
  | HCAP s -> HCNOT s
2099
  | HCNOT s -> HCAP s
2100 92feed46 Christoph Egger
  | HCVAR s -> f
2101 4fd28192 Thorsten Wißmann
  | HCAT (s, f1) -> HCAT (s, f1.HC.neg)
2102
  | HCOR (f1, f2) -> HCAND (f1.HC.neg, f2.HC.neg)
2103
  | HCAND (f1, f2) -> HCOR (f1.HC.neg, f2.HC.neg)
2104
  | HCEX (s, f2) -> HCAX (s, f2.HC.neg)
2105
  | HCAX (s, f2) -> HCEX (s, f2.HC.neg)
2106 f1fa9ad5 Thorsten Wißmann
  | HCENFORCES (s, f2) -> HCALLOWS (s, f2.HC.neg)
2107
  | HCALLOWS (s, f2) -> HCENFORCES (s, f2.HC.neg)
2108 af276a36 Thorsten Wißmann
  | HCMORETHAN (n, s, f1) -> HCMAXEXCEPT (n, s, f1.HC.neg)
2109
  | HCMAXEXCEPT (n, s, f1) -> HCMORETHAN (n, s, f1.HC.neg)
2110 9bae2c4f Thorsten Wißmann
  | HCATLEASTPROB (p, f1) -> HCLESSPROBFAIL (p, f1.HC.neg)
2111
  | HCLESSPROBFAIL (p, f1) -> HCATLEASTPROB (p, f1.HC.neg)
2112 c49eea11 Thorsten Wißmann
  | HCCONST s -> HCCONSTN s
2113
  | HCCONSTN s -> HCCONST s
2114 19f5dad0 Dirk Pattinson
  | HCID (f1) -> HCID(f1.HC.neg)
2115
  | HCNORM (f1, f2) -> HCNORMN(f1.HC.neg, f2.HC.neg)
2116
  | HCNORMN (f1, f2) -> HCNORM(f1.HC.neg, f2.HC.neg)
2117 d58bba0f Dirk Pattinson
  | HCCHC (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg)
2118 4fd28192 Thorsten Wißmann
  | HCFUS (first, f1) -> HCFUS (first, f1.HC.neg)
2119 92feed46 Christoph Egger
  | HCMU (name, f1) -> HCNU (name, f1.HC.neg)
2120
  | HCNU (name, f1) -> HCMU (name, f1.HC.neg)
2121 4fd28192 Thorsten Wißmann
2122
(** An instantiation of hash-consing for formulae.
2123
 *)
2124
module HcFormula = HC.Make(
2125
  struct
2126
    type nde = hcFormula_node
2127
    type fml = formula
2128
    let equal (n1 : nde) n2 = equal_hcFormula_node n1 n2
2129
    let hash (n : nde) = hash_hcFormula_node n
2130
    let negNde (n : nde) = negNde_hcFormula_node n
2131
    let toFml (n : nde) = toFml_hcFormula_node n
2132
  end
2133
 )
2134
2135
(** Converts a formula into its hash-consed version.
2136
    @param hcF A hash-cons table for formulae.
2137
    @param f A formula in negation normal form.
2138
    @return The hash-consed version of f.
2139
    @raise CoAlgException if f is not in negation normal form.
2140
*)
2141
let rec hc_formula hcF f =
2142
  match f with
2143
  | TRUE -> HcFormula.hashcons hcF HCTRUE
2144
  | FALSE -> HcFormula.hashcons hcF HCFALSE
2145
  | AP s -> HcFormula.hashcons hcF (HCAP s)
2146 508e3c33 Christoph Egger
  | VAR s -> HcFormula.hashcons hcF (HCVAR s)
2147 4fd28192 Thorsten Wißmann
  | NOT (AP s) -> HcFormula.hashcons hcF (HCNOT s)
2148
  | AT (s, f1) ->
2149
      let tf1 = hc_formula hcF f1 in
2150
      HcFormula.hashcons hcF (HCAT (s, tf1))
2151
  | OR (f1, f2) ->
2152
      let tf1 = hc_formula hcF f1 in
2153
      let tf2 = hc_formula hcF f2 in
2154
      HcFormula.hashcons hcF (HCOR (tf1, tf2))
2155
  | AND (f1, f2) ->
2156
      let tf1 = hc_formula hcF f1 in
2157
      let tf2 = hc_formula hcF f2 in
2158
      HcFormula.hashcons hcF (HCAND (tf1, tf2))
2159
  | NOT _
2160
  | EQU _
2161 af276a36 Thorsten Wißmann
  | MIN _
2162
  | MAX _
2163 4fd28192 Thorsten Wißmann
  | IMP _ -> raise (CoAlgException "Formula is not in negation normal form.")
2164
  | EX (s, f1) ->
2165
      let tf1 = hc_formula hcF f1 in
2166
      HcFormula.hashcons hcF (HCEX (s, tf1))
2167
  | AX (s, f1) ->
2168
      let tf1 = hc_formula hcF f1 in
2169
      HcFormula.hashcons hcF (HCAX (s, tf1))
2170 f1fa9ad5 Thorsten Wißmann
  | ENFORCES (s, f1) ->
2171
      let tf1 = hc_formula hcF f1 in
2172
      HcFormula.hashcons hcF (HCENFORCES (s, tf1))
2173
  | ALLOWS (s, f1) ->
2174
      let tf1 = hc_formula hcF f1 in
2175
      HcFormula.hashcons hcF (HCALLOWS (s, tf1))
2176 af276a36 Thorsten Wißmann
  | MORETHAN  (n, s, f1) ->
2177 4fd28192 Thorsten Wißmann
      let tf1 = hc_formula hcF f1 in
2178 af276a36 Thorsten Wißmann
      HcFormula.hashcons hcF (HCMORETHAN (n, s, tf1))
2179
  | MAXEXCEPT  (n, s, f1) ->
2180 4fd28192 Thorsten Wißmann
      let tf1 = hc_formula hcF f1 in
2181 af276a36 Thorsten Wißmann
      HcFormula.hashcons hcF (HCMAXEXCEPT (n, s, tf1))
2182 86b07be8 Thorsten Wißmann
  | ATLEASTPROB (p, f1) ->
2183
      HcFormula.hashcons hcF (HCATLEASTPROB (p, hc_formula hcF f1))
2184 9bae2c4f Thorsten Wißmann
  | LESSPROBFAIL (p, f1) ->
2185
      HcFormula.hashcons hcF (HCLESSPROBFAIL (p, hc_formula hcF f1))
2186 c49eea11 Thorsten Wißmann
  | CONST s ->
2187
      HcFormula.hashcons hcF (HCCONST s)
2188
  | CONSTN s ->
2189
      HcFormula.hashcons hcF (HCCONSTN s)
2190 19f5dad0 Dirk Pattinson
  | ID f1 ->
2191
    let tf1 = hc_formula hcF f1 in
2192
      HcFormula.hashcons hcF (HCID tf1)
2193
  | NORM (f1, f2) ->
2194
      let tf1 = hc_formula hcF f1 in
2195
      let tf2 = hc_formula hcF f2 in
2196
      HcFormula.hashcons hcF (HCNORM (tf1, tf2))
2197
  | NORMN (f1, f2) ->
2198
      let tf1 = hc_formula hcF f1 in
2199
      let tf2 = hc_formula hcF f2 in
2200
      HcFormula.hashcons hcF (HCNORMN (tf1, tf2))
2201 4fd28192 Thorsten Wißmann
  | CHC (f1, f2) ->
2202
      let tf1 = hc_formula hcF f1 in
2203
      let tf2 = hc_formula hcF f2 in
2204
      HcFormula.hashcons hcF (HCCHC (tf1, tf2))
2205
  | FUS (first, f1) ->
2206
      let tf1 = hc_formula hcF f1 in
2207
      HcFormula.hashcons hcF (HCFUS (first, tf1))
2208 508e3c33 Christoph Egger
  | MU (var, f1) ->
2209 c5c25acf Christoph Egger
     let tf1 = hc_formula hcF f1 in
2210
     HcFormula.hashcons hcF (HCMU (var, tf1))
2211 508e3c33 Christoph Egger
  | NU (var, f1) ->
2212 c5c25acf Christoph Egger
     let tf1 = hc_formula hcF f1 in
2213
     HcFormula.hashcons hcF (HCNU (var, tf1))
2214 97d73a78 Christoph Egger
  | AF _ | EF _
2215
  | AG _ | EG _
2216
  | AU _ | EU _
2217
  | AR _ | ER _
2218
  | AB _ | EB _ ->
2219 c5c25acf Christoph Egger
     raise (CoAlgException ("nnf: CTL should have been removed at this point"))
2220 4fd28192 Thorsten Wißmann
2221 cc07e93d Christoph Egger
(* Replace the Variable name in f with formula formula
2222
   hc_replace foo φ ψ => ψ[foo |-> φ]
2223
 *)
2224
let rec hc_replace hcF name (formula: hcFormula) (f: hcFormula) =
2225
  let func = hc_replace hcF name formula in
2226
  let gennew = HcFormula.hashcons hcF in
2227
  match f.HC.node with
2228
  | HCTRUE
2229
  | HCFALSE
2230
  | HCAP _
2231
  | HCNOT _
2232
  | HCCONST _
2233
  | HCCONSTN _ -> f
2234
  | HCVAR s ->
2235 c5c25acf Christoph Egger
     if compare s name == 0
2236
     then formula
2237
     else f
2238 cc07e93d Christoph Egger
  | HCAT (s, f1) ->
2239 c5c25acf Christoph Egger
     let nf1 = func f1 in
2240
     if nf1 == f1 then f else gennew (HCAT(s, nf1))
2241 cc07e93d Christoph Egger
  | HCOR (f1, f2) ->
2242 c5c25acf Christoph Egger
     let nf1 = func f1 in
2243
     let nf2 = func f2 in
2244
     if nf1 == f1 && nf2 == f2 then f else gennew (HCOR(nf1, nf2))
2245 cc07e93d Christoph Egger
  | HCAND (f1, f2) ->
2246 c5c25acf Christoph Egger
     let nf1 = func f1 in
2247
     let nf2 = func f2 in
2248
     if nf1 == f1 && nf2 == f2 then f else gennew (HCAND(nf1, nf2))
2249 cc07e93d Christoph Egger
  | HCEX (s, f1) ->
2250 c5c25acf Christoph Egger
     let nf1 = func f1 in
2251
     if nf1 == f1 then f else gennew (HCEX(s, nf1))
2252 cc07e93d Christoph Egger
  | HCAX (s, f1) ->
2253
     let nf1 = func f1 in
2254 c5c25acf Christoph Egger
     if nf1 == f1 then f else gennew (HCAX(s, nf1))
2255 cc07e93d Christoph Egger
  | HCENFORCES (s, f1) ->
2256 c5c25acf Christoph Egger
     let nf1 = func f1 in
2257
     if nf1 == f1 then f else gennew (HCENFORCES(s, nf1))
2258 cc07e93d Christoph Egger
  | HCALLOWS (s, f1) ->
2259
     let nf1 = func f1 in
2260 c5c25acf Christoph Egger
     if nf1 == f1 then f else gennew (HCALLOWS(s, nf1))
2261 cc07e93d Christoph Egger
  | HCMORETHAN  (n, s, f1) ->
2262
     let nf1 = func f1 in
2263 c5c25acf Christoph Egger
     if nf1 == f1 then f else gennew (HCMORETHAN(n, s, nf1))
2264 cc07e93d Christoph Egger
  | HCMAXEXCEPT  (n, s, f1) ->
2265 c5c25acf Christoph Egger
     let nf1 = func f1 in
2266
     if nf1 == f1 then f else gennew (HCMAXEXCEPT(n, s, nf1))
2267 cc07e93d Christoph Egger
  | HCATLEASTPROB (p, f1) ->
2268
     let nf1 = func f1 in
2269 c5c25acf Christoph Egger
     if nf1 == f1 then f else gennew (HCATLEASTPROB(p, nf1))
2270 cc07e93d Christoph Egger
  | HCLESSPROBFAIL (p, f1) ->
2271
     let nf1 = func f1 in
2272 c5c25acf Christoph Egger
     if nf1 == f1 then f else gennew (HCLESSPROBFAIL(p, nf1))
2273 cc07e93d Christoph Egger
  | HCID f1 ->
2274
     let nf1 = func f1 in
2275 c5c25acf Christoph Egger
     if nf1 == f1 then f else gennew (HCID(nf1))
2276 cc07e93d Christoph Egger
  | HCNORM (f1, f2) ->
2277 c5c25acf Christoph Egger
     let nf1 = func f1 in
2278
     let nf2 = func f2 in
2279
     if nf1 == f1 && nf2 == f2 then f else gennew (HCNORM(nf1, nf2))
2280 cc07e93d Christoph Egger
  | HCNORMN (f1, f2) ->
2281 c5c25acf Christoph Egger
     let nf1 = func f1 in
2282
     let nf2 = func f2 in
2283
     if nf1 == f1 && nf2 == f2 then f else gennew (HCNORMN(nf1, nf2))
2284 cc07e93d Christoph Egger
  | HCCHC (f1, f2) ->
2285 c5c25acf Christoph Egger
     let nf1 = func f1 in
2286
     let nf2 = func f2 in
2287
     if nf1 == f1 && nf2 == f2 then f else gennew (HCCHC(nf1, nf2))
2288 cc07e93d Christoph Egger
  | HCFUS (first, f1) ->
2289
     let nf1 = func f1 in
2290 c5c25acf Christoph Egger
     if nf1 == f1 then f else gennew (HCFUS(first, nf1))
2291 cc07e93d Christoph Egger
  | HCMU (var, f1) ->
2292 c5c25acf Christoph Egger
     if compare var name != 0 then
2293 854e1338 Christoph Egger
       let nf1 = func f1 in
2294 c5c25acf Christoph Egger
       if nf1 == f1 then f else gennew (HCMU(var, nf1))
2295
     else
2296
       f
2297 cc07e93d Christoph Egger
  | HCNU (var, f1) ->
2298 c5c25acf Christoph Egger
     if compare var name != 0 then
2299 854e1338 Christoph Egger
       let nf1 = func f1 in
2300 c5c25acf Christoph Egger
       if nf1 == f1 then f else gennew (HCNU(var, nf1))
2301
     else
2302
       f
2303 cc07e93d Christoph Egger
2304 5e7c8aa1 Christoph Egger
let rec hc_freeIn variable (f: hcFormula) =
2305
  match f.HC.node with
2306
  | HCTRUE
2307
  | HCFALSE
2308
  | HCAP _
2309
  | HCNOT _
2310
  | HCCONST _
2311
  | HCCONSTN _ -> false
2312
  | HCVAR s ->
2313
     if compare variable s == 0
2314
     then true
2315
     else false
2316
  | HCAT (s, f1) ->
2317
     hc_freeIn variable f1
2318
  | HCOR (f1, f2)
2319
  | HCAND (f1, f2) ->
2320
     hc_freeIn variable f1 || hc_freeIn variable f2
2321
  | HCEX (_, f1)
2322
  | HCAX (_, f1)
2323
  | HCENFORCES (_, f1)
2324
  | HCALLOWS (_, f1)
2325
  | HCMORETHAN  (_, _, f1)
2326
  | HCMAXEXCEPT  (_, _, f1)
2327
  | HCATLEASTPROB (_, f1)
2328
  | HCLESSPROBFAIL (_, f1)
2329
  | HCID f1 ->
2330
     hc_freeIn variable f1
2331
  | HCNORM (f1, f2)
2332
  | HCNORMN (f1, f2)
2333
  | HCCHC (f1, f2) ->
2334
     hc_freeIn variable f1 || hc_freeIn variable f2
2335
  | HCFUS (first, f1) ->
2336
     hc_freeIn variable f1
2337
  | HCMU (var, f1)
2338
  | HCNU (var, f1) ->
2339
     (* Do we need to exclude bound variables here? *)
2340
     hc_freeIn variable f1
2341
2342 cc07e93d Christoph Egger
2343 4fd28192 Thorsten Wißmann
(** An instantiation of a hash table (of the standard library)
2344
    for hash-consed formulae. The test for equality
2345
    and computing the hash value is done in constant time.
2346
 *)
2347
module HcFHt = Hashtbl.Make(
2348
  struct
2349
    type t = hcFormula
2350
    let equal (f1 : t) f2 = f1.HC.tag = f2.HC.tag
2351
    let hash (f : t) = f.HC.tag
2352
  end
2353
 )