Diagnosability Check Under Partial Observation:
---------------------------------------------
Default Input Files:  diagnosability_plant.data, diagnosability_spec.data, (diagnosability_plant.data_events)
Default Output File:  diagnosability.results
 
diagnosability_plant.data is the plant FSM.
diagnosability_spec.data is the specification FSM.
Filename diagnosability_plant.data_events is obtained automatically by concatenating "_events" to the first input filename. 
diagnosability_plant.data_events contains the masking information (controllability info is ignored) of diagnosability_plant.data.
diagnosability_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.

Determines whether FSM of plant diagnosability_plant.data is diagnosable under specification diagnosability_spec.data with controllability information in diagnosability_plant.data_events.
diagnosability.results contains either "Diagnosable" or "Not Diagnosable".


Underlying function: int po_diagnosability(FSM *fsmIn)
Modified Parameters: FSM *fsmIn, integer return
Temporary Files Used: mmlistfiles.tmp, mlist*.tmp
Source: Diagnosability.h, partialobs.c

fsmIn 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 diagnosability.
Returns TRUE if input FSM is diagnosable, or FALSE otherwise.