IMPLEMENTATION MODULE TERMINATION;
(* HALT terminates the image immediately ($abort/exit), so HasHalted
   is never observable as TRUE; termination is likewise not modelled
   across coroutines yet.  Both query the runtime flags. *)

PROCEDURE m2terminating () : BOOLEAN;
  EXTERNAL;

PROCEDURE m2hashalted () : BOOLEAN;
  EXTERNAL;

PROCEDURE IsTerminating () : BOOLEAN;
BEGIN
  RETURN m2terminating()
END IsTerminating;

PROCEDURE HasHalted () : BOOLEAN;
BEGIN
  RETURN m2hashalted()
END HasHalted;

END TERMINATION.