Don't pass the automaton to enumerate_cycle and is_weak_scc.
The scc_map knows the automaton already. * src/tgbaalgos/cycles.cc, src/tgbaalgos/cycles.hh, src/tgbaalgos/isweakscc.cc, src/tgbaalgos/isweakscc.hh: Simplify the interface. * src/tgbatest/ltl2tgba.cc: Adjust calls.
This commit is contained in:
parent
40de47f159
commit
d228784c39
5 changed files with 17 additions and 18 deletions
|
|
@ -23,9 +23,8 @@
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
enumerate_cycles::enumerate_cycles(const tgba* aut,
|
enumerate_cycles::enumerate_cycles(const scc_map& map)
|
||||||
const scc_map& map)
|
: aut_(map.get_aut()), sm_(map)
|
||||||
: aut_(aut), sm_(map)
|
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -63,12 +63,12 @@ namespace spot
|
||||||
/// dfs_ stack. Only the last portion of this stack may form a
|
/// dfs_ stack. Only the last portion of this stack may form a
|
||||||
/// cycle.
|
/// cycle.
|
||||||
///
|
///
|
||||||
/// The class constructor takes an automaton and an scc_map that
|
/// The class constructor takes an scc_map that should already have
|
||||||
/// should already have been built for that automaton. Calling
|
/// been built for its automaton. Calling run(n) will enumerate all
|
||||||
/// run(n) will enumerate all elementary cycles in SCC #n. Each
|
/// elementary cycles in SCC #n. Each time an SCC is found, the
|
||||||
/// time an SCC is found, the method cycle_found(s) is called with
|
/// method cycle_found(s) is called with the initial state s of the
|
||||||
/// the initial state s of the cycle: the cycle is constituted from
|
/// cycle: the cycle is constituted from all the states that are on
|
||||||
/// all the states that are on the dfs_ stack after s (including s).
|
/// the dfs_ stack after s (including s).
|
||||||
///
|
///
|
||||||
/// You should inherit from this class and redefine the
|
/// You should inherit from this class and redefine the
|
||||||
/// cycle_found() method to perform any work you would like to do on
|
/// cycle_found() method to perform any work you would like to do on
|
||||||
|
|
@ -130,7 +130,7 @@ namespace spot
|
||||||
dfs_stack dfs_;
|
dfs_stack dfs_;
|
||||||
|
|
||||||
public:
|
public:
|
||||||
enumerate_cycles(const tgba* aut, const scc_map& map);
|
enumerate_cycles(const scc_map& map);
|
||||||
|
|
||||||
/// \brief Run in SCC scc, and call \a cycle_found() for any new
|
/// \brief Run in SCC scc, and call \a cycle_found() for any new
|
||||||
/// elementary cycle found.
|
/// elementary cycle found.
|
||||||
|
|
|
||||||
|
|
@ -33,8 +33,8 @@ namespace spot
|
||||||
public:
|
public:
|
||||||
bool result;
|
bool result;
|
||||||
|
|
||||||
weak_checker(const tgba* aut, const scc_map& map)
|
weak_checker(const scc_map& map)
|
||||||
: enumerate_cycles(aut, map), result(true)
|
: enumerate_cycles(map), result(true)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -66,14 +66,14 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
bool
|
bool
|
||||||
is_weak_scc(const tgba* aut, scc_map& map, unsigned scc)
|
is_weak_scc(scc_map& map, unsigned scc)
|
||||||
{
|
{
|
||||||
// If no cycle is accepting, the SCC is weak.
|
// If no cycle is accepting, the SCC is weak.
|
||||||
if (!map.accepting(scc))
|
if (!map.accepting(scc))
|
||||||
return true;
|
return true;
|
||||||
// If the SCC is accepting, but one cycle is not, the SCC is not
|
// If the SCC is accepting, but one cycle is not, the SCC is not
|
||||||
// weak.
|
// weak.
|
||||||
weak_checker w(aut, map);
|
weak_checker w(map);
|
||||||
w.run(scc);
|
w.run(scc);
|
||||||
return w.result;
|
return w.result;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -28,7 +28,7 @@ namespace spot
|
||||||
/// \addtogroup tgba_misc
|
/// \addtogroup tgba_misc
|
||||||
/// @{
|
/// @{
|
||||||
|
|
||||||
/// \brief Whether the SCC number \a scc in \a aut is weak.
|
/// \brief Whether the SCC number \a scc in \a map is weak.
|
||||||
///
|
///
|
||||||
/// An SCC is weak if either its cycles are all accepting, or they
|
/// An SCC is weak if either its cycles are all accepting, or they
|
||||||
/// are all non-accepting.
|
/// are all non-accepting.
|
||||||
|
|
@ -38,7 +38,7 @@ namespace spot
|
||||||
/// whether the SCC is non-accepting already). For the accepting
|
/// whether the SCC is non-accepting already). For the accepting
|
||||||
/// SCCs, this function enumerates all cycles in the given SCC (it
|
/// SCCs, this function enumerates all cycles in the given SCC (it
|
||||||
/// stops if it find a non-accepting cycle).
|
/// stops if it find a non-accepting cycle).
|
||||||
bool is_weak_scc(const tgba* aut, scc_map& map, unsigned scc);
|
bool is_weak_scc(scc_map& map, unsigned scc);
|
||||||
|
|
||||||
/// @}
|
/// @}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -1425,7 +1425,7 @@ main(int argc, char** argv)
|
||||||
{
|
{
|
||||||
spot::scc_map m(a);
|
spot::scc_map m(a);
|
||||||
m.build_map();
|
m.build_map();
|
||||||
spot::enumerate_cycles c(a, m);
|
spot::enumerate_cycles c(m);
|
||||||
unsigned max = m.scc_count();
|
unsigned max = m.scc_count();
|
||||||
for (unsigned n = 0; n < max; ++n)
|
for (unsigned n = 0; n < max; ++n)
|
||||||
{
|
{
|
||||||
|
|
@ -1441,7 +1441,7 @@ main(int argc, char** argv)
|
||||||
unsigned max = m.scc_count();
|
unsigned max = m.scc_count();
|
||||||
for (unsigned n = 0; n < max; ++n)
|
for (unsigned n = 0; n < max; ++n)
|
||||||
{
|
{
|
||||||
bool w = spot::is_weak_scc(a, m, n);
|
bool w = spot::is_weak_scc(m, n);
|
||||||
std::cout << "SCC #" << n
|
std::cout << "SCC #" << n
|
||||||
<< (w ? " is weak" : " is not weak")
|
<< (w ? " is weak" : " is not weak")
|
||||||
<< std::endl;
|
<< std::endl;
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue