diff --git a/randmu.py b/randmu.py index 8c9711b4b40db79b3cbf878312bba654a35c9686..2c1ed65edf6e4e8fee0603b5f07d9444b179b312 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)