CIVLConfiguration.java

package dev.civl.mc.config.IF;

import java.io.PrintStream;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashMap;
import java.util.List;
import java.util.Map;

import dev.civl.gmc.GMCSection;
import dev.civl.gmc.Option.OptionType;
import dev.civl.mc.config.IF.CIVLConstants.DeadlockKind;
import dev.civl.mc.config.IF.CIVLConstants.ErrorStateEquivalence;
import dev.civl.mc.config.IF.CIVLConstants.MPIModelKind;
import dev.civl.mc.model.IF.CIVLInternalException;
import dev.civl.mc.model.IF.CIVLProperty;
import dev.civl.mc.model.IF.CIVLSource;
import dev.civl.mc.model.IF.ModelConfiguration;

/**
 * A CIVLConfiguration object encompasses all the parameters used to configure
 * CIVL for the execution of one or more tasks. It provides methods to get and
 * set these parameters. The types of the parameters are all simple Java types,
 * such as boolean or int, so this class does not use any other CIVL classes
 * 
 * @author siegel
 * 
 */
public class CIVLConfiguration {

	/**
	 * What kind of deadlocks should CIVL search for?
	 */
	private DeadlockKind checkDeadlockKind = DeadlockKind.ABSOLUTE;
	/*
	 * private boolean checkDivisionByZero = true; private boolean checkMemoryLeak =
	 * true; private boolean checkAssertionViolation = true; private boolean
	 * checkCommErr = true; private boolean checkConstWrite = true; private boolean
	 * checkInputWrite = true; private boolean checkInvalidCast = true; private
	 * boolean checkMallocErr = true; private boolean checkMpiErr = true; private
	 * boolean checkOutOfBounds = true; private boolean checkOutputRead = true;
	 * private boolean checkPointerErr = true; private boolean checkUndefVal = true;
	 * private boolean checkUnionErr = true; private boolean checkProcLeak = true;
	 * private boolean checkSeqErr = true; private boolean checkMemManageErr = true;
	 * private boolean checkTermination = true;
	 */

	Map<CIVLProperty, Boolean> toggleableCivlProps;

	/**
	 * Should CIVL run in "debug" mode, printing lots and lots of output?
	 */
	private boolean debug = false;

	/**
	 * Should CIVL actually print the stuff that the program it is analyzing sends
	 * to <code>stdout</code>? Could lead to a lot of printing, esp. when searching
	 * a state space, which may entail executing the same statement over and over
	 * again.
	 */
	private boolean enablePrintf = true;

	/**
	 * Should CIVL save some states as it searches, as opposed to doing a
	 * "stateless" search? Even if this is true, CIVL will not necessarily save
	 * every state, only important ones that have a chance of being encountered
	 * again in the search.
	 */
	private boolean saveStates = true;

	/**
	 * Should CIVL show the Abstract Syntax Tree (AST) that it produces from parsing
	 * the source code (before any transformations)?
	 */
	private boolean showAST = false;

	/**
	 * Should CIVL show the ample set when there are more than one processes in the
	 * ample set?
	 */
	private boolean showAmpleSet = false;

	/**
	 * Should CIVL show the ample set with the state when there are more than one
	 * processes in the ample set?
	 */
	private boolean showAmpleSetWtStates = false;

	/**
	 * Should CIVL show the CIVL model of the program?
	 */
	private boolean showModel = false;

	/**
	 * Should CIVL show states that are saved?
	 */
	private boolean showSavedStates = false;

	/**
	 * Should CIVL show all states, including saved states and intermediate states?
	 */
	private boolean showStates = false;

	/**
	 * Should CIVL show all transitions?
	 */
	private boolean showTransitions = false;

	/**
	 * Should CIVL show unreachable code?
	 */
	private boolean showUnreach = false;

	/**
	 * Should CIVL simplify states using the path condition?
	 */
	private boolean simplify = true;

	/**
	 * Is printf stateless?
	 */
	private boolean statelessPrintf = true;

	/**
	 * verbose mode?
	 */
	private boolean verbose = false;

	/**
	 * Should CIVL show the program after all applicable transformations?
	 */
	private boolean showProgram = false;

	/**
	 * Disable OpenMP simplifier?
	 */
	private boolean ompNoSimplify = false;

	/**
	 * Only relies on the OpenMP simplifier?
	 */
	private boolean ompOnlySimplifier = false;

	/**
	 * The output stream
	 */
	private PrintStream out;

	/**
	 * The print stream for errors.
	 */
	private PrintStream err;

	/**
	 * Should CIVL show the path condition of each state?
	 */
	private String showPathConditon = "NONE";

	/**
	 * Should CIVL delete terminated processes and renumber all processes?
	 */
	private boolean collectProcesses = true;

	/**
	 * Should CIVL delete invalid dyscopes and renumber all dyscopes?
	 */
	private boolean collectScopes = true;

	private boolean collectSymbolicNames = true;

	/**
	 * Should CIVL collect heap objects?
	 */
	private boolean collectHeaps = true;

	/**
	 * Is this run for CIVL web interface?
	 */
	private boolean web = false;

	/**
	 * Should CIVL show the preprocessing result?
	 */
	private boolean showPreproc = false;

	/**
	 * Should CIVL show the list of input variables of the model?
	 */
	private boolean showInputVars = false;

	/**
	 * Should CIVL show the time usage for each translation phase?
	 */
	private boolean showTime = false;

	/**
	 * Should CIVL show the impact/reachable memory units of processes at each
	 * state?
	 */
	private boolean showMemoryUnits = false;

	/**
	 * Should CIVL ignore the output after executing the command line.
	 */
	private boolean quiet = false;

	/**
	 * The upper bound of integer.
	 */
	private int intBit = 32;

	/**
	 * apply int operation transformer? Default false.
	 */
	private boolean intOperationTransiformer = false;

	/**
	 * Should CIVL tell SARL to use probabilistic techniques for verifying
	 * identities ?
	 */
	private boolean prob = false;

	/**
	 * The maximal number of processes allowed in a state. -1 means infinitely many
	 * processes are allowed.
	 */
	private int procBound = -1;

	private int maxProcs = 100;

	/**
	 * The loop decomposition strategy for OpenMP transformer, round robin by
	 * default.
	 */
	private int ompLoopDecomp = ModelConfiguration.DECOMP_ROUND_ROBIN;

	/**
	 * The error state equivalence semantics to suppress logging of redundant error
	 * states. All equivalences use the "kind" of error, but they vary in the
	 * portions of the state considered. LOC by default.
	 */
	private ErrorStateEquivalence errorStateEquiv = ErrorStateEquivalence.LOC;

	/**
	 * Direct symbolic execution based on file designating branches to direct and
	 * how to subset their outcomes.
	 */
	private String directSymEx = null;

	/**
	 * Is the current command replay? Not replay by default.
	 */
	private boolean isReplay = false;

	private boolean absAnalysis = false;

	private Map<String, Object> inputVariables;

	private boolean collectOutputs = false;

	/**
	 * If CIVL enables "MPI CONTRACT" mode
	 */
	private String mpiContractFunction = null;

	/**
	 * The MPI implementation model, by default is blocking:
	 */
	private MPIModelKind mpiModel = MPIModelKind.BLOCKING;

	private int timeout = -1;

	private boolean unpreproc = false;

	private boolean checkExpressionError = true;

	private boolean isInSubprogram = false;

	/**
	 * set to true iff loop invariant option is enabled.
	 */
	private boolean loopInvariantEnabled = false;

	private boolean convergeWithMemEq = false;

	/**
	 * whether updater thread is in used for printing update info periodically
	 */
	private boolean runtimeUpdate;

	/**
	 * Upper bound on the number of preemptions allowed in an execution, if doing a
	 * preemptive-bounded search. If it is -1 for a normal (not preemption-bounded)
	 * search.
	 */
	private int preemptionBound;

	/**
	 * If true, $local_start() and $local_end will be translated as no-op
	 */
	private boolean disableLocalBlock;

	/**
	 * If this is true, and termination is being checked, then a cycle in which some
	 * process remains enabled at each state will not be considered a violation of
	 * non-termination (as it is not considered to represent a real execution).
	 */
	private boolean fair;

	/**
	 * If this is true then DPOR algorithm is used. Note that collectProcesses
	 * becomes false when this is set to true.
	 */
	private boolean dpor;

	/**
	 * Constructs a new CIVL configuration object from the command line
	 * configuration.
	 * 
	 * @param config The command line configuration.
	 */
	public CIVLConfiguration(GMCSection config) {
		this.toggleableCivlProps = new HashMap<CIVLProperty, Boolean>();
		// Fill out CIVLProperty config info
		for (CIVLProperty prop : CIVLProperty.getAllConfigurableProperties()) {
			if (prop.getOption().type() == OptionType.BOOLEAN) {
				this.toggleableCivlProps.put(prop, config.isTrue(prop.getOption()));
			} else if (prop == CIVLProperty.DEADLOCK) {
				String deadlockString = (String) config.getValue(CIVLProperty.DEADLOCK.getOption());
				if (deadlockString != null) {
					switch (deadlockString) {
					case "absolute":
						this.checkDeadlockKind = DeadlockKind.ABSOLUTE;
						break;
					case "potential":
						this.checkDeadlockKind = DeadlockKind.POTENTIAL;
						break;
					case "none":
						this.checkDeadlockKind = DeadlockKind.NONE;
						break;
					default:
						throw new CIVLInternalException("invalid deadlock kind " + deadlockString, (CIVLSource) null);
					}
				}
			} else {
				throw new CIVLInternalException(
						"Configurable CIVLProperty declared but not recorded in CIVLConfiguration", (CIVLSource) null);
			}
		}

		String ompLoopDecompString = (String) config.getValue(CIVLConstants.ompLoopDecompO);
		String errorStateEquivString = (String) config.getValue(CIVLConstants.errorStateEquivO);

		this.setMpiModel(MPIModelKind.select((String) config.getValueOrDefault(CIVLConstants.mpiModelO)));
		if (ompLoopDecompString != null) {
			switch (ompLoopDecompString) {
			case "ALL":
				this.setOmpLoopDecomp(ModelConfiguration.DECOMP_ALL);
				break;
			case "ROUND_ROBIN":
				this.setOmpLoopDecomp(ModelConfiguration.DECOMP_ROUND_ROBIN);
				break;
			case "RANDOM":
				this.setOmpLoopDecomp(ModelConfiguration.DECOMP_RANDOM);
				break;
			default:
				throw new CIVLInternalException("invalid OpenMP loop decomposition strategy " + ompLoopDecompString,
						(CIVLSource) null);
			}
		}
		if (errorStateEquivString != null)
			switch (errorStateEquivString) {
			case "LOC":
				this.errorStateEquiv = ErrorStateEquivalence.LOC;
				break;
			case "CALLSTACK":
				this.errorStateEquiv = ErrorStateEquivalence.CALLSTACK;
				break;
			case "FULL":
				this.errorStateEquiv = ErrorStateEquivalence.FULL;
				break;
			default:
				throw new CIVLInternalException("invalid error state equivalence" + errorStateEquivString,
						(CIVLSource) null);
			}
		this.intOperationTransiformer = config.isTrue(CIVLConstants.intOperationTransformer);
		this.setShowMemoryUnits(config.isTrue(CIVLConstants.showMemoryUnitsO));
		this.debug = config.isTrue(CIVLConstants.debugO);
		this.enablePrintf = config.isTrue(CIVLConstants.enablePrintfO);
		this.saveStates = config.isTrue(CIVLConstants.saveStatesO);
		this.showAmpleSet = config.isTrue(CIVLConstants.showAmpleSetO);
		this.showAmpleSetWtStates = config.isTrue(CIVLConstants.showAmpleSetWtStatesO);
		this.showSavedStates = config.isTrue(CIVLConstants.showSavedStatesO);
		this.showStates = config.isTrue(CIVLConstants.showStatesO);
		this.showTransitions = config.isTrue(CIVLConstants.showTransitionsO);
		this.setShowUnreach(config.isTrue(CIVLConstants.showUnreachedCodeO));
		this.setAbsAnalysis(config.isTrue(CIVLConstants.analyzeAbsO));
		this.simplify = config.isTrue(CIVLConstants.simplifyO);
		this.statelessPrintf = config.isTrue(CIVLConstants.statelessPrintfO);
		this.verbose = config.isTrue(CIVLConstants.verboseO);
		this.setShowProgram(config.isTrue(CIVLConstants.showProgramO));
		this.showPathConditon = (String) config.getValue(CIVLConstants.showPathConditionO);
		if (this.showPathConditon == null)
			showPathConditon = "NONE";
		this.ompNoSimplify = config.isTrue(CIVLConstants.ompNoSimplifyO);
		this.ompOnlySimplifier = config.isTrue(CIVLConstants.ompOnlySimplifierO);
		this.collectProcesses = config.isTrue(CIVLConstants.collectProcessesO);
		this.collectScopes = config.isTrue(CIVLConstants.collectScopesO);
		this.setCollectHeaps(config.isTrue(CIVLConstants.collectHeapsO));
		this.web = config.isTrue(CIVLConstants.webO);
		this.setShowPreproc(config.isTrue(CIVLConstants.preprocO));
		this.setShowAST(config.isTrue(CIVLConstants.astO));
		this.setShowModel(config.isTrue(CIVLConstants.showModelO));
		this.showInputVars = config.isTrue(CIVLConstants.showInputVarsO);
		this.showTime = config.isTrue(CIVLConstants.showTimeO);
		this.procBound = (Integer) config.getValueOrDefault(CIVLConstants.procBoundO);
		this.intBit = (Integer) config.getValueOrDefault(CIVLConstants.intBit);
		this.setInputVariables(config.getMapValue(CIVLConstants.inputO));
		this.collectOutputs = config.isTrue(CIVLConstants.collectOutputO);
		this.maxProcs = (Integer) config.getValueOrDefault(CIVLConstants.maxProcsO);
		this.setMpiContractFunction((String) config.getValueOrDefault(CIVLConstants.mpiContractO));
		if (this.isEnableMpiContract())
			this.intOperationTransiformer = false;
		this.loopInvariantEnabled = config.isTrue(CIVLConstants.loopO);
		if (this.loopInvariantEnabled) {
			// Loop invariant transformation has cycles
			this.setToggleableProperty(CIVLProperty.TERMINATION, false);
		}
		this.convergeWithMemEq = config.isTrue(CIVLConstants.memEqO);
		this.collectSymbolicNames = config.isTrue(CIVLConstants.collectSymbolicConstantsO) || loopInvariantEnabled;
		this.setTimeout((int) config.getValueOrDefault(CIVLConstants.timeoutO));
		this.quiet = config.isTrue(CIVLConstants.quietO);
		this.prob = config.isTrue(CIVLConstants.probO);
		this.directSymEx = (String) config.getValue(CIVLConstants.direct0);
		this.runtimeUpdate = config.isTrue(CIVLConstants.runtimeUpdateO);
		this.preemptionBound = (Integer) config.getValueOrDefault(CIVLConstants.preemptionBoundO);
		this.disableLocalBlock = config.isTrue(CIVLConstants.disableLocalBlockO);
		this.fair = config.isTrue(CIVLConstants.fairO);
		this.dpor = config.isTrue(CIVLConstants.dporO);
		if (dpor) {
			this.collectProcesses = false;
			this.collectHeaps = false;
		}
	}

	public CIVLConfiguration(CIVLConfiguration config) {
		this.checkDeadlockKind = config.checkDeadlockKind;
		this.toggleableCivlProps = new HashMap<CIVLProperty, Boolean>(config.toggleableCivlProps);
		this.absAnalysis = config.absAnalysis;
		this.collectHeaps = config.collectHeaps;
		this.collectOutputs = config.collectOutputs;
		this.collectProcesses = config.collectProcesses;
		this.collectScopes = config.collectScopes;
		this.collectSymbolicNames = config.collectSymbolicNames;
		this.debug = config.debug;
		this.err = config.err;
		this.enablePrintf = config.enablePrintf;
		this.errorStateEquiv = config.errorStateEquiv;
		this.isReplay = config.isReplay;
		this.mpiContractFunction = config.mpiContractFunction;
		this.ompLoopDecomp = config.ompLoopDecomp;
		this.loopInvariantEnabled = config.loopInvariantEnabled;
		this.convergeWithMemEq = config.convergeWithMemEq;
		this.ompNoSimplify = config.ompNoSimplify;
		this.ompOnlySimplifier = config.ompOnlySimplifier;
		this.out = config.out;
		this.procBound = config.procBound;
		this.prob = config.prob;
		this.quiet = config.quiet;
		this.saveStates = config.saveStates;
		this.showAmpleSet = config.showAmpleSet;
		this.showAmpleSetWtStates = config.showAmpleSetWtStates;
		this.showAST = config.showAST;
		this.showInputVars = config.showInputVars;
		this.showMemoryUnits = config.showMemoryUnits;
		this.showPathConditon = config.showPathConditon;
		this.showPreproc = config.showPreproc;
		this.showProgram = config.showProgram;
		this.showSavedStates = config.showSavedStates;
		this.showStates = config.showStates;
		this.showTime = config.showTime;
		this.showTransitions = config.showTransitions;
		this.simplify = config.simplify;
		this.timeout = config.timeout;
		this.unpreproc = config.unpreproc;
		this.verbose = config.verbose;
		this.web = config.web;
		this.directSymEx = config.directSymEx;
		this.intBit = config.intBit;
		this.maxProcs = config.maxProcs;
		this.intOperationTransiformer = config.intOperationTransiformer;
		this.runtimeUpdate = config.runtimeUpdate;
		this.disableLocalBlock = config.disableLocalBlock;
		this.fair = config.fair;
		this.dpor = config.dpor;
	}

	public CIVLConfiguration() {
	}

	/**
	 * @return returns the kind of deadlocks we are checking for
	 */
	public DeadlockKind checkDeadlockKind() {
		return checkDeadlockKind;
	}

	/**
	 * Sets the kind of deadlocks we want to check for
	 * 
	 * @param checkDeadlockKind The new kind of deadlock we want to check for
	 */
	public void setCheckDeadlockKind(DeadlockKind checkDeadlockKind) {
		this.checkDeadlockKind = checkDeadlockKind;
	}

	/**
	 * Determines whether a CIVLProperty is toggleable. A CIVLProperty is toggleable
	 * if it is controlled by a boolean command line option.
	 * 
	 * @param prop The CIVLProperty that we want to check is toggleable
	 * @return whether prop is toggleable
	 */
	public boolean isToggleableProperty(CIVLProperty prop) {
		return toggleableCivlProps.containsKey(prop);
	}

	/**
	 * Determines if a toggleable property is toggled, i.e. is turned on.
	 * 
	 * @param prop The property we want to query. The property must be toggleable.
	 *             Otherwise it is an error.
	 * @return returns whether prop is toggled.
	 */
	public boolean isPropertyToggled(CIVLProperty prop) {
		Boolean b = this.toggleableCivlProps.get(prop);
		assert (b != null);
		return b.booleanValue();
	}

	/**
	 * Sets a CIVLProperty to be toggleable and to be either turned on or off
	 * 
	 * @param prop  The CIVLProperty we want to control
	 * @param value The value of the CIVLProperty
	 */
	public void setToggleableProperty(CIVLProperty prop, boolean value) {
		this.toggleableCivlProps.put(prop, value);
	}

	private String whitespace(int n) {
		assert n >= 0;
		char[] ws = new char[n];
		Arrays.fill(ws, ' ');
		return new String(ws);
	}

	/**
	 * Generates a summary of all CIVLProperty's that are enabled
	 * 
	 * @return summary of enabled CIVLProperty's
	 */
	public String getCheckedPropertiesSummary() {
		String summary = "";
		String yes = " + ";
		String no = "   ";

		List<CIVLProperty> unconfigProps = CIVLProperty.getAllUnconfigurableProperties();
		List<CIVLProperty> configProps = CIVLProperty.getAllConfigurableProperties();
		int numProps = unconfigProps.size() + configProps.size();
		List<CIVLProperty> props = new ArrayList<CIVLProperty>(numProps);

		props.addAll(unconfigProps);
		props.addAll(configProps);

		int numCols = 2;
		int colWidth = 35;
		int currCol = 0;

		for (CIVLProperty prop : props) {
			String summTitle = getSummaryTitle(prop);
			boolean checked = true;

			if (isToggleableProperty(prop)) {
				checked = isPropertyToggled(prop);
			} else if (prop == CIVLProperty.DEADLOCK) {
				// Print deadlock property
				switch (checkDeadlockKind) {
				case ABSOLUTE:
					summTitle = "Absolute " + summTitle.toLowerCase();
					break;
				case POTENTIAL:
					summTitle = "Potential " + summTitle.toLowerCase();
					break;
				case NONE:
					checked = false;
					break;
				}
			}
			summary += (checked ? yes : no) + summTitle;

			if (currCol < numCols - 1) {
				summary += whitespace(colWidth - summTitle.length());
				currCol++;
			} else {
				summary += "\n";
				currCol = 0;
			}
		}

		if (currCol > 0) {
			summary += "\n";
		}

		return summary;
	}

	private String getSummaryTitle(CIVLProperty prop) {
		String title = prop.getPropertyTitle();
		return title.substring(0, 1).toUpperCase() + title.substring(1);
	}

	public void setOut(PrintStream out) {
		this.out = out;
	}

	public void setErr(PrintStream err) {
		this.err = err;
	}

	public void setDebug(boolean debug) {
		this.debug = debug;
	}

	public void setEnablePrintf(boolean enablePrintf) {
		this.enablePrintf = enablePrintf;
	}

	public void setSaveStates(boolean saveStates) {
		this.saveStates = saveStates;
	}

	public void setShowAmpleSet(boolean showAmpleSet) {
		this.showAmpleSet = showAmpleSet;
	}

	public void setShowAmpleSetWtStates(boolean showAmpleSetWtStates) {
		this.showAmpleSetWtStates = showAmpleSetWtStates;
	}

	public void setShowSavedStates(boolean showSavedStates) {
		this.showSavedStates = showSavedStates;
	}

	public void setShowStates(boolean showStates) {
		this.showStates = showStates;
	}

	public void setShowTransitions(boolean showTransitions) {
		this.showTransitions = showTransitions;
	}

	public void setSimplify(boolean simplify) {
		this.simplify = simplify;
	}

	public void setStatelessPrintf(boolean statelessPrintf) {
		this.statelessPrintf = statelessPrintf;
	}

	public void setVerbose(boolean verbose) {
		this.verbose = verbose;
	}

	public boolean debug() {
		return debug;
	}

	public boolean verbose() {
		return verbose;
	}

	public boolean debugOrVerbose() {
		return debug || verbose;
	}

	public boolean enablePrintf() {
		return this.enablePrintf;
	}

	public boolean saveStates() {
		return this.saveStates;
	}

	public boolean showAmpleSet() {
		return this.showAmpleSet;
	}

	public boolean showAmpleSetWtStates() {
		return this.showAmpleSetWtStates;
	}

	public boolean showSavedStates() {
		return this.showSavedStates;
	}

	public boolean showStates() {
		return this.showStates;
	}

	public boolean showTransitions() {
		return this.showTransitions;
	}

	public boolean simplify() {
		return this.simplify;
	}

	public boolean statelessPrintf() {
		return this.statelessPrintf;
	}

	public PrintStream out() {
		return this.out;
	}

	public PrintStream err() {
		return this.err;
	}

	public boolean printTransitions() {
		return this.showTransitions || this.verbose || this.debug;
	}

	public boolean printStates() {
		return this.showStates || this.verbose || this.debug;
	}

	public ErrorStateEquivalence errorStateEquiv() {
		return errorStateEquiv;
	}

	public void setErrorStateEquiv(ErrorStateEquivalence errorStateEquiv) {
		this.errorStateEquiv = errorStateEquiv;
	}

	public String directSymEx() {
		return directSymEx;
	}

	public void setDirectSymEx(String directSymEx) {
		this.directSymEx = directSymEx;
	}

	public boolean prob() {
		return prob;
	}

	public void setProb(boolean enableProb) {
		this.prob = enableProb;
	}

	public void setCollectProcesses(boolean collectProcesses) {
		this.collectProcesses = collectProcesses;
	}

	public void setCollectScopes(boolean collectScopes) {
		this.collectScopes = collectScopes;
	}

	public boolean showProgram() {
		return showProgram;
	}

	public void setShowProgram(boolean showProgram) {
		this.showProgram = showProgram;
	}

	public boolean showPathConditonAsOneLine() {
		return showPathConditon.equals("LINE");
	}

	public boolean showPathConditonAsMultipleLine() {
		return showPathConditon.equals("BLOCK");
	}

	public boolean ompNoSimplify() {
		return ompNoSimplify;
	}

	public boolean ompOnlySimplifier() {
		return ompOnlySimplifier;
	}

	public void setOmpNoSimplifier(boolean ompNoSimplify) {
		this.ompNoSimplify = ompNoSimplify;
	}

	public void setOmpOnlySimplify(boolean ompOnlySimplify) {
		this.ompOnlySimplifier = ompOnlySimplify;
	}

	public boolean collectProcesses() {
		return this.collectProcesses;
	}

	public boolean collectScopes() {
		return this.collectScopes;
	}

	public boolean collectHeaps() {
		return collectHeaps;
	}

	public boolean web() {
		return web;
	}

	public void setCollectHeaps(boolean collectHeaps) {
		this.collectHeaps = collectHeaps;
	}

	public boolean showPreproc() {
		return showPreproc;
	}

	public void setShowPreproc(boolean showPreproc) {
		this.showPreproc = showPreproc;
	}

	public boolean showAST() {
		return showAST;
	}

	public void setShowAST(boolean showAST) {
		this.showAST = showAST;
	}

	public boolean showModel() {
		return showModel;
	}

	public void setShowModel(boolean showModel) {
		this.showModel = showModel;
	}

	public boolean showInputVars() {
		return showInputVars;
	}

	public void setShowInputVars(boolean showInputVars) {
		this.showInputVars = showInputVars;
	}

	public boolean showTime() {
		return showTime;
	}

	public void setShowTime(boolean showTime) {
		this.showTime = showTime;
	}

	public boolean showMemoryUnits() {
		return showMemoryUnits;
	}

	public void setShowMemoryUnits(boolean showMemoryUnits) {
		this.showMemoryUnits = showMemoryUnits;
	}

	/**
	 * returns the maximal number of processes allowed in a state. -1 means
	 * infinitely many processes are allowed.
	 */
	public int getProcBound() {
		return procBound;
	}

	public void setProcBound(int value) {
		this.procBound = value;
	}

	public int ompLoopDecomp() {
		return ompLoopDecomp;
	}

	public void setOmpLoopDecomp(int ompLoopDecomp) {
		this.ompLoopDecomp = ompLoopDecomp;
	}

	public boolean isReplay() {
		return isReplay;
	}

	public void setReplay(boolean isReplay) {
		this.isReplay = isReplay;
	}

	public void setRuntimeUpdate(boolean enableUpdateThread) {
		this.runtimeUpdate = enableUpdateThread;
	}

	public boolean runtimeUpdate() {
		return this.runtimeUpdate;
	}

	public boolean isQuiet() {
		return quiet;
	}

	public void setQuiet(boolean quiet) {
		this.quiet = quiet;
	}

	/**
	 * @return the showUnreach
	 */
	public boolean showUnreach() {
		return showUnreach;
	}

	/**
	 * @param showUnreach the showUnreach to set
	 */
	public void setShowUnreach(boolean showUnreach) {
		this.showUnreach = showUnreach;
	}

	/**
	 * @return the absAnalysis
	 */
	public boolean analyzeAbs() {
		return absAnalysis;
	}

	/**
	 * @param absAnalysis the absAnalysis to set
	 */
	public void setAbsAnalysis(boolean absAnalysis) {
		this.absAnalysis = absAnalysis;
	}

	/**
	 * @return the inputVariables
	 */
	public Map<String, Object> inputVariables() {
		return inputVariables;
	}

	/**
	 * @param inputVariables the inputVariables to set
	 */
	public void setInputVariables(Map<String, Object> inputVariables) {
		this.inputVariables = inputVariables;
	}

	/**
	 * @return the collectOutputs
	 */
	public boolean collectOutputs() {
		return collectOutputs;
	}

	/**
	 * @param collectOutputs the collectOutputs to set
	 */
	public void setCollectOutputs(boolean collectOutputs) {
		this.collectOutputs = collectOutputs;
	}

	public boolean isEnableMpiContract() {
		return mpiContractFunction != CIVLConstants.CONTRACT_CHECK_NONE;
	}

	public void setMpiContractFunction(String function) {
		if (function.equals(CIVLConstants.CONTRACT_CHECK_ALL))
			mpiContractFunction = CIVLConstants.CONTRACT_CHECK_ALL;
		else if (function.equals(CIVLConstants.CONTRACT_CHECK_NONE))
			mpiContractFunction = CIVLConstants.CONTRACT_CHECK_NONE;
		else
			mpiContractFunction = function;
	}

	public void setMpiModel(MPIModelKind modelKind) {
		mpiModel = modelKind;
	}

	/**
	 * @return the MPI implementation model that will be used for this run.
	 */
	public MPIModelKind mpiModel() {
		return mpiModel;
	}

	/**
	 * @return the timeout
	 */
	public int timeout() {
		return timeout;
	}

	/**
	 * @param timeout the timeout to set
	 */
	public void setTimeout(int timeout) {
		this.timeout = timeout;
	}

	public boolean unpreproc() {
		return unpreproc;
	}

	public void setUnpreproc(boolean unpreproc) {
		this.unpreproc = unpreproc;
	}

	/**
	 * @return the target function name which is the only one will be verified under
	 *         (mpi-)contract mode. Absent of the target function name will cause
	 *         this method returns <code>null</code> which means verify all
	 *         annotated functions.
	 */
	public String mpiContractFunction() {
		return this.mpiContractFunction;
	}

	/**
	 * @return the collectSymbolicNames
	 */
	public boolean collectSymbolicNames() {
		return collectSymbolicNames;
	}

	/**
	 * @param collectSymbolicNames the collectSymbolicNames to set
	 */
	public void setCollectSymbolicNames(boolean collectSymbolicNames) {
		this.collectSymbolicNames = collectSymbolicNames;
	}

	/**
	 * @return the checkExpressionError
	 */
	public boolean checkExpressionError() {
		return checkExpressionError;
	}

	/**
	 * @param checkExpressionError the checkExpressionError to set
	 */
	public void setCheckExpressionError(boolean checkExpressionError) {
		this.checkExpressionError = checkExpressionError;
	}

	public boolean showPathConditon() {
		return !this.showPathConditon.equals("NONE");
	}

	public boolean inSubprogram() {
		return isInSubprogram;
	}

	public void setInSubprogram(boolean isInSubprogram) {
		this.isInSubprogram = isInSubprogram;
	}

	public int getIntBit() {
		return intBit;
	}

	public void setIntBit(int intBit) {
		this.intBit = intBit;
	}

	public boolean isIntOperationTransiformer() {
		return intOperationTransiformer;
	}

	public void setIntOperationTransiformer(boolean intOperationTransiformer) {
		this.intOperationTransiformer = intOperationTransiformer;
	}

	public int getMaxProcs() {
		return maxProcs;
	}

	public void setMaxProcs(int maxProcs) {
		this.maxProcs = maxProcs;
	}

	/**
	 * @return true iff loop invariant is enabled
	 */
	public boolean loopInvariantEnabled() {
		return this.loopInvariantEnabled;
	}

	public boolean convergeWithMemEquality() {
		return this.convergeWithMemEq;
	}

	/**
	 * An upper bound on the number of preemptions allowed in an execution. Only
	 * used if doing a preemptive-bounded search. If doing a regular search, this
	 * will be -1, the default value. Otherwise, it should be nonnegative.
	 * 
	 * @return the preemption bound or -1
	 */
	public int preemptionBound() {
		return this.preemptionBound;
	}

	public boolean disableLocalBlock() {
		return this.disableLocalBlock;
	}

	/**
	 * If this is true, and termination is being checked, then a cycle in which some
	 * process remains enabled at each state will not be considered a violation of
	 * non-termination (as it is not considered to represent a real execution).
	 */
	public boolean isFair() {
		return fair;
	}

	public void setFair(boolean val) {
		this.fair = val;
	}

	/**
	 * Returns whether we are using dynamic partial order reduction
	 */
	public boolean dporEnabled() {
		return dpor;
	}

	public void setDpor(boolean val) {
		this.dpor = val;
		if (dpor)
			setCollectProcesses(false);
	}
}