* src/ltlvisit/clone.cc (clone): New const version.

* src/ltlvisit/clone.hh (clone): Likewise.
* src/ltlvisit/destroy.cc (destroy): New const version.
* src/ltlvisit/destroy.hh (destroy): Likewise.
* src/tgba/tgbabddconcretefactory.cc
(tgba_bdd_concrete_factory::create_state,
tgba_bdd_concrete_factory::create_atomic_prop,
tgba_bdd_concrete_factory::promise): Clone new formulae.
* src/tgba/tgbabdddict.cc (tgba_bdd_dict::tgba_bdd_dict,
tgba_bdd_dict::~tgba_bdd_dict, tgba_bdd_dict::operator=): New methods
that clone and destroy formulae.
* src/tgbatest/ltl2tgba.test, src/tgbatest/ltl2tgba.cc: New files.
* src/tgbatest/Makefile.am (check_PROGRAMS): Add ltl2tgba.
(ltl2tgba_SOURCES): New variable.
(TESTS): Add ltl2tgba.test.

ChangeLog

@@ -1,5 +1,21 @@
 2003-06-06  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
+	* src/ltlvisit/clone.cc (clone): New const version.
+	* src/ltlvisit/clone.hh (clone): Likewise.
+	* src/ltlvisit/destroy.cc (destroy): New const version.
+	* src/ltlvisit/destroy.hh (destroy): Likewise.
+	* src/tgba/tgbabddconcretefactory.cc
+	(tgba_bdd_concrete_factory::create_state,
+	tgba_bdd_concrete_factory::create_atomic_prop,
+	tgba_bdd_concrete_factory::promise): Clone new formulae.
+	* src/tgba/tgbabdddict.cc (tgba_bdd_dict::tgba_bdd_dict,
+	tgba_bdd_dict::~tgba_bdd_dict, tgba_bdd_dict::operator=): New methods
+	that clone and destroy formulae.
+	* src/tgbatest/ltl2tgba.test, src/tgbatest/ltl2tgba.cc: New files.
+	* src/tgbatest/Makefile.am (check_PROGRAMS): Add ltl2tgba.
+	(ltl2tgba_SOURCES): New variable.
+	(TESTS): Add ltl2tgba.test.
+
 	* src/ltltest/equals.cc, src/ltltest/readltl.cc,
 	src/tgba/bddprint.cc, src/ltltest/tostring.cc: Include <cassert>.
 

src/ltlvisit/clone.cc

@@ -70,5 +70,10 @@ namespace spot
       return v.result();
     }
 
+    formula*
+    clone(const formula* f)
+    {
+      return clone(const_cast<formula*>(f));
+    }
   }
 }

src/ltlvisit/clone.hh

@@ -36,6 +36,8 @@ namespace spot
 
     /// \brief Clone a formula.
     formula* clone(formula* f);
+    /// \brief Clone a formula.
+    formula* clone(const formula* f);
   }
 }
 

src/ltlvisit/destroy.cc

@@ -21,5 +21,11 @@ namespace spot
       destroy_visitor v;
       f->accept(v);
     }
+
+    void
+    destroy(const formula* f)
+    {
+      destroy(const_cast<formula*>(f));
+    }
   }
 }

src/ltlvisit/destroy.hh

@@ -9,6 +9,8 @@ namespace spot
   {
     /// \brief Destroys a formula
     void destroy(formula *f);
+    /// \brief Destroys a formula
+    void destroy(const formula *f);
   }
 }
 

src/tgba/tgbabddconcretefactory.cc

@@ -1,3 +1,4 @@
+#include "ltlvisit/clone.hh"
 #include "tgbabddconcretefactory.hh"
 
 namespace spot
@@ -14,8 +15,9 @@ namespace spot
     if (sii != dict_.now_map.end())
       return sii->second;
 
-    int num = create_pair();
+    f = clone(f);
 
+    int num = create_pair();
     dict_.now_map[f] = num;
     dict_.now_formula_map[num] = f;
 
@@ -37,6 +39,8 @@ namespace spot
     if (sii != dict_.var_map.end())
       return sii->second;
 
+    f = clone(f);
+
     int num = create_node();
     dict_.var_map[f] = num;
     dict_.var_formula_map[num] = f;
@@ -55,6 +59,8 @@ namespace spot
     if (sii != dict_.prom_map.end())
       return sii->second;
 
+    f = clone(f);
+
     int num = create_node();
     dict_.prom_map[f] = num;
     dict_.prom_formula_map[num] = f;

src/tgba/tgbabdddict.cc

@@ -1,5 +1,7 @@
 #include "tgbabdddict.hh"
 #include "ltlvisit/tostring.hh"
+#include "ltlvisit/clone.hh"
+#include "ltlvisit/destroy.hh"
 
 namespace spot
 {
@@ -55,4 +57,47 @@ namespace spot
     return true;
   }
 
+  tgba_bdd_dict::tgba_bdd_dict()
+  {
+  }
+
+  tgba_bdd_dict::tgba_bdd_dict(const tgba_bdd_dict& other)
+    : now_map(other.now_map),
+      now_formula_map(other.now_formula_map),
+      var_map(other.var_map),
+      var_formula_map(other.var_formula_map),
+      prom_map(other.prom_map),
+      prom_formula_map(other.prom_formula_map)
+  {
+    fv_map::iterator i;
+    for (i = now_map.begin(); i != now_map.end(); ++i)
+      ltl::clone(i->first);
+    for (i = var_map.begin(); i != var_map.end(); ++i)
+      ltl::clone(i->first);
+    for (i = prom_map.begin(); i != prom_map.end(); ++i)
+      ltl::clone(i->first);
+  }
+
+  tgba_bdd_dict&
+  tgba_bdd_dict::operator=(const tgba_bdd_dict& other)
+  {
+    if (this != &other)
+      {
+	this->~tgba_bdd_dict();
+	new (this) tgba_bdd_dict(other);
+      }
+    return *this;
+  }
+
+  tgba_bdd_dict::~tgba_bdd_dict()
+  {
+    fv_map::iterator i;
+    for (i = now_map.begin(); i != now_map.end(); ++i)
+      ltl::destroy(i->first);
+    for (i = var_map.begin(); i != var_map.end(); ++i)
+      ltl::destroy(i->first);
+    for (i = prom_map.begin(); i != prom_map.end(); ++i)
+      ltl::destroy(i->first);
+  }
+
 }

src/tgba/tgbabdddict.hh

@@ -29,6 +29,11 @@ namespace spot
 
     /// Whether this dictionary contains \a other.
     bool contains(const tgba_bdd_dict& other) const;
+
+    tgba_bdd_dict();
+    tgba_bdd_dict(const tgba_bdd_dict& other);
+    tgba_bdd_dict& operator=(const tgba_bdd_dict& other);
+    ~tgba_bdd_dict();
   };
 }
 

src/tgbatest/.cvsignore

@@ -6,3 +6,4 @@ explicit
 .libs
 tgbaread
 readsave
+ltl2tgba

src/tgbatest/Makefile.am

@@ -6,17 +6,19 @@ check_SCRIPTS = defs
 check_PROGRAMS = \
   explicit \
   readsave \
-  tgbaread
+  tgbaread \
-
+  ltl2tgba
 
 explicit_SOURCES = explicit.cc
+ltl2tgba_SOURCES = ltl2tgba.cc
 readsave_SOURCES = readsave.cc
 tgbaread_SOURCES = tgbaread.cc
 
 TESTS = \
   explicit.test \
   tgbaread.test \
-  readsave.test
+  readsave.test \
+  ltl2tgba.test
 
 EXTRA_DIST = $(TESTS)
 

src/tgbatest/ltl2tgba.cc

@@ -0,0 +1,59 @@
+#include <iostream>
+#include <cassert>
+#include "ltlvisit/destroy.hh"
+#include "ltlast/allnodes.hh"
+#include "ltlparse/public.hh"
+#include "tgba/ltl2tgba.hh"
+#include "tgbaalgos/dotty.hh"
+
+void
+syntax(char* prog)
+{
+  std::cerr << prog << " [-d] formula" << std::endl;
+  exit(2);
+}
+
+int
+main(int argc, char** argv)
+{
+  int exit_code = 0;
+
+  if (argc < 2)
+    syntax(argv[0]);
+
+  bool debug = false;
+  int formula_index = 1;
+
+  if (!strcmp(argv[1], "-d"))
+    {
+      debug = true;
+      if (argc < 3)
+	syntax(argv[0]);
+      formula_index = 2;
+    }
+
+  spot::ltl::environment& env(spot::ltl::default_environment::instance());
+  spot::ltl::parse_error_list pel;
+  spot::ltl::formula* f = spot::ltl::parse(argv[formula_index],
+					   pel, env, debug);
+
+  exit_code =
+    spot::ltl::format_parse_errors(std::cerr, argv[formula_index], pel);
+
+  if (f)
+    {
+      spot::tgba_bdd_concrete a = spot::ltl_to_tgba(f);
+      spot::ltl::destroy(f);
+      spot::dotty_reachable(std::cout, a);
+    }
+  else
+    {
+      exit_code = 1;
+    }
+
+  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/ltl2tgba.test

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