/* ****************************************************************
	File   : partialobs.c
	Author : Greg Stamp
	Date   : Jan, 2004

	Functions for dealing with partial observation.

   *************************************************************** */

#include "fsm_operators.c" /*not the best way to do this fsm_operators.o file not being created in makefile*/

char *M(char *, MASK_LIST *);
/*GLOBAL characters for po extract/remove*/
int GL_numsup, GL_Read_Del=-1;

/*stack of state list pointers*/
struct stack_stptr{
	ST_LIST *st_ptr; /*state pointers in LIFO order*/
	struct stack_stptr *next;
};

typedef struct stack_stptr STACKSTPTR;


/*list of transition names*/
struct tr_namelist{
	char name[MAX_LENGTH];
	struct tr_namelist *next;
};

typedef struct tr_namelist TR_NAMEL;

/*fp contains list of file names*/
MULT_MASKL *po_read_maskl(FILE *fp)
{	
	MULT_MASKL *mult_maskL, *tmp_mmaskL, **anchor;
	MASK_LIST *maskL;
	FILE *fpfromlist;
	char filename[MAX_LENGTH];

	anchor = &mult_maskL;
	while(fscanf(fp, "%s", filename) == 1) /*read filename*/
	{
		fpfromlist = fopen(filename, "r");
		
		if(!fpfromlist)
			prog_abort("po_read_maskl : Could not read file");
		
		maskL = po_readmask(fpfromlist);
		
		tmp_mmaskL = (MULT_MASKL *)malloc(sizeof(MULT_MASKL));
		tmp_mmaskL->masklist = maskL;
		tmp_mmaskL->next = NULL;
		*anchor = tmp_mmaskL;
		anchor = &tmp_mmaskL->next;
		fclose(fpfromlist);
	}

	return(mult_maskL);
}

void po_delete_maskl(MULT_MASKL *mult_maskL)
{
	MULT_MASKL *mmask_ptr;

   /* free mask list */
	while (mult_maskL) {
		mmask_ptr = mult_maskL->next;
		po_delete_mask(mult_maskL->masklist);
		free (mult_maskL);
		mult_maskL = mmask_ptr;
	}
	
}

/*READ CONTROLLABILITY FILES SIMILAR TO MASKED FILES*/
/*fcont contains list of uncontrollable events*/

void po_read_cont_file2(FILE *fcont, char *uncontlist[MAX_LENGTH])
{
	int i, fscanreturn, contbit;
	char tmpename[MAX_LENGTH];	
	
	i = 0;
	rewind(fcont);
	fscanreturn = fscanf(fcont, "%s%d", tmpename, &contbit);
	while(fscanreturn == 2) /*should check for max length also*/
	{
		if(!contbit){
			uncontlist[i] = (char *)calloc(sizeof(char), MAX_LENGTH);
			strcpy(uncontlist[i], tmpename);
			i++;
		}
		fscanreturn = fscanf(fcont, "%s%d", tmpename, &contbit);
	}
	uncontlist[i] = (char *)calloc(sizeof(char), MAX_LENGTH);
	*(uncontlist[i]) = '\0'; /*last value should be NULL*/
}

void po_del_uncontlist(char *uclist[MAX_LENGTH])
{
	while(*(uclist[0]) != '\0'){
		free(uclist[0]);
		uclist++;
	}
	free(uclist[0]);
}
/***********************/
/***********************/
/*Read new file format, create temporary files in old format*/

void po_extract_events(FILE *fp)
{
	FILE *mmlistfile, *mclistfile, *fpclist, *fpmlist, *fptempremove;
	int supcnt, eventcnt, numsup, numevents;
	int etype; /*etype for cont info*/
	char *maskname; /*M(event)*/
	char varfname[MAX_LENGTH], eventname[MAX_LENGTH], type_mask[MAX_LENGTH], aetype[3] = "0";

	if(GL_Read_Del!= 1)
	{
		fscanf(fp, "%d%d", &numsup, &numevents); /*read first two values of file*/

		GL_numsup = numsup; /*need to remember number of temp files created to del later*/
	
	if(numsup > 100)
	{
	puts("Something is wrong with the .data_events file? There are more than 100 supervisors");
	exit(0);
	}
	
	if(numevents > 10000)
	{
	puts("Something is wrong with the .data_events file? There are more than 10000 events");
	exit(0);
	}
		if(numsup !=0) /*more than one supervisor so create multiple files*/
		{
			mmlistfile = fopen("mmlistfiles.tmp", "w");
			mclistfile = fopen("mclistfiles.tmp", "w");
			
			for(supcnt = 0; supcnt < numsup; supcnt++)
			{
				fprintf(mmlistfile, "mlist%d.tmp\n", supcnt); /*create temp file with current # appended to name*/
				sprintf(varfname, "mlist%d.tmp", supcnt);
				fptempremove = fopen((const char*)varfname, "w+");/*to avoid problems with appending to preexisting file*/
				fclose(fptempremove);
				fprintf(mclistfile, "clist%d.tmp\n", supcnt);
				sprintf(varfname, "clist%d.tmp", supcnt);
				fptempremove = fopen((const char*)varfname, "w+");/*to avoid problems with appending to preexisting file*/
				fclose(fptempremove);
			}
			/*no masking info if numsup = 0*/
			fclose(mmlistfile);
			fclose(mclistfile);

	
			for(eventcnt = 0; eventcnt < numevents; eventcnt++)
			{
				for(supcnt = 0; supcnt < numsup; supcnt++)
				{
					sprintf(varfname, "clist%d.tmp", supcnt); /*open new temp file*/
					fpclist = fopen((const char*)varfname, "a+");
					sprintf(varfname, "mlist%d.tmp", supcnt); /*open new temp file*/
					fpmlist = fopen((const char*)varfname, "a+");
			
					if(supcnt == 0) /*first val is event name*/
						fscanf(fp, "%s", eventname);	
				
					fscanf(fp, "%s", type_mask); /* read sting ie: 1::* */
					strncpy(aetype, type_mask, 1);
					etype = atoi(aetype); /*first val is 0 or 1*/
					maskname = &type_mask[3]; /*3rd offset is start of mask name of event*/
			
					fprintf(fpclist, "%s\t%d\n", eventname, etype); /*print event name and cont/uncont val*/
					fprintf(fpmlist, "%s\t%s\n", eventname, maskname);

					fclose(fpclist);
					fclose(fpmlist);
				}
			}
		} /*only one controllability file and no mask file???*/
		else
		{
			for(eventcnt = 0; eventcnt < numevents; eventcnt++)
			{
				fpclist = fopen("clist.tmp", "a+");
				fscanf(fp, "%s%d", eventname, &etype); /*read event name and cont. bit*/
				/*added because controlcheck only has list of UNcontrol. events*/
				if(!etype)
				fprintf(fpclist, "%s\n", eventname);
				/*fprintf(fpclist, "%s\t%d\n", eventname, etype); /*print event name and cont/uncont val*/
				fclose(fpclist);
			}
		} /*end else*/
		GL_Read_Del = 1; /*have created tmp files, must delete before doing again*/
	} /*if file not read, haven't deleted previos temp files yet*/
	else
	{
		printf("%s\n", "Haven't removed tmp files created yet");
		exit(-1);
	}
}

void po_remove_event_temp_files(void)
{
	int supcnt;
	char varfname[MAX_LENGTH];

	if(GL_Read_Del == 1)
	{
		if(GL_numsup == 0) /*no supervisors/masking info, just one cont. file*/
		{
			unlink("clist.tmp");
		}
		else
		{
			unlink("mmlistfiles.tmp");
			unlink("mclistfiles.tmp");

			for(supcnt = 0; supcnt < GL_numsup; supcnt++)
				{	
				sprintf(varfname, "clist%d.tmp", supcnt); /*temp file*/
				unlink(varfname);
				sprintf(varfname, "mlist%d.tmp", supcnt); /*temp file*/
				unlink(varfname);
			}
		}
		GL_Read_Del = 0; /*have removed tmp files, must delete before doing again*/
	}
	else
	{
		printf("%s\n", "Haven't created tmp files yet");
		exit(-1);
	}
}

TR_NAMEL *po_read_tr_nameL(char *input)
{
	TR_NAMEL *tr_namelist, *tmp_namelist, **anchor;
	size_t length1, length2;
	char *commaptr, trname[MAX_LENGTH], tmpinput[MAX_LENGTH];
	
	anchor = &tr_namelist;
	strcpy(tmpinput, input);

	do{
		commaptr = strchr(tmpinput, (int)',');
		tmp_namelist = (TR_NAMEL *)malloc(sizeof(TR_NAMEL));
		memset(tmp_namelist->name, (int)'\0', sizeof(char)*MAX_LENGTH);

		if(commaptr != NULL)
			{
				length1 = strlen(tmpinput);
				length2 = strlen(commaptr);
			
				strncpy(tmp_namelist->name, tmpinput, length1-length2);
				strcpy(tmpinput, (commaptr+1));
		}
		else
			strcpy(tmp_namelist->name, tmpinput); /*last event*/
			
		tmp_namelist->next = NULL;
		*anchor = tmp_namelist;
		anchor = &tmp_namelist->next;
	
	}while(commaptr != NULL);

	return(tr_namelist);
}

void po_delete_tr_nameL(TR_NAMEL *trnameL)
{
	TR_NAMEL *trnameLptr;

   /* free the list of transition names */
	while (trnameL) {
		trnameLptr = trnameL->next;
		free (trnameL);
		trnameL = trnameLptr;
	}
}

void po_push(STACKSTPTR **topPtr, ST_LIST *newstptr)
{
	STACKSTPTR *newPtr;

	newPtr = (STACKSTPTR *)malloc(sizeof(STACKSTPTR));
	newPtr ->st_ptr = newstptr;	/*new state pointer is newstptr*/
	newPtr ->next = *topPtr; /*new next stack pointer is current stack pointer*/
	*topPtr = newPtr;			/*topPtr is at top*/
}

ST_LIST *po_pop(STACKSTPTR **topPtr)
{
	STACKSTPTR *tempPtr;
	ST_LIST *popValue;
	tempPtr = *topPtr;
	popValue = (*topPtr)->st_ptr;
	*topPtr = (*topPtr)->next; /*top pointer now points to next stack*/
	free(tempPtr);				/*free previous top pointer*/
	return(popValue);
}


void po_diag_remove_deadlock(fsmInOut)
FSM *fsmInOut;
{
	int num_states1, num_states2;
	ST_LIST *currentst;
	
	currentst = fsmInOut->states;
	if(currentst != NULL) /*could have no states*/
	{
		do{
			num_states1 = get_NStates(fsmInOut); /* Get number of states initially in fsm */
			while(currentst)
			{	
				if(currentst->trans == NULL) /*no transitions from current state so remove*/
					delete_state(fsmInOut, currentst);
				
				currentst = currentst ->next;
			}
			num_states2 = get_NStates(fsmInOut); /* After removing bad states find how many are left in FSM */
		}while((num_states1-num_states2)!= 0); /* Keep going until no states removed */
	}
}

/*only care about cycles of (.,dump,-dump) for diagnosability*/
void po_diag_create_pertinent_fsm(fsmIn, fsmOut)
FSM *fsmIn, *fsmOut;
{
	char *stateptr, *commaptr;
	ST_LIST *currentst;

	fsm_copy(fsmIn, fsmOut);
	
	currentst = fsmOut->states;
	while(currentst)
	{
		/*if state not (.,dump, notdump) delete*/
		commaptr = strchr(currentst->name,(int)','); /*second state after comma*/
		stateptr = strstr(currentst->name, "dump"); 
		if(stateptr != NULL)
		{
			if((commaptr+1) == stateptr) /*second state is dump*/
				{
					if(strstr((stateptr + 5), "dump") != NULL) /*don't want any other states to be dump*/
						delete_state(fsmOut, currentst); /*other states dump, so remove*/
				}
		}
		else /*none of the states are dump, so delete*/
			delete_state(fsmOut, currentst);
		
		currentst = currentst->next;
	}
}

/*put $ in front of state everywhere in fsm*/
void po_mark_state(FSM *fsm_mark, ST_LIST *curr_state)
{
	ST_LIST *temp_pr;
	TR_LIST *temp_trans;
	char state_name[MAX_LENGTH], newstate_name[MAX_LENGTH];

	if(!fsm_mark)
		prog_abort("po_mark_state: Null pointer passed as arg for FSM*");
	if(!curr_state)
		prog_abort("po_mark_state: Invalid ST_LIST* ");

	strcpy(state_name, curr_state->name); /*save state name for later*/
	/* Mark the state if not already*/
	if(*(curr_state->name) != '$')
	{
		strcpy(newstate_name, "$");
		strcat(newstate_name, curr_state->name);
		strcpy(curr_state->name, newstate_name);
	}

	/* Now locate the above state at all the places in the next_state
	column so that these can be marked.*/

	temp_pr = fsm_mark->states;
	temp_trans = temp_pr->trans;
	while(temp_pr) {
	  while(temp_trans) {
		if(strcmp(state_name, temp_trans->next_state->name)==0) {
			strcpy(temp_trans->next_state->name, newstate_name);
		} /* if ends */
		temp_trans=temp_trans->next;
	  } /* while temp_trans ends */
	  temp_pr = temp_pr->next;
	} /* while temp_pr ends */
}

int po_diagnosability(fsmIn) /*note, altering fsmIn*/
FSM *fsmIn;
{
	ST_LIST *currentst;
	TR_LIST *currenttr, *currenttrcheck;
	STACKSTPTR *stackPtrSearch = NULL, *stackPtrCheck = NULL, 
		*begin_stack_ptr = NULL, *end_stack_ptr = NULL, *current_stack_ptr = NULL, 
		*next_stack_ptr = NULL;
	int diag = 1;
	char tr1name[MAX_LENGTH], tr2name[MAX_LENGTH], *commaptr;
	size_t length1, length2;

	char trname[MAX_LENGTH];

	currentst = fsmIn->states;
	if(currentst != NULL) /*could have no states*/
	{
	while(diag) /*do dfs until all states marked or not diagnosable*/
	{
		while(*(currentst->name) == '$') /*find non marked state*/
		{	
			currentst = currentst->next;
			if(currentst == NULL)      /*all states exhausted*/
				break;
		}
		if(currentst == NULL)
		{
			while(stackPtrSearch != NULL) /*no more states to search so free stack*/
				po_pop(&stackPtrSearch);
			break;						/*exit loop*/
		}
		else /*non marked state found, mark and push on stack*/
		{
			/*need to mark the state, and the state in transition list*/
			po_mark_state(fsmIn, currentst);
			po_push(&stackPtrSearch, currentst);
		}
		
		currenttr = currentst->trans;
		
		/*stack must have a state ptr, continue if haven't found to be not diagnosable*/
		while(stackPtrSearch != NULL && diag && currenttr != NULL) /*state could have no transitions*/
		{
			
			if(*(currenttr->input) != '$') /*current transition not marked*/ 
			{
				/*mark transition (put $ at beginning of transition)*/
				strcpy(trname, "$");
				strcat(trname, currenttr->input);
				strcpy(currenttr->input, trname);

				if(*(currenttr->next_state->name) == '$') /*transition leads to marked state, therefore is a loop*/
				{
					po_push(&stackPtrSearch, currenttr->next_state);/*push next state on stack for search*/

					/*put state ptr list into reverse order for check*/
					while(stackPtrSearch != NULL)
						po_push(&stackPtrCheck, po_pop(&stackPtrSearch));
					
					/*do forward search to find the loop*/
					begin_stack_ptr = stackPtrCheck;
					end_stack_ptr = stackPtrCheck->next;
					while(begin_stack_ptr->st_ptr != end_stack_ptr->st_ptr)
					{
						while(begin_stack_ptr->st_ptr != end_stack_ptr->st_ptr)
							{			
								end_stack_ptr = end_stack_ptr->next;
								if(end_stack_ptr == NULL)
									break;		/*can't check end_stack_ptr->st_ptr if end_stack_ptr is NULL*/
						}

							/*if states didn't match, advance*/
							if(end_stack_ptr == NULL)
							{	
								begin_stack_ptr = begin_stack_ptr->next;
								end_stack_ptr = begin_stack_ptr->next;
							}
							if(end_stack_ptr == NULL)
								break;
					}

					/* if no states matched, only checking part of a cycle because other
					   part of cycle has already been checked (so check the whole stack)*/
					if(end_stack_ptr == NULL)
						begin_stack_ptr = stackPtrCheck;
			
					current_stack_ptr = begin_stack_ptr;				/*going from this state*/
					currenttrcheck = current_stack_ptr->st_ptr->trans;	/*using a transition*/
					next_stack_ptr = begin_stack_ptr->next;				/*to this next state*/
					
					while(next_stack_ptr != NULL && diag) /*will always go to the end, unless found !diag*/
					{
						/*if statement to handle parallel transitions*/
						if(current_stack_ptr->st_ptr == currentst)
							currenttrcheck = currenttr;
						else{
							/*find transition that leads to correct state*/
							/*transition must be marked. */
							while(strcmp(currenttrcheck->next_state->name, next_stack_ptr->st_ptr->name)!=0) 
							{
								currenttrcheck = currenttrcheck->next;
								if(*(currenttrcheck->input) != '$')
								{
									while(*(currenttrcheck->input) != '$')
										currenttrcheck = currenttrcheck->next;
								}
							}
						}

						/*found the transition, now see if OK, note skip looking at mark $*/
						commaptr = strchr((currenttrcheck->input +1),(int)',');
						length1 = strlen(currenttrcheck->input);
						length2 = strlen(commaptr);
						strncpy(tr1name, (currenttrcheck->input+1), length1-length2-1); /*first transition after $, before comma*/
						strcpy(tr2name, (commaptr + 1)); /*second transition after comma*/
						/*don't really need to look at second transition*/

						if(*tr1name != '*') /*if first transition is != *, not diagnosable*/
						 diag = 0;

						current_stack_ptr = next_stack_ptr; /*start from next state*/
						currenttrcheck = current_stack_ptr->st_ptr->trans; /*using a transition*/
						next_stack_ptr = current_stack_ptr->next; /*to the next next state*/
					}/*end while*/

					/*put state ptr list back into correct order for search*/
					while(stackPtrCheck != NULL)
						po_push(&stackPtrSearch, po_pop(&stackPtrCheck));

					po_pop(&stackPtrSearch); /*don't want to look at state reached in loop*/
					/*point everything back to state before end of loop*/
					currentst = stackPtrSearch->st_ptr; 
					currenttr = currentst->trans;					

				}/*end find loop if next state marked*/
				else{ 
					/*transition leads to a non marked state*/
					/*mark the state and push unto stack*/
					po_mark_state(fsmIn, currenttr->next_state);
					po_push(&stackPtrSearch, currenttr->next_state);
					currentst = stackPtrSearch->st_ptr;
					currenttr = currentst->trans;
				}

			} /*end current transition not marked if() */
			else{ /*if transition is marked, skip*/
					currenttr = currenttr->next;
			}
			if(currenttr == NULL) /* all transitions exhausted (all are marked)*/
			{
				po_pop(&stackPtrSearch);
			    if(stackPtrSearch != NULL)
				{
					/*point everything to back step state*/
					currentst = stackPtrSearch->st_ptr; 
					currenttr = currentst->trans;
				}
				else
				{
					currentst = NULL; 
					currenttr = NULL;
				}
			}
		}/*end while*/
		if(stackPtrSearch == NULL) /*could still have disjoint states to check*/
			currentst = fsmIn->states;
	} /*end while, do dfs for non marked states*/

	while(stackPtrSearch != NULL && !diag) /*if found to be not diagnosable, could still need to free stack*/
		po_pop(&stackPtrSearch);
	}/*end if currenst!=NULL*/
	return(diag);

} /*end po_diag*/	


/*FUNCTION TEST*/
void TEST(FSM *fsmIn)
{
	
	FSM fsmOut;
	FILE *fptest = fopen("testout","w+");

	po_diag_create_pertinent_fsm(fsmIn, &fsmOut);
	po_diag_remove_deadlock(&fsmOut);
	
	
	if(po_diagnosability(&fsmOut))
		puts("Diagnosable");
	else
		puts("Not Diagnosable");
	fsm_print(fptest, &fsmOut);
	fclose(fptest);
}

void TEST2(FILE *fp)
{
	MULT_MASKL *mmaskL;
	TR_NAMEL *trnameL;
	mmaskL = po_read_maskl(fp);
	po_delete_maskl(mmaskL);

	trnameL = po_read_tr_nameL("a,b,c,d");
	po_delete_tr_nameL(trnameL);
}

/***************************************************************/
MASK_LIST *po_readmask(fp)
FILE *fp;
{
	MASK_LIST *masklist;
	MASK_LIST *tmp2, **anchor, *mask_ptr;
	char st12[MAX_LENGTH], st22[MAX_LENGTH];
   /* Read in the masking information from the input file into masklist. */
   anchor = &masklist;

   /* read in information corresponding to pair of "original"
      and "masked" names from the input file */
   while(fscanf(fp, "%s %s", st12, st22) == 2) {

	  /* allocate space for a new element of mask list */
      tmp2 = (MASK_LIST *) malloc(sizeof(MASK_LIST));

	   
      /* copy information corresponding to the original and 
         masked names of the current event */
      strcpy(tmp2->original, st12);
      strcpy(tmp2->masked, st22);

      /* insert the new entry in the list */
      tmp2->next = NULL;
	  *anchor = tmp2;
      anchor = &tmp2->next;
   }
	return(masklist);
}
/*******************************************************************/
/* **************************************************************
/*free mask storage, taken from fsm_mask*/
void po_delete_mask(MASK_LIST *mlist)
{
	MASK_LIST *mask_ptr;

   /* free the storage used for storing the masking information */
	while (mlist) {
		mask_ptr = mlist->next;
		free (mlist);
		mlist = mask_ptr;
	}
}

/*return mask value of transition*/
char *M(char *trans, MASK_LIST *mask_list)
{
	MASK_LIST *mlistptr = mask_list;

	while(mlistptr){
		if(strcmp(trans, mlistptr->original)==0)
			return(mlistptr->masked); /*found masked value now return*/
		mlistptr = mlistptr->next;
	}
	return(trans); /*if didn't find masked value return original value*/
}


/* **************************************************************
   Function : masked_sync_comp

   This function constructs a state machine which is the 
   synchronous composition of two given state machines.
   The resultant state machine accepts the language which is
   the intersection of the languages accepted by the two input  
   state machines.

   Arguments : fsm1_ptr - pointer to the first state machine
               fsm2_ptr - pointer to the second state machine
               fsm3_ptr - pointer to the resultant state machine

   Return Type : void

   ************************************************************** */

void po_masked_sync_comp(fsm1_ptr, fsm2_ptr, fsm3_ptr, masklist)
FSM *fsm1_ptr, *fsm2_ptr, *fsm3_ptr;
MASK_LIST *masklist;
{
   char name[MAX_LENGTH];
   ST_LIST *st1, *st2, *st3, *tmp;
   TR_LIST *tr1, *tr2, *tmptr1,*tmptr2;
   EQUIV_LIST *list = NULL, *current_pair;
   int epstran1 = 0, epstran2 = 0; /*keep track of epsilon transitions*/	
   char trname[MAX_LENGTH];

   if (!fsm1_ptr || !fsm2_ptr || !fsm3_ptr)
	prog_abort("fsm_sync_comp : NULL pointer passed as argument for (FSM *)");

   /* initialize pointers to point to the first state of each
      of the two input state machines */
   st1 = fsm1_ptr->states;  st2 = fsm2_ptr->states;

   /* insert the initial state of the resultant state machine
      which is a concatenation of the initial states of the
      two input state machines */
   strcpy(name, st1->name);
   strcat(name, ",");
   /* check if the concatenation will result in a string which is
      of length greater than the maximum allowed */
   if (strlen(name) + strlen(st2->name) >= MAX_LENGTH)
      prog_abort("fsm_sync_comp : length of string exceeds MAX_LENGTH");

   strcat(name, st2->name);
   fsm3_ptr->states = alloc_state;
   /*fsm3_ptr->states->name = (char *) malloc(strlen(name) + 1);/*static now*/
   strcpy(fsm3_ptr->states->name, name);
   fsm3_ptr->states->marked = st1->marked && st2->marked;
   
   /* no other states in this machine as yet */
   fsm3_ptr->states->next = NULL;
 
   /* no transitions in this state as yet */
   fsm3_ptr->states->trans = NULL;

   /* keep a list of the states inserted in the resultant
      state machine */
   insert_pair(&list, st1, st2);

   /* Start from this initial state of the resultant state 
      machine and see if any other states need to be inserted
      in the synchronous composition state machine.  If such states 
      are found, they are also inserted in the resultant state 
      machine and then checked to see if they lead to other states 
      which need to be included.  The routine ends when all the 
      candidate states have been processed and at that time, the 
      machine fsm3 contains the synchronous composition of fsm1 
      and fsm2 */

   current_pair = list;
   while (current_pair) {
      st1 = current_pair->first;   
      st2 = current_pair->second;  /* the two states of the pair */
      tr1 = st1->trans;
      tr2 = st2->trans;    /* transitions allowed from these states */
      st3 = NULL;

      while (tr1) {
         while (tr2) {


            /* Handle epsilon transitions in the first state machine*/
	    
			 if (*M(tr1->input,masklist) == '*')
			 {
				
				 /* first get a pointer to the current state in fsm3 */
	       
				if (!st3) 
				{
					strcpy(name, st1->name);
					strcat(name, ",");
					/* first check if the length of the string exceeds the
						maximum allowed */
					if (strlen(name) + strlen(st2->name) >= MAX_LENGTH)
						prog_abort("fsm_sync_comp : length of string exceeds MAX_LENGTH");

					strcat(name, st2->name);
	 				st3 = find_state(fsm3_ptr, name);
				}

					/* Determine the name of the state which is the 
						resultant state for this transition in fsm3. 
						It is the concatenation of the names of the 
						resultant states in fsm1 and fsm2 */
				strcpy(name, tr1->next_state->name);
				strcat(name, ",");

				/* check length of string */
				if (strlen(name) + strlen(st2->name) >= MAX_LENGTH)
					prog_abort("fsm_sync_comp : length of string exceeds MAX_LENGTH");

				strcat(name, st2->name);

				/* insert this state in fsm3 */
				tmp = insert_state(fsm3_ptr, name);
				tmp->marked = tr1->next_state->marked && st2->marked;

				strcpy(trname, tr1->input);
				strcat(trname,",*"); /*insert a transition pair, no trans in 2nd machine*/

				/* insert the transition from the current state to the new state */
				insert_trans(fsm3_ptr, st3, trname, name);

				/* since a new state has been inserted in the resultant
					state machine, insert the corresponding pair in the
					linked list used to keep track of the various states
					of the resultant state machine */
				insert_pair(&list, tr1->next_state, st2);
				 
	       /*break;*/
	    }


   
   
   /* Handle epsilon transitions in the second state machine*/
	    
			 if (*M(tr2->input,masklist) == '*')
			 {
				 
				 /* first get a pointer to the current state in fsm3 */
	       
				if (!st3) 
				{
					strcpy(name, st1->name);
					strcat(name, ",");
					/* first check if the length of the string exceeds the
						maximum allowed */
					if (strlen(name) + strlen(st2->name) >= MAX_LENGTH)
						prog_abort("fsm_sync_comp : length of string exceeds MAX_LENGTH");

					strcat(name, st2->name);
	 				st3 = find_state(fsm3_ptr, name);
				}

					/* Determine the name of the state which is the 
						resultant state for this transition in fsm3. 
						It is the concatenation of the names of the 
						resultant states in fsm1 and fsm2 */
				strcpy(name, st1->name);
				strcat(name, ",");

				/* check length of string */
				if (strlen(name) + strlen(tr2->next_state->name) >= MAX_LENGTH)
					prog_abort("fsm_sync_comp : length of string exceeds MAX_LENGTH");

				strcat(name, tr2->next_state->name);

				/* insert this state in fsm3 */
				tmp = insert_state(fsm3_ptr, name);
				tmp->marked = st1->marked && tr2->next_state->marked;

				strcpy(trname, "*,");
				strcat(trname, tr2->input); /*insert a transition pair, no trans in 1st machine*/

				/* insert the transition from the current state to the new state */
				insert_trans(fsm3_ptr, st3, trname, name);

				/* since a new state has been inserted in the resultant
					state machine, insert the corresponding pair in the
					linked list used to keep track of the various states
					of the resultant state machine */
				insert_pair(&list, st1, tr2->next_state);

				

	       /*break;*/
	    }

		/*add transition when both states have the same transition*/

	    if ((strcmp(M(tr1->input,masklist), M(tr2->input,masklist)) == 0) && *M(tr1->input,masklist) !='*' && *M(tr2->input,masklist) !='*') {
		epstran1 = epstran2 = 0;
               /* first get a pointer to the current state in fsm3 */
	       if (!st3) {
		 strcpy(name, st1->name);
		 strcat(name, ",");
		 /* first check if the length of the string exceeds the
		    maximum allowed */
		 if (strlen(name) + strlen(st2->name) >= MAX_LENGTH)
		    prog_abort("fsm_sync_comp : length of string exceeds MAX_LENGTH");

		 strcat(name, st2->name);
	 	 st3 = find_state(fsm3_ptr, name);
	       }

               /* Determine the name of the state which is the 
                  resultant state for this transition in fsm3. 
                  It is the concatenation of the names of the 
		  resultant states in fsm1 and fsm2 */
	       strcpy(name, tr1->next_state->name);
		   strcat(name, ",");

	       /* check length of string */
	       if (strlen(name) + strlen(tr2->next_state->name) 
							>= MAX_LENGTH)
		  prog_abort("fsm_sync_comp : length of string exceeds MAX_LENGTH");

	       strcat(name, tr2->next_state->name);

               /* insert this state in fsm3 */
	       tmp = insert_state(fsm3_ptr, name);
	       tmp->marked = tr1->next_state->marked &&
					tr2->next_state->marked;
			
		   strcpy(trname, tr1->input);
		   strcat(trname,","); /*insert a transition pair*/
		   strcat(trname, tr2->input);


               /* insert the transition from the current state to
                  the new state */
	       insert_trans(fsm3_ptr, st3, trname, name);

               /* since a new state has been inserted in the resultant
                  state machine, insert the corresponding pair in the
                  linked list used to keep track of the various states
                  of the resultant state machine */
	       insert_pair(&list, tr1->next_state, tr2->next_state);

	       /*break;*/
	    }

            /* compare current transition of st1 with all 
               transitions of st2*/ 
			tr2 = tr2->next;
		}           	
         /* check all transitions of the current pair of states  */

		tr1 = tr1->next;
		tr2 = st2->trans;
      }

      /* check all the pairs of states */ 
      current_pair = current_pair->next;
   }
    	


/*repeat1*/
current_pair = list;
   while (current_pair) {
      st1 = current_pair->first;   
      st2 = current_pair->second;  /* the two states of the pair */
      tr1 = st1->trans;
      tr2 = st2->trans;    /* transitions allowed from these states */
      st3 = NULL;


	  while(tr1){

            /* Handle epsilon transitions in the first state machine*/
	    
			 if (*M(tr1->input,masklist) == '*')
			 {
				
				 /* first get a pointer to the current state in fsm3 */
	       
				if (!st3) 
				{
					strcpy(name, st1->name);
					strcat(name, ",");
					/* first check if the length of the string exceeds the
						maximum allowed */
					if (strlen(name) + strlen(st2->name) >= MAX_LENGTH)
						prog_abort("fsm_sync_comp : length of string exceeds MAX_LENGTH");

					strcat(name, st2->name);
	 				st3 = find_state(fsm3_ptr, name);
				}

					/* Determine the name of the state which is the 
						resultant state for this transition in fsm3. 
						It is the concatenation of the names of the 
						resultant states in fsm1 and fsm2 */
				strcpy(name, tr1->next_state->name);
				strcat(name, ",");

				/* check length of string */
				if (strlen(name) + strlen(st2->name) >= MAX_LENGTH)
					prog_abort("fsm_sync_comp : length of string exceeds MAX_LENGTH");

				strcat(name, st2->name);

				/* insert this state in fsm3 */
				tmp = insert_state(fsm3_ptr, name);
				tmp->marked = tr1->next_state->marked && st2->marked;

				strcpy(trname, tr1->input);
				strcat(trname,",*"); /*insert a transition pair, no trans in 2nd machine*/

				/* insert the transition from the current state to the new state */
				insert_trans(fsm3_ptr, st3, trname, name);

				/* since a new state has been inserted in the resultant
					state machine, insert the corresponding pair in the
					linked list used to keep track of the various states
					of the resultant state machine */
				insert_pair(&list, tr1->next_state, st2);
				 
	       /*break;*/
	    }

			tr1 = tr1->next;

}

current_pair = current_pair->next;
}


/*repeat2*/
current_pair = list;
   while (current_pair) {
      st1 = current_pair->first;   
      st2 = current_pair->second;  /* the two states of the pair */
      tr1 = st1->trans;
      tr2 = st2->trans;    /* transitions allowed from these states */
      st3 = NULL;


	  while(tr2){

   /* Handle epsilon transitions in the second state machine*/
	    
			 if (*M(tr2->input,masklist) == '*')
			 {
				 
				 /* first get a pointer to the current state in fsm3 */
	       
				if (!st3) 
				{
					strcpy(name, st1->name);
					strcat(name, ",");
					/* first check if the length of the string exceeds the
						maximum allowed */
					if (strlen(name) + strlen(st2->name) >= MAX_LENGTH)
						prog_abort("fsm_sync_comp : length of string exceeds MAX_LENGTH");

					strcat(name, st2->name);
	 				st3 = find_state(fsm3_ptr, name);
				}

					/* Determine the name of the state which is the 
						resultant state for this transition in fsm3. 
						It is the concatenation of the names of the 
						resultant states in fsm1 and fsm2 */
				strcpy(name, st1->name);
				strcat(name, ",");

				/* check length of string */
				if (strlen(name) + strlen(tr2->next_state->name) >= MAX_LENGTH)
					prog_abort("fsm_sync_comp : length of string exceeds MAX_LENGTH");

				strcat(name, tr2->next_state->name);

				/* insert this state in fsm3 */
				tmp = insert_state(fsm3_ptr, name);
				tmp->marked = st1->marked && tr2->next_state->marked;

				strcpy(trname, "*,");
				strcat(trname, tr2->input); /*insert a transition pair, no trans in 1st machine*/

				/* insert the transition from the current state to the new state */
				insert_trans(fsm3_ptr, st3, trname, name);

				/* since a new state has been inserted in the resultant
					state machine, insert the corresponding pair in the
					linked list used to keep track of the various states
					of the resultant state machine */
				insert_pair(&list, st1, tr2->next_state);

				

	       /*break;*/
	    }

			tr2 = tr2->next;

}

current_pair = current_pair->next;
}


   /* free the storage used to store the linked list of pairs 
      of states */
   while (list) {
      current_pair = list->next;
      free (list);
      list = current_pair;
   }

}




/********************************************************************/



void po_graph(fsmG, fsmS, fsmGSbar, mmaskL)
FSM *fsmG, *fsmS, *fsmGSbar;
MULT_MASKL *mmaskL;
{
	MULT_MASKL *mmaskLptr;
	FSM fsmSbar;/* *fsmGSbar;*/
	TRANS_LIST *tr_ptr = NULL;
	FILE *fptmp;

	fptmp = fopen("trlist","w+");

	fsm_find_sigma(fsmG, &tr_ptr); /*get list of events in plant should tr_ptr not be pointer?*/

	while(tr_ptr)
	{	/*TAG*/
		fprintf(fptmp, "%s\n", tr_ptr->input); /* write events ONLY *TAG*..and controllable information */
		tr_ptr = tr_ptr->next;
	}
	fclose(fptmp);
	fptmp = fopen("trlist","r");

	CompleteGraph(fptmp, fsmS, &fsmSbar);
	fsm_sync_comp(fsmG, &fsmSbar, fsmGSbar); /*look at what passing etc. fsmR should be result*/ 
	
	mmaskLptr = mmaskL;
	do{		/*was doing &fsmSbar, but want G||Sbar || S || S ...*/
		po_masked_sync_comp(fsmGSbar, fsmS, fsmGSbar, mmaskLptr->masklist);
		mmaskLptr = mmaskLptr->next;
	}while(mmaskLptr != NULL);

	fsm_delete(&fsmSbar);

	fclose(fptmp);
	unlink("trlist"); /*remove tmp file*/

}

/*observability test*/
int po_observability(fsmR, mmaskL)
FSM *fsmR;
MULT_MASKL *mmaskL;
{
	ST_LIST *currentst;    
	TR_LIST *currenttr;
	MULT_MASKL *mmaskLptr;
	TR_NAMEL *trnameL, *trnameLptr;
	char *commaptr, *stateptr;
	int obs = 1, same;

	/*now doing observability test*/
	/*notice first state will never be dump*/
	currentst = fsmR->states;
	while(currentst && obs)
	{
		if(strstr(currentst->name, "dump") == NULL) /*no states are dump*/
		{
			currenttr = currentst->trans;
			while(currenttr && obs)
			{
				trnameL = po_read_tr_nameL(currenttr->input); /*get all transitions*/
				trnameLptr = trnameL->next;
				mmaskLptr = mmaskL;
				same = 1;
				while(trnameLptr && same) /*note, should be same amount of masks as transitions*/
				{
				
					if(strcmp(M(trnameL->name, mmaskL->masklist), M(trnameLptr->name, mmaskLptr->masklist)) != 0)/*does M(first trans) = M(next trans)*/
						same = 0;

					mmaskLptr = mmaskLptr->next; /*use first mask for both first*/
					trnameLptr = trnameLptr->next;
				}
				
					if(same) /*are masked transitions equal?*/
					{
						commaptr = strchr(currenttr->next_state->name,(int)','); /*second state after comma*/
						stateptr = strstr(currenttr->next_state->name, "dump"); 
						if(stateptr != NULL)
						{	
							if((commaptr+1) == stateptr) /*second state is dump*/
								{ /*add check here if any supervisor has control over trans.?*/
								if(strstr((stateptr + 5), "dump") == NULL) /*don't want any other states to be dump*/
									obs = 0; /*not observable*/
								}
						}
					}
				currenttr = currenttr->next;
			}
		}
		currentst = currentst->next;
	}

	return(obs);
}


int po_normality(fsmR, mmaskL)
FSM *fsmR;
MULT_MASKL *mmaskL;
{
	ST_LIST *currentst;    
	TR_LIST *currenttr;
	MULT_MASKL *mmaskLptr;
	TR_NAMEL *trnameL, *trnameLptr;
	char *commaptr, *stateptr;
	int norm = 1, same;

	/*now doing normality test*/
	/*notice first state will never be dump*/
	currentst = fsmR->states;
	while(currentst && norm)
	{
		if(strstr(currentst->name, "dump") == NULL) /*no states are dump*/
		{
			currenttr = currentst->trans;
			while(currenttr && norm)
			{
				trnameL = po_read_tr_nameL(currenttr->input); /*get all transitions*/
				trnameLptr = trnameL->next;
				mmaskLptr = mmaskL;
				same = 1;
				while(trnameLptr && same) /*note, should be same amount of masks as transitions*/
				{
				
					if(strcmp(M(trnameL->name, mmaskL->masklist), M(trnameLptr->name, mmaskLptr->masklist)) != 0)/*does M(first trans) = M(next trans)*/
						same = 0;

					mmaskLptr = mmaskLptr->next; /*use first mask for both first*/
					trnameLptr = trnameLptr->next;
				}
				
					if(same) /*are masked transitions equal?*/
					{
						commaptr = strchr(currenttr->next_state->name,(int)','); /*second state after comma*/
						stateptr = strstr(currenttr->next_state->name, "dump"); 
						if(stateptr != NULL)
						{	
							if((commaptr+1) == stateptr) /*second state is dump*/
								{
								if(strstr((stateptr + 5), "dump") == NULL) /*don't want any other states to be dump*/
									norm = 0; /*not normal*/
								}
						}
					}
				currenttr = currenttr->next;
			}
		}
		currentst = currentst->next;
	}

	return(norm);
}
