Commit 5ec9d55f authored by Florian Renkin's avatar Florian Renkin
Browse files

simplify_acceptance: Use color inclusions to simplify a condition

This fixes #406.

* spot/twaalgos/cleanacc.cc: Add the simplification.
* tests/core/remfin.test, tests/python/automata.ipynb,
tests/python/remfin.py: Update tests.
* tests/python/simplacc.py: Update and add tests.
parent 05e6e088
Pipeline #20745 failed with stages
in 367 minutes and 50 seconds
......@@ -613,6 +613,100 @@ namespace spot
}
}
static
acc_cond::mark_t merge_marks(acc_cond::mark_t colors,
std::vector<acc_cond::mark_t> inclusions)
{
bool changed;
do
{
changed = false;
for (unsigned c : colors.sets())
{
if ((inclusions[c] & colors) != acc_cond::mark_t {})
{
auto new_colors = (colors - inclusions[c]);
if (new_colors != colors)
changed = true;
colors = new_colors;
break;
}
}
} while (changed);
return colors;
}
static
acc_cond::acc_code merge_colors(acc_cond::acc_code code,
std::vector<acc_cond::mark_t> inclusions)
{
if (code.empty())
return {};
int pos = code.size() - 1;
acc_cond::acc_code result;
do
{
switch (code[pos].sub.op)
{
case acc_cond::acc_op::And:
{
result = acc_cond::acc_code::t();
--pos;
while (pos > 0)
{
result = merge_colors(acc_cond::acc_code(&code[pos]), inclusions)
& result;
pos -= (code[pos].sub.size + 1);
}
return result;
}
case acc_cond::acc_op::Or:
{
result = acc_cond::acc_code::f();
--pos;
while (pos > 0)
{
result = merge_colors(acc_cond::acc_code(&code[pos]), inclusions)
| result;
pos -= (code[pos].sub.size + 1);
}
return result;
}
case acc_cond::acc_op::Fin:
{
auto res = acc_cond::acc_code::fin(merge_marks(code[pos - 1].mark,
inclusions));
return res;
}
case acc_cond::acc_op::Inf:
{
auto res = acc_cond::acc_code::inf(merge_marks(code[pos - 1].mark,
inclusions));
return res;
}
default:
SPOT_UNREACHABLE();
}
} while (pos > 0);
SPOT_UNREACHABLE();
}
// Create a vector of marks such that for every color c, result[c] contains
// all the colors that are on every transitions that also contain c
// (c is excluded).
static std::vector<acc_cond::mark_t> included_marks(twa_graph_ptr aut)
{
std::vector<acc_cond::mark_t> result(SPOT_MAX_ACCSETS,
acc_cond::mark_t::all());
for (unsigned i = 0; i < SPOT_MAX_ACCSETS; ++i)
result[i]^= acc_cond::mark_t {i};
for (auto& e: aut->edges())
for (auto c : e.acc.sets())
result[c] &= e.acc;
return result;
}
twa_graph_ptr simplify_acceptance_here(twa_graph_ptr aut)
{
for (;;)
......@@ -621,7 +715,10 @@ namespace spot
merge_identical_marks_here(aut);
if (aut->acc().is_generalized_buchi())
break;
acc_cond::acc_code old = aut->get_acceptance();
auto inc = included_marks(aut);
auto new_code = merge_colors(aut->get_acceptance(), inc);
aut->set_acceptance(acc_cond(aut->num_sets(), new_code));
acc_cond::acc_code old = new_code;
aut->set_acceptance(aut->acc().unit_propagation());
simplify_complementary_marks_here(aut);
fuse_marks_here(aut);
......
......@@ -311,48 +311,46 @@ State: 2 {0}
[!1] 2
--END--
HOA: v1
States: 4
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 4 Inf(0) | Inf(3) | (Inf(1)&Inf(2))
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[t] 0 {1 3}
[0] 1 {1 3}
[!0] 2 {1 3}
[t] 0 {0}
[0] 1 {0}
[!0] 2 {0}
State: 1
[1] 0 {1}
[0&1] 1 {1}
[!0&1] 2 {1 2}
[1] 0
[0&1] 1
[!0&1] 2 {0}
State: 2
[!1] 0
[0&!1] 1
[!0&!1] 2
[!0&!1] 3
State: 3
[!0&!1] 3 {0}
[!0&!1] 2 {0}
--END--
HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[t] 0 {1}
[0] 1 {1}
[!0] 2 {0 1}
[t] 0
[0] 1
[!0] 2 {0}
State: 1
[1] 0 {1}
[0&1] 1 {0 1}
[!0&1] 2 {0 1}
[1] 0
[0&1] 1 {0}
[!0&1] 2 {0}
State: 2
[!1] 0
[0&!1] 1 {0 1}
[!0&!1] 2 {0 1}
[0&!1] 1 {0}
[!0&!1] 2 {0}
--END--
HOA: v1
States: 1
......@@ -842,25 +840,23 @@ HOA: v1
States: 4
Start: 0
AP: 2 "b" "c"
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[!0] 0
[!0] 1
[0] 0
[0] 1
[0&!1] 2
[0&1] 3
[t] 0
[0&!1] 1
[0&1] 2
[!0] 3
State: 1
[!0] 1 {0 1}
[!0 | !1] 1 {0}
[0&1] 2
State: 2
[!0 | !1] 2 {0 1}
[0&1] 3 {0}
[!1] 1 {0}
[1] 2
State: 3
[!1] 2 {0 1}
[1] 3 {0}
[!0] 3 {0}
--END--
HOA: v1
States: 6
......@@ -912,7 +908,7 @@ State: 2 {0}
[!1] 2
--END--
HOA: v1
States: 4
States: 3
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
......@@ -930,10 +926,7 @@ State: 1
State: 2
[!1] 0
[0&!1] 1
[!0&!1] 2
[!0&!1] 3
State: 3
[!0&!1] 3 {0}
[!0&!1] 2 {0}
--END--
HOA: v1
States: 3
......
This diff is collapsed.
This diff is collapsed.
......@@ -92,4 +92,4 @@ State: 2
""")
b = spot.remove_fin(a)
size = (b.num_states(), b.num_edges())
assert size == (5, 15);
assert size == (5, 17);
......@@ -60,6 +60,11 @@ HOA: v1 States: 2 Start: 0 AP: 2 "p0" "p1" Acceptance: 5 Fin(0) &
(((Fin(1)|Fin(2)|Fin(3))&Inf(4)|Fin(3))) properties: trans-labels
explicit-labels trans-acc --BODY-- State: 0 [!0&!1] 0 {0 1 3} [0&1] 1
{0 2} [0&!1] 0 {2} State: 1 [0&1] 0 {0 2} [0&1] 1 {1} [0&!1] 1 {4} --END--
/* Issue #406 */
HOA: v1 States: 2 Start: 0 AP: 2 "p0" "p1" Acceptance: 4
(Fin(3) & (Inf(1) | Fin(0))) | (Inf(0)&Inf(2)&Inf(3)) properties: trans-labels
explicit-labels trans-acc deterministic --BODY-- State: 0 [0&!1] 0 {2 3}
[!0&!1] 1 {0 1} State: 1 [!0&!1] 0 {0 1} [0&1] 1 {1 2} --END--
"""))
res = []
......@@ -90,8 +95,10 @@ assert res == [
'((Inf(1) & Fin(2)) | Fin(5)) & (Inf(0) | (Inf(1) & (Inf(3) | Fin(4))))',
'Inf(0)',
'Fin(0)',
'Fin(0)|Fin(1)|Fin(2)',
'Inf(0)&Inf(1)&Inf(2)',
'((Fin(0)|Fin(1)) & Inf(3)) | Fin(2)',
'((Inf(0)&Inf(1)) | Fin(3)) & Inf(2)',
'Fin(0)',
'Inf(0)',
'(Fin(0) & Inf(2)) | Fin(1)',
'(Inf(0) | Fin(2)) & Inf(1)',
'(Fin(2) & (Inf(1) | Fin(0))) | (Inf(0)&Inf(2))',
'(Inf(2) | (Fin(1) & Inf(0))) & (Fin(0)|Fin(2))',
]
Supports Markdown
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