Project

General

Profile

Statistics
| Branch: | Revision:

cool / randmu.py @ master

History | View | Annotate | Download (15 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
        if not hasattr(self, '_coalition'):
402
            self._coalition = []
403
            while len(self._coalition) == 0:
404
                self._coalition = []
405
                for i in range(1, 6):
406
                    if random.getrandbits(1) == 1:
407
                        self._coalition.append(str(i))
408

    
409
        if syntax == 'tatl':
410
            return ",".join(self._coalition)
411
        else:
412
            return " ".join(self._coalition)
413

    
414

    
415

    
416
class Next(ATL):
417
    def __init__(self):
418
        self._subformula = Variable(self)
419

    
420

    
421
    def __str__(self):
422
        subformula = str(self._subformula)
423
        if syntax == 'tatl':
424
            return "<<%s>>X(%s)" % (self.coalition(), subformula,)
425
        else:
426
            return "[{%s}](%s)" % (self.coalition(), subformula,)
427

    
428

    
429
    def replace(self, what, withw):
430
        assert self._subformula == what
431
        self._subformula = withw
432

    
433

    
434
    def finalize(self, atoms, guarded, unguarded, fixpoint):
435
        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
436

    
437

    
438

    
439
class Always(ATL):
440
    def __init__(self):
441
        self._subformula = Variable(self)
442

    
443

    
444
    def __str__(self):
445
        subformula = str(self._subformula)
446
        if syntax == 'tatl':
447
            return "<<%s>>G(%s)" % (self.coalition(), subformula,)
448
        else:
449
            return "(ν X . ((%s) & [{%s}]X))" % (subformula,self.coalition())
450

    
451

    
452
    def replace(self, what, withw):
453
        assert self._subformula == what
454
        self._subformula = withw
455

    
456

    
457
    def finalize(self, atoms, guarded, unguarded, fixpoint):
458
        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
459

    
460

    
461

    
462
class Eventually(ATL):
463
    def __init__(self):
464
        self._subformula = Variable(self)
465

    
466

    
467
    def __str__(self):
468
        subformula = str(self._subformula)
469
        if syntax == 'tatl':
470
            return "<<%s>>F(%s)" % (self.coalition(), subformula,)
471
        else:
472
            return "(μ X . ((%s) | [{%s}]X))" % (subformula, self.coalition())
473

    
474

    
475
    def replace(self, what, withw):
476
        assert self._subformula == what
477
        self._subformula = withw
478

    
479

    
480
    def finalize(self, atoms, guarded, unguarded, fixpoint):
481
        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
482

    
483

    
484

    
485
class Until(ATL):
486
    def __init__(self):
487
        self._left = Variable(self)
488
        self._right = Variable(self)
489

    
490

    
491
    def __str__(self):
492
        left = str(self._left)
493
        right = str(self._right)
494
        if syntax == 'tatl':
495
            return "<<%s>>((%s) U (%s))" % (self.coalition(),left, right)
496
        else:
497
            return "(μ X . ((%s) | ((%s) & [{%s}]X)))" % (right,left,self.coalition())
498

    
499

    
500
    def replace(self, what, withw):
501
        if what == self._left:
502
            self._left = withw
503
        else:
504
            assert self._right == what
505
            self._right = withw
506

    
507

    
508
    def finalize(self, atoms, guarded, unguarded, fixpoint):
509
        self._left.finalize(atoms, guarded, unguarded, fixpoint)
510
        self._right.finalize(atoms, guarded, unguarded, fixpoint)
511

    
512

    
513

    
514
connectives = []
515

    
516

    
517
class Variable:
518
    def __init__(self, parent):
519
        self._parent = parent
520
        variables.append(self)
521

    
522

    
523
    def __str__(self):
524
        return "(undecided)"
525

    
526

    
527
    def replace(self):
528
        assert self._parent != None
529
        replacement = random.choice(connectives)()
530
        variables.remove(self)
531
        self._parent.replace(self, replacement)
532

    
533

    
534
    def finalize(self, atoms, guarded, unguarded, fixpoint):
535
        choice = random.choice(guarded + atoms)
536
        if choice in atoms:
537
            choice = random.choice([choice, "~%s" % choice])
538

    
539
        variables.remove(self)
540
        self._parent.replace(self, choice)
541

    
542

    
543

    
544
def main(args):
545
    global connectives
546
    if args.logic == 'afmu':
547
        connectives = [And, And, Or, Or, Box, Diamond, Mu, Nu]
548
        os.makedirs(os.path.join(args.destdir, 'cool'))
549
        os.makedirs(os.path.join(args.destdir, 'mlsolver'))
550

    
551
    elif args.logic == 'CTL':
552
        connectives = [And, And, Or, Or, Box, Diamond, AF, AG, EF, EG, AU, EU]
553
        os.makedirs(os.path.join(args.destdir, 'ctl'))
554

    
555
    elif args.logic == 'ATL':
556
        connectives = [And, And, Or, Or, Next, Always, Eventually, Until]
557
        os.makedirs(os.path.join(args.destdir, 'cool'))
558
        os.makedirs(os.path.join(args.destdir, 'tatl'))
559

    
560
    for i in range(0, args.count):
561
        global variables
562
        global syntax
563
        variables = []
564
        formula = random.choice(connectives)()
565

    
566
        for _ in range(0, args.constructors):
567
            random.choice(variables).replace()
568

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

    
571
        if args.logic == 'afmu':
572
            with open(os.path.join(args.destdir, 'cool', 'random.%04d.cool' % i), 'w') as f:
573
                syntax = 'cool'
574
                f.write(str(formula))
575

    
576
            with open(os.path.join(args.destdir, 'mlsolver', 'random.%04d.mlsolver' % i), 'w') as f:
577
                syntax = 'mlsolver'
578
                f.write(str(formula))
579

    
580
        elif args.logic == 'CTL':
581
            with open(os.path.join(args.destdir, 'ctl', 'random.%04d.ctl' % i), 'w') as f:
582
                syntax = 'ctl'
583
                f.write(str(formula))
584

    
585
        elif args.logic == 'ATL':
586
            with open(os.path.join(args.destdir, 'cool', 'random.%04d.cool' % i), 'w') as f:
587
                syntax = 'cool'
588
                f.write(str(formula))
589

    
590
            with open(os.path.join(args.destdir, 'tatl', 'random.%04d.tatl' % i), 'w') as f:
591
                syntax = 'tatl'
592
                f.write(str(formula))
593

    
594
    print(args.destdir)
595

    
596
if __name__ == '__main__':
597
    parser = argparse.ArgumentParser(description="Generator for random μ-Calculus-Formulas")
598
    parser.add_argument('--atoms', type=int, required=True,
599
                        help="Number of propositional arguments to use")
600
    parser.add_argument('--constructors', type=int, required=True,
601
                        help="Number of connectives to build")
602
    parser.add_argument('--count', type=int, required=True,
603
                        help="Number of formulas to generate")
604
    parser.add_argument('--destdir', type=str, required=True,
605
                        help="Directory to place created formulas in")
606
    parser.add_argument('--logic', choices=['CTL', 'ATL', 'afmu'], required=True)
607

    
608
    args = parser.parse_args()
609

    
610
    main(args)