Observability Check Under Partial Observation:
---------------------------------------------
Default Input Files: observability_plant.data, observability_spec.data, (observability_plant.data_events)
Default Output File: observability.results

observability_plant.data is the plant FSM.
observability_spec.data is the specification FSM.
observability_plant.data_events contains the masking information (controllability info is ignored) of observability_plant.data.
Filename observability_plant.data_events is obtained automatically by concatenating "_events" to the first input filename. 
observability_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 observability of plant observability_plant.data under specification observability_spec.data masking information in observability_plant.data_events.
observability.results contains either "Observable" or "Not Observable".


Underlying function: int po_observability(FSM *fsmR)
Modified Parameters: FSM *fsmR, integer return
Temporary Files Used: mmlistfiles.tmp, mlist*.tmp
Source: Observability.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 observability.
Returns TRUE if input FSM is observable, or FALSE otherwise