diff --git a/src/tgbaalgos/cycles.cc b/src/tgbaalgos/cycles.cc index e6551571f..907e3e636 100644 --- a/src/tgbaalgos/cycles.cc +++ b/src/tgbaalgos/cycles.cc @@ -23,9 +23,8 @@ namespace spot { - enumerate_cycles::enumerate_cycles(const tgba* aut, - const scc_map& map) - : aut_(aut), sm_(map) + enumerate_cycles::enumerate_cycles(const scc_map& map) + : aut_(map.get_aut()), sm_(map) { } diff --git a/src/tgbaalgos/cycles.hh b/src/tgbaalgos/cycles.hh index 77d29d431..72ed3bac9 100644 --- a/src/tgbaalgos/cycles.hh +++ b/src/tgbaalgos/cycles.hh @@ -63,12 +63,12 @@ namespace spot /// dfs_ stack. Only the last portion of this stack may form a /// cycle. /// - /// The class constructor takes an automaton and an scc_map that - /// should already have been built for that automaton. Calling - /// run(n) will enumerate all elementary cycles in SCC #n. Each - /// time an SCC is found, the method cycle_found(s) is called with - /// the initial state s of the cycle: the cycle is constituted from - /// all the states that are on the dfs_ stack after s (including s). + /// The class constructor takes an scc_map that should already have + /// been built for its automaton. Calling run(n) will enumerate all + /// elementary cycles in SCC #n. Each time an SCC is found, the + /// method cycle_found(s) is called with the initial state s of the + /// cycle: the cycle is constituted from all the states that are on + /// the dfs_ stack after s (including s). /// /// You should inherit from this class and redefine the /// cycle_found() method to perform any work you would like to do on @@ -130,7 +130,7 @@ namespace spot dfs_stack dfs_; 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 /// elementary cycle found. diff --git a/src/tgbaalgos/isweakscc.cc b/src/tgbaalgos/isweakscc.cc index 5a9dc13c7..19e1e7526 100644 --- a/src/tgbaalgos/isweakscc.cc +++ b/src/tgbaalgos/isweakscc.cc @@ -33,8 +33,8 @@ namespace spot public: bool result; - weak_checker(const tgba* aut, const scc_map& map) - : enumerate_cycles(aut, map), result(true) + weak_checker(const scc_map& map) + : enumerate_cycles(map), result(true) { } @@ -66,14 +66,14 @@ namespace spot } 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 (!map.accepting(scc)) return true; // If the SCC is accepting, but one cycle is not, the SCC is not // weak. - weak_checker w(aut, map); + weak_checker w(map); w.run(scc); return w.result; } diff --git a/src/tgbaalgos/isweakscc.hh b/src/tgbaalgos/isweakscc.hh index 931bb333d..d28a4b205 100644 --- a/src/tgbaalgos/isweakscc.hh +++ b/src/tgbaalgos/isweakscc.hh @@ -28,7 +28,7 @@ namespace spot /// \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 /// are all non-accepting. @@ -38,7 +38,7 @@ namespace spot /// whether the SCC is non-accepting already). For the accepting /// SCCs, this function enumerates all cycles in the given SCC (it /// 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); /// @} } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 5a0eeb322..6c690ecb1 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1425,7 +1425,7 @@ main(int argc, char** argv) { spot::scc_map m(a); m.build_map(); - spot::enumerate_cycles c(a, m); + spot::enumerate_cycles c(m); unsigned max = m.scc_count(); for (unsigned n = 0; n < max; ++n) { @@ -1441,7 +1441,7 @@ main(int argc, char** argv) unsigned max = m.scc_count(); 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 << (w ? " is weak" : " is not weak") << std::endl;