alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Speed up the obligation test.

Browse source 
* src/tgbaalgos/minimize.cc (minimize_obligation): Do not
minimize aut_neg_f, complement min_aut_f instead.
* src/tgbaalgos/minimize.hh: Adjust description.
This commit is contained in:
Alexandre Duret-Lutz 2011-01-05 14:15:15 +01:00
parent f06fc8ac77
commit ef317685c8
3 changed files with 22 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

8
ChangeLog
View file

@ -1,3 +1,11 @@
2011-01-05 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Speed up the obligation test.
* src/tgbaalgos/minimize.cc (minimize_obligation): Do not
minimize aut_neg_f, complement min_aut_f instead.
* src/tgbaalgos/minimize.hh: Adjust description.
2011-01-05 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2011-01-05 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/tgbaalgos/minimize.cc (minimize): Use the Loeding algorithm * src/tgbaalgos/minimize.cc (minimize): Use the Loeding algorithm

20
src/tgbaalgos/minimize.cc
View file

@ -271,7 +271,7 @@ namespace spot
tgba_explicit* minimize(const tgba* a, bool monitor) tgba_explicit_number* minimize(const tgba* a, bool monitor)
{ {
std::queue<hash_set*> todo; std::queue<hash_set*> todo;
// The list of equivalent states. // The list of equivalent states.
@ -496,7 +496,7 @@ namespace spot
const ltl::formula* f, const tgba* aut_neg_f) const ltl::formula* f, const tgba* aut_neg_f)
{ {
// WDBA minimization // WDBA minimization
tgba* min_aut_f = minimize(aut_f); tgba_explicit_number* min_aut_f = minimize(aut_f);
// If aut_f is a safety automaton, the WDBA minimization must be // If aut_f is a safety automaton, the WDBA minimization must be
// correct. // correct.
@ -545,20 +545,24 @@ namespace spot
{ {
delete ec; delete ec;
delete p; delete p;
tgba* min_aut_neg_f = minimize(aut_neg_f); // Complement the minimized WDBA.
tgba* p = new tgba_product(aut_f, min_aut_neg_f); min_aut_f->complement_all_acceptance_conditions();
tgba* p = new tgba_product(aut_f, min_aut_f);
emptiness_check* ec = couvreur99(p); emptiness_check* ec = couvreur99(p);
res = ec->check(); res = ec->check();
if (!res) if (!res)
// Finally, we are now sure that it was safe {
// to minimize the automaton. // Finally, we are now sure that it was safe
ok = true; // to minimize the automaton.
ok = true;
// Get the original automaton back.
min_aut_f->complement_all_acceptance_conditions();
}
delete res; delete res;
delete ec; delete ec;
delete p; delete p;
delete min_aut_neg_f;
} }
else else
{ {

4
src/tgbaalgos/minimize.hh
View file

@ -93,7 +93,7 @@ namespace spot
/// \endverbatim /// \endverbatim
/// (Note: although the above paper uses Spot, this function did not /// (Note: although the above paper uses Spot, this function did not
/// exist at that time.) /// exist at that time.)
tgba_explicit* minimize(const tgba* a, bool monitor = false); tgba_explicit_number* minimize(const tgba* a, bool monitor = false);
/// \brief Minimize an automaton if it represents an obligation property. /// \brief Minimize an automaton if it represents an obligation property.
@ -138,7 +138,7 @@ namespace spot
/// formula, then the result of \code minimize(aut) is returned. /// formula, then the result of \code minimize(aut) is returned.
/// Otherwise, if \a aut_neg_f was not supplied but \a f was, \a /// Otherwise, if \a aut_neg_f was not supplied but \a f was, \a
/// aut_neg_f is built from the negation of \a f. Then we check /// aut_neg_f is built from the negation of \a f. Then we check
/// that \code product(aut,minimize(aut_neg_f)) and \code /// that \code product(aut,!minimize(aut_f)) and \code
/// product(aut_neg_f,minize(aut)) are both empty. If they are, the /// product(aut_neg_f,minize(aut)) are both empty. If they are, the
/// the minimization was sound. (See the paper for full details.) /// the minimization was sound. (See the paper for full details.)
const tgba* minimize_obligation(const tgba* aut_f, const tgba* minimize_obligation(const tgba* aut_f,