<<>> <> <> <> <> <> <<>> DIRECTORY BridgeExec, IO, Rope, TypeScript, ViewerEvents ; BridgeRTTY: CEDAR DEFINITIONS ~ { <> <<>> ROPE: TYPE ~ Rope.ROPE; CaveState: TYPE ~ {dead, starting, opening, open, closing, closed, winner}; CaveStateCross: TYPE ~ RECORD [a: CaveState, b: CaveState]; PrivateInstance: TYPE ~ REF PrivateInstanceObject; PrivateInstanceObject: TYPE ~ RECORD [ args: ROPE ¬ NIL, nsp: BridgeExec.NetworkStreamPair ¬ [NIL, NIL], session: BridgeExec.Session ¬ NIL, caveState: CaveState ¬ dead, typescript: TypeScript.TS ¬ NIL, in: IO.STREAM ¬ NIL, out: IO.STREAM ¬ NIL, consumeUser: PROCESS ¬ NULL, consumeService: PROCESS ¬ NULL, stopFlushing: BOOL ¬ FALSE, -- for the forked output flusher outChanged: BOOL ¬ FALSE -- for the forked output flusher ]; <> <<>> UnknownTransition: ERROR; ChangeState: PROC [instance: PrivateInstance, new: CaveState]; ShutDown: PROC [instance: PrivateInstance] RETURNS [yes: BOOL ¬ TRUE]; ViewerEventDestroyProc: ViewerEvents.EventProc; Destroy: BridgeExec.DestroyProc; RttyCreate: BridgeExec.CreateProc; }.