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

Add trivial() and one_state_of() functions to scc_map.

* src/tgbaalgos/scc.hh, src/tgbaalgos/scc.cc (scc_map::trivial,
scc_map::one_state_of): Two new helper functions.
parent 5bc6d1d4
2011-01-04 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Add trivial() and one_state_of() functions to scc_map.
* src/tgbaalgos/scc.hh, src/tgbaalgos/scc.cc (scc_map::trivial,
scc_map::one_state_of): Two new helper functions.
2011-01-04 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/tgba/tgbaunion.hh: Remove one useless include.
......
// Copyright (C) 2008, 2009 Laboratoire de Recherche et Developpement de
// l'Epita.
// Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et
// Developpement de l'Epita.
//
// This file is part of Spot, a model checking library.
//
......@@ -74,6 +74,13 @@ namespace spot
return scc_map_[n].succ;
}
bool
scc_map::trivial(unsigned n) const
{
assert(scc_map_.size() > n);
return scc_map_[n].trivial;
}
bool
scc_map::accepting(unsigned n) const
{
......@@ -347,6 +354,12 @@ namespace spot
return scc_map_[n].states;
}
const state* scc_map::one_state_of(unsigned n) const
{
assert(scc_map_.size() > n);
return scc_map_[n].states.front();
}
unsigned scc_map::scc_count() const
{
return scc_map_.size();
......
......@@ -105,6 +105,13 @@ namespace spot
/// \pre This should only be called once build_map() has run.
const succ_type& succ(unsigned n) const;
/// \brief Return whether an SCC is trivial.
///
/// Trivial SCCs have one state and no self-loop.
///
/// \pre This should only be called once build_map() has run.
bool trivial(unsigned n) const;
/// \brief Return whether an SCC is accepting.
///
/// \pre This should only be called once build_map() has run.
......@@ -150,6 +157,14 @@ namespace spot
/// \pre This should only be called once build_map() has run.
const std::list<const state*>& states_of(unsigned n) const;
/// \brief Return one state of an SCC.
///
/// The state in the returned list is still owned by the scc_map
/// instance. It should NOT be deleted by the client code.
///
/// \pre This should only be called once build_map() has run.
const state* one_state_of(unsigned n) const;
/// \brief Return the number of the SCC a state belongs too.
///
/// \pre This should only be called once build_map() has run.
......
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