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

determinize: improve the storage of implications

Browse source 
* spot/twaalgos/determinize.cc: Store implications
in a vector, not a map.
* spot/twaalgos/simulation.cc, spot/twaalgos/simulation.hh: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2016-10-21 13:56:36 +02:00
parent 7ea9454614
commit 6ca555ed89
3 changed files with 13 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

14
spot/twaalgos/determinize.cc
View file

@ -66,7 +66,7 @@ namespace spot
compute_succs(const const_twa_graph_ptr& aut, compute_succs(const const_twa_graph_ptr& aut,
succs_t& res, succs_t& res,
const scc_info& scc, const scc_info& scc,
const std::map<int, bdd>& implications, const std::vector<bdd>& implications,
const std::vector<bool>& is_connected, const std::vector<bool>& is_connected,
std::unordered_map<bdd, unsigned, bdd_hash>& bdd2num, std::unordered_map<bdd, unsigned, bdd_hash>& bdd2num,
std::vector<bdd>& all_bdds, std::vector<bdd>& all_bdds,
@ -78,14 +78,14 @@ namespace spot
compute_succ(const const_twa_graph_ptr& aut, compute_succ(const const_twa_graph_ptr& aut,
const bdd& ap, const bdd& ap,
const scc_info& scc, const scc_info& scc,
const std::map<int, bdd>& implications, const std::vector<bdd>& implications,
const std::vector<bool>& is_connected, const std::vector<bool>& is_connected,
bool use_scc, bool use_scc,
bool use_simulation) const; bool use_simulation) const;
// The outermost brace of each node cannot be green // The outermost brace of each node cannot be green
void ungreenify_last_brace(); void ungreenify_last_brace();
// When a nodes a implies a node b, remove the node a. // When a nodes a implies a node b, remove the node a.
void merge_redundant_states(const std::map<int, bdd>& implications, void merge_redundant_states(const std::vector<bdd>& implications,
const scc_info& scc, const scc_info& scc,
const std::vector<bool>& is_connected); const std::vector<bool>& is_connected);
// Used when creating the list of successors // Used when creating the list of successors
@ -252,7 +252,7 @@ namespace spot
safra_state::compute_succ(const const_twa_graph_ptr& aut, safra_state::compute_succ(const const_twa_graph_ptr& aut,
const bdd& ap, const bdd& ap,
const scc_info& scc, const scc_info& scc,
const std::map<int, bdd>& implications, const std::vector<bdd>& implications,
const std::vector<bool>& is_connected, const std::vector<bool>& is_connected,
bool use_scc, bool use_scc,
bool use_simulation) const bool use_simulation) const
@ -289,7 +289,7 @@ namespace spot
safra_state::compute_succs(const const_twa_graph_ptr& aut, safra_state::compute_succs(const const_twa_graph_ptr& aut,
succs_t& res, succs_t& res,
const scc_info& scc, const scc_info& scc,
const std::map<int, bdd>& implications, const std::vector<bdd>& implications,
const std::vector<bool>& is_connected, const std::vector<bool>& is_connected,
std::unordered_map<bdd, unsigned, bdd_hash>& std::unordered_map<bdd, unsigned, bdd_hash>&
bdd2num, bdd2num,
@ -337,7 +337,7 @@ namespace spot
} }
void void
safra_state::merge_redundant_states(const std::map<int, bdd>& implications, safra_state::merge_redundant_states(const std::vector<bdd>& implications,
const scc_info& scc, const scc_info& scc,
const std::vector<bool>& is_connected) const std::vector<bool>& is_connected)
{ {
@ -590,7 +590,7 @@ namespace spot
// Degeneralize // Degeneralize
twa_graph_ptr aut = spot::degeneralize_tba(a); twa_graph_ptr aut = spot::degeneralize_tba(a);
std::map<int, bdd> implications; std::vector<bdd> implications;
if (use_simulation) if (use_simulation)
{ {
aut = spot::scc_filter(aut); aut = spot::scc_filter(aut);

8
spot/twaalgos/simulation.cc
View file

@ -343,7 +343,7 @@ namespace spot
} }
// The core loop of the algorithm. // The core loop of the algorithm.
twa_graph_ptr run(std::map<int, bdd>* implications = nullptr) twa_graph_ptr run(std::vector<bdd>* implications = nullptr)
{ {
main_loop(); main_loop();
return build_result(implications); return build_result(implications);
@ -462,7 +462,7 @@ namespace spot
} }
// Build the minimal resulting automaton. // Build the minimal resulting automaton.
twa_graph_ptr build_result(std::map<int, bdd>* implications = nullptr) twa_graph_ptr build_result(std::vector<bdd>* implications = nullptr)
{ {
twa_graph_ptr res = make_twa_graph(a_->get_dict()); twa_graph_ptr res = make_twa_graph(a_->get_dict());
res->copy_ap_of(a_); res->copy_ap_of(a_);
@ -473,6 +473,8 @@ namespace spot
auto* gb = res->create_namer<int>(); auto* gb = res->create_namer<int>();
if (implications)
implications->resize(bdd_lstate_.size());
// Create one state per partition. // Create one state per partition.
for (auto& p: bdd_lstate_) for (auto& p: bdd_lstate_)
{ {
@ -711,7 +713,7 @@ namespace spot
twa_graph_ptr twa_graph_ptr
simulation(const const_twa_graph_ptr& t, simulation(const const_twa_graph_ptr& t,
std::map<int, bdd>* implications) std::vector<bdd>* implications)
{ {
direct_simulation<false, false> simul(t); direct_simulation<false, false> simul(t);
return simul.run(implications); return simul.run(implications);

2
spot/twaalgos/simulation.hh
View file

@ -71,7 +71,7 @@ namespace spot
simulation(const const_twa_graph_ptr& automaton); simulation(const const_twa_graph_ptr& automaton);
SPOT_API twa_graph_ptr SPOT_API twa_graph_ptr
simulation(const const_twa_graph_ptr& automaton, simulation(const const_twa_graph_ptr& automaton,
std::map<int, bdd>* implementation); std::vector<bdd>* implications);
SPOT_API twa_graph_ptr SPOT_API twa_graph_ptr
simulation_sba(const const_twa_graph_ptr& automaton); simulation_sba(const const_twa_graph_ptr& automaton);
/// @} /// @}