* src/tgbaalgos/lbtt.cc (bdd_less_than): Move ...
* src/misc/bddlt.hh: ... in this new file. * src/misc/Makefile.am (misc_HEADERS): Add bddlt.hh.
This commit is contained in:
parent
d0a7a3ab54
commit
5bc2d77e60
4 changed files with 25 additions and 9 deletions
|
|
@ -1,5 +1,9 @@
|
||||||
2003-07-25 Alexandre Duret-Lutz <aduret@src.lip6.fr>
|
2003-07-25 Alexandre Duret-Lutz <aduret@src.lip6.fr>
|
||||||
|
|
||||||
|
* src/tgbaalgos/lbtt.cc (bdd_less_than): Move ...
|
||||||
|
* src/misc/bddlt.hh: ... in this new file.
|
||||||
|
* src/misc/Makefile.am (misc_HEADERS): Add bddlt.hh.
|
||||||
|
|
||||||
* iface/gspn/dcswave.test: Comment state space sizes.
|
* iface/gspn/dcswave.test: Comment state space sizes.
|
||||||
|
|
||||||
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS): Add reachiters.hh.
|
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS): Add reachiters.hh.
|
||||||
|
|
|
||||||
|
|
@ -5,6 +5,7 @@ miscdir = $(pkgincludedir)/misc
|
||||||
|
|
||||||
misc_HEADERS = \
|
misc_HEADERS = \
|
||||||
bddalloc.hh \
|
bddalloc.hh \
|
||||||
|
bddlt.hh \
|
||||||
const_sel.hh
|
const_sel.hh
|
||||||
|
|
||||||
noinst_LTLIBRARIES = libmisc.la
|
noinst_LTLIBRARIES = libmisc.la
|
||||||
|
|
|
||||||
19
src/misc/bddlt.hh
Normal file
19
src/misc/bddlt.hh
Normal file
|
|
@ -0,0 +1,19 @@
|
||||||
|
#ifndef SPOT_MISC_BDDLT_HH
|
||||||
|
# define SPOT_MISC_BDDLT_HH
|
||||||
|
|
||||||
|
# include <bdd.h>
|
||||||
|
|
||||||
|
namespace spot
|
||||||
|
{
|
||||||
|
/// Comparison functor for BDDs.
|
||||||
|
struct bdd_less_than
|
||||||
|
{
|
||||||
|
bool
|
||||||
|
operator()(const bdd& left, const bdd& right) const
|
||||||
|
{
|
||||||
|
return left.id() < right.id();
|
||||||
|
}
|
||||||
|
};
|
||||||
|
}
|
||||||
|
|
||||||
|
#endif // SPOT_MISC_BDDLT_HH
|
||||||
|
|
@ -7,18 +7,10 @@
|
||||||
#include "tgba/bddprint.hh"
|
#include "tgba/bddprint.hh"
|
||||||
#include "ltlvisit/tostring.hh"
|
#include "ltlvisit/tostring.hh"
|
||||||
#include "tgba/bddprint.hh"
|
#include "tgba/bddprint.hh"
|
||||||
|
#include "misc/bddlt.hh"
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
struct bdd_less_than
|
|
||||||
{
|
|
||||||
bool
|
|
||||||
operator()(const bdd& left, const bdd& right) const
|
|
||||||
{
|
|
||||||
return left.id() < right.id();
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
// At some point we'll need to print an accepting set into LBTT's
|
// At some point we'll need to print an accepting set into LBTT's
|
||||||
// forma. LBTT expect numbered accepting sets, so first we'll
|
// forma. LBTT expect numbered accepting sets, so first we'll
|
||||||
// number each accepting condition, and latter when we have to print
|
// number each accepting condition, and latter when we have to print
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue