Commit e5a37ff9 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

symplify_acceptance: More rules

Fixes #297. Implement the following rules.

Fin(i) & Fin(j) by f if i and j are complementary
Fin(i) & Inf(i) by f
Inf(i) | Inf(j) by t if i and j are complementary
Fin(i) | Inf(i) by t.

* spot/twaalgos/cleanacc.cc, spot/twaalgos/cleanacc.hh: Here.
* tests/python/merge.py: Add more test cases.
* NEWS: Mention the change.
parent d9f8c517
......@@ -160,6 +160,16 @@ New in spot 2.4.1.dev (not yet released)
conditions. The fmt parameter specify the format to use for that
name (e.g. to the style used in HOA, or that used by print_dot()).
- spot::simplify_acceptance() was already merging identical acceptance
sets, and detecting complementary sets i and j to perform the following
simplifications
Fin(i) & Inf(j) = Fin(i)
Fin(i) | Inf(j) = Inf(i)
It now additionally applies the following rules (again assuming i
and j are complementary):
Fin(i) & Fin(j) = f Inf(i) | Inf(j) = t
Fin(i) & Inf(i) = f Fin(i) | Inf(i) = t
Deprecation notices:
(These functions still work but compilers emit warnings.)
......
......@@ -174,15 +174,18 @@ namespace spot
{
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)
if (!tmp.empty())
{
inf &= std::move(tmp);
pos -= pos->sub.size + 1;
continue;
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);
......@@ -190,8 +193,18 @@ namespace spot
}
while (pos > start);
// Fin(i) & Inf(i) = f;
if (inf.front().mark & seen_fin)
return acc_cond::acc_code::f();
for (auto m: seen_fin.sets())
inf.front().mark -= complement[m];
{
acc_cond::mark_t cm = complement[m];
// Fin(i) & Fin(!i) = f;
if (cm & seen_fin)
return acc_cond::acc_code::f();
// Inf({!i}) & Fin({i}) = Fin({i})
inf.front().mark -= complement[m];
}
return inf & res;
}
......@@ -205,15 +218,18 @@ namespace spot
{
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)
if (!tmp.empty())
{
fin |= std::move(tmp);
pos -= pos->sub.size + 1;
continue;
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);
......@@ -221,9 +237,18 @@ namespace spot
}
while (pos > start);
// Fin(i) | Inf(i) = t;
if (fin.front().mark & seen_inf)
return acc_cond::acc_code::t();
for (auto m: seen_inf.sets())
fin.front().mark -= complement[m];
{
acc_cond::mark_t cm = complement[m];
// Inf({i}) | Inf({!i}) = t;
if (cm & seen_inf)
return acc_cond::acc_code::t();
// Fin({!i}) | Inf({i}) = Inf({i})
fin.front().mark -= complement[m];
}
return res | fin;
}
case acc_cond::acc_op::Fin:
......
......@@ -23,28 +23,48 @@
namespace spot
{
/// \ingroup twa_algorithms
/// \brief Remove useless acceptance sets
///
/// This removes from the automaton the acceptance marks that are
/// not used in the acceptance condition. This also removes from
/// the acceptance conditions the terms that corresponds to empty
/// or full sets.
///
/// If \a strip is true (the default), the remaining acceptance set
/// numbers will be shifted down to reduce maximal number of
/// acceptance sets used.
SPOT_API twa_graph_ptr
cleanup_acceptance_here(twa_graph_ptr aut, bool strip = true);
/// \ingroup twa_algorithms
/// \brief Remove useless acceptance sets
///
/// This removes from the automaton the acceptance marks that are
/// not used in the acceptance condition. This also removes from
/// the acceptance conditions the terms that corresponds to empty
/// or full sets.
///
SPOT_API twa_graph_ptr
cleanup_acceptance(const_twa_graph_ptr aut);
/// @{
/// \ingroup twa_algorithms
/// \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.
/// Does evereything cleanup_acceptance() does, but additionally:
/// merge identical sets, detect whether to sets i and j are
/// complementary to apply the following reductions:
/// - `Fin(i) & Inf(j) = Fin(i)`
/// - `Fin(i) & Fin(j) = f`
/// - `Fin(i) & Inf(i) = f`
/// - `Fin(i) | Inf(j) = Inf(j)`
/// - `Inf(i) | Inf(j) = t`
/// - `Fin(i) | Inf(i) = t`
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);
/// @}
}
......@@ -113,16 +113,88 @@ assert hoa == """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 2 (Fin(0) & Inf(0)) | (Fin(1) & Inf(1))
acc-name: none
Acceptance: 0 f
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
[0] 1
State: 1
[0] 1
[1] 2
State: 2
[1] 0
--END--"""
aut = spot.automaton("""
HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 4 (Inf(0) | Fin(1)) & (Inf(2) | Fin(3))
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0] 1 {0}
[0] 1 {0 1}
State: 1
[0] 1 {1}
[1] 2 {0 1}
[0] 1 {2 3}
[1] 2 {0 1 3}
State: 2
[1] 0 {1}
[1] 0 {2 3}
--END--""")
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
assert hoa == """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 2 Fin(1) | Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0] 1
State: 1
[0] 1 {0 1}
[1] 2 {1}
State: 2
[1] 0 {0 1}
--END--"""
aut = spot.automaton("""
HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 4 (Inf(0) | Fin(1)) & (Inf(2) | Fin(3))
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0] 1 {0 1}
State: 1
[0] 1 {2 3}
[1] 2 {0 1 2 3}
State: 2
[1] 0 {2 3}
--END--""")
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
assert hoa == """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
[0] 1
State: 1
[0] 1
[1] 2
State: 2
[1] 0
--END--"""
aut = spot.automaton("""HOA: v1
......@@ -645,3 +717,69 @@ State: 1
[0] 1
[!0] 0
--END--"""
aut = spot.automaton("""HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 4 Fin(0) & Fin(1) & Inf(2)
--BODY--
State: 0
[0] 1 {0}
State: 1
[0] 1 {1 2}
[1] 2 {0 2}
State: 2
[1] 0 {1}
--END--""")
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
assert hoa == """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
acc-name: none
Acceptance: 0 f
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
[0] 1
State: 1
[0] 1
[1] 2
State: 2
[1] 0
--END--"""
aut = spot.automaton("""HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 4 Inf(0) | Inf(1) | Inf(2)
--BODY--
State: 0
[0] 1 {0}
State: 1
[0] 1 {1 2}
[1] 2 {0 2}
State: 2
[1] 0 {1}
--END--""")
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
assert hoa == """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
[0] 1
State: 1
[0] 1
[1] 2
State: 2
[1] 0
--END--"""
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