(* Control execution *)

\* RunProcessRunning( stepdefs ) ==  { e.process : e \in Head( stepdefs ) }

RunInTransaction == tx_running                   \* state variable tx_running records transaction state