You can subscribe to this list here.
2004 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
(4) |
Jul
(53) |
Aug
(5) |
Sep
(2) |
Oct
(1) |
Nov
|
Dec
|
---|---|---|---|---|---|---|---|---|---|---|---|---|
2005 |
Jan
(8) |
Feb
(2) |
Mar
|
Apr
|
May
(1) |
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
(1) |
Dec
|
2006 |
Jan
|
Feb
|
Mar
|
Apr
(9) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
(4) |
Dec
|
2007 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
(3) |
Jul
(28) |
Aug
(9) |
Sep
|
Oct
|
Nov
|
Dec
|
2008 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
(4) |
Sep
|
Oct
|
Nov
|
Dec
|
2010 |
Jan
|
Feb
|
Mar
|
Apr
|
May
(2) |
Jun
|
Jul
|
Aug
|
Sep
(1) |
Oct
|
Nov
|
Dec
|
2011 |
Jan
|
Feb
(1) |
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
(1) |
Dec
|
2013 |
Jan
|
Feb
(1) |
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
2014 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
(5) |
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
From: Haim C. <hai...@us...> - 2004-07-22 16:20:59
|
Hi, I have just committed few files - mainly remove solitare from regress= ion=20 suite, yet leaving it as an example. It just takes too much time to run. See the ChangeLog. I am going to release buddy today or tomorrow, since I want BuDDy to = be=20 fresh and new when CUJ be delivered to subscribers over the world. J=F8rn, since I do not know if CUJ have time to update BuDDy link, I = will=20 appreciate if you could keep the redirection in your university homep= age=20 for a while. Here are my suggested plans after this release: + Documentation - I would like to automate and standardize the=20 documentation in BuDDy, using doxygen. Sub tasks: - translating all the comments to be doxygen-complaint. - keep the first part of buddy.ps (the one that J=F8rn have written a= nd=20 explains quite good about buddy) in some raw format, and compose the= =20 final document from this raw format and the products of doxygen. I kn= ow=20 that doxygen can generate ps files, but I still don't know which raw= =20 format to use for the first part of buddy.ps.... Maybe simple text ? = sxw=20 (OpenOffice) ? - automate documentation generation. (generate the required=20 documentation when invoking 'make dist') I will try to find a documentation expert that might be interested to= =20 help with this documentation task. + Apply bugs-fixing patches submitted by Alexandre I think that after this stage, the way will be open for adding new= =20 features into buddy. I will be happy to have your insightful comments about the suggested = plans. Haim |
From: Haim C. <hai...@us...> - 2004-07-16 09:13:51
|
Thanks, Could you please also modify bddtest so it will detect the bug ? Haim Alexandre Duret-Lutz wrote: >This fix two things in bdd_support() > >1) A memory leak, which I believe is clear enough. >2) The return value when bdd_support() is called on bddtrue or bddfalse. > Since variable sets are conjunctions (i.e., the union of variables > sets is &), the empty set should be TRUE, not FALSE. For instance > we should have > bdd_support(formula1 | formula2) > == bdd_support(formula1) & bdd_support(formula2) > In BuDDy 2.3 this fails if any of the two formulae is a constant. > >2004-07-15 Alexandre Duret-Lutz <ad...@sr...> > > * src/bddop.c (bdd_support): Fix memory leak, and return bddtrue > when no variables are used. > >Index: src/bddop.c >=================================================================== >RCS file: /cvsroot/buddy/buddy/src/bddop.c,v >retrieving revision 1.1.1.1 >diff -u -r1.1.1.1 bddop.c >--- src/bddop.c 25 Jun 2004 13:22:22 -0000 1.1.1.1 >+++ src/bddop.c 15 Jul 2004 20:03:25 -0000 >@@ -2061,13 +2061,16 @@ > int res=1; > > CHECKa(r, bddfalse); >- >+ >+ /* Variable sets are conjunctions, so the empty support is bddtrue. */ > if (r < 2) >- return bddfalse; >+ return bddtrue; > > /* On-demand allocation of support set */ > if (supportSize < bddvarnum) > { >+ if (supportSet) >+ free(supportSet); > if ((supportSet=(int*)malloc(bddvarnum*sizeof(int))) == NULL) > { > bdd_error(BDD_MEMORY); > > |
From: Alexandre Duret-L. <ad...@sr...> - 2004-07-15 20:28:11
|
bdd_default_errhandler is called on internal errors, due either to BuDDy or to its bad use. Anyway there are real error that you want to cure your program from. I've always been bitten by the default handler which tells you there is an error, but not where it happened and lose all the context making it hard to debug (especially when your program is not entirely deterministic and you have to way to reproduce the faulty run). This changes the default handler to abort(). Like assert() does; after all this is used in pretty much the same situation. This is much more useful because since that will preserve the context in a coredump, and from their you can narrow the bug in your application. 2004-07-15 Alexandre Duret-Lutz <ad...@sr...> * src/kernel.c (bdd_default_errhandler): Do not exit, abort. Index: src/kernel.c =================================================================== RCS file: /cvsroot/buddy/buddy/src/kernel.c,v retrieving revision 1.2 diff -u -r1.2 kernel.c --- src/kernel.c 13 Jul 2004 21:04:36 -0000 1.2 +++ src/kernel.c 15 Jul 2004 20:19:29 -0000 @@ -414,7 +414,7 @@ This function sets the handler to be {\tt handler}. If a {\tt NULL} argument is supplied then no calls are made when an error occurs. Possible error codes are found in {\tt bdd.h}. The default handler - is {\tt bdd\_default\_errhandler} which will use {\tt exit()} to + is {\tt bdd\_default\_errhandler} which will use {\tt abort()} to terminate the program. Any handler should be defined like this: @@ -803,7 +803,7 @@ void bdd_default_errhandler(int e) { fprintf(stderr, "BDD error: %s\n", bdd_errstring(e)); - exit(1); + abort(); } -- Alexandre Duret-Lutz |
From: Alexandre Duret-L. <ad...@sr...> - 2004-07-15 20:14:18
|
2004-07-15 Alexandre Duret-Lutz <ad...@sr...> * src/bddop.c (bdd_simplify, bdd_allsat): Typo in documentation. Index: src/bddop.c =================================================================== RCS file: /cvsroot/buddy/buddy/src/bddop.c,v retrieving revision 1.1.1.1 diff -u -r1.1.1.1 bddop.c --- src/bddop.c 25 Jun 2004 13:22:22 -0000 1.1.1.1 +++ src/bddop.c 15 Jul 2004 20:10:29 -0000 @@ -1426,7 +1426,7 @@ SHORT {* coudert and Madre's restrict function *} PROTO {* BDD bdd_simplify(BDD f, BDD d) *} DESCR {* Tries to simplify the BDD {\tt f} by restricting it to the - domaine covered by {\tt d}. No checks are done to see if the + domain covered by {\tt d}. No checks are done to see if the result is actually smaller than the input. This can be done by the user with a call to {\tt bdd\_nodecount}. *} ALSO {* bdd\_restrict *} @@ -2350,12 +2353,12 @@ NAME {* bdd\_allsat *} SECTION {* operator *} SHORT {* finds all satisfying variable assignments *} -PROTO {* BDD bdd_satone(BDD r, bddallsathandler handler) *} +PROTO {* BDD bdd_allsat(BDD r, bddallsathandler handler) *} DESCR {* Iterates through all legal variable assignments (those - that make the BDD come true) for the bdd {\tt r} and + that make the BDD come true) for the bdd {\tt r} and calls the callback handler {\tt handler} for each of them. The array passed to {\tt handler} contains one entry for - each of the globaly defined variables. Each entry is either + each of the globally defined variables. Each entry is either 0 if the variable is false, 1 if it is true, and -1 if it is a don't care. -- Alexandre Duret-Lutz |
From: Alexandre Duret-L. <ad...@sr...> - 2004-07-15 20:12:38
|
This fix two things in bdd_support() 1) A memory leak, which I believe is clear enough. 2) The return value when bdd_support() is called on bddtrue or bddfalse. Since variable sets are conjunctions (i.e., the union of variables sets is &), the empty set should be TRUE, not FALSE. For instance we should have bdd_support(formula1 | formula2) == bdd_support(formula1) & bdd_support(formula2) In BuDDy 2.3 this fails if any of the two formulae is a constant. 2004-07-15 Alexandre Duret-Lutz <ad...@sr...> * src/bddop.c (bdd_support): Fix memory leak, and return bddtrue when no variables are used. Index: src/bddop.c =================================================================== RCS file: /cvsroot/buddy/buddy/src/bddop.c,v retrieving revision 1.1.1.1 diff -u -r1.1.1.1 bddop.c --- src/bddop.c 25 Jun 2004 13:22:22 -0000 1.1.1.1 +++ src/bddop.c 15 Jul 2004 20:03:25 -0000 @@ -2061,13 +2061,16 @@ int res=1; CHECKa(r, bddfalse); - + + /* Variable sets are conjunctions, so the empty support is bddtrue. */ if (r < 2) - return bddfalse; + return bddtrue; /* On-demand allocation of support set */ if (supportSize < bddvarnum) { + if (supportSet) + free(supportSet); if ((supportSet=(int*)malloc(bddvarnum*sizeof(int))) == NULL) { bdd_error(BDD_MEMORY); -- Alexandre Duret-Lutz |
From: Haim C. <hai...@us...> - 2004-07-12 21:00:53
|
Hi, I will continue with committing new files tomorrow. Currently the CVS is not stable - please do not check out. I still need to check in files in the src and examples directories. Sorry for the inconvenience. Haim |
From: Haim C. <hai...@us...> - 2004-07-12 20:25:39
|
Hi, I will be committing files during the next hour. When finished, I will send another Email. Yes, there will be a ChangeLog file ! :-) Haim |
From: Alexandre Duret-L. <ad...@sr...> - 2004-07-12 18:22:19
|
>>> "Haim" == Haim Cohen <hai...@us...> writes: [...] Haim> Using bison, the bddcalc test fails, as it reach stack overflow. Haim> However, using yacc there are no problems. I am using bison 1.875 . Haim> Two options: Haim> + I am using an old bison - I will check for updates Haim> + We should use yacc Third option: fix the grammar so it can process its input with bounded stack. 2004-07-12 Alexandre Duret-Lutz <ad...@sr...> * examples/bddcalc/parser.yxx (actionSeq, varlist): Rewrite as left-recursive rules. Index: buddy/examples/bddcalc/parser.yxx =================================================================== RCS file: /Volumes/CVS/repository/spot/spot/buddy/examples/bddcalc/parser.yxx,v retrieving revision 1.1 diff -u -r1.1 parser.yxx --- buddy/examples/bddcalc/parser.yxx 28 Jun 2004 15:22:12 -0000 1.1 +++ buddy/examples/bddcalc/parser.yxx 12 Jul 2004 13:54:04 -0000 @@ -119,7 +119,7 @@ ; actionSeq: - action T_semi actionSeq + actionSeq action T_semi | action T_semi ; @@ -159,7 +159,7 @@ ; varlist: - T_id varlist { actQuantVar2(&$$,&$1,&$2); } + varlist T_id { actQuantVar2(&$$,&$2,&$1); } | T_id { actQuantVar1(&$$,&$1); } ; -- Alexandre Duret-Lutz |
From: Haim C. <hai...@us...> - 2004-07-10 10:39:40
|
Hi Alexandre, There have been few problems in SF, and currently we do not have CVS access. I hope they will be fixed soon. I am now trying to apply your patch. I have found that something is wrong with bison. Using bison, the bddcalc test fails, as it reach stack overflow. However, using yacc there are no problems. I am using bison 1.875 . Two options: + I am using an old bison - I will check for updates + We should use yacc I will appreciate your comment about this. Haim |
From: Alexandre Duret-L. <ad...@sr...> - 2004-07-06 19:33:50
|
Finally here it is, sorry for the delay. I've seen that you have removed the generated parser and lexer from the CVS repostory, so I'm assuming you will not want the generated Makefile.ins and configure files on CVS either. (That's easier to me, since that what I do too, so our .cvsignore files are the same.) I've written the Makefile.ams so that all the examples are only build during `make check', not during ordinary `make'. I do not know if that will please you (it is easy to change: simply replace check_PROGRAMS by noinst_PROGRAMS in all the examples/*/Makefile.am). The reason I did that in Spot is that when I build buddy I'm interested only by the library, not by the example, so I didn't want to waste time an disk. I think it still make sense in BuDDy proper, especially since you plan to turn examples/ into a test suite (`make check' would therefore build these examples, and use them to perform many checks.) The attached patch changes a couple of files and adds many. This patch does not includes file removals and file renaming that you must do BEFORE applying the patch. Below is the list of commands to run, so you can copy/paste. First make sure you do all of this work from a fresh and clean checkout of BuDDy. Also ensure you have recent Autotools. At least Autoconf >=2.57, Automake >=1.7.3, Libtool >=1.5 (1.4 might work); but preferably Autoconf 2.59, Automake 1.8.5, Libtool 1.5.6. Do check `autoconf --version', `automake --version', `libtoolize --version' before doing anything else; a recurrent error on autotool lists is that users think they have installed the right version but do run an older one. -------------------------------------------------- cvs rm -f config cvs rm -f makefile cvs rm -f doc/makefile cvs rm -f src/makefile cvs rm -f examples/adder/makefile cvs rm -f examples/bddcalc/makefile cvs rm -f examples/bddtest/makefile cvs rm -f examples/cmilner/makefile cvs rm -f examples/fdd/makefile cvs rm -f examples/milner/makefile cvs rm -f examples/money/makefile cvs rm -f examples/queen/makefile cvs rm -f examples/solitare/makefile mv examples/bddcalc/lexer.l examples/bddcalc/lexer.lxx cvs rm examples/bddcalc/lexer.l cvs add examples/bddcalc/lexer.lxx mv examples/bddcalc/parser.h examples/bddcalc/parser_.h cvs rm examples/bddcalc/parser.h cvs add examples/bddcalc/parser_.h mv examples/bddcalc/parser.y examples/bddcalc/parser.yxx cvs rm examples/bddcalc/parser.y cvs add examples/bddcalc/parser.yxx mkdir tools m4 cvs add tools m4 patch -p0 -i /where/is/the/autotool.patch cvs add .cvsignore cvs add Makefile.am cvs add README.CVS cvs add configure.ac cvs add doc/.cvsignore cvs add doc/Makefile.am cvs add examples/.cvsignore cvs add examples/Makefile.am cvs add examples/Makefile.def cvs add examples/adder/.cvsignore cvs add examples/adder/Makefile.am cvs add examples/bddcalc/.cvsignore cvs add examples/bddcalc/Makefile.am cvs add examples/bddtest/.cvsignore cvs add examples/bddtest/Makefile.am cvs add examples/cmilner/.cvsignore cvs add examples/cmilner/Makefile.am cvs add examples/fdd/.cvsignore cvs add examples/fdd/Makefile.am cvs add examples/milner/.cvsignore cvs add examples/milner/Makefile.am cvs add examples/money/.cvsignore cvs add examples/money/Makefile.am cvs add examples/queen/.cvsignore cvs add examples/queen/Makefile.am cvs add examples/solitare/.cvsignore cvs add examples/solitare/Makefile.am cvs add m4/debug.m4 cvs add src/.cvsignore cvs add src/Makefile.am cvs add tools/.cvsignore autoreconf -vfi ./configure make distcheck cvs commit -------------------------------------------------- The three commands before `cvs commit' ensure everything builds fine. The `make distcheck' command is what you normally use to make a release: it builds a tarball containing every file that must be distributed, then unpack it and build it (and even run `make check') to ensure everything works and nothing has been omitted. If it succeed, it will print something like ============================================ buddy-2.3a archives ready for distribution: buddy-2.3a.tar.gz ============================================ I've bumped the version number since this CVS version is neither 2.3 nor 2.4. You can change on the second line of configure.ac. Here is the ChangeLog entry (BTW, there is still no ChangeLog on CVS). 2004-07-06 Alexandre Duret-Lutz <ad...@sr...> Revamp build-system to use Autoconf, Automake, and Libtool. * Makefile.am, README.CVS, configure.ac, doc/Makefile.am, examples/Makefile.am, examples/Makefile.def, examples/adder/Makefile.am, examples/bddcalc/Makefile.am, examples/bddtest/Makefile.am, examples/cmilner/Makefile.am, examples/fdd/Makefile.am, examples/milner/Makefile.am, examples/money/Makefile.am, examples/queen/Makefile.am, examples/solitare/Makefile.am, m4/debug.m4, src/Makefile.am: New files. * config, makefile, doc/makefile, examples/adder/makefile, examples/bddcalc/makefile, examples/bddtest/makefile, examples/cmilner/makefile, examples/fdd/makefile, examples/milner/makefile, examples/money/makefile, examples/queen/makefile, examples/solitare/makefile, src/makefile: Delete. * examples/bddcalc/parser.h: Rename as ... * examples/bddcalc/parser_.h: ... this, because the automake rules will output token definitions for parser.yxx in parser.h. * examples/bddcalc/lexer.l, examples/bddcalc/parser.y: Rename as ... * examples/bddcalc/lexer.lxx, examples/bddcalc/parser.yxx: ... these, so automake knows these are C++ files. Include parser_.h instead of parser.h, and parser.h instead of token.h. * src/kernel.c: Include config.h to get the version macros. (bdd_versionstr): Simplify using PACKAGE_VERSION. (bdd_version): Rewrite using MAJOR_VERSION and MINOR_VERSION. * src/kernel.h: Give CLOCK_PER_SEC a default value of 60. * README: Update build instructions. Have fun! -- Alexandre Duret-Lutz |
From: Haim C. <hai...@us...> - 2004-07-02 15:00:36
|
2004-07-02 haimcohen <hai...@us...> * examples/bddcalc/makefile 1.2: tokens.h was added to the 'clean' target as it is generated by yacc * examples/bddcalc/parser.y 1.2: Tokens were separated by spaces instead of commas to comply with POSIX standard. Patch was supplied by Alexandre Duret-Lutz <ad...@sr...> |
From: Haim C. <hai...@us...> - 2004-07-02 12:27:31
|
I see. Great ! I prefer to go with the standard. I will apply your patch latter on. About the change log - it seems I made a mistake by not checking in first the original BuDDy. SF took time to fix my CVS access, so I released the code first. Anyway, these changes are minor and sum up to std namespace fixes to be C++-standard, and renaming examples to be the same as executables. I will create a ChangeLog every CVS commit I make. Thanks for this point ! The ChangeLog will also contain CVS versions, to keep track of the files. The next commit I will made will be about: 1. regression scripts 2. Changing documentation files in the project directory to somewhat comply with the GNU standard (NEWS,AUTHORS, etc...) After I commit the changes, I will be glad if other developers can review them and send their opinion. As you see, I am currently put an effort with 'administrative' changes. I hope that soon I will start add real code changes. Haim Alexandre Duret-Lutz wrote: >[...] > > Haim> After upgrading my yacc ( which is actually byacc ) to 1.9-27, the > Haim> warnings disappeared. > Haim> Any ideas ? > >Ideas about what? > >Your previous yacc was GNU Bison 1.875, the new one is Berkeley yacc 1.9. >Obviously the latter silently accepts non-standard %token definitions. > > |
From: Alexandre Duret-L. <Ale...@li...> - 2004-07-02 12:24:18
|
>>> "Haim" == Haim Cohen <hai...@us...> writes: Haim> I have never used autoconf+automake+libtool before for Haim> projects, but I have read a bit about those scripts. Your Haim> contribution will be much appreciated. BTW, I'm afraid I won't be able to work out the patch for this before next week. Haim> Could you please explain how do you generate the configure and Haim> Makefile.in files ? configure is generated from configure.ac by autoconf Makefile.in's are generated from Makefile.am's by automake You do not need to call these tools directly. Today's Autoconf versions come with a tool called `autoreconf' that will run everything for you (run it as `autoreconf -vfi'). configure.ac ---. .---> configure | | Makefile.am ---+ +---> Makefile.in +-->[autoreconf -vfi]--+ sub/Makefile.am ---+ +---> sub/Makefile.in | | ... ---' `---> ... Haim> What exactly ( version numbers ) and how should I run ? The latest versions are Autoconf 2.59 Automake 1.8.5 Libtool 1.5.6 new releases usually come with fixes to improve portability of the generated files to some systems, so as a maintainer of a package that ships such generated files you should really ensure you use up-to-date autotools. These three packages are really easy to install from source, so if they do not come prepackaged with your distribution you could get them from ftp::/ftp.gnu.org/gnu/ Simply make sure you install Autoconf before the two others. Haim> I have tried automake and autoconf, but it seems I do not Haim> use them correctly, or that I have old versions. I can't comment on this if you do not state how you used them and which version you have. [...] Haim> Did you take into account the config file in the original project Haim> which defines label for the preprocessor ? I did not find it in your Haim> version with configure. Well, the point of Autoconf (= automatic configuration) is indeed not to have users fiddle such config files. Of course, options like "swap count" or "cache stats" cannot be enabled automatically; it's up to the user. I've turned these into ./configure options, because that is more idiomatic. (The buddy/README file in Spot lists these options.) -- Alexandre Duret-Lutz |
From: Alexandre Duret-L. <Ale...@li...> - 2004-07-02 11:44:33
|
[...] Haim> After upgrading my yacc ( which is actually byacc ) to 1.9-27, the Haim> warnings disappeared. Haim> Any ideas ? Ideas about what? Your previous yacc was GNU Bison 1.875, the new one is Berkeley yacc 1.9. Obviously the latter silently accepts non-standard %token definitions. -- Alexandre Duret-Lutz |
From: Haim C. <hai...@us...> - 2004-07-01 17:36:41
|
>By the meantime, here is a patch that fixes the following >diagnostic output by the CVS version of Bison. I guess its >better to fix such things before changing the build. > >[...] >parser.y:67.12: warning: stray `,' treated as white space >parser.y:67.19: warning: stray `,' treated as white space >parser.y:67.29: warning: stray `,' treated as white space >parser.y:67.37: warning: stray `,' treated as white space >parser.y:69.17: warning: stray `,' treated as white space >parser.y:69.27: warning: stray `,' treated as white space >parser.y:70.14: warning: stray `,' treated as white space >parser.y:71.21: warning: stray `,' treated as white space >parser.y:71.32: warning: stray `,' treated as white space >parser.y:71.40: warning: stray `,' treated as white space >[...] > Alexandre, After upgrading my yacc ( which is actually byacc ) to 1.9-27, the warnings disappeared. Any ideas ? I will now start work on making the examples directory a regression suite. I am now starting to think it will take more time to make BuDDy automake+autoconf+libtool compatible. Haim |
From: Haim C. <hai...@us...> - 2004-07-01 15:47:43
|
Thanks ! I have never used autoconf+automake+libtool before for projects, but I have read a bit about those scripts. Your contribution will be much appreciated. I think that configure and Makefile.in files should be kept under CVS. Every tar I have downloaded, had these files in. Could you please explain how do you generate the configure and Makefile.in files ? What exactly ( version numbers ) and how should I run ? I have tried automake and autoconf, but it seems I do not use them correctly, or that I have old versions. configure was generated, but did not create Makefiles. I am running Mandrake, and it seems it comes with old version of these tools. Did you take into account the config file in the original project which defines label for the preprocessor ? I did not find it in your version with configure. One more request : I have found there is a patch submitting system in SF. Could we use this opportunity that you send a patch to try it out ? I want to find out which kind of functionality it provides. Thanks, Haim Alexandre Duret-Lutz wrote: >Hi Haim, > >Sorry for the delay (it will happen again :)). > > > >>>>"Haim" == Haim Cohen <hai...@us...> writes: >>>> >>>> > >[...] > > Haim> Everyone have read access to the BuDDy repository in > Haim> S.F. You should first checkout/read the current CVS > Haim> repository. > >I'll generate all my patches against the CVS version of BuDDy. > > Haim> It would be great if you could first merge your changes > Haim> into the BuDDy 2.3 and test them. > >I did that yesterday (i.e., I've imported BuDDy 2.3 into the Spot >CVS repository and merge my changes). (The result is in >http://spot.lip6.fr/dl/spot-0.0v.tar.gz) > >I though it would be peanuts because CHANGES said nothing >changed except the version, but it turned out I had other >changes to cope with, besides the version bump: many examples >were renamed, there is a new way of defining VERSION, ... > >I agree such changes do not belong to the CHANGES file (which >looks like what GNU projects call NEWS), yet it would have saved >me time to have a list of such changes, and I guess it would >help other contributors too. Maybe you could consider using a >ChangeLog to keep track of every changes, like in GNU projects? >(see also http://www.gnu.org/prep/standards_40.html#SEC40) > >[...] > > Haim> I think that the build automation with autoconf should be the first > Haim> thing to integrate into BuDDy. > >Wow, you're brave. I though this would be the most >controversial change! > >I have one question before I prepare a patch for this. Do you >want to keep generated files (configure, Makefile.in, ...) in CVS >or not? I personally keep them out of CVS, but see >http://sources.redhat.com/automake/automake.html#CVS >before making your mind. > > >By the meantime, here is a patch that fixes the following >diagnostic output by the CVS version of Bison. I guess its >better to fix such things before changing the build. > > |
From: Alexandre Duret-L. <ad...@sr...> - 2004-06-30 20:21:09
|
Hi Haim, Sorry for the delay (it will happen again :)). >>> "Haim" == Haim Cohen <hai...@us...> writes: [...] Haim> Everyone have read access to the BuDDy repository in Haim> S.F. You should first checkout/read the current CVS Haim> repository. I'll generate all my patches against the CVS version of BuDDy. Haim> It would be great if you could first merge your changes Haim> into the BuDDy 2.3 and test them. I did that yesterday (i.e., I've imported BuDDy 2.3 into the Spot CVS repository and merge my changes). (The result is in http://spot.lip6.fr/dl/spot-0.0v.tar.gz) I though it would be peanuts because CHANGES said nothing changed except the version, but it turned out I had other changes to cope with, besides the version bump: many examples were renamed, there is a new way of defining VERSION, ... I agree such changes do not belong to the CHANGES file (which looks like what GNU projects call NEWS), yet it would have saved me time to have a list of such changes, and I guess it would help other contributors too. Maybe you could consider using a ChangeLog to keep track of every changes, like in GNU projects? (see also http://www.gnu.org/prep/standards_40.html#SEC40) [...] Haim> I think that the build automation with autoconf should be the first Haim> thing to integrate into BuDDy. Wow, you're brave. I though this would be the most controversial change! I have one question before I prepare a patch for this. Do you want to keep generated files (configure, Makefile.in, ...) in CVS or not? I personally keep them out of CVS, but see http://sources.redhat.com/automake/automake.html#CVS before making your mind. By the meantime, here is a patch that fixes the following diagnostic output by the CVS version of Bison. I guess its better to fix such things before changing the build. [...] parser.y:67.12: warning: stray `,' treated as white space parser.y:67.19: warning: stray `,' treated as white space parser.y:67.29: warning: stray `,' treated as white space parser.y:67.37: warning: stray `,' treated as white space parser.y:69.17: warning: stray `,' treated as white space parser.y:69.27: warning: stray `,' treated as white space parser.y:70.14: warning: stray `,' treated as white space parser.y:71.21: warning: stray `,' treated as white space parser.y:71.32: warning: stray `,' treated as white space parser.y:71.40: warning: stray `,' treated as white space [...] FWIW, the standard for yacc can be found at http://www.opengroup.org/onlinepubs/009695399/utilities/yacc.html#tag_04_174_13_03 2004-06-30 Alexandre Duret-Lutz <ad...@sr...> * examples/bddcalc/parser.y: Remove superfluous comas causing warnings from CVS Bison. POSIX requires "%token"s to be space-separated, not coma-separated. Index: examples/bddcalc/parser.y =================================================================== RCS file: /cvsroot/buddy/buddy/examples/bddcalc/parser.y,v retrieving revision 1.1.1.1 diff -u -r1.1.1.1 parser.y --- examples/bddcalc/parser.y 25 Jun 2004 13:21:45 -0000 1.1.1.1 +++ examples/bddcalc/parser.y 30 Jun 2004 20:09:31 -0000 @@ -14,11 +14,11 @@ #include "slist.h" #include "hashtbl.h" #include "parser.h" - + /* Definitions for storing and caching of identifiers */ #define inputTag 0 #define exprTag 1 - + struct nodeData { nodeData(const nodeData &d) { tag=d.tag; name=sdup(d.name); val=d.val; } @@ -37,7 +37,7 @@ int linenum; bddgbchandler gbcHandler = bdd_default_gbchandler; - + /* Prototypes */ void actInit(token *nodes, token *cache); void actInputs(void); @@ -46,7 +46,7 @@ void actOpr2(token *res, token *left, token *right, int opr); void actNot(token *res, token *right); void actId(token *res, token *id); -void actConst(token *res, int); +void actConst(token *res, int); void actSize(token *id); void actDot(token *fname, token *id); void actAutoreorder(token *times, token *method); @@ -57,30 +57,30 @@ void actQuantVar2(token *res, token *id, token *list); void actQuantVar1(token *res, token *id); void actPrint(token *id); - + %} /************************************************************************* Token definitions *************************************************************************/ -%token T_id, T_str, T_intval, T_true, T_false +%token T_id T_str T_intval T_true T_false -%token T_initial, T_inputs, T_actions -%token T_size, T_dumpdot -%token T_autoreorder, T_reorder, T_win2, T_win2ite, T_sift, T_siftite, T_none -%token T_cache, T_tautology, T_print +%token T_initial T_inputs T_actions +%token T_size T_dumpdot +%token T_autoreorder T_reorder T_win2 T_win2ite T_sift T_siftite T_none +%token T_cache T_tautology T_print -%token T_lpar, T_rpar +%token T_lpar T_rpar %token T_equal -%token T_semi, T_dot +%token T_semi T_dot -%right T_exist, T_forall, T_dot +%right T_exist T_forall T_dot %left T_biimp %left T_imp -%left T_or, T_nor +%left T_or T_nor %left T_xor -%left T_nand, T_and +%left T_nand T_and %right T_not /************************************************************************* @@ -212,7 +212,7 @@ { using namespace std ; int c; - + while ((c=getopt(ac, av, "hg")) != EOF) { switch (c) @@ -225,7 +225,7 @@ break; } } - + if (optind >= ac) usage(); @@ -242,7 +242,7 @@ bdd_printstat(); bdd_done(); - + return 0; } @@ -279,7 +279,7 @@ { if (names.exists((*i).name)) yyerror("Redefinition of input %s", (*i).name); - + (*i).val = bdd_ithvar(vnum); hashData hd((*i).name, 0, &(*i)); names.add(hd); @@ -299,7 +299,7 @@ { if (names.exists(id->id)) yyerror("Redefinition of %s", id->id); - + nodeData *d = new nodeData(exprTag, sdup(id->id), *expr->bval); hashData hd(d->name, 0, d); names.add(hd); -- Alexandre Duret-Lutz |
From: Haim C. <hai...@us...> - 2004-06-26 08:36:00
|
>> >> I'd be happy if any of these could be merged back into mainline. >> Below is the detailed list of the changes I made. I can send diffs >> for any of these on request. >> Hi Alexandre ! Thanks for your bug fixes and improvements. I am happy to see that we are already starting to benefit from open source ! ] I think the best approach for merging changes made into different versions of BuDDy will be the following : Everyone have read access to the BuDDy repository in S.F. You should first checkout/read the current CVS repository. It would be great if you could first merge your changes into the BuDDy 2.3 and test them. It will assure us an easier integration later on. I also prefer to create release right after each successful integration and testing. This way we give a chance to people to try it. I assume most of the users will download the tar.gz file rather than checkout fresh files from CVS. I understand you made 3 kinds of changes : improvements, fixes and build automation. I think that the build automation with autoconf should be the first thing to integrate into BuDDy. I will appreciate comments from the members. Haim |
From: Alexandre Duret-L. <ad...@sr...> - 2004-06-26 00:01:05
|
Hi there, I'm glad to learn BuDDy is reviving. Over the last year I have been maintaining my own copy of BuDDy. I had to fix a few bugs, and added a couple of feature needed for the development of Spot (a model-checking library). You can find the BuDDy version I'm using in the spot distribution available at http://spot.lip6.fr/. The main changes are: - build with autoconf+automake+libtool for better integration into similar source trees - new functions: bdd_existcomp, bdd_forallcomp, bdd_uniquecomp,=20 bdd_appexcomp, bdd_appallcomp, bdd_appunicomp these are similar to the existing version without *comp, but these complement the BDD set given bdd_mergepairs, bdd_copypairs merge or copy pairs (I don't use these anymore, but they were useful at some point) - bug fixes: * bdd_support should return bddtrue when the support is empty. * Memory leak in bdd_support. * Spurious coma in the calculator grammar. * various typos in documentation - usability improvement: arrange so that bdd_default_errhandler coredumps on fatal errors, so we can debug more easily. I'd be happy if any of these could be merged back into mainline. Below is the detailed list of the changes I made. I can send diffs for any of these on request. 2004-01-07 Alexandre Duret-Lutz <ad...@sr...> * src/bddop.c (bdd_support): Free supportSet if it needs to be reallocated. This fixes a memory leak reported by Sou...@li.... 2003-11-14 Alexandre Duret-Lutz <ad...@sr...> * examples/Makefile.def (AM_CPPFLAGS): Add -I$(srcdir). 2003-08-06 Alexandre Duret-Lutz <ad...@sr...> * doc/Makefile.am (EXTRA_DIST): Replace buddy.ps by buddy.pdf (the latter has been rebuilt and on J=F8rn's request it explicitly mentions the differences with the 2.2 manual). * src/bddop.c (bdd_forallcomp, bdd_uniquecomp): Fix documentation. 2003-07-17 Alexandre Duret-Lutz <ad...@sr...> * src/bdd.h (bdd_existcomp, bdd_forallcomp, bdd_uniquecomp, bdd_appexcomp, bdd_appallcomp, bdd_appunicomp): Declare for C and C++. * src/bddop.c (CACHEID_EXISTC, CACHEID_FORALLC, CACHEID_UNIQUEC, CACHEID_APPEXC, CACHEID_APPALC, CACHEID_APPUNCC): New macros. (quatvarsetcomp): New variables. (varset2vartable): Take a second argument to indicate negation, set quatvarsetcomp. (INVARSET): Honor quatvarsetcomp. (quantify): New function, extracted from bdd_exist, bdd_forall, and bdd_appunicomp. (bdd_exist, bdd_forall, bdd_appunicomp): Use quantify. (bdd_existcomp, bdd_forallcomp, bdd_appunicompcomp): New functions. (appquantify): New function, extracted from bdd_appex, bdd_appall, and bdd_appuni. (bdd_appex, bdd_appall, bdd_appuni): Use appquantify. (bdd_appexcomp, bdd_appallcomp, bdd_appunicomp): New functions. * src/bddop.c (bdd_support): Return bddtrue when the support is empty, because variable sets are conjunctions. 2003-05-22 Alexandre Duret-Lutz <ad...@sr...> * src/pairs.c (bdd_mergepairs): New function. (bdd_copypair): Revert 2003-05-20's change. Use bdd_addref to copy result variables. * src/bdd.h (BDD_INVMERGE): New error code. (bdd_mergepairs): Declare. * src/kernel.c (errorstrings): Add string of BDDINV. * src/bddop.c (bdd_simplify): Typo in doc, s/domaine/domain/. 2003-05-20 Alexandre Duret-Lutz <ad...@sr...> * src/pairs.c (bdd_copypair): Use memcpy to copy from->result, and correctly copy p->last from from->last. * src/pairs.c (bdd_setbddpair): Fix prototype in documentation. 2003-05-19 Alexandre Duret-Lutz <ad...@sr...> * src/bdd.h: Declare bdd_copypair(). * src/pairs.c (bdd_copypair, bdd_pairalloc): New functions. (bdd_newpair): Use bdd_pairalloc. 2003-05-12 Alexandre Duret-Lutz <ad...@sr...> * src/kernel.c (bdd_default_errhandler): Call abort(), not exit(1). 2003-05-07 Alexandre Duret-Lutz <ad...@sr...> * src/bddop.c (bdd_allsat): Fix description. 2003-05-05 Alexandre Duret-Lutz <ad...@sr...> * configure.ac: Output config.h. * src/kernel.h: Include it. * src/Makefile.am (AM_CPPFLAGS): New variable. * configure.ac, Makefile.am, src/Makefile.am, doc/Makefile.am, examples/Makefile.am, examples/Makefile.def, examples/adder/Makefile.am, examples/calculator/Makefile.am, examples/cmilner/Makefile.am, examples/fdd/Makefile.am, examples/internal/Makefile.am, examples/milner/Makefile.am, examples/money/Makefile.am, examples/queen/Makefile.am, examples/solitar/Makefile.am, m4/debug.m4, m4/gccwarns.m4, ChangeLog, INSTALL: New files. * config, makefile, src/makefile, doc/makefile, examples/adder/makefile, examples/calculator/makefile examples/cmilner/makefile, examples/fdd/makefile, examples/internal/makefile, examples/milner/makefile, examples/money/makefile, examples/queen/makefile, examples/solitare/makefile : Delete. * examples/adder/adder.cxx, examples/fdd/statespace.cxx, examples/internal/bddtest.cxx, examples/milner/milner.cxx, examples/money/money.cxx, examples/queen/queen.cxx, examples/solitare/solitare.cxx: Include iostream. * examples/calculator/parser.y: Rename as ... * examples/calculator/parser.yxx: ... this. Remove spurious comas in %token, %right, and %left arguments. * examples/calculator/parser.h: Rename as ... * examples/calculator/parser_.h: ... this, because the bison rule with output parser.h (not tokens.h) from parser.y. * examples/calculator/lexer.l: Rename as ... * examples/calculator/lexer.lxx: ... this. Include parser.h instead of tokens.h. * examples/calculator/slist.h (voidSList::voisSListElem, SList::ite): Fix friend usage. * src/kernel.h (DEFAULT_CLOCK): Default to 60 if not already defined. * README: Update build instruction, and file listing. --=20 Alexandre Duret-Lutz |
From: Haim C. <hai...@us...> - 2004-06-25 19:05:57
|
Hi, I would like to suggest few improvements to BuDDy project infrastruct= ure. These improvements has no direct implications on the features in BuDD= y,=20 but I am sure they will increase robustness in the future. Documentation: Convert the in-code documentation to Doxygen format. Doxygen can=20 generate HTML, rtf, and LaTeX files. This will enable the automation of creating BuDDy API documentation f= rom=20 code. The first part of the current document about BuDDy will become a=20 document on its own. So, we can have 3 documents : BDD notes, Buddy introduction, and the= =20 reference manual generated by Doxygen. Generating the reference manual will be part of =B4make docs=B4, so i= t can=20 be generated during the make process. Testing: It is a good idea to have a regression suite. When a new feature is= =20 added, the developer must supply one or more new tests, that only the new version can pass. We can use the examples as the basis for this. We just need to keep t= he=20 expected results as well, and add a script to run all the tests. I have ideas for new features ( actually these are features which I h= ave=20 already wrote and tested in an old version of BuDDy, but I guess there will be no problems to merge them ). I can add them= =20 when I have the time: a. Binary files format which is also gzipped using zlib b. Randomize an assignment from a bdd. Good for constrained random= =20 generation. Comments are welcome. Haim |