diff --git a/NEWS b/NEWS index 1472d72d9..ad362d97d 100644 --- a/NEWS +++ b/NEWS @@ -28,6 +28,12 @@ New in spot 2.7.0.dev (not yet release) - The core translation for unambiguous automata was incorrectly tagging some non-weak automata as weak. + - The product_susp() function used to multiply an automaton with a + suspendable automaton could incorrectly build transition-based + automata when multipliying two state-based automata. This caused + ltl2tgba to emit error messages such as: "automaton has + transition-based acceptance despite prop_state_acc()==true" + New in spot 2.7 (2018-12-11) Command-line tools: diff --git a/spot/twaalgos/product.cc b/spot/twaalgos/product.cc index b03e28893..5579e706e 100644 --- a/spot/twaalgos/product.cc +++ b/spot/twaalgos/product.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -367,7 +367,7 @@ namespace spot auto target_scc = [&](unsigned scc) -> bool { return (!si.is_trivial(scc) - && (sync_all ||si.is_accepting_scc(scc) == and_acc)); + && (sync_all || si.is_accepting_scc(scc) == and_acc)); }; if (target_scc(si.scc_of(left_init))) @@ -385,20 +385,15 @@ namespace spot for (auto& l: left->out(top.first.first)) if (!target_scc(si.scc_of(l.dst))) { - if (!sbacc || top.first.second == -1U) - { - res->new_edge(top.second, new_state(l.dst, -1U), l.cond, - merge_acc(l.acc, rejmark)); - } - else - { - // This edge leaves a target SCC, but we build a - // state-based automaton, so make sure we still - // use the same acceptance marks as in the SCC. - auto rm = right->state_acc_sets(top.first.second); - res->new_edge(top.second, new_state(l.dst, -1U), l.cond, - merge_acc(l.acc, rm)); - } + acc_cond::mark_t right_acc = + (sbacc && top.first.second != -1U) + // This edge leaves a target SCC, but we build a + // state-based automaton, so make sure we still use + // the same acceptance marks as in the SCC we leave. + ? right->state_acc_sets(top.first.second) + : rejmark; + res->new_edge(top.second, new_state(l.dst, -1U), l.cond, + merge_acc(l.acc, right_acc)); } else { @@ -411,8 +406,15 @@ namespace spot if (cond == bddfalse) continue; auto dst = new_state(l.dst, r.dst); + + // For state-based automata, we cannot use the + // right-mark when entering a target SCC, because + // another sibling transition might be going to a + // non-target SCC without this mark. + acc_cond::mark_t right_acc = + (sbacc && top.first.second == -1U) ? rejmark : r.acc; res->new_edge(top.second, dst, cond, - merge_acc(l.acc, r.acc)); + merge_acc(l.acc, right_acc)); } } } diff --git a/tests/Makefile.am b/tests/Makefile.am index caad281c9..2f42108f7 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -273,6 +273,7 @@ TESTS_twa = \ core/monitor.test \ core/dra2dba.test \ core/unambig.test \ + core/unambig2.test \ core/ltlcross4.test \ core/ltl3ba.test \ core/streett.test \ diff --git a/tests/core/unambig2.test b/tests/core/unambig2.test new file mode 100755 index 000000000..c5b428fe3 --- /dev/null +++ b/tests/core/unambig2.test @@ -0,0 +1,123 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2019 Laboratoire de Recherche et +# Developpement 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 . + +. ./defs + +set -e + +# The following list of formulas was reported by Simon Jantsch. +cat >errors <