* src/tgbatest/bddprod.test: New file.

* src/tgbatest/Makefile.am (check_PROGRAMS): Add bddprod.
(bddprod_SOURCES, bddprod_CXXFLAGS): New variables.
(TESTS): Add bddprod.test.
* src/tgbatest/ltlprod.c: Handle BDD_CONCRETE_PRODUCT.

ChangeLog

 2003-06-06  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
+	* src/tgbatest/bddprod.test: New file.
+	* src/tgbatest/Makefile.am (check_PROGRAMS): Add bddprod.
+	(bddprod_SOURCES, bddprod_CXXFLAGS): New variables.
+	(TESTS): Add bddprod.test.
+	* src/tgbatest/ltlprod.c: Handle BDD_CONCRETE_PRODUCT.
+
 	* src/tgba/dictunion.cc (tgba_bdd_dict_union): Clone formulae
 	while building new dictionary.
 	* src/tgbatest/ltlprod.test, src/tgbatest/ltlprod.cc: New files.

src/tgbatest/.cvsignore

@@ -8,3 +8,4 @@ tgbaread
 readsave
 ltl2tgba
 ltlprod
+bddprod

src/tgbatest/Makefile.am

@@ -8,8 +8,11 @@ check_PROGRAMS = \
   readsave \
   tgbaread \
   ltl2tgba \
-  ltlprod
+  ltlprod \
+  bddprod
 
+bddprod_SOURCES = ltlprod.cc
+bddprod_CXXFLAGS = -DBDD_CONCRETE_PRODUCT
 explicit_SOURCES = explicit.cc
 ltl2tgba_SOURCES = ltl2tgba.cc
 ltlprod_SOURCES = ltlprod.cc
@@ -21,7 +24,8 @@ TESTS = \
   tgbaread.test \
   readsave.test \
   ltl2tgba.test \
-  ltlprod.test
+  ltlprod.test \
+  bddprod.test
 
 EXTRA_DIST = $(TESTS)
 

src/tgbatest/bddprod.test

+#!/bin/sh
+
+. ./defs
+
+set -e
+
+# We don't check the output, but just running these might be enough to
+# trigger assertions.
+
+./bddprod a b
+./bddprod a a
+./bddprod 'a U b' 'X f'
+./bddprod 'X a' 'X a'
+./bddprod 'X a' 'a U b'
+./bddprod 'a & b & c' 'b & d & c'
+./bddprod 'a | b | (c U (d & (g U (h ^ i))))' 'h ^ i'
+./bddprod 'Xa & (b U !a) & (b U !a)' '(b U !a) & f'

src/tgbatest/ltlprod.cc

@@ -5,6 +5,7 @@
 #include "ltlparse/public.hh"
 #include "tgba/ltl2tgba.hh"
 #include "tgba/tgbabddprod.hh"
+#include "tgba/tgbabddconcreteproduct.hh"
 #include "tgbaalgos/dotty.hh"
 
 void
@@ -42,7 +43,11 @@ main(int argc, char** argv)
     spot::ltl::destroy(f1);
     spot::ltl::destroy(f2);
 
+#ifdef BDD_CONCRETE_PRODUCT
+    spot::tgba_bdd_concrete p = spot::product(a1, a2);
+#else
     spot::tgba_bdd_product p(a1, a2);
+#endif
 
     spot::dotty_reachable(std::cout, p);
   }