diff --git a/ChangeLog b/ChangeLog index 43070a7d8..46d762d73 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2011-01-04 Alexandre Duret-Lutz + + Define tgba_product_init, a new kind of product with different + initial states. + + * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc + (tgba_product_init): New class. + 2011-01-04 Alexandre Duret-Lutz * src/tgbatest/spotlbtt.test: Add test for -l -R3b, showing many diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc index 6b4b6387d..dd502796a 100644 --- a/src/tgba/tgbaproduct.cc +++ b/src/tgba/tgbaproduct.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -333,4 +333,21 @@ namespace spot return "<" + left + ", " + right + ">"; } + ////////////////////////////////////////////////////////////////////// + // tgba_product_init + + tgba_product_init::tgba_product_init(const tgba* left, const tgba* right, + const state* left_init, + const state* right_init) + : tgba_product(left, right), + left_init_(left_init), right_init_(right_init) + { + } + + state* + tgba_product_init::get_init_state() const + { + return new state_product(left_init_->clone(), right_init_->clone()); + } + } diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh index 8d8ad79cb..2f1139ae6 100644 --- a/src/tgba/tgbaproduct.hh +++ b/src/tgba/tgbaproduct.hh @@ -1,3 +1,5 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -161,6 +163,18 @@ namespace spot tgba_product& operator=(const tgba_product&); }; + /// \brief A lazy product with different initial states. + class tgba_product_init: public tgba_product + { + public: + tgba_product_init(const tgba* left, const tgba* right, + const state* left_init, const state* right_init); + virtual state* get_init_state() const; + private: + const state* left_init_; + const state* right_init_; + }; + } #endif // SPOT_TGBA_TGBAPRODUCT_HH