Masking:
------
Default Input Files:  mask.data, (mask.data_events)
Default Output File:  mask.results

mask.data is the FSM to be masked.
mask.data_events contains the masking information (controllability info is ignored) of mask.data.
Filename mask.data_events is obtained automatically by concatenating "_events" to the first input filename.
mask.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.

Underlying function: void fsm_mask(FILE *fp, FSM *fsm1_ptr, FSM* fsm2_ptr)
Modified Parameters: FSM* fsm2_ptr
Temporary Files Used: mlist0.data
Source: Mask.h, fsm_general.c
 
Masks a state machine.
fp is a pointer to the input file containing the masking information.  This file is created from mask.data_events before calling the function.
fsm1_ptr is a pointer to the FSM to be masked.
fsm2_ptr is a pointer to the resulting masked FSM.
