Normality Check Under Partial Observation:
-----------------------------------------
Default Input Files:  normality_plant.data, normality_spec.data, (normality_plant.data_events)
Default Output File:  normality.results
 
normality_plant.data is the plant FSM.
normality_spec.data is the specification FSM.
Filename normality_plant.data_events is obtained automatically by concatenating "_events" to the first input filename.
normality_plant.data_events contains the masking information (controllability info is ignored) of normality_plant.data.
normality_plant.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 determines whether FSM of plant po_plant.data is normal under specification 

Determines whether FSM of plant normality_plant.data is normal under specification normality_spec.data with masking information in normality_plant.data_events.
normality.results contains either "Normal" or "Not Normal".


Underlying function: int po_normality(FSM *fsmR, MULT_MASKL *mmaskL)
Modified Parameters: FSM *fsmR, integer return
Temporary Files Used: mmlistfiles.tmp, mlist*.tmp
Source: Normality.h, partialobs.c

fsmR is a pointer to an FSM that has been created using the specification and masking information before the function is called.  This FSM is modified in the process of determining normality.
mmaskL is generated from normality_plant.data_events before calling this function.
Returns 1 if FSM is normal, 0 otherwise.