Project

General

Profile

Statistics
| Branch: | Revision:

cool / benchmarks / aconjunctive_mu / aconjunctive_mu_generator.ml @ a80babbf

History | View | Annotate | Download (25.8 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
let ag psi = NU("X", const_and psi (box "X"))
450

    
451
let early_init x m =
452
  let conjuncts = List.map (fun i -> (NOT (AP (name x (i-1))))) (iota m)
453
  in ag (const_and
454
           (const_imp (AP ("start" ^ x))
455
              (const_and (AP x) (conjoin conjuncts)))
456
           (const_imp (AP x) (diamond x)))
457

    
458
let rec early_psi n x i = match i with
459
  | 0 -> TRUE                   (* FIXME *)
460
  | _ ->
461
     conjoin
462
       [ const_or (NOT (AP (name x (n-i)))) (box (name x (n-i)))
463
       ; const_or (AP (name x (n-i))) (const_ax "" (NOT (AP (name x (n-i)))))
464
       ; early_psi n x (i-1)
465
       ]
466

    
467
let rec early_c_n n x i = match i with
468
  | 0  -> TRUE                  (* FIXME *)
469
  | _ ->
470
     const_or
471
       (conjoin [ NOT (AP (name x (n-i)))
472
                ; box (name x (n-i))
473
                ; early_psi n x (i-1)])
474
       (conjoin [ (AP (name x (n-i)))
475
                ; const_ax "" (NOT (AP (name x (n-i))))
476
                ; early_c_n n x (i-1) ])
477

    
478
let early_c x n = early_c_n n x n
479

    
480
let pow2 x = 1 lsl x
481

    
482
let bitlist j x = List.map (fun i -> x land (1 lsl (i-1)) <> 0) (iota j)
483

    
484
let early_bin r j i =
485
  conjoin
486
    (List.mapi
487
       (fun i bit -> if bit then (AP (name r i)) else (NOT (AP (name r i))))
488
       (bitlist j i))
489

    
490
let early_theta j =
491
  let n = pow2 j in
492
  let inside i = const_and (early_bin "r" j (i-1)) (diamond (name "X" i)) in
493
  let under_the_fixes = disjoin (List.map inside (iota n)) in
494
  let fix mu x f = if mu then MU(x, f) else NU(x, f) in
495
  let rec wrap fix_lit i f =
496
    if i > n then f
497
    else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f)
498
  in
499
  wrap false 1 under_the_fixes
500
(* let early_theta _ = MU ("Y", (const_or (AP "p") (diamond "Y"))) *)
501

    
502
let early_ac n j k =
503
  conjoin
504
    [ (AP "startp")
505
    ; early_init "p" n
506
    ; early_init "r" k
507
    ; ag (const_and
508
            (const_imp (AP "r") (early_c "r" k))
509
            (const_imp (AP "p") (early_c "p" n)))
510
    ; ag (conjoin
511
            [ const_imp
512
                (conjoin (List.map (fun i -> AP (name "p" (i - 1))) (iota (min j n))))
513
                (const_ex "" (const_and (AP "startr") (early_theta k)))
514
            ; NOT (const_and (AP "p") (AP "r"))
515
            ; const_imp (AP "r") (box "r")
516
            ]
517
        )
518
    ]
519

    
520
let af psi = MU("Y", const_or psi (box "Y"))
521

    
522
let early_caching_ac n j k =
523
  conjoin
524
    [ early_ac n j k
525
    ; (AP "b")
526
    ; early_init "q" n
527
    ; ag (conjoin [ NOT (const_and (AP "p") (AP "q"))
528
                  ; NOT (const_and (AP "q") (AP "r"))
529
                  ; const_imp (AP "q") (early_c "q" n)
530
                  ])
531
    ; ag (const_and (af (AP "b")) (const_imp (AP "b")
532
                                     (conjoin [ diamond "p"
533
                                              ; diamond "startq"
534
                                              ; const_ax "" (NOT (AP "b"))])
535
        ))
536
    ]
537

    
538
exception CTLException of string
539

    
540
(** Converts a formula into a string representation for MLSolver.
541
        @param f A formula.
542
        @return A string representing f for MLSolver.
543
        @raise CTLException If the name of an atomic program
544
        or a propositional variable in f is "tt" or "ff".
545
 *)
546
let exportMLSolver f =
547
  let sb = Buffer.create 3000 in
548
  let rec expML = function
549
    | TRUE -> Buffer.add_string sb "(tt)"
550
    | FALSE -> Buffer.add_string sb "(ff)"
551
    | AP s ->
552
       if s <> "tt" && s <> "ff" then begin
553
           Buffer.add_string sb s;
554
         end
555
       else raise (CTLException "Formula contains ff or tt.")
556
    | VAR s ->
557
       Buffer.add_string sb " ";
558
       Buffer.add_string sb s;
559
       Buffer.add_string sb " "
560
    | NOT f1 ->
561
       Buffer.add_string sb "(!";
562
       expML f1;
563
       Buffer.add_string sb ")"
564
    | EX (_, f1) ->
565
       Buffer.add_string sb "(<>";
566
       expML f1;
567
       Buffer.add_string sb ")"
568
    | AX (_, f1) ->
569
       Buffer.add_string sb "([]";
570
       expML f1;
571
       Buffer.add_string sb ")"
572
    | ID (f1) ->
573
       Buffer.add_string sb "(()";
574
       expML f1;
575
       Buffer.add_string sb ")"
576
    | EF f1 ->
577
       Buffer.add_string sb "(E F";
578
       expML f1;
579
       Buffer.add_string sb ")"
580
    | AF f1 ->
581
       Buffer.add_string sb "(A F";
582
       expML f1;
583
       Buffer.add_string sb ")"
584
    | EG f1 ->
585
       Buffer.add_string sb "(E G";
586
       expML f1;
587
       Buffer.add_string sb ")"
588
    | AG f1 ->
589
       Buffer.add_string sb "(A G";
590
       expML f1;
591
       Buffer.add_string sb ")"
592
    | EQU (f1, f2) ->
593
       Buffer.add_string sb  "(";
594
       expML f1;
595
       Buffer.add_string sb " <==> ";
596
       expML f2;
597
       Buffer.add_string sb ")"
598
    | IMP (f1, f2) ->
599
       Buffer.add_string sb "(";
600
       expML f1;
601
       Buffer.add_string sb " ==> ";
602
       expML f2;
603
       Buffer.add_string sb ")"
604
    | OR (f1, f2) ->
605
       Buffer.add_string sb "(";
606
       expML f1;
607
       Buffer.add_string sb " | ";
608
       expML f2;
609
       Buffer.add_string sb ")"
610
    | AND (f1, f2) ->
611
       Buffer.add_string sb "(";
612
       expML f1;
613
       Buffer.add_string sb " & ";
614
       expML f2;
615
       Buffer.add_string sb ")"
616
    | EU (f1, f2) ->
617
       Buffer.add_string sb "(E (";
618
       expML f1;
619
       Buffer.add_string sb " U ";
620
       expML f2;
621
       Buffer.add_string sb "))"
622
    | AU (f1, f2) ->
623
       Buffer.add_string sb "(A (";
624
       expML f1;
625
       Buffer.add_string sb " U ";
626
       expML f2;
627
       Buffer.add_string sb "))"
628
    | EB (f1, f2) ->
629
       Buffer.add_string sb "(E (";
630
       expML f1;
631
       Buffer.add_string sb " R ";
632
       expML (NOT f2);
633
       Buffer.add_string sb "))"
634
    | AB (f1, f2) ->
635
       Buffer.add_string sb "(A (";
636
       expML f1;
637
       Buffer.add_string sb " R ";
638
       expML (NOT f2);
639
       Buffer.add_string sb "))"
640
    | NU (var, f1) ->
641
       Buffer.add_string sb ("(nu " ^ var ^ ". ");
642
       expML f1;
643
       Buffer.add_string sb ")"
644
    | MU (var, f1) ->
645
       Buffer.add_string sb ("(mu " ^ var ^ ". ");
646
       expML f1;
647
       Buffer.add_string sb ")"
648
    | _ -> raise (CTLException "exportMLSolver: Unsupported formula");
649
  in
650
  expML f;
651
  Buffer.contents sb
652

    
653
let print_usage () =
654
  print_endline ("Usage: " ^ Sys.argv.(0) ^ " SYNTAX FORMULA_FAMILY n");
655
  print_endline "";
656
  print_endline "SYNTAX: Either 'cool' or 'mlsolver'";
657
  print_endline "";
658
  print_endline "FORMULA_FAMILY:";
659
  print_endline "    - linear_dpa_is_nba: linear parity condition is
660
                         nondet. b├╝chi condition [1]; valid";
661
  print_endline "    - linear_dpa_is_nba_neg: same, but negated; unsatisfiable";
662
  print_endline "    - pg_even_odd: parity games are more expressive than even-odd games; valid";
663
  print_endline "    - pg_even_odd_neg: same, but negated; unsatisfiable";
664
  print_endline "    - pg_domgame: parity games are more expressive than dominator games; valid";
665
  print_endline "    - pg_domgame_neg: same, but negated; unsatisfiable";
666
  print_endline "    - enpa_is_enba: transform ex. npa to equivalent ex. nba; valid";
667
  print_endline "    - enpa_is_enba_neg: same, but negated; unsatisfiable";
668
  print_endline "    - enpa_to_enba: ex. npa implies ex. nba
669
                         (left-to-right direction of enpa_is_enba); valid";
670
  print_endline "    - enpa_to_enba_neg: same, but negated; unsatisfiable";
671
  print_endline "    - unpa_is_unba: transform univ. npa to equivalent univ. nba; valid";
672
  print_endline "    - unpa_is_unba_neg: same, but negated; satisfiable";
673
  print_endline "    - unpa_to_unba: univ. npa implies univ. nba
674
                         (left-to-right direction of unpa_is_unba); valid";
675
  print_endline "    - unpa_to_unba_neg: same, but negated; satisfiable";
676
  print_endline "    - unpa_is_unba_dual: dual formulation of unpa_is_unba, with
677
                         odd dominators; valid";
678
  print_endline "    - unpa_is_unba_dual_neg: same, but negated; unsatisfiable";
679
  print_endline "";
680
  print_endline "n: Index of the formula in the family";
681
  print_endline "";
682
  print_endline "[1]: http://files.oliverfriedmann.de/papers/a_solver_for_modal_fixpoint_logics.pdf, page 7"
683

    
684
let () =
685
  if Array.length Sys.argv <> 4 then
686
    print_usage ()
687
  else
688
    let syntax = match Sys.argv.(1) with
689
      | "cool" -> exportFormula
690
      | "mlsolver" -> exportMLSolver
691
      | _ -> print_usage (); exit 1
692
    in
693
    let family = match Sys.argv.(2) with
694
      | "linear_dpa_is_nba" -> linear_dpa_is_nba
695
      | "linear_dpa_is_nba_neg" -> neg_linear_dpa_is_nba
696
      | "enpa_is_enba" -> enpa_is_enba
697
      | "enpa_is_enba_neg" -> neg_enpa_is_enba
698
      | "enpa_to_enba" -> enpa_to_enba
699
      | "enpa_to_enba_neg" -> neg_enpa_to_enba
700
      | "unpa_is_unba" -> unpa_is_unba
701
      | "unpa_is_unba_neg" -> neg_unpa_is_unba
702
      | "unpa_to_unba" -> unpa_to_unba
703
      | "unpa_to_unba_neg" -> neg_unpa_to_unba
704
      | "unpa_is_unba_dual" -> unpa_is_unba_dual
705
      | "unpa_is_unba_dual_neg" -> neg_unpa_is_unba_dual
706
      | "pg_even_odd" -> pg_even_odd
707
      | "pg_even_odd_neg" -> neg_pg_even_odd
708
      | "pg_domgame" -> pg_domgame
709
      | "pg_domgame_neg" -> neg_pg_domgame
710
      | "early_ac" -> fun i -> early_ac i 4 2
711
      | "early_caching_ac" -> fun i -> early_caching_ac i 4 2
712
      | _ -> print_usage (); exit 1
713
    in
714
    let n = int_of_string Sys.argv.(3) in
715
    print_endline (syntax (family n));