alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

simplify_acceptance: generalize the complementary mark rewriting

Browse source 
Fixes #403.

* spot/twaalgos/cleanacc.cc (simplify_complementary_marks_here):
Assume that two colors are complementary in a broad sense, i.e., on is
present if (but not only if) the other is missing before applying
those rewritings.  Technically, this is usually not necessary, because
the changes done in #418 will cause such "covering-the-full-automaton"
pair of colors to be disjoint so complementary in a strict sense.  It
might make a difference (this is not tested) in presence of reused
colors which #418 cannot remove.  In any case, it's simply less code
to implement the broad sense.
* tests/python/toparity.py: Add test case from #403, which is
reduced to two states with recent optimizations.
This commit is contained in:
Alexandre Duret-Lutz 2020-07-29 14:37:38 +02:00
parent 0c4b701630
commit a375089e52
2 changed files with 20 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

12
spot/twaalgos/cleanacc.cc
View file

@ -124,7 +124,7 @@ namespace spot
while (rbegin > rend); while (rbegin > rend);
if (rbegin <= rend) if (rbegin <= rend)
return res; return res;
// Fin(i) & Inf(i) = f; // Fin(i) & Inf(i) = f; (also done by unit-fin)
if (rbegin[-1].mark & seen_fin) if (rbegin[-1].mark & seen_fin)
return std::move(falsecode); return std::move(falsecode);
for (auto m: seen_fin.sets()) for (auto m: seen_fin.sets())
@ -192,6 +192,8 @@ namespace spot
return aut; return aut;
// complement[i] holds sets that appear when set #i does not. // complement[i] holds sets that appear when set #i does not.
// (This is not a strict complement, i.e., the sets in
// complement[i] are allowed to occur at the same time as i.)
unsigned num_sets = acc.num_sets(); unsigned num_sets = acc.num_sets();
std::vector<acc_cond::mark_t> complement(num_sets); std::vector<acc_cond::mark_t> complement(num_sets);
@ -214,12 +216,8 @@ namespace spot
{ {
prev_acc = tacc; prev_acc = tacc;
for (unsigned m: used_in_cond.sets()) for (unsigned m: used_in_cond.sets())
{ if (!tacc.has(m))
if (tacc.has(m)) complement[m] &= tacc;
complement[m] -= tacc;
else
complement[m] &= tacc;
}
}; };
if (b != e) if (b != e)
{ {

15
tests/python/toparity.py
View file

@ -220,6 +220,21 @@ State: 1
[!0&!1] 1 {0 3} [!0&!1] 1 {0 3}
--END--"""), [7, 5, 3, 6, 5, 5, 3]) --END--"""), [7, 5, 3, 6, 5, 5, 3])
test(spot.automaton("""HOA: v1
States: 2
Start: 0
AP: 2 "p0" "p1"
Acceptance: 5 ((Fin(1)|Fin(3)|Fin(4)) | Inf(2) | Inf(0))
& (Inf(0) | Inf(1)) & (Inf(2) | Inf(1))
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[0&1] 0 {1 3}
[!0&1] 1 {0}
State: 1
[0&1] 1 {2 3 4}
[!0&!1] 0 {1 2}
--END--"""), [9, 3, 2, 3, 3, 3, 2])
for i,f in enumerate(spot.randltl(10, 400)): for i,f in enumerate(spot.randltl(10, 400)):
test(spot.translate(f, "det", "G"), full=(i<100)) test(spot.translate(f, "det", "G"), full=(i<100))