diff --git a/wrap/python/spot.py b/wrap/python/spot.py index bd2d9049c..668cc9878 100644 --- a/wrap/python/spot.py +++ b/wrap/python/spot.py @@ -417,11 +417,10 @@ def _addfilter(fun): def nfiltf(self, *args, **kwargs): it = filter(lambda f: not getattr(f, fun)(*args, **kwargs), self) return formulaiterator(it) - setattr(formulaiterator, fun, filtf) if fun[:3] == 'is_': - notfun = fun[:3] + 'not_' + fun[3:] + notfun = 'is_not_' + fun[3:] elif fun[:4] == 'has_': - notfun = fun[:4] + 'no_' + fun[4:] + notfun = 'has_no_' + fun[4:] else: notfun = 'not_' + fun setattr(formulaiterator, fun, filtf) @@ -433,9 +432,9 @@ def _addfilter(fun): def _addmap(fun): def mapf(self, *args, **kwargs): return formulaiterator(map(lambda f: getattr(f, fun)(*args, **kwargs), -self)) - setattr(formula, fun, lambda self, *args, **kwargs: globals()[fun](self, - *args, **kwargs)) + self)) + setattr(formula, fun, + lambda self, *args, **kwargs: globals()[fun](self, *args, **kwargs)) setattr(formulaiterator, fun, mapf) def randltl(ap, n = -1, **kwargs): @@ -531,18 +530,26 @@ def randltl(ap, n = -1, **kwargs): sys.stderr.write("internal error: unknown type of output") return - def _randltlgenerator(rg): - i = 0 - while i != n: - f = rg.next() + class _randltliterator: + def __init__(self, rg, n): + self.rg = rg + self.i = 0 + self.n = n + def __iter__(self): + return self + def __next__(self): + if self.i == self.n: + raise StopIteration + f = self.rg.next() if f is None: - sys.stderr.write("Warning: could not generate a new unique formula " \ - "after " + str(MAX_TRIALS) + " trials.\n") - yield None - else: - yield f - i += 1 - return formulaiterator(_randltlgenerator(rg)) + sys.stderr.write("Warning: could not generate a new " + "unique formula after {} trials.\n" + .format(MAX_TRIALS)) + raise StopIteration + self.i += 1 + return f + + return formulaiterator(_randltliterator(rg, n)) def simplify(f, **kwargs): level = kwargs.get('level', None) diff --git a/wrap/python/tests/randltl.ipynb b/wrap/python/tests/randltl.ipynb index cdd2a3acd..fd163cbce 100644 --- a/wrap/python/tests/randltl.ipynb +++ b/wrap/python/tests/randltl.ipynb @@ -1,7 +1,23 @@ { "metadata": { - "name": "", - "signature": "sha256:54b0c9570ca91322c466f914d622a3723cd3e450612a055a188927bf50dfdaf8" + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.4.3+" + }, + "name": "" }, "nbformat": 3, "nbformat_minor": 0, @@ -164,7 +180,7 @@ "output_type": "stream", "stream": "stdout", "text": [ - "G(p2 U Gp0)\n" + "G(p1 U Gp0)\n" ] } ], @@ -199,7 +215,7 @@ "output_type": "stream", "stream": "stdout", "text": [ - "{{p0 && p1}[*]}<>-> (Fp1 & Fp0)\n" + "{{p0 && p2}[*]}<>-> (Fp2 & Fp0)\n" ] } ], @@ -571,11 +587,11 @@ "stream": "stdout", "text": [ "0\n", - "!(F!p0 M 1)\n", - "(Gp1 | Fp0) M 1\n", - "F!(!p0 <-> FGp0)\n", - "Gp0 U (p0 U GFp0)\n", - "(!p0 U p0) U ((p1 & (p1 U (!p1 & (!p1 -> Fp0))) & ((!p0 U !p1) | (p0 U !p1))) | (!p1 & (!p1 U (p1 & (!p1 -> Fp0))) & ((!p0 U p1) | (p0 U p1))) | (p0 & (p0 U (!p0 & (!p1 -> Fp0))) & ((!p1 U !p0) | (p1 U !p0))) | (!p0 & (!p0 U (p0 & (!p1 -> Fp0))) & ((!p1 U p0) | (p1 U p0))) | ((!p1 -> Fp0) & (Gp1 | G!p1) & (Gp0 | G!p0)))\n" + "!(F!p1 M 1)\n", + "(Gp0 | Fp1) M 1\n", + "F!(!p1 <-> FGp1)\n", + "Gp1 U (p1 U GFp1)\n", + "(!p1 U p1) U ((p0 & (p0 U (!p0 & (!p0 -> Fp1))) & ((!p1 U !p0) | (p1 U !p0))) | (!p0 & (!p0 U (p0 & (!p0 -> Fp1))) & ((!p1 U p0) | (p1 U p0))) | (p1 & (p1 U (!p1 & (!p0 -> Fp1))) & ((!p0 U !p1) | (p0 U !p1))) | (!p1 & (!p1 U (p1 & (!p0 -> Fp1))) & ((!p0 U p1) | (p0 U p1))) | ((!p0 -> Fp1) & (Gp0 | G!p0) & (Gp1 | G!p1)))\n" ] } ],