alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Define tgba_product_init, a new kind of product with different

Browse source 
initial states.

* src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc
(tgba_product_init): New class.
This commit is contained in:
Alexandre Duret-Lutz 2011-01-04 18:59:24 +01:00
parent f4e583d078
commit 92756e49c8
3 changed files with 40 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

8
ChangeLog
View file

@ -1,3 +1,11 @@
2011-01-04 Alexandre Duret-Lutz <adl@lrde.epita.fr>
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 <adl@lrde.epita.fr> 2011-01-04 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/tgbatest/spotlbtt.test: Add test for -l -R3b, showing many * src/tgbatest/spotlbtt.test: Add test for -l -R3b, showing many

19
src/tgba/tgbaproduct.cc
View file

@ -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). // de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@ -333,4 +333,21 @@ namespace spot
return "<" + left + ", " + right + ">"; 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());
}
} }

14
src/tgba/tgbaproduct.hh
View file

@ -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 // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
@ -161,6 +163,18 @@ namespace spot
tgba_product& operator=(const tgba_product&); 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 #endif // SPOT_TGBA_TGBAPRODUCT_HH