----------------------------- MODULE MCTwoPhase ----------------------------- 
(***************************************************************************)
(* This module is added because TLC does not allow a compound identifier   *)
(* like Bar!AltSpec to be given as a PROPERTY in the configuration file.   *)
(***************************************************************************)
EXTENDS TwoPhase
Bar_AltSpec == Bar!AltSpec
=============================================================================