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

improve cleanup_parity() and colorize_parity()

Fixes #384.

* spot/twaalgos/parity.cc: Here.
* tests/core/parity2.test, tests/python/highlighting.ipynb,
tests/python/parity.py: Adjust test cases.
* tests/python/parity.ipynb: Improve the presentation.
* NEWS: Mention the change.
parent f0b77e21
...@@ -103,6 +103,11 @@ New in spot 2.7.5.dev (not yet released) ...@@ -103,6 +103,11 @@ New in spot 2.7.5.dev (not yet released)
F(G(a & Fb) = FGa & GFb (unless option "reduce_size_strictly") F(G(a & Fb) = FGa & GFb (unless option "reduce_size_strictly")
G(F(a & Gb)) = GFa & FGb (unless option "reduce_size_strictly") G(F(a & Gb)) = GFa & FGb (unless option "reduce_size_strictly")
- cleanup_parity() and colorize_parity() were cleaned up a bit,
resulting in fewer colors used in some cases. In particular,
colorize_parity() learned that coloring transitiant edges does not
require the introduction of a new color.
New in spot 2.7.5 (2019-06-05) New in spot 2.7.5 (2019-06-05)
Build: Build:
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2016, 2018 Laboratoire de Recherche et Développement // Copyright (C) 2016, 2018, 2019 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -22,6 +22,7 @@ ...@@ -22,6 +22,7 @@
#include <spot/twa/twagraph.hh> #include <spot/twa/twagraph.hh>
#include <spot/twaalgos/product.hh> #include <spot/twaalgos/product.hh>
#include <spot/twaalgos/complete.hh> #include <spot/twaalgos/complete.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <vector> #include <vector>
#include <utility> #include <utility>
#include <functional> #include <functional>
...@@ -165,104 +166,121 @@ namespace spot ...@@ -165,104 +166,121 @@ namespace spot
twa_graph_ptr twa_graph_ptr
cleanup_parity_here(twa_graph_ptr aut, bool keep_style) cleanup_parity_here(twa_graph_ptr aut, bool keep_style)
{ {
unsigned num_sets = aut->num_sets();
if (num_sets == 0)
return aut;
bool current_max; bool current_max;
bool current_odd; bool current_odd;
if (!aut->acc().is_parity(current_max, current_odd, true)) if (!aut->acc().is_parity(current_max, current_odd, true))
input_is_not_parity("cleanup_parity"); input_is_not_parity("cleanup_parity");
auto num_sets = aut->num_sets();
if (num_sets == 0)
return aut;
// Compute all the used sets // Gather all the used colors, while leaving only one per edge.
auto used_in_aut = acc_cond::mark_t(); auto used_in_aut = acc_cond::mark_t();
acc_cond::mark_t allsets = aut->acc().all_sets();
if (current_max)
for (auto& t: aut->edges()) for (auto& t: aut->edges())
{ {
// leave only one color on each transition if (auto maxset = (t.acc & allsets).max_set())
if (current_max)
{ {
auto maxset = t.acc.max_set();
if (maxset)
t.acc = acc_cond::mark_t{maxset - 1}; t.acc = acc_cond::mark_t{maxset - 1};
used_in_aut |= t.acc;
} }
else else
{ {
t.acc = t.acc.lowest(); t.acc = acc_cond::mark_t{};
} }
// recall colors used in the automaton }
else
for (auto& t: aut->edges())
{
t.acc = (t.acc & allsets).lowest();
used_in_aut |= t.acc; used_in_aut |= t.acc;
} }
// remove from the acceptance condition the unused one (starting from the if (used_in_aut)
// least significant) {
auto useful = used_in_aut; if (current_max)
int useful_min = 0; // If max even or max odd: if 0 is not used, we can remove 1, if
int useful_max = num_sets-1; // 2 is not used, we can remove 3, etc.
if (!current_max) // This is obvious from the encoding:
{ // max odd n = ... Inf(3) | (Fin(2) & (Inf(1) | Fin(0)))
int n = num_sets-1; // max even n = ... Fin(3) & (Inf(2) | (Fin(1) & Inf(0)))
while (n >= 0 && !useful.has(n))
{
if (n > 0)
useful.clear(n-1);
n -= 2;
}
useful_max = n;
}
else
{ {
unsigned n = 0; unsigned n = 0;
while (n < num_sets && !useful.has(n)) while (n + 1 < num_sets && !used_in_aut.has(n))
{ {
useful.clear(n+1); used_in_aut.clear(n + 1);
n += 2; n += 2;
} }
useful_min = n;
} }
if (used_in_aut) else
// min even and min odd simply work the other way around:
// min even 4 = Inf(0) | (Fin(1) & (Inf(2) | Fin(3)))
// min odd 4 = Fin(0) & (Inf(1) | (Fin(2) & Inf(3)))
{ {
// Never remove the least significant acceptance set, and mark the int n = num_sets - 1;
// acceptance set 0 to keep the style if needed. while (n >= 1 && !used_in_aut.has(n))
if (keep_style && useful_min <= useful_max)
{ {
useful.set(useful_min); used_in_aut.clear(n - 1);
useful.set(useful_max); n -= 2;
}
}
} }
// Fill the vector shift with the new acceptance sets // If no color needed in the automaton, exit early.
std::vector<unsigned> shift(num_sets); if (!used_in_aut)
{
if ((current_max && current_odd)
|| (!current_max && current_odd == (num_sets & 1)))
aut->set_acceptance(0, acc_cond::acc_code::t());
else
aut->set_acceptance(0, acc_cond::acc_code::f());
for (auto& e: aut->edges())
e.acc = {};
return aut;
}
// Renumber colors. Two used colors separated by a unused color
// can be merged.
std::vector<unsigned> rename(num_sets);
int prev_used = -1; int prev_used = -1;
bool change_style = false; bool change_style = false;
unsigned new_index = 0; unsigned new_index = 0;
for (auto i = 0U; i < num_sets; ++i) for (auto i = 0U; i < num_sets; ++i)
if (useful.has(i)) if (used_in_aut.has(i))
{ {
if (prev_used == -1) if (prev_used == -1)
change_style = i % 2 != 0; {
else if ((i + prev_used) % 2 != 0) if (i & 1)
{
if (keep_style)
new_index = 1;
else
change_style = true;
}
}
else if ((i + prev_used) & 1)
++new_index; ++new_index;
shift[i] = new_index; rename[i] = new_index;
prev_used = i; prev_used = i;
} }
assert(prev_used >= 0);
// Update all the transitions with the vector shift // Update all colors according to RENAME.
// Using max_set or min_set makes no difference since
// there is now at most one color per edge.
for (auto& t: aut->edges()) for (auto& t: aut->edges())
{ {
t.acc &= useful; acc_cond::mark_t m = t.acc & used_in_aut;
auto maxset = t.acc.max_set(); unsigned color = m.max_set();
if (maxset) if (color)
t.acc = acc_cond::mark_t{shift[maxset - 1]}; t.acc = acc_cond::mark_t{rename[color - 1]};
}
auto new_num_sets = new_index + 1;
if (!useful)
{
new_num_sets = 0;
if (current_max)
change_style = false;
else else
change_style = num_sets % 2 == 1; t.acc = m;
} }
unsigned new_num_sets = new_index + 1;
if (new_num_sets < num_sets) if (new_num_sets < num_sets)
{ {
auto new_acc = auto new_acc =
...@@ -271,14 +289,9 @@ namespace spot ...@@ -271,14 +289,9 @@ namespace spot
new_num_sets); new_num_sets);
aut->set_acceptance(new_num_sets, new_acc); aut->set_acceptance(new_num_sets, new_acc);
} }
}
else else
{ {
if ((current_max && current_odd) assert(!change_style);
|| (!current_max && current_odd != (num_sets % 2 == 0)))
aut->set_acceptance(0, acc_cond::acc_code::t());
else
aut->set_acceptance(0, acc_cond::acc_code::f());
} }
return aut; return aut;
} }
...@@ -297,44 +310,79 @@ namespace spot ...@@ -297,44 +310,79 @@ namespace spot
bool current_odd; bool current_odd;
if (!aut->acc().is_parity(current_max, current_odd, true)) if (!aut->acc().is_parity(current_max, current_odd, true))
input_is_not_parity("colorize_parity"); input_is_not_parity("colorize_parity");
if (!aut->is_existential())
throw std::runtime_error
("colorize_parity_here() does not support alternation");
bool has_empty = false; bool has_empty_in_scc = false;
{
scc_info si(aut, scc_info_options::NONE);
for (const auto& e: aut->edges()) for (const auto& e: aut->edges())
if (!e.acc) if (!e.acc && si.scc_of(e.src) == si.scc_of(e.dst))
{ {
has_empty = true; has_empty_in_scc = true;
break; break;
} }
auto num_sets = aut->num_sets(); }
unsigned num_sets = aut->num_sets();
bool new_odd = current_odd;
int incr = 0; int incr = 0;
if (has_empty) unsigned empty = current_max ? 0 : num_sets - 1;
if (has_empty_in_scc)
{
// If the automaton has an SCC transition that belongs to no set
// (called "empty trans." below), we may need to introduce a
// new acceptance set. What to do depends on the kind
// (min/max) and style (odd/even) of parity acceptance and the
// number (n) of colors used.
//
// | kind/style | n | empty tr. | other tr. | result |
// |------------+-----+------------+-----------+--------------|
// | max odd | any | set to {0} | add 1 | max even n+1 |
// | max even | any | set to {0} | add 1 | max odd n+1 |
// | min odd | any | set to {n} | unchanged | min odd n+1 |
// | min even | any | set to {n} | unchanged | min even n+1 |
//
// In the above table, the "max" cases both change their style
// We may want to add a second acceptance set to keep the
// style:
//
// | kind/style | n | empty tr. | other tr. | result |
// |------------+-----+------------+-----------+--------------|
// | max odd | any | set to {1} | add 2 | max odd n+2 |
// | max even | any | set to {1} | add 2 | max even n+2 |
if (current_max)
{ {
// If the automaton has a transition that belong to any set, we need to incr = 1 + keep_style;
// introduce a new acceptance set.
// We may want to add a second acceptance set to keep the style of
// the parity acceptance
incr = 1 + (keep_style && current_max);
num_sets += incr; num_sets += incr;
bool new_style = current_odd == (keep_style || !current_max); new_odd = current_odd == keep_style;
auto new_acc = acc_cond::acc_code::parity(current_max, empty = keep_style;
new_style, num_sets); }
else
{
empty = num_sets++;
}
auto new_acc =
acc_cond::acc_code::parity(current_max, new_odd, num_sets);
aut->set_acceptance(num_sets, new_acc); aut->set_acceptance(num_sets, new_acc);
} }
if (current_max) if (current_max)
{ {
--incr; --incr;
for (auto& e: aut->edges()) for (auto& e: aut->edges())
{ {
auto maxset = e.acc.max_set(); auto maxset = e.acc.max_set();
e.acc = acc_cond::mark_t{maxset ? maxset + incr : incr}; e.acc = acc_cond::mark_t{maxset ? maxset + incr : empty};
} }
} }
else else
{ {
auto unused_mark = num_sets - incr;
for (auto& e: aut->edges()) for (auto& e: aut->edges())
e.acc = e.acc ? e.acc.lowest() : acc_cond::mark_t{unused_mark}; e.acc = e.acc ? e.acc.lowest() : acc_cond::mark_t{empty};
} }
return aut; return aut;
} }
......
...@@ -245,12 +245,12 @@ name: "(p0 W XXGp0) & G(Fp1 & FGp2)" ...@@ -245,12 +245,12 @@ name: "(p0 W XXGp0) & G(Fp1 & FGp2)"
States: 5 States: 5
Start: 0 Start: 0
AP: 3 "p0" "p1" "p2" AP: 3 "p0" "p1" "p2"
acc-name: parity max even 3 acc-name: Streett 1
Acceptance: 3 Inf(2) | (Fin(1) & Inf(0)) Acceptance: 2 Fin(0) | Inf(1)
properties: trans-labels explicit-labels trans-acc colored properties: trans-labels explicit-labels trans-acc colored
--BODY-- --BODY--
State: 0 State: 0
[0] 0 {1} [0] 0 {0}
[!0] 1 {0} [!0] 1 {0}
[0&1&2] 2 {0} [0&1&2] 2 {0}
State: 1 State: 1
...@@ -258,14 +258,14 @@ State: 1 ...@@ -258,14 +258,14 @@ State: 1
[1&2] 4 {0} [1&2] 4 {0}
State: 2 State: 2
[!0] 1 {0} [!0] 1 {0}
[0&!1&2] 2 {1} [0&!1&2] 2 {0}
[0&1&2] 2 {2} [0&1&2] 2 {1}
State: 3 State: 3
[0] 3 {1} [0] 3 {0}
[0&1&2] 4 {0} [0&1&2] 4 {0}
State: 4 State: 4
[0&!1&2] 4 {1} [0&!1&2] 4 {0}
[0&1&2] 4 {2} [0&1&2] 4 {1}
--END-- --END--
HOA: v1 HOA: v1
name: "FGa" name: "FGa"
...@@ -304,24 +304,24 @@ name: "(p0 W XXGp0) & G(Fp1 & FGp2)" ...@@ -304,24 +304,24 @@ name: "(p0 W XXGp0) & G(Fp1 & FGp2)"
States: 5 States: 5
Start: 0 Start: 0
AP: 3 "p0" "p1" "p2" AP: 3 "p0" "p1" "p2"
acc-name: parity min odd 4 acc-name: parity min odd 3
Acceptance: 4 Fin(0) & (Inf(1) | (Fin(2) & Inf(3))) Acceptance: 3 Fin(0) & (Inf(1) | Fin(2))
properties: trans-labels explicit-labels trans-acc colored properties: trans-labels explicit-labels trans-acc colored
--BODY-- --BODY--
State: 0 State: 0
[0] 0 {2} [0] 0 {2}
[!0] 1 {3} [!0] 1 {2}
[0&1&2] 2 {3} [0&1&2] 2 {2}
State: 1 State: 1
[t] 3 {3} [t] 3 {2}
[1&2] 4 {3} [1&2] 4 {2}
State: 2 State: 2
[!0] 1 {3} [!0] 1 {2}
[0&1&2] 2 {1} [0&1&2] 2 {1}
[0&!1&2] 2 {2} [0&!1&2] 2 {2}
State: 3 State: 3
[0] 3 {2} [0] 3 {2}
[0&1&2] 4 {3} [0&1&2] 4 {2}
State: 4 State: 4
[0&1&2] 4 {1} [0&1&2] 4 {1}
[0&!1&2] 4 {2} [0&!1&2] 4 {2}
...@@ -980,21 +980,21 @@ name: "(p0 W XXGp0) & G(Fp1 & FGp2)" ...@@ -980,21 +980,21 @@ name: "(p0 W XXGp0) & G(Fp1 & FGp2)"
States: 5 States: 5
Start: 0 Start: 0
AP: 3 "p0" "p1" "p2" AP: 3 "p0" "p1" "p2"
acc-name: parity min odd 4 acc-name: parity min odd 3
Acceptance: 4 Fin(0) & (Inf(1) | (Fin(2) & Inf(3))) Acceptance: 3 Fin(0) & (Inf(1) | Fin(2))
properties: trans-labels explicit-labels trans-acc colored properties: trans-labels explicit-labels trans-acc colored
properties: deterministic properties: deterministic
--BODY-- --BODY--
State: 0 State: 0
[0&!1 | 0&!2] 0 {2} [0&!1 | 0&!2] 0 {2}
[!0] 1 {3} [!0] 1 {2}
[0&1&2] 2 {1} [0&1&2] 2 {1}
State: 1 State: 1
[!1 | !2] 3 {3} [!1 | !2] 3 {2}
[1&2] 4 {3} [1&2] 4 {2}
State: 2 State: 2
[0&!2] 0 {0} [0&!2] 0 {0}
[!0] 1 {3} [!0] 1 {2}
[0&1&2] 2 {1} [0&1&2] 2 {1}
[0&!1&2] 2 {2} [0&!1&2] 2 {2}
State: 3 State: 3
...@@ -1042,21 +1042,21 @@ name: "(p0 W XXGp0) & G(Fp1 & FGp2)" ...@@ -1042,21 +1042,21 @@ name: "(p0 W XXGp0) & G(Fp1 & FGp2)"
States: 5 States: 5
Start: 0 Start: 0
AP: 3 "p0" "p1" "p2" AP: 3 "p0" "p1" "p2"
acc-name: parity min odd 4 acc-name: parity min odd 3
Acceptance: 4 Fin(0) & (Inf(1) | (Fin(2) & Inf(3))) Acceptance: 3 Fin(0) & (Inf(1) | Fin(2))
properties: trans-labels explicit-labels trans-acc colored properties: trans-labels explicit-labels trans-acc colored
properties: deterministic properties: deterministic
--BODY-- --BODY--
State: 0 State: 0
[0&!1 | 0&!2] 0 {2} [0&!1 | 0&!2] 0 {2}
[!0] 1 {3} [!0] 1 {2}
[0&1&2] 2 {1} [0&1&2] 2 {1}
State: 1 State: 1
[!1 | !2] 3 {3} [!1 | !2] 3 {2}
[1&2] 4 {3} [1&2] 4 {2}
State: 2 State: 2
[0&!2] 0 {0} [0&!2] 0 {0}
[!0] 1 {3} [!0] 1 {2}
[0&1&2] 2 {1} [0&1&2] 2 {1}
[0&!1&2] 2 {2} [0&!1&2] 2 {2}
State: 3 State: 3
...@@ -1527,7 +1527,6 @@ ltlcross 'ltl2tgba -P' 'ltl2tgba -P"odd max"' 'ltl2tgba -P"even min"' \ ...@@ -1527,7 +1527,6 @@ ltlcross 'ltl2tgba -P' 'ltl2tgba -P"odd max"' 'ltl2tgba -P"even min"' \
'ltl2tgba -p' 'ltl2tgba -p"odd max"' 'ltl2tgba -p"even min"' \ 'ltl2tgba -p' 'ltl2tgba -p"odd max"' 'ltl2tgba -p"even min"' \
-f FGa -f 'GFa&GFb' -f 'GF(a <-> XXXb)' -f '(p0 W XXGp0) & GFp1 & FGp2' -f FGa -f 'GFa&GFb' -f 'GF(a <-> XXXb)' -f '(p0 W XXGp0) & GFp1 & FGp2'
# Test the behavior of our determinization on Max Michel automata. # Test the behavior of our determinization on Max Michel automata.
# Any change to Spot that lowers the output.states is welcome :-) # Any change to Spot that lowers the output.states is welcome :-)
genaut --m-nba=1..4 | autcross --language-preserved 'autfilt -D' --csv=out.csv genaut --m-nba=1..4 | autcross --language-preserved 'autfilt -D' --csv=out.csv
......
...@@ -240,7 +240,7 @@ ...@@ -240,7 +240,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b80ee2a0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f52302b76f0> >"
] ]
}, },
"execution_count": 4, "execution_count": 4,
...@@ -352,7 +352,7 @@ ...@@ -352,7 +352,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7f55b8012060> >" "<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7f523026d2d0> >"
] ]
}, },
"execution_count": 5, "execution_count": 5,
...@@ -462,7 +462,7 @@ ...@@ -462,7 +462,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b80ee2a0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f52302b76f0> >"
] ]
}, },
"execution_count": 6, "execution_count": 6,
...@@ -695,7 +695,7 @@ ...@@ -695,7 +695,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b8012840> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f523026d540> >"
] ]
}, },
"execution_count": 8, "execution_count": 8,
...@@ -890,7 +890,7 @@ ...@@ -890,7 +890,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f55b8012840> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f523026d540> >"
] ]
},