(***********************************************************************
     Macros to control process execution && time
     ***********************************************************************)
    macro tick() {
          now := TickNext( now ); \* now := now + 1;
    }
    
    macro enable( s ) {
      (* head in sequence 'steps' enable processes *)
      \* await Len( steps ) # 0 /\ ProcessEnabled( steps, s );
      await ProcessEnabled( steps, s );
      
      (* process entered, remove head from sequence 'steps' *)
      step  := ProcessRunning( steps ); \* Head( steps );
      step_parameter  := ProcessParameter( steps );
      \* steps := ProcessesToRun( steps ); \* Tail( steps );

      (* Reset infrastructure service responses on process entry *)
      responses := InfrastructureServiceInit;

      (* time advances by one tick for each process step *)
      tick();
      \* debug( s );
    }

    (*  Remove currently running prosess from head of 'step'.
    
	Calling this macro enables next process to take turn.
        If a process comprises several steps, this results
	processes runing parallel, unless 'process_done' is
	called in the end of the process.
    
    *)
    
    macro process_done( s ) {
        steps := ProcessesToRun( steps ); \* Tail( steps );
    }