Commit fc1d8e50 authored by Etienne Renault's avatar Etienne Renault

twacube_to_twa: allows use of existing BDD_dict

* spot/twacube_algos/convert.cc,
spot/twacube_algos/convert.hh: Here.
* tests/core/twacube.cc: Test it.
parent f38f7f3a
Pipeline #19086 passed with stage
in 171 minutes and 56 seconds
...@@ -134,14 +134,15 @@ namespace spot ...@@ -134,14 +134,15 @@ namespace spot
} }
spot::twa_graph_ptr spot::twa_graph_ptr
twacube_to_twa(spot::twacube_ptr twacube) twacube_to_twa(spot::twacube_ptr twacube, spot::bdd_dict_ptr d)
{ {
// Grab necessary variables // Grab necessary variables
auto& theg = twacube->get_graph(); auto& theg = twacube->get_graph();
spot::cubeset cs = twacube->get_cubeset(); spot::cubeset cs = twacube->get_cubeset();
// Build the resulting graph // Build the resulting graph
auto d = spot::make_bdd_dict(); if (d == nullptr)
d = spot::make_bdd_dict();
auto res = make_twa_graph(d); auto res = make_twa_graph(d);
// Fix the acceptance of the resulting automaton // Fix the acceptance of the resulting automaton
......
...@@ -50,9 +50,12 @@ namespace spot ...@@ -50,9 +50,12 @@ namespace spot
SPOT_API twacube_ptr SPOT_API twacube_ptr
twa_to_twacube(spot::const_twa_graph_ptr aut); twa_to_twacube(spot::const_twa_graph_ptr aut);
/// \brief Convert a twacube into a twa /// \brief Convert a twacube into a twa.
/// When \d is specified, the BDD_dict in parameter is used rather than
/// creating a new one.
SPOT_API spot::twa_graph_ptr SPOT_API spot::twa_graph_ptr
twacube_to_twa(spot::twacube_ptr twacube); twacube_to_twa(spot::twacube_ptr twacube,
spot::bdd_dict_ptr d = nullptr);
/// \brief Check wether a twacube and a twa are equivalent /// \brief Check wether a twacube and a twa are equivalent
SPOT_API bool are_equivalent(const spot::twacube_ptr twacube, SPOT_API bool are_equivalent(const spot::twacube_ptr twacube,
......
...@@ -44,8 +44,10 @@ static void checkit(std::string f_str) ...@@ -44,8 +44,10 @@ static void checkit(std::string f_str)
auto propcube = spot::twa_to_twacube(prop); auto propcube = spot::twa_to_twacube(prop);
assert(spot::are_equivalent(propcube, prop)); assert(spot::are_equivalent(propcube, prop));
auto propcubeback = spot::twacube_to_twa(propcube); auto propcubeback = spot::twacube_to_twa(propcube, dict);
assert(spot::are_equivalent(propcube, propcubeback)); assert(spot::are_equivalent(propcube, propcubeback));
assert(spot::are_equivalent(prop, propcubeback));
} }
int main() int main()
......
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