From 0233f31ee0a04fc64891200f4fdcc54d7e0dbe2b Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 6 Jun 2003 13:53:01 +0000
Subject: [PATCH] * 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                 |  6 ++++++
 src/tgbatest/.cvsignore   |  1 +
 src/tgbatest/Makefile.am  |  8 ++++++--
 src/tgbatest/bddprod.test | 17 +++++++++++++++++
 src/tgbatest/ltlprod.cc   |  5 +++++
 5 files changed, 35 insertions(+), 2 deletions(-)
 create mode 100755 src/tgbatest/bddprod.test

diff --git a/ChangeLog b/ChangeLog
index 0b1d948c2..75525411a 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,11 @@
 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.
diff --git a/src/tgbatest/.cvsignore b/src/tgbatest/.cvsignore
index b163d6a29..33733f242 100644
--- a/src/tgbatest/.cvsignore
+++ b/src/tgbatest/.cvsignore
@@ -8,3 +8,4 @@ tgbaread
 readsave
 ltl2tgba
 ltlprod
+bddprod
diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am
index dce28b477..28140d1b0 100644
--- a/src/tgbatest/Makefile.am
+++ b/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)
 
diff --git a/src/tgbatest/bddprod.test b/src/tgbatest/bddprod.test
new file mode 100755
index 000000000..61604fc6e
--- /dev/null
+++ b/src/tgbatest/bddprod.test
@@ -0,0 +1,17 @@
+#!/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'
diff --git a/src/tgbatest/ltlprod.cc b/src/tgbatest/ltlprod.cc
index 4897e0ff6..c68075215 100644
--- a/src/tgbatest/ltlprod.cc
+++ b/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);
   }