ltl2tgba: clear simplification cache between translations

The cache used in formula simplification will keep atomic propositions
defined between several translations, and may impact variable order.
Reported by Maximilien Colange.

* spot/tl/simplify.hh, spot/tl/simplify.cc,
spot/twaalgos/translate.cc, spot/twaalgos/translate.hh (clear_cache):
New method.
* bin/ltl2tgba.cc, bin/ltl2tgta.cc: Call it.
* spot/twaalgos/stats.cc: Do not keep a point to the formula after
printing statistics.
* tests/core/ltl2tgba.test: Add a test case.
* tests/core/readsave.test: Adjust one formula.
* NEWS: Mention the issue.

NEWS

@@ -15,6 +15,10 @@ New in spot 2.3.3.dev (not yet released)
     when q is a subformula that is both eventual and universal
     was documented but not applied in some forgotten cases.
 
+  - Because of some caching inside of ltl2tgba, translating multiple
+    formula in single ltl2tgba run could produce automata different
+    from those produced by individual runs.
+
 New in spot 2.3.3 (2017-04-11)
 
   Tools:

bin/ltl2tgba.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
+// Copyright (C) 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche
 // et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -146,6 +146,10 @@ namespace
 
       printer.print(aut, timer, f, filename, linenum, nullptr,
                     prefix, suffix);
+      // If we keep simplification caches around, atomic propositions
+      // will still be defined, and one translation may influence the
+      // variable order of the next one.
+      trans.clear_caches();
       return 0;
     }
   };

bin/ltl2tgta.cc

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
+// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement
-// et Développement de l'Epita (LRDE).
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -211,6 +211,10 @@ namespace
             tgta = spot::minimize_tgta(tgta);
           spot::print_dot(std::cout, tgta->get_ta());
         }
+      // If we keep simplification caches around, atomic propositions
+      // will still be defined, and one translation may influence the
+      // variable order of the next one.
+      trans.clear_caches();
       flush_cout();
       return 0;
     }

spot/tl/simplify.cc

@@ -3481,4 +3481,13 @@ namespace spot
     cache_->clear_as_bdd_cache();
     cache_->lcc.clear();
   }
+
+  void
+  tl_simplifier::clear_caches()
+  {
+    tl_simplifier_cache* c =
+      new tl_simplifier_cache(get_dict(), cache_->options);
+    std::swap(c, cache_);
+    delete c;
+  }
 }

spot/tl/simplify.hh

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
+// Copyright (C) 2011-2017 Laboratoire de Recherche et Developpement
-// Recherche et Developpement de l'Epita (LRDE).
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -176,6 +176,11 @@ namespace spot
     /// This also clears the language containment cache.
     void clear_as_bdd_cache();
 
+    /// \brief Clear all caches.
+    ///
+    /// This empties all the cache used by the simplifier.
+    void clear_caches();
+
     /// Return the bdd_dict used.
     bdd_dict_ptr get_dict() const;
 

spot/twaalgos/stats.cc

@@ -385,7 +385,11 @@ namespace spot
       }
 
     auto& os = format(format_);
-    scc_.reset(); // Make sure we do not hold a pointer to the automaton
+    // Make sure we do not hold a pointer to the automaton or the
+    // formula, as these may prevent atomic proposition to be freed
+    // before a next job.
+    scc_.reset();
+    form_ = nullptr;
     return os;
   }
 

spot/twaalgos/translate.cc

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
+// Copyright (C) 2013-2017 Laboratoire de Recherche et Développement
-// Développement de l'Epita (LRDE).
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -106,4 +106,9 @@ namespace spot
     return run(&f);
   }
 
+  void translator::clear_caches()
+  {
+    simpl_->clear_caches();
+  }
+
 }

spot/twaalgos/translate.hh

@@ -132,6 +132,9 @@ namespace spot
     /// by the simplified version.
     twa_graph_ptr run(formula* f);
 
+    /// \brief Clear the LTL simplification caches.
+    void clear_caches();
+
   protected:
     void setup_opt(const option_map* opt);
     void build_simplifier(const bdd_dict_ptr& dict);

tests/core/ltl2tgba.test

@@ -1,10 +1,10 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016
+# Copyright (C) 2009-2017 Laboratoire de Recherche et Développement de
-# Laboratoire de Recherche et Développement de l'Epita (LRDE).
+# l'Epita (LRDE).
-# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003-2004 Laboratoire d'Informatique de Paris 6
-# département Systèmes Répartis Coopératifs (SRC), Université Pierre
+# (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
-# et Marie Curie.
+# Pierre et Marie Curie.
 #
 # This file is part of Spot, a model checking library.
 #
@@ -230,3 +230,11 @@ ltl2tgba -f a -s | autfilt -q --ap=1 --lbtt | autfilt -q --ap=1
 # of the test-suite where this resize is triggered, so do not remove
 # it unless you can find another place that triggers that.
 genltl --go-theta=18 | ltl2tgba --low --any -q
+
+# Calling ltl2tgba once for two formulas should give the same result
+# as calling twice on each formula.  We had a problem where the order
+# of atomic propositions would be sensible to the formulas seen
+# before.
+(ltl2tgba Fb ; ltl2tgba 'GFa & GFb') >out1
+ltl2tgba Fb 'GFa & GFb' >out2
+diff out1 out2

tests/core/readsave.test

@@ -122,7 +122,7 @@ cat >expected <<EOF
 <F(b | Ga), 3 states>, 5, 1
 <F(!b & G(!b | G!a)), 3 states>, 5, 1
 <XF!b, 3 states>, 4, 1
-<Gb | G!b, 3 states>, 4, 1
+<G!b | Gb, 3 states>, 4, 1
 <XFb, 3 states>, 4, 1
 <F(b W a), 3 states>, 6, 1
 <(a & !b & (b | (!b M F!a))) | (!a & (b | (!b & (b W Ga)))), 3 states>, 5, 1