Project

General

Profile

Statistics
| Branch: | Revision:

cool / randmu.py @ 7d83cfb6

History | View | Annotate | Download (14.6 KB)

1
#!/usr/bin/python3
2
#
3
# Ideal:
4

    
5
#   Start with a single variable. While formula is still below the
6
#   target size, replace a random variable by a random
7
#   connective. once the target size has been reached, replace all
8
#   unguarded variables by propositional atoms. Replace all remaining
9
#   variables by either an allowed fixpoint variable or a
10
#   propositional atom
11

    
12
import random
13
import string
14
import argparse
15
import os
16

    
17

    
18
variables = []
19
syntax = 'cool'
20

    
21

    
22
def _gensym():
23
    i = 0
24
    while True:
25
        i = i + 1
26
        yield "G%d" % i
27

    
28

    
29
gensym = iter(_gensym())
30

    
31

    
32

    
33
class Connective:
34
    pass
35

    
36

    
37

    
38
class Propositional(Connective):
39
    pass
40

    
41

    
42

    
43
class And(Propositional):
44
    def __init__(self):
45
        self._left = Variable(self)
46
        self._right = Variable(self)
47

    
48

    
49
    def __str__(self):
50
        left = str(self._left)
51
        right = str(self._right)
52
        if syntax == 'tatl':
53
            return "((%s) /\ (%s))" % (left, right)
54
        else:
55
            return "((%s) & (%s))" % (left, right)
56

    
57

    
58
    def replace(self, what, withw):
59
        if what == self._left:
60
            self._left = withw
61
        else:
62
            assert self._right == what
63
            self._right = withw
64

    
65

    
66
    def finalize(self, atoms, guarded, unguarded, fixpoint):
67
        self._left.finalize(atoms, guarded, unguarded, fixpoint)
68
        self._right.finalize(atoms, guarded, unguarded, fixpoint)
69

    
70

    
71

    
72
class Or(Propositional):
73
    def __init__(self):
74
        self._left = Variable(self)
75
        self._right = Variable(self)
76

    
77

    
78
    def __str__(self):
79
        left = str(self._left)
80
        right = str(self._right)
81
        if syntax == 'tatl':
82
            return "((%s) \/ (%s))" % (left, right)
83
        else:
84
            return "((%s) | (%s))" % (left, right)
85

    
86

    
87
    def replace(self, what, withw):
88
        if what == self._left:
89
            self._left = withw
90
        else:
91
            assert self._right == what
92
            self._right = withw
93

    
94

    
95
    def finalize(self, atoms, guarded, unguarded, fixpoint):
96
        self._left.finalize(atoms, guarded, unguarded, fixpoint)
97
        self._right.finalize(atoms, guarded, unguarded, fixpoint)
98

    
99

    
100

    
101
class Modal(Connective):
102
    pass
103

    
104

    
105
class Box(Modal):
106
    def __init__(self):
107
        self._subformula = Variable(self)
108

    
109

    
110
    def __str__(self):
111
        subformula = str(self._subformula)
112
        if syntax == 'ctl':
113
            return "AX (%s)" % (subformula,)
114
        else:
115
            return "[] (%s)" % (subformula,)
116

    
117

    
118
    def replace(self, what, withw):
119
        assert self._subformula == what
120
        self._subformula = withw
121

    
122

    
123
    def finalize(self, atoms, guarded, unguarded, fixpoint):
124
        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
125

    
126

    
127

    
128
class Diamond(Modal):
129
    def __init__(self):
130
        self._subformula = Variable(self)
131

    
132

    
133
    def __str__(self):
134
        subformula = str(self._subformula)
135
        if syntax == 'ctl':
136
            return "EX (%s)" % (subformula,)
137
        else:
138
            return "<> (%s)" % (subformula,)
139

    
140

    
141
    def replace(self, what, withw):
142
        assert self._subformula == what
143
        self._subformula = withw
144

    
145

    
146
    def finalize(self, atoms, guarded, unguarded, fixpoint):
147
        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
148

    
149

    
150

    
151
class Fixpoint(Connective):
152
    pass
153

    
154
class Mu(Fixpoint):
155
    def __init__(self):
156
        self._subformula = Variable(self)
157
        self._var = next(gensym)
158

    
159

    
160
    def __str__(self):
161
        subformula = str(self._subformula)
162
        if syntax == 'cool':
163
            return "(μ %s . (%s))" % (self._var, subformula)
164
        else:
165
            return "(mu %s . (%s))" % (self._var, subformula)
166

    
167

    
168
    def replace(self, what, withw):
169
        assert self._subformula == what
170
        self._subformula = withw
171

    
172

    
173
    def finalize(self, atoms, guarded, unguarded, fixpoint):
174
        if fixpoint == 'nu':
175
            guarded = []
176
            unguarded = []
177

    
178
        self._subformula.finalize(atoms, guarded, unguarded + [self._var], 'mu')
179

    
180

    
181

    
182
class Nu(Fixpoint):
183
    def __init__(self):
184
        self._subformula = Variable(self)
185
        self._var = next(gensym)
186

    
187

    
188
    def __str__(self):
189
        subformula = str(self._subformula)
190
        if syntax == 'cool':
191
            return "(ν %s . (%s))" % (self._var, subformula)
192
        else:
193
            return "(nu %s . (%s))" % (self._var, subformula)
194

    
195

    
196
    def replace(self, what, withw):
197
        assert self._subformula == what
198
        self._subformula = withw
199

    
200

    
201
    def finalize(self, atoms, guarded, unguarded, fixpoint):
202
        if fixpoint == 'mu':
203
            guarded = []
204
            unguarded = []
205

    
206
        self._subformula.finalize(atoms, guarded, unguarded + [self._var], 'nu')
207

    
208

    
209

    
210
class CTL(Connective):
211
    pass
212

    
213

    
214

    
215
class AG(CTL):
216
    def __init__(self):
217
        self._subformula = Variable(self)
218

    
219

    
220
    def __str__(self):
221
        subformula = str(self._subformula)
222
        return "AG (%s)" % (subformula,)
223

    
224

    
225
    def replace(self, what, withw):
226
        assert self._subformula == what
227
        self._subformula = withw
228

    
229

    
230
    def finalize(self, atoms, guarded, unguarded, fixpoint):
231
        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
232

    
233

    
234

    
235
class AF(CTL):
236
    def __init__(self):
237
        self._subformula = Variable(self)
238

    
239

    
240
    def __str__(self):
241
        subformula = str(self._subformula)
242
        return "AF (%s)" % (subformula,)
243

    
244

    
245
    def replace(self, what, withw):
246
        assert self._subformula == what
247
        self._subformula = withw
248

    
249

    
250
    def finalize(self, atoms, guarded, unguarded, fixpoint):
251
        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
252

    
253

    
254

    
255
class EG(CTL):
256
    def __init__(self):
257
        self._subformula = Variable(self)
258

    
259

    
260
    def __str__(self):
261
        subformula = str(self._subformula)
262
        return "EG (%s)" % (subformula,)
263

    
264

    
265
    def replace(self, what, withw):
266
        assert self._subformula == what
267
        self._subformula = withw
268

    
269

    
270
    def finalize(self, atoms, guarded, unguarded, fixpoint):
271
        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
272

    
273

    
274

    
275
class EF(CTL):
276
    def __init__(self):
277
        self._subformula = Variable(self)
278

    
279

    
280
    def __str__(self):
281
        subformula = str(self._subformula)
282
        return "EF (%s)" % (subformula,)
283

    
284

    
285
    def replace(self, what, withw):
286
        assert self._subformula == what
287
        self._subformula = withw
288

    
289

    
290
    def finalize(self, atoms, guarded, unguarded, fixpoint):
291
        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
292

    
293

    
294

    
295
class AU(CTL):
296
    def __init__(self):
297
        self._left = Variable(self)
298
        self._right = Variable(self)
299

    
300

    
301
    def __str__(self):
302
        left = str(self._left)
303
        right = str(self._right)
304
        return "A((%s) U (%s))" % (left, right)
305

    
306

    
307
    def replace(self, what, withw):
308
        if what == self._left:
309
            self._left = withw
310
        else:
311
            assert self._right == what
312
            self._right = withw
313

    
314

    
315
    def finalize(self, atoms, guarded, unguarded, fixpoint):
316
        self._left.finalize(atoms, guarded, unguarded, fixpoint)
317
        self._right.finalize(atoms, guarded, unguarded, fixpoint)
318

    
319

    
320

    
321
class AR(CTL):
322
    def __init__(self):
323
        self._left = Variable(self)
324
        self._right = Variable(self)
325

    
326

    
327
    def __str__(self):
328
        left = str(self._left)
329
        right = str(self._right)
330
        return "A((%s) R (%s))" % (left, right)
331

    
332

    
333
    def replace(self, what, withw):
334
        if what == self._left:
335
            self._left = withw
336
        else:
337
            assert self._right == what
338
            self._right = withw
339

    
340

    
341
    def finalize(self, atoms, guarded, unguarded, fixpoint):
342
        self._left.finalize(atoms, guarded, unguarded, fixpoint)
343
        self._right.finalize(atoms, guarded, unguarded, fixpoint)
344

    
345

    
346

    
347
class EU(CTL):
348
    def __init__(self):
349
        self._left = Variable(self)
350
        self._right = Variable(self)
351

    
352

    
353
    def __str__(self):
354
        left = str(self._left)
355
        right = str(self._right)
356
        return "E((%s) U (%s))" % (left, right)
357

    
358

    
359
    def replace(self, what, withw):
360
        if what == self._left:
361
            self._left = withw
362
        else:
363
            assert self._right == what
364
            self._right = withw
365

    
366

    
367
    def finalize(self, atoms, guarded, unguarded, fixpoint):
368
        self._left.finalize(atoms, guarded, unguarded, fixpoint)
369
        self._right.finalize(atoms, guarded, unguarded, fixpoint)
370

    
371

    
372

    
373
class ER(CTL):
374
    def __init__(self):
375
        self._left = Variable(self)
376
        self._right = Variable(self)
377

    
378

    
379
    def __str__(self):
380
        left = str(self._left)
381
        right = str(self._right)
382
        return "E((%s) R (%s))" % (left, right)
383

    
384

    
385
    def replace(self, what, withw):
386
        if what == self._left:
387
            self._left = withw
388
        else:
389
            assert self._right == what
390
            self._right = withw
391

    
392

    
393
    def finalize(self, atoms, guarded, unguarded, fixpoint):
394
        self._left.finalize(atoms, guarded, unguarded, fixpoint)
395
        self._right.finalize(atoms, guarded, unguarded, fixpoint)
396

    
397

    
398

    
399
class ATL:
400
    def coalition(self):
401
        return "1,2,3"
402

    
403

    
404

    
405
class Next(ATL):
406
    def __init__(self):
407
        self._subformula = Variable(self)
408

    
409

    
410
    def __str__(self):
411
        subformula = str(self._subformula)
412
        if syntax == 'tatl':
413
            return "<<%s>>X(%s)" % (self.coalition(), subformula,)
414
        else:
415
            return "[{%s}](%s)" % (self.coalition(), subformula,)
416

    
417

    
418
    def replace(self, what, withw):
419
        assert self._subformula == what
420
        self._subformula = withw
421

    
422

    
423
    def finalize(self, atoms, guarded, unguarded, fixpoint):
424
        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
425

    
426

    
427

    
428
class Always(ATL):
429
    def __init__(self):
430
        self._subformula = Variable(self)
431

    
432

    
433
    def __str__(self):
434
        subformula = str(self._subformula)
435
        if syntax == 'tatl':
436
            return "<<%s>>G(%s)" % (self.coalition(), subformula,)
437
        else:
438
            return "(ν X . ((%s) & [{%s}]X))" % (subformula,self.coalition())
439

    
440

    
441
    def replace(self, what, withw):
442
        assert self._subformula == what
443
        self._subformula = withw
444

    
445

    
446
    def finalize(self, atoms, guarded, unguarded, fixpoint):
447
        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
448

    
449

    
450

    
451
class Eventually(ATL):
452
    def __init__(self):
453
        self._subformula = Variable(self)
454

    
455

    
456
    def __str__(self):
457
        subformula = str(self._subformula)
458
        if syntax == 'tatl':
459
            return "<<%s>>F(%s)" % (self.coalition(), subformula,)
460
        else:
461
            return "(μ X . ((%s) | [{%s}]X))" % (subformula, self.coalition())
462

    
463

    
464
    def replace(self, what, withw):
465
        assert self._subformula == what
466
        self._subformula = withw
467

    
468

    
469
    def finalize(self, atoms, guarded, unguarded, fixpoint):
470
        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
471

    
472

    
473

    
474
class Until(ATL):
475
    def __init__(self):
476
        self._left = Variable(self)
477
        self._right = Variable(self)
478

    
479

    
480
    def __str__(self):
481
        left = str(self._left)
482
        right = str(self._right)
483
        if syntax == 'tatl':
484
            return "<<%s>>((%s) U (%s))" % (self.coalition(),left, right)
485
        else:
486
            return "(μ X . ((%s) | ((%s) & [{%s}]X)))" % (right,left,self.coalition())
487

    
488

    
489
    def replace(self, what, withw):
490
        if what == self._left:
491
            self._left = withw
492
        else:
493
            assert self._right == what
494
            self._right = withw
495

    
496

    
497
    def finalize(self, atoms, guarded, unguarded, fixpoint):
498
        self._left.finalize(atoms, guarded, unguarded, fixpoint)
499
        self._right.finalize(atoms, guarded, unguarded, fixpoint)
500

    
501

    
502

    
503
connectives = []
504

    
505

    
506
class Variable:
507
    def __init__(self, parent):
508
        self._parent = parent
509
        variables.append(self)
510

    
511

    
512
    def __str__(self):
513
        return "(undecided)"
514

    
515

    
516
    def replace(self):
517
        assert self._parent != None
518
        replacement = random.choice(connectives)()
519
        variables.remove(self)
520
        self._parent.replace(self, replacement)
521

    
522

    
523
    def finalize(self, atoms, guarded, unguarded, fixpoint):
524
        choice = random.choice(guarded + atoms)
525
        if choice in atoms:
526
            choice = random.choice([choice, "~%s" % choice])
527

    
528
        variables.remove(self)
529
        self._parent.replace(self, choice)
530

    
531

    
532

    
533
def main(args):
534
    global connectives
535
    if args.logic == 'afmu':
536
        connectives = [And, And, Or, Or, Box, Diamond, Mu, Nu]
537
        os.makedirs(os.path.join(args.destdir, 'cool'))
538
        os.makedirs(os.path.join(args.destdir, 'mlsolver'))
539

    
540
    elif args.logic == 'CTL':
541
        connectives = [And, And, Or, Or, Box, Diamond, AF, AG, EF, EG, AU, EU]
542
        os.makedirs(os.path.join(args.destdir, 'ctl'))
543

    
544
    elif args.logic == 'ATL':
545
        connectives = [And, And, Or, Or, Next, Always, Eventually, Until]
546
        os.makedirs(os.path.join(args.destdir, 'cool'))
547
        os.makedirs(os.path.join(args.destdir, 'tatl'))
548

    
549
    for i in range(0, args.count):
550
        global variables
551
        global syntax
552
        variables = []
553
        formula = random.choice(connectives)()
554

    
555
        for _ in range(0, args.constructors):
556
            random.choice(variables).replace()
557

    
558
        formula.finalize(list(string.ascii_lowercase[:args.atoms]), [], [], 'none')
559

    
560
        if args.logic == 'afmu':
561
            with open(os.path.join(args.destdir, 'cool', 'random.%04d.cool' % i), 'w') as f:
562
                syntax = 'cool'
563
                f.write(str(formula))
564

    
565
            with open(os.path.join(args.destdir, 'mlsolver', 'random.%04d.mlsolver' % i), 'w') as f:
566
                syntax = 'mlsolver'
567
                f.write(str(formula))
568

    
569
        elif args.logic == 'CTL':
570
            with open(os.path.join(args.destdir, 'ctl', 'random.%04d.ctl' % i), 'w') as f:
571
                syntax = 'ctl'
572
                f.write(str(formula))
573

    
574
        elif args.logic == 'ATL':
575
            with open(os.path.join(args.destdir, 'cool', 'random.%04d.cool' % i), 'w') as f:
576
                syntax = 'cool'
577
                f.write(str(formula))
578

    
579
            with open(os.path.join(args.destdir, 'tatl', 'random.%04d.tatl' % i), 'w') as f:
580
                syntax = 'tatl'
581
                f.write(str(formula))
582

    
583
    print(args.destdir)
584

    
585
if __name__ == '__main__':
586
    parser = argparse.ArgumentParser(description="Generator for random μ-Calculus-Formulas")
587
    parser.add_argument('--atoms', type=int, required=True,
588
                        help="Number of propositional arguments to use")
589
    parser.add_argument('--constructors', type=int, required=True,
590
                        help="Number of connectives to build")
591
    parser.add_argument('--count', type=int, required=True,
592
                        help="Number of formulas to generate")
593
    parser.add_argument('--destdir', type=str, required=True,
594
                        help="Directory to place created formulas in")
595
    parser.add_argument('--logic', choices=['CTL', 'ATL', 'afmu'], required=True)
596

    
597
    args = parser.parse_args()
598

    
599
    main(args)