## cool / randmu.py @ master

History | View | Annotate | Download (15 KB)

1 | 4eab42c3 | Christoph Egger | ```
#!/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 | 60d2d6aa | Christoph Egger | ```
syntax = 'cool'
``` |

20 | 4eab42c3 | Christoph Egger | |

21 | |||

22 | def _gensym(): |
||

23 | ```
i = 0
``` |
||

24 | while True: |
||

25 | ```
i = i + 1
``` |
||

26 | 3b329210 | Christoph Egger | yield "G%d" % i |

27 | 4eab42c3 | Christoph Egger | |

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 | becb9ab2 | Christoph Egger | if syntax == 'tatl': |

53 | return "((%s) /\ (%s))" % (left, right) |
||

54 | ```
else:
``` |
||

55 | return "((%s) & (%s))" % (left, right) |
||

56 | 4eab42c3 | Christoph Egger | |

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 | 39c9b648 | Christoph Egger | ```
self._left.finalize(atoms, guarded, unguarded, fixpoint)
``` |

68 | ```
self._right.finalize(atoms, guarded, unguarded, fixpoint)
``` |
||

69 | 4eab42c3 | Christoph Egger | |

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 | becb9ab2 | Christoph Egger | if syntax == 'tatl': |

82 | return "((%s) \/ (%s))" % (left, right) |
||

83 | ```
else:
``` |
||

84 | return "((%s) | (%s))" % (left, right) |
||

85 | 4eab42c3 | Christoph Egger | |

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 | 39c9b648 | Christoph Egger | ```
self._left.finalize(atoms, guarded, unguarded, fixpoint)
``` |

97 | ```
self._right.finalize(atoms, guarded, unguarded, fixpoint)
``` |
||

98 | 4eab42c3 | Christoph Egger | |

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 | 60d2d6aa | Christoph Egger | if syntax == 'ctl': |

113 | return "AX (%s)" % (subformula,) |
||

114 | ```
else:
``` |
||

115 | return "[] (%s)" % (subformula,) |
||

116 | 4eab42c3 | Christoph Egger | |

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 | 39c9b648 | Christoph Egger | ```
self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
``` |

125 | 4eab42c3 | Christoph Egger | |

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 | 60d2d6aa | Christoph Egger | if syntax == 'ctl': |

136 | return "EX (%s)" % (subformula,) |
||

137 | ```
else:
``` |
||

138 | return "<> (%s)" % (subformula,) |
||

139 | 4eab42c3 | Christoph Egger | |

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 | 39c9b648 | Christoph Egger | ```
self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
``` |

148 | 4eab42c3 | Christoph Egger | |

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 | 60d2d6aa | Christoph Egger | if syntax == 'cool': |

163 | 23f1d0e0 | Christoph Egger | return "(μ %s . (%s))" % (self._var, subformula) |

164 | 3b329210 | Christoph Egger | ```
else:
``` |

165 | 23f1d0e0 | Christoph Egger | return "(mu %s . (%s))" % (self._var, subformula) |

166 | 4eab42c3 | Christoph Egger | |

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 | 39c9b648 | Christoph Egger | if fixpoint == 'nu': |

175 | guarded = [] |
||

176 | unguarded = [] |
||

177 | 3b329210 | Christoph Egger | |

178 | 39c9b648 | Christoph Egger | self._subformula.finalize(atoms, guarded, unguarded + [self._var], 'mu') |

179 | 4eab42c3 | Christoph Egger | |

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 | 60d2d6aa | Christoph Egger | if syntax == 'cool': |

191 | 23f1d0e0 | Christoph Egger | return "(ν %s . (%s))" % (self._var, subformula) |

192 | 3b329210 | Christoph Egger | ```
else:
``` |

193 | 23f1d0e0 | Christoph Egger | return "(nu %s . (%s))" % (self._var, subformula) |

194 | 4eab42c3 | Christoph Egger | |

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 | 39c9b648 | Christoph Egger | if fixpoint == 'mu': |

203 | guarded = [] |
||

204 | unguarded = [] |
||

205 | 3b329210 | Christoph Egger | |

206 | 39c9b648 | Christoph Egger | self._subformula.finalize(atoms, guarded, unguarded + [self._var], 'nu') |

207 | 4eab42c3 | Christoph Egger | |

208 | |||

209 | |||

210 | 60d2d6aa | Christoph Egger | 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 | becb9ab2 | Christoph Egger | class ATL: |

400 | def coalition(self): |
||

401 | 74870253 | Christoph Egger | 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 | becb9ab2 | Christoph Egger | |

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 | 7d83cfb6 | Christoph Egger | return "<<%s>>X(%s)" % (self.coalition(), subformula,) |

425 | becb9ab2 | Christoph Egger | ```
else:
``` |

426 | 7d83cfb6 | Christoph Egger | return "[{%s}](%s)" % (self.coalition(), subformula,) |

427 | becb9ab2 | Christoph Egger | |

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 | 7d83cfb6 | Christoph Egger | return "<<%s>>G(%s)" % (self.coalition(), subformula,) |

448 | becb9ab2 | Christoph Egger | ```
else:
``` |

449 | 7d83cfb6 | Christoph Egger | return "(ν X . ((%s) & [{%s}]X))" % (subformula,self.coalition()) |

450 | becb9ab2 | Christoph Egger | |

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 | 7d83cfb6 | Christoph Egger | return "(μ X . ((%s) | [{%s}]X))" % (subformula, self.coalition()) |

473 | becb9ab2 | Christoph Egger | |

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 | 7d83cfb6 | Christoph Egger | return "(μ X . ((%s) | ((%s) & [{%s}]X)))" % (right,left,self.coalition()) |

498 | becb9ab2 | Christoph Egger | |

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 | 60d2d6aa | Christoph Egger | |

514 | connectives = [] |
||

515 | 4eab42c3 | Christoph Egger | |

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 | 39c9b648 | Christoph Egger | 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 | 4eab42c3 | Christoph Egger | |

542 | |||

543 | |||

544 | def main(args): |
||

545 | 60d2d6aa | Christoph Egger | ```
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 | 3e2aa1b8 | Christoph Egger | connectives = [And, And, Or, Or, Box, Diamond, AF, AG, EF, EG, AU, EU] |

553 | 60d2d6aa | Christoph Egger | ```
os.makedirs(os.path.join(args.destdir, 'ctl'))
``` |

554 | |||

555 | becb9ab2 | Christoph Egger | 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 | 4eab42c3 | Christoph Egger | for i in range(0, args.count): |

561 | ```
global variables
``` |
||

562 | 60d2d6aa | Christoph Egger | ```
global syntax
``` |

563 | 4eab42c3 | Christoph Egger | 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 | 3b329210 | Christoph Egger | |

571 | 60d2d6aa | Christoph Egger | 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 | d0628bb9 | Christoph Egger | ```
syntax = 'ctl'
``` |

583 | 60d2d6aa | Christoph Egger | ```
f.write(str(formula))
``` |

584 | 4eab42c3 | Christoph Egger | |

585 | becb9ab2 | Christoph Egger | 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 | 4eab42c3 | Christoph Egger | 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 | becb9ab2 | Christoph Egger | parser.add_argument('--logic', choices=['CTL', 'ATL', 'afmu'], required=True) |

607 | 4eab42c3 | Christoph Egger | |

608 | args = parser.parse_args() |
||

609 | |||

610 | main(args) |