python: cleanup with autopep8
* tests/python/341.py, tests/python/alarm.py, tests/python/bdddict.py, tests/python/bddnqueen.py, tests/python/bugdet.py, tests/python/dualize.py, tests/python/except.py, tests/python/gen.py, tests/python/genem.py, tests/python/implies.py, tests/python/interdep.py, tests/python/ipnbdoctest.py, tests/python/kripke.py, tests/python/ltl2tgba.py, tests/python/ltlf.py, tests/python/ltlparse.py, tests/python/ltlsimple.py, tests/python/relabel.py, tests/python/rs_like.py, tests/python/sccsplit.py, tests/python/semidet.py, tests/python/setacc.py, tests/python/setxor.py, tests/python/split.py, tests/python/streett_totgba.py, tests/python/stutter.py, tests/python/sum.py, tests/python/toparity.py, tests/python/toweak.py, tests/python/trival.py, python/spot/__init__.py, python/spot/aux.py, python/spot/jupyter.py: Reformat with autopep8. fixup! * spot/tl/simplify.cc: Fix typos in tracing code.
This commit is contained in:
Alexandre Duret-Lutz
parent
5b01ce32dd
commit
822fe77891
33 changed files with 444 additions and 356 deletions
|
|
@ -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='''<g transform="translate({})">
|
||||
highlight = '''<g transform="translate({})">
|
||||
<line x1="-10" y1="-10" x2="10" y2="10" stroke="red" stroke-width="5" />
|
||||
<line x1="-10" y1="10" x2="10" y2="-10" stroke="red" stroke-width="5" />
|
||||
</g>'''.format(coords[cl])
|
||||
else:
|
||||
highlight=''
|
||||
highlight = ''
|
||||
return '''
|
||||
<svg height="210" width="220" xmlns="http://www.w3.org/2000/svg" version="1.1">
|
||||
<polygon points="20,0 200,120 200,210 20,210" fill="cyan" opacity=".2" />
|
||||
|
|
@ -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 = '''
|
||||
<svg height="{h3}" width="{w}" xmlns="http://www.w3.org/2000/svg" version="1.1">
|
||||
<rect x="0" y="0" width="{w}" height="{height}" fill="{bgcolor}"/>
|
||||
|
|
@ -1236,11 +1250,11 @@ class twa_word:
|
|||
if cur != 0:
|
||||
if last == -cur:
|
||||
txt += \
|
||||
('<line x1="{x}" y1="{y1}" x2="{x}" y2="{y2}" {red}/>'
|
||||
('<line x1="{x}" y1="{y1}" x2="{x}" y2="{y2}" {red}/>'
|
||||
.format(x=xpos*50, y1=ypos*50+5,
|
||||
y2=ypos*50+45, **d))
|
||||
txt += \
|
||||
('<line x1="{x1}" y1="{y}" x2="{x2}" y2="{y}" {red}/>'
|
||||
('<line x1="{x1}" y1="{y}" x2="{x2}" y2="{y}" {red}/>'
|
||||
.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()
|
||||
|
|
|
|||
|
|
@ -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()
|
||||
|
|
|
|||
|
|
@ -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 += ("<div style='vertical-align:text-top;display:{};{}'>{}</div>"
|
||||
.format(dpy, width, rep))
|
||||
.format(dpy, width, rep))
|
||||
display(HTML(res))
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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 ||
|
||||
|
|
|
|||
|
|
@ -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")
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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:
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
||||
|
|
|
|||
|
|
@ -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])
|
||||
|
|
|
|||
|
|
@ -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()
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -28,6 +28,7 @@ import sys
|
|||
import getopt
|
||||
import spot
|
||||
|
||||
|
||||
def usage(prog):
|
||||
sys.stderr.write("""Usage: %s [OPTIONS...] formula
|
||||
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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')
|
||||
|
|
|
|||
|
|
@ -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')
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -24,9 +24,9 @@ import spot
|
|||
# Test case reduced from a report from Juraj Major <major@fi.muni.cz>.
|
||||
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
|
||||
|
||||
|
|
|
|||
|
|
@ -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()
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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}'
|
||||
|
|
|
|||
|
|
@ -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])
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue