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

stength: fix detection of terminal automata

Browse source 
Fixes issue #553.

* spot/twaalgos/strength.cc (is_type_automaton): Make sure an
accepting SCC is not followed by a rejecting one.
(is_terminal_automaton): Mark the third-argument version deprecated.
* spot/twaalgos/strength.hh: Adjust.
* spot/twaalgos/couvreurnew.cc: Remove the inappropriate terminal
optimization.
* bin/ltlfilt.cc, spot/tl/hierarchy.cc, spot/twaalgos/gfguarantee.cc,
tests/core/ikwiad.cc: Remove usage of the third argument of
is_terminal_automaton.
* tests/core/readsave.test, tests/core/strength.test: Adjust test
cases.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2023-11-21 16:40:33 +01:00
parent 63362d535f
commit 62fb0c354e
10 changed files with 75 additions and 82 deletions
Download patch file Download diff file Expand all files Collapse all files

16
NEWS
View file

@ -166,6 +166,22 @@ New in spot 2.11.6.dev (not yet released)
computation on that color that caused it to crash with a "Too many
acceptance sets used" message. (issue #552)
- The detection of terminal automata used did not exactly
match the definition used in the HOA format. The definition
of a terminal automaton is supposed to be:
1. the automaton is weak
2. its accepting SCCs are complete
3. no accepting cycle can reach a rejecting cycle
However the implementation actually replaced the last point
by the following variant:
3'. no accepting edge can reach a rejecting cycle
This caused issues in automata with t acceptance. Fixing the code
by replacing 3' by 3 this also made the third argument of
is_terminal_automaton(), an optional boolean indicating whether
transition between SCCs should be ignored when computing 3',
completely obsolete. This third argument has been marked as
depreated. (Issue #553)
New in spot 2.11.6 (2023-08-01)
Bug fixes:

2
bin/ltlfilt.cc
View file

@ -843,7 +843,7 @@ namespace
{
spot::scc_info si(min);
matched &= !guarantee
|| is_terminal_automaton(min, &si, true);
|| is_terminal_automaton(min, &si);
matched &= !safety || is_safety_automaton(min, &si);
}
}

4
spot/tl/hierarchy.cc
View file

@ -286,9 +286,7 @@ namespace spot
if (aut != min) // An obligation.
{
scc_info si(min);
// The minimba WDBA can have some trivial accepting SCCs
// that we should ignore in is_terminal_automaton().
bool g = is_terminal_automaton(min, &si, true);
bool g = is_terminal_automaton(min, &si);
bool s = is_safety_automaton(min, &si);
if (g)
return s ? 'B' : 'G';

55
spot/twaalgos/couvreurnew.cc
View file

@ -549,10 +549,7 @@ namespace spot
return run_;
}
// A simple enum for the different automata strengths.
enum twa_strength { STRONG, WEAK, TERMINAL };
template<bool is_explicit, twa_strength strength>
template<bool is_explicit, bool is_strong>
class couvreur99_new : public emptiness_check, public ec_statistics
{
using T = twa_iteration<is_explicit>;
@ -696,7 +693,7 @@ namespace spot
state_t init = T::initial_state(ecs_->aut);
ecs_->h[init] = 1;
ecs_->root.push(1);
if (strength == STRONG)
if (is_strong)
arc.push({});
auto iter = T::succ(ecs_->aut, init);
todo.emplace(init, iter);
@ -706,7 +703,7 @@ namespace spot
while (!todo.empty())
{
if (strength == STRONG)
if (is_strong)
assert(ecs_->root.size() == arc.size());
// We are looking at the next successor in SUCC.
@ -727,7 +724,7 @@ namespace spot
assert(!ecs_->root.empty());
if (ecs_->root.top().index == ecs_->h[curr])
{
if (strength == STRONG)
if (is_strong)
{
assert(!arc.empty());
arc.pop();
@ -759,21 +756,7 @@ namespace spot
}
// Fetch the values we are interested in...
auto acc = succ->acc();
if (!need_accepting_run)
if (strength == TERMINAL && ecs_->aut->acc().accepting(acc))
{
// We have found an accepting SCC.
// Release all iterators in todo.
while (!todo.empty())
{
T::it_destroy(ecs_->aut, todo.top().second);
todo.pop();
dec_depth();
}
// We do not need an accepting run.
return true;
}
acc_cond::mark_t acc = succ->acc();
state_t dest = succ->dst();
// ... and point the iterator to the next successor, for
// the next iteration.
@ -788,7 +771,7 @@ namespace spot
// Yes. Bump number, stack the stack, and register its
// successors for later processing.
ecs_->root.push(++num);
if (strength == STRONG)
if (is_strong)
arc.push(acc);
iterator_t iter = T::succ(ecs_->aut, dest);
todo.emplace(dest, iter);
@ -818,7 +801,7 @@ namespace spot
while (threshold < ecs_->root.top().index)
{
assert(!ecs_->root.empty());
if (strength == STRONG)
if (is_strong)
{
assert(!arc.empty());
acc |= ecs_->root.top().condition;
@ -864,20 +847,18 @@ namespace spot
} // anonymous namespace
template<twa_strength strength>
using cna = couvreur99_new<false, strength>;
template<twa_strength strength>
using cne = couvreur99_new<true, strength>;
template<bool is_strong>
using cna = couvreur99_new<false, is_strong>;
template<bool is_strong>
using cne = couvreur99_new<true, is_strong>;
emptiness_check_ptr
get_couvreur99_new_abstract(const const_twa_ptr& a, option_map o)
{
// NB: The order of the if's matter.
if (a->prop_terminal())
return SPOT_make_shared_enabled__(cna<TERMINAL>, a, o);
if (a->prop_weak())
return SPOT_make_shared_enabled__(cna<WEAK>, a, o);
return SPOT_make_shared_enabled__(cna<STRONG>, a, o);
return SPOT_make_shared_enabled__(cna<false>, a, o);
else
return SPOT_make_shared_enabled__(cna<true>, a, o);
}
emptiness_check_ptr
@ -886,12 +867,10 @@ namespace spot
const_twa_graph_ptr ag = std::dynamic_pointer_cast<const twa_graph>(a);
if (ag) // the automaton is explicit
{
// NB: The order of the if's matter.
if (a->prop_terminal())
return SPOT_make_shared_enabled__(cne<TERMINAL>, ag, o);
if (a->prop_weak())
return SPOT_make_shared_enabled__(cne<WEAK>, ag, o);
return SPOT_make_shared_enabled__(cne<STRONG>, ag, o);
return SPOT_make_shared_enabled__(cne<false>, ag, o);
else
return SPOT_make_shared_enabled__(cne<true>, ag, o);
}
else // the automaton is abstract
{

6
spot/twaalgos/gfguarantee.cc
View file

@ -57,7 +57,7 @@ namespace spot
bool want_merge_edges = false;
twa_graph_ptr aut = std::const_pointer_cast<twa_graph>(si.get_aut());
if (!is_terminal_automaton(aut, &si, true))
if (!is_terminal_automaton(aut, &si))
throw std::runtime_error("g_f_terminal() expects a terminal automaton");
// If a terminal automaton has only one SCC, it is either
@ -490,13 +490,13 @@ namespace spot
return nullptr;
scc_info si(reduced);
if (!is_terminal_automaton(reduced, &si, true))
if (!is_terminal_automaton(reduced, &si))
return nullptr;
do_g_f_terminal_inplace(si, state_based);
if (!deterministic)
{
scc_info si2(aut);
if (!is_terminal_automaton(aut, &si2, true))
if (!is_terminal_automaton(aut, &si2))
return reduced;
do_g_f_terminal_inplace(si2, state_based);
if (aut->num_states() < reduced->num_states())

44
spot/twaalgos/strength.cc
View file

@ -32,8 +32,7 @@ namespace spot
namespace
{
template <bool terminal, bool inweak = false, bool set = false>
bool is_type_automaton(const twa_graph_ptr& aut, scc_info* si,
bool ignore_trivial_term = false)
bool is_type_automaton(const twa_graph_ptr& aut, scc_info* si)
{
// Create an scc_info if the user did not give one to us.
bool need_si = !si;
@ -85,36 +84,29 @@ namespace spot
break;
}
}
if (terminal && si->is_accepting_scc(i) && !is_complete_scc(*si, i))
if (terminal && is_term && si->is_accepting_scc(i))
{
is_term = false;
if (!set)
break;
}
}
// A terminal automaton should accept any word that has a prefix
// leading to an accepting edge. In other words, we cannot have
// an accepting edge that goes into a rejecting SCC.
if (terminal && is_term && !ignore_trivial_term)
for (auto& e: aut->edges())
if (si->is_rejecting_scc(si->scc_of(e.dst))
&& aut->acc().accepting(e.acc))
is_term = is_complete_scc(*si, i);
if (is_term)
{
for (unsigned j: si->succ(i))
if (si->is_rejecting_scc(j))
{
is_term = false;
break;
}
}
if (!is_term && !set)
break;
}
}
exit:
if (need_si)
delete si;
if (set)
{
if (terminal)
{
if (!ignore_trivial_term)
aut->prop_terminal(is_term && is_weak);
else if (is_term && is_weak)
aut->prop_terminal(true);
}
aut->prop_weak(is_weak);
aut->prop_very_weak(is_single_state_scc && is_weak);
if (inweak)
@ -127,19 +119,23 @@ namespace spot
}
bool
is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* si,
bool ignore_trivial_term)
is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* si)
{
trival v = aut->prop_terminal();
if (v.is_known())
return v.is_true();
bool res =
is_type_automaton<true>(std::const_pointer_cast<twa_graph>(aut), si,
ignore_trivial_term);
is_type_automaton<true>(std::const_pointer_cast<twa_graph>(aut), si);
std::const_pointer_cast<twa_graph>(aut)->prop_terminal(res);
return res;
}
bool
is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* si, bool)
{
return is_terminal_automaton(aut, si);
}
bool
is_weak_automaton(const const_twa_graph_ptr& aut, scc_info* si)
{

19
spot/twaalgos/strength.hh
View file

@ -25,11 +25,8 @@ namespace spot
/// \brief Check whether an automaton is terminal.
///
/// An automaton is terminal if it is weak, all its accepting SCCs
/// are complete, and no accepting transitions lead to a
/// non-accepting SCC.
///
/// If ignore_trivial_scc is set, accepting transitions from trivial
/// SCCs are ignored.
/// are complete, and no accepting SCC may lead to a non-accepting
/// SCC.
///
/// This property guarantees that a word is accepted if it has some
/// prefix that reaches an accepting transition.
@ -43,8 +40,16 @@ namespace spot
/// the prop_terminal() property of the automaton as a side-effect,
/// so further calls will return in constant-time.
SPOT_API bool
is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr,
bool ignore_trivial_scc = false);
is_terminal_automaton(const const_twa_graph_ptr& aut,
scc_info* sm = nullptr);
// 3-arg form was deprecated in Spot 2.12
SPOT_DEPRECATED("is third argument of is_terminal_automaton()"
" is now ignored")
SPOT_API bool
is_terminal_automaton(const const_twa_graph_ptr& aut,
scc_info* sm, bool);
/// \brief Check whether an automaton is weak.
///

3
tests/core/ikwiad.cc
View file

@ -1368,8 +1368,7 @@ checked_main(int argc, char** argv)
}
else
{
bool g = is_terminal_automaton(ensure_digraph(a),
nullptr, true);
bool g = is_terminal_automaton(ensure_digraph(a));
bool s = is_safety_automaton(ensure_digraph(a));
if (g && !s)
{

2
tests/core/readsave.test
View file

@ -826,7 +826,7 @@ test `autfilt --is-terminal -c output4` = 0
sed 's/\[0\]/[t]/g' expect4 > output4d
test `autfilt -B --small output4d | autfilt --is-terminal -c` = 1
test `autfilt --is-terminal -c output4d` = 0 # FIXME: Issue #553
test `autfilt --is-terminal -c output4d` = 1 # Issue #553
autfilt -B -Hv --small input4 >output5
cat >expect5<<EOF

2
tests/core/strength.test
View file

@ -679,7 +679,7 @@ AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic very-weak
properties: deterministic terminal very-weak
--BODY--
State: 0
[t] 0