> > Hi,
> > I am using Cudd-2.3.0 for my dissertation project, and I am in the following situation:
> >
> > DdNode *
> > Cudd_bddExistAbstract(
> > DdManager * manager,
> > DdNode * f,
> > DdNode * cube
> > )
> >
> > Existentially abstracts all the variables in cube from f. Returns the abstracted BDD if successful; NULL otherwise.
> >
> > First FSM
> > 0-0-1-0-1---------1----------------------------------------------------------------------------------------------------------------------- 1
> > 0-1-0-0-1---------1----------------------------------------------------------------------------------------------------------------------- 1
> > 1-0-1-1-0---------0----------------------------------------------------------------------------------------------------------------------- 1
> > 1-1-0-1-0---------0----------------------------------------------------------------------------------------------------------------------- 1
> > Second FSM
> > 0-0-0-0-0-0-1-1-0-0-0-0-0-------------------------0--------------------------------------------------------------------------------------- 1
> > 0-0-0-0-0-1-0-0-0-1-0-0-0-------------------------0--------------------------------------------------------------------------------------- 1
> > 0-0-0-0-1-0-0-0-0-0-0-1-0-------------------------0--------------------------------------------------------------------------------------- 1
> > 0-0-0-1-0-0-0-0-0-0-0-0-1-------------------------0--------------------------------------------------------------------------------------- 1
> > 0-0-1-0-0-0-0-0-0-0-1-0-0-------------------------1--------------------------------------------------------------------------------------- 1
> > 0-1-0-0-0-0-0-0-1-0-0-0-0-------------------------0--------------------------------------------------------------------------------------- 1
> > 1-0-0-0-0-0-1-0-1-0-0-0-0-------------------------0--------------------------------------------------------------------------------------- 1
> > 1-0-0-0-0-1-0-0-1-0-0-0-0-------------------------0--------------------------------------------------------------------------------------- 1
> > 1-0-0-0-1-0-0-0-0-1-0-0-0-------------------------0--------------------------------------------------------------------------------------- 1
> > 1-0-0-1-0-0-0-0-0-0-1-0-0-------------------------0--------------------------------------------------------------------------------------- 1
> > 1-0-1-0-0-0-0-0-0-0-0-0-1-------------------------1--------------------------------------------------------------------------------------- 1
> > 1-1-0-0-0-0-0-0-0-1-0-0-0-------------------------0--------------------------------------------------------------------------------------- 1
> > S1
> > ------1-1--------------------------------------------------------------------------------------------------------------------------------- 1
> > S2
> > --------------1-1-1-1-1-1----------------------------------------------------------------------------------------------------------------- 1
> >
> > lambda1 = Cudd_bddExistAbstract (fsmdd->DDm, fsmdd1->transition, S1);
> > lambda2 = Cudd_bddExistAbstract (fsmdd->DDm, fsmdd2->transition, S2);
> >
> > Here I've got the following results:
> > lambda1
> > 0-0-1-------------1----------------------------------------------------------------------------------------------------------------------- 1
> > 0-1-0-------------1----------------------------------------------------------------------------------------------------------------------- 1
> > 1-0-1-------------0----------------------------------------------------------------------------------------------------------------------- 1
> > 1-1-0-------------0----------------------------------------------------------------------------------------------------------------------- 1
> > lambda2
> > --0-0-0-0-0-1-------------------------------------0--------------------------------------------------------------------------------------- 1
> > --0-0-0-0-1-0-------------------------------------0--------------------------------------------------------------------------------------- 1
> > --0-0-0-1-0-0-------------------------------------0--------------------------------------------------------------------------------------- 1
> > --0-0-1-0-0-0-------------------------------------0--------------------------------------------------------------------------------------- 1
> > --0-1-0-0-0-0-------------------------------------1--------------------------------------------------------------------------------------- 1
> > --1-0-0-0-0-0-------------------------------------0--------------------------------------------------------------------------------------- 1
> >
> > it seemns that lambda1 is correct, but lambda2 is not.
> > =============================================================================================================================================
> > I want to obtain for lambda2 this:
> >
> > lambda2
> > 0-0-0-0-0-0-1-------------------------------------0--------------------------------------------------------------------------------------- 1
> > 0-0-0-0-0-1-0-------------------------------------0--------------------------------------------------------------------------------------- 1
> > 0-0-0-0-1-0-0-------------------------------------0--------------------------------------------------------------------------------------- 1
> > 0-0-0-1-0-0-0-------------------------------------0--------------------------------------------------------------------------------------- 1
> > 0-0-1-0-0-0-0-------------------------------------1--------------------------------------------------------------------------------------- 1
> > 0-1-0-0-0-0-0-------------------------------------0--------------------------------------------------------------------------------------- 1
> > 1-0-0-0-0-0-1-------------------------------------0--------------------------------------------------------------------------------------- 1
> > 1-0-0-0-0-1-0-------------------------------------0--------------------------------------------------------------------------------------- 1
> > 1-0-0-0-1-0-0-------------------------------------0--------------------------------------------------------------------------------------- 1
> > 1-0-0-1-0-0-0-------------------------------------0--------------------------------------------------------------------------------------- 1
> > 1-0-1-0-0-0-0-------------------------------------1--------------------------------------------------------------------------------------- 1
> > 1-1-0-0-0-0-0-------------------------------------0--------------------------------------------------------------------------------------- 1
> >
> > Where do you think it might be the problem?
> > Thank you,
> > Codrin.
codrin@sdf.lonestar.org
SDF Public Access UNIX System - http://sdf.lonestar.org
This archive was generated by hypermail 2b30 : Wed May 01 2002 - 04:38:12 MDT