CollectiveVerifier.java

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

import java.io.FileNotFoundException;
import java.io.PrintWriter;

import edu.udel.cis.vsl.tass.config.CompareConfiguration;
import edu.udel.cis.vsl.tass.config.RunConfiguration;
import edu.udel.cis.vsl.tass.config.VerifyConfiguration;
import edu.udel.cis.vsl.tass.config.RunConfiguration.DeadlockStrategy;
import edu.udel.cis.vsl.tass.config.RunConfiguration.ReductionStrategy;
import edu.udel.cis.vsl.tass.dynamic.Dynamics;
import edu.udel.cis.vsl.tass.dynamic.IF.DynamicFactoryIF;
import edu.udel.cis.vsl.tass.kripke.Kripke;
import edu.udel.cis.vsl.tass.kripke.IF.TASSEnablerIF;
import edu.udel.cis.vsl.tass.kripke.IF.TASSStateManagerIF;
import edu.udel.cis.vsl.tass.kripke.IF.VerificationUtility;
import edu.udel.cis.vsl.tass.library.Libraries;
import edu.udel.cis.vsl.tass.log.Logs;
import edu.udel.cis.vsl.tass.log.IF.ErrorLogIF;
import edu.udel.cis.vsl.tass.log.IF.ExcessiveErrorException;
import edu.udel.cis.vsl.tass.model.IF.ModelFactoryIF;
import edu.udel.cis.vsl.tass.model.IF.ModelIF;
import edu.udel.cis.vsl.tass.model.IF.ModelSequence;
import edu.udel.cis.vsl.tass.number.Numbers;
import edu.udel.cis.vsl.tass.number.IF.NumberFactoryIF;
import edu.udel.cis.vsl.tass.predicate.Predicates;
import edu.udel.cis.vsl.tass.predicate.IF.PredicateFactoryIF;
import edu.udel.cis.vsl.tass.predicate.IF.TASSPredicateIF;
import edu.udel.cis.vsl.tass.prove.Prove;
import edu.udel.cis.vsl.tass.prove.IF.TheoremProverIF;
import edu.udel.cis.vsl.tass.search.DfsSearcher;
import edu.udel.cis.vsl.tass.semantics.Semantics;
import edu.udel.cis.vsl.tass.semantics.IF.EvaluatorIF;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionProblem;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionStateException;
import edu.udel.cis.vsl.tass.semantics.IF.LibraryExecutorLoaderIF;
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.simplify.Simplify;
import edu.udel.cis.vsl.tass.simplify.IF.SymbolicSimplifierFactoryIF;
import edu.udel.cis.vsl.tass.state.States;
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.StatefulEnvironmentIF;
import edu.udel.cis.vsl.tass.symbolic.Symbolics;
import edu.udel.cis.vsl.tass.symbolic.IF.SymbolicUniverseIF;
import edu.udel.cis.vsl.tass.transition.Transitions;
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;
import edu.udel.cis.vsl.tass.util.Reports;

public class CollectiveVerifier {

	private LibraryExecutorLoaderIF loader;

	private ModelFactoryIF modelFactory;

	private PredicateFactoryIF predicateFactory;

	private ModelSequence modelSequence;

	private RunConfiguration configuration;

	private ErrorLogIF log;

	private PrintWriter out;

	private PrintWriter searchOut;

	private StateIF initialState;

	private TASSPredicateIF deadlockPredicate, predicate;

	private NumberFactoryIF numberFactory;

	private DynamicFactoryIF dynamicFactory;

	private SymbolicUniverseIF universe;

	private SymbolicSimplifierFactoryIF simplifierFactory;

	private TheoremProverIF prover;

	private StateFactoryIF stateFactory;

	private TransitionFactoryIF transitionFactory;

	private TASSStateManagerIF stateManager;

	private DfsSearcher<StateIF, TransitionIF, TransitionSequenceIF> searcher;

	private EvaluatorIF evaluator;

	private TASSEnablerIF enabler;

	private String name;

	/**
	 * when more than one model, do you run them sequentially or concurrently?
	 */
	boolean sequential;

	/** Explore all transitions in a model (i.e., no partial order reduction)? */
	boolean full;

	public CollectiveVerifier(ModelIF model, VerifyConfiguration configuration)
			throws FileNotFoundException {
		ModelIF[] models = new ModelIF[] { model };

		this.modelFactory = model.modelFactory();
		this.predicateFactory = Predicates.newPredicateFactory();
		this.modelSequence = new ModelSequence(models);
		this.log = Logs.newErrorLog(configuration, model);
		this.configuration = configuration;
		initialize(model);
		predicate = (deadlockPredicate == null ? predicateFactory
				.newFalsePredicate() : deadlockPredicate);
		if (configuration.verbose()) {
			model.print(configuration.out());
		}
	}

	public CollectiveVerifier(ModelIF specModel, ModelIF implModel,
			CompareConfiguration configuration) throws FileNotFoundException {
		ModelIF[] models = new ModelIF[] { specModel, implModel };

		this.modelFactory = specModel.modelFactory();
		this.predicateFactory = Predicates.newPredicateFactory();
		this.modelSequence = new ModelSequence(models);
		this.log = Logs.newErrorLog(configuration, specModel, implModel);
		this.configuration = configuration;
		initialize(implModel); // only check deadlock on impl
		predicate = predicateFactory.newComparisonPredicate(modelSequence,
				dynamicFactory, stateFactory, deadlockPredicate,
				configuration.bufferBound(), log);
		if (configuration.verbose()) {
			specModel.print(configuration.out());
			implModel.print(configuration.out());
		}
	}

	// for now, only checking deadlock in specified model...
	private void initialize(ModelIF deadlockModel) {
		StatefulEnvironmentIF deadlockEnvironment;
		DeadlockStrategy deadlockStrategy = configuration.deadlockStrategy();

		log.setErrorBound(configuration.errorBound());
		this.out = configuration.out();
		this.searchOut = (configuration.verbose() ? out : null);
		this.numberFactory = Numbers.REAL_FACTORY;
		this.universe = Symbolics.newRealUniverse(configuration, numberFactory);
		this.simplifierFactory = Simplify.newSimplifierFactory(universe);
		if (configuration.simplify()) {
			this.prover = Prove.newIdealCVC3HybridProver(universe,
					configuration);
		} else {
			this.prover = Prove.newCVC3Prover(universe, configuration);
		}
		this.dynamicFactory = Dynamics.newDynamicFactory(modelFactory,
				simplifierFactory, prover, configuration);
		this.loader = Libraries.newLibraryExecutorLoader(configuration,
				dynamicFactory, log);
		this.stateFactory = States.newStateFactory(modelSequence,
				dynamicFactory);
		this.transitionFactory = Transitions.newTransitionFactory();
		this.evaluator = Semantics.newEvaluator(dynamicFactory,
				configuration.bufferBound(), log);
		this.full = configuration.reductionStrategy() == ReductionStrategy.STANDARD;
		// if option -cqmin (collective queue minimization heuristic)
		// is true, use concurrent option in urgent POR. This favors
		// procs which are behind in a collective assertion. Else
		// use sequential option. Default should be true as this usually helps.
		this.sequential = !configuration.cqmin();
		for (ModelIF model : modelSequence.models()) {
			if (name == null) {
				name = model.name();
			} else {
				name += "-" + model.name();
			}
		}
		// log.setStateManager(stateManager);
		// log.setDynamicFactory(dynamicFactory);
		deadlockEnvironment = States.newEnvironment(modelSequence,
				stateFactory, log);
		if (deadlockStrategy == DeadlockStrategy.POTENTIAL) {
			deadlockPredicate = predicateFactory.newPotentialDeadlock(
					deadlockModel, dynamicFactory, deadlockEnvironment,
					evaluator, log);
		} else if (deadlockStrategy == DeadlockStrategy.ABSOLUTE) {
			deadlockPredicate = predicateFactory.newAbsoluteDeadlock(
					deadlockModel, dynamicFactory, deadlockEnvironment,
					evaluator, log);
		} else {
			deadlockPredicate = null;
		}
		this.stateManager = Kripke.newStateManager(loader, modelSequence,
				dynamicFactory, stateFactory, configuration.bufferBound(), log,
				deadlockPredicate);
	}

	public boolean search() throws FileNotFoundException {
		if (configuration instanceof VerifyConfiguration) {
		} else {
			ModelIF spec = modelSequence.modelWithIndex(0);
			ModelIF impl = modelSequence.modelWithIndex(1);

			try {
				VerificationUtility.checkCompatibility(loader, universe,
						dynamicFactory, spec, impl, log);
			} catch (ExecutionProblem problem) {
				out.println(problem);
				out.println("TASS terminating.");
				out.flush();
				return false;
			}
		}
		return searchGeneric();
	}

	private boolean searchGeneric() throws FileNotFoundException {
		double startTime = System.currentTimeMillis(), endTime;
		boolean searchNotComplete = false;
		boolean result;

		enabler = Kripke.newEnabler(modelSequence, dynamicFactory,
				stateFactory, transitionFactory, configuration.bufferBound(),
				log, sequential, full);
		stateManager.setEnabler(enabler);
		searcher = new DfsSearcher<StateIF, TransitionIF, TransitionSequenceIF>(
				enabler, stateManager, predicate, searchOut);
		searcher.setName(name);
		if (configuration.useLoopTechnique()) {
			// cycles are normal: loops
			searcher.setReportCycleAsViolation(false);
		} else {
			// cycles represent possible non-termination
			searcher.setReportCycleAsViolation(true);
		}
		log.setSearcher(searcher);
		try {
			initialState = stateManager.initialState();
			boolean workRemains = searcher.search(initialState);

			if (workRemains && searcher.cycleFound()) {
				log.report(new ExecutionStateException(searcher.currentState()
						.locations(), ErrorKind.CYCLE, Certainty.PROVEABLE,
						"Possible non-termination: cycle found in state space."));
			}
			while (workRemains) {
				workRemains = searcher.proceedToNewState();
				if (workRemains)
					workRemains = searcher.search();
				if (workRemains && searcher.cycleFound()) {
					log.report(new ExecutionStateException(searcher
							.currentState().locations(), ErrorKind.CYCLE,
							Certainty.PROVEABLE,
							"Possible non-termination: cycle found in state space."));
				}
			}
		} catch (ExcessiveErrorException e) {
			searchNotComplete = true;
		}
		result = log.numErrors() == 0;
		if (!result) {
			if (!configuration.replay())
				log.writeModels();
			log.print();
		}
		endTime = System.currentTimeMillis();
		if (searchNotComplete) {
			out.println("Terminating search before completion.");
		} else {
			out.println("Search complete.");
		}
		out.println();
		out.println("STATS:");
		printStats(out, dynamicFactory, stateManager.numStatesSeen(),
				searcher.numStatesMatched(), stateManager.numStatesSaved(),
				stateManager.numTransitionsExecuted(),
				searcher.numTransitions());
		out.println("   time (s)            : " + (endTime - startTime)
				/ 1000.0);
		out.println();
		if (result) {
			out.println("RESULT: The specified properties hold "
					+ "on all executions.");
		} else {
			out.println("RESULT: Some properties MAY NOT hold: "
					+ "counterexample found.");
		}
		if (searchNotComplete) {
			out.println("NOTE: Search not complete.");
		}
		out.println();
		out.flush();
		// close the symbolic universe
		dynamicFactory.shutdown();
		prover.close();
		return result;
	}

	private static void printStats(PrintWriter out,
			DynamicFactoryIF dynamicFactory, long numStatesSeen,
			long numStatesMatched, long numStatesSaved,
			long numTransitionsExecuted, long numTransitionsStack) {
		long numValues = dynamicFactory.numValues();
		long numQueries = dynamicFactory.numQueries();
		long numMessages = dynamicFactory.numMessages();
		long numProverValidCalls = dynamicFactory.numProverValidCalls();
		long heapSize = Runtime.getRuntime().totalMemory();

		long[] data = new long[] { numStatesSeen, numStatesMatched,
				numStatesSaved, numTransitionsExecuted, numTransitionsStack,
				numValues, numQueries, numMessages, numProverValidCalls,
				heapSize };
		int width = Reports.maxWidth(data);

		out.print("   statesSeen          : ");
		Reports.printInt(out, width, numStatesSeen);
		out.println();

		out.print("   statesMatched       : ");
		Reports.printInt(out, width, numStatesMatched);
		out.println();

		out.print("   statesSaved         : ");
		Reports.printInt(out, width, numStatesSaved);
		out.println();

		out.print("   transitionsExecuted : ");
		Reports.printInt(out, width, numTransitionsExecuted);
		out.println();

		out.print("   transitionsStacked  : ");
		Reports.printInt(out, width, numTransitionsStack);
		out.println();

		out.print("   valuesSaved         : ");
		Reports.printInt(out, width, numValues);
		out.println();

		out.print("   messagesSaved       : ");
		Reports.printInt(out, width, numMessages);
		out.println();

		out.print("   queries             : ");
		Reports.printInt(out, width, numQueries);
		out.println();

		out.print("   proverValidCalls    : ");
		Reports.printInt(out, width, numProverValidCalls);
		out.println();

		out.print("   memory              : ");
		Reports.printInt(out, width, heapSize);
		out.println();
	}

}