Project

General

Profile

Statistics
| Branch: | Revision:

cool / gen.ml @ 77f7da85

History | View | Annotate | Download (22.9 KB)

1
open CoAlgFormula
2

    
3
(* Generates hard aconjunctive mu-calculus formulas with deep
4
nesting of fixpoints *)
5

    
6
let iota n =
7
  let rec intern i n =
8
    if i = n then [i]
9
    else i::intern (i+1) n
10
  in
11
  intern 1 n
12

    
13
let name n i = n ^ string_of_int i
14

    
15
(* Join a list of formulas with OR *)
16
let disjoin list = match list with
17
  | [] -> FALSE
18
  | h :: tl -> List.fold_left const_or h tl
19

    
20
(* Join a list of formulas with AND *)
21
let conjoin list = match list with
22
  | [] -> TRUE
23
  | h :: tl -> List.fold_left const_and h tl
24

    
25
let box name = const_ax "" (VAR name)
26
let diamond name = const_ex "" (VAR name)
27
let circle name = (ID (VAR name))
28

    
29
let psi n =
30
  let inside i =
31
    let not_qis =
32
      List.map (fun j -> (NOT (AP (name "q" j))))
33
               (List.filter (fun x -> x <> i) (iota n))
34
    in
35
    (const_and (AP (name "q" i)) (conjoin not_qis))
36
  in
37

    
38
  (NU("X",const_and (circle "X") (disjoin (List.map inside (iota n)))))
39

    
40
let psi_neg n =
41
  let inside i =
42
    let qis =
43
      List.map (fun j -> (AP (name "q" j)))
44
               (List.filter (fun x -> x <> i) (iota n))
45
    in
46
    disjoin (NOT (AP (name "q" i)) :: qis)
47
  in
48

    
49
  (MU("X", const_or (circle "X") (conjoin (List.map inside (iota n)))))
50

    
51
let before_biimpl_neg n =
52
  let inside i = const_and (AP (name "q" i)) (circle (name "X" i)) in
53
  let under_the_fixes = disjoin (List.map inside (iota n)) in
54
  let fix mu x f = if mu then MU(x, f) else NU(x, f) in
55
  let rec wrap fix_lit i f =
56
    if i > n then f
57
    else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f)
58
  in
59
  wrap false 1 under_the_fixes
60

    
61
let before_biimpl n =
62
  let inside i = const_and (AP (name "q" i)) (circle (name "X" i)) in
63
  let under_the_fixes = disjoin (List.map inside (iota n)) in
64
  let fix mu x f = if mu then MU(x, f) else NU(x, f) in
65
  let rec wrap fix_lit i f =
66
    if i > n then f
67
    else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f)
68
  in
69
  wrap true 1 under_the_fixes
70

    
71
let isEven i = i mod 2 = 0
72
let isOdd i = i mod 2 = 1
73

    
74
let after_biimpl n =
75
  let conjunct j =
76
    (MU("X", const_or (NU("Y", const_and (NOT (AP (name "q" j))) (circle "Y")))
77
                      (circle "X")))
78
  in
79
   let disjunct i =
80
     let conjuncts =
81
       List.map conjunct (List.filter (fun j -> j > i && isOdd j) (iota n))
82
     in
83
     let inside =
84
       (NU("X", const_and (MU("Y", const_or (AP (name "q" i)) (circle "Y")))
85
                          (circle "X")))
86
     in
87
     (const_and inside (conjoin conjuncts))
88
   in
89
   let disjuncts = List.map disjunct (List.filter isEven (iota n)) in
90
   disjoin disjuncts
91

    
92
let after_biimpl_neg n =
93
  let disjunct j =
94
    (NU("X",
95
        const_and
96
          (MU("Y", const_or (AP (name "q" j)) (circle "Y")))
97
          (circle "X")))
98
  in
99
   let conjunct i =
100
     let disjuncts =
101
       List.map disjunct (List.filter (fun j -> j > i && isOdd j) (iota n))
102
     in
103
     let inside =
104
       (MU("X",
105
           const_or
106
             (NU("Y", const_and (NOT (AP (name "q" i))) (circle "Y")))
107
             (circle "X")))
108
     in
109
     (const_or inside (disjoin disjuncts))
110
   in
111
   let conjuncts = List.map conjunct (List.filter isEven (iota n)) in
112
   conjoin conjuncts
113

    
114
let linear_dpa_is_nba n =
115
  const_or
116
    (psi_neg n)
117
    (const_and
118
       (const_or (before_biimpl_neg n) (after_biimpl n))
119
       (const_or (before_biimpl n) (after_biimpl_neg n)))
120

    
121
let neg_linear_dpa_is_nba n =
122
  const_and (psi n)
123
            (const_or (const_and (before_biimpl n) (after_biimpl_neg n))
124
                      (const_and (before_biimpl_neg n) (after_biimpl n)))
125

    
126
let psi2 n =
127
  let inside i =
128
    let not_qis =
129
      List.map (fun j -> (NOT (AP (name "q" j))))
130
               (List.filter (fun x -> x <> i) (iota n))
131
    in
132
    (const_and (AP (name "q" i)) (conjoin not_qis))
133
  in
134

    
135
  (const_and (NU("X",const_and (box "X") (disjoin (List.map inside (iota n)))))
136
             (NU("X",const_and (box "X") (const_or (const_and (NOT (AP (name "q" (n+2))))
137
                (AP (name "q" (n+1)))) (const_and (NOT (AP (name "q" (n+1)))) (AP (name "q" (n+2))))))))
138

    
139
let psi_neg2 n =
140
  let inside i =
141
    let qis =
142
      List.map (fun j -> (AP (name "q" j)))
143
               (List.filter (fun x -> x <> i) (iota n))
144
    in
145
    disjoin (NOT (AP (name "q" i)) :: qis)
146
  in
147

    
148
  (const_or (MU("X",const_or (diamond "X") (conjoin (List.map inside (iota n)))))
149
            (MU("X",const_or (diamond "X") (const_and (const_or (NOT (AP (name "q" (n+1))))
150
               (AP (name "q" (n+2)))) (const_or (NOT (AP (name "q" (n+2)))) (AP (name "q" (n+1))))))))
151

    
152
let pgwin n =
153
  let inside_e i = const_and (AP (name "q" i)) (diamond (name "X" i)) in
154
  let inside_a i = const_and (AP (name "q" i)) (box (name "X" i)) in
155
  let under_the_fixes = (const_or (const_and ((AP (name "q" (n+2)))) (disjoin (List.map inside_e (iota n))))
156
                                  (const_and ((AP (name "q" (n+1)))) (disjoin (List.map inside_a (iota n))))) in
157
  let fix mu x f = if mu then MU(x, f) else NU(x, f) in
158
  let rec wrap fix_lit i f =
159
    if i > n then f
160
    else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f)
161
  in
162
  wrap true 1 under_the_fixes
163

    
164
let pglose n =
165
  let inside_e i = const_and (AP (name "q" i)) (box (name "X" i)) in
166
  let inside_a i = const_and (AP (name "q" i)) (diamond (name "X" i)) in
167
  let under_the_fixes = (const_or (const_and ((AP (name "q" (n+2)))) (disjoin (List.map inside_e (iota n))))
168
                                  (const_and ((AP (name "q" (n+1)))) (disjoin (List.map inside_a (iota n))))) in
169
  let fix mu x f = if mu then MU(x, f) else NU(x, f) in
170
  let rec wrap fix_lit i f =
171
    if i > n then f
172
    else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f)
173
  in
174
  wrap false 1 under_the_fixes
175

    
176
let egwin n =
177
   let disjunct_ee i = const_and (AP (name "q" i)) (diamond "X") in
178
   let disjunct_eo i = const_and (AP (name "q" i)) (diamond "Y") in
179
   let disjunct_ae i = const_and (AP (name "q" i)) (box "X") in
180
   let disjunct_ao i = const_and (AP (name "q" i)) (box "Y") in
181
   let disjuncts_ee = List.map disjunct_ee (List.filter isEven (iota n)) in
182
   let disjuncts_eo = List.map disjunct_eo (List.filter isOdd (iota n)) in
183
   let disjuncts_ae = List.map disjunct_ae (List.filter isEven (iota n)) in
184
   let disjuncts_ao = List.map disjunct_ao (List.filter isOdd (iota n)) in
185

    
186
   (NU("X",MU("Y",const_or (const_and ((AP (name "q" (n+2)))) (const_or (disjoin disjuncts_ee) (disjoin disjuncts_eo) ))
187
                           (const_and ((AP (name "q" (n+1)))) (const_or (disjoin disjuncts_ae) (disjoin disjuncts_ao) )) )))
188

    
189
let eglose n =
190
   let disjunct_ee i = const_and (AP (name "q" i)) (box "X") in
191
   let disjunct_eo i = const_and (AP (name "q" i)) (box "Y") in
192
   let disjunct_ae i = const_and (AP (name "q" i)) (diamond "X") in
193
   let disjunct_ao i = const_and (AP (name "q" i)) (diamond "Y") in
194
   let disjuncts_ee = List.map disjunct_ee (List.filter isEven (iota n)) in
195
   let disjuncts_eo = List.map disjunct_eo (List.filter isOdd (iota n)) in
196
   let disjuncts_ae = List.map disjunct_ae (List.filter isEven (iota n)) in
197
   let disjuncts_ao = List.map disjunct_ao (List.filter isOdd (iota n)) in
198

    
199
   (MU("X",NU("Y",const_or (const_and ((AP (name "q" (n+2)))) (const_or (disjoin disjuncts_ee) (disjoin disjuncts_eo) ))
200
                           (const_and ((AP (name "q" (n+1)))) (const_or (disjoin disjuncts_ae) (disjoin disjuncts_ao) )) )))
201

    
202
let pg_even_odd n =
203
  const_or
204
    (psi_neg2 n)
205
    (const_or
206
       (pglose n)
207
       (egwin n))
208

    
209
let neg_pg_even_odd n =
210
  const_and (psi2 n)
211
            (const_and (pgwin n)
212
                      (eglose n))
213

    
214

    
215
let dgwin n =
216
   let disjunct_eg i = const_and (AP (name "q" i)) (diamond "X") in
217
   let disjunct_el i = const_and (AP (name "q" i)) (diamond "Z") in
218
   let disjunct_ag i = const_and (AP (name "q" i)) (box "X") in
219
   let disjunct_al i = const_and (AP (name "q" i)) (box "Z") in
220
   let disjuncts_eg i = List.map disjunct_eg (List.filter (fun j -> j > i) (iota n)) in
221
   let disjuncts_el i = List.map disjunct_el (List.filter (fun j -> j < i) (iota n)) in
222
   let disjuncts_ag i = List.map disjunct_ag (List.filter (fun j -> j > i) (iota n)) in
223
   let disjuncts_al i = List.map disjunct_al (List.filter (fun j -> j < i) (iota n)) in
224
   let dom_game n i = (NU("X",(MU("Y",NU("Z", (const_or (const_and (AP (name "q" (n+2)))
225
                (const_or (const_and (AP (name "q" i)) (diamond "Y"))
226
                (const_or (disjoin (disjuncts_eg i)) (disjoin
227
(disjuncts_el i))))																	) (const_and (AP (name "q" (n+1))) (const_or (const_and (AP (name "q" i)) (box "Y"))
228
               (const_or (disjoin (disjuncts_ag i)) (disjoin (disjuncts_al i)) ))																				))))))) in
229
   let conjuncts = List.map (dom_game n) (List.filter isOdd (iota n)) in
230

    
231
   conjoin conjuncts
232

    
233
let dglose n =
234
   let disjunct_eg i = const_and (AP (name "q" i)) (diamond "X") in
235
   let disjunct_el i = const_and (AP (name "q" i)) (diamond "Z") in
236
   let disjunct_ag i = const_and (AP (name "q" i)) (box "X") in
237
   let disjunct_al i = const_and (AP (name "q" i)) (box "Z") in
238
   let disjuncts_eg i = List.map disjunct_eg (List.filter (fun j -> j > i) (iota n)) in
239
   let disjuncts_el i = List.map disjunct_el (List.filter (fun j -> j < i) (iota n)) in
240
   let disjuncts_ag i = List.map disjunct_ag (List.filter (fun j -> j > i) (iota n)) in
241
   let disjuncts_al i = List.map disjunct_al (List.filter (fun j -> j < i) (iota n)) in
242
   let neg_dom_game n i = (MU("X",(NU("Y",MU("Z", (const_or (const_and (AP (name "q" (n+2)))
243
                (const_or (const_and (AP (name "q" i)) (box "Y"))
244
                (const_or (disjoin (disjuncts_ag i)) (disjoin
245
(disjuncts_al i))))																	) (const_and (AP (name "q" (n+1))) (const_or (const_and (AP (name "q" i)) (diamond "Y"))
246
               (const_or (disjoin (disjuncts_eg i)) (disjoin (disjuncts_el i)) ))																				))))))) in
247
   let disjuncts = List.map (neg_dom_game n) (List.filter isOdd (iota n)) in
248

    
249
   disjoin disjuncts
250

    
251
let pg_domgame n =
252
  const_or
253
    (psi_neg2 n)
254
    (const_or
255
       (pglose n)
256
       (dgwin n))
257

    
258
let neg_pg_domgame n =
259
  const_and (psi2 n)
260
            (const_and (pgwin n)
261
                      (dglose n))
262

    
263

    
264
let psi3 n =
265
  let inside i =
266
    let not_qis =
267
      List.map (fun j -> (NOT (AP (name "q" j))))
268
               (List.filter (fun x -> x <> i) (iota n))
269
    in
270
    (const_and (AP (name "q" i)) (conjoin not_qis))
271
  in
272

    
273
  (NU("X",const_and (box "X") (disjoin (List.map inside (iota n)))))
274

    
275
let psi_neg3 n =
276
  let inside i =
277
    let qis =
278
      List.map (fun j -> (AP (name "q" j)))
279
               (List.filter (fun x -> x <> i) (iota n))
280
    in
281
    disjoin (NOT (AP (name "q" i)) :: qis)
282
  in
283

    
284
  (MU("X",const_or (diamond "X") (conjoin (List.map inside (iota n)))))
285

    
286
let epa_acc n =
287
  let inside_e i = const_and (AP (name "q" i)) (diamond (name "X" i)) in
288
  let under_the_fixes = disjoin (List.map inside_e (iota n)) in
289
  let fix mu x f = if mu then MU(x, f) else NU(x, f) in
290
  let rec wrap fix_lit i f =
291
    if i > n then f
292
    else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f)
293
  in
294
  wrap true 1 under_the_fixes
295

    
296
let epa_nacc n =
297
  let inside_a i = const_and (AP (name "q" i)) (box (name "X" i)) in
298
  let under_the_fixes = disjoin (List.map inside_a (iota n)) in
299
  let fix mu x f = if mu then MU(x, f) else NU(x, f) in
300
  let rec wrap fix_lit i f =
301
    if i > n then f
302
    else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f)
303
  in
304
  wrap false 1 under_the_fixes
305

    
306
let enba_acc n =
307
   let disjunct_eg i = const_and (AP (name "q" i)) (diamond "X") in
308
   let disjunct_el i = const_and (AP (name "q" i)) (diamond "Z") in
309
   let disjuncts_eg i = List.map disjunct_eg (List.filter (fun j -> j > i) (iota n)) in
310
   let disjuncts_el i = List.map disjunct_el (List.filter (fun j -> j < i) (iota n)) in
311
   let dom_aut i = (MU("X",(NU("Y",MU("Z", (const_or (const_and (AP (name "q" i)) (diamond "Y"))
312
                                           (const_or (disjoin (disjuncts_eg i)) (disjoin (disjuncts_el i)) )) ))))) in
313
   let disjuncts = List.map dom_aut (List.filter isEven (iota n)) in
314

    
315
   disjoin disjuncts
316

    
317
let enba_nacc n =
318
   let disjunct_ag i = const_and (AP (name "q" i)) (box "X") in
319
   let disjunct_al i = const_and (AP (name "q" i)) (box "Z") in
320
   let disjuncts_ag i = List.map disjunct_ag (List.filter (fun j -> j > i) (iota n)) in
321
   let disjuncts_al i = List.map disjunct_al (List.filter (fun j -> j < i) (iota n)) in
322
   let neg_dom_aut i = (NU("X",(MU("Y",NU("Z", (const_or (const_and (AP (name "q" i)) (box "Y")) (const_or (disjoin (disjuncts_ag i)) (disjoin (disjuncts_al i)) )) ))))) in
323
   let conjuncts = List.map neg_dom_aut (List.filter isEven (iota n)) in
324

    
325
   conjoin conjuncts
326

    
327
let enpa_is_enba n =
328
  const_or
329
    (psi_neg3 n)
330
    (const_and
331
       (const_or (epa_nacc n) (enba_acc n))
332
       (const_or (epa_acc n) (enba_nacc n)))
333

    
334
let neg_enpa_is_enba n =
335
  const_and (psi3 n)
336
            (const_or (const_and (epa_acc n) (enba_nacc n))
337
                      (const_and (epa_nacc n) (enba_acc n)))
338

    
339
let enpa_to_enba n =
340
  const_or
341
    (psi_neg3 n)
342
    (const_or
343
       (epa_nacc n)
344
       (enba_acc n))
345

    
346
let neg_enpa_to_enba n =
347
  const_and (psi3 n)
348
            (const_and (epa_acc n)
349
                      (enba_nacc n))
350

    
351
let upa_acc n =
352
  let inside_a i = const_and (AP (name "q" i)) (box (name "X" i)) in
353
  let under_the_fixes = disjoin (List.map inside_a (iota n)) in
354
  let fix mu x f = if mu then MU(x, f) else NU(x, f) in
355
  let rec wrap fix_lit i f =
356
    if i > n then f
357
    else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f)
358
  in
359
  wrap true 1 under_the_fixes
360

    
361
let upa_nacc n =
362
  let inside_e i = const_and (AP (name "q" i)) (diamond (name "X" i)) in
363
  let under_the_fixes = disjoin (List.map inside_e (iota n)) in
364
  let fix mu x f = if mu then MU(x, f) else NU(x, f) in
365
  let rec wrap fix_lit i f =
366
    if i > n then f
367
    else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f)
368
  in
369
  wrap false 1 under_the_fixes
370

    
371
let unba_acc n =
372
   let disjunct_ag i = const_and (AP (name "q" i)) (box "X") in
373
   let disjunct_al i = const_and (AP (name "q" i)) (box "Z") in
374
   let disjuncts_ag i = List.map disjunct_ag (List.filter (fun j -> j > i) (iota n)) in
375
   let disjuncts_al i = List.map disjunct_al (List.filter (fun j -> j < i) (iota n)) in
376
   let dom_aut i = (MU("X",(NU("Y",MU("Z", (const_or (const_and (AP (name "q" i)) (box "Y"))
377
                                           (const_or (disjoin (disjuncts_ag i)) (disjoin (disjuncts_al i)) )) ))))) in
378
   let disjuncts = List.map dom_aut (List.filter isEven (iota n)) in
379

    
380
   disjoin disjuncts
381

    
382
let unba_nacc n =
383
   let disjunct_eg i = const_and (AP (name "q" i)) (diamond "X") in
384
   let disjunct_el i = const_and (AP (name "q" i)) (diamond "Z") in
385
   let disjuncts_eg i = List.map disjunct_eg (List.filter (fun j -> j > i) (iota n)) in
386
   let disjuncts_el i = List.map disjunct_el (List.filter (fun j -> j < i) (iota n)) in
387
   let neg_dom_aut i = (NU("X",(MU("Y",NU("Z", (const_or (const_and (AP (name "q" i)) (diamond "Y")) (const_or (disjoin (disjuncts_eg i)) (disjoin (disjuncts_el i)) )) ))))) in
388
   let conjuncts = List.map neg_dom_aut (List.filter isEven (iota n)) in
389

    
390
   conjoin conjuncts
391

    
392
let unpa_is_unba n =
393
  const_or
394
    (psi_neg3 n)
395
    (const_and
396
       (const_or (upa_nacc n) (unba_acc n))
397
       (const_or (upa_acc n) (unba_nacc n)))
398

    
399
let neg_unpa_is_unba n =
400
  const_and (psi3 n)
401
            (const_or (const_and (upa_acc n) (unba_nacc n))
402
                      (const_and (upa_nacc n) (unba_acc n)))
403

    
404
let unpa_to_unba n =
405
  const_or
406
    (psi_neg3 n)
407
    (const_or
408
       (upa_nacc n)
409
       (unba_acc n))
410

    
411
let neg_unpa_to_unba n =
412
  const_and (psi3 n)
413
            (const_and (upa_acc n)
414
                      (unba_nacc n))
415

    
416
let unba_acc_dual n =
417
   let disjunct_ag i = const_and (AP (name "q" i)) (box "X") in
418
   let disjunct_al i = const_and (AP (name "q" i)) (box "Z") in
419
   let disjuncts_ag i = List.map disjunct_ag (List.filter (fun j -> j > i) (iota n)) in
420
   let disjuncts_al i = List.map disjunct_al (List.filter (fun j -> j < i) (iota n)) in
421
   let dom_aut i = (NU("X",(MU("Y",NU("Z", (const_or (const_and (AP (name "q" i)) (box "Y"))
422
                                           (const_or (disjoin (disjuncts_ag i)) (disjoin (disjuncts_al i)) )) ))))) in
423
   let conjuncts = List.map dom_aut (List.filter isOdd (iota n)) in
424

    
425
   conjoin conjuncts
426

    
427
let unba_nacc_dual n =
428
   let disjunct_eg i = const_and (AP (name "q" i)) (diamond "X") in
429
   let disjunct_el i = const_and (AP (name "q" i)) (diamond "Z") in
430
   let disjuncts_eg i = List.map disjunct_eg (List.filter (fun j -> j > i) (iota n)) in
431
   let disjuncts_el i = List.map disjunct_el (List.filter (fun j -> j < i) (iota n)) in
432
   let neg_dom_aut i = (MU("X",(NU("Y",MU("Z", (const_or (const_and (AP (name "q" i)) (diamond "Y")) (const_or (disjoin (disjuncts_eg i)) (disjoin (disjuncts_el i)) )) ))))) in
433
   let disjuncts = List.map neg_dom_aut (List.filter isOdd (iota n)) in
434

    
435
   disjoin disjuncts
436

    
437
let unpa_is_unba_dual n =
438
  const_or
439
    (psi_neg3 n)
440
    (const_and
441
       (const_or (upa_nacc n) (unba_acc_dual n))
442
       (const_or (upa_acc n) (unba_nacc_dual n)))
443

    
444
let neg_unpa_is_unba_dual n =
445
  const_and (psi3 n)
446
            (const_or (const_and (upa_acc n) (unba_nacc_dual n))
447
                      (const_and (upa_nacc n) (unba_acc_dual n)))
448

    
449

    
450
exception CTLException of string
451

    
452
(** Converts a formula into a string representation for MLSolver.
453
        @param f A formula.
454
        @return A string representing f for MLSolver.
455
        @raise CTLException If the name of an atomic program
456
        or a propositional variable in f is "tt" or "ff".
457
 *)
458
let exportMLSolver f =
459
  let sb = Buffer.create 3000 in
460
  let rec expML = function
461
    | TRUE -> Buffer.add_string sb "(tt)"
462
    | FALSE -> Buffer.add_string sb "(ff)"
463
    | AP s ->
464
       if s <> "tt" && s <> "ff" then begin
465
           Buffer.add_string sb s;
466
         end
467
       else raise (CTLException "Formula contains ff or tt.")
468
    | VAR s ->
469
       Buffer.add_string sb " ";
470
       Buffer.add_string sb s;
471
       Buffer.add_string sb " "
472
    | NOT f1 ->
473
       Buffer.add_string sb "(!";
474
       expML f1;
475
       Buffer.add_string sb ")"
476
    | EX (_, f1) ->
477
       Buffer.add_string sb "(<>";
478
       expML f1;
479
       Buffer.add_string sb ")"
480
    | AX (_, f1) ->
481
       Buffer.add_string sb "([]";
482
       expML f1;
483
       Buffer.add_string sb ")"
484
    | ID (f1) ->
485
       Buffer.add_string sb "(()";
486
       expML f1;
487
       Buffer.add_string sb ")"
488
    | EF f1 ->
489
       Buffer.add_string sb "(E F";
490
       expML f1;
491
       Buffer.add_string sb ")"
492
    | AF f1 ->
493
       Buffer.add_string sb "(A F";
494
       expML f1;
495
       Buffer.add_string sb ")"
496
    | EG f1 ->
497
       Buffer.add_string sb "(E G";
498
       expML f1;
499
       Buffer.add_string sb ")"
500
    | AG f1 ->
501
       Buffer.add_string sb "(A G";
502
       expML f1;
503
       Buffer.add_string sb ")"
504
    | EQU (f1, f2) ->
505
       Buffer.add_string sb  "(";
506
       expML f1;
507
       Buffer.add_string sb " <==> ";
508
       expML f2;
509
       Buffer.add_string sb ")"
510
    | IMP (f1, f2) ->
511
       Buffer.add_string sb "(";
512
       expML f1;
513
       Buffer.add_string sb " ==> ";
514
       expML f2;
515
       Buffer.add_string sb ")"
516
    | OR (f1, f2) ->
517
       Buffer.add_string sb "(";
518
       expML f1;
519
       Buffer.add_string sb " | ";
520
       expML f2;
521
       Buffer.add_string sb ")"
522
    | AND (f1, f2) ->
523
       Buffer.add_string sb "(";
524
       expML f1;
525
       Buffer.add_string sb " & ";
526
       expML f2;
527
       Buffer.add_string sb ")"
528
    | EU (f1, f2) ->
529
       Buffer.add_string sb "(E (";
530
       expML f1;
531
       Buffer.add_string sb " U ";
532
       expML f2;
533
       Buffer.add_string sb "))"
534
    | AU (f1, f2) ->
535
       Buffer.add_string sb "(A (";
536
       expML f1;
537
       Buffer.add_string sb " U ";
538
       expML f2;
539
       Buffer.add_string sb "))"
540
    | EB (f1, f2) ->
541
       Buffer.add_string sb "(E (";
542
       expML f1;
543
       Buffer.add_string sb " R ";
544
       expML (NOT f2);
545
       Buffer.add_string sb "))"
546
    | AB (f1, f2) ->
547
       Buffer.add_string sb "(A (";
548
       expML f1;
549
       Buffer.add_string sb " R ";
550
       expML (NOT f2);
551
       Buffer.add_string sb "))"
552
    | NU (var, f1) ->
553
       Buffer.add_string sb ("(nu " ^ var ^ ". ");
554
       expML f1;
555
       Buffer.add_string sb ")"
556
    | MU (var, f1) ->
557
       Buffer.add_string sb ("(mu " ^ var ^ ". ");
558
       expML f1;
559
       Buffer.add_string sb ")"
560
  in
561
  expML f;
562
  Buffer.contents sb
563

    
564
let print_usage () =
565
  print_endline ("Usage: " ^ Sys.argv.(0) ^ " SYNTAX FORMULA_FAMILY n");
566
  print_endline "";
567
  print_endline "SYNTAX: Either 'cool' or 'mlsolver'";
568
  print_endline "";
569
  print_endline "FORMULA_FAMILY:";
570
  print_endline "    - linear_dpa_is_nba: linear parity condition is
571
                         nondet. b├╝chi condition [1]; valid";
572
  print_endline "    - linear_dpa_is_nba_neg: same, but negated; unsatisfiable";
573
  print_endline "    - pg_even_odd: parity games are more expressive than even-odd games; valid";
574
  print_endline "    - pg_even_odd_neg: same, bug negated; unsatisfiable";
575
  print_endline "    - pg_domgame: parity games are more expressive than dominator games; valid";
576
  print_endline "    - pg_domgame_neg: same, bug negated; unsatisfiable";
577
  print_endline "    - enpa_is_enba: transform ex. npa to equivalent ex. nba; valid";
578
  print_endline "    - enpa_is_enba_neg: same, bug negated; unsatisfiable";
579
  print_endline "    - enpa_to_enba: ex. npa implies ex. nba
580
                         (left-to-right direction of enpa_is_enba); valid";
581
  print_endline "    - enpa_to_enba_neg: same, bug negated; unsatisfiable";
582
  print_endline "    - unpa_is_unba: transform univ. npa to equivalent univ. nba; valid";
583
  print_endline "    - unpa_is_unba_neg: same, bug negated; satisfiable";
584
  print_endline "    - unpa_to_unba: univ. npa implies univ. nba
585
                         (left-to-right direction of unpa_is_unba); valid";
586
  print_endline "    - unpa_to_unba_neg: same, bug negated; satisfiable";
587
  print_endline "    - unpa_is_unba_dual: dual formulation of unpa_is_unba, with
588
                         odd dominators; valid";
589
  print_endline "    - unpa_is_unba_dual_neg: same, bug negated; unsatisfiable";
590
  print_endline "";
591
  print_endline "n: Index of the formula in the family";
592
  print_endline "";
593
  print_endline "[1]: http://files.oliverfriedmann.de/papers/a_solver_for_modal_fixpoint_logics.pdf, page 7"
594

    
595
let () =
596
  if Array.length Sys.argv <> 4 then
597
    print_usage ()
598
  else
599
    let syntax = match Sys.argv.(1) with
600
      | "cool" -> exportFormula
601
      | "mlsolver" -> exportMLSolver
602
      | _ -> print_usage (); exit 1
603
    in
604
    let family = match Sys.argv.(2) with
605
      | "linear_dpa_is_nba" -> linear_dpa_is_nba
606
      | "linear_dpa_is_nba_neg" -> neg_linear_dpa_is_nba
607
      | "enpa_is_enba" -> enpa_is_enba
608
      | "enpa_is_enba_neg" -> neg_enpa_is_enba
609
      | "enpa_to_enba" -> enpa_to_enba
610
      | "enpa_to_enba_neg" -> neg_enpa_to_enba
611
      | "unpa_is_unba" -> unpa_is_unba
612
      | "unpa_is_unba_neg" -> neg_unpa_is_unba
613
      | "unpa_to_unba" -> unpa_to_unba
614
      | "unpa_to_unba_neg" -> neg_unpa_to_unba
615
      | "unpa_is_unba_dual" -> unpa_is_unba_dual
616
      | "unpa_is_unba_dual_neg" -> neg_unpa_is_unba_dual
617
      | "pg_even_odd" -> pg_even_odd
618
      | "pg_even_odd_neg" -> neg_pg_even_odd
619
      | "pg_domgame" -> pg_domgame
620
      | "pg_domgame_neg" -> neg_pg_domgame
621
      | _ -> print_usage (); exit 1
622
    in
623
    let n = int_of_string Sys.argv.(3) in
624
    print_endline (syntax (family n));