/*===========================================================================
Function:	ProgressTest()
Comments:	This function does a Progress Test on a given plant to check
		if it satisfies progress constraints.
		Note: This should be used only when you need to check if a 
		given sample test system satisfies progress properties or
		not.  It should not be used to synthesize converters.
Inputs:		fsmP - The fsm of the plant
		fsmK - the fsm of the service specfication or desired behavior
		fpK_events - The event set in the desired behavior
		fpK_aug - augmentation event set for the desired behavior
		fsm_result - the resultant state machine is passed back as a
		pointer to the calling function.
		fpLabel- The file pointer to the event set based on which
		the fsm is to be labelled, before performing progress test.

Output:		returns a TRUE if progress test passes else returns a FALSE
============================================================================*/
#include "fsm.h"
#include "converter.h"

int ProgressTest(FSM *fsmP, FSM *fsmK, FILE *fpK_events, FILE *fpK_aug, FSM *fsm_result, FILE *fpLabel)
{

	FSM fsmK_comp;	
	int rv; /* return value */

	if(!fsmP)
		prog_abort("ProgressTest: Null pointer for arg FSM *");
	if(!fsmK)
		prog_abort("ProgressTest: Null pointer for arg FSM *");
	if(!fsm_result)
		prog_abort("ProgressTest: Null pointer for arg FSM *");

	if(!fpK_events)
		prog_abort("ProgressTest: Invalid File pointer");
	if(!fpK_aug)
		prog_abort("ProgressTest: Invalid File pointer");

	/*Complete the graph of the service specification */
        CompleteGraph(fpK_events, fsmK, &fsmK_comp);

	/* Augment the completed graph with uncommon events from fsmP */
        AugmentFsm(fpK_aug, &fsmK_comp);

        /* Compose the completed graph of the service specification with the
        plant fsm */
        fsm_sync_comp(fsmP, &fsmK_comp, fsm_result);

	/* Label the events not belonging to the event set in the file given
	by fpLabel as "*" (epsilon transitions) */
	LabelEvents(fsm_result, fpLabel);

	/* Now call ProgressCheck to see if the system passes progress tests
	or not */ 
	rv = ProgressCheck(fsm_result, fsmK);
 
	rewind(fpK_events); 
        rewind(fpK_aug);
        rewind(fpLabel);
        
        return(rv);


}

