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:
parent
b4db34995f
commit
0ba1097636
4 changed files with 21 additions and 18 deletions
|
|
@ -833,13 +833,15 @@ const std::vector<unsigned>& states,
|
||||||
std::map<unsigned, std::vector<unsigned>>& partial_history,
|
std::map<unsigned, std::vector<unsigned>>& partial_history,
|
||||||
state_2_car_scc& state_2_car)
|
state_2_car_scc& state_2_car)
|
||||||
{
|
{
|
||||||
for (unsigned current_state : states)
|
for (auto& edge : aut->edges())
|
||||||
for (auto& edge : aut->out(current_state))
|
|
||||||
{
|
{
|
||||||
unsigned
|
unsigned
|
||||||
src = edge.src,
|
src = edge.src,
|
||||||
dst = edge.dst;
|
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;
|
continue;
|
||||||
unsigned dst_scc = num2car[dst].state_scc;
|
unsigned dst_scc = num2car[dst].state_scc;
|
||||||
auto cant_change = partial_history[aut->edge_number(edge)];
|
auto cant_change = partial_history[aut->edge_number(edge)];
|
||||||
|
|
|
||||||
|
|
@ -63,9 +63,9 @@ namespace spot
|
||||||
/// Only allow degeneralization if it reduces the number of colors in the
|
/// Only allow degeneralization if it reduces the number of colors in the
|
||||||
/// acceptance condition.
|
/// acceptance condition.
|
||||||
bool reduce_col_deg = false;
|
bool reduce_col_deg = false;
|
||||||
/// Use propagate_marks_here to increase the number of marks on transition in
|
/// Use propagate_marks_here to increase the number of marks on transition
|
||||||
/// order to move more colors (and increase the number of compatible states)
|
/// in order to move more colors (and increase the number of
|
||||||
/// when we apply LAR.
|
/// compatible states) when we apply LAR.
|
||||||
bool propagate_col = true;
|
bool propagate_col = true;
|
||||||
/// If \a pretty_print is true, states of the output automaton are
|
/// If \a pretty_print is true, states of the output automaton are
|
||||||
/// named to help debugging.
|
/// named to help debugging.
|
||||||
|
|
|
||||||
|
|
@ -78,7 +78,8 @@ assert hoa == """HOA: v1
|
||||||
States: 3
|
States: 3
|
||||||
Start: 0
|
Start: 0
|
||||||
AP: 2 "a" "b"
|
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
|
properties: trans-labels explicit-labels trans-acc
|
||||||
--BODY--
|
--BODY--
|
||||||
State: 0
|
State: 0
|
||||||
|
|
|
||||||
|
|
@ -288,7 +288,7 @@ State: 4
|
||||||
[0&!1] 4
|
[0&!1] 4
|
||||||
[0&1] 4 {1 2 4}
|
[0&1] 4 {1 2 4}
|
||||||
--END--
|
--END--
|
||||||
"""), [9, 6, 6, 6, 7, 6, 6])
|
"""), [9, 6, 7, 7, 6, 6, 6])
|
||||||
|
|
||||||
test(spot.automaton("""
|
test(spot.automaton("""
|
||||||
HOA: v1
|
HOA: v1
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue