From 9464043d39fa50cb5f3c06d2ec9b3dca793d0820 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 14 Jan 2018 15:04:02 +0100 Subject: [PATCH] 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. --- NEWS | 4 ++ spot/twaalgos/totgba.cc | 17 +++++--- tests/Makefile.am | 1 + tests/python/streett_totgba2.py | 70 +++++++++++++++++++++++++++++++++ 4 files changed, 87 insertions(+), 5 deletions(-) create mode 100644 tests/python/streett_totgba2.py diff --git a/NEWS b/NEWS index fd2b86bf5..57447072e 100644 --- a/NEWS +++ b/NEWS @@ -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. diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index 9403d5075..ecf8b1c60 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -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); diff --git a/tests/Makefile.am b/tests/Makefile.am index ed0f6c4bc..de418f193 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -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 \ diff --git a/tests/python/streett_totgba2.py b/tests/python/streett_totgba2.py new file mode 100644 index 000000000..852eff0af --- /dev/null +++ b/tests/python/streett_totgba2.py @@ -0,0 +1,70 @@ +#!/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 . + +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)