#include "fsm.h"
#include "converter.h"
/***************************************************************************
Function: ProgressCheck()
Purpose: This function ensures that there is no dead locking in the 
	 fsm, obtained after safety checks are made.
	 A state is declared bad, if on executing an external event, 
	 the reachability analysis results in reaching an undesirable state.
	 Now an undesirable state is one where the second co-ordinate is a 
	 dump state.
	 This is an initialization procedure and it does not delete any of the
	 bad states.  A state (x, y), where y!= dump is declared bad if the 
	 set of external events of A is not a subset or equal to the set of 
	 external events that can be executed at (x, y) in B sync_composition 
	 Ac, after zero or more internal transitions.
Input:	 fsm_ptr - pointer to the fsm which contains the machine on which 
	 progress checks are to be made.
	 fsm_serv - pointer to the system which contains the desired service
	 behavior.
Output:	 return a TRUE or FALSE value depending on whether progress passed
	 or failed.

Author:	 Sudhir Nelvagal
Advisor: Dr. Ratnesh Kumar

*****************************************************************************/
int ProgressCheck(FSM *fsm_ptr, FSM *fsm_serv)
{
	char *tran_label[MAX_LENGTH], *serv_trlabel[MAX_LENGTH];
	char temp_name[10];
	int i=0,count=0,j=0, k=0,ext_hit=0, ext_miss=0, no_trans=0;
	int no_of_states=0,found, subset;
	int passed=MAX_LENGTH; /* init the flag to an arbitrary value */
	ST_LIST *current, *curr_ptr,*temp_ptr;
	TR_LIST *current_tr, *curr_trns, *temp_tr;
	NAME_LIST *list = NULL, *name_ptr=NULL;

	if(!fsm_ptr) 
		prog_abort("ProgressCheck: Null pointer as arg for FSM* ");
	if(!fsm_serv)
		prog_abort("ProgressCheck: Null pointer as arg for FSM* ");

	for(i=0;i<MAX_LENGTH;i++) {
		tran_label[i] = (char *)calloc(LENGTH, sizeof(char));
		serv_trlabel[i] = (char *)calloc(LENGTH, sizeof(char));
	}
	i=0;
	
	/* Now mark the states as bad if the set of external events that
	can be executed at (x, y) in B sync_comp Ac after zero or more 
	internal transitions results in a bad state...which is defined */

	/* initialize all the pointers so that we start from the first
	state */
	current = fsm_ptr->states;
	current_tr = fsm_ptr->states->trans;
	j=0,i=0;
	while(current) {
 		/* if (x,y) such that y !=dump@$, which are the bad states */
	  	if(strstr(current->name, "@$")==NULL) {
		 /* compute reachability or epsilon closure */
		 no_of_states=fsm_reachability(fsm_ptr,current->name,"*",&list);
		 name_ptr = list;
		 while(name_ptr) {
			temp_ptr = fsm_ptr->states;
			strcpy(temp_name, name_ptr->name);
			while(temp_ptr) {
			  if(strcmp(temp_ptr->name, temp_name)==0 &&
		  	     strstr(temp_name, "@$")==NULL) {
			 	no_trans = get_NTrans(temp_ptr);
				temp_tr = temp_ptr->trans;
				while(temp_tr){
				 if(strcmp(temp_tr->input, "*")!=0){
				   found=FindLabel(tran_label, temp_tr->input);
				   if(!found) {
				     strcpy(tran_label[j],temp_tr->input);
				     break;
				     j++;
				   }
				  }	
				   temp_tr = temp_tr->next;
				}
			  }
			 temp_ptr = temp_ptr->next;
			}							
			name_ptr = name_ptr->next;			
		 } 
		/* check to see if the set of ext events that can be executed
	  	at y in A is a subset of the set of ext events that can be 
	  	executed at (x, y) in B sync_comp Ac after zero or more
	  	external transitions, with the end state being a good state*/
		
		 
		curr_ptr = fsm_serv->states;
		while(curr_ptr) {
			/* co-ordinate y in composed sysem must be a co-ordinate in A */
			if(strstr(current->name, curr_ptr->name)!=NULL) {
				curr_trns = curr_ptr->trans;
				while(curr_trns) {
				   strcpy(serv_trlabel[k], curr_trns->input);
				   k++;
				   curr_trns = curr_trns->next;
				}
			}
			curr_ptr = curr_ptr -> next;
		} /* while curr_ptr ends */

		/* Do a containment test on the event labels from the composed
		system and the desired service specification */
		
		subset = Containment(tran_label, serv_trlabel);
		if(!subset) {
			MarkBadState(fsm_ptr, current, temp_tr);
			passed = FALSE;
		}
		
		/* point to the next state in the main loop*/
		}  /* If on line 60 ends */
		current = current ->next;
 
		for(j=0;j<MAX_LENGTH;j++) {
			*tran_label[j] ='\0';	
			*serv_trlabel[j] = '\0';
		}
		free(list);
		j = 0;
		k = 0;
	} 	/* while current  ends */ 
	for(j=0;j<MAX_LENGTH;j++) {
		free(tran_label[j]);	
		free(serv_trlabel[j]);
	}
	/*free(*name_ptr);this gives an error, note, name_ptr = list..so freed with next line (GREG)*/
	delete_name(&list);
	if(passed == MAX_LENGTH)
		return(TRUE);
	else if(passed == FALSE)
		return(FALSE);
} 
