product: Büchi|Büchi=Büchi, CoBüchi&CoBüchi=CoBüchi

Improve the construction of the above constructions, saving colors.

* spot/twaalgos/product.cc: Here.
* spot/twaalgos/product.hh, NEWS: Mention it.
* tests/core/prodchain.test, tests/core/prodor.test,
tests/python/_product_weak.ipynb: Adjust.

NEWS

@@ -114,10 +114,14 @@ New in spot 2.10.6.dev  (not yet released)
     to obtain a simple model checker (that returns true or false,
     without counterexample).
 
+  - product() learned that the product of two co-Büchi automata
+    is a co-Büchi automaton.  And product_or() learned that the
+    "or"-product of two Büchi automata is a Büchi automaton.
+
   - spot::parallel_policy is an object that can be passed to some
     algorithm to specify how many threads can be used if Spot has been
     compiled with --enable-pthread.  Currently, only
-    twa_graph::merge_states() support it.
+    twa_graph::merge_states() supports it.
 
  Python bindings:
 

spot/twaalgos/product.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014-2020 Laboratoire de Recherche et Développement
+// Copyright (C) 2014-2020, 2022 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -122,8 +122,23 @@ namespace spot
       res->copy_ap_of(left);
       res->copy_ap_of(right);
 
+      auto& lacc = left->acc();
+      auto& racc = right->acc();
+
       bool leftweak = left->prop_weak().is_true();
       bool rightweak = right->prop_weak().is_true();
+
+      // The conjunction of two co-Büchi automata is a co-Büchi automaton.
+      // The disjunction of two Büchi automata is a Büchi automaton.
+      //
+      // The code to handle this case is similar to the weak_weak case,
+      // except we do not set the weak property on the result.
+      if (!leftweak
+          && !rightweak
+          && ((aop == and_acc && lacc.is_co_buchi() && racc.is_co_buchi())
+              || (aop == or_acc && lacc.is_buchi() && racc.is_buchi())))
+        goto and_cobuchi_or_buchi;
+
       // We have optimization to the standard product in case one
       // of the arguments is weak.
       if (leftweak || rightweak)
@@ -132,14 +147,13 @@ namespace spot
           // t, f, Büchi or co-Büchi.  We use co-Büchi only when
           // t and f cannot be used, and both acceptance conditions
           // are in {t,f,co-Büchi}.
-          if (leftweak && rightweak)
+          if ((leftweak && rightweak))
             {
             weak_weak:
               res->prop_weak(true);
+            and_cobuchi_or_buchi:
               acc_cond::mark_t accmark = {0};
               acc_cond::mark_t rejmark = {};
-              auto& lacc = left->acc();
-              auto& racc = right->acc();
               if ((lacc.is_co_buchi() && (racc.is_co_buchi()
                                          || racc.num_sets() == 0))
                   || (lacc.num_sets() == 0 && racc.is_co_buchi()))

spot/twaalgos/product.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014-2015, 2018-2020 Laboratoire de Recherche et
+// Copyright (C) 2014-2015, 2018-2020, 2022 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -37,10 +37,14 @@ namespace spot
   /// The resulting automaton will accept the intersection of both
   /// languages and have an acceptance condition that is the
   /// conjunction of the acceptance conditions of the two input
-  /// automata.  In case one of the left or right automaton is weak,
+  /// automata.
-  /// the acceptance condition of the result is made simpler: it
+  ///
-  /// usually is the acceptance condition of the other argument,
+  /// As an optionmization, in case one of the left or right automaton
+  /// is weak, the acceptance condition of the result is made simpler:
+  /// it usually is the acceptance condition of the other argument,
   /// therefore avoiding the need to introduce new accepting sets.
+  /// Similarly, the product of two co-Büchi automata will be a
+  /// co-Büchi automaton.
   ///
   /// The algorithm also defines a named property called
   /// "product-states" with type spot::product_states.  This stores
@@ -64,10 +68,14 @@ namespace spot
   /// languages recognized by each input automaton (with its initial
   /// state changed) and have an acceptance condition that is the
   /// conjunction of the acceptance conditions of the two input
-  /// automata.  In case one of the left or right automaton is weak,
+  /// automata.
-  /// the acceptance condition of the result is made simpler: it
+  ///
-  /// usually is the acceptance condition of the other argument,
+  /// As an optionmization, in case one of the left or right automaton
+  /// is weak, the acceptance condition of the result is made simpler:
+  /// it usually is the acceptance condition of the other argument,
   /// therefore avoiding the need to introduce new accepting sets.
+  /// Similarly, the product of two co-Büchi automata will be a
+  /// co-Büchi automaton.
   ///
   /// The algorithm also defines a named property called
   /// "product-states" with type spot::product_states.  This stores
@@ -89,10 +97,15 @@ namespace spot
   /// The resulting automaton will accept the union of both
   /// languages and have an acceptance condition that is the
   /// disjunction of the acceptance conditions of the two input
-  /// automata.  In case one of the left or right automaton is weak,
+  /// automata.
-  /// the acceptance condition of the result is made simpler: it
+  ///
-  /// usually is the acceptance condition of the other argument,
+  /// As an optionmization, in case one of the left or right automaton
+  /// is weak, the acceptance condition of the result is made simpler:
+  /// it usually is the acceptance condition of the other argument,
   /// therefore avoiding the need to introduce new accepting sets.
+  /// Similarly, the product_pr of two Büchi automata will be a
+  /// Büchi automaton.
+  ///
   ///
   /// The algorithm also defines a named property called
   /// "product-states" with type spot::product_states.  This stores
@@ -112,10 +125,14 @@ namespace spot
   /// recognized by each input automaton (with its initial state
   /// changed) and have an acceptance condition that is the
   /// disjunction of the acceptance conditions of the two input
-  /// automata. In case one of the left or right automaton is weak,
+  /// automata.
-  /// the acceptance condition of the result is made simpler: it
+  ///
-  /// usually is the acceptance condition of the other argument,
+  /// As an optionmization, in case one of the left or right automaton
+  /// is weak, the acceptance condition of the result is made simpler:
+  /// it usually is the acceptance condition of the other argument,
   /// therefore avoiding the need to introduce new accepting sets.
+  /// Similarly, the product_pr of two Büchi automata will be a
+  /// Büchi automaton.
   ///
   /// The algorithm also defines a named property called
   /// "product-states" with type spot::product_states.  This stores

tests/core/prodchain.test

@@ -32,12 +32,12 @@ for i in *.hoa; do
   shift
 done
 shift
-if $MAX_ACCSETS -eq 32; then
+if [ $MAX_ACCSETS -eq 32 ]; then
   autfilt "$@" 2> error && exit 1
   grep 'Too many acceptance sets used' error
 fi
-autfilt -B "$@" > result
+autfilt -B --low "$@" > result
-test "127,253,508,1" = `autfilt --stats=%s,%e,%t,%a result`
+test "4,7,16,1" = `autfilt --stats=%s,%e,%t,%a result`
 
 set x
 shift
@@ -46,9 +46,37 @@ for i in *.hoa; do
   shift
 done
 shift
-if $MAX_ACCSETS -eq 32; then
+autfilt -B --low "$@" > result
-  autfilt "$@" 2> error && exit 1
+test "45,89,180,1" = `autfilt --stats=%s,%e,%t,%a result`
+
+
+set x
+shift
+for i in 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 \
+         22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42; do
+  ltl2tgba -D --cobuchi -S "{a[*$i]}<>->FGb" > $i.hoa
+done
+for i in *.hoa; do
+  set x "$@" --product $i
+  shift
+done
+shift
+autfilt -D --cobuchi --low -S "$@" > result
+test "85,170,174,1" = `autfilt --stats=%s,%e,%t,%a result`
+
+set x
+shift
+for i in *.hoa; do
+  set x "$@" --product-or $i
+  shift
+done
+shift
+if [ $MAX_ACCSETS -eq 32 ]; then
+  autfilt --cobuchi -S "$@" 2> error && exit 1
   grep 'Too many acceptance sets used' error
 fi
-autfilt -B "$@" > result
+# FIXME: implement degeneralization for generalized-co-Büchi
-test "45,89,180,1" = `autfilt --stats=%s,%e,%t,%a result`
+# autfilt --cobuchi --low -S "$@" > result
+# test "45,89,180,1" = `autfilt --stats=%s,%e,%t,%a result`
+
+true

tests/core/prodor.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2015, 2017-2018, 2021 Laboratoire de Recherche et
+# Copyright (C) 2015, 2017-2018, 2021-2022 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -154,8 +154,8 @@ diff por.hoa exp
 
 ltl2tgba -BDH 'GFa' > gfa.hoa
 ltl2tgba -x '!wdba-minimize' -DH 'Xb' > xb.hoa
-autfilt --product-or gfa.hoa xb.hoa -H > por.hoa
+autfilt --product-or gfa.hoa xb.hoa -H > por2.hoa
-cat por.hoa
+cat por2.hoa
 
 cat >exp <<EOF
 HOA: v1
@@ -194,4 +194,4 @@ State: 6
 [!0] 6
 --END--
 EOF
-diff por.hoa exp
+diff por2.hoa exp