to_parity: Improve to_parity and update tests

* spot/twaalgos/toparity.cc: Use a better search of the
transitions when we search compatible states.
* spot/twaalgos/toparity.hh: Use less that 80 columns.
* tests/python/merge.py, tests/python/toparity.py: Update tests.
This commit is contained in:
Florian Renkin 2020-04-10 19:22:20 +02:00
parent b4db34995f
commit 0ba1097636
4 changed files with 21 additions and 18 deletions

View file

@ -833,13 +833,15 @@ const std::vector<unsigned>& states,
std::map<unsigned, std::vector<unsigned>>& partial_history,
state_2_car_scc& state_2_car)
{
for (unsigned current_state : states)
for (auto& edge : aut->out(current_state))
for (auto& edge : aut->edges())
{
unsigned
src = edge.src,
dst = edge.dst;
if (src == dst)
// We don't change loops or transitions that were not created in
// the current SCC.
if (src == dst
|| std::find(states.begin(), states.end(), src) == states.end())
continue;
unsigned dst_scc = num2car[dst].state_scc;
auto cant_change = partial_history[aut->edge_number(edge)];

View file

@ -63,9 +63,9 @@ namespace spot
/// Only allow degeneralization if it reduces the number of colors in the
/// acceptance condition.
bool reduce_col_deg = false;
/// 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.
/// 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
/// named to help debugging.

View file

@ -78,7 +78,8 @@ assert hoa == """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 2 Fin(1) | Inf(0)
acc-name: parity min even 2
Acceptance: 2 Inf(0) | Fin(1)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0

View file

@ -288,7 +288,7 @@ State: 4
[0&!1] 4
[0&1] 4 {1 2 4}
--END--
"""), [9, 6, 6, 6, 7, 6, 6])
"""), [9, 6, 7, 7, 6, 6, 6])
test(spot.automaton("""
HOA: v1