(***********************************************************************
     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 );
      \* NOTICE deterministic .await and with NON-determ choice below
      \* MUST \ s1,s2 \ steps: s1.process = s2.process
      await ProcessEnabled( steps, s );
      
      (* process entered, remove head from sequence 'steps' *)
      with ( r \in Head( steps ) ) {
	 \* step  := ProcessRunning( steps ); \* Head( steps ).process;
	 \* step_parameter  := ProcessParameter( steps );
	 \* await( r.process = s);
         step := r.process;
	 step_parameter := r;
      };
      
      \* steps := ProcessesToRun( steps ); \* Tail( steps );

      \* Context to resume to from Head(steps ), Nil = not resuming
      resume_context  := ProcessStep( steps ).ctx;      

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

      (* Flag Transaction started *)
      tx_running := TRUE;

      (* 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 );

        \* process must clear resume context
	assert( resume_context = Nil );
	
	(* Flag Transaction started *)
        tx_running := FALSE;
	
    }