Commit 9464043d authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

fix streett_to_generalized_buchi

Fixes #316.

* spot/twaalgos/totgba.cc: Fix confusing definition of scc_inf_wo_fin.
* tests/python/streett_totgba2.py: New test case.
* tests/Makefile.am: Add it.
* NEWS: Mention the bug.
parent 8a74ae6c
......@@ -243,6 +243,10 @@ New in spot 2.4.4.dev (net yet released)
set. In spot 2.4.x this function was only used by autfilt
--simplify-acceptance; in 2.5 it is now used in remove_fin().
- spot::streett_to_generalized_buchi() could generate incorrect
automata with empty language if some Fin set did not intersect all
accepting SCCs (in other words, the fix from 2.4.1 was incorrect).
- ltlcross could crash when calling remove_fin() on an automaton
with 32 acceptance sets would need an additional set.
......
......@@ -556,8 +556,9 @@ namespace spot
else
inf_alone |= pair.inf;
for (unsigned mark: pair.inf.sets())
inf_to_finpairs[mark] |= pair.fin;
if (pair.inf)
for (unsigned mark: pair.inf.sets())
inf_to_finpairs[mark] |= pair.fin;
}
scc_info si(in, scc_info_options::NONE);
......@@ -573,13 +574,19 @@ namespace spot
auto acc_fin = acc & fin; // {0, 2, 4,6}
auto acc_inf = acc & inf; // { 1, 3, 7,9}
acc_cond::mark_t fin_wo_inf = 0U;
// Fin sets that are alone either because the acceptance
// condition has not matching Inf, or because the SCC the not
// intersect the matching inf.
for (unsigned mark: acc_fin.sets())
if (!fin_to_infpairs[mark] || (fin_to_infpairs[mark] - acc_inf))
fin_wo_inf.set(mark);
// Inf sets that *do* have a matching Fin in the acceptance
// condition but without matching Fin in the SCC: they can be
// considered as always present in the SCC.
acc_cond::mark_t inf_wo_fin = 0U;
for (unsigned mark: acc_inf.sets())
if (!inf_to_finpairs[mark] || (inf_to_finpairs[mark] - acc_fin))
for (unsigned mark: inf.sets())
if (inf_to_finpairs[mark] && (inf_to_finpairs[mark] - acc_fin))
inf_wo_fin.set(mark);
sccfi.emplace_back(fin_wo_inf, inf_wo_fin,
......@@ -671,7 +678,7 @@ namespace spot
// If the acceptance is (Fin(0) | Inf(1)) & Inf(2)
// but we do not see any Fin set in this SCC, a
// mark {2} should become {1,2} before striping.
acc = (t.acc | (inf - scc_inf_wo_fin)).strip(to_strip);
acc = (t.acc | scc_inf_wo_fin).strip(to_strip);
}
assert((acc & out->acc().all_sets()) == acc);
......
......@@ -388,6 +388,7 @@ TESTS_python = \
python/setxor.py \
python/simstate.py \
python/streett_totgba.py \
python/streett_totgba2.py \
python/rs_like.py \
python/sum.py \
python/trival.py \
......
#!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2018 Laboratoire de Recherche et Développement de
# l'EPITA.
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 3 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
import spot
# Issue 316
a = spot.automaton("""
HOA: v1
States: 8
Start: 0
AP: 3 "b" "a" "c"
Acceptance: 5 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) & Inf(4)
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
[!0&!2] 1
[0&!2] 2
[2] 3
State: 1
[0&2] 4
[0&1&2] 5
State: 2
[!0&!2] 1
[!0&2] 3
State: 3
[!0&!2] 1
[!0&2] 3
[0&2] 4
[0&1&2] 5
State: 4
[2] 4
[0&1&2] 5
[!0&!2] 6
State: 5 {4}
[1&2] 5
[!0&1&!2] 7
State: 6
[0&2] 4
[0&1&2] 5
State: 7 {1 3 4}
[0&1&2] 5
--END--
""")
tgba = spot.streett_to_generalized_buchi(a)
assert tgba.acc().is_generalized_buchi()
ba = spot.simplify_acceptance(a)
assert ba.acc().is_buchi()
nba = spot.dualize(ba.postprocess('generic', 'deterministic'))
ntgba = spot.dualize(tgba.postprocess('generic', 'deterministic'))
assert not ba.intersects(ntgba)
assert not tgba.intersects(nba)
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