/****************************************************************************/
/*                                                                          */
/*                      Chaine de CAO & VLSI   Alliance                     */
/*                                                                          */
/*    Produit :  Synthetiseur de FSM                                       */
/*    Fichier :  syf_verif.c                                                  */
/*                                                                          */
/*    (c) copyright 1992 Laboratoire MASI equipe CAO & VLSI                 */
/*    Tous droits reserves                                                  */
/*    Support : e-mail cao-vlsi@masi.ibp.fr                                 */
/*                                                                          */
/*    Auteur(s) :  C. Sarwary                            le : 04/03/1992     */
/*                                                                          */
/*    Modifie par :                                     le : ../../....     */
/*    Modifie par :                                     le : ../../....     */
/*    Modifie par :                                     le : ../../....     */
/*                                                                          */
/***************************************************************************/
#include <stdio.h>
#include MUT_H
#include LOG_H
#include "../beh104/beh104.h"
#include "syf_auto.h"
#include "syf_must.h"
#include "syf_beh2fsm.h"
extern int syf_scan ;
typedef struct doubleI
	{
	struct doubleI *next ;
	int newI, lastI ;
	}*pDoubleI ;
/*---------------------------------------------------------
verifCode	: Verifie la coherence du codage .
----------------------------
parametres	: rien .
----------------------------
return		: void.
-----------------------------------------------------------*/
verifCode()
{
pCode code,code2 ;
int i, j ;

code = autoSys->code ;
for(i = 0; i < autoSys->numberState; i++)
	{
	code2 = code ;
	code2++ ;
	for(j = i + 1; j < autoSys->numberState; j++)
		{
		if(code->code == code2->code)
			{
			printf("Tow states are the same code : H%x\n",code->code) ;
			exit(-1) ;
			}
		code2++ ;
		}
	code++ ;
	}
}
/*---------------------------------------------------------
fsm_verify	: Verifie la coherence de FSM .
----------------------------
parametres	: rien .
----------------------------
return		: void.
-----------------------------------------------------------*/
fsm_verify()
{
pState state ;
pTrans trans, trans2 ;
int i, j, erFlag ;
pStack stack ;

printf("Coherence verification of %s\n",autoSys->name) ;

	/* Detection des Etats Puits */
state = autoSys->state ;

for(i = 0; i < autoSys->numberState;i++)
	{
	if(state->trans == NULL)
		if(flagPile)
			{
			erFlag = 1;
			stack = autoSys->stack ;
			while(stack && erFlag)
				{
				if((stack->ctrl == PUSH) && stack->returnStatelabel == i)
					erFlag = 0 ;
				stack = stack->next ;
				}
			if(erFlag == 1)
				printf("warning : No transition to %s state\n",state->name) ;
			}
		else
			printf("warning : No transition to %s state\n",state->name) ;
	state++ ;
	}

	/* Detection des Etats source */
for(i = 0; i < autoSys->numberState;i++)
	{
	state = autoSys->state ;
	erFlag = 1 ;
	for(j = 0; (j < autoSys->numberState) && erFlag;j++)
		{
		trans = state->trans ;
		while(trans && erFlag)
			{
			if(trans->sPlabel == i)
				erFlag = 0 ;
			trans = trans->next ;
			}
		state++ ;
		}
	if(erFlag)
		{
		if(flagPile)
			{	
			stack = autoSys->stack ;
			while(stack && erFlag)
				{
				if((stack->ctrl == POP) && stack->curentStatelabel == i)
					erFlag = 0 ;
				stack = stack->next ;
				}
			}
		if(erFlag)
			printf("warning : No transition from %s state\n",(autoSys->state+i)->name) ;
		}
	}

	/* verify if there is no more than one transition with the same condition */
for(i = 0; i < autoSys->numberState;i++)
	{
	trans = (autoSys->state + i)->trans ;
	while(trans)
		{
		state = autoSys->state + i + 1 ;
		for(j = i + 1; j < autoSys->numberState;j++)
			{
			trans2 = state->trans ;
			while(trans2)
				{
				if(trans->sPlabel == trans2->sPlabel)
					{
					if(equalExpr(trans->abl,trans2->abl))
						{
						printf("Warning : transitions %s->%s and %s->%s have same transition condition\n",(autoSys->state+ trans->sPlabel)->name,state->name,
						  (autoSys->state+ trans->sPlabel)->name,
						  (autoSys->state + i)->name) ;
						}
					}
				trans2 = trans2->next ;
				}
			state++ ;
			}
		trans = trans->next ;
		}
	}
/*
state = autoSys->state ;
for(i = 0; i < autoSys->numberState;i++)
	{
	trans = state->trans ;
	while(trans)
		{
		trans2 = trans->next ;
		while(trans2)
			{
			if(equalExpr(trans->abl,trans2->abl))
				{
				printf("Warning : transitions %s->%s and %s->%s have same \ 
					transition condition\n",(autoSys->state+
					trans->sPlabel)->name,state->name,(autoSys->state+
					trans2->sPlabel)->name,state->name) ;
				}
			trans2 = trans2->next ;
			}
		trans = trans->next ;
		}
	state++ ;
	}
*/
/*** Coherence des pragmas par rapport aux options ****/
/** scan-path **/

if(syf_scan)
	{
	if(autoSys->testMode == NULL || autoSys->scin == NULL ||
					autoSys->scout == NULL)
		{
		printf("Pragma for scan-path signals missed\n") ;
		exit(-1) ;
		}
	if(!existName(autoSys->input,autoSys->numberIn,autoSys->scin))
		{
		printf("scan-path signal '%s' missed\n",autoSys->scin) ;
		exit(-1) ;
		}
	if(!existName(autoSys->input,autoSys->numberIn,autoSys->testMode))
		{
		printf("scan-path signal '%s' missed\n",autoSys->testMode) ;
		exit(-1) ;
		}
	if(existOut(autoSys->scout) == -1)
		{
		printf("scan-path signal '%s' missed\n",autoSys->scout) ;
		exit(-1) ;
		}
	}
}
/*---------------------------------------------------------
givMainProcess	: Recherche le process principal( process de transition d'etats.
----------------------------
parametres	: tete de process .
----------------------------
return		: le process principal.
-----------------------------------------------------------*/
struct syf_bepcs *givMainProcess(pcs)
struct syf_bepcs *pcs ;
{
chain_list *sens ;

while(pcs)
	{
	sens = pcs->SENSITIVITY ;
	while(sens) 
		{
		if(!strcmp((char *)sens->DATA,CURENT_STATE)) 
			return(pcs) ;
		sens = sens->NEXT ;
		}
	pcs = pcs->NEXT ;
	}
printf("ERROR : %s must be a sensitivity signal for the main process\n",CURENT_STATE);
exit(-1) ;
}
/*---------------------------------------------------------
syf_beh_verify	: Verifie la coherence de befig pour FSM .
----------------------------
parametres	: beh .
----------------------------
return		: void.
-----------------------------------------------------------*/
syf_beh_verify(beh)
struct syf_befig *beh ;
{
struct syf_bepcs *pcs ;
struct ptype *ins ;
chain_list *sens ;

printf("Verification ...\n") ;
pcs = beh->BEPCS ;
pcs = givMainProcess(pcs) ;

	/* Pas de NEXT_STATE dans la list de sensitivity du process principal */

sens = pcs->SENSITIVITY ;
while(sens) 
	{
	if(!strcmp((char *)sens->DATA,NEXT_STATE)) 
		{
		printf("ERROR : Illegal sensitivity : %s, in the main process\n",(char *)sens->DATA);
		exit(-1) ;
		}
	sens = sens->NEXT ;
	}

	/* pas d'affectation de stack ni de CURENT_STATE dans le process principal*/
ins = pcs->INSTRUCTION ;
while(ins)
	{
	switch(ins->TYPE)
		{
		case BEH_BECAS :
			verifWhen((struct syf_becas *)(ins->DATA)) ;	
			break ;
		case BEH_BEIFS :
			verifIf((struct syf_beifs *)(ins->DATA),0) ;
			break ;
		case BEH_BEASG :
			verifAsg((struct syf_beasg *)(ins),1) ;
			break ;
		default :
			printf("ERROR : Unknown operator\n") ; 
			exit(-1) ;
		}
	ins = ins->NEXT ;

	/*syf_displayChain_list(pcs->SENSITIVITY) ;*/
	}
}
/*---------------------------------------------------------
verifIf	: Verifie les parametres d'un IF pour les automates. 
----------------------------
parametres	: ifs .
			  mode : Si 1 verifie si une sortie n'est pas assigne'e.
----------------------------
return		: void.
-----------------------------------------------------------*/
verifIf(ifs,mode)
struct syf_beifs *ifs ;
int mode ;
{
verifAsg((struct ptype *)ifs->CNDTRUE, mode) ;
verifAsg((struct ptype *)ifs->CNDFALSE, mode) ;
}
/*---------------------------------------------------------
verifWhen	: Verifie les parametres d'un WHEN pour les automates. 
----------------------------
parametres	: cas .
----------------------------
return		: void.
-----------------------------------------------------------*/
verifWhen(cas)
struct syf_becas *cas ;
{
struct syf_becho *choice ;
struct ptype *ins ;
int i ;

choice = cas->CHOICE ;
for(i = 0; i < (int)cas->SIZE -1; i++)
	{
	ins = choice[i].INSTRUCTION ;
	verifAsg(ins,0) ;
	}
}
/*---------------------------------------------------------
verifAsg	: Verifie les affectations pour un automate :
			  pas d'affectation de STACK_i.
----------------------------
parametres	: typ .
			  mode : Si 1 verifie si une sortie n'est pas assigne'e.
			  Aucune assignation de sortie n'est autorise'e en dehors d'un
			  etat.
----------------------------
return		: void.
-----------------------------------------------------------*/
verifAsg(typ,mode)
struct ptype *typ ;
int mode ;
{
struct ptype *ins ;
struct syf_beasg *asg ;

ins = typ ;
while(ins)
	{
	switch(ins->TYPE)
		{
		case BEH_BEASG :
			asg = (struct syf_beasg *)(ins->DATA) ;
			if((flagPile && (!strncmp(STACK_NAME[0],asg->NAME,6))) || 
			  !strncmp(CURENT_STATE,asg->NAME,strlen(CURENT_STATE)))
				{
				printf("ERROR : Illegal assignement : %s\n",asg->NAME) ;
				exit(-1) ;
				}
			if(mode)
				{
				if(existOut(asg->NAME) != -1)
					{
					printf("SYF : Output(%s) can not be assigned without next_state assignment\n",asg->NAME) ;
					exit(-1) ;
					}
				}
			break ;
		case BEH_BECAS :
			verifWhen((struct syf_becas *)(ins->DATA)) ;
			break ;
		case BEH_BEIFS :
			verifIf((struct syf_beifs *)(ins->DATA),mode) ;
			break ;
		}
	ins = ins->NEXT ;
	}
}
/*---------------------------------------------------------
verifPushPop: Verifie l'exclusivite des imbrications des pushs. 
----------------------------
parametres	: .
----------------------------
return		: void.
-----------------------------------------------------------*/
verifPushPop()
{
pStack stack ;
int i, test ;
chain_list *lst ;

i = 1 ;
test = 1 ;
markAllPushPop() ;
while(test)
  {
  test = 0 ;
  stack = autoSys->stack ;
  while(stack)
	{
	lst = NULL ;
	if(stack->ctrl==POP && 
				(autoSys->state+stack->curentStatelabel)->user ==(void*)-2)
		{
		printf("\tPOP%d:%s\n",i,(autoSys->state+stack->curentStatelabel)->name);
		if(markSubAuto(stack->curentStatelabel,i,NULL,&lst))
			test = 1 ;
		else 
			(autoSys->state+stack->curentStatelabel)->user = NULL;/* traiter
							autrement qd remplacement */
		i++ ;
		}
	stack = stack->next ;
	}
  }
}
/*---------------------------------------------------------
markPop: marque tous les etats de POP a -2. 
----------------------------
parametres	: .
----------------------------
return		: void.
-----------------------------------------------------------*/
markPop()
{
pStack stack ;

stack = autoSys->stack ;
while(stack)
	{
	if(stack->ctrl == POP)
		(autoSys->state+stack->curentStatelabel)->user = (void *)-2 ;
	stack = stack->next ;
	}

}
/*---------------------------------------------------------
markAllPushPop: marque tous les etats de PUSH a -1, et POP a -2. 
----------------------------
parametres	: .
----------------------------
return		: void.
-----------------------------------------------------------*/
markAllPushPop()
{
pStack stack ;

stack = autoSys->stack ;
while(stack)
	{
	if(stack->ctrl == PUSH)
		(autoSys->state+stack->curentStatelabel)->user = (void *)-1 ;
	else
	  if(stack->ctrl == POP)
		(autoSys->state+stack->curentStatelabel)->user = (void *)-2 ;
	stack = stack->next ;
	}

}
/*---------------------------------------------------------
markSubAuto: mark le sous automate a partir d'un pop passe en param jusqu'au 
			 push. Fonction recursive.
----------------------------
parametres	: label de l'etat pop.
----------------------------
return		:1 : si recursif, 0 si non 
-----------------------------------------------------------*/
markSubAuto(label,mark,cnd,lst)
int label, mark ;
chain_list *cnd ;
chain_list **lst ;
{
pState state ;
pTrans trans ;

*lst = addchain(*lst,label) ;
state = autoSys->state + label ;
if(state->user != (void *)-1)
	{
	state->user = (void *)mark ;
	trans = state->trans ;
	if(!trans)/* on suppose pas de trans => trans par POP */
			{
			printf("-----recursion\n") ;
			return(1) ;
			}
	while(trans)
		{
		/*printf("\t\t%s\n",(autoSys->state+trans->sPlabel)->name);*/
		if(label != trans->sPlabel && ((autoSys->state + trans->sPlabel)->user != (void *)mark))
			markSubAuto(trans->sPlabel,mark,trans->abl,lst) ;
		trans = trans->next ;
		}
	}
else
	{
	if(isPush1(label,cnd))
		printf("\t\t\tPUSH : %s\n",state->name) ;
	else
		{
		state->user = (void *)mark ;
		trans = state->trans ;
		if(!trans)
			{
			printf("-----recursion\n") ;
			return(1) ;
			}
		while(trans)
			{
			printf("\t\t%s\n",(autoSys->state+trans->sPlabel)->name);
			if(label != trans->sPlabel && ((autoSys->state + trans->sPlabel)->user != (void *)mark))
				{
				state->user = (void *)-1 ;
				markSubAuto(trans->sPlabel,mark,trans->abl,lst) ;
				}
			trans = trans->next ;
			}
		}
	}
return(0) ;
}
/*---------------------------------------------------------
isPush		: Verifie l'existence d'un PUSH avec curentState = label, et 
			  condition cnd.
----------------------------
parametres	: pC,label, retStateLabel, cnd 
----------------------------
return		: 1 : TRUE, 0 : FALSE.
-----------------------------------------------------------*/
isPush(pC,label,retStateLabel,cnd)
pCircuit pC ;
int label, retStateLabel ;
pNode cnd ;
{
pStack stack ;
pNode bdd ;

stack = autoSys->stack ;
while(stack)
	{
	if(stack->ctrl == PUSH && stack->returnStatelabel == retStateLabel)
		{
		bdd = ablToBddCct(pC,stack->abl) ;
		if(applyBinBdd(AND,bdd,cnd) == bdd)
			return(1) ;
		}
	stack = stack->next ;
	}
return(0) ;
}
/*---------------------------------------------------------
isPush1		: Verifie l'existence d'un PUSH avec curentState = label, et 
			  condition cnd.
----------------------------
parametres	: label, retStateLabel, cnd 
----------------------------
return		: 1 : TRUE, 0 : FALSE.
-----------------------------------------------------------*/
isPush1(label,cnd)
int label ;
chain_list *cnd ;
{
pStack stack ;

stack = autoSys->stack ;
while(stack)
	{
	if(stack->ctrl == PUSH)
		{
		if(equalExpr(stack->abl,cnd))
			return(1) ;
		}
	stack = stack->next ;
	}
return(0) ;
}
/*---------------------------------------------------------
displayLst	: Visualisation d'une list chainee avec le champ data comme le label d'un etat. 
----------------------------
parametres	: lst 
----------------------------
return		: 
-----------------------------------------------------------*/
displayLst(lst)
chain_list *lst ;
{
chain_list *curLst ;

curLst = lst ;

printf("------------ Display Push2Pop States List -------------\n") ;
while(curLst)
	{
	printf("%s\n",(autoSys->state + (int)curLst->DATA)->name) ;
	curLst = curLst->NEXT ;
	}
fflush(stdout) ;
}
/*---------------------------------------------------------
flattenStack: met a plat un STACK FSM(elimine le STACK. 
----------------------------
parametres	: 
----------------------------
return		: 
-----------------------------------------------------------*/
flattenStack()
{
int test,i, j, label,  initStateNum, retStateLabel ;
pStack stack ;
chain_list *lst, *lst2, *curLst, *allList, *invLst() ;
pState state ;
pTrans trans,trans2, copyTrans() ;
pCircuit pC ;
pNode pushCnd ;

					printf("---------- FlattenStack -----------\n") ;
pC = makeLocalBdd() ;
initStateNum = autoSys->numberState ;
i = 1 ;
test = 1 ;
allList = NULL ;
markAllPushPop() ;
while(test)
  {
  test = 0 ;
  stack = autoSys->stack ;
  while(stack)
	{
	if(stack->ctrl == PUSH) 
		{
		label = stack->curentStatelabel ;
		retStateLabel = stack->returnStatelabel ;
		pushCnd = ablToBddCct(pC,stack->abl) ;
		if(syf_trace)
			{
  			printf("--------- index : %d, Push State : %s ------\n",i,(autoSys->state + label)->name) ;
			printf("--> ReturnState : %s\n",(autoSys->state + retStateLabel)->name) ;
			}
		state = autoSys->state ;
		for(j = 0; j < initStateNum; j++)
			{
			trans = state->trans ;
			trans = copyTrans(trans) ;
			trans2 = trans ;
			/*printf("state Essaye : %s\n",(autoSys->state + j)->name) ;*/
			while(trans)
				{
				if(label == trans->sPlabel && j!=label )
					{
					if(applyBinBdd(AND,trans->bdd,pushCnd) == pushCnd && 
							isPush(pC,label,retStateLabel,trans->bdd))
						{
						lst = NULL ;
						lst = addchain(lst,label) ;/*le 1er label est tj celui de l'etat PUSH */
						if(!(markPush2Pop(j,i,NULL,&lst,label)))
							{
							test = 1 ;
							/*freechain(lst) ;*/
							lst = NULL ;
							i++ ; 
							break ; /* cas de recursion */
							}
						else
							{
							if(syf_trace)
								printf("--> nextState : %s\n",state->name) ;
							if(allList == NULL)
								{
								lst2 = lst ;
								lst2 = invLst(lst) ;
								allList = lst2->NEXT ;
								curLst = allList ;
								}
							else
								{
								lst2 = lst ;
								lst2 = invLst(lst) ;
								while(curLst)
									{
									if(curLst->NEXT == NULL)
										{
										curLst->NEXT = lst2->NEXT ;
										break ;
										}
									curLst = curLst->NEXT ;
									}
								}
							if(syf_trace)
								{
								printf("--> Sub-FSM States list :\n") ;
								displayLst(lst) ;
								}
							markPop() ;
							if(!syf_trace)
								{
								printf(".") ;
								fflush(stdout) ;
								}
							doubleSubFsm(pC,lst,retStateLabel,pushCnd,i) ;
							if(!syf_trace)
								{
								printf("+") ;
								fflush(stdout) ;
								}
							/*unMark(&lst)*/
							markPop() ;
							i++ ; 
							break ;
							}
						}
					}
				trans = trans->next ;
				}
			freeTrans(trans2) ;
			state++ ;
			}
	(autoSys->state + stack->curentStatelabel)->user = (void *)-5 ; 
		}
	stack = stack->next ;
	}
  }
flagPile = 0 ;
if(!syf_trace)
	printf("\nMax State Number : %d\n",autoSys->numberState) ;
regenerState(allList) ;
autoSys->stack = NULL ;
if(syf_trace)
	{
	printf("--> Flatten Final States List :\n") ;
	displayStateName() ;
	}
	/*displayAuto() ;*/
destroyCct(pC) ;
if(!syf_trace)
	printf("\nState Number : %d\n",autoSys->numberState) ;
printf("---------- End of FlattenStack -----------\n") ;
}
/*---------------------------------------------------------
markPush2Pop: marque tous les etats de PUSH a POP. 
----------------------------
parametres	: label,mark,cnd,lst,pushState.
----------------------------
return		: void.
-----------------------------------------------------------*/
markPush2Pop(label,mark,cnd,lst,pushState)
int label, mark ;
pNode cnd ;
chain_list **lst ;
int pushState ;
{
int i,test ;
pState state ;
pTrans trans ;

/*printf("%d<-->%s\n",mark,(autoSys->state + label)->name) ;*/
if((autoSys->state + label)->user == (void *)-1) /******* CAS DE PUSH *********/
	{
	if(label == pushState)
		{
		printf("ERROR : recursive PUSH by %s\n",(autoSys->state +label)->name) ;
		exit(-1) ;
		}
	if(syf_trace)
		{
		printf("---- RECURSION ----> ") ;
		printf("state : %s\n",(autoSys->state + label)->name) ;
		fflush(stdout) ;
		}
	return(0) ; /* recursion */
	}

*lst = addchain(*lst,label) ; /* dans le cas de NOP ou POP */

(autoSys->state + label)->user = (void *)mark ;

state = autoSys->state ;
for(i = 0; i < autoSys->numberState; i++)
	{
	trans = state->trans ;
	while(trans)
		{
		if(trans->sPlabel != -1)
			{
			if(label == trans->sPlabel && ((autoSys->state + i)->user != (void *)mark))
				{
				test = markPush2Pop(i,mark,trans->bdd,lst,pushState);/*voir le cas de etat pop a +ieurs branch*/
				if(test == 0)
					return(0) ;
				}
			}
		trans = trans->next ;
		}
		/*printf("FIN DE TRANS\n") ;*/
	state++ ;
	}
					/********** CAS DE POP **********/

/*printf("**************** POP : %s **********\n",(autoSys->state + label)->name);*/
return(1) ;
}
/*---------------------------------------------------------
doubleSubFsm: dedouble un sous graphe. 
----------------------------
parametres	: lst, retStateLabel,pushCnd, index pour nouveaux etats.
----------------------------
return		: void.
-----------------------------------------------------------*/
doubleSubFsm(pC,lst,retStateLabel,pushCnd,index)
pCircuit pC ;
chain_list *lst ;
int retStateLabel ;
pNode pushCnd ;
int index ;
{
chain_list *newLst, *popLst, *abl, *invLst(), *givePopLst() ;
chain_list *givePopCnd() ;
int newState, label ;
pTrans trans ;

newLst = invLst(lst) ;
popLst = givePopLst(lst) ;
if(popLst == NULL)
	{
	printf("PUSH state without POP detected\n") ;
	exit(-1) ;
	}
		/************ Traitement de l'etat PUSH ************/
label = (int)(newLst->DATA) ;

delFromStack(pC,label,retStateLabel,pushCnd) ;

if(syf_trace)
	{
	printf("-->POP states list :\n") ;
	displayLst(popLst) ;
	}
while(popLst)
	{
	abl = givePopCnd((int)(popLst->DATA)) ;
	newState = createState(nameI((autoSys->state + (int)popLst->DATA)->name,index),NULL,NULL,NULL) ;
	trans = createTrans(abl,newState) ;
	trans->bdd = ablToBddCct(pC,abl) ;
	/*printf("ajout de %s vers %s\n",(autoSys->state + newState)->name,(autoSys->state + retStateLabel)->name) ;*/
	ajoutTrans(retStateLabel,trans) ;
	/*displayTrans(autoSys->state + label) ;*/
	popLst = popLst->NEXT ;
	}
newLst = newLst->NEXT ;

		/************ Autre etats (POP et NOP) *************/
doubleState(pC,newLst,index,label,pushCnd) ;
}
/*---------------------------------------------------------
givePopCnd: Donne la condition pour que un pop soit execute'. 
----------------------------
parametres	: label.
----------------------------
return		: able de la condition.
-----------------------------------------------------------*/
chain_list *givePopCnd(label)
int label ;
{
pStack stack ;
chain_list *abl ;

abl = NULL ;
stack = autoSys->stack ;
while(stack && abl == NULL)
	{
	if(stack->curentStatelabel == label && stack->ctrl == POP)
		abl = stack->abl ;
	stack = stack->next ;
	}
if(abl == NULL)
	{
	printf("%s is not a POP state\n",(autoSys->state + label)->name) ;
	exit(-1) ;
	}
return(abl) ;
}
/*---------------------------------------------------------
doubleState : double les etats de la list avec les changement des noms.
----------------------------
parametres	: newLst, index, pushStateLabel, pushCnd.
----------------------------
return		: .
-----------------------------------------------------------*/
doubleState(pC,newLst, index,pushStateLabel,pushCnd)
chain_list *newLst ;
int index, pushStateLabel ;
pNode pushCnd ;
{
chain_list *curLst ;
int label, newLabel ;
pTrans trans, lastTrans ;

createDoubleState(newLst,index) ;
			/****** L'etat suivant un PUSH : C'est le premier etat de la list ******/
			/** Elimination de la transition de push pour l'etat suivant un PUSH **/
label = (int)newLst->DATA ;
trans = (autoSys->state + (int)newLst->DATA)->trans ;
lastTrans = trans ;
/*printf("--> PUSH : %s\n",(autoSys->state + pushStateLabel)->name) ;
printf("ETAT SUIVANT UN PUSH : %s\n",(autoSys->state + label)->name) ;*/
while(trans)
	{
	/*printf("ETAT PUSH : %s\n",(autoSys->state + trans->sPlabel)->name) ;*/
	/*displayExpr(trans->abl) ;*/
	if(trans->sPlabel == pushStateLabel && applyBinBdd(AND,trans->bdd,pushCnd) == pushCnd)
		{
		if(trans == lastTrans)
			{
			freeExpr(trans->abl) ;
			(autoSys->state + label)->trans = trans->next ;
			/*printf("Elimination de %s vers %s\n",(autoSys->state + trans->sPlabel)->name,(autoSys->state + label)->name) ;*/
			/*free(trans) ;*/
			trans = (autoSys->state + label)->trans ;
			}
		else
			{
			freeExpr(trans->abl) ;
			/*printf("Elimination de %s vers %s\n",(autoSys->state + trans->sPlabel)->name,(autoSys->state + label)->name) ;*/
			/*free(trans) ;*/
			lastTrans->next = trans->next ;
			trans = lastTrans ;
			}
		break ;
		}
	lastTrans = trans ;
	trans = trans->next ;
	}

curLst = newLst ;
label = giveLabel(nameI((autoSys->state + (int)curLst->DATA)->name,index)) ;
ajoutTrans(label,createTrans(bddToAblCct(pC,pushCnd),pushStateLabel)) ;
((autoSys->state + label)->trans)->bdd = pushCnd ;
trans = (autoSys->state + label)->trans ;
while(trans)
	{
	if(isLabel(newLst,trans->sPlabel) || pushStateLabel == trans->sPlabel)
		{
		newLabel = getLabel(newLst,trans->sPlabel,index) ;
		if(newLabel != trans->sPlabel) /* Sinon il s'agit d'un autre chemin de push */
			{
			/*printf("ajout de %s vers %s\n",(autoSys->state +newLabel)->name,(autoSys->state +label)) ;*/
			ajoutTrans(label,createTrans(trans->abl,newLabel)) ;
			((autoSys->state + label)->trans)->bdd = trans->bdd ;
			}
		}
	trans = trans->next ;
	}
		
			/****** Les autres etats ******/
curLst = curLst->NEXT ;
while(curLst)
	{
	label = giveLabel(nameI((autoSys->state + (int)curLst->DATA)->name,index)) ;
	trans = (autoSys->state + (int)(curLst->DATA))->trans ;
	while(trans)
		{
		if(isLabel(newLst,trans->sPlabel))
			{
			newLabel = getLabel(newLst,trans->sPlabel,index) ;
			ajoutTrans(label,createTrans(trans->abl,newLabel)) ;
			((autoSys->state + label)->trans)->bdd = trans->bdd ;
			}
		trans = trans->next ;
		}
	curLst = curLst->NEXT ;
	}
if(syf_trace)
	{
	printf("--> State number : %d\n", autoSys->numberState) ;
	/*displayStateName() ;*/
	}
}
/*---------------------------------------------------------
getLabel : calcule un nouveau label, si label donne' se trouve dans la list
		   fourni, newLabel = fonc(label,index) sinon newLabel = label.
----------------------------
parametres	: lst, label, index.
----------------------------
return		: newLabel.
-----------------------------------------------------------*/
getLabel(lst,label, index)
chain_list *lst ;
int index, label ;
{
int newLabel ;
chain_list *curLst ;

curLst = lst ;
while(curLst)
	{
	if(label == (int)(curLst->DATA))
		{
		newLabel = giveLabel(nameI((autoSys->state+(int)curLst->DATA)->name,index));
		return(newLabel) ;
		}
	curLst = curLst->NEXT ;
	}
return(label) ;
}
/*---------------------------------------------------------
delFromStack : Elimine de la list des stack l'etat de label 'label', avec
			   condition 'cnd'.
----------------------------
parametres	: label,retStateLabel cnd.
----------------------------
return		: returnStatelabel correspondant sinon -1.
-----------------------------------------------------------*/
delFromStack(pC,label,retStateLabel, cnd)
pCircuit pC ;
int label, retStateLabel ;
pNode cnd ;
{
pStack stack, lastStack ;
chain_list *abl ;

stack = autoSys->stack ;
lastStack = NULL ;
while(stack)
	{
	if(stack->curentStatelabel == label && stack->returnStatelabel == retStateLabel && ablToBddCct(pC,stack->abl) == cnd)
		{
		if(lastStack == NULL)
			{
			freeExpr(stack->abl) ;
			autoSys->stack = stack->next ;
			}
		else	
			{
			freeExpr(stack->abl) ;
			lastStack->next = stack->next ;
			}
		break ;
		}
	lastStack = stack ;
	stack = stack->next ;
	}
}
/*---------------------------------------------------------
givePopLst: Donne la list des etats pop contenu dans 'lst'. 
----------------------------
parametres	: lst.
----------------------------
return		: list des POP.
-----------------------------------------------------------*/
chain_list *givePopLst(lst)
chain_list *lst ;
{
pStack stack ;
chain_list *popLst, *curLst ;

popLst = NULL ;
stack = autoSys->stack ;
while(stack)
	{
	if(stack->ctrl == POP)
		{
		curLst = lst ;
		while(curLst)
			{
			if(stack->curentStatelabel == (int)(curLst->DATA))
				popLst = addchain(popLst,stack->curentStatelabel) ;
			curLst = curLst->NEXT ;
			}
		}
	stack = stack->next ;
	}
return(popLst) ;
}
/*---------------------------------------------------------
invLst: Inverse l'ordre des elements d'un chain_list.
----------------------------
parametres	: lst.
----------------------------
return		: list inverse'.
-----------------------------------------------------------*/
chain_list *invLst(lst)
chain_list *lst ;
{
chain_list *invLst, *curLst ;

curLst = lst ;
invLst = NULL ;
while(curLst)
	{
	invLst = addchain(invLst,curLst->DATA) ;
	curLst = curLst->NEXT ;
	}
return(invLst) ;
}
/*---------------------------------------------------------
giveLabel: donne label d'un etat d'apres son nom.
----------------------------
parametres	: name.
----------------------------
return		: label.
-----------------------------------------------------------*/
giveLabel(name)
char *name ;
{
pState state ;
int i ;

state = autoSys->state ;
for(i = 0; i < autoSys->numberState; i++)
	if(!strcmp(name,(state + i)->name))
		return(i) ;
printf("%s : Unknown State\n") ;
exit(-1) ;
}
/*---------------------------------------------------------
createDoubleState: duplique les etats de la list. Ne copie pas les transitions.
----------------------------
parametres	: list,index.
----------------------------
return		: .
-----------------------------------------------------------*/
createDoubleState(list,index)
chain_list *list ;
int index ;
{
chain_list *curLst ;
pLocOut locOut, locOutDc, newLocOut, newLocOutDc, doubleLocOut() ;
pState state, newState ;
int label, newLabel ;

curLst = list ;
while(curLst)
	{
	label = (int)(curLst->DATA) ;
	state = autoSys->state + label ;
	newLabel = createState(nameI(state->name,index),NULL,NULL,NULL);
	newState = autoSys->state + newLabel ;
	locOut = state->locOut ;
	locOutDc = state->locOutDc ;
	newLocOut = NULL ;
	newLocOutDc = NULL ;
	while(locOut)
		{
		newLocOut = doubleLocOut(newLocOut,locOut) ;
		locOut = locOut->next ;
		}
	while(locOutDc)
		{
		newLocOutDc = doubleLocOut(newLocOutDc,locOutDc) ;
		locOut = locOutDc->next ;
		}
	newState->locOut = newLocOut ;
	newState->locOutDc = newLocOutDc ;
	curLst = curLst->NEXT ;
	}
}
/*---------------------------------------------------------
doubleLocOut: duplique un locOut.
----------------------------
parametres	: locOut.
----------------------------
return		: newLocOut.
-----------------------------------------------------------*/
pLocOut doubleLocOut(newLocOut,locOut)
pLocOut newLocOut, locOut ;
{
pLocOut curLocOut ;

curLocOut = (pLocOut)mbkalloc(sizeof(struct locOutput)) ;

curLocOut->label = locOut->label ;
curLocOut->abl = copyExpr(locOut->abl) ;
curLocOut->next = newLocOut ;

return(curLocOut) ;
}
/*---------------------------------------------------------
regenerState: regenere la table des etats en eliminant les etats dont
			  les labels sont dans la list.
----------------------------
parametres	: lst.
----------------------------
return		: .
-----------------------------------------------------------*/
regenerState(lst)
chain_list *lst ;
{
chain_list *newLst, *curLst, *lastLst ;
int i ;
pDoubleI dLab, curDLab ;

if(lst == NULL)
	{
	printf("regenereState : No state in the list.\n") ;
	exit(-1) ;
	}
/*displayCode(0) ;*/
curLst = lst ;
newLst = addchain(NULL,curLst->DATA) ;
curLst = curLst->NEXT ;
while(curLst) /* Elimine plusieurs apparitions */
	{
	if(!isLabel(newLst,(int)curLst->DATA))
		newLst = addchain(newLst,curLst->DATA) ;
	curLst = curLst->NEXT ;
	}
if(syf_trace)
	{
	printf("--> States Elimination :\n") ;
	displayLst(newLst) ;
	}
dLab = (struct doubleI *)mbkalloc(sizeof(struct doubleI)) ;
curDLab = dLab ;
curDLab->newI = -1 ;
curDLab->lastI = -1 ;
curDLab->next = NULL ;
for(i = autoSys->numberState -1; i >= 0 ; i--)
	{
	curLst = newLst ;
	while(curLst)
		{
		if(i > (int)curLst->DATA) 
			{
			curDLab->newI = (int)curLst->DATA ;
			curDLab->lastI = i ;
			curDLab->next = (struct doubleI *)mbkalloc(sizeof(struct doubleI)) ;
			curDLab = curDLab->next ;
			curDLab->newI = -1 ;
			curDLab->lastI = -1 ;
			curDLab->next = NULL ;
			if(curLst == newLst)
				{
				newLst = curLst->NEXT ;
				/*freechain(curLst) ;*/
				}
			else
				{
				lastLst->NEXT = curLst->NEXT ;
				/*freechain(curLst) ;*/
				}
			break ;
			}
		else
			{
			lastLst = curLst ;
			curLst = curLst->NEXT ;
			}
		}
	}
if(syf_trace) 
	{
	printf("--> States Index Exchange :\n") ;
	displayDoubleI(dLab) ;
	}
printf("Change of State Label\n") ;
for(i = 0; i < autoSys->numberState; i++)
	changeLabel(i,dLab) ;

printf("Copy of new States\n") ;
copyState(dLab) ;
}
/*---------------------------------------------------------
changeLabel : dans la structure state de label 'label' interchange toute les occurences de dLab . 
----------------------------
parametres	: label, dLab.
----------------------------
return		: .
-----------------------------------------------------------*/
changeLabel(label,dLab)
int label ;
pDoubleI dLab;
{
pDoubleI curLab;
pState state ;
pLocOut locOut, locOutDc ;
pTrans trans ;

state = autoSys->state + label ;
curLab = dLab ;
while(curLab && curLab->newI != -1)
	{
	trans = state->trans ;
	while(trans)
		{
		if(curLab->lastI == trans->sPlabel)
			trans->sPlabel = curLab->newI ;
		trans = trans->next ;
		}
	locOut = state->locOut ;
	while(locOut)
		{
		if(curLab->lastI == locOut->label)
			locOut->label = curLab->newI ;
		locOut = locOut->next ;
		}
	locOutDc = state->locOutDc ;
	while(locOutDc)
		{
		if(curLab->lastI == locOutDc->label)
			locOutDc->label = curLab->newI ;
		locOutDc = locOutDc->next ;
		}
	curLab = curLab->next ;
	}
}
/*---------------------------------------------------------
copyState   : copie les donnees de l'ancien etat dans le nouveau d'apres le list des doubleLabel . 
----------------------------
parametres	: dLab.
----------------------------
return		: .
-----------------------------------------------------------*/
copyState(dLab)
pDoubleI dLab;
{
pDoubleI curLab;
pState state, newState ;

curLab = dLab ;
/*displayStateName() ;*/
while(curLab && curLab->lastI != -1)
	{
	newState = autoSys->state + curLab->newI ;
	state = autoSys->state + curLab->lastI ;

	newState->name = state->name ;
	/*printf("%d : %s, code : %d\n",newState - autoSys->state,newState->name,(autoSys->code + curLab->newI)->code) ;*/
	fflush(stdout) ;

	/*freeTrans(newStat->trans) ;*/
	newState->trans = state->trans ;

	/*freeLocOut(newStat->locOut) ;*/
	newState->locOut = state->locOut ;

	/*freeLocOut(newStat->locOutDc) ;*/
	newState->locOutDc = state->locOutDc ;

	autoSys->numberState = autoSys->numberState -1 ;
	curLab = curLab->next ;
	}
/*displayStateName() ;*/
}
/*---------------------------------------------------------
isLabel		: Teste l'existence d'un entier dans une chain_list.
----------------------------
parametres	: lst, data.
----------------------------
return		: .
-----------------------------------------------------------*/
isLabel(lst,data)
chain_list *lst ;
int data ;
{
chain_list *curLst ;

curLst = lst ;
while(curLst)
	{
	if(data == (int)curLst->DATA)
		return(1) ;
	curLst = curLst->NEXT ;
	}
return(0) ;
}



displayDoubleI(dI) 
pDoubleI dI ;
{
pDoubleI curDI ;

printf("----------- DOUBLE INTEGER STRUCT DISPLAY ----------\n") ;
curDI = dI ;
while(curDI)
	{
	printf("%s <----> %s\n",(autoSys->state + curDI->lastI)->name,(autoSys->state +curDI->newI)->name);
	curDI = curDI->next ;
	if(curDI->newI == -1)
		break ;
	}
fflush(stdout) ;
}
/*---------------------------------------------------------
displayUser		: displays the user field of state structure.
----------------------------
parametres	: .
----------------------------
return		: .
-----------------------------------------------------------*/
displayUser()
{
pState state ;
int i ;

printf("--------------------- State user field display -----------------------\n") ;
state = autoSys->state ;
for(i = 0; i < autoSys->numberState; i++)
	printf("%s->user : %d\n",(state + i)->name,(int)(state + i)->user) ;
fflush(stdout) ;
}
/*---------------------------------------------------------
copyTrans	: copy a list of trans into a new list.
----------------------------
parametres	: trans.
----------------------------
return		: .
-----------------------------------------------------------*/
pTrans copyTrans(trans)
pTrans trans ;
{
pTrans newTrans, curTrans, curNewTrans ;

if(trans == NULL)
	return(NULL) ;
curTrans = trans ;
newTrans = createTrans(curTrans->abl,curTrans->sPlabel) ;
newTrans->bdd = curTrans->bdd ;
curNewTrans = newTrans ;
curTrans = curTrans->next ;

while(curTrans)
	{
	curNewTrans->next = createTrans(curTrans->abl,curTrans->sPlabel) ;
	curNewTrans->next->bdd = curTrans->bdd ;
	curTrans = curTrans->next ;
	curNewTrans = curNewTrans->next ;
	}
return(newTrans) ;
}
/*---------------------------------------------------------
markFsm	: marque les etats d'un automate, en partant de premier etat de la list
		  des etats et en parcourant ces transitions.
----------------------------
parametres	: .
----------------------------
return		: .
-----------------------------------------------------------*/
markkFsm()
{
}
