From aa40482352aa48393b6bd93ce28dbf8df9075484 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 10 May 2017 15:59:58 +0200 Subject: [PATCH] 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 | 4 ++++ bin/ltl2tgba.cc | 6 +++++- bin/ltl2tgta.cc | 8 ++++++-- spot/tl/simplify.cc | 9 +++++++++ spot/tl/simplify.hh | 9 +++++++-- spot/twaalgos/stats.cc | 6 +++++- spot/twaalgos/translate.cc | 9 +++++++-- spot/twaalgos/translate.hh | 3 +++ tests/core/ltl2tgba.test | 18 +++++++++++++----- tests/core/readsave.test | 2 +- 10 files changed, 60 insertions(+), 14 deletions(-) diff --git a/NEWS b/NEWS index 232303d06..aa525ad61 100644 --- a/NEWS +++ b/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: diff --git a/bin/ltl2tgba.cc b/bin/ltl2tgba.cc index 41beae20d..44cd1dca4 100644 --- a/bin/ltl2tgba.cc +++ b/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; } }; diff --git a/bin/ltl2tgta.cc b/bin/ltl2tgta.cc index 469344e2b..3c61926c2 100644 --- a/bin/ltl2tgta.cc +++ b/bin/ltl2tgta.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement +// 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; } diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc index 3c03666fe..6732c36bc 100644 --- a/spot/tl/simplify.cc +++ b/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; + } } diff --git a/spot/tl/simplify.hh b/spot/tl/simplify.hh index c2f6a3c36..d06a3d5c7 100644 --- a/spot/tl/simplify.hh +++ b/spot/tl/simplify.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de -// Recherche et Developpement de l'Epita (LRDE). +// Copyright (C) 2011-2017 Laboratoire de Recherche et Developpement +// 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; diff --git a/spot/twaalgos/stats.cc b/spot/twaalgos/stats.cc index 5ff628e62..e521c7efe 100644 --- a/spot/twaalgos/stats.cc +++ b/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; } diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index 4ec085524..dc117490d 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2013-2017 Laboratoire de Recherche et Développement +// 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(); + } + } diff --git a/spot/twaalgos/translate.hh b/spot/twaalgos/translate.hh index 545474ba7..569c87218 100644 --- a/spot/twaalgos/translate.hh +++ b/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); diff --git a/tests/core/ltl2tgba.test b/tests/core/ltl2tgba.test index bdfbd0805..7b82b172c 100755 --- a/tests/core/ltl2tgba.test +++ b/tests/core/ltl2tgba.test @@ -1,10 +1,10 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 -# Laboratoire de Recherche et Développement de l'Epita (LRDE). -# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre -# et Marie Curie. +# Copyright (C) 2009-2017 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). +# Copyright (C) 2003-2004 Laboratoire d'Informatique de Paris 6 +# (LIP6), département Systèmes Répartis Coopératifs (SRC), Université +# 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 diff --git a/tests/core/readsave.test b/tests/core/readsave.test index 40cf0e634..0fd2efe60 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -122,7 +122,7 @@ cat >expected <, 5, 1 , 5, 1 , 4, 1 -, 4, 1 +, 4, 1 , 4, 1 , 6, 1 <(a & !b & (b | (!b M F!a))) | (!a & (b | (!b & (b W Ga)))), 3 states>, 5, 1