From 3b329210c0feb25c40d9e6f37c2832c0e50516f9 Mon Sep 17 00:00:00 2001 From: Christoph Egger <Christoph.Egger@fau.de> Date: Fri, 6 May 2016 16:50:52 +0200 Subject: [PATCH] Also create mlsolver-compatible versions --- randmu.py | 23 ++++++++++++++++++----- 1 file changed, 18 insertions(+), 5 deletions(-) diff --git a/randmu.py b/randmu.py index 8c9711b..2c1ed65 100755 --- a/randmu.py +++ b/randmu.py @@ -16,13 +16,14 @@ import os variables = [] +cool = True def _gensym(): i = 0 while True: i = i + 1 - yield "gen%d" % i + yield "G%d" % i gensym = iter(_gensym()) @@ -188,7 +189,10 @@ class Mu(Fixpoint): def __str__(self): subformula = str(self._subformula) - return "μ %s . (%s)" % (self._var, subformula) + if cool: + return "μ %s . (%s)" % (self._var, subformula) + else: + return "mu %s . (%s)" % (self._var, subformula) def replace(self, what, withw): @@ -201,7 +205,7 @@ class Mu(Fixpoint): if fixpoint == 'nu': guarded = [] unguarded = [] - + self._subformula.finalize(atoms, guarded, unguarded + [self._var], 'mu') else: self._subformula = random.choice(atoms + guarded) @@ -216,7 +220,10 @@ class Nu(Fixpoint): def __str__(self): subformula = str(self._subformula) - return "ν %s . (%s)" % (self._var, subformula) + if cool: + return "ν %s . (%s)" % (self._var, subformula) + else: + return "nu %s . (%s)" % (self._var, subformula) def replace(self, what, withw): @@ -229,7 +236,7 @@ class Nu(Fixpoint): if fixpoint == 'mu': guarded = [] unguarded = [] - + self._subformula.finalize(atoms, guarded, unguarded + [self._var], 'nu') else: self._subformula = random.choice(atoms + guarded) @@ -266,6 +273,7 @@ def main(args): os.makedirs(os.path.join(args.destdir, 'mlsolver')) for i in range(0, args.count): global variables + global cool variables = [] formula = random.choice(connectives)() @@ -274,6 +282,11 @@ def main(args): formula.finalize(list(string.ascii_lowercase[:args.atoms]), [], [], 'none') with open(os.path.join(args.destdir, 'cool', 'random.%04d.cool' % i), 'w') as f: + cool = True + f.write(str(formula)) + + with open(os.path.join(args.destdir, 'mlsolver', 'random.%04d.mlsolver' % i), 'w') as f: + cool = False f.write(str(formula)) print(args.destdir) -- GitLab