alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Speedup is_weak_scc() if all transitions in the SCC are accepting.

Browse source 
* src/tgbaalgos/isweakscc.cc, src/tgbaalgos/isweakscc.hh: Speedup when
all transitions are accepting.
This commit is contained in:
Alexandre Duret-Lutz 2012-09-21 15:09:08 +02:00
parent d228784c39
commit 3c17c418a2
2 changed files with 9 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tgbaalgos/isweakscc.cc
View file

@ -71,6 +71,10 @@ namespace spot
// 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 all transitions use all acceptance conditions, the SCC is weak.
if (map.useful_acc_of(scc) ==
bdd_support(map.get_aut()->neg_acceptance_conditions()))
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(map); weak_checker w(map);

8
src/tgbaalgos/isweakscc.hh
View file

@ -35,9 +35,11 @@ namespace spot
/// ///
/// The scc_map \a map should have been built already. The absence /// The scc_map \a map should have been built already. The absence
/// of accepting cycle is easy to check (the scc_map can tell /// of accepting cycle is easy to check (the scc_map can tell
/// whether the SCC is non-accepting already). For the accepting /// whether the SCC is non-accepting already). Similarly, an SCC in
/// SCCs, this function enumerates all cycles in the given SCC (it /// which all transitions belong to all acceptance sets is
/// stops if it find a non-accepting cycle). /// necessarily weak.
/// For other accepting SCCs, this function enumerates all cycles in
/// the given SCC (it stops if it find a non-accepting cycle).
bool is_weak_scc(scc_map& map, unsigned scc); bool is_weak_scc(scc_map& map, unsigned scc);
/// @} /// @}