* 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/Makefile.am (check_PROGRAMS): Add ltlprod.
(ltlprod_SOURCES): New variable.
(TESTS): Add ltlprod.test.

ChangeLog

 2003-06-06  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
+	* 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/Makefile.am (check_PROGRAMS): Add ltlprod.
+	(ltlprod_SOURCES): New variable.
+	(TESTS): Add ltlprod.test.
+
 	* src/ltlvisit/clone.cc (clone): New const version.
 	* src/ltlvisit/clone.hh (clone): Likewise.
 	* src/ltlvisit/destroy.cc (destroy): New const version.

src/tgba/dictunion.cc

 #include <set>
 #include "dictunion.hh"
+#include "ltlvisit/clone.hh"
 #include <bdd.h>
 #include <cassert>
 
@@ -9,8 +10,6 @@ namespace spot
   tgba_bdd_dict
   tgba_bdd_dict_union(const tgba_bdd_dict& l, const tgba_bdd_dict& r)
   {
-    tgba_bdd_dict res;
-
     std::set<const ltl::formula*> now;
     std::set<const ltl::formula*> var;
     std::set<const ltl::formula*> prom;
@@ -49,21 +48,26 @@ namespace spot
     // Next BDD variable to use.
     int v = 0;
 
+    tgba_bdd_dict res;
+
     std::set<const ltl::formula*>::const_iterator f;
     for (f = prom.begin(); f != prom.end(); ++f)
       {
+	clone(*f);
 	res.prom_map[*f] = v;
 	res.prom_formula_map[v] = *f;
 	++v;
       }
     for (f = var.begin(); f != var.end(); ++f)
       {
+	clone(*f);
 	res.var_map[*f] = v;
 	res.var_formula_map[v] = *f;
 	++v;
       }
     for (f = now.begin(); f != now.end(); ++f)
       {
+	clone(*f);
 	res.now_map[*f] = v;
 	res.now_formula_map[v] = *f;
 	v += 2;

src/tgbatest/.cvsignore

@@ -7,3 +7,4 @@ explicit
 tgbaread
 readsave
 ltl2tgba
+ltlprod

src/tgbatest/Makefile.am

@@ -7,10 +7,12 @@ check_PROGRAMS = \
   explicit \
   readsave \
   tgbaread \
-  ltl2tgba
+  ltl2tgba \
+  ltlprod
 
 explicit_SOURCES = explicit.cc
 ltl2tgba_SOURCES = ltl2tgba.cc
+ltlprod_SOURCES = ltlprod.cc
 readsave_SOURCES = readsave.cc
 tgbaread_SOURCES = tgbaread.cc
 
@@ -18,8 +20,9 @@ TESTS = \
   explicit.test \
   tgbaread.test \
   readsave.test \
-  ltl2tgba.test
+  ltl2tgba.test \
+  ltlprod.test
 
 EXTRA_DIST = $(TESTS)
 
-CLEANFILES = inpu stdout expected
+CLEANFILES = input stdout expected

src/tgbatest/ltlprod.cc

+#include <iostream>
+#include <cassert>
+#include "ltlvisit/destroy.hh"
+#include "ltlast/allnodes.hh"
+#include "ltlparse/public.hh"
+#include "tgba/ltl2tgba.hh"
+#include "tgba/tgbabddprod.hh"
+#include "tgbaalgos/dotty.hh"
+
+void
+syntax(char* prog)
+{
+  std::cerr << prog << " formula1 formula2" << std::endl;
+  exit(2);
+}
+
+int
+main(int argc, char** argv)
+{
+  int exit_code = 0;
+
+  if (argc != 3)
+    syntax(argv[0]);
+
+  spot::ltl::environment& env(spot::ltl::default_environment::instance());
+
+  spot::ltl::parse_error_list pel1;
+  spot::ltl::formula* f1 = spot::ltl::parse(argv[1], pel1, env);
+
+  if (spot::ltl::format_parse_errors(std::cerr, argv[1], pel1))
+    return 2;
+
+  spot::ltl::parse_error_list pel2;
+  spot::ltl::formula* f2 = spot::ltl::parse(argv[2], pel2, env);
+
+  if (spot::ltl::format_parse_errors(std::cerr, argv[2], pel2))
+    return 2;
+
+  {
+    spot::tgba_bdd_concrete a1 = spot::ltl_to_tgba(f1);
+    spot::tgba_bdd_concrete a2 = spot::ltl_to_tgba(f2);
+    spot::ltl::destroy(f1);
+    spot::ltl::destroy(f2);
+
+    spot::tgba_bdd_product p(a1, a2);
+
+    spot::dotty_reachable(std::cout, p);
+  }
+
+  assert(spot::ltl::atomic_prop::instance_count() == 0);
+  assert(spot::ltl::unop::instance_count() == 0);
+  assert(spot::ltl::binop::instance_count() == 0);
+  assert(spot::ltl::multop::instance_count() == 0);
+  return exit_code;
+}

src/tgbatest/ltlprod.test

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