#include "fsm.h"
#include "converter.h"
void AddSelfLoops();

/*=============================================================================
Function:	NormalityCheck()
Comments:	This function does a normality check on a system with respect
		to another system.  Typically the desired behavior S and 
		plant G.
		Algorithm is to compose G, S1 and S2, where G is the plant,
		S1 is the completed graph of S and S2 is the state machine
		with the following transitions added to it:
		1. Self loop on every unobservable event at every state.
		2. An epsilon transition for each unobservable transition in
		   S, apart from its original unobservable transition.
		Note that: all the states in G and S only are marked.
		Now see if any of the reachable states in the resultant 
		machine is marked or not.  If it is MARKED, then it is
		NOT NORMAL, else it is NORMAL.

Inputs:		fp - pointer to file containing set of unobservable events.
		fpr -pointer to file containing event set of S.
		fsmP-fsm of the plant.(protocol)
		fsmS-fsm of the supervisor.(converter)

Output:		This function returns a TRUE if machine is normal else
		returns a FALSE

Note:		This will work as long as you don't have to augment state 
		machines, before composition, as there is no provision to
		input the augmentation event set for the state machines.
=============================================================================*/
int NormalityCheck(FILE *fp, FILE *fpr, FSM *fsmP, FSM *fsmS)
{
	int no_states, flag = MAX_LENGTH;
	FILE  *fp_out;
#ifdef X
FILE *fp_aug;
#endif
	FSM fsmS1, fsmS2, fsm_out, fsm_tmp;
	ST_LIST *curr_state;
	TR_LIST *curr_trans;
	NAME_LIST *name_list=NULL, *name_ptr;
	int num_trans, i=0, j, new_num_trans, num_states, count=0;
	int UNOBSERVABLE;
	char *buffer[MAX_LENGTH], new_buffer[LENGTH];
	char *unobslist[MAX_LENGTH], *temp[MAX_LENGTH];

	if(!fp)
		prog_abort("NormalityCheck: Invalid file pointer");
	if(!fpr)
		prog_abort("NormalityCheck: Invalid file pointer");
	if(!fsmP)
		prog_abort("NormalityCheck: Null pointer arg for FSM* ");
	if(!fsmS)
		prog_abort("NormalityCheck: Null pointer arg for FSM* ");

	for(i=0;i<MAX_LENGTH;i++) {
                buffer[i] = (char *)calloc(sizeof(char), LENGTH);
                temp[i] = (char *)calloc(sizeof(char), LENGTH);
                unobslist[i] = (char *)calloc(sizeof(char), LENGTH);
        }
        i=0;

	fp_out = fopen("S2.data", "w+");	
#ifdef X
fp_aug = fopen("aug_S1.data", "r");
#endif

	/* scan in the list of unobservable events into a buffer Greg Changed*/
	while(fscanf(fp, "%s", temp[i])==1) {
                strcpy(unobslist[i],temp[i]);
                i++;
        }
	rewind(fp);

	/* Complete the graph of S to obtain S1 */
	CompleteGraph(fpr, fsmS, &fsmS1);

	/* Add the following transitions in S to obtain S2.
        (i)  Self loop on all unobservable events at every state.
        (ii) An epsilon transition for each unobservable transition
             from any state. */

	/* Add Self Loops on all unobservable events at every state */
	AddSelfLoops(fp, fsmS); 
	rewind(fp); /* rewind fp to BOF */

	/* Add an Epsilon transition for all unobs transition from any state*/

	curr_state = fsmS->states;
        curr_trans = fsmS->states->trans;
        i=0;
        while(curr_state) {
          curr_trans = curr_state->trans;
          num_trans = get_NTrans(curr_state);
          sprintf(buffer[i], "\n%s\t%d\t", curr_state->name,curr_state->marked);
          /* Find out if the transition label is an unobservable event */
          while(curr_trans) {
             UNOBSERVABLE = FindLabel(unobslist, curr_trans->input);
             if(UNOBSERVABLE) {
                count++;
                /* retain the original transitions as it is */
                sprintf(buffer[++i], "%s\t%d\t%s\n", curr_trans->input,
                curr_trans->type, curr_trans->next_state->name);
 
                /* add an epsilon transition now */
                sprintf(buffer[++i], "%s\t%d\t%s\n", "*", curr_trans->type,
		   	curr_trans->next_state->name);
		insert_trans(fsmS, curr_state, "*", curr_trans->type,
				curr_trans->next_state->name);
             }
             else {
                /* retain the original transitions as it is */
                sprintf(buffer[++i], "%s\t%d\t%s\n", curr_trans->input,
                curr_trans->type, curr_trans->next_state->name);
             }
             curr_trans = curr_trans->next;
          }
          new_num_trans = num_trans+count;
          sprintf(new_buffer, "%d\n", new_num_trans);
          new_buffer[strlen(new_buffer)-1] = '\0'; /*Greg Changed*/
          fprintf(fp_out, "%s%s", buffer[0], new_buffer);
          fflush(fp_out);
          for(j=1;j<=new_num_trans;j++) {
                fprintf(fp_out, "%s", buffer[j]);
                fflush(fp_out);
          }
          for(i=0;i<MAX_LENGTH;i++) {
                *buffer[i]='\0';
          }
	  i=0;
          curr_state = curr_state->next;
          count=0;
        }
	fflush(fp_out);	
	fclose(fp_out);

	fsm_remove_epsilon(fsmS, &fsmS2); /* remove "*" transitions */
	fsm_sync_comp(fsmP, &fsmS1, &fsm_tmp);
	fsm_rename(&fsm_tmp);
#ifdef X
	AugmentFsm(fp_aug, &fsm_tmp);
#endif
	fsm_sync_comp(&fsm_tmp, &fsmS2, &fsm_out);
	fsm_rename(&fsm_out);	
	
	fp_out = fopen("tmp", "w");
	fsm_print(fp_out, &fsm_out);
	fflush(fp_out);

	curr_state = fsm_out.states;
	curr_trans = fsm_out.states->trans;

	no_states=fsm_reachability(&fsm_out,curr_state->name,"ALL",&name_list);
	name_ptr = name_list;
	while(name_ptr) {
		while(curr_state) {
		   if(strcmp(name_ptr->name, curr_state->name)==0) {
		      if(curr_state->marked == MKD) {
			flag = FALSE;
	              }
		   } 
		   curr_state = curr_state->next;
		}
		name_ptr = name_ptr -> next;
	}

	rewind(fp);
	rewind(fpr);		
	fclose(fp_out);
	fsm_delete(&fsmS1);
	fsm_delete(&fsmS2);
	fsm_delete(&fsm_tmp);
	fsm_delete(&fsm_out);
/**/
	for(i=0; i< MAX_LENGTH; i++) {
		free(buffer[i]);
		free(temp[i]);
		free(unobslist[i]);
	}
/*Just isn't working..should*/
	unlink("tmp");
	unlink("S2.data"); /*Greg added..file not necessary to keep?*/
	if(flag == MAX_LENGTH)
		return(TRUE);
	else if(flag == FALSE)
		return(FALSE);

}

/*=========================================================================== 
Function: 	AddSelfLoops();
Comments: 	This function adds self loops at each state for every event 
		in the file pointer fp.
Inputs:		fp - file pointer to the file containing the events on which
		a self loop is added at every state.
		fsm_pr -pointer to the FSM on which this operation is performed
============================================================================*/
void AddSelfLoops(FILE *fp, FSM *fsm_pr)
{
	FILE *fp_out;
	int i=0,j=0,k=0,p=0,num_tran,num_aug,num_event,no_states;
	char *augevent[MAX_LENGTH], *tempevent[MAX_LENGTH], *temp[MAX_LENGTH];
	ST_LIST *curr_stat;
	TR_LIST *curr_tran;

	for(i=0;i<MAX_LENGTH;i++) {
		augevent[i] = (char *)calloc(sizeof(char), MAX_LENGTH);
		temp[i] = (char *)calloc(sizeof(char), MAX_LENGTH);
		tempevent[i] = (char *)calloc(sizeof(char), MAX_LENGTH);
	}

	if((fp_out = fopen("fsm.tmp", "w+"))==NULL) {
		perror("File Open");
		exit(1);
	}

	no_states = get_NStates(fsm_pr); /* # of states in the fsm */
	fprintf(fp_out, "%d\n", no_states);	
	i=0;
	while(fscanf(fp, "%s", temp[i])==1) { /*Greg Changed*/
		strcpy(tempevent[i],temp[i]);
		strcpy(augevent[i], temp[i]); 
		i++;
	}
	num_event = i;	/* num of events in the list */
	
	curr_stat = fsm_pr->states; /* point to the initial state */
	curr_tran = fsm_pr->states->trans; /* initial trans of initial state */
	while(curr_stat) {
		num_tran = get_NTrans(curr_stat); /* num of transitions */
		
		/*Write the  data to a tmp file */
		fprintf(fp_out, "\n%s\t%d\t%d\n", curr_stat->name,
				curr_stat->marked, num_event+num_tran);

		/* obtain all transitions at each state */	
		i=0,j=k=num_event;	/* init the variables */
		while(num_tran) {  /* until all transitions are covered */
			/* The existing transitions are maintained */
			fprintf(fp_out,"%s\t%d\t%s\n",curr_tran->input,
				curr_tran->type,curr_tran->next_state->name);
			curr_tran = curr_tran->next; /* point to next tran */
			num_tran--;
		}	
		/* Now write this augmented trans to the FSM */
		for(p=0;p<num_event;p++) {
			fprintf(fp_out, "%s\t%d\t%s\n", tempevent[p],0,
					curr_stat->name);
		}
		
		curr_stat = curr_stat->next; /* point to the next state */
		/* reinitialize trans ptr to point to next state's transition
		as long as all the states are not covered */
		if(curr_stat) {
			curr_tran = curr_stat ->trans;
		}
	}		
	/* close the file after writing */
	fflush(fp_out);
	fclose(fp_out);	
	/* Now read the data written in "fsm.tmp" into an FSM structure */
	if((fp_out = fopen("fsm.tmp", "r"))==NULL) {
		perror("File Open");
		exit(1);
	}
	/* read it into the fsm structure pointer, which was passed to
	this function so that compose.c can use it in its program if needed */
	fsm_read(fp_out, fsm_pr);

	for(i=0;i<MAX_LENGTH;i++) {
		free(augevent[i]);
		free(temp[i]);
		free(tempevent[i]);
	}
	/*free(augevent); //unneccessary freeing
	free(tempevent);
	free(temp);*/
	fclose(fp_out);	
	unlink("fsm.tmp");
	rewind(fp);



} /*AddSelfLoops ends */
