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

Preliminary support for monitors.

* src/tgbatest/ltl2tgba.cc (-M): New option for building
deterministic monitors.
* src/tgbaalgos/minimize.cc (minimize): Take a monitor
argument and adjust the code.
* src/tgbaalgos/minimize.hh (minimize): Document it.
parent a962bb6d
2010-11-25 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Preliminary support for monitors.
* src/tgbatest/ltl2tgba.cc (-M): New option for building
deterministic monitors.
* src/tgbaalgos/minimize.cc (minimize): Take a monitor
argument and adjust the code.
* src/tgbaalgos/minimize.hh (minimize): Document it.
2010-11-25 Alexandre Duret-Lutz <adl@lrde.epita.fr>
"ltl2tgba -Rm -X foo.tgba" would fail.
......
......@@ -135,14 +135,14 @@ namespace spot
return res;
}
tgba_explicit* minimize(const tgba* a)
tgba_explicit* minimize(const tgba* a, bool monitor)
{
// The list of accepting states of a.
std::list<const state*> acc_list;
std::queue<hash_set*> todo;
// The list of equivalent states.
std::list<hash_set*> done;
tgba_explicit* det_a = tgba_powerset(a, &acc_list);
tgba_explicit* det_a = tgba_powerset(a, monitor ? 0 : &acc_list);
hash_set* final = new hash_set;
hash_set* non_final = new hash_set;
hash_map state_set_map;
......
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -25,8 +25,74 @@
namespace spot
{
tgba_explicit* minimize(const tgba* a);
// \brief Use the powerset construction to minimize a TGBA.
//
// If \a monitor is set of \c false (the default), then the
// minimized automaton is correct only for properties that belong to
// the class of "obligation properties". This algorithm assumes
// that the given automaton expresses an obligation properties and
// will return an automaton that is bogus (i.e. not equivalent to
// the original) if that is not the case.
//
// Please see the following paper for a discussion of this
// technique.
//
// \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
//
// Dax et al. suggest one way to check whether a property
// \f$\varphi\f$ expressed as an LTL formula is an obligation:
// 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
// the two products $\f \mathrm{minimize(A_{\lnot f})\otimes A_f\f$
// and $\f \mathrm{minimize(A_f)\otimes A_{\lnot f}\f$ are 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
// the is_safety_automaton() function. Since safety properties are
// a subclass of obligation properties, you can apply the
// minimization without further test. Note however that this is
// only a sufficient condition.
//
// If \a monitor is set to \c true, the automaton will be converted
// into minimal deterministic monitor. All useless SCCs should have
// been previously removed (using scc_filter() for instance). Then
// the automaton will be reduced as if all states where accepting
// states.
//
// For more detail about monitors, see the following paper:
// \verbatim
// @InProceedings{ tabakov.10.rv,
// author = {Deian Tabakov and Moshe Y. Vardi},
// title = {Optimized Temporal Monitors for SystemC{$^*$}},
// booktitle = {Proceedings of the 10th International Conferance on
// Runtime Verification},
// pages = {436--451},
// year = 2010,
// volume = {6418},
// series = {Lecture Notes in Computer Science},
// month = nov,
// publisher = {Spring-Verlag}
// }
// \endverbatim
// (Note: although the above paper uses Spot, this function did not
// exist at that time.)
tgba_explicit* minimize(const tgba* a, bool monitor = false);
}
#endif /* !SPOT_TGBAALGOS_MINIMIZE_HH */
......@@ -213,6 +213,11 @@ syntax(char* prog)
<< " -Rm attempt to minimize the automata" << std::endl
<< std::endl
<< "Automaton conversion:"
<< " -M convert into a deterministic minimal monitor "
<< "(implies -R3 or R3b)" << std::endl
<< std::endl
<< "Options for performing emptiness checks:" << std::endl
<< " -e[ALGO] run emptiness check, expect and compute an "
<< "accepting run" << std::endl
......@@ -316,6 +321,7 @@ main(int argc, char** argv)
bool graph_run_tgba_opt = false;
bool opt_reduce = false;
bool opt_minimize = false;
bool opt_monitor = false;
bool containment = false;
bool show_fc = false;
bool spin_comments = false;
......@@ -632,6 +638,10 @@ main(int argc, char** argv)
{
opt_minimize = true;
}
else if (!strcmp(argv[formula_index], "-M"))
{
opt_monitor = true;
}
else if (!strcmp(argv[formula_index], "-s"))
{
dupexp = DFS;
......@@ -856,6 +866,14 @@ main(int argc, char** argv)
to_free = a;
}
if (opt_monitor && ((reduc_aut & spot::Reduce_Scc) == 0))
{
if (dynamic_cast<spot::tgba_bdd_concrete*>(a))
symbolic_scc_pruning = true;
else
reduc_aut |= spot::Reduce_Scc;
}
if (symbolic_scc_pruning)
{
spot::tgba_bdd_concrete* bc =
......@@ -976,6 +994,13 @@ main(int argc, char** argv)
tm.stop("WDBA-check");
}
if (opt_monitor)
{
tm.start("Monitor minimization");
a = minimized = minimize(a, true);
tm.stop("Monitor minimization");
}
spot::tgba_reduc* aut_red = 0;
if (reduc_aut != spot::Reduce_None)
{
......
Markdown is supported
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