Options.java

package edu.udel.cis.vsl.tass.config;

import java.util.Collection;
import java.util.LinkedHashMap;
import java.util.Map;

import edu.udel.cis.vsl.tass.config.Option.OptionKind;
import edu.udel.cis.vsl.tass.config.Option.OptionType;
import edu.udel.cis.vsl.tass.config.RunConfiguration.DeadlockStrategy;
import edu.udel.cis.vsl.tass.config.RunConfiguration.Frontend;
import edu.udel.cis.vsl.tass.config.RunConfiguration.ReductionStrategy;

public class Options {

	private static CompareConfiguration emptyCompareConfig = new CompareConfiguration();
	private static VerifyConfiguration emptyVerifyConfig = new VerifyConfiguration();
	private static Map<String, Option> optionMap;

	static {
		buildOptionMap();
	}

	private static void buildOptionMap() {
		optionMap = new LinkedHashMap<String, Option>();
		addOptionBufferBound();
		addOptionCollectiveAssertions();
		addOptionCollectiveQueueMinimization();
		addOptionCycles();
		addOptionDeadlock();
		addOptionDebug();
		addOptionDrawGraph();
		addOptionErrorBound();
		addOptionFrontend();
		addOptionLoop();
		addOptionNumProcs();
		addOptionNumProcs1();
		addOptionNumProcs2();
		addOptionReduce();
		addOptionShowModel();
		addOptionShowProverQueries();
		addOptionShowQueries();
		addOptionShowSavedStates();
		addOptionShowSimplifications();
		addOptionShowStates();
		addOptionShowTransitions();
		addOptionSimplify();
		addOptionVerbose();
	}

	private static void add(Option option) {
		String defaultValueString;

		if (option.appliesToVerify()) {
			defaultValueString = option.get(emptyVerifyConfig).toString();
		} else {
			defaultValueString = option.get(emptyCompareConfig).toString();
		}
		option.setDefaultValue(defaultValueString);
		optionMap.put(option.name(), option);
	}

	private static void addOptionBufferBound() {
		add(new Option("buffer", OptionKind.RUN, OptionType.INTEGER,
				"upper bound on total number of buffered messages") {

			@Override
			public Object get(RunConfiguration configuration) {
				return configuration.bufferBound();
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				int bound = (Integer) value;

				if (bound < 0)
					throw new IllegalArgumentException(
							"Expected nonnegative value");
				configuration.setBufferBound(bound);
			}
		});
	}

	private static void addOptionCollectiveAssertions() {
		add(new Option("ca", OptionKind.RUN, OptionType.BOOLEAN,
				"check collective assertions") {

			@Override
			public Object get(RunConfiguration configuration) {
				return configuration.useCollectiveAssertions();
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				configuration.setUseCollectiveAssertions((Boolean) value);
			}
		});
	}

	private static void addOptionCollectiveQueueMinimization() {
		add(new Option("cqmin", OptionKind.RUN, OptionType.BOOLEAN,
				"use collective queue minimization heuristic") {

			@Override
			public Object get(RunConfiguration configuration) {
				return configuration.cqmin();
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				configuration.setCqmin((Boolean) value);
			}

		});
	}

	private static void addOptionCycles() {
		add(new Option("detectCycles", OptionKind.RUN, OptionType.BOOLEAN,
				"report cycles in state space as errors") {

			@Override
			public Object get(RunConfiguration configuration) {
				return configuration.detectCycles();
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				configuration.setDetectCycles((Boolean) value);
			}
		});
	}

	private static void addOptionDeadlock() {
		add(new Option("deadlock", OptionKind.RUN, OptionType.STRING,
				"deadlock detection: ignore, absolute, or potential") {

			@Override
			public Object get(RunConfiguration configuration) {
				switch (configuration.deadlockStrategy()) {
				case ABSOLUTE:
					return "absolute";
				case IGNORE:
					return "ignore";
				case POTENTIAL:
					return "potential";
				default:
					throw new RuntimeException("Internal Error.");
				}
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				if ("absolute".equals(value))
					configuration
							.setDeadlockStrategy(DeadlockStrategy.ABSOLUTE);
				else if ("ignore".equals(value))
					configuration.setDeadlockStrategy(DeadlockStrategy.IGNORE);
				else if ("potential".equals(value))
					configuration
							.setDeadlockStrategy(DeadlockStrategy.POTENTIAL);
				else
					throw new IllegalArgumentException(
							"Expected ignore, absolute, or potential");
			}
		});
	}

	private static void addOptionDebug() {
		add(new Option("debug", OptionKind.RUN, OptionType.BOOLEAN,
				"print very detailed output") {

			@Override
			public Object get(RunConfiguration configuration) {
				return configuration.debugOut() != null;
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				if ((Boolean) value)
					configuration.setDebugOut(configuration.out());
				else
					configuration.setDebugOut(null);
			}
		});
	}

	private static void addOptionDrawGraph() {
		add(new Option("drawgraph", OptionKind.RUN, OptionType.BOOLEAN,
				"draw graph of reachable state space") {

			@Override
			public Object get(RunConfiguration configuration) {
				return configuration.drawGraph();
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				configuration.setDrawGraph((Boolean) value);
			}
		});
	}

	private static void addOptionErrorBound() {
		add(new Option("errorBound", OptionKind.RUN, OptionType.INTEGER,
				"upper bound on number of errors found before quitting") {

			@Override
			public Object get(RunConfiguration configuration) {
				return configuration.errorBound();
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				int bound = (Integer) value;

				if (bound < 0)
					throw new IllegalArgumentException(
							"Expected nonnegative value");
				configuration.setErrorBound(bound);
			}
		});
	}
	
	private static void addOptionFrontend() {
		add(new Option("frontend", OptionKind.RUN, OptionType.STRING, "frontend to use: antlr or clang") {
			@Override
			public Object get(RunConfiguration configuration) {
				switch (configuration.getFrontend()) {
				case ANTLR:
					return "antlr";
				case CLANG:
					return "clang";
				default:
					throw new RuntimeException("Internal Error.");
				}
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				if ("antlr".equals(value))
					configuration
							.setFrontend(Frontend.ANTLR);
				else if ("clang".equals(value))
					configuration.setFrontend(Frontend.CLANG);
				else
					throw new IllegalArgumentException(
							"Expected antlr or clang");
			}
		});		
	}

	private static void addOptionLoop() {
		add(new Option("loop", OptionKind.RUN, OptionType.BOOLEAN,
				"use collective loop invariant technique") {

			@Override
			public Object get(RunConfiguration configuration) {
				return configuration.useLoopTechnique();
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				configuration.setLoopTechnique((Boolean) value);
			}
		});
	}

	private static void addOptionNumProcs() {
		add(new Option("np", OptionKind.VERIFY, OptionType.INTEGER,
				"number of processes in verify run") {

			@Override
			public Object get(RunConfiguration configuration) {
				return ((VerifyConfiguration) configuration).numProcs();
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				int numProcs = (Integer) value;

				if (numProcs <= 0)
					throw new IllegalArgumentException(
							"Expected positive integer");
				((VerifyConfiguration) configuration).setNumProcs(numProcs);
			}
		});
	}

	private static void addOptionNumProcs1() {
		add(new Option("np1", OptionKind.COMPARE, OptionType.INTEGER,
				"number of processes in specification (compare mode only)") {

			@Override
			public Object get(RunConfiguration configuration) {
				return ((CompareConfiguration) configuration).specNumProcs();
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				int numProcs = (Integer) value;

				if (numProcs <= 0)
					throw new IllegalArgumentException(
							"Expected positive integer");
				((CompareConfiguration) configuration)
						.setSpecNumProcs(numProcs);
			}
		});
	}

	private static void addOptionNumProcs2() {
		add(new Option("np2", OptionKind.COMPARE, OptionType.INTEGER,
				"number of processes in implementation (compare mode only)") {

			@Override
			public Object get(RunConfiguration configuration) {
				return ((CompareConfiguration) configuration).implNumProcs();
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				int numProcs = (Integer) value;

				if (numProcs <= 0)
					throw new IllegalArgumentException(
							"Expected positive integer");
				((CompareConfiguration) configuration)
						.setImplNumProcs(numProcs);
			}
		});
	}

	private static void addOptionReduce() {
		add(new Option("reduce", OptionKind.RUN, OptionType.STRING,
				"partial order reduction strategy: std or urgent") {

			@Override
			public Object get(RunConfiguration configuration) {
				switch (configuration.reductionStrategy()) {
				case STANDARD:
					return "standard";
				case URGENT:
					return "urgent";
				default:
					throw new RuntimeException("Internal Error.");
				}
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				if ("std".equals(value))
					configuration
							.setReductionStrategy(ReductionStrategy.STANDARD);
				else if ("urgent".equals(value))
					configuration
							.setReductionStrategy(ReductionStrategy.URGENT);
				else
					throw new IllegalArgumentException("Expected std or urgent");
			}
		});
	}

	private static void addOptionShowModel() {
		add(new Option("showModel", OptionKind.RUN, OptionType.BOOLEAN,
				"print the model(s) extracted from source") {

			@Override
			public Object get(RunConfiguration configuration) {
				return configuration.showModel();
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				configuration.setShowModel((Boolean) value);
			}
		});
	}

	private static void addOptionShowProverQueries() {
		add(new Option("showProverQueries", OptionKind.RUN, OptionType.BOOLEAN,
				"show queries passed to theorem prover") {
			@Override
			public Object get(RunConfiguration configuration) {
				return configuration.showProverQueries();
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				configuration.setShowProverQueries((Boolean) value);
			}
		});
	}

	private static void addOptionShowQueries() {
		add(new Option("showQueries", OptionKind.RUN, OptionType.BOOLEAN,
				"show all queries") {

			@Override
			public Object get(RunConfiguration configuration) {
				return configuration.showQueries();
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				configuration.setShowQueries((Boolean) value);
			}
		});
	}

	private static void addOptionShowSavedStates() {
		add(new Option("showSavedStates", OptionKind.RUN, OptionType.BOOLEAN,
				"show saved states only") {

			@Override
			public Object get(RunConfiguration configuration) {
				return configuration.showSavedStates();
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				configuration.setShowSavedStates((Boolean) value);
			}
		});
	}

	private static void addOptionShowSimplifications() {
		add(new Option("showSimplifications", OptionKind.RUN,
				OptionType.BOOLEAN, "show results of symbolic simplifications") {

			@Override
			public Object get(RunConfiguration configuration) {
				return configuration.showSimplifications();
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				configuration.setShowSimplifications((Boolean) value);
			}
		});
	}

	private static void addOptionShowStates() {
		add(new Option("showStates", OptionKind.RUN, OptionType.BOOLEAN,
				"show all states") {

			@Override
			public Object get(RunConfiguration configuration) {
				return configuration.showStates();
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				configuration.setShowStates((Boolean) value);
			}
		});
	}

	private static void addOptionShowTransitions() {
		add(new Option("showTransitions", OptionKind.RUN, OptionType.BOOLEAN,
				"show transitions") {

			@Override
			public Object get(RunConfiguration configuration) {
				return configuration.showTransitions();
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				configuration.setShowTransitions((Boolean) value);
			}
		});
	}

	private static void addOptionSimplify() {
		add(new Option("simplify", OptionKind.RUN, OptionType.BOOLEAN,
				"simplify saved states and predicates") {

			@Override
			public Object get(RunConfiguration configuration) {
				return configuration.simplify();
			}

			@Override
			public void set(RunConfiguration configuration, Object value) {
				configuration.setSimplify((Boolean) value);
			}
		});
	}

	private static void addOptionVerbose() {
		add(new Option("verbose", OptionKind.RUN, OptionType.BOOLEAN,
				"verbose output") {

			@Override
			public Object get(RunConfiguration configuration) {
				return configuration.verbose();
			}

			public void set(RunConfiguration configuration, Object value) {
				configuration.setVerbose((Boolean) value);
			}
		});
	}

	public static Option getOption(String name) {
		return optionMap.get(name);
	}

	public static Collection<Option> options() {
		return optionMap.values();
	}

	public static boolean isApplicable(RunConfiguration configuration,
			Option option) {
		return (configuration instanceof VerifyConfiguration && option
				.appliesToVerify())
				|| (configuration instanceof CompareConfiguration && option
						.appliesToCompare());
	}

}