Commit fd0d752b authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

to_parity: only call reduce_parity() when prefix_parity is enabled

Calling reduce_parity() in to_parity() is confusing, because then
running to_parity() on one SCC does not necessarily produce the same
output as running to_parity() on the entire automaton.  However it is
necessary for the implementation of parity_prefix.  As a compromise,
disable reduce_parity() when parity_prefix is disabled, this way we
can use that to demonstrate how the algorithm works.

* spot/twaalgos/toparity.hh, spot/twaalgos/toparity.cc: Do not
call reduce_parity() when parity_prefix is disabled.
* tests/python/toparity.py: Adjust.
parent 102ef043
Pipeline #18173 passed with stages
in 128 minutes and 55 seconds
......@@ -1679,13 +1679,25 @@ run()
res_->set_init_state(initial_state_res->second);
else
res_->new_state();
res_->set_acceptance(
acc_cond::acc_code::parity_max(is_odd, SPOT_MAX_ACCSETS));
if (options.pretty_print)
res_->set_named_prop("state-names", names);
reduce_parity_here(res_);
res_->purge_unreachable_states();
// res_->merge_states();
// If parity_prefix is used, we use all available colors by
// default: The IAR/CAR are using lower indices, and the prefix is
// using the upper indices. So we use reduce_parity() to clear
// the mess. If parity_prefix is not used,
unsigned max_color = SPOT_MAX_ACCSETS;
if (!options.parity_prefix)
{
acc_cond::mark_t all = {};
for (auto& e: res_->edges())
all |= e.acc;
max_color = all.max_set();
}
res_->set_acceptance(acc_cond::acc_code::parity_max(is_odd, max_color));
if (options.parity_prefix)
reduce_parity_here(res_);
return res_;
}
......
......@@ -31,16 +31,16 @@ namespace spot
/// several elements in a record, it tries to find an order such
/// that the new permutation already exists.
bool search_ex = true;
/// If \a use_last is true and \a search_ex are true, we use the
/// If \c use_last is true and \a search_ex are true, we use the
/// most recent state when we find multiple existing state
/// compatible with the current move.
bool use_last = true;
/// If \a force_order is true, we force to use an order when CAR or IAR is
bool use_last = true;
/// If \c force_order is true, we force to use an order when CAR or IAR is
/// applied. Given a state s and a set E ({0}, {0 1}, {2} for example) we
/// construct an order on colors. With the given example, we ask to have
/// a permutation that start with [0 …], [0 1 …] or [2 …] in
/// that order of preference.
bool force_order = true;
bool force_order = true;
/// If \c partial_degen is true, apply a partial
/// degeneralization to remove occurrences of acceptance
/// subformulas such as `Fin(x) | Fin(y)` or `Inf(x) & Inf(y)`.
......@@ -51,15 +51,25 @@ namespace spot
/// If \c scc_acc_clean is true, to_parity() will ignore colors
/// no occoring in an SCC while processing this SCC.
bool acc_clean = true;
/// If \a parity_equiv is true, to_parity() will check if there
/// If \c parity_equiv is true, to_parity() will check if there
/// exists a permutations of colors such that the acceptance
/// condition is a parity condition.
bool parity_equiv = true;
/// If \a parity_prefix is true, to_parity() will remove the prefix of
/// the acceptance condition that correspond to parity, works on the
// remaining and adds marks to process the prefix.
bool parity_prefix = true;
/// If \a rabin_to_buchi is true, to_parity() tries to convert a Rabin or
bool parity_equiv = true;
/// If \c parity_prefix is true, to_parity() will use a special
/// handling for acceptance conditions of the form `Inf(m0) |
/// (Fin(m1) & (Inf(m2) | (… β)))` that start as a parity
/// condition (modulo a renumbering of `m0`, `m1`, `m2`, ...) but where
/// `β` can be an arbitrary formula. In this case, the paritization
/// algorithm is really applied only to `β`, and the marks of the
/// prefix are appended after a suitable renumbering.
///
/// For technical reasons, activating this option (and this is the
/// default) causes reduce_parity() to be called at the end to
/// minimize the number of colors used. It is therefore
/// recommended to disable this option when one wants to follow
/// the output CAR/IAR constructions.
bool parity_prefix = true;
/// If \c rabin_to_buchi is true, to_parity() tries to convert a Rabin or
/// Streett condition to Büchi or co-Büchi with
/// rabin_to_buchi_if_realizable().
bool rabin_to_buchi = true;
......@@ -69,8 +79,8 @@ namespace spot
/// Use propagate_marks_here to increase the number of marks on transition
/// in order to move more colors (and increase the number of
/// compatible states) when we apply LAR.
bool propagate_col = true;
/// If \a pretty_print is true, states of the output automaton are
bool propagate_col = true;
/// If \c pretty_print is true, states of the output automaton are
/// named to help debugging.
bool pretty_print = false;
};
......
......@@ -106,6 +106,10 @@ def test(aut, expected_num_states=[], full=True):
propagate_col = opt.propagate_col,
pretty_print = opt.pretty_print,
)
p1st, p1ed, p1se = p1.num_states(), p1.num_edges(), p1.num_sets()
if opt.parity_prefix is False:
# Reduce the number of colors to help are_equivalent
spot.reduce_parity_here(p1)
assert spot.are_equivalent(aut, p1)
if expected_num is not None:
assert p1.num_states() == expected_num
......@@ -113,9 +117,9 @@ def test(aut, expected_num_states=[], full=True):
# 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()
assert p2.num_states() == p1st
assert p2.num_edges() == p1ed
assert p2.num_sets() == p1se
test(spot.automaton("""HOA: v1
name: "(FGp0 & ((XFp0 & F!p1) | F(Gp1 & XG!p0))) | G(F!p0 & (XFp0 | F!p1) &
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment