python: simplify to_parity() interface
* python/spot/__init__.py (to_parity): Iterate over the attributes of spot.to_parity_options instead of naming each option explicitely, also accept a to_parity_options() instance as argument. * tests/python/toparity.py: Add tests for both styles of calls, and reduce the number of random tests to lower the run time of this test.
This commit is contained in:
Alexandre Duret-Lutz
parent
1750c0fb6d
commit
1db319267f
2 changed files with 50 additions and 60 deletions
|
|
@ -1292,28 +1292,22 @@ class scc_and_mark_filter:
|
|||
self.restore_acceptance()
|
||||
|
||||
|
||||
def to_parity(aut, **kwargs):
|
||||
option = to_parity_options()
|
||||
if "search_ex" in kwargs:
|
||||
option.search_ex = kwargs.get("search_ex")
|
||||
if "use_last" in kwargs:
|
||||
option.use_last = kwargs.get("use_last")
|
||||
if "force_order" in kwargs:
|
||||
option.force_order = kwargs.get("force_order")
|
||||
if "partial_degen" in kwargs:
|
||||
option.partial_degen = kwargs.get("partial_degen")
|
||||
if "acc_clean" in kwargs:
|
||||
option.acc_clean = kwargs.get("acc_clean")
|
||||
if "parity_equiv" in kwargs:
|
||||
option.parity_equiv = kwargs.get("parity_equiv")
|
||||
if "parity_prefix" in kwargs:
|
||||
option.parity_prefix = kwargs.get("parity_prefix")
|
||||
if "rabin_to_buchi" in kwargs:
|
||||
option.rabin_to_buchi = kwargs.get("rabin_to_buchi")
|
||||
if "reduce_col_deg" in kwargs:
|
||||
option.reduce_col_deg = kwargs.get("reduce_col_deg")
|
||||
if "propagate_col" in kwargs:
|
||||
option.propagate_col = kwargs.get("propagate_col")
|
||||
if "pretty_print" in kwargs:
|
||||
option.pretty_print = kwargs.get("pretty_print")
|
||||
return impl.to_parity(aut, option)
|
||||
def to_parity(aut, options = to_parity_options(), **kwargs):
|
||||
"""Convert aut into a parity acceptance.
|
||||
|
||||
This procedure combines multiple strategies to attempt to
|
||||
produce a small parity automaton. The resulting parity
|
||||
acceptance is either "max odd" or "max even".
|
||||
|
||||
The default optimization options maybe altered by passing either an
|
||||
instance of to_parity_options object as options argument, or by
|
||||
passing additional kwargs that will be used to update options.
|
||||
|
||||
Note that if you pass both your own options object and kwargs,
|
||||
options will be updated in place.
|
||||
"""
|
||||
if kwargs:
|
||||
for key,val in to_parity_options.__dict__.items():
|
||||
if not key.startswith('_') and key != "thisown" and key in kwargs:
|
||||
setattr(options, key, kwargs.get(key))
|
||||
return impl.to_parity(aut, options)
|
||||
|
|
|
|||
|
|
@ -89,28 +89,29 @@ options = [
|
|||
]
|
||||
|
||||
|
||||
def test(aut):
|
||||
global i
|
||||
def test(aut, full=True):
|
||||
for opt in options:
|
||||
try:
|
||||
p = spot.to_parity(aut,
|
||||
search_ex = opt.search_ex,
|
||||
use_last = opt.use_last,
|
||||
force_order = opt.force_order,
|
||||
partial_degen = opt.partial_degen,
|
||||
acc_clean = opt.acc_clean,
|
||||
parity_equiv = opt.parity_equiv,
|
||||
parity_prefix = opt.parity_prefix,
|
||||
rabin_to_buchi = opt.rabin_to_buchi,
|
||||
reduce_col_deg = opt.reduce_col_deg,
|
||||
propagate_col = opt.propagate_col,
|
||||
pretty_print = opt.pretty_print,
|
||||
)
|
||||
assert(spot.are_equivalent(aut, p))
|
||||
except:
|
||||
# are_equivalent can raise exception
|
||||
assert(False)
|
||||
|
||||
p1 = spot.to_parity(aut,
|
||||
search_ex = opt.search_ex,
|
||||
use_last = opt.use_last,
|
||||
force_order = opt.force_order,
|
||||
partial_degen = opt.partial_degen,
|
||||
acc_clean = opt.acc_clean,
|
||||
parity_equiv = opt.parity_equiv,
|
||||
parity_prefix = opt.parity_prefix,
|
||||
rabin_to_buchi = opt.rabin_to_buchi,
|
||||
reduce_col_deg = opt.reduce_col_deg,
|
||||
propagate_col = opt.propagate_col,
|
||||
pretty_print = opt.pretty_print,
|
||||
)
|
||||
assert spot.are_equivalent(aut, p1)
|
||||
if full:
|
||||
# Make sure passing opt is the same as setting
|
||||
# each argument individually
|
||||
p2 = spot.to_parity(aut, opt)
|
||||
assert p2.num_states() == p1.num_states()
|
||||
assert p2.num_edges() == p1.num_edges()
|
||||
assert p2.num_sets() == p1.num_sets()
|
||||
|
||||
test(spot.automaton("""HOA: v1
|
||||
name: "(FGp0 & ((XFp0 & F!p1) | F(Gp1 & XG!p0))) | G(F!p0 & (XFp0 | F!p1) &
|
||||
|
|
@ -210,22 +211,13 @@ State: 1
|
|||
[!0&!1] 1 {0 3}
|
||||
--END--"""))
|
||||
|
||||
test(spot.automaton("""
|
||||
HOA: v1 States: 6 Start: 0 AP: 2 "p0" "p1" Acceptance: 6 Inf(5) |
|
||||
Fin(2) | Inf(1) | (Inf(0) & Fin(3)) | Inf(4) properties: trans-labels
|
||||
explicit-labels trans-acc --BODY-- State: 0 [0&1] 2 {4 5} [0&1] 4 {0 4}
|
||||
[!0&!1] 3 {3 5} State: 1 [0&!1] 3 {1 5} [!0&!1] 5 {0 1} State: 2 [!0&!1]
|
||||
0 {0 3} [0&!1] 1 {0} State: 3 [!0&1] 4 {1 2 3} [0&1] 3 {3 4 5} State:
|
||||
4 [!0&!1] 1 {2 4} State: 5 [!0&1] 4 --END--
|
||||
"""))
|
||||
|
||||
for f in spot.randltl(15, 2000):
|
||||
test(spot.translate(f, "det", "G"))
|
||||
for i,f in enumerate(spot.randltl(10, 400)):
|
||||
test(spot.translate(f, "det", "G"), full=(i<100))
|
||||
|
||||
for f in spot.randltl(5, 25000):
|
||||
test(spot.translate(f))
|
||||
for f in spot.randltl(5, 2500):
|
||||
test(spot.translate(f), full=False)
|
||||
|
||||
test(spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det'))
|
||||
|
||||
test(spot.automaton("""
|
||||
HOA: v1
|
||||
|
|
@ -317,7 +309,7 @@ State: 1
|
|||
"""))
|
||||
|
||||
|
||||
# Tests for the old version of to_parity (CAR)
|
||||
# Tests both the old and new version of to_parity
|
||||
a = spot.automaton("""HOA: v1
|
||||
States: 1
|
||||
Start: 0
|
||||
|
|
@ -332,6 +324,7 @@ State: 0
|
|||
--END--""")
|
||||
p = spot.to_parity_old(a, True)
|
||||
assert spot.are_equivalent(a, p)
|
||||
test(a)
|
||||
|
||||
a = spot.automaton("""
|
||||
HOA: v1 States: 6 Start: 0 AP: 2 "p0" "p1" Acceptance: 6 Inf(5) |
|
||||
|
|
@ -344,6 +337,8 @@ explicit-labels trans-acc --BODY-- State: 0 [0&1] 2 {4 5} [0&1] 4 {0 4}
|
|||
p = spot.to_parity_old(a, True)
|
||||
assert p.num_states() == 22
|
||||
assert spot.are_equivalent(a, p)
|
||||
test(a)
|
||||
assert spot.to_parity(a).num_states() == 6
|
||||
|
||||
for f in spot.randltl(4, 400):
|
||||
d = spot.translate(f, "det", "G")
|
||||
|
|
@ -359,3 +354,4 @@ for f in spot.randltl(5, 2000):
|
|||
a = spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det')
|
||||
b = spot.to_parity_old(a, True)
|
||||
assert a.equivalent_to(b)
|
||||
test(a)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue