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.
This commit is contained in:
Alexandre Duret-Lutz
parent
8e19d3f47e
commit
f07fbbae79
10 changed files with 60 additions and 14 deletions
4
NEWS
4
NEWS
|
|
@ -100,6 +100,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.
|
||||
|
||||
Backward-incompatible changes:
|
||||
|
||||
- spot::acc_cond::mark_t::operator bool() has been marked as
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
};
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue