From aa4a582f1be7d4931f5f6524f090ca4b1d0c7567 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 28 Jun 2004 15:22:11 +0000 Subject: [PATCH] Merge BuDDy 2.3. * examples/calculator/, examples/internal/: Were renamed as ... * examples/bddcalc/, examples/bddtest/: ... these. * configure.ac: Adjust version and output Makefiles. * examples/Makefile.am (SUBDIRS): Adjust subdir renaming. * examples/cmilner/milner.c, examples/fdd/statespace.cxx: Were renamed as ... * examples/cmilner/cmilner.c, examples/fdd/fdd.cxx: ... these. * examples/cmilner/Makefile.am, examples/fdd/Makefile.am: Adjust accordingly. * src/Makefile.am (AM_CPPFLAGS): Define VERSION. --- buddy/ChangeLog | 14 + buddy/README | 59 ++-- buddy/configure.ac | 6 +- buddy/doc/Makefile.am | 2 +- buddy/doc/tech.txt | 186 ----------- buddy/examples/Makefile.am | 5 +- buddy/examples/adder/adder.cxx | 31 +- buddy/examples/bddcalc/.cvsignore | 8 + buddy/examples/bddcalc/Makefile.am | 24 ++ buddy/examples/bddcalc/{lexer.l => lexer.lxx} | 2 +- buddy/examples/bddcalc/makefile | 45 --- .../examples/bddcalc/{parser.y => parser.yxx} | 34 +- .../examples/bddcalc/{parser.h => parser_.h} | 0 buddy/examples/bddcalc/tokens.h | 39 --- buddy/examples/bddtest/.cvsignore | 4 + buddy/examples/bddtest/Makefile.am | 3 + buddy/examples/bddtest/makefile | 38 --- buddy/examples/cmilner/Makefile.am | 4 +- buddy/examples/cmilner/milner.c | 299 ------------------ buddy/examples/fdd/Makefile.am | 4 +- buddy/examples/fdd/statespace.cxx | 79 ----- buddy/examples/milner/milner.cxx | 8 +- buddy/examples/money/money.cxx | 3 +- buddy/examples/queen/queen.cxx | 1 + buddy/examples/solitare/solitare.cxx | 20 +- buddy/src/Makefile.am | 4 +- buddy/src/kernel.h | 4 +- 27 files changed, 130 insertions(+), 796 deletions(-) delete mode 100644 buddy/doc/tech.txt create mode 100644 buddy/examples/bddcalc/.cvsignore create mode 100644 buddy/examples/bddcalc/Makefile.am rename buddy/examples/bddcalc/{lexer.l => lexer.lxx} (99%) delete mode 100644 buddy/examples/bddcalc/makefile rename buddy/examples/bddcalc/{parser.y => parser.yxx} (94%) rename buddy/examples/bddcalc/{parser.h => parser_.h} (100%) delete mode 100644 buddy/examples/bddcalc/tokens.h create mode 100644 buddy/examples/bddtest/.cvsignore create mode 100644 buddy/examples/bddtest/Makefile.am delete mode 100644 buddy/examples/bddtest/makefile delete mode 100644 buddy/examples/cmilner/milner.c delete mode 100644 buddy/examples/fdd/statespace.cxx diff --git a/buddy/ChangeLog b/buddy/ChangeLog index 0f8a11a64..7e59a5e20 100644 --- a/buddy/ChangeLog +++ b/buddy/ChangeLog @@ -1,3 +1,17 @@ +2004-06-28 Alexandre Duret-Lutz + + Merge BuDDy 2.3. + * examples/calculator/, examples/internal/: Were renamed as ... + * examples/bddcalc/, examples/bddtest/: ... these. + * configure.ac: Adjust version and output Makefiles. + * examples/Makefile.am (SUBDIRS): Adjust subdir renaming. + * examples/cmilner/milner.c, examples/fdd/statespace.cxx: Were + renamed as ... + * examples/cmilner/cmilner.c, examples/fdd/fdd.cxx: ... these. + * examples/cmilner/Makefile.am, examples/fdd/Makefile.am: Adjust + accordingly. + * src/Makefile.am (AM_CPPFLAGS): Define VERSION. + 2004-01-07 Alexandre Duret-Lutz * src/bddop.c (bdd_support): Free supportSet if it needs to be diff --git a/buddy/README b/buddy/README index a0aa17818..dd739a634 100644 --- a/buddy/README +++ b/buddy/README @@ -1,7 +1,7 @@ ========================================================================== *** BuDDy *** Binary Decision Diagrams - Library Package v2.2a + Library Package v2.3a -------------------------------------------------------------------------- Copyright (C) 1996-2002 by Jorn Lind-Nielsen All rights reserved @@ -32,12 +32,27 @@ ========================================================================== +--------------------------------------------------------------------- +--- PREFACE -------------------------------------------------------- +--------------------------------------------------------------------- + +BuDDy was originally developed by Jorn Lind-Nielsen as a part of his +Phd thesis. +After using BuDDy as a BDD library for long time ( while getting some +support from Jorn through Email ), I have been suggested by Jorn to take +ownership of the project and move it to SourceForge. +I invite all users who are interested to participate in the development +to contact me. ( I always have desired tasks / features awaiting... ) +I hope that BuDDy will prosper under my management. + +Haim Cohen +haimcohen2002@hotmail.com --------------------------------------------------------------------- --- REQUIREMENTS ---------------------------------------------------- --------------------------------------------------------------------- -* A (not to old) C++ compiler +* A (not too old) C++ compiler. I use g++ 3.3.3 * A machine that supports 32 bit integers @@ -54,10 +69,10 @@ The following commands should build and install the library. `./configure' accepts many arguments to tune your installation. The following options are noteworthy: - --includedir=/somewhere/include + --includedir=/somewhere/include Specify where header files will be installed. - --libdir=/somewhere/lib + --libdir=/somewhere/lib Specify where libraries will be installed. --disable-shared @@ -70,7 +85,7 @@ The following options are noteworthy: Count number of fundamental variable swaps (for debugging) --enable-cache-stats - Gather statistical information about operator and unique node + Gather statistical information about operator and unique node caching (for debugging) Run `./configure --help' for a complete listing, and see @@ -89,8 +104,8 @@ could be: g++ -I/usr/local/include myfile.cc -o myfile -L/usr/local/lib -lbdd -Your machine may be setup to use the above directories auto- -matically, so you might be able to do: +Your machine may be setup to use the above directories automatically, +so you might be able to do: g++ myfile.cc -o myfile -lbdd @@ -102,41 +117,17 @@ matically, so you might be able to do: src: All files needed for the BuDDy package. examples: Example files fdd: An example of use of the FDD interface. - calculator: An example of a BDD calculator. Uses reordering. + bddcalc: An example of a BDD calculator. Uses reordering. adder: Construction of a N-bit adder. Uses reordering. - milner: A calculation of the reachable statespace for Milner's + milner: A calculation of the reachable state space for Milner's scheduler. C++. cmilner: As above but purely in ANSI-C. queen: Solution to the N-queen chess problem. solitare: Solution to a solitare game. money: Solution to the send-more-money problem (bvec demo). - internal: Some internal regression tests. + bddtest : Some internal tests. doc: Documentation. buddy.ps: Package documentation. bddnotes.ps: BDD introduction notes. tools: Tools used during the build. m4: A couple of macros used to build ./configure. - ---------------------------------------------------------------------- ---- FEEDBACK -------------------------------------------------------- ---------------------------------------------------------------------- - -Please do not hesitate to send any questions or bug reports to: - - Jorn Lind-Nielsen: buddy@itu.dk - (or maybe jorn_lind_nielsen@hotmail.com or jln@fjeldgruppen.dk) - -It may take some time to get an answer since BuDDy do not have that -much focus any more - but I'll try to give a reasonable answer -in (finite) time. - -New updates and other info can be found at: - - http://www.it-c.dk/research/buddy/ - (or http://www.itu.dk/research/buddy) - - -Hope you find some use for this software - - Jorn Lind-Nielsen - diff --git a/buddy/configure.ac b/buddy/configure.ac index e169759e1..3052d2d92 100644 --- a/buddy/configure.ac +++ b/buddy/configure.ac @@ -1,5 +1,5 @@ AC_PREREQ([2.57]) -AC_INIT([buddy], [2.2a]) +AC_INIT([buddy], [2.3a]) AC_CONFIG_AUX_DIR([tools]) AM_INIT_AUTOMAKE([foreign nostdinc no-define 1.7.3]) @@ -22,10 +22,10 @@ AC_CONFIG_FILES([ doc/Makefile examples/Makefile examples/adder/Makefile - examples/calculator/Makefile + examples/bddcalc/Makefile + examples/bddtest/Makefile examples/cmilner/Makefile examples/fdd/Makefile - examples/internal/Makefile examples/milner/Makefile examples/money/Makefile examples/queen/Makefile diff --git a/buddy/doc/Makefile.am b/buddy/doc/Makefile.am index 9d2ed0a48..b770f73a1 100644 --- a/buddy/doc/Makefile.am +++ b/buddy/doc/Makefile.am @@ -1 +1 @@ -EXTRA_DIST = bddnotes.ps buddy.pdf tech.txt +EXTRA_DIST = bddnotes.ps buddy.pdf diff --git a/buddy/doc/tech.txt b/buddy/doc/tech.txt deleted file mode 100644 index 9a3fa6a63..000000000 --- a/buddy/doc/tech.txt +++ /dev/null @@ -1,186 +0,0 @@ -**************************************************************************** - How to create your own internal BDD functions. -**************************************************************************** - -PLEASE NOTE -That interrupting variable reordering has been introduced after this document was written. - - -===[ Functions that do not change or produce new BDDs ]===================== - -I'll do this by example. Take "bdd_satcount" that counts the number of -satisfying assignments that makes a BDD true. - -Almost all functions consists of some introduction followed by a -recursion through the BDD. - -* Use the type BDD for all references (numbers) to BDD nodes. -* External BDD variables used internally in the package are - defined in "kernel.h" -* Macros for reading BDD nodes are: - LEVEL(r) - LOW(r) - HIGH(r) - ISCONST(r) => true if r is one of the terminals - - -double bdd_satcount(BDD r) -{ - double size=1; - int n; - - CHECKa(r, 0.0); /* CHECK for valid nodes - defined in kernel.h */ - - miscid = CACHEID_SATCOU; /* Setup global variables. This is - used extensively instead of passing - arguments to the recursive functions, - for faster recursive calls */ - - for (n=0 ; na == root && entry->c == miscid) - return entry->r.dres; - - /* Do whatever calculations are needed */ - - size = 0; - s = 1; - - for (m=LEVEL(root)+1 ; ma = root; - entry->c = miscid; - entry->r.dres = size; - - return size; /* Return result */ -} - - - -===[ Functions that produces new BDDs ]===================================== - -Functions that produces BDD nodes must take great care to avoid -loosing intermidiate nodes when automatic garbage collections -occur. This is doneby stacking each intermidiate result until they are no more used. This stack is check by the garbage collector. - -Macros for accessing the stack: - INITREF: Reset the stack - PUSHREF(n): Push the node 'n' on the stack - READREF(p): Read 'p' positions down the stack - POPREF(p): Pop 'p' nodes off the stack. - -Again I'll illustrate this with an example - the NOT operator. - -BDD bdd_not(BDD r) -{ - int res; - CHECKa(r, bddfalse); /* Validate arguments */ - - INITREF; /* Important! resets the stack */ - - res = not_rec(r); /* Recurse */ - checkreorder(res); /* Check to see if a reordering was called for */ - - return res; /* Return result */ -} - - -static BDD not_rec(BDD r) -{ - BddCacheData *entry; /* Cache entry pointer */ - BDD res; - - if (ISZERO(r)) /* Check constant terminals */ - return BDDONE; - if (ISONE(r)) - return BDDZERO; - - /* Lookup in cache */ - entry = BddCache_lookup(&applycache, NOTHASH(r)); - if (entry->a == r && entry->c == bddop_not) - return entry->r.res; - - /* Recurse AND push result on the reference stack */ - PUSHREF( not_rec(LOW(r)) ); - PUSHREF( not_rec(HIGH(r)) ); - - /* Create a new BDD node */ - res = bdd_makenode(LEVEL(r), READREF(2), READREF(1)); - - /* Pop result off the stack */ - POPREF(2); - - /* Insert in cache */ - entry->a = r; - entry->c = bddop_not; - entry->r.res = res; - - /* Return the result */ - return res; -} - - - - -===[ Documentation ]======================================================== - -ALL entries visible to the user should be documentet by an commented -section like the one shown here, placed right before the code. - -Each doc. entry consist of a keyword followed by {* ... text -... *}. The entries are: - - NAME: Name of the function. - SECTION: Which part to place the documentation in. - SHORT: One line description of the code. - PROTO: The exact prototype. - DESCR: Multiline description of the code. - ALSO: Other relevant stuff. - RETURN: The returned value. - -/* -NAME {* bdd\_satcount *} -SECTION {* info *} -SHORT {* Calculates the number of satisfying variable assignments *} -PROTO {* double bdd_satcount(BDD r) *} -DESCR {* Calculates how many possible variable assignments there exists - such that {\tt r} is satisfied, taking all defined variables - into account. *} -ALSO {* bdd\_satone, bdd\_fullsatone, bdd\_satcountln *} -RETURN {* The number of possible assignments. *} -*/ diff --git a/buddy/examples/Makefile.am b/buddy/examples/Makefile.am index da71976af..596e79b7e 100644 --- a/buddy/examples/Makefile.am +++ b/buddy/examples/Makefile.am @@ -1,11 +1,10 @@ SUBDIRS = \ adder \ - calculator \ + bddcalc \ + bddtest \ cmilner \ fdd \ - internal \ milner \ money \ queen \ solitare - diff --git a/buddy/examples/adder/adder.cxx b/buddy/examples/adder/adder.cxx index bb17ef945..771214ef2 100644 --- a/buddy/examples/adder/adder.cxx +++ b/buddy/examples/adder/adder.cxx @@ -27,7 +27,7 @@ bdd *xout; void build_adder(void) { int n; - + for (n=0 ; n 0) @@ -48,9 +48,10 @@ void build_adder(void) int main(int argc, char **argv) { + using namespace std ; int method=BDD_REORDER_NONE; int n; - + if(argc < 2 || argc > 3) { cout << "usage: adder N R\n"; @@ -59,7 +60,7 @@ int main(int argc, char **argv) cout << " in this case 'adder' starts with a worst case ordering\n"; exit(1); } - + N = atoi(argv[1]); if (N <= 0) { @@ -90,17 +91,15 @@ int main(int argc, char **argv) if (strcmp(argv[2], "rand") == 0) method = BDD_REORDER_RANDOM; } - - long c0 = clock(); - + bdd_init(500,1000); bdd_setvarnum(2*N); - + ainp = new bdd[N]; binp = new bdd[N]; co = new bdd[N]; xout = new bdd[N]; - + for (n=0 ; n #include +#include "parser_.h" #include "parser.h" -#include "tokens.h" %} diff --git a/buddy/examples/bddcalc/makefile b/buddy/examples/bddcalc/makefile deleted file mode 100644 index 783dd7002..000000000 --- a/buddy/examples/bddcalc/makefile +++ /dev/null @@ -1,45 +0,0 @@ -# --------------------------- -# Makefile for BDD calculator -# --------------------------- - -all: bddcalc - -# --- Compiler flags -CFLAGS = -O3 -pedantic -Wall -ansi -L../../src -I../../src - -# --- C++ compiler -CPP = g++ - -# --- C compiler -CC = gcc - -# --- You may need to change these according to your flex and bison versions -parser.cxx: parser.h parser.y - yacc -d -o parser.cxx parser.y - mv parser.cxx.h tokens.h - -lexer.cxx: tokens.h parser.h lexer.l - flex -olexer.cxx lexer.l - - -# --- Do not touch --- - -.SUFFIXES: .cxx .c - -.cxx.o: - $(CPP) $(CFLAGS) -c $< - -.c.o: - $(CC) $(CFLAGS) -c $< - -bddcalc: parser.o lexer.o hashtbl.o bddlib - $(CPP) $(CFLAGS) parser.o lexer.o hashtbl.o -o bddcalc -lbdd -lm - -bddlib: - cd ../../src ; make - -clean: - rm -f *~ examples/*~ - rm -f *.o - rm -f bddcalc parser.cxx lexer.cxx - diff --git a/buddy/examples/bddcalc/parser.y b/buddy/examples/bddcalc/parser.yxx similarity index 94% rename from buddy/examples/bddcalc/parser.y rename to buddy/examples/bddcalc/parser.yxx index 9b57db30d..3f814c761 100644 --- a/buddy/examples/bddcalc/parser.y +++ b/buddy/examples/bddcalc/parser.yxx @@ -6,15 +6,17 @@ *************************************************************************/ %{ -#include +#include #include #include #include #define IMPLEMENTSLIST /* Special for list template handling */ #include "slist.h" #include "hashtbl.h" -#include "parser.h" - +#include "parser_.h" + + using namespace std; + /* Definitions for storing and caching of identifiers */ #define inputTag 0 #define exprTag 1 @@ -64,23 +66,23 @@ 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 /************************************************************************* @@ -201,7 +203,6 @@ print: void usage(void) { - using namespace std ; cerr << "USAGE: bddcalc [-hg] file\n"; cerr << " -h : print this message\n"; cerr << " -g : disable garbage collection info\n"; @@ -210,7 +211,6 @@ void usage(void) int main(int ac, char **av) { - using namespace std ; int c; while ((c=getopt(ac, av, "hg")) != EOF) @@ -389,7 +389,6 @@ void actQuantVar1(token *res, token *id) void actSize(token *id) { - using namespace std ; hashData hd; if (names.lookup(id->id,hd) == 0) @@ -404,7 +403,6 @@ void actSize(token *id) void actDot(token *fname, token *id) { - using namespace std ; hashData hd; if (names.lookup(id->id,hd) == 0) @@ -434,7 +432,6 @@ void actCache(void) void actTautology(token *id) { - using namespace std ; hashData hd; if (names.lookup(id->id,hd) == 0) @@ -451,7 +448,6 @@ void actTautology(token *id) void actPrint(token *id) { - using namespace std ; hashData hd; if (names.lookup(id->id,hd) == 0) diff --git a/buddy/examples/bddcalc/parser.h b/buddy/examples/bddcalc/parser_.h similarity index 100% rename from buddy/examples/bddcalc/parser.h rename to buddy/examples/bddcalc/parser_.h diff --git a/buddy/examples/bddcalc/tokens.h b/buddy/examples/bddcalc/tokens.h deleted file mode 100644 index 6a41e8d5b..000000000 --- a/buddy/examples/bddcalc/tokens.h +++ /dev/null @@ -1,39 +0,0 @@ -#ifndef YYERRCODE -#define YYERRCODE 256 -#endif - -#define T_id 257 -#define T_str 258 -#define T_intval 259 -#define T_true 260 -#define T_false 261 -#define T_initial 262 -#define T_inputs 263 -#define T_actions 264 -#define T_size 265 -#define T_dumpdot 266 -#define T_autoreorder 267 -#define T_reorder 268 -#define T_win2 269 -#define T_win2ite 270 -#define T_sift 271 -#define T_siftite 272 -#define T_none 273 -#define T_cache 274 -#define T_tautology 275 -#define T_print 276 -#define T_lpar 277 -#define T_rpar 278 -#define T_equal 279 -#define T_semi 280 -#define T_dot 281 -#define T_exist 282 -#define T_forall 283 -#define T_biimp 284 -#define T_imp 285 -#define T_or 286 -#define T_nor 287 -#define T_xor 288 -#define T_nand 289 -#define T_and 290 -#define T_not 291 diff --git a/buddy/examples/bddtest/.cvsignore b/buddy/examples/bddtest/.cvsignore new file mode 100644 index 000000000..796d735e8 --- /dev/null +++ b/buddy/examples/bddtest/.cvsignore @@ -0,0 +1,4 @@ +Makefile +Makefile.in +.deps +bddtest diff --git a/buddy/examples/bddtest/Makefile.am b/buddy/examples/bddtest/Makefile.am new file mode 100644 index 000000000..eb8820a5d --- /dev/null +++ b/buddy/examples/bddtest/Makefile.am @@ -0,0 +1,3 @@ +include ../Makefile.def +check_PROGRAMS = bddtest +bddtest_SOURCES = bddtest.cxx diff --git a/buddy/examples/bddtest/makefile b/buddy/examples/bddtest/makefile deleted file mode 100644 index 184d4964f..000000000 --- a/buddy/examples/bddtest/makefile +++ /dev/null @@ -1,38 +0,0 @@ -# -------------------------------- -# Makefile for internal tests -# -------------------------------- - -# --- Compiler flags -CFLAGS = -g -pedantic -Wall -ansi -L../../src -I../../src - -# --- C++ compiler -CPP = g++ - -# --- C compiler -CC = gcc - - -# --- Do not touch --- - -.SUFFIXES: .cxx .c - -.cxx.o: - $(CPP) $(CFLAGS) -c $< - -.c.o: - $(CC) $(CFLAGS) -c $< - -bddtest: bddtest.o bddlib - $(CPP) $(CFLAGS) bddtest.o -o bddtest -lbdd -lm - -bddlib: - cd ../../src ; make - -clean: - rm -f *~ - rm -f *.o - rm -f bddtest - -bddtest.o: ../../src/bdd.h - - diff --git a/buddy/examples/cmilner/Makefile.am b/buddy/examples/cmilner/Makefile.am index 09a9ab7e0..736851736 100644 --- a/buddy/examples/cmilner/Makefile.am +++ b/buddy/examples/cmilner/Makefile.am @@ -1,4 +1,4 @@ include ../Makefile.def EXTRA_DIST = readme -check_PROGRAMS = milner -milner_SOURCES = milner.c +check_PROGRAMS = cmilner +cmilner_SOURCES = cmilner.c diff --git a/buddy/examples/cmilner/milner.c b/buddy/examples/cmilner/milner.c deleted file mode 100644 index 65b70f139..000000000 --- a/buddy/examples/cmilner/milner.c +++ /dev/null @@ -1,299 +0,0 @@ -#include -#include -#include -#include -#include "bdd.h" - -int N; /* Number of cyclers */ -int *normvar; /* Current state variables */ -int *primvar; /* Next state variables */ - -bdd normvarset; -bddPair *pairs; - -bdd A(bdd* x, bdd* y, int z) -{ - bdd res = bddtrue, tmp1, tmp2; - int i; - - for(i=0 ; i 1 -> 2 -> 3 -> 4 -> 5 -> -> 7 -> 0 - */ - -#include -#include "fdd.h" -using namespace std; - -/* Use the transition relation "transRel" to iterate through the statespace - */ -void findStateSpace(bdd transRel) -{ - /* Create a new pair for renaming the next-state variables to - * current-state variables */ - bddPair *p = bdd_newpair(); - fdd_setpair(p,1,0); - - /* Get a BDD that represents all the current-state variables */ - bdd currentStateVar = fdd_ithset(0); - - /* Start with the initial state */ - bdd reachedStates = fdd_ithvar(0,0); - - bdd tmp = bddfalse; - - /* Repeat until no new states are found */ - do - { - tmp = reachedStates; - - /* Calculate: Newset = (exists V_cur. transRel & Reached)[cur/next] */ - bdd newset; - newset = reachedStates & transRel; - newset = bdd_exist(newset, currentStateVar); - newset = bdd_replace(newset, p); - - cout << "Front: " << (newset - reachedStates) << endl; - - /* Add the new states to the found states */ - reachedStates = reachedStates | newset; - } - while (tmp != reachedStates); -} - - -main() -{ - /* Initialize BuDDy and declare two interleaved FDD variable blocks - * with the domain [0..7] */ - int domain[2] = {8,8}; - - bdd_init(100,100); - fdd_extdomain(domain, 2); - - /* Initialize the transition relation with no transitions */ - bdd T = bddfalse; - - /* Add all the transitions (from state 'i' to state 'i+1') */ - for (int i=0 ; i<8 ; i++) - { - /* Set the current state to be state 'i' */ - bdd current = fdd_ithvar(0,i); - - /* Set the next state to be state 'i+1' */ - bdd next = fdd_ithvar(1, (i+1) % 8); - - /* Add the transition */ - T = T | (current & next); - } - - cout << fddset << "Transition relation: " << T << endl << endl; - - /* Calculate the reachable statespace */ - findStateSpace(T); -} diff --git a/buddy/examples/milner/milner.cxx b/buddy/examples/milner/milner.cxx index 8fc52fea1..808604050 100644 --- a/buddy/examples/milner/milner.cxx +++ b/buddy/examples/milner/milner.cxx @@ -1,6 +1,5 @@ #include #include -#include #include #include "bdd.h" #include @@ -98,6 +97,7 @@ bdd reachable_states(bdd I, bdd T) int main(int argc, char** argv) { + using namespace std ; int n; if(argc < 2) { @@ -113,8 +113,6 @@ int main(int argc, char** argv) exit(2); } - long clk1 = clock(); - bdd_init(500000, 50000); bdd_setvarnum(N*6); @@ -164,8 +162,6 @@ int main(int argc, char** argv) bdd T = transitions(t,tp,h,hp,c,cp); bdd R = reachable_states(I,T); - long clk2 = clock(); - bddStat s; bdd_stats(&s); @@ -175,8 +171,6 @@ int main(int argc, char** argv) cout << endl << "Number of nodes in T is " << bdd_nodecount( T ) << endl; cout << "Number of nodes in R is " << bdd_nodecount( R ) << endl << endl; - cout << (float)(clk2 - clk1)/(float)(CLOCKS_PER_SEC) << " sec.\n"; - //bdd_printstat(); cout << "Nodenum: " << bdd_getnodenum() << endl; bdd_done(); diff --git a/buddy/examples/money/money.cxx b/buddy/examples/money/money.cxx index 26ede1d8a..650f22e49 100644 --- a/buddy/examples/money/money.cxx +++ b/buddy/examples/money/money.cxx @@ -16,7 +16,8 @@ using namespace std; int main(void) { - // Allocate 11 domains with room for up to 3*10 + using namespace std ; + // Allocate 11 domains with room for up to 3*10 static int dom[11] = {30,30,30,30,30,30,30,30,30,30,30}; bdd_init(10000,10000); diff --git a/buddy/examples/queen/queen.cxx b/buddy/examples/queen/queen.cxx index 85f878914..3498116fc 100644 --- a/buddy/examples/queen/queen.cxx +++ b/buddy/examples/queen/queen.cxx @@ -76,6 +76,7 @@ void build(int i, int j) int main(int ac, char **av) { + using namespace std ; int n,i,j; if (ac != 2) diff --git a/buddy/examples/solitare/solitare.cxx b/buddy/examples/solitare/solitare.cxx index 5f0bc2216..4f6829dc1 100644 --- a/buddy/examples/solitare/solitare.cxx +++ b/buddy/examples/solitare/solitare.cxx @@ -1,5 +1,4 @@ #include -#include #include #include #include @@ -121,6 +120,7 @@ bdd make_move(int src, int tmp, int dst) void make_transition_relation(void) { + using namespace std ; T = bddfalse; for (int n=0 ; moves[n][0]!=moves[n][1] ; n++) @@ -160,9 +160,9 @@ void iterate(void) next = bdd_replace(next, pair); reachable |= next; - cout << cou << ": " << bdd_nodecount(reachable) + std::cout << cou << ": " << bdd_nodecount(reachable) << " nodes, " << bdd_satcount(reachable)/dummyStateNum - << " states\n" << flush; + << " states\n" << std::endl ; cou++; } while (tmp != reachable); @@ -186,10 +186,10 @@ void iterate_front(void) front = next - reachable; reachable |= front; - cout << cou << ": " << bdd_nodecount(reachable) - << " , " << bdd_satcount(reachable)/dummyStateNum << endl; - cout << cou << ": " << bdd_nodecount(front) - << " , " << bdd_satcount(front)/dummyStateNum << endl; + std::cout << cou << ": " << bdd_nodecount(reachable) + << " , " << bdd_satcount(reachable)/dummyStateNum << std::endl; + std::cout << cou << ": " << bdd_nodecount(front) + << " , " << bdd_satcount(front)/dummyStateNum << std::endl; cou++; } while (tmp != reachable); @@ -212,15 +212,9 @@ void setup(void) int main(void) { - long c1, c2; - - c1 = clock(); - setup(); iterate(); - c2 = clock(); - printf("Time: %.1f sec.\n", ((float)(c2-c1))/CLOCKS_PER_SEC); system("ps aux | grep \"./solitare\" | grep -v \"grep\""); } diff --git a/buddy/src/Makefile.am b/buddy/src/Makefile.am index 596b56b70..9bcf8f505 100644 --- a/buddy/src/Makefile.am +++ b/buddy/src/Makefile.am @@ -1,5 +1,5 @@ -# For -AM_CPPFLAGS = -I$(top_builddir) +# For +AM_CPPFLAGS = -I$(top_builddir) -DVERSION=23 include_HEADERS = bdd.h fdd.h bvec.h diff --git a/buddy/src/kernel.h b/buddy/src/kernel.h index d80d30933..580311724 100644 --- a/buddy/src/kernel.h +++ b/buddy/src/kernel.h @@ -28,7 +28,7 @@ ========================================================================*/ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/src/kernel.h,v 1.4 2003/05/20 08:22:36 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/src/kernel.h,v 1.5 2004/06/28 15:22:13 adl Exp $ FILE: kernel.h DESCR: Kernel specific definitions for BDD package AUTH: Jorn Lind @@ -119,8 +119,6 @@ extern bddCacheStat bddcachestats; /*=== KERNEL DEFINITIONS ===============================================*/ -#define VERSION 22 - #define MAXVAR 0x1FFFFF #define MAXREF 0x3FF