diff --git a/ChangeLog b/ChangeLog index 4cbf8daed..b86a408ee 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,34 @@ +2003-07-15 Alexandre Duret-Lutz + + Homogenize passing of automata as pointers, not references. + Disallow copy for security. + + * src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete): Disallow copy. + * src/tgba/tgbaexplicit.hh (tgba_explicit): Likewise. + * src/tgba/tgbaexplicit.cc (tgba_explicit::operator=, + tgba_explicit::tgba_explicit(tgba_explicit)): Remove. + * src/tgba/tgbabddconcreteproduct.cc + (tgba_bdd_concrete_product_factory::tgba_bdd_concrete_product_factory, + product): Take operand automata as pointers. + * src/tgba/tgbabddconcreteproduct.hh (product): Likewise. + * src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: + (tgba_product): Disallow copy. + (tgba_product::tgba_product): Take operand automata as pointers. + * src/tgbaalgos/dotty.cc (dotty_state, dotty_rec, dotty_reachable): + Take tgba arguments as pointer. + * src/tgbaalgos/dotty.hh (dotty_reachable): Likewise. + * src/tgbaalgos/lbtt.cc (fill_todo, lbtt_reachable): Likewise. + * src/tgbaalgos/lbtt.hh (lbtt_reachable): Likewise. + * src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.hh (ltl_to_tgba): + Likewise. + * src/tgbaalgos/save.cc (save_rec, tgba_save_reachable): Likewise. + * src/tgbaalgos/save.hh (save): Likewise. + * src/tgbatest/explicit.cc, src/tgbatest/explprod.cc, + src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc, + src/tgbatest/mixprod.cc, src/tgbatest/readsave.cc, + src/tgbatest/spotlbtt.cc, src/tgbatest/tgbaread.cc, + src/tgbatest/tripprod.cc: Likewise. + 2003-07-14 Alexandre Duret-Lutz Before this change, all automata would construct their own diff --git a/src/tgba/tgbabddconcrete.hh b/src/tgba/tgbabddconcrete.hh index 788462979..6136f6dd2 100644 --- a/src/tgba/tgbabddconcrete.hh +++ b/src/tgba/tgbabddconcrete.hh @@ -58,6 +58,10 @@ namespace spot protected: tgba_bdd_core_data data_; ///< Core data associated to the automaton. bdd init_; ///< Initial state. + private: + // Disallow copy. + tgba_bdd_concrete(const tgba_bdd_concrete&); + tgba_bdd_concrete& tgba_bdd_concrete::operator=(const tgba_bdd_concrete&); }; } diff --git a/src/tgba/tgbabddconcreteproduct.cc b/src/tgba/tgbabddconcreteproduct.cc index 5a6de7526..0e2368632 100644 --- a/src/tgba/tgbabddconcreteproduct.cc +++ b/src/tgba/tgbabddconcreteproduct.cc @@ -11,15 +11,15 @@ namespace spot class tgba_bdd_product_factory: public tgba_bdd_factory { public: - tgba_bdd_product_factory(const tgba_bdd_concrete& left, - const tgba_bdd_concrete& right) - : dict_(left.get_dict()), + tgba_bdd_product_factory(const tgba_bdd_concrete* left, + const tgba_bdd_concrete* right) + : dict_(left->get_dict()), left_(left), right_(right), - data_(left_.get_core_data(), right_.get_core_data()), - init_(left_.get_init_bdd() & right_.get_init_bdd()) + data_(left_->get_core_data(), right_->get_core_data()), + init_(left_->get_init_bdd() & right_->get_init_bdd()) { - assert(dict_ == right.get_dict()); + assert(dict_ == right->get_dict()); } virtual @@ -47,16 +47,16 @@ namespace spot private: bdd_dict* dict_; - const tgba_bdd_concrete& left_; - const tgba_bdd_concrete& right_; + const tgba_bdd_concrete* left_; + const tgba_bdd_concrete* right_; tgba_bdd_core_data data_; bdd init_; }; - tgba_bdd_concrete - product(const tgba_bdd_concrete& left, const tgba_bdd_concrete& right) + tgba_bdd_concrete* + product(const tgba_bdd_concrete* left, const tgba_bdd_concrete* right) { tgba_bdd_product_factory p(left, right); - return tgba_bdd_concrete(p, p.get_init_state()); + return new tgba_bdd_concrete(p, p.get_init_state()); } } diff --git a/src/tgba/tgbabddconcreteproduct.hh b/src/tgba/tgbabddconcreteproduct.hh index 5ee1ab10b..106dd6561 100644 --- a/src/tgba/tgbabddconcreteproduct.hh +++ b/src/tgba/tgbabddconcreteproduct.hh @@ -9,8 +9,8 @@ namespace spot /// /// This function build the resulting product, as another /// tgba::tgba_bdd_concrete automaton. - tgba_bdd_concrete - product(const tgba_bdd_concrete& left, const tgba_bdd_concrete& right); + tgba_bdd_concrete* + product(const tgba_bdd_concrete* left, const tgba_bdd_concrete* right); } #endif // SPOT_TGBA_TGBABDDCONCRETEPRODUCT_HH diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index d74c56963..e6e31be20 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -87,31 +87,6 @@ namespace spot { } - tgba_explicit::tgba_explicit(const tgba_explicit& other) - : tgba(), - name_state_map_(other.name_state_map_), - state_name_map_(other.state_name_map_), - dict_(other.dict_), - init_(other.init_), - all_accepting_conditions_(other.all_accepting_conditions_), - neg_accepting_conditions_(other.neg_accepting_conditions_), - all_accepting_conditions_computed_(other. - all_accepting_conditions_computed_) - { - dict_->register_all_variables_of(&other, this); - } - - tgba_explicit& - tgba_explicit::operator=(const tgba_explicit& other) - { - if (&other != this) - { - this->~tgba_explicit(); - new (this) tgba_explicit(other); - } - return *this; - } - tgba_explicit::~tgba_explicit() { ns_map::iterator i; diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index c14b831fe..14f0d8423 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -17,8 +17,6 @@ namespace spot { public: tgba_explicit(bdd_dict* dict); - tgba_explicit(const tgba_explicit& other); - tgba_explicit& tgba_explicit::operator=(const tgba_explicit& other); struct transition; typedef std::list state; @@ -65,6 +63,11 @@ namespace spot mutable bdd all_accepting_conditions_; bdd neg_accepting_conditions_; mutable bool all_accepting_conditions_computed_; + + private: + // Disallow copy. + tgba_explicit(const tgba_explicit& other); + tgba_explicit& tgba_explicit::operator=(const tgba_explicit& other); }; diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc index 8cd41abbf..5d90d2984 100644 --- a/src/tgba/tgbaproduct.cc +++ b/src/tgba/tgbaproduct.cc @@ -143,10 +143,10 @@ namespace spot //////////////////////////////////////////////////////////// // tgba_product - tgba_product::tgba_product(const tgba& left, const tgba& right) - : dict_(left.get_dict()), left_(&left), right_(&right) + tgba_product::tgba_product(const tgba* left, const tgba* right) + : dict_(left->get_dict()), left_(left), right_(right) { - assert(dict_ == right.get_dict()); + assert(dict_ == right->get_dict()); all_accepting_conditions_ = ((left_->all_accepting_conditions() & right_->neg_accepting_conditions()) diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh index 54cef2929..9da14ca5d 100644 --- a/src/tgba/tgbaproduct.hh +++ b/src/tgba/tgbaproduct.hh @@ -87,14 +87,14 @@ namespace spot }; /// \brief A lazy product. (States are computed on the fly.) - class tgba_product : public tgba + class tgba_product: public tgba { public: /// \brief Constructor. /// \param left The left automata in the product. /// \param right The right automata in the product. /// Do not be fooled by these arguments: a product is commutative. - tgba_product(const tgba& left, const tgba& right); + tgba_product(const tgba* left, const tgba* right); virtual ~tgba_product(); @@ -116,6 +116,9 @@ namespace spot const tgba* right_; bdd all_accepting_conditions_; bdd neg_accepting_conditions_; + // Disallow copy. + tgba_product(const tgba_product&); + tgba_product& tgba_product::operator=(const tgba_product&); }; } diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index e5b49e139..46c6c3431 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -10,7 +10,7 @@ namespace spot /// Output and record a state. static bool dotty_state(std::ostream& os, - const tgba& g, state* st, seen_map& m, int& node) + const tgba* g, state* st, seen_map& m, int& node) { seen_map::iterator i = m.find(st); @@ -25,24 +25,24 @@ namespace spot m[st] = node; os << " " << node << " [label=\"" - << g.format_state(st) << "\"]" << std::endl; + << g->format_state(st) << "\"]" << std::endl; return true; } /// Process successors. static void dotty_rec(std::ostream& os, - const tgba& g, state* st, seen_map& m, int father) + const tgba* g, state* st, seen_map& m, int father) { - tgba_succ_iterator* si = g.succ_iter(st); + tgba_succ_iterator* si = g->succ_iter(st); for (si->first(); !si->done(); si->next()) { int node; state* s = si->current_state(); bool recurse = dotty_state(os, g, s, m, node); os << " " << father << " -> " << node << " [label=\""; - bdd_print_set(os, g.get_dict(), si->current_condition()) << "\\n"; - bdd_print_set(os, g.get_dict(), si->current_accepting_conditions()) + bdd_print_set(os, g->get_dict(), si->current_condition()) << "\\n"; + bdd_print_set(os, g->get_dict(), si->current_accepting_conditions()) << "\"]" << std::endl; if (recurse) { @@ -58,10 +58,10 @@ namespace spot } std::ostream& - dotty_reachable(std::ostream& os, const tgba& g) + dotty_reachable(std::ostream& os, const tgba* g) { seen_map m; - state* state = g.get_init_state(); + state* state = g->get_init_state(); os << "digraph G {" << std::endl; os << " size=\"7.26,10.69\"" << std::endl; os << " 0 [label=\"\", style=invis]" << std::endl; diff --git a/src/tgbaalgos/dotty.hh b/src/tgbaalgos/dotty.hh index 5f87bad0b..395349b8f 100644 --- a/src/tgbaalgos/dotty.hh +++ b/src/tgbaalgos/dotty.hh @@ -7,7 +7,7 @@ namespace spot { /// \brief Print reachable states in dot format. - std::ostream& dotty_reachable(std::ostream& os, const tgba& g); + std::ostream& dotty_reachable(std::ostream& os, const tgba* g); } #endif // SPOT_TGBAALGOS_DOTTY_HH diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index 9736b34be..9712af113 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -130,7 +130,7 @@ namespace spot // a supplementary state, to act as initial state for LBTT.) void fill_todo(todo_set& todo, seen_map& seen, acp_seen_map& acp_seen, - state* state, const tgba& g, + state* state, const tgba* g, minmax_pair& mmp, unsigned& state_number, bool init) { @@ -147,7 +147,7 @@ namespace spot // Browse the successors of STATE to gather accepting // conditions of outgoing transitions. bdd_set acc_seen; - tgba_succ_iterator* si = g.succ_iter(state); + tgba_succ_iterator* si = g->succ_iter(state); for (si->first(); !si->done(); si->next()) { acc_seen.insert(si->current_accepting_conditions()); @@ -176,9 +176,9 @@ namespace spot } std::ostream& - lbtt_reachable(std::ostream& os, const tgba& g) + lbtt_reachable(std::ostream& os, const tgba* g) { - const bdd_dict* d = g.get_dict(); + const bdd_dict* d = g->get_dict(); std::ostringstream body; seen_map seen; @@ -189,8 +189,8 @@ namespace spot minmax_pair mmp; fill_todo(todo, seen, acp_seen, - g.get_init_state(), g, mmp, state_number, true); - accepting_cond_splitter acs(g.all_accepting_conditions()); + g->get_init_state(), g, mmp, state_number, true); + accepting_cond_splitter acs(g->all_accepting_conditions()); while(! todo.empty()) { @@ -209,7 +209,7 @@ namespace spot acs.split(body, sap.second); body << "-1" << std::endl; - tgba_succ_iterator* si = g.succ_iter(sap.first); + tgba_succ_iterator* si = g->succ_iter(sap.first); for (si->first(); !si->done(); si->next()) { // We have put the accepting conditions on the state, diff --git a/src/tgbaalgos/lbtt.hh b/src/tgbaalgos/lbtt.hh index a8442b4cf..11eb3243c 100644 --- a/src/tgbaalgos/lbtt.hh +++ b/src/tgbaalgos/lbtt.hh @@ -28,7 +28,7 @@ namespace spot /// /// \param g The automata to print. /// \param os Where to print. - std::ostream& lbtt_reachable(std::ostream& os, const tgba& g); + std::ostream& lbtt_reachable(std::ostream& os, const tgba* g); } #endif // SPOT_TGBAALGOS_LBTT_HH diff --git a/src/tgbaalgos/ltl2tgba.cc b/src/tgbaalgos/ltl2tgba.cc index a48f48158..8934f5e62 100644 --- a/src/tgbaalgos/ltl2tgba.cc +++ b/src/tgbaalgos/ltl2tgba.cc @@ -230,7 +230,7 @@ namespace spot bool root_; }; - tgba_bdd_concrete + tgba_bdd_concrete* ltl_to_tgba(const ltl::formula* f, bdd_dict* dict) { // Normalize the formula. We want all the negations on @@ -249,7 +249,6 @@ namespace spot fact.finish(); // Finally setup the resulting automaton. - tgba_bdd_concrete g(fact, v.result()); - return g; + return new tgba_bdd_concrete(fact, v.result()); } } diff --git a/src/tgbaalgos/ltl2tgba.hh b/src/tgbaalgos/ltl2tgba.hh index 7e7c682b8..3b38bf12e 100644 --- a/src/tgbaalgos/ltl2tgba.hh +++ b/src/tgbaalgos/ltl2tgba.hh @@ -7,7 +7,7 @@ namespace spot { /// Build a spot::tgba_bdd_concrete from an LTL formula. - tgba_bdd_concrete ltl_to_tgba(const ltl::formula* f, bdd_dict* dict); + tgba_bdd_concrete* ltl_to_tgba(const ltl::formula* f, bdd_dict* dict); } #endif // SPOT_TGBA_LTL2TGBA_HH diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc index 4d28b1883..735983835 100644 --- a/src/tgbaalgos/save.cc +++ b/src/tgbaalgos/save.cc @@ -10,18 +10,18 @@ namespace spot /// Process successors. static void - save_rec(std::ostream& os, const tgba& g, state* st, seen_set& m) + save_rec(std::ostream& os, const tgba* g, state* st, seen_set& m) { m.insert(st); - std::string cur = g.format_state(st); - tgba_succ_iterator* si = g.succ_iter(st); + std::string cur = g->format_state(st); + tgba_succ_iterator* si = g->succ_iter(st); for (si->first(); !si->done(); si->next()) { state* s = si->current_state(); - os << "\"" << cur << "\", \"" << g.format_state(s) << "\", "; + os << "\"" << cur << "\", \"" << g->format_state(s) << "\", "; - bdd_print_sat(os, g.get_dict(), si->current_condition()) << ","; - bdd_print_acc(os, g.get_dict(), si->current_accepting_conditions()) + bdd_print_sat(os, g->get_dict(), si->current_condition()) << ","; + bdd_print_acc(os, g->get_dict(), si->current_accepting_conditions()) << ";" << std::endl; // Destination already explored? @@ -40,9 +40,9 @@ namespace spot } std::ostream& - tgba_save_reachable(std::ostream& os, const tgba& g) + tgba_save_reachable(std::ostream& os, const tgba* g) { - const bdd_dict* d = g.get_dict(); + const bdd_dict* d = g->get_dict(); os << "acc ="; for (bdd_dict::fv_map::const_iterator ai = d->acc_map.begin(); ai != d->acc_map.end(); ++ai) @@ -53,7 +53,7 @@ namespace spot os << ";" << std::endl; seen_set m; - state* state = g.get_init_state(); + state* state = g->get_init_state(); save_rec(os, g, state, m); // Finally delete all states used as keys in m: for (seen_set::iterator i = m.begin(); i != m.end(); ++i) diff --git a/src/tgbaalgos/save.hh b/src/tgbaalgos/save.hh index 8bba79908..e00cfc100 100644 --- a/src/tgbaalgos/save.hh +++ b/src/tgbaalgos/save.hh @@ -7,7 +7,7 @@ namespace spot { /// \brief Save reachable states in text format. - std::ostream& tgba_save_reachable(std::ostream& os, const tgba& g); + std::ostream& tgba_save_reachable(std::ostream& os, const tgba* g); } #endif // SPOT_TGBAALGOS_SAVE_HH diff --git a/src/tgbatest/explicit.cc b/src/tgbatest/explicit.cc index 7a836e132..bf493f3bd 100644 --- a/src/tgbatest/explicit.cc +++ b/src/tgbatest/explicit.cc @@ -29,7 +29,7 @@ main() a->add_accepting_condition(t1, e.require("q")); a->add_accepting_condition(t2, e.require("r")); - spot::dotty_reachable(std::cout, *a); + spot::dotty_reachable(std::cout, a); delete a; delete dict; diff --git a/src/tgbatest/explprod.cc b/src/tgbatest/explprod.cc index 719da7d52..1d7c32229 100644 --- a/src/tgbatest/explprod.cc +++ b/src/tgbatest/explprod.cc @@ -35,8 +35,8 @@ main(int argc, char** argv) return 2; { - spot::tgba_product p(*a1, *a2); - spot::tgba_save_reachable(std::cout, p); + spot::tgba_product p(a1, a2); + spot::tgba_save_reachable(std::cout, &p); } assert(spot::ltl::unop::instance_count() == 0); diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 97af56acc..95e818ef1 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -88,7 +88,7 @@ main(int argc, char** argv) spot::bdd_dict* dict = new spot::bdd_dict(); if (f) { - spot::tgba_bdd_concrete a = spot::ltl_to_tgba(f, dict); + spot::tgba_bdd_concrete* a = spot::ltl_to_tgba(f, dict); spot::ltl::destroy(f); switch (output) { @@ -96,23 +96,23 @@ main(int argc, char** argv) spot::dotty_reachable(std::cout, a); break; case 1: - spot::bdd_print_dot(std::cout, a.get_dict(), - a.get_core_data().relation); + spot::bdd_print_dot(std::cout, a->get_dict(), + a->get_core_data().relation); break; case 2: - spot::bdd_print_dot(std::cout, a.get_dict(), - a.get_core_data().accepting_conditions); + spot::bdd_print_dot(std::cout, a->get_dict(), + a->get_core_data().accepting_conditions); break; case 3: - spot::bdd_print_set(std::cout, a.get_dict(), - a.get_core_data().relation); + spot::bdd_print_set(std::cout, a->get_dict(), + a->get_core_data().relation); break; case 4: - spot::bdd_print_set(std::cout, a.get_dict(), - a.get_core_data().accepting_conditions); + spot::bdd_print_set(std::cout, a->get_dict(), + a->get_core_data().accepting_conditions); break; case 5: - a.get_dict()->dump(std::cout); + a->get_dict()->dump(std::cout); break; case 6: spot::lbtt_reachable(std::cout, a); @@ -120,6 +120,7 @@ main(int argc, char** argv) default: assert(!"unknown output option"); } + delete a; } else { diff --git a/src/tgbatest/ltlprod.cc b/src/tgbatest/ltlprod.cc index 556c95124..572830dbb 100644 --- a/src/tgbatest/ltlprod.cc +++ b/src/tgbatest/ltlprod.cc @@ -39,18 +39,20 @@ main(int argc, char** argv) spot::bdd_dict* dict = new spot::bdd_dict(); { - spot::tgba_bdd_concrete a1 = spot::ltl_to_tgba(f1, dict); - spot::tgba_bdd_concrete a2 = spot::ltl_to_tgba(f2, dict); + spot::tgba_bdd_concrete* a1 = spot::ltl_to_tgba(f1, dict); + spot::tgba_bdd_concrete* a2 = spot::ltl_to_tgba(f2, dict); spot::ltl::destroy(f1); spot::ltl::destroy(f2); #ifdef BDD_CONCRETE_PRODUCT - spot::tgba_bdd_concrete p = spot::product(a1, a2); + spot::tgba_bdd_concrete* p = spot::product(a1, a2); #else - spot::tgba_product p(a1, a2); + spot::tgba_product* p = new spot::tgba_product(a1, a2); #endif - spot::dotty_reachable(std::cout, p); + delete p; + delete a1; + delete a2; } assert(spot::ltl::atomic_prop::instance_count() == 0); diff --git a/src/tgbatest/mixprod.cc b/src/tgbatest/mixprod.cc index 3125452e0..396254621 100644 --- a/src/tgbatest/mixprod.cc +++ b/src/tgbatest/mixprod.cc @@ -39,11 +39,11 @@ main(int argc, char** argv) return 2; { - spot::tgba_bdd_concrete a1 = spot::ltl_to_tgba(f1, dict); + spot::tgba_bdd_concrete* a1 = spot::ltl_to_tgba(f1, dict); spot::ltl::destroy(f1); - spot::tgba_product p(a1, *a2); - - spot::tgba_save_reachable(std::cout, p); + spot::tgba_product p(a1, a2); + spot::tgba_save_reachable(std::cout, &p); + delete a1; } assert(spot::ltl::unop::instance_count() == 0); diff --git a/src/tgbatest/readsave.cc b/src/tgbatest/readsave.cc index c8bb52674..4f49c62b1 100644 --- a/src/tgbatest/readsave.cc +++ b/src/tgbatest/readsave.cc @@ -43,7 +43,7 @@ main(int argc, char** argv) if (a) { - spot::tgba_save_reachable(std::cout, *a); + spot::tgba_save_reachable(std::cout, a); delete a; } else diff --git a/src/tgbatest/spotlbtt.cc b/src/tgbatest/spotlbtt.cc index 3e471836d..48e498c2d 100644 --- a/src/tgbatest/spotlbtt.cc +++ b/src/tgbatest/spotlbtt.cc @@ -48,9 +48,10 @@ main(int argc, char** argv) if (f) { - spot::tgba_bdd_concrete a = spot::ltl_to_tgba(f, dict); + spot::tgba_bdd_concrete* a = spot::ltl_to_tgba(f, dict); spot::ltl::destroy(f); spot::lbtt_reachable(std::cout, a); + delete a; } else { diff --git a/src/tgbatest/tgbaread.cc b/src/tgbatest/tgbaread.cc index 3408775cb..d22a32fa4 100644 --- a/src/tgbatest/tgbaread.cc +++ b/src/tgbatest/tgbaread.cc @@ -43,7 +43,7 @@ main(int argc, char** argv) if (a) { - spot::dotty_reachable(std::cout, *a); + spot::dotty_reachable(std::cout, a); delete a; } else diff --git a/src/tgbatest/tripprod.cc b/src/tgbatest/tripprod.cc index f9fa6eab8..2004ab2b1 100644 --- a/src/tgbatest/tripprod.cc +++ b/src/tgbatest/tripprod.cc @@ -39,9 +39,9 @@ main(int argc, char** argv) return 2; { - spot::tgba_product p(*a1, *a2); - spot::tgba_product p2(p, *a3); - spot::tgba_save_reachable(std::cout, p2); + spot::tgba_product p(a1, a2); + spot::tgba_product p2(&p, a3); + spot::tgba_save_reachable(std::cout, &p2); } assert(spot::ltl::unop::instance_count() == 0);