Module dev.civl.mc
Package dev.civl.mc.config.IF

Class CIVLConfiguration

java.lang.Object
dev.civl.mc.config.IF.CIVLConfiguration
public class CIVLConfiguration extends Object
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

  • Field Details

  • Constructor Details

    • CIVLConfiguration

      public CIVLConfiguration(dev.civl.gmc.GMCSection config)
      Constructs a new CIVL configuration object from the command line configuration.
      Parameters:
      config - The command line configuration.

    • CIVLConfiguration

      public CIVLConfiguration(CIVLConfiguration config)

    • CIVLConfiguration

      public CIVLConfiguration()

  • Method Details

    • checkDeadlockKind

      public CIVLConstants.DeadlockKind checkDeadlockKind()
      Returns:
      returns the kind of deadlocks we are checking for

    • setCheckDeadlockKind

      public void setCheckDeadlockKind(CIVLConstants.DeadlockKind checkDeadlockKind)
      Sets the kind of deadlocks we want to check for
      Parameters:
      checkDeadlockKind - The new kind of deadlock we want to check for

    • isToggleableProperty

      public boolean isToggleableProperty(CIVLProperty prop)
      Determines whether a CIVLProperty is toggleable. A CIVLProperty is toggleable if it is controlled by a boolean command line option.
      Parameters:
      prop - The CIVLProperty that we want to check is toggleable
      Returns:
      whether prop is toggleable

    • isPropertyToggled

      public boolean isPropertyToggled(CIVLProperty prop)
      Determines if a toggleable property is toggled, i.e. is turned on.
      Parameters:
      prop - The property we want to query. The property must be toggleable. Otherwise it is an error.
      Returns:
      returns whether prop is toggled.

    • setToggleableProperty

      public void setToggleableProperty(CIVLProperty prop, boolean value)
      Sets a CIVLProperty to be toggleable and to be either turned on or off
      Parameters:
      prop - The CIVLProperty we want to control
      value - The value of the CIVLProperty

    • getCheckedPropertiesSummary

      public String getCheckedPropertiesSummary()
      Generates a summary of all CIVLProperty's that are enabled
      Returns:
      summary of enabled CIVLProperty's

    • setOut

      public void setOut(PrintStream out)

    • setErr

      public void setErr(PrintStream err)

    • setDebug

      public void setDebug(boolean debug)

    • setEnablePrintf

      public void setEnablePrintf(boolean enablePrintf)

    • setSaveStates

      public void setSaveStates(boolean saveStates)

    • setShowAmpleSet

      public void setShowAmpleSet(boolean showAmpleSet)

    • setShowAmpleSetWtStates

      public void setShowAmpleSetWtStates(boolean showAmpleSetWtStates)

    • setShowSavedStates

      public void setShowSavedStates(boolean showSavedStates)

    • setShowStates

      public void setShowStates(boolean showStates)

    • setShowTransitions

      public void setShowTransitions(boolean showTransitions)

    • setSimplify

      public void setSimplify(boolean simplify)

    • setStatelessPrintf

      public void setStatelessPrintf(boolean statelessPrintf)

    • setVerbose

      public void setVerbose(boolean verbose)

    • debug

      public boolean debug()

    • verbose

      public boolean verbose()

    • debugOrVerbose

      public boolean debugOrVerbose()

    • enablePrintf

      public boolean enablePrintf()

    • saveStates

      public boolean saveStates()

    • showAmpleSet

      public boolean showAmpleSet()

    • showAmpleSetWtStates

      public boolean showAmpleSetWtStates()

    • showSavedStates

      public boolean showSavedStates()

    • showStates

      public boolean showStates()

    • showTransitions

      public boolean showTransitions()

    • simplify

      public boolean simplify()

    • statelessPrintf

      public boolean statelessPrintf()

    • out

      public PrintStream out()

    • err

      public PrintStream err()

    • printTransitions

      public boolean printTransitions()

    • printStates

      public boolean printStates()

    • errorStateEquiv

      public CIVLConstants.ErrorStateEquivalence errorStateEquiv()

    • setErrorStateEquiv

      public void setErrorStateEquiv(CIVLConstants.ErrorStateEquivalence errorStateEquiv)

    • directSymEx

      public String directSymEx()

    • setDirectSymEx

      public void setDirectSymEx(String directSymEx)

    • prob

      public boolean prob()

    • setProb

      public void setProb(boolean enableProb)

    • setCollectProcesses

      public void setCollectProcesses(boolean collectProcesses)

    • setCollectScopes

      public void setCollectScopes(boolean collectScopes)

    • showProgram

      public boolean showProgram()

    • setShowProgram

      public void setShowProgram(boolean showProgram)

    • showPathConditonAsOneLine

      public boolean showPathConditonAsOneLine()

    • showPathConditonAsMultipleLine

      public boolean showPathConditonAsMultipleLine()

    • ompNoSimplify

      public boolean ompNoSimplify()

    • ompOnlySimplifier

      public boolean ompOnlySimplifier()

    • setOmpNoSimplifier

      public void setOmpNoSimplifier(boolean ompNoSimplify)

    • setOmpOnlySimplify

      public void setOmpOnlySimplify(boolean ompOnlySimplify)

    • collectProcesses

      public boolean collectProcesses()

    • collectScopes

      public boolean collectScopes()

    • collectHeaps

      public boolean collectHeaps()

    • web

      public boolean web()

    • setCollectHeaps

      public void setCollectHeaps(boolean collectHeaps)

    • showPreproc

      public boolean showPreproc()

    • setShowPreproc

      public void setShowPreproc(boolean showPreproc)

    • showAST

      public boolean showAST()

    • setShowAST

      public void setShowAST(boolean showAST)

    • showModel

      public boolean showModel()

    • setShowModel

      public void setShowModel(boolean showModel)

    • showInputVars

      public boolean showInputVars()

    • setShowInputVars

      public void setShowInputVars(boolean showInputVars)

    • showTime

      public boolean showTime()

    • setShowTime

      public void setShowTime(boolean showTime)

    • showMemoryUnits

      public boolean showMemoryUnits()

    • setShowMemoryUnits

      public void setShowMemoryUnits(boolean showMemoryUnits)

    • getProcBound

      public int getProcBound()
      returns the maximal number of processes allowed in a state. -1 means infinitely many processes are allowed.

    • setProcBound

      public void setProcBound(int value)

    • ompLoopDecomp

      public int ompLoopDecomp()

    • setOmpLoopDecomp

      public void setOmpLoopDecomp(int ompLoopDecomp)

    • isReplay

      public boolean isReplay()

    • setReplay

      public void setReplay(boolean isReplay)

    • setRuntimeUpdate

      public void setRuntimeUpdate(boolean enableUpdateThread)

    • runtimeUpdate

      public boolean runtimeUpdate()

    • isQuiet

      public boolean isQuiet()

    • setQuiet

      public void setQuiet(boolean quiet)

    • showUnreach

      public boolean showUnreach()
      Returns:
      the showUnreach

    • setShowUnreach

      public void setShowUnreach(boolean showUnreach)
      Parameters:
      showUnreach - the showUnreach to set

    • analyzeAbs

      public boolean analyzeAbs()
      Returns:
      the absAnalysis

    • setAbsAnalysis

      public void setAbsAnalysis(boolean absAnalysis)
      Parameters:
      absAnalysis - the absAnalysis to set

    • inputVariables

      public Map<String,Object> inputVariables()
      Returns:
      the inputVariables

    • setInputVariables

      public void setInputVariables(Map<String,Object> inputVariables)
      Parameters:
      inputVariables - the inputVariables to set

    • collectOutputs

      public boolean collectOutputs()
      Returns:
      the collectOutputs

    • setCollectOutputs

      public void setCollectOutputs(boolean collectOutputs)
      Parameters:
      collectOutputs - the collectOutputs to set

    • isEnableMpiContract

      public boolean isEnableMpiContract()

    • setMpiContractFunction

      public void setMpiContractFunction(String function)

    • setMpiModel

      public void setMpiModel(CIVLConstants.MPIModelKind modelKind)

    • mpiModel

      public CIVLConstants.MPIModelKind mpiModel()
      Returns:
      the MPI implementation model that will be used for this run.

    • timeout

      public int timeout()
      Returns:
      the timeout

    • setTimeout

      public void setTimeout(int timeout)
      Parameters:
      timeout - the timeout to set

    • unpreproc

      public boolean unpreproc()

    • setUnpreproc

      public void setUnpreproc(boolean unpreproc)

    • mpiContractFunction

      public String mpiContractFunction()
      Returns:
      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 null which means verify all annotated functions.

    • collectSymbolicNames

      public boolean collectSymbolicNames()
      Returns:
      the collectSymbolicNames

    • setCollectSymbolicNames

      public void setCollectSymbolicNames(boolean collectSymbolicNames)
      Parameters:
      collectSymbolicNames - the collectSymbolicNames to set

    • checkExpressionError

      public boolean checkExpressionError()
      Returns:
      the checkExpressionError

    • setCheckExpressionError

      public void setCheckExpressionError(boolean checkExpressionError)
      Parameters:
      checkExpressionError - the checkExpressionError to set

    • showPathConditon

      public boolean showPathConditon()

    • inSubprogram

      public boolean inSubprogram()

    • setInSubprogram

      public void setInSubprogram(boolean isInSubprogram)

    • getIntBit

      public int getIntBit()

    • setIntBit

      public void setIntBit(int intBit)

    • isIntOperationTransiformer

      public boolean isIntOperationTransiformer()

    • setIntOperationTransiformer

      public void setIntOperationTransiformer(boolean intOperationTransiformer)

    • getMaxProcs

      public int getMaxProcs()

    • setMaxProcs

      public void setMaxProcs(int maxProcs)

    • loopInvariantEnabled

      public boolean loopInvariantEnabled()
      Returns:
      true iff loop invariant is enabled

    • convergeWithMemEquality

      public boolean convergeWithMemEquality()

    • preemptionBound

      public int preemptionBound()
      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.
      Returns:
      the preemption bound or -1

    • disableLocalBlock

      public boolean disableLocalBlock()

    • isFair

      public boolean isFair()
      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).

    • setFair

      public void setFair(boolean val)

    • dporEnabled

      public boolean dporEnabled()
      Returns whether we are using dynamic partial order reduction

    • setDpor

      public void setDpor(boolean val)