diff --git a/ChangeLog b/ChangeLog index ec3bf6957..91ccc6957 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,13 @@ 2003-08-01 Alexandre Duret-Lutz + * configure.ac, NEWS: Bump version to 0.0f. + * iface/gspn/simple.test, iface/gspn/dcswave.test, + iface/gspn/dcswaveltl.test: Make sure the example directory + is writable. + * m4/lbtt.m4, m4/buddy.m4: Always configure buddy/ and lbtt/, + regardless of the --with-included-buddy and --with-included-lbtt + settings. + * wrap/python/Makefile.am (python_PYTHON, _spot_la_SOURCES): Explicitely refer to spot_wrap.cxx and spot.py as $(srcdir)/spot_wrap.cxx and $(srcdir)/spot.py. @@ -251,7 +259,7 @@ share the same dictionary. An empty dictionary should be constructed by the user and passed to the automaton' constructors as necessary. - This huge change removes most code than it adds. + This huge change removes more code than it adds. * src/Makefile.am (libspot_la_LIBADD): Add misc/libmisc.la. * src/misc/bddalloc.hh, src/misc/bddalloc.cc: New files. These diff --git a/NEWS b/NEWS index e50ef4974..91b02a502 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,18 @@ +New in spot 0.0f (2003-08-01): + + * More python bindings, still only for the spot::ltl:: namespace. + * Functional GSPN interface. (Enable with --with-gspn=directory.) + * The LTL scanner recognizes /\, \/, and xor. + * Upgrade to lbtt 1.0.2. + * tgba_tba_proxy is an on-the-fly degeneralizer. + * Implements the "magic search" algorithm. + (Works only on a tgba_tba_proxy.) + * Tgba's output algorithms (save(), dotty()) now non-recursive. + * During products, succ_iter will optimize its set of successors + using information computed from the current product state. + * BDD dictionnaries are now shared between automata and. This + gets rid of all the BDD-variable translating machinery. + New in spot 0.0d (2003-07-13): * Optimize translation of G operators occurring at the root diff --git a/configure.ac b/configure.ac index 2ba0e162b..95c586964 100644 --- a/configure.ac +++ b/configure.ac @@ -1,5 +1,5 @@ AC_PREREQ([2.57]) -AC_INIT([spot], [0.0e]) +AC_INIT([spot], [0.0f]) AC_CONFIG_AUX_DIR([tools]) AM_INIT_AUTOMAKE([foreign nostdinc check-news 1.7.3]) diff --git a/iface/gspn/dcswave.test b/iface/gspn/dcswave.test index 1d19358be..ca225ac76 100755 --- a/iface/gspn/dcswave.test +++ b/iface/gspn/dcswave.test @@ -5,6 +5,7 @@ set -e cp -R $srcdir/examples/DCSwave . +chmod +w DCSwave # Run this if you want, it builds approximately 3,600,000 states. # ../dottygspn-rg DCSwave/DCSWave ATTiIDLj SCi SCj >output diff --git a/iface/gspn/dcswaveltl.test b/iface/gspn/dcswaveltl.test index f4bf7f41f..5c67c25ac 100755 --- a/iface/gspn/dcswaveltl.test +++ b/iface/gspn/dcswaveltl.test @@ -5,6 +5,7 @@ set -e cp -R $srcdir/examples/DCSwave . +chmod +w DCSwave # G(ATTiIDLj => F(!SCj U SCi)) is true ../ltlgspn-srg DCSwave/DCSWave '!G(ATTiIDLj => F(!SCj U SCi))' ATTiIDLj SCi SCj > output diff --git a/iface/gspn/simple.test b/iface/gspn/simple.test index 9514c5cdd..c433981eb 100755 --- a/iface/gspn/simple.test +++ b/iface/gspn/simple.test @@ -5,6 +5,7 @@ set -e cp -R $srcdir/examples/simple . +chmod +w simple # Unknown properties should be flagged. ../dottygspn-rg simple/simple unknown && exit 1 diff --git a/m4/buddy.m4 b/m4/buddy.m4 index 0466c17ac..23c43c489 100644 --- a/m4/buddy.m4 +++ b/m4/buddy.m4 @@ -17,12 +17,16 @@ AC_DEFUN([AX_CHECK_BUDDY], [ fi if test "$with_included_buddy" = yes; then - AC_CONFIG_SUBDIRS([buddy]) BUDDY_LDFLAGS='$(top_builddir)/buddy/src/libbdd.la' BUDDY_CPPFLAGS='-I$(top_srcdir)/buddy/src' else BUDDY_LDFLAGS='-lbdd' fi + # We always configure BuDDy, this is needed to ensure + # it gets distributed properly. Whether with_included_buddy is + # set or not affects whether we *use* or *build* BuDDy. + AC_CONFIG_SUBDIRS([buddy]) + AM_CONDITIONAL([WITH_INCLUDED_BUDDY], [test "$with_included_buddy" = yes]) AC_SUBST([BUDDY_LDFLAGS]) AC_SUBST([BUDDY_CPPFLAGS]) diff --git a/m4/lbtt.m4 b/m4/lbtt.m4 index 09e191c1f..69f0a58e3 100644 --- a/m4/lbtt.m4 +++ b/m4/lbtt.m4 @@ -16,13 +16,17 @@ AC_DEFUN([AX_CHECK_LBTT], [ fi if test "$with_included_lbtt" = yes; then - AC_CONFIG_SUBDIRS([lbtt]) LBTT='${top_builddir}/lbtt/src/lbtt' LBTT_TRANSLATE='${top_builddir}/lbtt/src/lbtt-translate' else LBTT=lbtt LBTT_TRANSLATE=lbtt-translate fi + # We always configure lbtt, this is needed to ensure + # it gets distributed properly. Whether with_included_buddy is + # set or not affects whether we *use* or *build* lbtt. + AC_CONFIG_SUBDIRS([lbtt]) + AM_CONDITIONAL([WITH_INCLUDED_LBTT], [test "$with_included_lbtt" = yes]) AC_SUBST([LBTT]) AC_SUBST([LBTT_TRANSLATE])