diff --git a/spot/twacube_algos/convert.cc b/spot/twacube_algos/convert.cc index ba84ce46e..e49194b90 100644 --- a/spot/twacube_algos/convert.cc +++ b/spot/twacube_algos/convert.cc @@ -134,14 +134,15 @@ namespace spot } 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 auto& theg = twacube->get_graph(); spot::cubeset cs = twacube->get_cubeset(); // Build the resulting graph - auto d = spot::make_bdd_dict(); + if (d == nullptr) + d = spot::make_bdd_dict(); auto res = make_twa_graph(d); // Fix the acceptance of the resulting automaton diff --git a/spot/twacube_algos/convert.hh b/spot/twacube_algos/convert.hh index bdcfc7155..f21aaec3f 100644 --- a/spot/twacube_algos/convert.hh +++ b/spot/twacube_algos/convert.hh @@ -50,9 +50,12 @@ namespace spot SPOT_API twacube_ptr 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 - 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 SPOT_API bool are_equivalent(const spot::twacube_ptr twacube, diff --git a/tests/core/twacube.cc b/tests/core/twacube.cc index 08333cc4e..31eeaed69 100644 --- a/tests/core/twacube.cc +++ b/tests/core/twacube.cc @@ -44,8 +44,10 @@ static void checkit(std::string f_str) auto propcube = spot::twa_to_twacube(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(prop, propcubeback)); } int main()