diff --git a/python/spot/__init__.py b/python/spot/__init__.py index dfd01dad1..9c3c92f67 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -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) diff --git a/tests/python/toparity.py b/tests/python/toparity.py index 78cb2afc0..d6159ae83 100644 --- a/tests/python/toparity.py +++ b/tests/python/toparity.py @@ -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)