Commit 907d173d authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Move the logic for detecting when the minimize() algorithm is

correct from ltl2tgba to the library.

* src/tgbaalgos/minimize.hh,
src/tgbaalgos/minimize.cc (minimize_obligation): New function.
* src/tgbatests/ltl2tgba.cc (main): Fix constness of automata,
and call minimize_obligation() for -R3b.
parent 241ba112
2011-01-04 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Move the logic for detecting when the minimize() algorithm is
correct from ltl2tgba to the library.
* src/tgbaalgos/minimize.hh,
src/tgbaalgos/minimize.cc (minimize_obligation): New function.
* src/tgbatests/ltl2tgba.cc (main): Fix constness of automata,
and call minimize_obligation() for -R3b.
2010-12-26 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2010-12-26 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Make minimization of obligation properties and deterministic Make minimization of obligation properties and deterministic
......
// Copyright (C) 2010 Laboratoire de Recherche et Développement // Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -22,7 +22,13 @@ ...@@ -22,7 +22,13 @@
#include "minimize.hh" #include "minimize.hh"
#include "ltlast/allnodes.hh" #include "ltlast/allnodes.hh"
#include "misc/hash.hh" #include "misc/hash.hh"
#include "tgba/tgbaproduct.hh"
#include "tgba/tgbatba.hh"
#include "tgbaalgos/powerset.hh" #include "tgbaalgos/powerset.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/safety.hh"
#include "tgbaalgos/sccfilter.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
namespace spot namespace spot
{ {
...@@ -300,4 +306,87 @@ namespace spot ...@@ -300,4 +306,87 @@ namespace spot
return res; return res;
} }
const tgba*
minimize_obligation(const tgba* aut_f,
const ltl::formula* f, const tgba* aut_neg_f)
{
// WDBA minimization
tgba* min_aut_f = minimize(aut_f);
// If aut_f is a safety automaton, the WDBA minimization must be
// correct.
if (is_safety_automaton(aut_f))
{
return min_aut_f;
}
if (!f && !aut_neg_f)
{
// We do not now if the minimization is safe.
return 0;
}
const tgba* to_free = 0;
// Build negation automaton if not supplied.
if (!aut_neg_f)
{
assert(f);
ltl::formula* neg_f = ltl::unop::instance(ltl::unop::Not, f->clone());
aut_neg_f = ltl_to_tgba_fm(neg_f, aut_f->get_dict());
neg_f->destroy();
// Remove useless SCCs.
const tgba* tmp = scc_filter(aut_neg_f, true);
delete aut_neg_f;
to_free = aut_neg_f = tmp;
}
// If the negation is a safety automaton, then the
// minimization is correct.
if (is_safety_automaton(aut_neg_f))
{
delete to_free;
return min_aut_f;
}
bool ok = false;
tgba* p = new tgba_product(min_aut_f, aut_neg_f);
emptiness_check* ec = couvreur99(p);
emptiness_check_result* res = ec->check();
if (!res)
{
delete ec;
delete p;
tgba* min_aut_neg_f = minimize(aut_neg_f);
tgba* p = new tgba_product(aut_f, min_aut_neg_f);
emptiness_check* ec = couvreur99(p);
res = ec->check();
if (!res)
// Finally, we are now sure that it was safe
// to minimize the automaton.
ok = true;
delete res;
delete ec;
delete p;
delete min_aut_neg_f;
}
else
{
delete res;
delete ec;
delete p;
}
delete to_free;
if (ok)
return min_aut_f;
delete min_aut_f;
return aut_f;
}
} }
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -22,77 +22,129 @@ ...@@ -22,77 +22,129 @@
# define SPOT_TGBAALGOS_MINIMIZE_HH # define SPOT_TGBAALGOS_MINIMIZE_HH
# include "tgba/tgbaexplicit.hh" # include "tgba/tgbaexplicit.hh"
# include "ltlast/formula.hh"
namespace spot namespace spot
{ {
// \brief Use the powerset construction to minimize a TGBA. /// \brief Use the powerset construction to minimize a TGBA.
// ///
// If \a monitor is set of \c false (the default), then the /// If \a monitor is set to \c false (the default), then the
// minimized automaton is correct only for properties that belong to /// minimized automaton is correct only for properties that belong
// the class of "obligation properties". This algorithm assumes /// to the class of "obligation properties". This algorithm assumes
// that the given automaton expresses an obligation properties and /// that the given automaton expresses an obligation properties and
// will return an automaton that is bogus (i.e. not equivalent to /// will return an automaton that is bogus (i.e. not equivalent to
// the original) if that is not the case. /// the original) if that is not the case.
// ///
// Please see the following paper for a discussion of this /// Please see the following paper for a discussion of this
// technique. /// technique.
// ///
// \verbatim /// \verbatim
// @InProceedings{ dax.07.atva, /// @InProceedings{ dax.07.atva,
// author = {Christian Dax and Jochen Eisinger and Felix Klaedtke}, /// author = {Christian Dax and Jochen Eisinger and Felix Klaedtke},
// title = {Mechanizing the Powerset Construction for Restricted /// title = {Mechanizing the Powerset Construction for Restricted
// Classes of {$\omega$}-Automata}, /// Classes of {$\omega$}-Automata},
// year = 2007, /// year = 2007,
// series = {Lecture Notes in Computer Science}, /// series = {Lecture Notes in Computer Science},
// publisher = {Springer-Verlag}, /// publisher = {Springer-Verlag},
// volume = 4762, /// volume = 4762,
// booktitle = {Proceedings of the 5th International Symposium on /// booktitle = {Proceedings of the 5th International Symposium on
// Automated Technology for Verification and Analysis /// Automated Technology for Verification and Analysis
// (ATVA'07)}, /// (ATVA'07)},
// editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino /// editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino
// and Yoshio Okamura}, /// and Yoshio Okamura},
// month = oct /// month = oct
// } /// }
// \endverbatim /// \endverbatim
// ///
// Dax et al. suggest one way to check whether a property /// Dax et al. suggest one way to check whether a property
// \f$\varphi\f$ expressed as an LTL formula is an obligation: /// \f$\varphi\f$ expressed as an LTL formula is an obligation:
// translate the formula and its negation as two automata \f$A_f\f$ /// translate the formula and its negation as two automata \f$A_f\f$
// and \f$A_{\lnot f}\f$, then minimize both automata and check that /// and \f$A_{\lnot f}\f$, then minimize both automata and check
// the two products $\f \mathrm{minimize(A_{\lnot f})\otimes A_f\f$ /// that the two products $\f \mathrm{minimize(A_{\lnot f})\otimes
// and $\f \mathrm{minimize(A_f)\otimes A_{\lnot f}\f$ are empty. /// A_f\f$ and $\f \mathrm{minimize(A_f)\otimes A_{\lnot f}\f$ are
// If that is the case, then the minimization was correct. /// empty. If that is the case, then the minimization was correct.
// ///
// You may also want to check if \$A_f\$ is a safety automaton using /// You may also want to check if \$A_f\$ is a safety automaton
// the is_safety_automaton() function. Since safety properties are /// using the is_safety_automaton() function. Since safety
// a subclass of obligation properties, you can apply the /// properties are a subclass of obligation properties, you can
// minimization without further test. Note however that this is /// apply the minimization without further test. Note however that
// only a sufficient condition. /// this is only a sufficient condition.
// ///
// If \a monitor is set to \c true, the automaton will be converted /// If \a monitor is set to \c true, the automaton will be converted
// into minimal deterministic monitor. All useless SCCs should have /// into minimal deterministic monitor. All useless SCCs should
// been previously removed (using scc_filter() for instance). Then /// have been previously removed (using scc_filter() for instance).
// the automaton will be reduced as if all states where accepting /// Then the automaton will be reduced as if all states where
// states. /// accepting states.
// ///
// For more detail about monitors, see the following paper: /// For more detail about monitors, see the following paper:
// \verbatim /// \verbatim
// @InProceedings{ tabakov.10.rv, /// @InProceedings{ tabakov.10.rv,
// author = {Deian Tabakov and Moshe Y. Vardi}, /// author = {Deian Tabakov and Moshe Y. Vardi},
// title = {Optimized Temporal Monitors for SystemC{$^*$}}, /// title = {Optimized Temporal Monitors for SystemC{$^*$}},
// booktitle = {Proceedings of the 10th International Conferance on /// booktitle = {Proceedings of the 10th International Conferance
// Runtime Verification}, /// on Runtime Verification},
// pages = {436--451}, /// pages = {436--451},
// year = 2010, /// year = 2010,
// volume = {6418}, /// volume = {6418},
// series = {Lecture Notes in Computer Science}, /// series = {Lecture Notes in Computer Science},
// month = nov, /// month = nov,
// publisher = {Spring-Verlag} /// publisher = {Spring-Verlag}
// } /// }
// \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* minimize(const tgba* a, bool monitor = false);
/// \brief Minimize an automaton if it represents an obligation property.
///
/// This function attempt to minimize the automaton \a aut_f using the
/// algorithm implemented in the minimize() function, and presented
/// by the following paper:
///
/// \verbatim
/// @InProceedings{ dax.07.atva,
/// author = {Christian Dax and Jochen Eisinger and Felix Klaedtke},
/// title = {Mechanizing the Powerset Construction for Restricted
/// Classes of {$\omega$}-Automata},
/// year = 2007,
/// series = {Lecture Notes in Computer Science},
/// publisher = {Springer-Verlag},
/// volume = 4762,
/// booktitle = {Proceedings of the 5th International Symposium on
/// Automated Technology for Verification and Analysis
/// (ATVA'07)},
/// editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino
/// and Yoshio Okamura},
/// month = oct
/// }
/// \endverbatim
///
/// Because it is hard to determine if an automaton correspond
/// to an obligation property, you should supply either the formula
/// \a f expressed by the automaton \a aut_f, or \a aut_neg_f the negation
/// of the automaton \a aut_neg_f.
///
/// \param aut_f the automaton to minimize
/// \param f the LTL formula represented by the automaton \a aut_f
/// \param aut_neg_f an automaton representing the negation of \a aut_f
/// \return a new tgba if the automaton could be minimized, aut_f if
/// the automaton cannot be minimized, 0 if we do not if if the
/// minimization is correct because neither \a f nor \a aut_neg_f
/// were supplied.
///
/// The function proceeds as follows. If the formula \a f or the
/// automaton \a aut can easily be proved to represent an obligation
/// formula, then the result of \code minimize(aut) is returned.
/// 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
/// that \code product(aut,minimize(aut_neg_f)) and \code
/// product(aut_neg_f,minize(aut)) are both empty. If they are, the
/// the minimization was sound. (See the paper for full details.)
const tgba* minimize_obligation(const tgba* aut_f,
const ltl::formula* f = 0,
const tgba* aut_neg_f = 0);
} }
#endif /* !SPOT_TGBAALGOS_MINIMIZE_HH */ #endif /* !SPOT_TGBAALGOS_MINIMIZE_HH */
// Copyright (C) 2007, 2008, 2009, 2010 Laboratoire de Recherche et // Copyright (C) 2007, 2008, 2009, 2010, 2011 Laboratoire de Recherche et
// Dveloppement de l'Epita (LRDE). // Dveloppement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire d'Informatique de // Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire d'Informatique de
// Paris 6 (LIP6), dpartement Systmes Rpartis // Paris 6 (LIP6), dpartement Systmes Rpartis
...@@ -327,8 +327,8 @@ main(int argc, char** argv) ...@@ -327,8 +327,8 @@ main(int argc, char** argv)
spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::ltl::atomic_prop_set* unobservables = 0; spot::ltl::atomic_prop_set* unobservables = 0;
spot::tgba_explicit_string* system = 0; spot::tgba_explicit_string* system = 0;
spot::tgba* product = 0; const spot::tgba* product = 0;
spot::tgba* product_to_free = 0; const spot::tgba* product_to_free = 0;
spot::bdd_dict* dict = new spot::bdd_dict(); spot::bdd_dict* dict = new spot::bdd_dict();
spot::timer_map tm; spot::timer_map tm;
bool use_timer = false; bool use_timer = false;
...@@ -789,9 +789,9 @@ main(int argc, char** argv) ...@@ -789,9 +789,9 @@ main(int argc, char** argv)
} }
if (f || from_file) if (f || from_file)
{ {
spot::tgba_bdd_concrete* concrete = 0; const spot::tgba_bdd_concrete* concrete = 0;
spot::tgba* to_free = 0; const spot::tgba* to_free = 0;
spot::tgba* a = 0; const spot::tgba* a = 0;
if (from_file) if (from_file)
{ {
...@@ -867,7 +867,7 @@ main(int argc, char** argv) ...@@ -867,7 +867,7 @@ main(int argc, char** argv)
if (opt_monitor && ((reduc_aut & spot::Reduce_Scc) == 0)) if (opt_monitor && ((reduc_aut & spot::Reduce_Scc) == 0))
{ {
if (dynamic_cast<spot::tgba_bdd_concrete*>(a)) if (dynamic_cast<const spot::tgba_bdd_concrete*>(a))
symbolic_scc_pruning = true; symbolic_scc_pruning = true;
else else
reduc_aut |= spot::Reduce_Scc; reduc_aut |= spot::Reduce_Scc;
...@@ -875,8 +875,8 @@ main(int argc, char** argv) ...@@ -875,8 +875,8 @@ main(int argc, char** argv)
if (symbolic_scc_pruning) if (symbolic_scc_pruning)
{ {
spot::tgba_bdd_concrete* bc = const spot::tgba_bdd_concrete* bc =
dynamic_cast<spot::tgba_bdd_concrete*>(a); dynamic_cast<const spot::tgba_bdd_concrete*>(a);
if (!bc) if (!bc)
{ {
std::cerr << ("Error: Automaton is not symbolic: cannot " std::cerr << ("Error: Automaton is not symbolic: cannot "
...@@ -890,14 +890,15 @@ main(int argc, char** argv) ...@@ -890,14 +890,15 @@ main(int argc, char** argv)
{ {
tm.start("reducing A_f w/ symbolic SCC pruning"); tm.start("reducing A_f w/ symbolic SCC pruning");
if (bc) if (bc)
bc->delete_unaccepting_scc(); const_cast<spot::tgba_bdd_concrete*>(bc)
->delete_unaccepting_scc();
tm.stop("reducing A_f w/ symbolic SCC pruning"); tm.stop("reducing A_f w/ symbolic SCC pruning");
} }
} }
// Remove dead SCCs and useless acceptance conditions before // Remove dead SCCs and useless acceptance conditions before
// degeneralization. // degeneralization.
spot::tgba* aut_scc = 0; const spot::tgba* aut_scc = 0;
if (reduc_aut & spot::Reduce_Scc) if (reduc_aut & spot::Reduce_Scc)
{ {
tm.start("reducing A_f w/ SCC"); tm.start("reducing A_f w/ SCC");
...@@ -905,8 +906,8 @@ main(int argc, char** argv) ...@@ -905,8 +906,8 @@ main(int argc, char** argv)
tm.stop("reducing A_f w/ SCC"); tm.stop("reducing A_f w/ SCC");
} }
spot::tgba_tba_proxy* degeneralized = 0; const spot::tgba_tba_proxy* degeneralized = 0;
spot::tgba_sgba_proxy* state_labeled = 0; const spot::tgba_sgba_proxy* state_labeled = 0;
unsigned int n_acc = a->number_of_acceptance_conditions(); unsigned int n_acc = a->number_of_acceptance_conditions();
if (echeck_inst if (echeck_inst
...@@ -923,74 +924,31 @@ main(int argc, char** argv) ...@@ -923,74 +924,31 @@ main(int argc, char** argv)
a = state_labeled = new spot::tgba_sgba_proxy(a); a = state_labeled = new spot::tgba_sgba_proxy(a);
} }
spot::tgba_explicit* minimized = 0; const spot::tgba* minimized = 0;
if (opt_minimize) if (opt_minimize)
{ {
tm.start("WDBA-minimization"); tm.start("obligation minimization");
minimized = minimize(a); minimized = minimize_obligation(a, f);
tm.stop("WDBA-minimization"); tm.stop("obligation minimization");
tm.start("WDBA-check");
// If A is a safety automaton, the WDBA minimization if (minimized == 0)
// must be correct.
if (is_safety_automaton(a))
{
a = minimized;
}
else // We don't know if A is a safety automaton.
{ {
if (!f) // if (!f)
{ {
std::cerr << "Error: Without a formula I cannot make " std::cerr << "Error: Without a formula I cannot make "
<< "sure that the automaton built with -Rm\n" << "sure that the automaton built with -Rm\n"
<< " is correct." << std::endl; << " is correct." << std::endl;
exit(2); exit(2);
} }
// Let's make sure that A recognizes the same language
// as MINIMIZED.
spot::ltl::formula* neg =
spot::ltl::unop::instance(spot::ltl::unop::Not, f->clone());
spot::tgba* n = spot::ltl_to_tgba_fm(neg, dict, fm_exprop_opt,
fm_symb_merge_opt,
post_branching,
fair_loop_approx,
unobservables, fm_red);
neg->destroy();
spot::tgba* nscc = spot::scc_filter(n, true);
// If the negation is a safety automaton,
// then the minimization is correct.
if (is_safety_automaton(n))
{
a = minimized;
}
else
{
spot::tgba* p = new spot::tgba_product(minimized, nscc);
spot::emptiness_check* ec = couvreur99(p);
spot::emptiness_check_result* res = ec->check();
if (!res)
{
delete ec;
delete p;
spot::tgba* nm = minimize(nscc);
p = new spot::tgba_product(a, nm);
ec = couvreur99(p);
res = ec->check();
if (!res)
{
// Finally, we are now sure that it was safe
// to minimize the automaton.
a = minimized;
}
delete nm;
}
delete res;
delete ec;
delete p;
}
delete nscc;
delete n;
} }
tm.stop("WDBA-check"); else if (minimized == a)
{
minimized = 0;
}
else
{
a = minimized;
}
} }
if (opt_monitor) if (opt_monitor)
...@@ -1059,7 +1017,7 @@ main(int argc, char** argv) ...@@ -1059,7 +1017,7 @@ main(int argc, char** argv)
} }
} }
spot::tgba_explicit* expl = 0; const spot::tgba_explicit* expl = 0;
switch (dupexp) switch (dupexp)
{ {
case NoneDup: case NoneDup:
...@@ -1072,7 +1030,7 @@ main(int argc, char** argv) ...@@ -1072,7 +1030,7 @@ main(int argc, char** argv)
break; break;
} }
spot::tgba* product_degeneralized = 0; const spot::tgba* product_degeneralized = 0;
if (system) if (system)
{ {
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment