diff --git a/iface/ltsmin/finite.test b/iface/ltsmin/finite.test index 05be4e4a819667edfb5abe92bf59066769617713..bede9bc0c41e176d3d4683eae3557802c428bec2 100755 --- a/iface/ltsmin/finite.test +++ b/iface/ltsmin/finite.test @@ -54,5 +54,5 @@ run 0 ../modelcheck -ddead -e $srcdir/finite.dve \ '!(G(dead -> ("P.a==2" | "P.b==3")))' # This used to segfault because of a bug in -# tgba_product::transition_annotation. +# twa_product::transition_annotation. run 0 ../modelcheck -gp $srcdir/finite.dve true diff --git a/src/ta/tgtaproduct.cc b/src/ta/tgtaproduct.cc index 068baec51a64f979fb2fbb4554529a76fff8d7e7..4b4157c0ae8d0c6a26b3b2b39beb45b8a80418c9 100644 --- a/src/ta/tgtaproduct.cc +++ b/src/ta/tgtaproduct.cc @@ -45,7 +45,7 @@ namespace spot tgta_product::tgta_product(const const_kripke_ptr& left, const const_tgta_ptr& right): - tgba_product(left, right) + twa_product(left, right) { } diff --git a/src/ta/tgtaproduct.hh b/src/ta/tgtaproduct.hh index b91b9125ca7ba7bbf025534b2bfd14d3e1ce06bf..9620abff69fc41f916c53629308697f79541b36c 100644 --- a/src/ta/tgtaproduct.hh +++ b/src/ta/tgtaproduct.hh @@ -29,7 +29,7 @@ namespace spot { /// \brief A lazy product. (States are computed on the fly.) - class SPOT_API tgta_product : public tgba_product + class SPOT_API tgta_product : public twa_product { public: tgta_product(const const_kripke_ptr& left, diff --git a/src/tgba/fwd.hh b/src/tgba/fwd.hh index c3b588d0bdcd7c9e454fc7e043f95e3c753dfa56..40ce575d3f211c9192ed07b3fd85cf7e855eea6a 100644 --- a/src/tgba/fwd.hh +++ b/src/tgba/fwd.hh @@ -31,7 +31,7 @@ namespace spot typedef std::shared_ptr const_twa_graph_ptr; typedef std::shared_ptr twa_graph_ptr; - class tgba_product; - typedef std::shared_ptr const_tgba_product_ptr; - typedef std::shared_ptr tgba_product_ptr; + class twa_product; + typedef std::shared_ptr const_twa_product_ptr; + typedef std::shared_ptr twa_product_ptr; } diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc index d5f11c4cc322c442301981deb36e9d0641f2017c..f53813d614f567e2e86cfb3b15f3214af246db8f 100644 --- a/src/tgba/tgbaproduct.cc +++ b/src/tgba/tgbaproduct.cc @@ -84,7 +84,7 @@ namespace spot public: tgba_succ_iterator_product_common(tgba_succ_iterator* left, tgba_succ_iterator* right, - const tgba_product* prod, + const twa_product* prod, fixed_size_pool* pool) : left_(left), right_(right), prod_(prod), pool_(pool) { @@ -140,9 +140,9 @@ namespace spot protected: tgba_succ_iterator* left_; tgba_succ_iterator* right_; - const tgba_product* prod_; + const twa_product* prod_; fixed_size_pool* pool_; - friend class spot::tgba_product; + friend class spot::twa_product; }; @@ -152,7 +152,7 @@ namespace spot public: tgba_succ_iterator_product(tgba_succ_iterator* left, tgba_succ_iterator* right, - const tgba_product* prod, + const twa_product* prod, fixed_size_pool* pool) : tgba_succ_iterator_product_common(left, right, prod, pool) { @@ -222,7 +222,7 @@ namespace spot public: tgba_succ_iterator_product_kripke(tgba_succ_iterator* left, tgba_succ_iterator* right, - const tgba_product* prod, + const twa_product* prod, fixed_size_pool* pool) : tgba_succ_iterator_product_common(left, right, prod, pool) { @@ -280,9 +280,9 @@ namespace spot } // anonymous //////////////////////////////////////////////////////////// - // tgba_product + // twa_product - tgba_product::tgba_product(const const_tgba_ptr& left, + twa_product::twa_product(const const_tgba_ptr& left, const const_tgba_ptr& right) : twa(left->get_dict()), left_(left), right_(right), pool_(sizeof(state_product)) @@ -318,7 +318,7 @@ namespace spot set_acceptance(left_num + right->acc().num_sets(), right_acc); } - tgba_product::~tgba_product() + twa_product::~twa_product() { get_dict()->unregister_all_my_variables(this); // Prevent these states from being destroyed by ~tgba(): they @@ -331,7 +331,7 @@ namespace spot } state* - tgba_product::get_init_state() const + twa_product::get_init_state() const { fixed_size_pool* p = const_cast(&pool_); return new(p->allocate()) state_product(left_->get_init_state(), @@ -339,7 +339,7 @@ namespace spot } tgba_succ_iterator* - tgba_product::succ_iter(const state* state) const + twa_product::succ_iter(const state* state) const { const state_product* s = down_cast(state); assert(s); @@ -363,7 +363,7 @@ namespace spot } bdd - tgba_product::compute_support_conditions(const state* in) const + twa_product::compute_support_conditions(const state* in) const { const state_product* s = down_cast(in); assert(s); @@ -372,18 +372,18 @@ namespace spot return lsc & rsc; } - const acc_cond& tgba_product::left_acc() const + const acc_cond& twa_product::left_acc() const { return left_->acc(); } - const acc_cond& tgba_product::right_acc() const + const acc_cond& twa_product::right_acc() const { return right_->acc(); } std::string - tgba_product::format_state(const state* state) const + twa_product::format_state(const state* state) const { const state_product* s = down_cast(state); assert(s); @@ -393,7 +393,7 @@ namespace spot } state* - tgba_product::project_state(const state* s, const const_tgba_ptr& t) const + twa_product::project_state(const state* s, const const_tgba_ptr& t) const { const state_product* s2 = down_cast(s); assert(s2); @@ -406,7 +406,7 @@ namespace spot } std::string - tgba_product::transition_annotation(const tgba_succ_iterator* t) const + twa_product::transition_annotation(const tgba_succ_iterator* t) const { const tgba_succ_iterator_product_common* i = down_cast(t); @@ -421,13 +421,13 @@ namespace spot } ////////////////////////////////////////////////////////////////////// - // tgba_product_init + // twa_product_init - tgba_product_init::tgba_product_init(const const_tgba_ptr& left, + twa_product_init::twa_product_init(const const_tgba_ptr& left, const const_tgba_ptr& right, const state* left_init, const state* right_init) - : tgba_product(left, right), + : twa_product(left, right), left_init_(left_init), right_init_(right_init) { if (left_ != left) @@ -435,7 +435,7 @@ namespace spot } state* - tgba_product_init::get_init_state() const + twa_product_init::get_init_state() const { fixed_size_pool* p = const_cast(&pool_); return new(p->allocate()) state_product(left_init_->clone(), diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh index 278b759ede3dc21326e044d81bfac79e1660f41c..8d5c0fc2ef9bc4ca9f04ef50e162dc9ada7ee8f0 100644 --- a/src/tgba/tgbaproduct.hh +++ b/src/tgba/tgbaproduct.hh @@ -29,7 +29,7 @@ namespace spot { /// \ingroup tgba_on_the_fly_algorithms - /// \brief A state for spot::tgba_product. + /// \brief A state for spot::twa_product. /// /// This state is in fact a pair of state: the state from the left /// automaton and that of the right. @@ -77,16 +77,16 @@ namespace spot /// \brief A lazy product. (States are computed on the fly.) - class SPOT_API tgba_product: public twa + class SPOT_API twa_product: public twa { 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 const_tgba_ptr& left, const const_tgba_ptr& right); + twa_product(const const_tgba_ptr& left, const const_tgba_ptr& right); - virtual ~tgba_product(); + virtual ~twa_product(); virtual state* get_init_state() const; @@ -114,15 +114,15 @@ namespace spot private: // Disallow copy. - tgba_product(const tgba_product&) SPOT_DELETED; - tgba_product& operator=(const tgba_product&) SPOT_DELETED; + twa_product(const twa_product&) SPOT_DELETED; + twa_product& operator=(const twa_product&) SPOT_DELETED; }; /// \brief A lazy product with different initial states. - class SPOT_API tgba_product_init final: public tgba_product + class SPOT_API twa_product_init final: public twa_product { public: - tgba_product_init(const const_tgba_ptr& left, const const_tgba_ptr& right, + twa_product_init(const const_tgba_ptr& left, const const_tgba_ptr& right, const state* left_init, const state* right_init); virtual state* get_init_state() const; protected: @@ -131,19 +131,19 @@ namespace spot }; /// \brief on-the-fly TGBA product - inline tgba_product_ptr otf_product(const const_tgba_ptr& left, + inline twa_product_ptr otf_product(const const_tgba_ptr& left, const const_tgba_ptr& right) { - return std::make_shared(left, right); + return std::make_shared(left, right); } /// \brief on-the-fly TGBA product with forced initial states - inline tgba_product_ptr otf_product_at(const const_tgba_ptr& left, + inline twa_product_ptr otf_product_at(const const_tgba_ptr& left, const const_tgba_ptr& right, const state* left_init, const state* right_init) { - return std::make_shared(left, right, + return std::make_shared(left, right, left_init, right_init); } } diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index 3e195ea6337f53f091ef9bd54104cc311f4cc43a..8da2a67febaa16d1b915878d588c925df7a5257e 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -50,8 +50,8 @@ %shared_ptr(spot::bdd_dict) %shared_ptr(spot::twa) %shared_ptr(spot::twa_graph) -%shared_ptr(spot::tgba_product) -%shared_ptr(spot::tgba_product_init) +%shared_ptr(spot::twa_product) +%shared_ptr(spot::twa_product_init) %shared_ptr(spot::taa_tgba) %shared_ptr(spot::taa_tgba_string) %shared_ptr(spot::taa_tgba_formula)