0f15d28fe8
src/tgbaalgos/weight.hh: New files. * src/tgbaalgos/Makefile.am: Add them. * src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc, src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh, : Add emptiness check statistics capability. * src/tgbatest/randtgba.cc: Print these statistics. * src/tgbatest/ltl2tgba.cc: tau03opt search can deal without acceptance condition. * src/tgbatest/emptchk.test: Test tau03opt search.
64 lines
2.3 KiB
C++
64 lines
2.3 KiB
C++
// Copyright (C) 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_WEIGHT_HH
|
|
# define SPOT_TGBAALGOS_WEIGHT_HH
|
|
|
|
#include <iosfwd>
|
|
#include <map>
|
|
#include <bdd.h>
|
|
|
|
namespace spot
|
|
{
|
|
/// \brief Manage for a given automaton a vector of counter indexed by
|
|
/// its acceptance condition
|
|
|
|
class weight
|
|
{
|
|
public:
|
|
/// Construct a empty vector (all counters set to zero).
|
|
///
|
|
/// \param neg_all_cond : negation of all the acceptance conditions of
|
|
/// the automaton (the bdd returned by tgba::neg_acceptance_conditions()).
|
|
weight(const bdd& neg_all_cond);
|
|
/// Increment by one the counters of each acceptance condition in \a acc.
|
|
weight& operator+=(const bdd& acc);
|
|
/// Decrement by one the counters of each acceptance condition in \a acc.
|
|
weight& operator-=(const bdd& acc);
|
|
/// Return the set of each acceptance condition such that its counter is
|
|
/// strictly greatest than the corresponding counter in w.
|
|
///
|
|
/// \pre For each acceptance condition, its counter is greatest or equal to
|
|
/// the corresponding counter in w.
|
|
bdd operator-(const weight& w) const;
|
|
friend std::ostream& operator<<(std::ostream& os, const weight& w);
|
|
|
|
private:
|
|
typedef std::map<int, int> weight_vector;
|
|
weight_vector m;
|
|
bdd neg_all_acc;
|
|
static weight_vector* pm;
|
|
static void inc_weight_handler(char* varset, int size);
|
|
static void dec_weight_handler(char* varset, int size);
|
|
};
|
|
};
|
|
|
|
#endif // SPOT_TGBAALGOS_WEIGHT_HH
|