Enabler.java

package edu.udel.cis.vsl.tass.kripke.impl;

import java.io.PrintWriter;
import java.util.LinkedList;
import java.util.NoSuchElementException;

import edu.udel.cis.vsl.tass.config.RunConfiguration;
import edu.udel.cis.vsl.tass.config.RunConfiguration.DeadlockStrategy;
import edu.udel.cis.vsl.tass.dynamic.IF.DynamicException;
import edu.udel.cis.vsl.tass.dynamic.IF.DynamicFactoryIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.ValueIF;
import edu.udel.cis.vsl.tass.kripke.IF.TASSEnablerIF;
import edu.udel.cis.vsl.tass.model.IF.CollectiveAssertionIF;
import edu.udel.cis.vsl.tass.model.IF.ModelIF;
import edu.udel.cis.vsl.tass.model.IF.ModelSequence;
import edu.udel.cis.vsl.tass.model.IF.ProcessIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ExpressionIF.ExpressionKind;
import edu.udel.cis.vsl.tass.model.IF.location.AnySourceReceiveLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.LocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.SendLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.StandardReceiveLocationIF;
import edu.udel.cis.vsl.tass.model.IF.statement.ReceiveStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.SendStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.StatementIF;
import edu.udel.cis.vsl.tass.morph.MorphicVector;
import edu.udel.cis.vsl.tass.number.IF.IntegerNumberIF;
import edu.udel.cis.vsl.tass.number.IF.NumberIF;
import edu.udel.cis.vsl.tass.semantics.Semantics;
import edu.udel.cis.vsl.tass.semantics.IF.LogIF;
import edu.udel.cis.vsl.tass.semantics.IF.EvaluatorIF;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionException;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionStateException;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionProblem.Certainty;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionProblem.ErrorKind;
import edu.udel.cis.vsl.tass.state.States;
import edu.udel.cis.vsl.tass.state.IF.CollectiveRecordIF;
import edu.udel.cis.vsl.tass.state.IF.StateFactoryIF;
import edu.udel.cis.vsl.tass.state.IF.StateIF;
import edu.udel.cis.vsl.tass.state.IF.SystemEnvironmentIF;
import edu.udel.cis.vsl.tass.transition.IF.SimpleTransitionIF;
import edu.udel.cis.vsl.tass.transition.IF.SynchronousTransitionIF;
import edu.udel.cis.vsl.tass.transition.IF.TransitionFactoryIF;
import edu.udel.cis.vsl.tass.transition.IF.TransitionIF;
import edu.udel.cis.vsl.tass.transition.IF.TransitionSequenceIF;

/**
 * This enabler implements both the standard ("full") enabling algorithm, and
 * the Urgent Partial Order Reduction scheme. It can be applied to multiple
 * models or a single model. If applied to multiple models, it also applies in
 * the case where the models run sequentially (i.e., one model runs to
 * completion, then the next one runs to completion, etc.) or the case where the
 * models run concurrently.
 * 
 * Urgent POR (Partial Order Reduction): The strategy will either return the set
 * of all enabled transitions ("full") or the set of enabled transitions for one
 * process. In the latter case, a receive statement for which there is no
 * buffered messages encodes a synchronous transition in which the corresponding
 * send in the sending process must execute first. (I.e., a synchronous
 * transition is considered to reside in the receiving process.)
 * <p>
 * 
 * Loop through procs, starting from 0 and moving up. If there are no enabled
 * transitions from this proc continue.
 * <p>
 * 
 * If location is local (see method isLocal in class LocationIF), the set of
 * enabled transitions is the set of all enabled transitions from that proc.
 * <p>
 * 
 * If location is (regular, non-anysource) receive, and all variables are local,
 * and the receive is enabled or there is a matching send which can execute
 * synchronously with it, return this transition.
 * <p>
 * 
 * If location is an anysource-receive, and all are enabled (or you know they
 * will never be enabled) or synchronously enabled return set of all transitions
 * from this receive.
 * 
 * If you can't find one like above, return set of all enabled transitions.
 * 
 * @author siegel
 * 
 */
public class Enabler implements TASSEnablerIF {

	private ModelSequence modelSequence;

	private TransitionFactoryIF transitionFactory;

	private int numModels;

	private int totalNumProcs;

	private DynamicFactoryIF dynamicFactory;

	// private int numProcs;

	private EvaluatorIF evaluator;

	private SystemEnvironmentIF environment;

	private boolean debug = false;

	private PrintWriter debugOut = null;

	private ValueIF trueValue, falseValue;

	private LogIF log;

	private int bottom;

	private StateIF cachedState = null;

	private TransitionSequenceIF cachedSequence = null;

	/**
	 * If true: run one model to completion before next model starts. Otherwise:
	 * models run concurrently.
	 */
	private boolean sequential;

	/**
	 * If true: no partial order reduction within a model: explore all possible
	 * transitions within that model.
	 */
	private boolean full;

	private boolean useCollectiveAssertions;

	private boolean useLoopTechnique;

	private boolean findPotentialDeadlocks;

	/** Replaying a trace? */
	private boolean replay = false;

	/**
	 * Used if replaying a trace: for each sequence in the stack with more than
	 * one outgoing transition, this gives the index of the transition to
	 * choose. This is null if not replaying a trace.
	 */
	private int[] guide = null;

	/** Current position in guide. Used only if replaying trace. */
	private int guideIndex = 0;

	public Enabler(ModelSequence modelSequence,
			DynamicFactoryIF dynamicFactory, StateFactoryIF stateFactory,
			TransitionFactoryIF transitionFactory, int bufferSize, LogIF log,
			boolean sequential, boolean full) {
		RunConfiguration configuration = dynamicFactory.configuration();

		this.replay = configuration.replay();
		if (replay) {
			this.guide = configuration.guide();
		}
		this.useCollectiveAssertions = configuration.useCollectiveAssertions();
		this.useLoopTechnique = configuration.useLoopTechnique();
		this.modelSequence = modelSequence;
		this.numModels = modelSequence.numModels();
		this.transitionFactory = transitionFactory;
		this.totalNumProcs = modelSequence.totalNumProcs();
		this.dynamicFactory = dynamicFactory;
		this.log = log;
		this.sequential = sequential;
		this.full = full;
		this.evaluator = Semantics
				.newEvaluator(dynamicFactory, bufferSize, log);
		this.environment = States.newEnvironment(modelSequence, stateFactory,
				log);
		this.trueValue = dynamicFactory.trueValue();
		this.falseValue = dynamicFactory.falseValue();
		this.bottom = (useLoopTechnique ? 1 : 0);
		this.findPotentialDeadlocks = configuration.deadlockStrategy() == DeadlockStrategy.POTENTIAL;
	}

	public void setReplay(int[] guide) {
		assert guide != null;
		this.guide = guide;
		this.replay = true;
	}

	/* Methods to create TransitionSequence objects... */

	/**
	 * Constructs and returns a new empty transition sequence. hasNext will
	 * return false. It can be initialized by shifting on transitions, or used
	 * to represent an empty sequence.
	 */
	private TransitionSequenceIF newEmptyFullTransitionSequence(StateIF state) {
		return transitionFactory.newTransitionSequence(state, true);
	}

	/**
	 * Creates a new transition sequence object representing the ordered set of
	 * "ample" transitions resulting from Partial Order Reduction. The sequence
	 * is specified by providing the first transition in the sequence. When
	 * peek() or next() is called, this given firstTransition will be returned.
	 */
	private TransitionSequenceIF newPartialTransitionSequence(StateIF state,
			TransitionIF firstTransition) {
		TransitionSequenceIF result = transitionFactory.newTransitionSequence(
				state, false);

		result.shift(firstTransition);
		proceedToNextPartial(result);
		return result;
	}

	/** Returns true iff the sequence has length exactly 1. */
	@Override
	public boolean hasOneTransition(TransitionSequenceIF sequence) {
		return sequence.peek() != null && sequence.peek2() == null;
	}

	public void setCache(StateIF state, TransitionSequenceIF sequence) {
		this.cachedState = state;
		this.cachedSequence = sequence;
	}

	public TransitionSequenceIF enabledTransitions(StateIF state) {
		TransitionSequenceIF sequence;

		if (state == cachedState) {
			sequence = cachedSequence;
			cachedState = null;
			cachedSequence = null;
			return sequence;
		}
		sequence = computeEnabledTransitions(state);
		if (replay && sequence.isMultiple()) {
			int index = guide[guideIndex];

			guideIndex++;
			for (int i = 0; i < index; i++) {
				if (!hasNext(sequence)) {
					log.report(new ExecutionStateException(state.locations(),
							ErrorKind.INTERNAL, Certainty.NONE,
							"Playback failure: request for transition " + index
									+ " but only " + (i + 1)
									+ "transition(s) enabled."));
				}
				next(sequence);
			}
			assert peek(sequence) != null;
			// nullify second transition...
			sequence.prune();
		}
		return sequence;
	}

	public TransitionSequenceIF computeEnabledTransitions(StateIF source) {
		TransitionSequenceIF result;

		if (source.pathCondition().equals(falseValue))
			return newEmptyFullTransitionSequence(source);
		try {
			if (sequential) { // sequential execution of models
				for (int i = 0; i < numModels; i++) {
					ModelIF model = modelSequence.modelWithIndex(i);

					result = (full ? allEnabled(model, source)
							: enabledTransitionsUrgent(model, source));
					if (result != null)
						return result;
				}
			} else { // concurrent execution of models
				if (full) { // all enabled transitions in a model
					assert false; // this foolish option not supported
				} else { // urgent POR
					result = enabledUrgentConcurrent(source);
					if (result != null)
						return result;
				}
			}
		} catch (ExecutionException e) {
			log.report(e);
			return newEmptyFullTransitionSequence(source);
		}
		if (useLoopTechnique || useCollectiveAssertions) {
			MorphicVector<CollectiveRecordIF> queue = source.collectiveQueue();
			int queueSize = queue.size();

			if (queueSize > bottom) {
				log.report(new ExecutionStateException(source.locations(),
						ErrorKind.ASSERTION_VIOLATION, Certainty.MAYBE,
						"Collective assertions remained when program halted at "
								+ source));
			}
		}
		return newEmptyFullTransitionSequence(source);
	}

	/**
	 * Returns the set of all enabled transitions in a given model, from the
	 * given state, assuming there is at least one. Else returns null. Used by
	 * both urgent and full algorithms.
	 */
	private TransitionSequenceIF allEnabled(ModelIF model, StateIF source) {
		TransitionSequenceIF sequence = newEmptyFullTransitionSequence(source);

		if (proceedToNextFull(model, sequence, true)) {
			// at least 1 enabled transition queued up
			proceedToNextFull(model, sequence, false);
			// queue up the second one
			return sequence;
		} else {
			return null;
		}
	}

	/**
	 * Is this an essentially non-deterministic (END) state? Need the set of
	 * outgoing transitions to tell.
	 */
	public boolean isNonDeterministic(TransitionSequenceIF sequence) {
		if (!sequence.isMultiple())
			// only one transition
			return false;
		if (!sequence.full() || totalNumProcs == 1) {
			TransitionIF transition = sequence.peek();

			if (transition instanceof SimpleTransitionIF) {
				SimpleTransitionIF simple = (SimpleTransitionIF) transition;
				StatementIF statement = simple.statement();
				LocationIF location = statement.sourceLocation();

				if (location.isBranch() || location.isLoop())
					return false;
			} else {
				assert false;
			}
		}
		return true;
	}

	/**
	 * Attempts to form an ample set from the enabled transitions of the given
	 * process, from the given state. If this is not possible, returns null.
	 * Ensures that there is at least one enabled transition.
	 */
	private TransitionSequenceIF enabledTransitionsUrgent(ProcessIF process,
			StateIF source) throws ExecutionException {
		LocationIF location = environment.location(process);
		ValueIF pathCondition;

		environment.setState(source);
		pathCondition = environment.getAssumption();
		if (location == null || pathCondition.equals(falseValue))
			return null;
		if (location.isLocal()) {
			for (StatementIF statement = location.firstStatement(); statement != null; statement = statement
					.next()) {
				ValueIF newPathCondition = newPathCondition(statement);

				if (newPathCondition != null) {
					return newPartialTransitionSequence(source,
							transitionFactory.newSimpleTransition(statement,
									newPathCondition));
				}
			}
		} else if (location instanceof SendLocationIF) {
			SendLocationIF sendLocation = (SendLocationIF) location;
			SendStatementIF send = sendLocation.statement();
			ExpressionIF destinationExpression = send.destination();
			ValueIF destinationValue = evaluator.evaluate(environment,
					destinationExpression);
			NumberIF destinationNumber;

			destinationNumber = dynamicFactory.numericValue(trueValue,
					destinationValue);
			if (destinationNumber != null) {
				if (destinationNumber.signum() < 0) {
					// represents a no-op send (as in send to MPI_PROC_NULL)
					return newPartialTransitionSequence(source,
							transitionFactory.newSimpleTransition(send,
									pathCondition));
				}
			}
			// a buffered send can be used for ample if not interested
			// in potential deadlock
			if (!findPotentialDeadlocks) {
				ValueIF newPathCondition = newPathCondition(send);

				if (newPathCondition != null) {
					TransitionSequenceIF result = newPartialTransitionSequence(
							source, transitionFactory.newSimpleTransition(send,
									newPathCondition));

					result.setBufferedSend(true);
					return result;
				}
			}
		} else if (location instanceof StandardReceiveLocationIF) {
			StandardReceiveLocationIF receiveLocation = (StandardReceiveLocationIF) location;
			ReceiveStatementIF receive = receiveLocation.statement();
			ValueIF newPathCondition = newPathCondition(receive);
			ExpressionIF sourceExpression = receive.source();
			ValueIF sourceValue = evaluator.evaluate(environment,
					sourceExpression);
			NumberIF sourceNumber;

			sourceNumber = dynamicFactory.numericValue(trueValue, sourceValue);
			if (sourceNumber != null) {
				if (sourceNumber.signum() < 0) {
					// represents a no-op receive, as in MPI_PROC_NULL
					return newPartialTransitionSequence(source,
							transitionFactory.newSimpleTransition(receive,
									pathCondition));
				}
			}
			if (newPathCondition != null) {
				return newPartialTransitionSequence(source,
						transitionFactory.newSimpleTransition(receive,
								newPathCondition));
			} else {
				SendStatementIF send = match(receive);

				if (send != null)
					return newPartialTransitionSequence(source,
							transitionFactory.newSynchronousTransition(send,
									receive, pathCondition));
			}
		} else if (location instanceof AnySourceReceiveLocationIF) {
			TransitionIF transition = null;
			boolean urgent = true;

			for (StatementIF statement : location.statements()) {
				ReceiveStatementIF receive = (ReceiveStatementIF) statement;
				ValueIF newPathCondition = newPathCondition(receive);
				SendStatementIF send = null;

				if (newPathCondition == null && (send = match(receive)) == null) {
					if (!senderTerminated(receive)) {
						urgent = false;
						break;
					}
				} else {
					if (transition == null) {
						if (newPathCondition != null) {
							transition = transitionFactory.newSimpleTransition(
									receive, pathCondition);
						} else {
							transition = transitionFactory
									.newSynchronousTransition(send, receive,
											pathCondition);
						}
					}
				}
			}
			if (urgent && transition != null)
				return newPartialTransitionSequence(source, transition);
		}
		return null;
	}

	/**
	 * Returns a set of enabled transitions from a model, using the urgent POR.
	 * If no ample set is found, it will return the set of all enabled
	 * transitions, assuming there is at least one. If there are no enabled
	 * transitions, will return null.
	 */
	private TransitionSequenceIF enabledTransitionsUrgent(ModelIF model,
			StateIF source) throws ExecutionException {
		int numProcs = model.numProcs();
		TransitionSequenceIF result;
		TransitionSequenceIF bufferedSendSequence = null;

		environment.setState(source);
		for (int i = 0; i < numProcs; i++) {
			ProcessIF process = model.process(i);

			result = enabledTransitionsUrgent(process, source);
			if (result != null) {
				if (result.isBufferedSend()) {
					// use this one only if no other is available.
					if (bufferedSendSequence == null)
						bufferedSendSequence = result;
				} else {
					return result;
				}
			}
		}
		if (bufferedSendSequence != null)
			return bufferedSendSequence;
		return allEnabled(model, source);
	}

	/**
	 * Returns a nonempty set of enabled transitions in one model, or null if
	 * there is no enabled transition in any model. Urgent POR is used, and a
	 * preference for a process which is "behind" in a collective action is also
	 * used. If no "behind" process can be used for an ample set, preference is
	 * given to a model which is a "laggard", i.e., has at least one process
	 * which is behind.
	 */
	private TransitionSequenceIF enabledUrgentConcurrent(StateIF source)
			throws ExecutionException {
		TransitionSequenceIF result;
		MorphicVector<CollectiveRecordIF> queue;
		int queueLength;
		/*
		 * indexes of models that have at least one proc "behind" in a
		 * collective action...
		 */
		LinkedList<Integer> laggardList = new LinkedList<Integer>();
		/* is the model in the laggardList? */
		boolean[] inLaggardList = new boolean[numModels];
		/*
		 * initially all false, set to true if tried to find ample for that
		 * proc, and failed...
		 */
		boolean[] attemptedProcs = new boolean[totalNumProcs];
		/*
		 * intially all false, set to true if there is no enabled transition at
		 * all in that model...
		 */
		boolean[] attemptedModels = new boolean[numModels];

		environment.setState(source);
		queue = environment.collectiveQueue();
		queueLength = queue.size();
		/*
		 * Try to find a process that is "behind" in a collective action and see
		 * if it has an ample set. Start with the most behind, and work up.
		 */
		for (int i = bottom; i < queueLength; i++) {
			CollectiveRecordIF record = queue.get(i);

			if (record.isComplete())
				continue;

			CollectiveAssertionIF assertion = record.assertion();
			int numProcs = assertion.numProcs();

			for (int j = 0; j < numProcs; j++) {
				ProcessIF process = assertion.process(j);

				if (!record.reachedBy(process)) {
					int globalProcIndex = modelSequence
							.globalIndexOfProcess(process);

					if (attemptedProcs[globalProcIndex])
						continue;
					result = enabledTransitionsUrgent(process, source);
					if (result != null) {
						return result;
					} else {
						ModelIF model = process.model();
						int modelIndex = modelSequence.indexOf(model);

						if (!inLaggardList[modelIndex]) {
							laggardList.add(modelIndex);
							inLaggardList[modelIndex] = true;
						}
						attemptedProcs[globalProcIndex] = true;
					}
				}
			}
		}
		/*
		 * If you made it to this point, there was no "behind" process with an
		 * ample set. Now try to schedule a "lagging" model: one with at least
		 * one process that is "behind". If you find such a model, try to find
		 * an ample set in it, but if you can't, schedule all enabled
		 * transitions in that model, assuming there is at least one.
		 */
		for (int modelIndex : laggardList) {
			if (!attemptedModels[modelIndex]) {
				ModelIF model = modelSequence.modelWithIndex(modelIndex);
				int numProcs = model.numProcs();

				for (int i = 0; i < numProcs; i++) {
					ProcessIF process = model.process(i);
					int globalProcIndex = modelSequence
							.globalIndexOfProcess(process);

					if (attemptedProcs[globalProcIndex])
						continue;
					result = enabledTransitionsUrgent(process, source);
					if (result != null) {
						return result;
					} else {
						attemptedProcs[globalProcIndex] = true;
					}
				}
				// no urgent for this model, but try all enabled:
				result = allEnabled(model, source);
				if (result != null)
					return result;
				attemptedModels[modelIndex] = true;
			}
		}
		/*
		 * If you made it this far, there are no "lagging" models with any
		 * enabled transitions. Are there any models left that might have at
		 * least one enabled transition?
		 */
		for (int modelIndex = 0; modelIndex < numModels; modelIndex++) {
			if (!attemptedModels[modelIndex]) {
				ModelIF model = modelSequence.modelWithIndex(modelIndex);
				int numProcs = model.numProcs();

				for (int i = 0; i < numProcs; i++) {
					ProcessIF process = model.process(i);
					int globalProcIndex = modelSequence
							.globalIndexOfProcess(process);

					if (attemptedProcs[globalProcIndex])
						continue;
					result = enabledTransitionsUrgent(process, source);
					if (result != null) {
						return result;
					} else {
						attemptedProcs[globalProcIndex] = true;
					}
				}
				// no urgent for this model, but try all enabled:
				result = allEnabled(model, source);
				if (result != null)
					return result;
				attemptedModels[modelIndex] = true;
			}
		}
		/* At this point there are no enabled transitions in any model */
		return null;
	}

	public boolean debugging() {
		return debug;
	}

	public PrintWriter getDebugOut() {
		return debugOut;
	}

	public boolean hasNext(TransitionSequenceIF sequence) {
		return ((TransitionSequenceIF) sequence).peek() != null;
	}

	public TransitionIF next(TransitionSequenceIF sequence) {
		TransitionSequenceIF seq = (TransitionSequenceIF) sequence;
		TransitionIF transition = seq.peek();

		if (transition == null)
			throw new NoSuchElementException("no next transition from "
					+ seq.state());
		if (seq.full())
			proceedToNextFull(transition.model(), seq, false);
		else
			proceedToNextPartial(seq);
		return transition;
	}

	public TransitionIF peek(TransitionSequenceIF sequence) {
		return ((TransitionSequenceIF) sequence).peek();
	}

	private void print(TransitionIF transition, PrintWriter out) {
		if (transition instanceof SimpleTransitionIF) {
			SimpleTransitionIF simpleTransition = (SimpleTransitionIF) transition;
			StatementIF statement = simpleTransition.statement();

			out.print("\"" + statement + "\", pc: "
					+ transition.pathCondition());
		} else {
			SynchronousTransitionIF synchronousTransition = (SynchronousTransitionIF) transition;
			ReceiveStatementIF receive = synchronousTransition.receive();
			SendStatementIF send = synchronousTransition.send();

			out.print("\"" + send + "\", \"" + receive + "\", pc: "
					+ transition.pathCondition());
		}
	}

	public void print(PrintWriter out, TransitionSequenceIF sequence) {
		TransitionSequenceIF seq = (TransitionSequenceIF) sequence;

		out.print("[source=" + seq.state() + ",transition: ");
		print(seq.peek(), out);
		out.print("]");
	}

	/**
	 * Prints the transition with some additional information concerning the
	 * index of this transition in the sequence.
	 */
	@Override
	public void printFirstTransition(PrintWriter out,
			TransitionSequenceIF sequence) {
		if (sequence == null) {
			out.print("null");
		} else {
			int index = sequence.index();
			TransitionIF transition = sequence.peek();

			out.print("(" + index + ") ");
			if (transition == null) {
				out.print("null");
			} else {
				transition.print(out);
			}
		}
	}

	public void printRemaining(PrintWriter out, TransitionSequenceIF sequence) {
		out.print("remaining transitions");
	}

	public void setDebugOut(PrintWriter out) {
		debugOut = out;
	}

	public void setDebugging(boolean value) {
		debug = value;
	}

	public StateIF source(TransitionSequenceIF sequence) {
		return ((TransitionSequenceIF) sequence).state();
	}

	/**
	 * Proceeds to the next transition in the sequence for a full enabled set of
	 * transitions. A full sequence consists of only simple transitions.
	 * 
	 * If "initialize" is true, then this means that the sequence has not yet
	 * been initialized with any transition, and this method will find and shift
	 * on the first transition, if there is one. In this case, it will return
	 * false if there is no first transition. Otherwise, returns true.
	 * 
	 * If initialize is false, this indicates the sequence has already been
	 * initialized and the first transition in the sequence should be non-null.
	 * In this case the method will find the next transition and shift it on and
	 * return true, if there is a next transition, else it will shift on false
	 * and return false.
	 */
	private boolean proceedToNextFull(ModelIF model,
			TransitionSequenceIF sequence, boolean initialize) {
		int numProcs = model.numProcs();
		SimpleTransitionIF transition = (SimpleTransitionIF) sequence.peek2();
		int pid;
		StatementIF statement = null;

		environment.setState(sequence.state());
		if (transition != null) {
			assert !initialize;
			statement = transition.statement();
			assert statement != null;
			pid = statement.process().pid();
			statement = statement.next();
		} else {
			if (initialize) {
				assert sequence.peek() == null;
				pid = 0;
				statement = (environment.emptyStack(model.process(0)) ? null
						: environment.location(model.process(0))
								.firstStatement());
			} else { // this is the end
				sequence.shift(null);
				return false;
			}
		}
		try {
			while (true) {
				while (statement != null) {
					ValueIF newPathCondition = newPathCondition(statement);

					if (newPathCondition != null) {
						sequence.shift(transitionFactory.newSimpleTransition(
								statement, newPathCondition));
						return true;
					}
					statement = statement.next();
				}
				pid++;
				if (pid >= numProcs)
					break;
				statement = (environment.emptyStack(model.process(pid)) ? null
						: environment.location(model.process(pid))
								.firstStatement());
			}
		} catch (ExecutionException e) {
			log.report(e);
		}
		sequence.shift(null);
		return false;
	}

	/**
	 * Proceeds to next transition in sequence in the case where the sequence
	 * represents a proper urgent set. It assumes this sequence has already been
	 * initialized.
	 */
	private void proceedToNextPartial(TransitionSequenceIF sequence) {
		TransitionIF transition = sequence.peek2();
		StatementIF statement = null;
		LocationIF location;
		ValueIF pathCondition;

		if (transition == null) { // at end...
			sequence.shift(null);
			return;
		}
		environment.setState(sequence.state());
		pathCondition = environment.getAssumption();
		assert pathCondition != null && !pathCondition.equals(falseValue);
		if (transition instanceof SimpleTransitionIF) {
			statement = ((SimpleTransitionIF) transition).statement();
		} else {
			statement = ((SynchronousTransitionIF) transition).receive();
		}
		location = statement.sourceLocation();
		statement = statement.next();
		if (statement == null) {
			sequence.shift(null);
			return;
		}
		if (location.isLocal()) {
			try {
				while (statement != null) {
					ValueIF newPathCondition = newPathCondition(statement);

					if (newPathCondition != null) {
						sequence.shift(transitionFactory.newSimpleTransition(
								statement, newPathCondition));
						return;
					}
					statement = statement.next();
				}
			} catch (ExecutionException e) {
				log.report(e);
			}
			sequence.shift(null);
			return;
		}
		if (location instanceof AnySourceReceiveLocationIF) {
			try {
				while (statement != null) {
					ReceiveStatementIF receive = (ReceiveStatementIF) statement;
					ValueIF newPathCondition = newPathCondition(receive);
					SendStatementIF send = null;

					if (newPathCondition != null) {
						sequence.shift(transitionFactory.newSimpleTransition(
								receive, pathCondition));
						return;
					} else if ((send = match(receive)) != null) {
						sequence.shift(transitionFactory
								.newSynchronousTransition(send, receive,
										newPathCondition));
						return;
					}
					statement = statement.next();
				}
			} catch (ExecutionException e) {
				log.report(e);
			}
			sequence.shift(null);
			return;
		}
		throw new RuntimeException("Unknown urgent set type of location: "
				+ location + ": " + location.kind());
	}

	private ValueIF newPathCondition(StatementIF statement)
			throws ExecutionException {
		try {
			ValueIF oldPathCondition = environment.getAssumption();
			ExpressionIF guardExpression = statement.guard();
			ValueIF guardValue = evaluator.evaluate(environment,
					guardExpression);

			if (dynamicFactory.isValid(oldPathCondition, guardValue)) {
				return oldPathCondition;
			} else if (dynamicFactory.isValid(oldPathCondition,
					dynamicFactory.not(oldPathCondition, guardValue))) {
				return null;
			} else {
				ValueIF newPathCondition = dynamicFactory.and(trueValue,
						oldPathCondition, guardValue);

				// TODO: experiment: always simplify path condition....
				// newPathCondition = dynamicFactory.noAssumptionSimplifier()
				// .simplify(newPathCondition);
				return newPathCondition;
			}
		} catch (DynamicException e) {
			throw new ExecutionException(statement, e, Certainty.NONE);
		}
	}

	private ProcessIF getSource(ReceiveStatementIF statement)
			throws ExecutionException {
		ModelIF model = statement.model();

		ValueIF assumption = environment.getAssumption();
		ExpressionIF sourceExpression = statement.source();
		ValueIF sourcePidValue = evaluator.evaluate(environment,
				sourceExpression);
		int sourcePid = ((IntegerNumberIF) dynamicFactory.numericValue(
				assumption, sourcePidValue)).intValue();
		ProcessIF sender = model.process(sourcePid);

		return sender;
	}

	private ProcessIF getDestination(SendStatementIF statement)
			throws ExecutionException {
		ModelIF model = statement.model();

		ExpressionIF destinationExpression = statement.destination();
		ValueIF destinationPidValue = evaluator.evaluate(environment,
				destinationExpression);
		int destinationPid = ((IntegerNumberIF) dynamicFactory.numericValue(
				environment.getAssumption(), destinationPidValue)).intValue();
		ProcessIF destination = model.process(destinationPid);

		return destination;
	}

	/**
	 * Given a receive statement that is not currently enabled, find out if
	 * there is a matching send currently enabled so that the transitions can
	 * execute synchronously. If so return that send statement. Otherwise return
	 * null.
	 */
	private SendStatementIF match(ReceiveStatementIF receive)
			throws ExecutionException {
		ProcessIF receiver = receive.process();
		ProcessIF sender = getSource(receive);
		LocationIF location = environment.location(sender);

		if (location == null)
			return null;
		if (location instanceof SendLocationIF) {
			SendStatementIF send = ((SendLocationIF) location).statement();

			if (getDestination(send).equals(receiver)) {
				ExpressionIF receiveTagExpression = receive.tag();
				ExpressionIF sendTagExpression = send.tag();
				ValueIF sendTagValue = evaluator.evaluate(environment,
						sendTagExpression);
				ValueIF assumption = environment.getAssumption();
				int sendTag = ((IntegerNumberIF) dynamicFactory.numericValue(
						assumption, sendTagValue)).intValue();

				if (receiveTagExpression.kind() == ExpressionKind.ANY) {
					// cannot match a send with a negative tag: represents
					// collective
					if (sendTag >= 0)
						return send;
				} else {
					ValueIF receiveTagValue = evaluator.evaluate(environment,
							receiveTagExpression);
					int receiveTag = ((IntegerNumberIF) dynamicFactory
							.numericValue(assumption, receiveTagValue))
							.intValue();

					if (sendTag == receiveTag)
						return send;
				}
			}
		}
		return null;
	}

	private boolean senderTerminated(ReceiveStatementIF receive)
			throws ExecutionException {
		return environment.emptyStack(getSource(receive));
	}

}