Commit a12d676b authored by Thomas Medioni's avatar Thomas Medioni

introduce spot::simplify_acceptance()

Simplify some automata where some marks are identical,
or complementary to another. Fixes #216.

* NEWS: mention the new function.
* spot/twaalgos/cleanacc.cc, spot/twaalgos/cleanacc.hh: Implement
  the function.
* tests/Makefile.am, tests/python/merge.py: Test this implementation.
parent 22620e18
...@@ -104,6 +104,10 @@ New in spot 2.3.4.dev (not yet released) ...@@ -104,6 +104,10 @@ New in spot 2.3.4.dev (not yet released)
automaton. This parameter is defaulted to true, in order to automaton. This parameter is defaulted to true, in order to
keep this modification backward-compatible. keep this modification backward-compatible.
- The new function spot::simplify_acceptance() is able to perform
some simplifications on an acceptance condition, and might lead
to the removal of some acceptance sets.
Python: Python:
- The 'spot.gen' package exports the functions from libspotgen. - The 'spot.gen' package exports the functions from libspotgen.
......
...@@ -73,5 +73,224 @@ namespace spot ...@@ -73,5 +73,224 @@ namespace spot
twa::prop_set::all())); twa::prop_set::all()));
} }
namespace
{
twa_graph_ptr merge_identical_marks_here(twa_graph_ptr aut)
{
// always cleanup before proceeding, otherwise if some mark appears in the
// acceptance condition, but not in the automaton the result is undefined.
cleanup_acceptance_here(aut, false);
auto& acc = aut->acc();
auto& c = acc.get_acceptance();
acc_cond::mark_t used_in_cond = c.used_sets();
if (!used_in_cond)
return aut;
unsigned num_sets = acc.num_sets();
std::vector<acc_cond::mark_t> always_together(num_sets);
for (unsigned i = 0; i < num_sets; ++i)
if (used_in_cond.has(i))
always_together[i] = used_in_cond;
else
always_together[i] = acc_cond::mark_t({i});
acc_cond::mark_t previous_a = 0U;
for (auto& t: aut->edges())
{
acc_cond::mark_t a = t.acc & used_in_cond;
if (a == previous_a)
continue;
previous_a = a;
for (unsigned m: a.sets())
{
acc_cond::mark_t at = always_together[m];
acc_cond::mark_t newm = at & a;
for (unsigned rem: (at - newm).sets())
always_together[rem] -= newm;
always_together[m] = newm;
}
}
acc_cond::mark_t to_remove = 0U;
for (unsigned i = 0; i < num_sets; ++i)
{
auto oldm = always_together[i];
if (oldm == acc_cond::mark_t({i}))
continue;
acc_cond::mark_t newm = oldm.lowest();
to_remove |= oldm - newm;
always_together[i] = newm;
}
for (auto& t: aut->edges())
t.acc -= to_remove;
// Replace the marks in the acceptance condition
auto pos = &c.back();
auto end = &c.front();
while (pos > end)
{
switch (pos->sub.op)
{
case acc_cond::acc_op::And:
case acc_cond::acc_op::Or:
--pos;
break;
case acc_cond::acc_op::Fin:
case acc_cond::acc_op::Inf:
case acc_cond::acc_op::FinNeg:
case acc_cond::acc_op::InfNeg:
acc_cond::mark_t replace = pos[-1].mark & to_remove;
pos[-1].mark -= replace;
for (unsigned m: replace.sets())
pos[-1].mark |= always_together[m];
pos -= 2;
break;
}
}
return aut;
}
// Eventually remove complementary marks from the acceptance condition.
acc_cond::acc_code remove_compl_rec(const acc_cond::acc_word* pos,
const std::vector<acc_cond::mark_t>&
complement)
{
auto start = pos - pos->sub.size;
switch (pos->sub.op)
{
case acc_cond::acc_op::And:
{
--pos;
auto res = acc_cond::acc_code::t();
acc_cond::mark_t seen_fin = 0U;
auto inf = acc_cond::acc_code::inf(0U);
do
{
auto tmp = remove_compl_rec(pos, complement);
if (tmp.back().sub.op == acc_cond::acc_op::Fin
&& tmp.front().mark.count() == 1)
seen_fin |= tmp.front().mark;
if (tmp.back().sub.op == acc_cond::acc_op::Inf)
{
inf &= std::move(tmp);
pos -= pos->sub.size + 1;
continue;
}
tmp &= std::move(res);
std::swap(tmp, res);
pos -= pos->sub.size + 1;
}
while (pos > start);
for (auto m: seen_fin.sets())
inf.front().mark -= complement[m];
res &= inf;
return res;
}
case acc_cond::acc_op::Or:
{
--pos;
auto res = acc_cond::acc_code::f();
acc_cond::mark_t seen_inf = 0U;
auto fin = acc_cond::acc_code::f();
do
{
auto tmp = remove_compl_rec(pos, complement);
if (tmp.back().sub.op == acc_cond::acc_op::Inf
&& tmp.front().mark.count() == 1)
seen_inf |= tmp.front().mark;
if (tmp.back().sub.op == acc_cond::acc_op::Fin)
{
fin |= std::move(tmp);
pos -= pos->sub.size + 1;
continue;
}
tmp |= std::move(res);
std::swap(tmp, res);
pos -= pos->sub.size + 1;
}
while (pos > start);
for (auto m: seen_inf.sets())
fin.front().mark -= complement[m];
res |= fin;
return res;
}
case acc_cond::acc_op::Fin:
return acc_cond::acc_code::fin(pos[-1].mark);
case acc_cond::acc_op::Inf:
return acc_cond::acc_code::inf(pos[-1].mark);
case acc_cond::acc_op::FinNeg:
case acc_cond::acc_op::InfNeg:
SPOT_UNREACHABLE();
};
SPOT_UNREACHABLE();
return {};
}
// Always cleanup_acceptance_here with stripping after calling this function
// As complementary marks might be simplified in the acceptance condition.
twa_graph_ptr simplify_complementary_marks_here(twa_graph_ptr aut)
{
auto& acc = aut->acc();
auto c = acc.get_acceptance();
acc_cond::mark_t used_in_cond = c.used_sets();
if (!used_in_cond)
return aut;
unsigned num_sets = acc.num_sets();
std::vector<acc_cond::mark_t> complement(num_sets);
for (unsigned i = 0; i < num_sets; ++i)
if (used_in_cond.has(i))
complement[i] = used_in_cond - acc_cond::mark_t({i});
acc_cond::mark_t previous_a = 0U;
for (auto& t: aut->edges())
{
if (t.acc == previous_a)
continue;
previous_a = t.acc;
for (unsigned m: used_in_cond.sets())
{
if (t.acc.has(m))
complement[m] -= t.acc;
else
complement[m] &= t.acc;
}
}
aut->set_acceptance(num_sets,
remove_compl_rec(&acc.get_acceptance().back(),
complement));
return aut;
}
}
twa_graph_ptr simplify_acceptance_here(twa_graph_ptr aut)
{
cleanup_acceptance_here(aut, false);
merge_identical_marks_here(aut);
simplify_complementary_marks_here(aut);
cleanup_acceptance_here(aut, true);
return aut;
}
twa_graph_ptr simplify_acceptance(const_twa_graph_ptr aut)
{
return simplify_acceptance_here(make_twa_graph(aut, twa::prop_set::all()));
}
} }
...@@ -34,4 +34,17 @@ namespace spot ...@@ -34,4 +34,17 @@ namespace spot
/// \brief Remove useless acceptance sets /// \brief Remove useless acceptance sets
SPOT_API twa_graph_ptr SPOT_API twa_graph_ptr
cleanup_acceptance(const_twa_graph_ptr aut); cleanup_acceptance(const_twa_graph_ptr aut);
/// \brief Simplify an acceptance condition
///
/// Remove useless acceptance sets.
/// Merge identical sets.
/// If some sets are complement to each other, might result in the
/// simplification of some clause in the acceptance condition.
SPOT_API twa_graph_ptr
simplify_acceptance_here(twa_graph_ptr aut);
/// \brief Simplify an acceptance condition
SPOT_API twa_graph_ptr
simplify_acceptance(const_twa_graph_ptr aut);
} }
...@@ -348,6 +348,7 @@ TESTS_python = \ ...@@ -348,6 +348,7 @@ TESTS_python = \
python/ltlf.py \ python/ltlf.py \
python/ltlparse.py \ python/ltlparse.py \
python/ltlsimple.py \ python/ltlsimple.py \
python/merge.py \
python/minato.py \ python/minato.py \
python/misc-ec.py \ python/misc-ec.py \
python/optionmap.py \ python/optionmap.py \
......
This diff is collapsed.
Markdown is supported
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