VerificationUtility.java

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

import java.io.PrintWriter;
import java.util.Collection;
import java.util.HashSet;
import java.util.LinkedHashMap;
import java.util.Map;

import edu.udel.cis.vsl.tass.config.RunConfiguration;
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.Kripke;
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.expression.ExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.type.TypeIF;
import edu.udel.cis.vsl.tass.model.IF.variable.SharedVariableIF;
import edu.udel.cis.vsl.tass.model.IF.variable.VariableIF;
import edu.udel.cis.vsl.tass.number.IF.IntegerNumberIF;
import edu.udel.cis.vsl.tass.number.IF.RationalNumberIF;
import edu.udel.cis.vsl.tass.prove.Prove;
import edu.udel.cis.vsl.tass.prove.IF.TheoremProverIF;
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.ExecutionException;
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.LogIF;
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.IF.SymbolicUniverseIF;

public class VerificationUtility {

	public static void checkCompatibility(LibraryExecutorLoaderIF loader,
			SymbolicUniverseIF universe, DynamicFactoryIF dynamicFactory,
			ModelIF model1, ModelIF model2, LogIF log)
			throws ExecutionException, ExecutionStateException {
		RunConfiguration configuration = universe.configuration();
		ModelSequence modelSequence1 = new ModelSequence(model1);
		ModelSequence modelSequence2 = new ModelSequence(model2);
		PrintWriter debugOut = configuration.debugOut();

		SymbolicSimplifierFactoryIF simplifierFactory = Simplify
				.newSimplifierFactory(universe);
		TheoremProverIF prover = Prove.newIdealCVC3HybridProver(universe,
				configuration);
		EvaluatorIF evaluator = Semantics.newEvaluator(dynamicFactory,
				configuration.bufferBound(), log);
		StateFactoryIF stateFactory1 = States.newStateFactory(modelSequence1,
				dynamicFactory);
		StateFactoryIF stateFactory2 = States.newStateFactory(modelSequence2,
				dynamicFactory);
		StatefulEnvironmentIF e1 = States.newEnvironment(modelSequence1,
				stateFactory1, log);
		StatefulEnvironmentIF e2 = States.newEnvironment(modelSequence2,
				stateFactory2, log);
		TASSStateManagerIF manager1 = Kripke.newStateManager(loader,
				modelSequence1, dynamicFactory, stateFactory1, configuration
						.bufferBound(), log);
		TASSStateManagerIF manager2 = Kripke.newStateManager(loader,
				modelSequence2, dynamicFactory, stateFactory2, configuration
						.bufferBound(), log);
		Map<VariableIF, ValueIF> inputs = new LinkedHashMap<VariableIF, ValueIF>();
		StateIF state1, state2;
		ValueIF predicate1, predicate2;

		if (debugOut == null) {
			debugOut = new PrintWriter(System.err);
		}
		state1 = manager1.preInitialState(dynamicFactory.symbolicValue(true),
				null, true, true);
		e1.setState(state1);
		predicate1 = e1.getAssumption();
		for (SharedVariableIF inputVariable1 : model1.scope().inputVariables()) {
			SharedVariableIF inputVariable2 = inputVariable1
					.correspondingVariable();
			ValueIF initialValue;

			if (inputVariable2 == null) {
				throw new ExecutionException(inputVariable1,
						ErrorKind.FUNCTIONAL_COMPATIBILITY,
						Certainty.PROVEABLE, "No corresponding variable in "
								+ model2);
			}
			initialValue = e1
					.valueOf(dynamicFactory.sharedCell(inputVariable1));
			if (initialValue == null) {
				dynamicFactory.shutdown();
				throw new ExecutionException(inputVariable1,
						ErrorKind.FUNCTIONAL_COMPATIBILITY,
						Certainty.PROVEABLE, "Input variable of " + model1
								+ " has no initial value");
			}
			inputs.put(inputVariable2, initialValue);
		}
		state2 = manager2.preInitialState(dynamicFactory.symbolicValue(true),
				inputs, true, true);
		e2.setState(state2);
		e2.setAssumption(dynamicFactory.trueValue());
		for (VariableIF inputVariable2 : inputs.keySet()) {
			ExpressionIF assumption = ((SharedVariableIF) inputVariable2)
					.assumption();

			if (assumption != null) {
				ValueIF assumptionValue = evaluator.evaluate(e2, assumption);

				try {
					e2.addAssumption(assumptionValue);
				} catch (ExecutionProblem problem) {
					throw new ExecutionStateException(e2.locations(), problem);
				}
			}
		}
		predicate2 = e2.getAssumption();
		try {
			// TODO: check whether valid is MAYBE or NO...
			if (!dynamicFactory.isValid(predicate1, predicate2)) {
				dynamicFactory.shutdown();
				throw new ExecutionStateException(e2.locations(),
						ErrorKind.FUNCTIONAL_COMPATIBILITY, Certainty.MAYBE,
						"Inconsistent input assumptions: predicate1 does not imply predicate2:\n"
								+ predicate1 + "\n" + predicate2);
			}
			if (!dynamicFactory.isValid(predicate2, predicate1)) {
				debugOut.println("Initial states:\n");
				manager1.printStateLong(debugOut, state1);
				manager2.printStateLong(debugOut, state2);
				dynamicFactory.shutdown();

				throw new ExecutionStateException(e2.locations(),
						ErrorKind.FUNCTIONAL_COMPATIBILITY, Certainty.NONE,
						"Inconsistent input assumptions: predicate2 does not imply predicate1:\n"
								+ predicate2 + "\n" + predicate1);
			}
		} catch (DynamicException error) {
			throw new ExecutionStateException(e2.locations(), error,
					Certainty.NONE);
		}
		checkNonKeyAssumptions(model1, model2, dynamicFactory);
		prover.close();
		simplifierFactory.close();
	}

	/**
	 * Checks that non-corresponding variables in model2 do not contain
	 * assumptions which refer to corresponding variables in model2.
	 * 
	 * @throws ExecutionException
	 */
	private static void checkNonKeyAssumptions(ModelIF model1, ModelIF model2,
			DynamicFactoryIF dynamicFactory) throws ExecutionException {
		Collection<SharedVariableIF> keyVariables = new HashSet<SharedVariableIF>();
		Collection<SharedVariableIF> nonKeyVariables = new HashSet<SharedVariableIF>();

		for (SharedVariableIF variable : model1.scope().inputVariables()) {
			keyVariables.add(variable.correspondingVariable());
		}
		nonKeyVariables.addAll(model2.scope().inputVariables());
		nonKeyVariables.removeAll(keyVariables);
		for (SharedVariableIF variable : nonKeyVariables) {
			ExpressionIF assumption = variable.assumption();

			if (assumption != null) {
				Collection<VariableIF> references = assumption.freeVariables();

				for (VariableIF r : references) {
					if (keyVariables.contains(r)) {
						dynamicFactory.shutdown();
						throw new ExecutionException(variable,
								ErrorKind.FUNCTIONAL_COMPATIBILITY,
								Certainty.NONE,
								"Non-corresponding input variable assumption refers to corresponding variable "
										+ r);
					}
				}
			}
		}
	}

	public static Map<VariableIF, ValueIF> inputMap(ModelIF model,
			DynamicFactoryIF factory) {
		return inputMap(new ModelSequence(new ModelIF[] { model }), factory);
	}

	public static Map<VariableIF, ValueIF> inputMap(
			ModelSequence modelSequence, DynamicFactoryIF factory) {
		RunConfiguration configuration = factory.configuration();
		Map<String, Object> map = configuration.inputMap();
		Map<VariableIF, ValueIF> inputMap = new LinkedHashMap<VariableIF, ValueIF>();

		for (Map.Entry<String, Object> entry : map.entrySet()) {
			String name = entry.getKey();
			Object object = entry.getValue();
			VariableIF variable = null;

			for (ModelIF model : modelSequence.models()) {
				variable = model.scope().variableWithName(name);
				if (variable != null)
					break;
			}
			if (variable != null) {
				TypeIF type = variable.type();
				TypeIF.TypeKind kind = type.kind();
				ValueIF value;

				if (object instanceof Boolean) {
					value = factory.symbolicValue((Boolean) object);
					if (kind != TypeIF.TypeKind.BOOLEAN)
						throw new IllegalArgumentException(
								"Input type mismatch: " + variable + " ("
										+ type + ") = " + value + "(boolean)");
				} else if (object instanceof IntegerNumberIF) {
					value = factory.symbolicValue((IntegerNumberIF) object);
					if (kind != TypeIF.TypeKind.INTEGER)
						throw new IllegalArgumentException(
								"Input type mismatch: " + variable + " ("
										+ type + ") = " + value + "(int)");
				} else if (object instanceof RationalNumberIF) {
					value = factory.symbolicValue((RationalNumberIF) object);
					if (kind != TypeIF.TypeKind.RATIONAL)
						throw new IllegalArgumentException(
								"Input type mismatch: " + variable + " ("
										+ type + ") = " + value + "(real)");
				} else {
					throw new IllegalArgumentException(
							"Unknown type of value : " + object);
				}
				inputMap.put(variable, value);
			}
		}
		return inputMap;
	}
}