(* Control execution *)

\* RunProcessRunning( stepdefs ) ==  { e.process : e \in Head( stepdefs ) }
RunProcessRunning( stepdefs ) ==  (CHOOSE s \in Head( stepdefs ): TRUE ).process
RunProcessEnabled( stepdefs, s ) == Len( stepdefs ) # 0 /\ s =  RunProcessRunning( stepdefs )
RunProcessesToRun( stepdefs ) == Tail( stepdefs )
RunProcessParameter( stepdefs ) == Head( stepdefs )