Controllability Check:
---------------------
Default Input Files :  control.data, (control.data_events)
Default Output File:  control.results
 
control.data contains the FSM to be checked.
control.data_events contains the controllability information (masking info is ignored) of control.data FSM.
Filename control.data_events is obtained automatically by concatenating "_events" to the first input filename. 
control.data_events is to be created before running this function through "Cont/Mask Info Table" in the GUI. Do not specify this event file as one of the input files.
This function checks whether the FSM specified in control.data is controllable or not.
control.results contains either "Controllable" or "Not Controllable".


Underlying function: int ControlCheck(FSM *fsm_ptr, FILE *fp)
Modified Parameters: integer return
Temporary Files Used: clist0.tmp
Source: ControlCheck.h, control.c

Performs a control check on a given state machine.
fsm_ptr is the pointer to the FSM under consideration. 
fp contains the controllability information of all events in the FSM.  This file is generated from the input "_events" file before ControlCheck is called.
Returns TRUE if input FSM is controllable, or FALSE otherwise.

It is recommended to use ControlCheck in order to synthesize controllers.

