diff --git a/python/spot/__init__.py b/python/spot/__init__.py index c1bc8b229..b8400427e 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -107,14 +107,17 @@ if 'op_ff' not in globals(): _bdd_dict = make_bdd_dict() - __om_init_tmp = option_map.__init__ + + def __om_init_new(self, str=None): __om_init_tmp(self) if str: res = self.parse_options(str) if res: - raise RuntimeError("failed to parse option at: '" + str +"'") + raise RuntimeError("failed to parse option at: '" + str + "'") + + option_map.__init__ = __om_init_new @@ -162,6 +165,7 @@ class twa: self.highlight_edge(val, color) return self + @_extend(twa) class twa: def to_str(a, format='hoa', opt=None): @@ -192,6 +196,7 @@ class twa: f.write('\n') return a + @_extend(twa_graph) class twa_graph: def show_storage(self, opt=None): @@ -200,12 +205,14 @@ class twa_graph: from IPython.display import SVG return SVG(_ostream_to_svg(ostr)) + def make_twa_graph(*args): from spot.impl import make_twa_graph as mtg if len(args) == 0: return mtg(_bdd_dict) return mtg(*args) + @_extend(formula) class formula: def __init__(self, str): @@ -243,8 +250,8 @@ class formula: return str_sclatex_psl(self, parenth) elif format == 'mathjax' or format == 'j': return (str_sclatex_psl(self, parenth). - replace("``", "\\unicode{x201C}"). - replace("\\textrm{''}", "\\unicode{x201D}")) + replace("``", "\\unicode{x201C}"). + replace("\\textrm{''}", "\\unicode{x201D}")) elif format == 'dot' or format == 'd': ostr = ostringstream() print_dot_psl(ostr, self) @@ -475,9 +482,9 @@ def automata(*sources, timeout=None, ignore_abort=True, # universal_newlines for str output instead of bytes # when the pipe is read from Python (which happens # when timeout is set). + prefn = None if no_sid else os.setsid proc = subprocess.Popen(filename[:-1], shell=True, - preexec_fn= - None if no_sid else os.setsid, + preexec_fn=prefn, universal_newlines=True, stdout=subprocess.PIPE) if timeout is None: @@ -751,7 +758,7 @@ formula.translate = translate # instance methods (i.e., self passed as first argument # automatically), because only user-defined functions are converted as # instance methods. -def _add_formula(meth, name = None): +def _add_formula(meth, name=None): setattr(formula, name or meth, (lambda self, *args, **kwargs: globals()[meth](self, *args, **kwargs))) @@ -811,10 +818,11 @@ twa.postprocess = postprocess # instance methods (i.e., self passed as first argument # automatically), because only user-defined functions are converted as # instance methods. -def _add_twa_graph(meth, name = None): +def _add_twa_graph(meth, name=None): setattr(twa_graph, name or meth, (lambda self, *args, **kwargs: globals()[meth](self, *args, **kwargs))) + for meth in ('scc_filter', 'scc_filter_states', 'is_deterministic', 'is_unambiguous', 'contains'): @@ -824,6 +832,8 @@ _add_twa_graph('are_equivalent', 'equivalent_to') # Wrapper around a formula iterator to which we add some methods of formula # (using _addfilter and _addmap), so that we can write things like # formulas.simplify().is_X_free(). + + class formulaiterator: def __init__(self, formulas): self._formulas = formulas @@ -1003,14 +1013,14 @@ def simplify(f, **kwargs): favor_event_univ = kwargs.get('favor_event_univ', False) simp_opts = tl_simplifier_options(basics, - synt_impl, - event_univ, - cont_checks, - cont_checks_stronger, - nenoform_stop_on_boolean, - reduce_size_strictly, - boolean_to_isop, - favor_event_univ) + synt_impl, + event_univ, + cont_checks, + cont_checks_stronger, + nenoform_stop_on_boolean, + reduce_size_strictly, + boolean_to_isop, + favor_event_univ) return tl_simplifier(simp_opts).simplify(f) @@ -1025,14 +1035,13 @@ for fun in ['remove_x', 'relabel', 'relabel_bse', _addmap(fun) - # Better interface to the corresponding C++ function. def sat_minimize(aut, acc=None, colored=False, state_based=False, states=0, max_states=0, sat_naive=False, sat_langmap=False, sat_incr=0, sat_incr_steps=0, display_log=False, return_log=False): - args='' + args = '' if acc is not None: if type(acc) is not str: raise ValueError("argument 'acc' should be a string") @@ -1079,16 +1088,19 @@ def parse_word(word, dic=_bdd_dict): from spot.impl import parse_word as pw return pw(word, dic) + def bdd_to_formula(b, dic=_bdd_dict): from spot.impl import bdd_to_formula as bf return bf(b, dic) + def language_containment_checker(dic=_bdd_dict): from spot.impl import language_containment_checker as c c.contains = lambda this, a, b: c.contained(this, b, a) c.are_equivalent = lambda this, a, b: c.equal(this, a, b) return c(dic) + def mp_hierarchy_svg(cl=None): """ Return an some string containing an SVG picture of the Manna & @@ -1099,7 +1111,7 @@ def mp_hierarchy_svg(cl=None): `mp_class(cl)`. """ - if type(cl)==formula: + if type(cl) == formula: cl = mp_class(cl) ch = None coords = { @@ -1112,12 +1124,12 @@ def mp_hierarchy_svg(cl=None): 'B': '110,198', } if cl in coords: - highlight=''' + highlight = ''' '''.format(coords[cl]) else: - highlight='' + highlight = '' return ''' @@ -1150,8 +1162,10 @@ def show_mp_hierarchy(cl): from IPython.display import SVG return SVG(mp_hierarchy_svg(cl)) + formula.show_mp_hierarchy = show_mp_hierarchy + @_extend(twa_word) class twa_word: def _repr_latex_(self): @@ -1162,8 +1176,8 @@ class twa_word: res += '; ' res += bdd_to_formula(letter, bd).to_str('j') if len(res) > 1: - res += '; '; - res += '\\mathsf{cycle}\\{'; + res += '; ' + res += '\\mathsf{cycle}\\{' for idx, letter in enumerate(self.cycle): if idx: res += '; ' @@ -1201,7 +1215,7 @@ class twa_word: 'txt': 'text-anchor="start" font-size="20"', 'red': 'stroke="#ff0000" stroke-width="2"', 'sml': 'text-anchor="start" font-size="10"' - } + } txt = ''' @@ -1236,11 +1250,11 @@ class twa_word: if cur != 0: if last == -cur: txt += \ - ('' + ('' .format(x=xpos*50, y1=ypos*50+5, y2=ypos*50+45, **d)) txt += \ - ('' + ('' .format(x1=xpos*50, x2=(xpos+1)*50, y=ypos*50+25-20*cur, **d)) last = cur @@ -1263,5 +1277,6 @@ class twa_word: class scc_and_mark_filter: def __enter__(self): return self + def __exit__(self, exc_type, exc_value, traceback): self.restore_acceptance() diff --git a/python/spot/aux.py b/python/spot/aux.py index e4fa284b5..53d787e89 100644 --- a/python/spot/aux.py +++ b/python/spot/aux.py @@ -28,6 +28,7 @@ import os import errno import contextlib + def extend(*classes): """ Decorator that extends all the given classes with the contents @@ -89,6 +90,7 @@ def rm_f(filename): if e.errno != errno.ENOENT: raise + @contextlib.contextmanager def tmpdir(): cwd = os.getcwd() diff --git a/python/spot/jupyter.py b/python/spot/jupyter.py index 7b933db9f..fdd312399 100644 --- a/python/spot/jupyter.py +++ b/python/spot/jupyter.py @@ -23,6 +23,7 @@ Auxiliary functions for Spot's Python bindings. from IPython.display import display, HTML + def display_inline(*args, per_row=None, show=None): """ This is a wrapper around IPython's `display()` to display multiple @@ -49,5 +50,5 @@ def display_inline(*args, per_row=None, show=None): else: rep = str(arg) res += ("
{}
" - .format(dpy, width, rep)) + .format(dpy, width, rep)) display(HTML(res)) diff --git a/tests/python/341.py b/tests/python/341.py index 6a0ddea41..4c5937149 100644 --- a/tests/python/341.py +++ b/tests/python/341.py @@ -20,6 +20,7 @@ import spot from subprocess import _active + def two_intersecting_automata(): """return two random automata with a non-empty intersection""" g = spot.automata('randaut -A4 -Q5 -n-1 2 |') @@ -27,9 +28,10 @@ def two_intersecting_automata(): if a.intersects(b): return a, b + for i in range(5): two_intersecting_automata() n = len(_active) print(n, "active processes") -assert(n == 0); +assert(n == 0) diff --git a/tests/python/alarm.py b/tests/python/alarm.py index 30af57206..679dc1867 100755 --- a/tests/python/alarm.py +++ b/tests/python/alarm.py @@ -23,11 +23,13 @@ import signal import sys import os + def alarm_handler(signum, frame): sys.stdout.write("signaled\n") os.kill(child, signal.SIGTERM) exit(0) + f = """!(G(F(P_Rbt2.observe)&& F(P_Rbt3.observe) && F(P_rbt1.observe)&& F(P_Rbt1.plus || P_Rbt1.moins || P_Rbt1.stop)&& F(P_Rbt3.plus || P_Rbt3.moins || P_Rbt3.stop) && F(P_Rbt2.plus || diff --git a/tests/python/bdddict.py b/tests/python/bdddict.py index 366f18fdd..bdb5fc2df 100644 --- a/tests/python/bdddict.py +++ b/tests/python/bdddict.py @@ -20,6 +20,10 @@ # Make sure we can leep track of BDD association in Python using bdd_dict, as # discussed in issue #372. + +import spot + + class bdd_holder: def __init__(self, aut): self.bdddict = d = aut.get_dict() @@ -48,10 +52,10 @@ class bdd_holder3: self.bdddict.unregister_all_my_variables(self) - def check_ok(): assert type(bdict.varnum(spot.formula.ap("a"))) is int + def check_nok(): try: bdict.varnum(spot.formula.ap("a")) @@ -60,12 +64,13 @@ def check_nok(): else: raise RuntimeError("missing exception") + def debug(txt): # print(txt) # bdict.dump(spot.get_cout()) pass -import spot + aut = spot.translate("a U b") bdict = aut.get_dict() debug("aut") diff --git a/tests/python/bddnqueen.py b/tests/python/bddnqueen.py index c336bf2ce..95809979e 100755 --- a/tests/python/bddnqueen.py +++ b/tests/python/bddnqueen.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2010, 2011, 2012, 2014 Laboratoire de Recherche et +# Copyright (C) 2010, 2011, 2012, 2014, 2019 Laboratoire de Recherche et # Développement de l'EPITA. # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 # (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -26,9 +26,12 @@ import sys from buddy import * -# Build the requirements for all other fields than (i,j) assuming -# that (i,j) has a queen. + def build(i, j): + """ + Build the requirements for all other fields than (i,j) assuming + that (i,j) has a queen. + """ a = b = c = d = bddtrue # No one in the same column. @@ -59,7 +62,6 @@ def build(i, j): queen &= a & b & c & d - # Get the number of queens from the command-line, or default to 8. if len(sys.argv) > 1: N = int(argv[1]) @@ -97,7 +99,6 @@ solution = bdd_satone(queen) bdd_printset(solution) from spot import nl_cout - nl_cout() # Cleanup all BDD variables before calling bdd_done(), otherwise diff --git a/tests/python/bugdet.py b/tests/python/bugdet.py index 6f0941d69..9e06e0db3 100644 --- a/tests/python/bugdet.py +++ b/tests/python/bugdet.py @@ -73,7 +73,7 @@ State: 6 {0} State: 7 {0} [0&!1&2] 7 --END-- -"""); +""") # In Reuben's report this first block built an incorrect deterministic # automaton, which ultimately led to an non-empty product. The second @@ -82,10 +82,10 @@ print("use_simulation=True") b1 = spot.tgba_determinize(b, False, True, True, True) assert b1.num_states() == 5 b1 = spot.remove_fin(spot.dualize(b1)) -assert not a.intersects(b1); +assert not a.intersects(b1) print("\nuse_simulation=False") b2 = spot.tgba_determinize(b, False, True, False, True) assert b2.num_states() == 5 b2 = spot.remove_fin(spot.dualize(b2)) -assert not a.intersects(b2); +assert not a.intersects(b2) diff --git a/tests/python/dualize.py b/tests/python/dualize.py index e5d9cc0aa..6a054bf10 100755 --- a/tests/python/dualize.py +++ b/tests/python/dualize.py @@ -21,68 +21,78 @@ import spot import buddy -match_strings = [('is_buchi', 'is_co_buchi'),\ - ('is_generalized_buchi', 'is_generalized_co_buchi'),\ - ('is_all', 'is_none'),\ +match_strings = [('is_buchi', 'is_co_buchi'), + ('is_generalized_buchi', 'is_generalized_co_buchi'), + ('is_all', 'is_none'), ('is_all', 'is_all'), ('is_buchi', 'is_all')] # existential and universal are dual # deterministic is self-dual + + def dualtype(aut, dual): - if dual.acc().is_none(): return True - return (not spot.is_deterministic(aut) or spot.is_deterministic(dual))\ - and (spot.is_universal(dual) or not aut.is_existential())\ - and (dual.is_existential() or not spot.is_universal(aut)) + if dual.acc().is_none(): + return True + return (not spot.is_deterministic(aut) or spot.is_deterministic(dual))\ + and (spot.is_universal(dual) or not aut.is_existential())\ + and (dual.is_existential() or not spot.is_universal(aut)) + def produce_phi(rg, n): - phi = [] - while len(phi) < n: - phi.append(rg.next()) - return phi + phi = [] + while len(phi) < n: + phi.append(rg.next()) + return phi + def produce_automaton(phi): - aut = [] - for f in phi: - aut.append(spot.translate(f)) - return aut + aut = [] + for f in phi: + aut.append(spot.translate(f)) + return aut -def test_aut(aut, d = None): - if d is None: - d = spot.dualize(aut) - aa = aut.acc() - da = d.acc() - complete = spot.is_complete(aut) - univ = aut.is_univ_dest(aut.get_init_state_number()) - an = aut.num_states() - dn = d.num_states() +def test_aut(aut, d=None): + if d is None: + d = spot.dualize(aut) + aa = aut.acc() + da = d.acc() - if not dualtype(aut, d): - return (False, 'Incorrect transition mode resulting of dual') - for p in match_strings: - if ((getattr(aa, p[0])() and getattr(da, p[1])())\ - or (getattr(aa, p[1])() and getattr(da, p[0])())): - return (True, '') - return (False, 'Incorrect acceptance type dual') + complete = spot.is_complete(aut) + univ = aut.is_univ_dest(aut.get_init_state_number()) + an = aut.num_states() + dn = d.num_states() + + if not dualtype(aut, d): + return (False, 'Incorrect transition mode resulting of dual') + for p in match_strings: + if ((getattr(aa, p[0])() and getattr(da, p[1])()) + or (getattr(aa, p[1])() and getattr(da, p[0])())): + return (True, '') + return (False, 'Incorrect acceptance type dual') # Tests that a (deterministic) automaton and its complement have complementary # languages. # FIXME This test could be extended to non-deterministic automata with a # dealternization procedure. + + def test_complement(aut): - assert aut.is_deterministic() - d = spot.dualize(aut) - s = spot.product_or(aut, d) - assert spot.dualize(s).is_empty() + assert aut.is_deterministic() + d = spot.dualize(aut) + s = spot.product_or(aut, d) + assert spot.dualize(s).is_empty() + def test_assert(a, d=None): - t = test_aut(a, d) - if not t[0]: - print (t[1]) - print (a.to_str('hoa')) - print (spot.dualize(a).to_str('hoa')) - assert False + t = test_aut(a, d) + if not t[0]: + print (t[1]) + print (a.to_str('hoa')) + print (spot.dualize(a).to_str('hoa')) + assert False + aut = spot.translate('a') @@ -591,8 +601,8 @@ spot.srand(0) rg = spot.randltlgenerator(2, opts) for a in produce_automaton(produce_phi(rg, 1000)): - test_assert(a) - test_assert(spot.dualize(a), spot.dualize(spot.dualize(a))) + test_assert(a) + test_assert(spot.dualize(a), spot.dualize(spot.dualize(a))) aut = spot.automaton(""" HOA: v1 @@ -606,4 +616,4 @@ State: 0 test_complement(aut) for a in spot.automata('randaut -A \"random 0..6\" -H -D -n50 4|'): - test_complement(a) + test_complement(a) diff --git a/tests/python/except.py b/tests/python/except.py index 0d4819d10..d69417d22 100644 --- a/tests/python/except.py +++ b/tests/python/except.py @@ -25,6 +25,7 @@ import spot import buddy + def report_missing_exception(): raise RuntimeError("missing exception") @@ -147,7 +148,7 @@ else: report_missing_exception() try: - m = spot.mark_t([0,n,1]) + m = spot.mark_t([0, n, 1]) except RuntimeError as e: assert "bit index is out of bounds" in str(e) else: diff --git a/tests/python/gen.py b/tests/python/gen.py index 85596d978..dd844741c 100644 --- a/tests/python/gen.py +++ b/tests/python/gen.py @@ -71,8 +71,8 @@ else: try: gen.ltl_pattern(gen.LTL_OR_G, -10) except RuntimeError as e: - assert 'or-g' in str(e) - assert 'positive' in str(e) + assert 'or-g' in str(e) + assert 'positive' in str(e) else: exit(2) diff --git a/tests/python/genem.py b/tests/python/genem.py index e1cbd64e6..a2741a2fc 100644 --- a/tests/python/genem.py +++ b/tests/python/genem.py @@ -139,8 +139,6 @@ State: 1 [0&1] 0 {4 6 7} [0&!1] 1 {3 6} [!0&1] 0 {4 7} [!0&!1] 1 {0} --END--""") - - def generic_emptiness2_rec(aut): spot.cleanup_acceptance_here(aut, False) # Catching 'false' acceptance here is an optimization that could be removed. @@ -183,6 +181,8 @@ def generic_emptiness2_rec(aut): return True # A very old python version of spot.generic_emptiness_check() + + def generic_emptiness2(aut): old_a = spot.acc_cond(aut.acc()) res = generic_emptiness2_rec(aut) @@ -191,6 +191,8 @@ def generic_emptiness2(aut): return res # A more modern python version of spot.generic_emptiness_check() + + def is_empty1(g): si = spot.scc_info_with_options(g, spot.scc_info_options_NONE) for scc_num in range(si.scc_count()): @@ -200,17 +202,21 @@ def is_empty1(g): return False return True + def is_scc_empty1(si, scc_num, acc=None): - if acc is None: # acceptance isn't forced, get it from the automaton + if acc is None: # acceptance isn't forced, get it from the automaton acc = si.get_aut().acc() occur, common = si.acc_sets_of(scc_num), si.common_sets_of(scc_num) acc = acc.restrict_to(occur) acc = acc.remove(common, False) - if acc.is_t(): return False - if acc.is_f(): return True - if acc.accepting(occur): return False + if acc.is_t(): + return False + if acc.is_f(): + return True + if acc.accepting(occur): + return False for cl in acc.top_disjuncts(): - fu = cl.fin_unit() # Is there Fin at the top level + fu = cl.fin_unit() # Is there Fin at the top level if fu: with spot.scc_and_mark_filter(si, scc_num, fu) as filt: filt.override_acceptance(cl.remove(fu, True)) @@ -229,22 +235,25 @@ def is_scc_empty1(si, scc_num, acc=None): return False return True + def is_empty2(g): return is_empty2_rec(spot.scc_and_mark_filter(g, g.acc().fin_unit())) + def is_empty2_rec(g): si = spot.scc_info_with_options(g, spot.scc_info_options_STOP_ON_ACC) if si.one_accepting_scc() >= 0: return False for scc_num in range(si.scc_count()): - if si.is_rejecting_scc(scc_num): # this includes trivial SCCs + if si.is_rejecting_scc(scc_num): # this includes trivial SCCs continue if not is_scc_empty2(si, scc_num): return False return True + def is_scc_empty2(si, scc_num, acc=None): - if acc is None: # acceptance isn't forced, get it from the automaton + if acc is None: # acceptance isn't forced, get it from the automaton acc = si.get_aut().acc() occur, common = si.acc_sets_of(scc_num), si.common_sets_of(scc_num) acc = acc.restrict_to(occur) @@ -252,7 +261,7 @@ def is_scc_empty2(si, scc_num, acc=None): # 3 stop conditions removed here, because they are caught by # one_accepting_scc() or is_rejecting_scc() in is_empty2_rec() for cl in acc.top_disjuncts(): - fu = cl.fin_unit() # Is there Fin at the top level + fu = cl.fin_unit() # Is there Fin at the top level if fu: with spot.scc_and_mark_filter(si, scc_num, fu) as filt: filt.override_acceptance(cl.remove(fu, True)) @@ -271,6 +280,7 @@ def is_scc_empty2(si, scc_num, acc=None): return False return True + def run_bench(automata): for aut in automata: # Make sure our three implementation behave identically @@ -287,4 +297,5 @@ def run_bench(automata): run3 = spot.generic_accepting_run(aut) assert run3.replay(spot.get_cout()) is True + run_bench([a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a11, a360]) diff --git a/tests/python/implies.py b/tests/python/implies.py index 2e8a86e3c..2e4e64ddd 100755 --- a/tests/python/implies.py +++ b/tests/python/implies.py @@ -25,37 +25,37 @@ bdd_setvarnum(5) V = [bdd_ithvar(i) for i in range(5)] -a = V[0] & V[1] & -V[2] -b = V[0] & V[1] & -V[2] & -V[3] +a = V[0] & V[1] & -V[2] +b = V[0] & V[1] & -V[2] & -V[3] c = -V[0] & V[1] & -V[2] & -V[3] -d = V[1] & -V[2] -e = V[1] & V[2] & -V[3] & V[4] -f = V[0] & -V[3] & V[4] +d = V[1] & -V[2] +e = V[1] & V[2] & -V[3] & V[4] +f = V[0] & -V[3] & V[4] g = -V[0] | V[1] -assert(bdd_implies(b,a)) -assert(not bdd_implies(a,b)) -assert(not bdd_implies(c,a)) -assert(bdd_implies(a,d)) -assert(bdd_implies(b,d)) -assert(bdd_implies(c,d)) -assert(bdd_implies(d,d)) -assert(not bdd_implies(e,d)) -assert(not bdd_implies(d,e)) -assert(not bdd_implies(f,e)) -assert(not bdd_implies(e,f)) -assert(bdd_implies(bddfalse,f)) -assert(not bdd_implies(bddtrue,f)) -assert(bdd_implies(f,bddtrue)) -assert(not bdd_implies(f,bddfalse)) -assert(bdd_implies(a,g)) +assert(bdd_implies(b, a)) +assert(not bdd_implies(a, b)) +assert(not bdd_implies(c, a)) +assert(bdd_implies(a, d)) +assert(bdd_implies(b, d)) +assert(bdd_implies(c, d)) +assert(bdd_implies(d, d)) +assert(not bdd_implies(e, d)) +assert(not bdd_implies(d, e)) +assert(not bdd_implies(f, e)) +assert(not bdd_implies(e, f)) +assert(bdd_implies(bddfalse, f)) +assert(not bdd_implies(bddtrue, f)) +assert(bdd_implies(f, bddtrue)) +assert(not bdd_implies(f, bddfalse)) +assert(bdd_implies(a, g)) a = (-V[2] & (-V[1] | V[0])) | (-V[0] & V[1] & V[2]) b = V[1] | -V[2] -assert(bdd_implies(a,b)) +assert(bdd_implies(a, b)) # Cleanup all BDD variables before calling bdd_done(), otherwise # bdd_delref will be called after bdd_done() and this is unsafe in # optimized builds. -V = a = b = c = d = e = f = g = 0; +V = a = b = c = d = e = f = g = 0 bdd_done() diff --git a/tests/python/interdep.py b/tests/python/interdep.py index 57acffa1f..efe17c4cb 100755 --- a/tests/python/interdep.py +++ b/tests/python/interdep.py @@ -34,7 +34,8 @@ d = simp.get_dict() a = spot.ltl_to_tgba_fm(pf.f, d) g = spot.parse_infix_boolean('b&c', e) b = simp.as_bdd(g.f) -buddy.bdd_printset(b); spot.nl_cout() +buddy.bdd_printset(b) +spot.nl_cout() del g s0 = a.get_init_state() @@ -43,11 +44,13 @@ it.first() while not it.done(): c = it.cond() sys.stdout.write("%s\n" % c) - b &= c # `&=' is defined only in buddy. So if this statement works - # it means buddy can grok spot's objects. - buddy.bdd_printset(c); spot.nl_cout() + b &= c # `&=' is defined only in buddy. So if this statement works + # it means buddy can grok spot's objects. + buddy.bdd_printset(c) + spot.nl_cout() it.next() -buddy.bdd_printset(b); spot.nl_cout() +buddy.bdd_printset(b) +spot.nl_cout() sys.stdout.write("%s\n" % b) del it del s0 diff --git a/tests/python/ipnbdoctest.py b/tests/python/ipnbdoctest.py index 107adff50..20b69722f 100755 --- a/tests/python/ipnbdoctest.py +++ b/tests/python/ipnbdoctest.py @@ -12,7 +12,9 @@ with those stored in the notebook. from __future__ import print_function -import os,sys,time +import os +import sys +import time import base64 import re import pprint @@ -40,7 +42,7 @@ except ImportError: except ImportError: try: from IPython.zmq.blockingkernelmanager \ - import BlockingKernelManager as KernelManager + import BlockingKernelManager as KernelManager except: print('IPython is needed to run this script.') sys.exit(77) @@ -51,6 +53,7 @@ try: except ImportError: from IPython.nbformat import v4 as nbformat + def compare_png(a64, b64): """compare two b64 PNGs (incomplete)""" try: @@ -61,6 +64,7 @@ def compare_png(a64, b64): bdata = base64.decodestring(b64) return True + def canonicalize(s, type, ignores): """sanitize a string for comparison. @@ -163,8 +167,8 @@ def canonical_dict(dict, ignores): if 'ename' in dict and dict['ename'] == 'CalledProcessError': # CalledProcessError message has a final dot in Python 3.6 dict['evalue'] = \ - re.sub(r"(' returned non-zero exit status \d+)\.", r'\1', - dict['evalue']) + re.sub(r"(' returned non-zero exit status \d+)\.", r'\1', + dict['evalue']) if 'transient' in dict: del dict['transient'] @@ -195,6 +199,7 @@ def compare_outputs(ref, test, ignores=[]): fromfile='expected', tofile='effective'))) return False + def _wait_for_ready_backport(kc): """Backport BlockingKernelClient.wait_for_ready from IPython 3""" # Wait for kernel info reply on shell channel @@ -210,6 +215,7 @@ def _wait_for_ready_backport(kc): except Empty: break + def run_cell(kc, cell): kc.execute(cell.source) # wait for finish, maximum 30s @@ -295,7 +301,6 @@ def test_notebook(ipynb): print("OK") successes += 1 - print("tested notebook %s" % ipynb) print(" %3i cells successfully replicated" % successes) if failures: @@ -308,6 +313,7 @@ def test_notebook(ipynb): if failures | errors: sys.exit(1) + if __name__ == '__main__': for ipynb in sys.argv[1:]: print("testing %s" % ipynb) diff --git a/tests/python/kripke.py b/tests/python/kripke.py index 30f07a81f..f3ce218b2 100644 --- a/tests/python/kripke.py +++ b/tests/python/kripke.py @@ -36,7 +36,7 @@ k.new_edge(s3, s3) k.new_edge(s3, s2) k.set_init_state(s1) -hoa="""HOA: v1 +hoa = """HOA: v1 States: 3 Start: 0 AP: 2 "p1" "p2" diff --git a/tests/python/ltl2tgba.py b/tests/python/ltl2tgba.py index 83d4055dd..6f2dfdd49 100755 --- a/tests/python/ltl2tgba.py +++ b/tests/python/ltl2tgba.py @@ -28,6 +28,7 @@ import sys import getopt import spot + def usage(prog): sys.stderr.write("""Usage: %s [OPTIONS...] formula diff --git a/tests/python/ltlf.py b/tests/python/ltlf.py index 5953180d6..5676a2a1b 100644 --- a/tests/python/ltlf.py +++ b/tests/python/ltlf.py @@ -30,7 +30,7 @@ formulas = ['GFa', 'FGa', '(GFa) U b', '(a M b) W c', 'a W (b M c)', '(a U b) R c', 'a R (b U c)', '(a W b) M c', 'a M (b W c)', - ] + ] # The rewriting assume the atomic proposition will not change # once we reache the non-alive part. diff --git a/tests/python/ltlparse.py b/tests/python/ltlparse.py index 29404f0c9..f0dbc373f 100755 --- a/tests/python/ltlparse.py +++ b/tests/python/ltlparse.py @@ -44,8 +44,8 @@ for str1, isl in l: assert isl == pf.f.is_leaf() del pf -assert spot.formula('a').is_leaf(); -assert spot.formula('0').is_leaf(); +assert spot.formula('a').is_leaf() +assert spot.formula('0').is_leaf() for str1 in ['a * b', 'a xor b', 'a <-> b']: pf = spot.parse_infix_boolean(str1, e, False) @@ -84,70 +84,71 @@ assert f6.errors del f6 for (x, msg) in [('{foo[->bug]}', "treating this goto block as [->]"), - ('{foo[->', 'missing closing bracket for goto operator'), - ('{foo[->3..1]}', "reversed range"), - ('{foo[*bug]}', "treating this star block as [*]"), - ('{foo[*bug', "missing closing bracket for star"), - ('{foo[*3..1]}', "reversed range"), - ('{[*3..1]}', "reversed range"), - ('{foo[:*bug]}', "treating this fusion-star block as [:*]"), - ('{foo[:*3..1]}', "reversed range"), - ('{foo[:*bug', "missing closing bracket for fusion-star"), - ('{foo[=bug]}', "treating this equal block as [=]"), - ('{foo[=bug', "missing closing bracket for equal operator"), - ('{foo[=3..1]}', "reversed range"), - ('{()}', "treating this brace block as false"), - ('{(a b)}', "treating this parenthetical block as false"), - ('{(a*}', "missing closing parenthesis"), - ('{(a*&)}', "missing right operand for " - + "\"non-length-matching and operator\""), - ('{(a*&&)}', "missing right operand for " - + "\"length-matching and operator\""), - ('{(a*|)}', "missing right operand for \"or operator\""), - ('{a*;}', "missing right operand for \"concat operator\""), - ('{a*::b}', "missing right operand for \"fusion operator\""), - ('{a* xor }', "missing right operand for \"xor operator\""), - ('{a* -> }', "missing right operand for " - + "\"implication operator\""), - ('{a <-> <-> b }', - "missing right operand for \"equivalent operator\""), - ('{a;b b}', "ignoring this"), - ('{*', "missing closing brace"), - ('{(a', "missing closing parenthesis"), - ('{* a', "ignoring trailing garbage and missing closing brace"), - ('F(a b)', "ignoring this"), - ('F(-)', "treating this parenthetical block as false"), - ('F(', "missing closing parenthesis"), - ('F(a b', "ignoring trailing garbage and " - + "missing closing parenthesis"), - ('F(-', "missing closing parenthesis"), - ('F(-', "parenthetical block as false"), - ('a&', "missing right operand for \"and operator\""), - ('a*', "missing right operand for \"and operator\""), - ('a|', "missing right operand for \"or operator\""), - ('a^', "missing right operand for \"xor operator\""), - ('a->', "missing right operand for \"implication operator\""), - ('a<->', "missing right operand for \"equivalent operator\""), - ('!', "missing right operand for \"not operator\""), - ('a W', "missing right operand for \"weak until operator\""), - ('a U', "missing right operand for \"until operator\""), - ('a R', "missing right operand for \"release operator\""), - ('a M', "missing right operand for " - + "\"strong release operator\""), - ('{a}[]->', "missing right operand for " - + "\"universal overlapping concat operator\""), - ('{a}[]=>', "missing right operand for " - + "\"universal non-overlapping concat operator\""), - ('{a}<>->', "missing right operand for " - + "\"existential overlapping concat operator\""), - ('{a}<>=>', "missing right operand for " - + "\"existential non-overlapping concat operator\""), - ('(X)', "missing right operand for \"next operator\""), - ('("X)', "unclosed string"), - ('("X)', "missing closing parenthesis"), - ('{"X', "unclosed string"), - ('{"X}', "missing closing brace"), - ]: + ('{foo[->', 'missing closing bracket for goto operator'), + ('{foo[->3..1]}', "reversed range"), + ('{foo[*bug]}', "treating this star block as [*]"), + ('{foo[*bug', "missing closing bracket for star"), + ('{foo[*3..1]}', "reversed range"), + ('{[*3..1]}', "reversed range"), + ('{foo[:*bug]}', "treating this fusion-star block as [:*]"), + ('{foo[:*3..1]}', "reversed range"), + ('{foo[:*bug', "missing closing bracket for fusion-star"), + ('{foo[=bug]}', "treating this equal block as [=]"), + ('{foo[=bug', "missing closing bracket for equal operator"), + ('{foo[=3..1]}', "reversed range"), + ('{()}', "treating this brace block as false"), + ('{(a b)}', "treating this parenthetical block as false"), + ('{(a*}', "missing closing parenthesis"), + ('{(a*&)}', "missing right operand for " + + "\"non-length-matching and operator\""), + ('{(a*&&)}', "missing right operand for " + + "\"length-matching and operator\""), + ('{(a*|)}', "missing right operand for \"or operator\""), + ('{a*;}', "missing right operand for \"concat operator\""), + ('{a*::b}', "missing right operand for \"fusion operator\""), + ('{a* xor }', "missing right operand for \"xor operator\""), + ('{a* -> }', "missing right operand for " + + "\"implication operator\""), + ('{a <-> <-> b }', + "missing right operand for \"equivalent operator\""), + ('{a;b b}', "ignoring this"), + ('{*', "missing closing brace"), + ('{(a', "missing closing parenthesis"), + ('{* a', + "ignoring trailing garbage and missing closing brace"), + ('F(a b)', "ignoring this"), + ('F(-)', "treating this parenthetical block as false"), + ('F(', "missing closing parenthesis"), + ('F(a b', "ignoring trailing garbage and " + + "missing closing parenthesis"), + ('F(-', "missing closing parenthesis"), + ('F(-', "parenthetical block as false"), + ('a&', "missing right operand for \"and operator\""), + ('a*', "missing right operand for \"and operator\""), + ('a|', "missing right operand for \"or operator\""), + ('a^', "missing right operand for \"xor operator\""), + ('a->', "missing right operand for \"implication operator\""), + ('a<->', "missing right operand for \"equivalent operator\""), + ('!', "missing right operand for \"not operator\""), + ('a W', "missing right operand for \"weak until operator\""), + ('a U', "missing right operand for \"until operator\""), + ('a R', "missing right operand for \"release operator\""), + ('a M', "missing right operand for " + + "\"strong release operator\""), + ('{a}[]->', "missing right operand for " + + "\"universal overlapping concat operator\""), + ('{a}[]=>', "missing right operand for " + + "\"universal non-overlapping concat operator\""), + ('{a}<>->', "missing right operand for " + + "\"existential overlapping concat operator\""), + ('{a}<>=>', "missing right operand for " + + "\"existential non-overlapping concat operator\""), + ('(X)', "missing right operand for \"next operator\""), + ('("X)', "unclosed string"), + ('("X)', "missing closing parenthesis"), + ('{"X', "unclosed string"), + ('{"X}', "missing closing brace"), + ]: f7 = spot.parse_infix_psl(x) assert f7.errors ostr = spot.ostringstream() @@ -158,20 +159,20 @@ for (x, msg) in [('{foo[->bug]}', "treating this goto block as [->]"), del f7 for (x, msg) in [('a&', "missing right operand for \"and operator\""), - ('a*', "missing right operand for \"and operator\""), - ('a|', "missing right operand for \"or operator\""), - ('a^', "missing right operand for \"xor operator\""), - ('a->', "missing right operand for \"implication operator\""), - ('a<->', "missing right operand for \"equivalent operator\""), - ('(-', "parenthetical block as false"), - ('(-', "missing closing parenthesis"), - ('(-)', "treating this parenthetical block as false"), - ('(a', "missing closing parenthesis"), - ('(a b)', "ignoring this"), - ('(a b', "ignoring trailing garbage and " - + "missing closing parenthesis"), - ('!', "missing right operand for \"not operator\""), - ]: + ('a*', "missing right operand for \"and operator\""), + ('a|', "missing right operand for \"or operator\""), + ('a^', "missing right operand for \"xor operator\""), + ('a->', "missing right operand for \"implication operator\""), + ('a<->', "missing right operand for \"equivalent operator\""), + ('(-', "parenthetical block as false"), + ('(-', "missing closing parenthesis"), + ('(-)', "treating this parenthetical block as false"), + ('(a', "missing closing parenthesis"), + ('(a b)', "ignoring this"), + ('(a b', "ignoring trailing garbage and " + + "missing closing parenthesis"), + ('!', "missing right operand for \"not operator\""), + ]: f8 = spot.parse_infix_boolean(x) assert f8.errors ostr = spot.ostringstream() @@ -182,12 +183,12 @@ for (x, msg) in [('a&', "missing right operand for \"and operator\""), del f8 for (x, msg) in [('a->', "missing right operand for \"implication operator\""), - ('a<->', "missing right operand for \"equivalent operator\""), - ('(aa', "missing closing parenthesis"), - ('("aa', "missing closing parenthesis"), - ('"(aa', "unclosed string"), - ('{aa', "missing closing brace"), - ]: + ('a<->', "missing right operand for \"equivalent operator\""), + ('(aa', "missing closing parenthesis"), + ('("aa', "missing closing parenthesis"), + ('"(aa', "unclosed string"), + ('{aa', "missing closing brace"), + ]: f9 = spot.parse_infix_psl(x, spot.default_environment.instance(), False, True) assert f9.errors diff --git a/tests/python/ltlsimple.py b/tests/python/ltlsimple.py index bb3d6c206..ac9e3c426 100755 --- a/tests/python/ltlsimple.py +++ b/tests/python/ltlsimple.py @@ -23,7 +23,7 @@ import spot import sys -#---------------------------------------------------------------------- +# ---------------------------------------------------------------------- a = spot.formula.ap('a') b = spot.formula.ap('b') c = spot.formula.ap('c') @@ -31,7 +31,7 @@ c2 = spot.formula.ap('c') assert c == c2 -op = spot.formula.And([a, b]) +op = spot.formula.And([a, b]) op2 = spot.formula.And([op, c]) op3 = spot.formula.And([a, c, b]) @@ -55,7 +55,7 @@ assert op4 == op2 del op2, op3, op4 -#---------------------------------------------------------------------- +# ---------------------------------------------------------------------- a = spot.formula.ap('a') b = spot.formula.ap('b') c = spot.formula.ap('c') @@ -65,14 +65,15 @@ F = spot.formula.ff() f1 = spot.formula.Equiv(c, a) f2 = spot.formula.Implies(a, b) f3 = spot.formula.Xor(b, c) -f4 = spot.formula.Not(f3); del f3 +f4 = spot.formula.Not(f3) +del f3 f5 = spot.formula.Xor(F, c) del a, b, c, T, F, f1, f2, f4, f5 assert spot.fnode_instances_check() -#---------------------------------------------------------------------- +# ---------------------------------------------------------------------- assert str([str(x) for x in spot.formula('a &b & c')]) == "['a', 'b', 'c']" @@ -83,18 +84,23 @@ def switch_g_f(x): return spot.formula.G(switch_g_f(x[0])) return x.map(switch_g_f) + f = spot.formula('GFa & XFGb & Fc & G(a | b | Fd)') assert str(switch_g_f(f)) == 'FGa & XGFb & Gc & F(a | b | Gd)' x = 0 + + def count_g(f): global x if f._is(spot.op_G): x += 1 + + f.traverse(count_g) assert x == 3 -#---------------------------------------------------------------------- +# ---------------------------------------------------------------------- # The example from tut01.org @@ -106,7 +112,7 @@ Spin syntax: {f:s} Default for shell: echo {f:q} | ... LBT for shell: echo {f:lq} | ... Default for CSV: ...,{f:c},... -Wring, centered: {f:w:~^50}""".format(f = formula) +Wring, centered: {f:w:~^50}""".format(f=formula) assert res == """\ Default output: a U (b U "$strange[0]=name") @@ -135,10 +141,13 @@ for (input, output) in [('(a&b)<->b', 'b->(a&b)'), assert(f == output) assert(spot.are_equivalent(input, output)) + def myparse(input): env = spot.default_environment.instance() pf = spot.parse_infix_psl(input, env) return pf.f + + # This used to fail, because myparse would return a pointer # to pf.f inside the destroyed pf. assert myparse('a U b') == spot.formula('a U b') diff --git a/tests/python/relabel.py b/tests/python/relabel.py index 344581ca1..5a4a370eb 100644 --- a/tests/python/relabel.py +++ b/tests/python/relabel.py @@ -37,7 +37,7 @@ assert h == f autg = g.translate() spot.relabel_here(autg, m) assert str(autg.ap()) == \ - '(spot.formula("a"), spot.formula("b"), spot.formula("c"))' + '(spot.formula("a"), spot.formula("b"), spot.formula("c"))' assert spot.isomorphism_checker.are_isomorphic(autg, f.translate()) a = spot.formula('a') diff --git a/tests/python/rs_like.py b/tests/python/rs_like.py index d08225b09..7b4ee75cf 100644 --- a/tests/python/rs_like.py +++ b/tests/python/rs_like.py @@ -27,32 +27,39 @@ m2 = spot.mark_t([2]) m3 = spot.mark_t([3]) mall = spot.mark_t() + def test_rs(acc, rs, expected_res, expected_pairs): - res, p = getattr(acc, 'is_' + rs + '_like')() - assert res == expected_res - if expected_res: - expected_pairs.sort() - p = sorted(p) - for a,b in zip (p, expected_pairs): - assert a.fin == b.fin and a.inf == b.inf + res, p = getattr(acc, 'is_' + rs + '_like')() + assert res == expected_res + if expected_res: + expected_pairs.sort() + p = sorted(p) + for a, b in zip(p, expected_pairs): + assert a.fin == b.fin and a.inf == b.inf + def switch_pairs(pairs): - if pairs == None: - return None - r = [] - for p in pairs: - r.append(spot.rs_pair(p.inf, p.fin)) - return r + if pairs == None: + return None + r = [] + for p in pairs: + r.append(spot.rs_pair(p.inf, p.fin)) + return r + def test_streett(acc, expected_streett_like, expected_pairs): - test_rs(acc, 'streett', expected_streett_like, expected_pairs) - o_acc = spot.acc_cond(acc.get_acceptance().complement()) - test_rs(o_acc, 'rabin', expected_streett_like, switch_pairs(expected_pairs)) + test_rs(acc, 'streett', expected_streett_like, expected_pairs) + o_acc = spot.acc_cond(acc.get_acceptance().complement()) + test_rs(o_acc, 'rabin', expected_streett_like, + switch_pairs(expected_pairs)) + def test_rabin(acc, expected_rabin_like, expected_pairs): - test_rs(acc, 'rabin', expected_rabin_like, expected_pairs) - o_acc = spot.acc_cond(acc.get_acceptance().complement()) - test_rs(o_acc, 'streett', expected_rabin_like, switch_pairs(expected_pairs)) + test_rs(acc, 'rabin', expected_rabin_like, expected_pairs) + o_acc = spot.acc_cond(acc.get_acceptance().complement()) + test_rs(o_acc, 'streett', expected_rabin_like, + switch_pairs(expected_pairs)) + acc = spot.acc_cond(spot.acc_code('Fin(0)')) test_streett(acc, True, [spot.rs_pair(m0, mall)]) @@ -75,12 +82,12 @@ test_streett(acc, True, [spot.rs_pair(m0, m1), spot.rs_pair(m0, m2)]) acc = spot.acc_cond(spot.acc_code('(Fin(0)|Inf(1))&(Fin(1)|Inf(2))')) test_streett(acc, True, [spot.rs_pair(m0, m1), spot.rs_pair(m1, m2)]) -acc = spot.acc_cond(spot.acc_code('(Fin(0)|Inf(1))&(Fin(1)|Inf(2))'\ +acc = spot.acc_cond(spot.acc_code('(Fin(0)|Inf(1))&(Fin(1)|Inf(2))' '&(Fin(3)&Inf(3))')) -test_streett(acc, True, [spot.rs_pair(m0, m1), spot.rs_pair(m1, m2),\ - spot.rs_pair(m3, mall), spot.rs_pair(mall, m3)]) +test_streett(acc, True, [spot.rs_pair(m0, m1), spot.rs_pair(m1, m2), + spot.rs_pair(m3, mall), spot.rs_pair(mall, m3)]) -acc = spot.acc_cond(spot.acc_code('(Fin(0)|Inf(1))&(Fin(1)|Inf(2))'\ +acc = spot.acc_cond(spot.acc_code('(Fin(0)|Inf(1))&(Fin(1)|Inf(2))' '&(Fin(3)&Inf(3))&(Fin(4)|Inf(5)|Inf(6))')) test_streett(acc, False, None) @@ -102,13 +109,11 @@ test_rabin(acc, True, [spot.rs_pair(m0, m1), spot.rs_pair(m0, m2)]) acc = spot.acc_cond(spot.acc_code('(Fin(0)&Inf(1))|(Fin(1)&Inf(2))')) test_rabin(acc, True, [spot.rs_pair(m0, m1), spot.rs_pair(m1, m2)]) -acc = spot.acc_cond(spot.acc_code('(Fin(0)&Inf(1))|(Fin(1)&Inf(2))'\ +acc = spot.acc_cond(spot.acc_code('(Fin(0)&Inf(1))|(Fin(1)&Inf(2))' '|(Fin(3)|Inf(3))')) -test_rabin(acc, True, [spot.rs_pair(m0, m1), spot.rs_pair(m1, m2),\ - spot.rs_pair(m3, mall), spot.rs_pair(mall, m3)]) +test_rabin(acc, True, [spot.rs_pair(m0, m1), spot.rs_pair(m1, m2), + spot.rs_pair(m3, mall), spot.rs_pair(mall, m3)]) -acc = spot.acc_cond(spot.acc_code('(Fin(0)&Inf(1))|(Fin(1)&Inf(2))'\ +acc = spot.acc_cond(spot.acc_code('(Fin(0)&Inf(1))|(Fin(1)&Inf(2))' '|(Fin(3)|Inf(3))|(Fin(4)&Inf(5)&Inf(6))')) test_rabin(acc, False, None) - - diff --git a/tests/python/sccsplit.py b/tests/python/sccsplit.py index cf8c0e33d..9095a1a29 100644 --- a/tests/python/sccsplit.py +++ b/tests/python/sccsplit.py @@ -26,5 +26,5 @@ s = "" for aut2 in si.split_on_sets(0, [0]): # This call to to_str() used to fail because split_on_sets had not # registered the atomic propositions of aut - s += aut2.to_str(); + s += aut2.to_str() assert spot.automaton(s).num_states() == 8 diff --git a/tests/python/semidet.py b/tests/python/semidet.py index 022713f3e..856b3b7d2 100644 --- a/tests/python/semidet.py +++ b/tests/python/semidet.py @@ -24,7 +24,7 @@ formulas = [('(Gp0 | Fp1) M 1', False, True), ('(p1 | (Fp0 R (p1 W p0))) M 1', True, True), ('!G(F(p1 & Fp0) W p1)', False, True), ('X(!p0 W Xp1)', False, False), - ('FG(p0)', False, True) ] + ('FG(p0)', False, True)] for f, isd, issd in formulas: print(f) diff --git a/tests/python/setacc.py b/tests/python/setacc.py index cc09c40c1..f614d2439 100644 --- a/tests/python/setacc.py +++ b/tests/python/setacc.py @@ -24,9 +24,9 @@ import spot # Test case reduced from a report from Juraj Major . a = spot.make_twa_graph(spot._bdd_dict) a.set_acceptance(0, spot.acc_code("t")) -assert(a.prop_state_acc() == True); +assert(a.prop_state_acc() == True) a.set_acceptance(1, spot.acc_code("Fin(0)")) -assert(a.prop_state_acc() == spot.trival.maybe()); +assert(a.prop_state_acc() == spot.trival.maybe()) # Some tests for used_inf_fin_sets(), which return a pair of mark_t. @@ -34,8 +34,8 @@ assert(a.prop_state_acc() == spot.trival.maybe()); assert inf == [] assert fin == [0] (inf, fin) = spot.acc_code("(Fin(0)|Inf(1))&Fin(2)&Inf(0)").used_inf_fin_sets() -assert inf == [0,1] -assert fin == [0,2] +assert inf == [0, 1] +assert fin == [0, 2] # is_rabin_like() returns (bool, [(inf, fin), ...]) (b, v) = spot.acc_cond("(Fin(0)&Inf(1))|(Fin(2)&Inf(0))").is_rabin_like() @@ -51,7 +51,7 @@ assert len(v) == 0 (b, v) = spot.acc_cond("(Fin(0)|Inf(1))&(Fin(2)|Inf(0))").is_streett_like() assert b == True assert repr(v) == \ - '(spot.rs_pair(fin=[0], inf=[1]), spot.rs_pair(fin=[2], inf=[0]))' + '(spot.rs_pair(fin=[0], inf=[1]), spot.rs_pair(fin=[2], inf=[0]))' v2 = (spot.rs_pair(fin=[0], inf=[1]), spot.rs_pair(fin=[2], inf=[0])) assert v == v2 diff --git a/tests/python/setxor.py b/tests/python/setxor.py index 66f93c81a..7cd1e5da1 100755 --- a/tests/python/setxor.py +++ b/tests/python/setxor.py @@ -25,25 +25,25 @@ bdd_setvarnum(5) V = [bdd_ithvar(i) for i in range(5)] -a = V[0] & -V[1] & V[2] & -V[3] -b = V[0] & V[1] & V[2] & -V[3] -c = -V[0] & V[1] & -V[2] & -V[3] +a = V[0] & -V[1] & V[2] & -V[3] +b = V[0] & V[1] & V[2] & -V[3] +c = -V[0] & V[1] & -V[2] & -V[3] -assert(c == bdd_setxor(a,b)) -assert(c == bdd_setxor(b,a)) -assert(a == bdd_setxor(b,c)) -assert(a == bdd_setxor(c,b)) -assert(b == bdd_setxor(a,c)) -assert(b == bdd_setxor(c,a)) +assert(c == bdd_setxor(a, b)) +assert(c == bdd_setxor(b, a)) +assert(a == bdd_setxor(b, c)) +assert(a == bdd_setxor(c, b)) +assert(b == bdd_setxor(a, c)) +assert(b == bdd_setxor(c, a)) -d = V[1] & V[2] & -V[3] & V[4] -e = V[0] & V[1] & -V[2] & -V[3] & V[4] +d = V[1] & V[2] & -V[3] & V[4] +e = V[0] & V[1] & -V[2] & -V[3] & V[4] -assert(e == bdd_setxor(a,d)) -assert(e == bdd_setxor(d,a)) +assert(e == bdd_setxor(a, d)) +assert(e == bdd_setxor(d, a)) # Cleanup all BDD variables before calling bdd_done(), otherwise # bdd_delref will be called after bdd_done() and this is unsafe in # optimized builds. -V = a = b = c = d = e = 0; +V = a = b = c = d = e = 0 bdd_done() diff --git a/tests/python/split.py b/tests/python/split.py index 7aab05038..51a7b40d9 100644 --- a/tests/python/split.py +++ b/tests/python/split.py @@ -19,10 +19,14 @@ import spot -def incl(a,b): + +def incl(a, b): return not b.intersects(spot.dualize(spot.tgba_determinize(a))) -def equiv(a,b): - return incl(a,b) and incl(b,a) + + +def equiv(a, b): + return incl(a, b) and incl(b, a) + def do_split(f, in_list): aut = spot.translate(f) @@ -30,7 +34,8 @@ def do_split(f, in_list): for a in in_list: inputs &= spot.buddy.bdd_ithvar(aut.get_dict().varnum(spot.formula(a))) s = spot.split_2step(aut, inputs) - return aut,s + return aut, s + aut, s = do_split('(FG !a) <-> (GF b)', ['a']) assert equiv(aut, spot.unsplit_2step(s)) @@ -58,46 +63,45 @@ State: 2 --END--""" aut, s = do_split('! ((G (req -> (F ack))) && (G (go -> (F grant))))', ['go', - 'req']) + 'req']) assert equiv(aut, spot.unsplit_2step(s)) # FIXME s.to_str() is NOT the same on Debian stable and on Debian unstable # we should investigate this -#assert s.to_str() == """HOA: v1 -#States: 9 -#Start: 0 -#AP: 4 "ack" "req" "go" "grant" -#acc-name: Buchi -#Acceptance: 1 Inf(0) -#properties: trans-labels explicit-labels state-acc -#--BODY-- -#State: 0 -#[1&!2] 3 -#[!1&!2] 4 -#[1&2] 5 -#[!1&2] 6 -#State: 1 -#[t] 7 -#State: 2 -#[t] 8 -#State: 3 -#[t] 0 -#[!0] 1 -#State: 4 -#[t] 0 -#State: 5 -#[t] 0 -#[!0] 1 -#[!3] 2 -#State: 6 -#[t] 0 -#[!3] 2 -#State: 7 {0} -#[!0] 1 -#State: 8 {0} -#[!3] 2 -#--END--""" +# assert s.to_str() == """HOA: v1 +# States: 9 +# Start: 0 +# AP: 4 "ack" "req" "go" "grant" +# acc-name: Buchi +# Acceptance: 1 Inf(0) +# properties: trans-labels explicit-labels state-acc +# --BODY-- +# State: 0 +# [1&!2] 3 +# [!1&!2] 4 +# [1&2] 5 +# [!1&2] 6 +# State: 1 +# [t] 7 +# State: 2 +# [t] 8 +# State: 3 +# [t] 0 +# [!0] 1 +# State: 4 +# [t] 0 +# State: 5 +# [t] 0 +# [!0] 1 +# [!3] 2 +# State: 6 +# [t] 0 +# [!3] 2 +# State: 7 {0} +# [!0] 1 +# State: 8 {0} +# [!3] 2 +# --END--""" aut, s = do_split('((G (((! g_0) || (! g_1)) && ((r_0 && (X r_1)) -> (F (g_0 \ && g_1))))) && (G (r_0 -> F g_0))) && (G (r_1 -> F g_1))', ['r_0', 'r_1']) assert equiv(aut, spot.unsplit_2step(s)) - diff --git a/tests/python/streett_totgba.py b/tests/python/streett_totgba.py index 7e1083a4e..65c1c256e 100644 --- a/tests/python/streett_totgba.py +++ b/tests/python/streett_totgba.py @@ -23,27 +23,29 @@ import os import shutil import sys + def tgba(a): - if not a.is_existential(): - a = spot.remove_alternation(a) - a = spot.to_generalized_buchi(a) - return a + if not a.is_existential(): + a = spot.remove_alternation(a) + a = spot.to_generalized_buchi(a) + return a + def test_aut(aut): - stgba = tgba(aut) - assert stgba.equivalent_to(aut) - os.environ["SPOT_STREETT_CONV_MIN"] = '1' - sftgba = tgba(aut) - del os.environ["SPOT_STREETT_CONV_MIN"] - assert stgba.equivalent_to(sftgba) + stgba = tgba(aut) + assert stgba.equivalent_to(aut) + os.environ["SPOT_STREETT_CONV_MIN"] = '1' + sftgba = tgba(aut) + del os.environ["SPOT_STREETT_CONV_MIN"] + assert stgba.equivalent_to(sftgba) - slike = spot.simplify_acceptance(aut) + slike = spot.simplify_acceptance(aut) - sltgba = tgba(slike) - os.environ["SPOT_STREETT_CONV_MIN"] = "1" - slftgba = tgba(slike) - del os.environ["SPOT_STREETT_CONV_MIN"] - assert sltgba.equivalent_to(slftgba) + sltgba = tgba(slike) + os.environ["SPOT_STREETT_CONV_MIN"] = "1" + slftgba = tgba(slike) + del os.environ["SPOT_STREETT_CONV_MIN"] + assert sltgba.equivalent_to(slftgba) # Those automata are generated with ltl2dstar, which is NOT part of spot, # using the following command: @@ -51,11 +53,12 @@ def test_aut(aut): # ltldo "ltl2dstar --automata=streett --output-format=hoa\ # --ltl2nba=spin:ltl2tgba@-s %L ->%O" -F- --name=%f -H" + if shutil.which('ltl2dstar') is None: - sys.exit(77) + sys.exit(77) for a in spot.automata('genltl --eh-patterns --dac-patterns --hkrss-patterns\ --sb-patterns |\ ltldo "ltl2dstar --automata=streett --output-format=hoa\ --ltl2nba=spin:ltl2tgba@-s %L ->%O"\ -T5 -F- --name=%f -H|'): - test_aut(a) + test_aut(a) diff --git a/tests/python/stutter.py b/tests/python/stutter.py index 3b1079000..48240f940 100644 --- a/tests/python/stutter.py +++ b/tests/python/stutter.py @@ -24,6 +24,7 @@ import spot + def explain_stut(f): f = spot.formula(f) pos = spot.translate(f) @@ -41,6 +42,7 @@ def explain_stut(f): word2.simplify() return(word, word2) + # Test from issue #388 w1, w2 = explain_stut('{(a:b) | (a;b)}|->Gc') assert str(w1) == 'a & !b & !c; cycle{!a & b & !c}' diff --git a/tests/python/sum.py b/tests/python/sum.py index cafc0a963..af59e1a44 100644 --- a/tests/python/sum.py +++ b/tests/python/sum.py @@ -46,37 +46,39 @@ rg = spot.randltlgenerator(2, opts) dict = spot.make_bdd_dict() + def produce_phi(rg, n): - phi = [] - while len(phi) < n: - f = rg.next() - if f.is_syntactic_persistence(): - phi.append(f) - return phi + phi = [] + while len(phi) < n: + f = rg.next() + if f.is_syntactic_persistence(): + phi.append(f) + return phi + phi1 = produce_phi(rg, 1000) phi2 = produce_phi(rg, 1000) inputres = [] aut = [] for p in zip(phi1, phi2): - inputres.append(spot.formula.Or(p)) - a1 = spot.ltl_to_tgba_fm(p[0], dict) - a2 = spot.ltl_to_tgba_fm(p[1], dict) - aut.append(spot.to_generalized_buchi( \ - spot.remove_alternation(spot.sum(a1, a2), True))) + inputres.append(spot.formula.Or(p)) + a1 = spot.ltl_to_tgba_fm(p[0], dict) + a2 = spot.ltl_to_tgba_fm(p[1], dict) + aut.append(spot.to_generalized_buchi( + spot.remove_alternation(spot.sum(a1, a2), True))) for p in zip(aut, inputres): - assert p[0].equivalent_to(p[1]) + assert p[0].equivalent_to(p[1]) aut = [] inputres = [] for p in zip(phi1, phi2): - inputres.append(spot.formula.And(p)) - a1 = spot.ltl_to_tgba_fm(p[0], dict) - a2 = spot.ltl_to_tgba_fm(p[1], dict) - aut.append(spot.to_generalized_buchi( \ - spot.remove_alternation(spot.sum_and(a1, a2), True))) + inputres.append(spot.formula.And(p)) + a1 = spot.ltl_to_tgba_fm(p[0], dict) + a2 = spot.ltl_to_tgba_fm(p[1], dict) + aut.append(spot.to_generalized_buchi( + spot.remove_alternation(spot.sum_and(a1, a2), True))) for p in zip(aut, inputres): - assert p[0].equivalent_to(p[1]) + assert p[0].equivalent_to(p[1]) diff --git a/tests/python/toparity.py b/tests/python/toparity.py index bd62baafd..e714a72d7 100644 --- a/tests/python/toparity.py +++ b/tests/python/toparity.py @@ -46,6 +46,6 @@ for f in spot.randltl(5, 2000): assert spot.are_equivalent(n, p) # Issue #390. -a = spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det'); -b = spot.to_parity(a); +a = spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det') +b = spot.to_parity(a) assert a.equivalent_to(b) diff --git a/tests/python/toweak.py b/tests/python/toweak.py index 0510a6850..550ab6408 100644 --- a/tests/python/toweak.py +++ b/tests/python/toweak.py @@ -29,11 +29,13 @@ GF!b (b & GF!b) | (!b & FGb) b | (a & XF(b R a)) | (!a & XG(!b U !a))""" + def test_phi(phi): - a = spot.translate(phi, 'TGBA', 'SBAcc') + a = spot.translate(phi, 'TGBA', 'SBAcc') res = spot.to_weak_alternating(spot.dualize(a)) assert res.equivalent_to(spot.formula.Not(spot.formula(phi))) + for p in phi1.split('\n'): print(p) test_phi(p) diff --git a/tests/python/trival.py b/tests/python/trival.py index f9274e630..8fcf6a1fa 100644 --- a/tests/python/trival.py +++ b/tests/python/trival.py @@ -39,9 +39,9 @@ assert v4 == spot.trival(spot.trival.maybe_value) assert v3 assert -v2 assert not -v1 -assert not v1; +assert not v1 assert not -v3 for u in (v1, v2, v3): - for v in (v1, v2, v3): - assert (u & v) == -(-u | -v) + for v in (v1, v2, v3): + assert (u & v) == -(-u | -v)