/*===========================================================================
Function:	SafetyTest()
Comments:	This function offers a higher level of abstraction to the
		function SafetyCheck.  This function will prepare the data
		before hand and do the composition of two state machines
		before calling SafetyCheck.
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.

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

int SafetyTest(FSM *fsmP, FSM *fsmK, FILE *fpK_events, FILE *fpK_aug, FSM *fsm_result)
{
	FSM fsmK_comp;	
	int rv;	/* return Value */

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

	if(!fpK_events)
		prog_abort("SafetyTest: Invalid file pointer");
	if((fpK_aug))
		prog_abort("SafetyTest: 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);

	/* Now call SafetyCheck to see if the system is safe or not */
	rv = SafetyCheck(fsm_result);

	rewind(fpK_events);
	rewind(fpK_aug);
	
	return(rv);
	

} /* EOF SafetyTest */
