7069d5406b
formula automaton and the synchronized product) from LBTT. Idea from Jean-Michel Couvreur. * src/tgbaalgos/lbtt.cc (nonacceptant_lbtt_bfs): New class. (nonacceptant_lbtt_reachable): New function. * src/tgbaalgos/lbtt.hh (nonacceptant_lbtt_reachable): New function. * src/tgbatest/ltl2tgba.cc (main): Call nonacceptant_lbtt_reachable if the -T option is used. * src/tgbatest/spotlbtt.test: Setup the -T variants, disabled by default.
72 lines
3 KiB
C++
72 lines
3 KiB
C++
// 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.
|
|
//
|
|
// Spot is free software; you can redistribute it and/or modify it
|
|
// under the terms of the GNU General Public License as published by
|
|
// the Free Software Foundation; either version 2 of the License, or
|
|
// (at your option) any later version.
|
|
//
|
|
// Spot is distributed in the hope that it will be useful, but WITHOUT
|
|
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
|
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
|
// License for more details.
|
|
//
|
|
// You should have received a copy of the GNU General Public License
|
|
// along with Spot; see the file COPYING. If not, write to the Free
|
|
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
|
// 02111-1307, USA.
|
|
|
|
#ifndef SPOT_TGBAALGOS_LBTT_HH
|
|
# define SPOT_TGBAALGOS_LBTT_HH
|
|
|
|
#include "tgba/tgba.hh"
|
|
#include <iostream>
|
|
|
|
namespace spot
|
|
{
|
|
/// \brief Print reachable states in LBTT format.
|
|
///
|
|
/// Note that LBTT expects an automaton with transition
|
|
/// labeled by propositional formulae, and generalized
|
|
/// Büchi acceptance conditions on \b states. This
|
|
/// is unlike our spot::tgba automata which put
|
|
/// both generalized acceptance conditions (and propositional
|
|
/// formulae) on \b transitions.
|
|
///
|
|
/// This algorithm will therefore produce an automata where
|
|
/// acceptance conditions have been moved from each transition to
|
|
/// the previous state. In the worst case, doing so will multiply
|
|
/// the number of states and transitions of the automata by
|
|
/// <code>2^|Acc|</code>. where <code>|Acc|</code> is the number of
|
|
/// acceptance conditions used by the automata. (It can be a bit
|
|
/// more because LBTT allows only for one initial state:
|
|
/// lbtt_reachable() may also have to create an additional state in
|
|
/// case the source initial state had to be split.) You have been
|
|
/// warned.
|
|
///
|
|
/// \param g The automata to print.
|
|
/// \param os Where to print.
|
|
std::ostream& lbtt_reachable(std::ostream& os, const tgba* g);
|
|
|
|
/// \brief Print an LBTT automaton for statistics.
|
|
///
|
|
/// Output \a g in LBTT's format but ignoring the acceptance
|
|
/// conditions, of all its transitions. This produces an automaton
|
|
/// that has the same size as \a g, and whose synchronized product
|
|
/// with another automaton also has the same size. This will also
|
|
/// declare as much acceptance conditions has there is in \a g (they
|
|
/// will just be never used).
|
|
///
|
|
/// The produced automaton will not recognize any word (unless \a g
|
|
/// has no acceptance condition, in which case this function is a
|
|
/// no-op).
|
|
///
|
|
/// The produced automaton is useful to obtain accurate statistics
|
|
/// from LBTT, without any size blow up of the automata.
|
|
std::ostream& nonacceptant_lbtt_reachable(std::ostream& os, const tgba* g);
|
|
}
|
|
|
|
#endif // SPOT_TGBAALGOS_LBTT_HH
|