From d8a0f307eb31e7375b4fbef1f42ae828091c16d2 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 6 Mar 2020 23:23:13 +0100
Subject: [PATCH] product: fix handling of operand with false acceptance

* NEWS: Mention the issue.
* spot/twaalgos/product.cc: Fix it.
* tests/python/prodexpt.py: Test it.
---
 NEWS                     |  7 ++++++
 spot/twaalgos/product.cc | 49 +++++++++++++++++++++++++++-------------
 tests/python/prodexpt.py | 35 ++++++++++++++++++++++++++--
 3 files changed, 73 insertions(+), 18 deletions(-)

diff --git a/NEWS b/NEWS
index 4f689eeca..1ab4ea6d5 100644
--- a/NEWS
+++ b/NEWS
@@ -91,6 +91,13 @@ New in spot 2.8.6.dev (not yet released)
   - car() is a new variant of LAR algorithm that combines several
     strategies for paritazing any automaton.
 
+  Bugs fixed:
+
+  - Building a product between two complete automata where one operand
+    had false acceptance could create a incomplete automaton
+    incorrectly tagged as complete, causing the print_hoa() function
+    to raise an exception.
+
 New in spot 2.8.6 (2020-02-19)
 
   Bugs fixed:
diff --git a/spot/twaalgos/product.cc b/spot/twaalgos/product.cc
index f68192d15..84efbcf32 100644
--- a/spot/twaalgos/product.cc
+++ b/spot/twaalgos/product.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement
+// Copyright (C) 2014-2020 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -285,21 +285,34 @@ namespace spot
       if (!res)                 // aborted
         return nullptr;
 
-      // The product of two non-deterministic automata could be
-      // deterministic.  Likewise for non-complete automata.
-      if (left->prop_universal() && right->prop_universal())
-        res->prop_universal(true);
-      if (left->prop_complete() && right->prop_complete())
-        res->prop_complete(true);
-      if (left->prop_stutter_invariant() && right->prop_stutter_invariant())
-        res->prop_stutter_invariant(true);
-      if (left->prop_inherently_weak() && right->prop_inherently_weak())
-        res->prop_inherently_weak(true);
-      if (left->prop_weak() && right->prop_weak())
-        res->prop_weak(true);
-      if (left->prop_terminal() && right->prop_terminal())
-        res->prop_terminal(true);
-      res->prop_state_acc(left->prop_state_acc() && right->prop_state_acc());
+      if (res->acc().is_f())
+        {
+          assert(res->num_edges() == 0);
+          res->prop_universal(true);
+          res->prop_complete(false);
+          res->prop_stutter_invariant(true);
+          res->prop_terminal(true);
+          res->prop_state_acc(true);
+        }
+      else
+        {
+          // The product of two non-deterministic automata could be
+          // deterministic.  Likewise for non-complete automata.
+          if (left->prop_universal() && right->prop_universal())
+            res->prop_universal(true);
+          if (left->prop_complete() && right->prop_complete())
+            res->prop_complete(true);
+          if (left->prop_stutter_invariant() && right->prop_stutter_invariant())
+            res->prop_stutter_invariant(true);
+          if (left->prop_inherently_weak() && right->prop_inherently_weak())
+            res->prop_inherently_weak(true);
+          if (left->prop_weak() && right->prop_weak())
+            res->prop_weak(true);
+          if (left->prop_terminal() && right->prop_terminal())
+            res->prop_terminal(true);
+          res->prop_state_acc(left->prop_state_acc()
+                              && right->prop_state_acc());
+        }
       return res;
     }
   }
@@ -450,6 +463,10 @@ namespace spot
             {
               auto res = make_twa_graph(left->get_dict());
               res->new_state();
+              res->prop_terminal(true);
+              res->prop_stutter_invariant(true);
+              res->prop_universal(true);
+              res->prop_complete(false);
               return res;
             }
           return make_twa_graph(left, twa::prop_set::all());
diff --git a/tests/python/prodexpt.py b/tests/python/prodexpt.py
index 246fccba1..098bafb26 100644
--- a/tests/python/prodexpt.py
+++ b/tests/python/prodexpt.py
@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2016-2017, 2019 Laboratoire de Recherche et Développement de
-# l'Epita (LRDE).
+# Copyright (C) 2016-2017, 2019-2020 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -102,3 +102,34 @@ res = spot.product(left, right, spot.output_aborter(900, 9000))
 assert res is None
 res = spot.product(left, right, spot.output_aborter(1000, 9000))
 assert res is not None
+
+a, b = spot.automata("""HOA: v1 States: 1 Start: 0 AP: 0 acc-name: all
+Acceptance: 0 t properties: trans-labels explicit-labels state-acc complete
+properties: deterministic stutter-invariant weak --BODY-- State: 0 [t] 0
+--END-- HOA: v1 States: 1 Start: 0 AP: 0 acc-name: none Acceptance: 0 f
+properties: trans-labels explicit-labels state-acc complete properties:
+deterministic stutter-invariant weak --BODY-- State: 0 [t] 0 --END--""")
+out = spot.product(a, b).to_str()
+assert out == """HOA: v1
+States: 1
+Start: 0
+AP: 0
+acc-name: none
+Acceptance: 0 f
+properties: trans-labels explicit-labels state-acc deterministic
+properties: stutter-invariant terminal
+--BODY--
+State: 0
+--END--"""
+out = spot.product_susp(a, b).to_str()
+assert out == """HOA: v1
+States: 1
+Start: 0
+AP: 0
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc deterministic
+properties: stutter-invariant terminal
+--BODY--
+State: 0
+--END--"""