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

convert: simplify interfaces

Browse source 
* spot/twacube_algos/convert.cc, spot/twacube_algos/convert.hh,
tests/core/twacube.cc: here.
This commit is contained in:
Etienne Renault 2016-04-20 14:22:21 +02:00
parent e11f24dbc1
commit d430129bb1
3 changed files with 15 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

13
spot/twacube_algos/convert.cc
View file

@ -59,12 +59,14 @@ namespace spot
return result; return result;
} }
spot::twacube* twa_to_twacube(spot::twa_graph_ptr& aut, spot::twacube* twa_to_twacube(const spot::const_twa_graph_ptr aut)
std::unordered_map<int, int>& ap_binder,
std::vector<std::string>& aps)
{ {
// Compute the necessary binder and extract atomic propositions
std::unordered_map<int, int> ap_binder;
std::vector<std::string>* aps = extract_aps(aut, ap_binder);
// Declare the twa cube // Declare the twa cube
spot::twacube* tg = new spot::twacube(aps); spot::twacube* tg = new spot::twacube(*aps);
// Fix acceptance // Fix acceptance
tg->acc() = aut->acc(); tg->acc() = aut->acc();
@ -111,11 +113,12 @@ namespace spot
} }
// Must be contiguous to support swarming. // Must be contiguous to support swarming.
assert(tg->succ_contiguous()); assert(tg->succ_contiguous());
delete aps;
return tg; return tg;
} }
std::vector<std::string>* std::vector<std::string>*
extract_aps(spot::twa_graph_ptr& aut, extract_aps(const spot::const_twa_graph_ptr aut,
std::unordered_map<int, int>& ap_binder) std::unordered_map<int, int>& ap_binder)
{ {
std::vector<std::string>* aps = new std::vector<std::string>(); std::vector<std::string>* aps = new std::vector<std::string>();

9
spot/twacube_algos/convert.hh
View file

@ -40,16 +40,15 @@ namespace spot
SPOT_API bdd cube_to_bdd(spot::cube cube, const cubeset& cubeset, SPOT_API bdd cube_to_bdd(spot::cube cube, const cubeset& cubeset,
std::unordered_map<int, int>& reverse_binder); std::unordered_map<int, int>& reverse_binder);
/// \brief Extract the atomic propositions from the automaton /// \brief Extract the atomic propositions from the automaton. This method
/// also fill the binder, i.e. the mapping between BDD indexes to cube indexes
SPOT_API std::vector<std::string>* SPOT_API std::vector<std::string>*
extract_aps(spot::twa_graph_ptr& aut, extract_aps(spot::const_twa_graph_ptr aut,
std::unordered_map<int, int>& ap_binder); std::unordered_map<int, int>& ap_binder);
/// \brief Convert a twa into a twacube /// \brief Convert a twa into a twacube
SPOT_API spot::twacube* SPOT_API spot::twacube*
twa_to_twacube(spot::twa_graph_ptr& aut, twa_to_twacube(spot::const_twa_graph_ptr aut);
std::unordered_map<int, int>& ap_binder,
std::vector<std::string>& aps);
/// \brief Convert a twacube into a twa /// \brief Convert a twacube into a twa
SPOT_API spot::twa_graph_ptr SPOT_API spot::twa_graph_ptr

12
tests/core/twacube.cc
View file

@ -46,29 +46,23 @@ int main()
tg->new_edge(s3, s2, p1 >> p2, 0U); tg->new_edge(s3, s2, p1 >> p2, 0U);
tg->new_edge(s3, s3, bddtrue, spot::acc_cond::mark_t({0, 1})); tg->new_edge(s3, s3, bddtrue, spot::acc_cond::mark_t({0, 1}));
// Map Bdd indexes to cube indexes
std::unordered_map<int, int> ap_binder;
// Get the set of propositions used by this automaton
std::vector<std::string>* aps = extract_aps(tg, ap_binder);
// Test translation // Test translation
auto* aut = twa_to_twacube(tg, ap_binder, *aps); auto* aut = twa_to_twacube(tg);
spot::print_dot(std::cout, tg); spot::print_dot(std::cout, tg);
std::cout << "-----------\n" << *aut << "-----------\n"; std::cout << "-----------\n" << *aut << "-----------\n";
const std::vector<std::string>& aps = aut->get_ap();
unsigned int seed = 17; unsigned int seed = 17;
for (auto it = aut->succ(2); !it->done(); it->next()) for (auto it = aut->succ(2); !it->done(); it->next())
{ {
auto& t = aut->trans_storage(it, seed); auto& t = aut->trans_storage(it, seed);
auto& d = aut->trans_data(it, seed); auto& d = aut->trans_data(it, seed);
std::cout << t.src << ' ' << t.dst << ' ' std::cout << t.src << ' ' << t.dst << ' '
<< ' ' << aut->get_cubeset().dump(d.cube_, *aps) << ' ' << aut->get_cubeset().dump(d.cube_, aps)
<< ' ' << d.acc_ << ' ' << d.acc_
<< std::endl; << std::endl;
} }
spot::print_dot(std::cout, spot::twacube_to_twa(aut)); spot::print_dot(std::cout, spot::twacube_to_twa(aut));
delete aps;
delete aut; delete aut;
} }