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

twa_run: reduce now diagnoses rejecting runs

Browse source 
Part of #471.

* spot/twaalgos/emptiness.cc: Throw an exception if
the cycle is rejecting.
* spot/twaalgos/emptiness.hh: Document this behavior.
* tests/python/except.py: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2021-07-07 17:20:33 +02:00
parent f493f72015
commit 09e4ab74a1
3 changed files with 26 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

11
spot/twaalgos/emptiness.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2011-2019 Laboratoire de Recherche et
// Copyright (C) 2009, 2011-2019, 2021 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -343,8 +343,14 @@ namespace spot
state_set seen;
const state_set* target;
};
[[noreturn]] static void report_rejecting_cycle()
{
throw std::runtime_error("twa_run::reduce() expects an accepting cycle");
}
}
twa_run_ptr twa_run::reduce() const
{
ensure_non_empty_cycle("twa_run::reduce()");
@ -368,7 +374,8 @@ namespace spot
twa_run::steps::const_iterator seg = cycle.end();
do
{
assert(seg != cycle.begin());
if (SPOT_UNLIKELY(seg == cycle.begin()))
report_rejecting_cycle();
--seg;
seen_acc |= seg->acc;
}

5
spot/twaalgos/emptiness.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2013-2018, 2020 Laboratoire de
// Copyright (C) 2011, 2013-2018, 2020-2021 Laboratoire de
// Recherche et Developpement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -419,6 +419,9 @@ namespace spot
/// this fragment with fewer edges than in the original cycle.
/// (This step works best in Fin-less automata.) And then trying
/// to find a shorter prefix leading to any state of the cycle.
///
/// An <code>std::runtime_error</code> is thrown if the run
/// to reduce is not accepting.
twa_run_ptr reduce() const;
/// \brief Project an accepting run

13
tests/python/except.py
View file

@ -134,6 +134,19 @@ except RuntimeError as e:
else:
report_missing_exception()
a = spot.translate('Fa')
a = spot.to_generalized_rabin(a, False)
r = a.accepting_run()
r = r.reduce()
assert r.cycle[0].acc == spot.mark_t([1])
r.cycle[0].acc = spot.mark_t([0])
try:
r.reduce();
except RuntimeError as e:
assert "expects an accepting cycle" in str(e)
else:
report_missing_exception()
f = spot.formula('GF(a | Gb)')
try:
spot.gf_guarantee_to_ba(f, spot._bdd_dict)