From f6607f1a2c7695be9d59aa5ee5dabf60510afa2d Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 18 May 2017 16:46:11 +0200
Subject: [PATCH] bin: release all subformulas between runs

Fixes #262, reported by Maximilien Colange.

* bin/common_output.cc, bin/common_aoutput.cc, bin/common_aoutput.hh:
Clear the set of atomic propositions if --stats=%[...]x was used.
* spot/twa/bdddict.cc: Release any formula associated to a BDD when it
is unregistered, do not wait for the dictionary's destruction.  This
was the main culprit for #262.
* tests/core/ltl2tgba.test: Add test cases.
* NEWS: Mention the bug.
---
 NEWS                     |  6 +++++-
 bin/common_aoutput.cc    |  2 ++
 bin/common_aoutput.hh    |  6 +++++-
 bin/common_output.cc     |  8 +++++++-
 spot/twa/bdddict.cc      | 14 +++++---------
 tests/core/ltl2tgba.test | 17 +++++++++++++++++
 6 files changed, 41 insertions(+), 12 deletions(-)

diff --git a/NEWS b/NEWS
index 90cf66bb0..a939abeac 100644
--- a/NEWS
+++ b/NEWS
@@ -1,6 +1,10 @@
 New in spot 2.3.4.dev (not yet released)
 
-  Nothing yet.
+  Bugs fixed:
+
+  - We have fixed new cases where translating multiple formula in a
+    single ltl2tgba run could produce automata different from those
+    produced by individual runs.
 
 New in spot 2.3.4 (2017-05-11)
 
diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc
index 182caf2ba..18a9ef6fb 100644
--- a/bin/common_aoutput.cc
+++ b/bin/common_aoutput.cc
@@ -513,6 +513,8 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut,
   output_aut_ = nullptr;
   input_aut_ = nullptr;
   haut_scc_.reset();
+  aut_ap_.clear();
+  haut_ap_.clear();
   return res;
 }
 
diff --git a/bin/common_aoutput.hh b/bin/common_aoutput.hh
index 83a774438..678b65bea 100644
--- a/bin/common_aoutput.hh
+++ b/bin/common_aoutput.hh
@@ -121,11 +121,15 @@ protected:
               });
   }
 public:
+  void clear()
+  {
+    val_.clear();
+  }
 
   template<class T>
   void set(T begin, T end)
   {
-    val_.clear();
+    clear();
     val_.insert(val_.end(), begin, end);
     sort();
   }
diff --git a/bin/common_output.cc b/bin/common_output.cc
index abe85a819..674d19d20 100644
--- a/bin/common_output.cc
+++ b/bin/common_output.cc
@@ -239,7 +239,13 @@ namespace
         size_ = spot::length(f);
       if (has('h'))
         class_ = spot::mp_class(f);
-      return format(format_);
+      auto& res = format(format_);
+      // Make sure we do not store the formula until the next one is
+      // printed, as the order in which APs are registered may
+      // influence the automata output.
+      fl_ = nullptr;
+      ap_.clear();
+      return res;
     }
 
   private:
diff --git a/spot/twa/bdddict.cc b/spot/twa/bdddict.cc
index 07b8280c3..ef601ad70 100644
--- a/spot/twa/bdddict.cc
+++ b/spot/twa/bdddict.cc
@@ -235,7 +235,6 @@ namespace spot
     // ME was the last user of this variable.
     // Let's free it.  First, we need to find
     // if this is a Var or an Acc variable.
-    int n = 1;
     formula f = nullptr;
     switch (bdd_map[v].type)
       {
@@ -249,21 +248,19 @@ namespace spot
         break;
       case anon:
         {
-          bdd_dict_priv::free_anonymous_list_of_type::iterator i;
           // Nobody use this variable as an anonymous variable
           // anymore, so remove it entirely from the anonymous
           // free list so it can be used for something else.
-          for (i = priv_->free_anonymous_list_of.begin();
-               i != priv_->free_anonymous_list_of.end(); ++i)
-            i->second.remove(v, n);
+          for (auto& fal: priv_->free_anonymous_list_of)
+            fal.second.remove(v, 1);
           break;
         }
       }
     // Actually release the associated BDD variables, and the
     // formula itself.
-    priv_->release_variables(v, n);
-    while (n--)
-      bdd_map[v + n].type = anon;
+    priv_->release_variables(v, 1);
+    bdd_map[v].type = anon;
+    bdd_map[v].f = nullptr;
   }
 
   void
@@ -326,7 +323,6 @@ namespace spot
   bdd_dict::assert_emptiness() const
   {
     bool fail = false;
-
     bool var_seen = false;
     bool acc_seen = false;
     bool refs_seen = false;
diff --git a/tests/core/ltl2tgba.test b/tests/core/ltl2tgba.test
index 7b82b172c..a1c08208d 100755
--- a/tests/core/ltl2tgba.test
+++ b/tests/core/ltl2tgba.test
@@ -238,3 +238,20 @@ genltl --go-theta=18 | ltl2tgba --low --any -q
 (ltl2tgba Fb ; ltl2tgba 'GFa & GFb') >out1
 ltl2tgba Fb 'GFa & GFb' >out2
 diff out1 out2
+
+# Because atomic proposition were not released by bdd_dict, different
+# order of transitions could be observed in automata output after a
+# previous translation by the same process.  (issue #262).
+ltl2tgba --low --any 'Xp1 xor (Fp1 M (!p1 M (Fp0 W p1)))' \
+         'Fp0 -> XXG(1 U Gp1)' > res1
+ltl2tgba --low --any 'Xp1 xor (Fp1 M (!p1 M (Fp0 W p1)))' >res2
+ltl2tgba --low --any 'Fp0 -> XXG(1 U Gp1)' >>res2
+diff res1 res2
+
+# The same should work when printing SCCs or atomic propositions
+s='--stats=%c,%[,]x'
+ltl2tgba --low --any 'Xp1 xor (Fp1 M (!p1 M (Fp0 W p1)))' \
+         'Fp0 -> XXG(1 U Gp1)' "$s" >res1
+ltl2tgba --low --any 'Xp1 xor (Fp1 M (!p1 M (Fp0 W p1)))' "$s" >res2
+ltl2tgba --low --any 'Fp0 -> XXG(1 U Gp1)' "$s" >>res2
+diff res1 res2