product: raise an exception if the dict are different

Fixes #132.

* python/spot.py (translate): Allow changing the dictionary.
* tests/python/prodexpt.py: New file.
* tests/Makefile.am: Add it.
* spot/twa/twaproduct.cc, spot/twaalgos/product.cc: Add them.
* NEWS: Mention the change.

NEWS

@@ -1,5 +1,10 @@
 New in spot 1.99.7a (not yet released)
 
+  Library:
+
+  * Building products with different dictionaries now raise an
+    exception instead of using an assertion that could be disabled.
+
   Documentation:
 
   * There is a new page giving informal illustrations (and extra

python/spot.py

@@ -574,7 +574,7 @@ def _postproc_translate_options(obj, default_type, *args):
     obj.set_level(optm_)
 
 
-def translate(formula, *args):
+def translate(formula, *args, dict=_bdd_dict):
     """Translate a formula into an automaton.
 
     Keep in mind that 'Deterministic' expresses just a preference that
@@ -592,7 +592,7 @@ def translate(formula, *args):
 
     The default corresponds to 'tgba', 'small' and 'high'.
     """
-    a = translator(_bdd_dict)
+    a = translator(dict)
     _postproc_translate_options(a, postprocessor.TGBA, *args)
     if type(formula) == str:
         formula = parse_formula(formula)

spot/twa/twaproduct.cc

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2011, 2012, 2014, 2015 Laboratoire de Recherche et
+// Copyright (C) 2009, 2011, 2012, 2014, 2015, 2016 Laboratoire de
-// Développement de l'Epita (LRDE).
+// Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 // Université Pierre et Marie Curie.
@@ -283,6 +283,9 @@ namespace spot
     : twa(left->get_dict()), left_(left), right_(right),
       pool_(sizeof(state_product))
   {
+    if (left->get_dict() != right->get_dict())
+      throw std::runtime_error("twa_product: left and right automata should "
+			       "share their bdd_dict");
     assert(get_dict() == right_->get_dict());
 
     // If one of the side is a Kripke structure, it is easier to deal

spot/twaalgos/product.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015 Laboratoire de Recherche et
+// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -49,7 +49,9 @@ namespace spot
       std::unordered_map<product_state, unsigned, product_state_hash> s2n;
       std::deque<std::pair<product_state, unsigned>> todo;
 
-      assert(left->get_dict() == right->get_dict());
+      if (left->get_dict() != right->get_dict())
+	throw std::runtime_error("product: left and right automata should "
+				 "share their bdd_dict");
       auto res = make_twa_graph(left->get_dict());
       res->copy_ap_of(left);
       res->copy_ap_of(right);

tests/Makefile.am

@@ -302,6 +302,7 @@ TESTS_python = \
   python/optionmap.py \
   python/parsetgba.py \
   python/piperead.ipynb \
+  python/prodexpt.py \
   python/product.ipynb \
   python/randaut.ipynb \
   python/randgen.py \

tests/python/prodexpt.py

@@ -0,0 +1,38 @@
+# -*- mode: python; coding: utf-8 -*-
+# Copyright (C) 2016  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 <http://www.gnu.org/licenses/>.
+
+import spot
+
+# make sure that we are not allowed to build the product of two automata with
+# different dictionnaries.
+
+aut1 = spot.translate('Xa')
+aut2 = spot.translate('Xb', dict=spot.make_bdd_dict())
+
+try:
+    spot.product(aut1, aut2)
+    exit(2)
+except RuntimeError:
+    pass
+
+try:
+    spot.otf_product(aut1, aut2)
+    exit(2)
+except RuntimeError:
+    pass