product_susp: fix product of state-based automata

Reported by Simon Jantsch.

* spot/twaalgos/product.cc: Here.
* tests/core/unambig2.test: New file, testing this plus
the previous patch.
* tests/Makefile.am: Add unambig2.test.
* NEWS: Mention the bug.

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:

spot/twaalgos/product.cc

 // -*- 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));
                   }
               }
         }

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 \

tests/core/unambig2.test

+#!/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 <http://www.gnu.org/licenses/>.
+
+. ./defs
+
+set -e
+
+# The following list of formulas was reported by Simon Jantsch.
+cat >errors <<EOF
+| G ! "2" F & X "1" F "2"
+| V X "2" "2" F W "2" f
+| & "2" G "1" F G "2"
+i U t "2" U F "2" "1"
+& G F "1" i "1" F "2"
+& G F "2" ^ "2" X G "2"
+| F G "1" & "1" X "1"
+i W "2" G "1" G "1"
+! | | "2" G "1" F G "2"
+i | G "1" W "2" "1" F G "2"
+i ^ "2" G X "2" F G "1"
+& & "2" G F "1" U t "1"
+| F G "1" i F "1" "2"
+| U "1" X ! "1" F G ! "1"
+! & ! F G "1" i G "1" "2"
+i ! F G "2" i U t "2" "1"
+| ! G F "2" & "2" G "1"
+| & "1" ! U t "2" F ! F "2"
+& G ! G "1" | "1" X "1"
+& G ! G "2" | "1" F "2"
+i G F "2" & "2" X "2"
+& ! G "1" W "2" G "1"
+& | "2" F "1" G F "2"
+| F G "1" & "1" W "2" f
+& F "2" W "1" ! F "2"
+| G | X "1" G "2" F ! F "1"
+| F W "2" f i F "2" "1"
+& W F "2" f i G "1" "2"
+| ! F "2" U F "2" "1"
+& G F "2" ! & "2" G "1"
+| | "1" ! F "2" F G "1"
+& & "2" U t "1" G U t "2"
+i G U t "2" & "1" ! F "2"
+& G ! G "1" W X "1" "1"
+| & "2" X "1" F G "1"
+i G F "2" & "2" G "1"
+! & & "2" F "1" G F "1"
+& & "1" F "2" ! F G "2"
+| & "2" X "2" F W "2" f
+i X W "1" G "2" G "2"
+i X G "2" ! W "1" G "2"
+! i i "2" X "2" F G "2"
+& G U t "2" i G "1" "2"
+i G F "1" & F "2" X "1"
+| F G "2" & "1" X "2"
+i G F "2" & ! "2" G "1"
+| G ! "2" U U t "2" "1"
+i W F "2" f ! V "2" X "1"
+| F V f "2" & "2" X "2"
+& | "2" F "1" G F "1"
+& F "2" ! U F "2" "1"
+& G ! G "1" | "2" X "2"
+G ^ ! G "2" F ^ "1" G ! G "2"
+i ! F G "2" i "1" ! F "2"
+& G F "2" i W "2" f "1"
+& F "2" ! U F "2" ! "1"
+& G F "1" i G "1" "2"
+i G F "2" & "1" X "1"
+! i W ! G "2" f V X "2" "2"
+| G i "1" X "2" i G F "2" G "1"
+& F "2" W "1" W ! "2" f
+| F G ! "2" & "2" X "2"
+! & i "2" F "1" ! U t G "2"
+| F G "2" & "1" ! F "2"
+! & U t "1" ! U F "1" "2"
+! | | "2" ! G ! G "2" G "1"
+| i F "2" "1" F G "1"
+| F G "1" & ! "1" G "2"
+& | "1" X "1" G F "1"
+& i "2" F "1" G F "1"
+& & "1" F "2" G F "1"
+! & F "1" ! X U F "1" "2"
+i ! F G "2" V F "2" "1"
+i ! U ! G "1" "2" G "1"
+i i "1" F "2" F ! F "2"
+i F "1" | "2" F G "2"
+& U t "2" W "1" ! F "2"
+i G | G "2" W "1" "2" G "2"
+! & ! F G "2" | F "2" ! F "2"
+| F W "1" f & "2" ! F "1"
+| F G "1" U ! "1" X "1"
+& i X "2" "2" ! F G "2"
+& | "1" X "1" ! F W "1" f
+& ! G "2" ! U ! G "2" "1"
+| F G "2" & "1" W "2" f
+& i ! U t "1" "2" G ! G "1"
+& V "2" X "1" G F "1"
+| F G "2" & ! "2" W "1" f
+! i W "2" F "1" F G "2"
+& & "2" G F "2" ! G "1"
+| ! F "1" F & F "1" X "2"
+| F G "2" & ! "2" X "2"
+| F G "2" i F "2" & "1" "2"
+i i X "2" "2" F G "2"
+EOF
+
+ltlcross --lbt-input -F errors 'ltl2tgba -U -B --low' 'ltl2tgba'