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

* configure.ac, NEWS: Bump version to 0.0f.

Browse source 
* 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.
This commit is contained in:
Alexandre Duret-Lutz 2003-08-01 10:25:56 +00:00
parent 286405da95
commit 5b245d7dd1
8 changed files with 38 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

10
ChangeLog
View file

@ -1,5 +1,13 @@
2003-08-01 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* 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

15
NEWS
View file

@ -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

2
configure.ac
View file

@ -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])

1
iface/gspn/dcswave.test
View file

@ -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

1
iface/gspn/dcswaveltl.test
View file

@ -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

1
iface/gspn/simple.test
View file

@ -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

6
m4/buddy.m4
View file

@ -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])

6
m4/lbtt.m4
View file

@ -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])