Cleanup the minimize.hh interface.
* src/tgbaalgos/minimize.hh, src/tgbaalgos/minimize.cc (minimize): Split into ... (minimize_wdba, minimize_monitor): ... these two functions. * src/tgbatest/ltl2tgba.cc (main): Adjust the call to minimize_monitor. * wrap/python/cgi-bin/ltl2tgba.in: Adjust the calls to minimize_monitor and minimize_obligation. * wrap/python/spot.i: Declare minimize_monitor, minimize_wdba, minimize_obligations. * src/tgba/tgbaexplicit.hh (tgba_explicit_string) (tgba_explicit_formula, tgba_explicit_number): Add fake declarations so that SWIG can see they inherits from tgba.
This commit is contained in:
Alexandre Duret-Lutz
parent
92126a6cf9
commit
8c972ad3ce
7 changed files with 182 additions and 136 deletions
17
ChangeLog
17
ChangeLog
|
|
@ -1,3 +1,20 @@
|
|||
2011-01-05 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||
|
||||
Cleanup the minimize.hh interface.
|
||||
|
||||
* src/tgbaalgos/minimize.hh, src/tgbaalgos/minimize.cc
|
||||
(minimize): Split into ...
|
||||
(minimize_wdba, minimize_monitor): ... these two functions.
|
||||
* src/tgbatest/ltl2tgba.cc (main): Adjust the call to
|
||||
minimize_monitor.
|
||||
* wrap/python/cgi-bin/ltl2tgba.in: Adjust the calls to
|
||||
minimize_monitor and minimize_obligation.
|
||||
* wrap/python/spot.i: Declare minimize_monitor, minimize_wdba,
|
||||
minimize_obligations.
|
||||
* src/tgba/tgbaexplicit.hh (tgba_explicit_string)
|
||||
(tgba_explicit_formula, tgba_explicit_number): Add fake
|
||||
declarations so that SWIG can see they inherits from tgba.
|
||||
|
||||
2011-01-05 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||
|
||||
Cleanup the DFA minimization algorithm.
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
// 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).
|
||||
// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
|
||||
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
|
|
@ -313,6 +313,7 @@ namespace spot
|
|||
|
||||
};
|
||||
|
||||
#ifndef SWIG
|
||||
class tgba_explicit_string:
|
||||
public tgba_explicit_labelled<std::string, string_hash>
|
||||
{
|
||||
|
|
@ -333,7 +334,13 @@ namespace spot
|
|||
name_state_map_[alias_name] = add_state(real_name);
|
||||
}
|
||||
};
|
||||
#else
|
||||
class tgba_explicit_string: public tgba
|
||||
{
|
||||
};
|
||||
#endif
|
||||
|
||||
#ifndef SWIG
|
||||
class tgba_explicit_formula:
|
||||
public tgba_explicit_labelled<const ltl::formula*, ltl::formula_ptr_hash>
|
||||
{
|
||||
|
|
@ -345,7 +352,13 @@ namespace spot
|
|||
virtual state* add_default_init();
|
||||
virtual std::string format_state(const spot::state* s) const;
|
||||
};
|
||||
#else
|
||||
class tgba_explicit_formula: public tgba
|
||||
{
|
||||
};
|
||||
#endif
|
||||
|
||||
#ifndef SWIG
|
||||
class tgba_explicit_number:
|
||||
public tgba_explicit_labelled<int, std::tr1::hash<int> >
|
||||
{
|
||||
|
|
@ -357,6 +370,11 @@ namespace spot
|
|||
virtual state* add_default_init();
|
||||
virtual std::string format_state(const spot::state* s) const;
|
||||
};
|
||||
#else
|
||||
class tgba_explicit_number: public tgba
|
||||
{
|
||||
};
|
||||
#endif
|
||||
}
|
||||
|
||||
#endif // SPOT_TGBA_TGBAEXPLICIT_HH
|
||||
|
|
|
|||
|
|
@ -506,7 +506,20 @@ namespace spot
|
|||
}
|
||||
|
||||
|
||||
tgba_explicit_number* minimize(const tgba* a, bool monitor)
|
||||
tgba_explicit_number* minimize_monitor(const tgba* a)
|
||||
{
|
||||
hash_set* final = new hash_set;
|
||||
tgba_explicit_number* det_a;
|
||||
|
||||
{
|
||||
power_map pm;
|
||||
det_a = tgba_powerset(a, pm);
|
||||
}
|
||||
// final is empty: there is no acceptance condition
|
||||
return minimize_dfa(det_a, final);
|
||||
}
|
||||
|
||||
tgba_explicit_number* minimize_wdba(const tgba* a)
|
||||
{
|
||||
hash_set* final = new hash_set;
|
||||
tgba_explicit_number* det_a;
|
||||
|
|
@ -515,8 +528,6 @@ namespace spot
|
|||
power_map pm;
|
||||
det_a = tgba_powerset(a, pm);
|
||||
|
||||
if (!monitor)
|
||||
{
|
||||
// For each SCC of the deterministic automaton, determine if
|
||||
// it is accepting or not.
|
||||
scc_map sm(det_a);
|
||||
|
|
@ -568,7 +579,6 @@ namespace spot
|
|||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
return minimize_dfa(det_a, final);
|
||||
}
|
||||
|
|
@ -577,8 +587,7 @@ namespace spot
|
|||
minimize_obligation(const tgba* aut_f,
|
||||
const ltl::formula* f, const tgba* aut_neg_f)
|
||||
{
|
||||
// WDBA minimization
|
||||
tgba_explicit_number* min_aut_f = minimize(aut_f);
|
||||
tgba_explicit_number* min_aut_f = minimize_wdba(aut_f);
|
||||
|
||||
// If aut_f is a safety automaton, the WDBA minimization must be
|
||||
// correct.
|
||||
|
|
|
|||
|
|
@ -26,14 +26,51 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Use the powerset construction to minimize a TGBA.
|
||||
/// \addtogroup tgba_reduction
|
||||
/// @{
|
||||
|
||||
/// \brief Construct a minimal deterministic monitor.
|
||||
///
|
||||
/// If \a monitor is set to \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.
|
||||
/// 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
|
||||
/// determinized and minimized using the standard DFA construction
|
||||
/// 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 in Spot at that time.)
|
||||
///
|
||||
/// \param a the automaton to convert into a minimal deterministic monitor
|
||||
/// \pre Dead SCCs should have been removed from \a a before
|
||||
/// calling this function.
|
||||
tgba_explicit_number* minimize_monitor(const tgba* a);
|
||||
|
||||
/// \brief Minimize a Büchi automaton in the WDBA class.
|
||||
///
|
||||
/// This takes a TGBA whose language is representable by
|
||||
/// a Weak Deterministic Büchi Automaton, and construct
|
||||
/// a minimal WDBA for this language.
|
||||
///
|
||||
/// If the input automaton does not represent a WDBA language,
|
||||
/// the resulting automaton is still a WDBA, but it will not
|
||||
/// be equivalent to the original automaton. Use the
|
||||
/// minimize_obligation() function if you are not sure whether
|
||||
/// it is safe to call this function.
|
||||
///
|
||||
/// Please see the following paper for a discussion of this
|
||||
/// technique.
|
||||
|
|
@ -55,51 +92,12 @@ namespace spot
|
|||
/// 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_number* minimize(const tgba* a, bool monitor = false);
|
||||
|
||||
tgba_explicit_number* minimize_wdba(const tgba* a);
|
||||
|
||||
/// \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
|
||||
/// This function attempts to minimize the automaton \a aut_f using the
|
||||
/// algorithm implemented in the minimize_wdba() function, and presented
|
||||
/// by the following paper:
|
||||
///
|
||||
/// \verbatim
|
||||
|
|
@ -120,7 +118,7 @@ namespace spot
|
|||
/// }
|
||||
/// \endverbatim
|
||||
///
|
||||
/// Because it is hard to determine if an automaton correspond
|
||||
/// Because it is hard to determine if an automaton corresponds
|
||||
/// 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.
|
||||
|
|
@ -135,16 +133,18 @@ namespace spot
|
|||
///
|
||||
/// 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_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.)
|
||||
/// formula, then the result of <code>minimize(aut)</code> 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_f))</code> and <code>
|
||||
/// product(aut_neg_f,minize(aut))</code> 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 */
|
||||
|
|
|
|||
|
|
@ -954,7 +954,7 @@ main(int argc, char** argv)
|
|||
if (opt_monitor)
|
||||
{
|
||||
tm.start("Monitor minimization");
|
||||
a = minimized = minimize(a, true);
|
||||
a = minimized = minimize_monitor(a);
|
||||
tm.stop("Monitor minimization");
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
#!@PYTHON@
|
||||
# -*- mode: python; coding: iso-8859-1 -*-
|
||||
# Copyright (C) 2007, 2009, 2010 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
# Copyright (C) 2007, 2009, 2010, 2011 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
# Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
|
||||
# Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
# Université Pierre et Marie Curie.
|
||||
|
|
@ -572,9 +572,9 @@ elif trans_taa:
|
|||
automaton = spot.ltl_to_taa(f, dict, refined_rules)
|
||||
|
||||
if reduce_dmonitor:
|
||||
automaton = spot.minimize(automaton, True)
|
||||
automaton = spot.minimize_monitor(automaton)
|
||||
elif reduce_wdba:
|
||||
automaton = spot.minimize(automaton, False)
|
||||
automaton = spot.minimize_obligation(automaton)
|
||||
elif reduce_scc:
|
||||
# Do not suppress all useless acceptance conditions if
|
||||
# degeneralization is requested: keeping those that lead to
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
// 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).
|
||||
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique
|
||||
// de Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
|
|
@ -147,7 +147,9 @@ using namespace spot;
|
|||
%feature("new") spot::ltl_to_taa;
|
||||
%feature("new") spot::ltl_to_tgba_fm;
|
||||
%feature("new") spot::ltl_to_tgba_lacim;
|
||||
%feature("new") spot::minimize;
|
||||
%feature("new") spot::minimize_wdba;
|
||||
%feature("new") spot::minimize_monitor;
|
||||
%feature("new") spot::minimize_obligation;
|
||||
%feature("new") spot::reduc_tgba_sim;
|
||||
%feature("new") spot::scc_filter;
|
||||
%feature("new") spot::tgba_dupexp_bfs;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue