Commit 11704d31 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

scc_info: improve split_on_sets

* spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh (split_on_set):
Allow names to be preserved
* python/spot/impl.i: Instantiate std::vector<spot::twa_graph_ptr>.
parent 33af116f
...@@ -577,6 +577,7 @@ def state_is_accepting(self, src) -> "bool": ...@@ -577,6 +577,7 @@ def state_is_accepting(self, src) -> "bool":
%include <spot/twaalgos/sccinfo.hh> %include <spot/twaalgos/sccinfo.hh>
%template(scc_info_scc_edges) spot::internal::scc_edges<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data> const, spot::internal::keep_all>; %template(scc_info_scc_edges) spot::internal::scc_edges<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data> const, spot::internal::keep_all>;
%template(scc_info_inner_scc_edges) spot::internal::scc_edges<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data> const, spot::internal::keep_inner_scc>; %template(scc_info_inner_scc_edges) spot::internal::scc_edges<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data> const, spot::internal::keep_inner_scc>;
%template(vector_twa_graph) std::vector<spot::twa_graph_ptr>;
%include <spot/twaalgos/strength.hh> %include <spot/twaalgos/strength.hh>
%include <spot/twaalgos/sccfilter.hh> %include <spot/twaalgos/sccfilter.hh>
%include <spot/twaalgos/stats.hh> %include <spot/twaalgos/stats.hh>
......
...@@ -448,7 +448,8 @@ namespace spot ...@@ -448,7 +448,8 @@ namespace spot
} }
std::vector<twa_graph_ptr> std::vector<twa_graph_ptr>
scc_info::split_on_sets(unsigned scc, acc_cond::mark_t sets) const scc_info::split_on_sets(unsigned scc, acc_cond::mark_t sets,
bool preserve_names) const
{ {
std::vector<twa_graph_ptr> res; std::vector<twa_graph_ptr> res;
...@@ -480,7 +481,11 @@ namespace spot ...@@ -480,7 +481,11 @@ namespace spot
}, },
init); init);
if (copy->num_edges()) if (copy->num_edges())
res.push_back(copy); {
if (preserve_names)
copy->copy_state_names_from(aut_);
res.push_back(copy);
}
} }
return res; return res;
} }
...@@ -564,5 +569,4 @@ namespace spot ...@@ -564,5 +569,4 @@ namespace spot
return res; return res;
} }
} }
...@@ -549,14 +549,19 @@ namespace spot ...@@ -549,14 +549,19 @@ namespace spot
bdd scc_ap_support(unsigned scc) const; bdd scc_ap_support(unsigned scc) const;
protected: /// \brief Split an SCC into multiple automata separated by some
/// \brief: Remove in 'scc', edges containing any mark in 'sets'. /// acceptance sets.
/// ///
/// Such a deletion may split the SCC, in which case, the function builds /// Pretend that the transitions of SCC \a scc that belong to any
/// and returns more than one automaton representing the specified SCC. /// of the sets given in \a sets have been removed, and return a
std::vector<twa_graph_ptr> /// set of automata necessary to cover all remaining states.
split_on_sets(unsigned scc, acc_cond::mark_t sets) const; ///
/// Set \a preserve_names to True if you want to keep the original
/// name of each states for display. (This is a bit slower.)
std::vector<twa_graph_ptr> split_on_sets(unsigned scc,
acc_cond::mark_t sets,
bool preserve_names = false) const;
protected:
/// \brief: Recursive function used by states_on_acc_cycle_of(). /// \brief: Recursive function used by states_on_acc_cycle_of().
void void
states_on_acc_cycle_of_rec(unsigned scc, states_on_acc_cycle_of_rec(unsigned scc,
...@@ -573,7 +578,6 @@ namespace spot ...@@ -573,7 +578,6 @@ namespace spot
/// acceptance condition. /// acceptance condition.
std::vector<unsigned> std::vector<unsigned>
states_on_acc_cycle_of(unsigned scc) const; states_on_acc_cycle_of(unsigned scc) const;
}; };
......
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