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

postproc: make sure WDBA have an acceptance set if BA is desired

Browse source 
* src/tgbaalgos/postproc.cc: Here.
* src/tgbatest/ltl2tgba.test: Make sure ltl2tgba -B 0 has one
acceptance set.
This commit is contained in:
Alexandre Duret-Lutz 2015-02-25 23:38:24 +01:00
parent f0b1b9438f
commit 095ac93b5b
2 changed files with 28 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/tgbaalgos/postproc.cc
View file

@ -33,6 +33,20 @@
namespace spot
{
namespace
{
static tgba_digraph_ptr
ensure_ba(tgba_digraph_ptr& a)
{
if (a->acc().num_sets() == 0)
{
auto m = a->set_single_acceptance_set();
for (auto& t: a->transitions())
t.acc = m;
}
return a;
}
}
postprocessor::postprocessor(const option_map* opt)
: type_(TGBA), pref_(Small), level_(High),
@ -106,7 +120,6 @@ namespace spot
}
}
tgba_digraph_ptr
postprocessor::do_degen(const tgba_digraph_ptr& a)
{
@ -204,11 +217,18 @@ namespace spot
bool reject_bigger = (PREF_ == Small) && (level_ == Medium);
dba = minimize_obligation(a, f, 0, reject_bigger);
if (dba && dba->is_inherently_weak() && dba->is_deterministic())
{
// The WDBA is a BA, so no degeneralization is required.
// We just need to add an acceptance set if there is none.
dba_is_minimal = dba_is_wdba = true;
if (type_ == BA)
ensure_ba(dba);
}
else
{
// Minimization failed.
dba = nullptr;
// The WDBA is a BA, so no degeneralization is required.
}
}
// Run a simulation when wdba failed (or was not run), or

3
src/tgbatest/ltl2tgba.test
View file

@ -97,6 +97,9 @@ EOF
run 0 ../checkpsl check.txt
# Make sure False has one acceptance set when generating Büchi automata
test 1 -eq `../../bin/ltl2tgba -B false --stats %a`
# In particular, Spot 0.9 would incorrectly reject the sequence:
# (a̅b;a̅b;a̅b̅);(a̅b;a̅b;a̅b̅);(a̅b;a̅b;a̅b̅);... in 'G!{(b;1)*;a}'
# This means the following automaton was incorrectly empty in Spot 0.9.