Index (GMC 2.0 main 57 [df56db2])

A B C D E F G H I L M N O P R S T U V W
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form

A

addAllToBacktrack(Collection<Integer>) - Method in class dev.civl.gmc.dpor.DporStackEntry: Adds all of the processes in procs which are not already in the backtrack set Precondition: All processes in procs are enabled at this entry's state
addEntry(DporStackEntry<?, ?>) - Method in class dev.civl.gmc.dpor.DporHbSet
addFreeArg(String) - Method in class dev.civl.gmc.GMCSection: Adds a free argument to the list of free arguments associated to this configuration.
addRace(DporStackEntry<STATE, TRANSITION>, int) - Method in class dev.civl.gmc.dpor.DporSearchStack: Marks a race between the transition of entry and one of the next transitions at the current state from the process pid.
addSection(GMCSection) - Method in class dev.civl.gmc.GMCConfiguration: Adds a section to the NON-anonymous section map.
addToBacktrack(int) - Method in class dev.civl.gmc.dpor.DporStackEntry: Add process pid into this entry's backtrack set
addTraceStep(TraceStepIF<STATE>) - Method in class dev.civl.gmc.Trace: Adds a new trace step to this trace.
allTransitions(Integer) - Method in class dev.civl.gmc.smc.MatrixDirectedGraph: Get all outgoing transitions from the given source state to all other states in this graph.
ampleSet(Integer) - Method in class dev.civl.gmc.smc.SMCEnabler: Return the candidate ampleSet of transitions departing from a given state by satisfying the following three conditions:
ampleSet(STATE) - Method in interface dev.civl.gmc.seq.EnablerIF: Return the candidate ampleSet of transitions departing from a given state by satisfying the following three conditions:
ANONYMOUS_SECTION - Static variable in class dev.civl.gmc.GMCConfiguration: The reserved name of the anonymous GMCSection of a configuration.

B

BOOLEAN - Enum constant in enum class dev.civl.gmc.Option.OptionType
boundDepth(int) - Method in class dev.civl.gmc.seq.DfsSearcher

C

cacheTraceStep(TRANSITION, TraceStepIF<STATE>) - Method in class dev.civl.gmc.dpor.DporNode: Accepts a transition and the trace step that it entails and caches this association.
checkDependent(DporSearchStack<STATE, TRANSITION>, int, int) - Method in interface dev.civl.gmc.dpor.DependencyAnalyzer: Checks whether the transition at "stackIndex" in the stack is dependent with process pid
checkStackTrace(StackEntry<STATE, TRANSITION>) - Method in class dev.civl.gmc.seq.DfsSearcher
chooseEnabledTransition(STATE) - Method in class dev.civl.gmc.GuidedTransitionChooser
chooseEnabledTransition(STATE) - Method in class dev.civl.gmc.RandomTransitionChooser
chooseEnabledTransition(STATE) - Method in interface dev.civl.gmc.TransitionChooser: Using some protocol, chooses one of the transitions enabled at the given state.
clone() - Method in class dev.civl.gmc.GMCConfiguration: Returns a deep copy of this configuration.
clone() - Method in class dev.civl.gmc.GMCSection: Returns a deep copy of this configuration.
CommandLineException - Exception Class in dev.civl.gmc: An exception that is thrown if the command line arguments are not formatted correctly.
CommandLineException(String) - Constructor for exception class dev.civl.gmc.CommandLineException: Constructs new instance with given message.
CommandLineParser - Class in dev.civl.gmc: A tool for parsing a command line and generating a GMCConfiguration.
CommandLineParser(Collection<Option>) - Constructor for class dev.civl.gmc.CommandLineParser: Constructs a new parser from the given collection of options.
compareTo(LogEntry) - Method in class dev.civl.gmc.LogEntry: Compares this with another log entry in the natural order.
ConcurrentDfsSearcher<STATE,TRANSITION> - Class in dev.civl.gmc.concurrent: This ConcurrentDfsSearcher is implemented based on Alfons Laarman's algorithm in paper "Partial-Order Reduction for Multi-Core LTL Model Checking", but there are improvements being made.
ConcurrentDfsSearcher(EnablerIF<STATE, TRANSITION>, ConcurrentStateManagerIF<STATE, TRANSITION>, StatePredicateIF<STATE>, int) - Constructor for class dev.civl.gmc.concurrent.ConcurrentDfsSearcher
ConcurrentNode<STATE> - Class in dev.civl.gmc.concurrent
ConcurrentNode(STATE) - Constructor for class dev.civl.gmc.concurrent.ConcurrentNode
ConcurrentNodeFactory<STATE,TRANSITION> - Class in dev.civl.gmc.concurrent
ConcurrentNodeFactory(ConcurrentStateManagerIF<STATE, TRANSITION>) - Constructor for class dev.civl.gmc.concurrent.ConcurrentNodeFactory
ConcurrentStateManagerIF<STATE,TRANSITION> - Class in dev.civl.gmc.concurrent: A ConcurrentStateManager is used by a ConcurrentDfsSearcher which encapsulates all methods that are needed by ConcurrentDfsSearcher on STATE.
ConcurrentStateManagerIF() - Constructor for class dev.civl.gmc.concurrent.ConcurrentStateManagerIF
contains(DporStackEntry<?, ?>) - Method in class dev.civl.gmc.dpor.DporHbSet
currentState() - Method in class dev.civl.gmc.dpor.DporSearchStack
currentState() - Method in class dev.civl.gmc.seq.DfsSearcher: Returns the state at the top of the stack, without modifying the stack.
currentTransition() - Method in class dev.civl.gmc.dpor.DporSearchStack
currentTransition() - Method in class dev.civl.gmc.dpor.DporStackEntry
cycleFound() - Method in class dev.civl.gmc.concurrent.ConcurrentDfsSearcher
cycleFound() - Method in class dev.civl.gmc.seq.DfsSearcher: If reportCycleAsViolation is true, and the search terminates with a "true" value, then this method can be called to determine whether the predicate holds (indicating a standard property violation) or a cycle has been found.

D

debug(Integer, List<Integer>) - Method in class dev.civl.gmc.smc.SimpleStateManager
debug(STATE, List<Integer>) - Method in class dev.civl.gmc.seq.StateManager
debugging() - Method in interface dev.civl.gmc.seq.EnablerIF: Returns the current value of the debugging flag.
debugging() - Method in class dev.civl.gmc.smc.SMCEnabler
decrementTotal() - Method in class dev.civl.gmc.concurrent.MyThreadPool
decrementWaiting() - Method in class dev.civl.gmc.concurrent.MyThreadPool: Decrease the counter for waiting threads.
defaultValue() - Method in class dev.civl.gmc.Option: Returns the default value for this option
DependencyAnalyzer<STATE,TRANSITION> - Interface in dev.civl.gmc.dpor
description() - Method in class dev.civl.gmc.Option: Returns the human-readable description of this option.
dev.civl.gmc - module dev.civl.gmc
dev.civl.gmc - package dev.civl.gmc: The root package of generic model checking is used to construct model checking applications, either sequential or concurrent.
dev.civl.gmc.concurrent - package dev.civl.gmc.concurrent: This package provides concurrent generic model checking functionality.
dev.civl.gmc.dpor - package dev.civl.gmc.dpor
dev.civl.gmc.seq - package dev.civl.gmc.seq: This package provides sequential generic model checking functionality.
dev.civl.gmc.smc - package dev.civl.gmc.smc: A simple implementation of General Model Checker (GMC) is used by a set of code coverage test cases.
dev.civl.gmc.util - package dev.civl.gmc.util: The utility package for GMC, providing a set of utility classes and functions used by GMC.
DfsSearcher<STATE,TRANSITION> - Class in dev.civl.gmc.seq: A DfsSearcher performs a depth-first search of the state space of a transition system, stopping immediately if it finds a state satisfying the given predicate.
DfsSearcher(EnablerIF<STATE, TRANSITION>, StateManager<STATE, TRANSITION>, StatePredicateIF<STATE>, GMCConfiguration) - Constructor for class dev.civl.gmc.seq.DfsSearcher
DfsSearcher(EnablerIF<STATE, TRANSITION>, StateManager<STATE, TRANSITION>, StatePredicateIF<STATE>, GMCConfiguration, PrintStream) - Constructor for class dev.civl.gmc.seq.DfsSearcher: Constructs a new depth first search searcher.
DOUBLE - Enum constant in enum class dev.civl.gmc.Option.OptionType
DporDfsSearcher<STATE,TRANSITION> - Class in dev.civl.gmc.dpor
DporDfsSearcher(DependencyAnalyzer<STATE, TRANSITION>, StateManager<STATE, TRANSITION>, StatePredicateIF<STATE>, GMCConfiguration) - Constructor for class dev.civl.gmc.dpor.DporDfsSearcher
DporDfsSearcher(DependencyAnalyzer<STATE, TRANSITION>, StateManager<STATE, TRANSITION>, StatePredicateIF<STATE>, GMCConfiguration, PrintStream) - Constructor for class dev.civl.gmc.dpor.DporDfsSearcher: Constructs a new depth first search searcher.
DporHbSet - Class in dev.civl.gmc.dpor: Maintains a set of stack entries which are downward closed wrt to the happens-before relation.
DporHbSet() - Constructor for class dev.civl.gmc.dpor.DporHbSet
DporNode<STATE,TRANSITION> - Class in dev.civl.gmc.dpor: Wraps a STATE object with transition caching and persistent data used in the DPOR search
DporNode(STATE, int) - Constructor for class dev.civl.gmc.dpor.DporNode
DporNodeFactory<STATE,TRANSITION> - Class in dev.civl.gmc.dpor
DporNodeFactory(StateManager<STATE, TRANSITION>, boolean) - Constructor for class dev.civl.gmc.dpor.DporNodeFactory
DporSearchStack<STATE,TRANSITION> - Class in dev.civl.gmc.dpor: This class represents the search stack used in the DPOR algorithm.
DporSearchStack.StackTraversal - Class in dev.civl.gmc.dpor: A structure for efficiently traversing the interior entries of this stack in reverse order, skipping entries whose transition occur in a DporHbSet supplied to this object when constructed.
DporStackEntry<STATE,TRANSITION> - Class in dev.civl.gmc.dpor: An element of the DporSearchStack.
DporTransitionData - Class in dev.civl.gmc.dpor: A simple structure to bundle data that is associated to a transition in an execution explored by DPOR.

E

EnablerIF<STATE,TRANSITION> - Interface in dev.civl.gmc.seq: An EnablerIF tells you which transitions should be explored from a given state.
equals(Object) - Method in class dev.civl.gmc.LogEntry: Determines whether this log entry is equal to the given object.
equals(Object) - Method in class dev.civl.gmc.Option
errorBound() - Method in class dev.civl.gmc.ErrorLog
ErrorLog - Class in dev.civl.gmc: A log for recording errors and corresponding traces encountered during a model checking run.
ErrorLog(File, String, PrintStream) - Constructor for class dev.civl.gmc.ErrorLog: Creates new ErrorLog.
ExcessiveErrorException - Exception Class in dev.civl.gmc: An exception thrown when the number of errors encountered in the course of a search of a state-transition system exceeds some specified bound.
ExcessiveErrorException(int) - Constructor for exception class dev.civl.gmc.ExcessiveErrorException: Constructs new instance with given numErrors.
existingTransitions(Integer) - Method in class dev.civl.gmc.smc.MatrixDirectedGraph: Get all existing outgoing transitions from the given sourceState in this graph.
explanation() - Method in class dev.civl.gmc.FalsePredicate: Returns the string "The false predicate is always false."
explanation() - Method in class dev.civl.gmc.smc.Predicate
explanation() - Method in interface dev.civl.gmc.StatePredicateIF: Returns a human-readable explanation of why the predicate does or does not hold, after method StatePredicateIF.holdsAt(S) has been called.
explore(STATE) - Method in class dev.civl.gmc.dpor.DporDfsSearcher: Explore the state space starting at initialState using DPOR.

F

fairCycleCheck() - Method in class dev.civl.gmc.seq.DfsSearcher: Gets the fairCycleCheck bit.
FALSE - Enum constant in enum class dev.civl.gmc.concurrent.ProvisoValue
FalsePredicate<S> - Class in dev.civl.gmc: The state predicate which simply returns "false" at every state.
FalsePredicate() - Constructor for class dev.civl.gmc.FalsePredicate
fullSet(Integer) - Method in class dev.civl.gmc.smc.SMCEnabler
fullSet(STATE) - Method in interface dev.civl.gmc.seq.EnablerIF: Computes the set of transitions which are enabled at state.
fullyExplored() - Method in class dev.civl.gmc.concurrent.ConcurrentNode: Indicate whether a STATE is fully explored (all its descendants have been visited).

G

get(int) - Method in class dev.civl.gmc.dpor.DporSearchStack

getActiveNum() - Method in class dev.civl.gmc.concurrent.MyThreadPool

getAllOptions() - Static method in class dev.civl.gmc.smc.SMCConstants

getAnonymousSection() - Method in class dev.civl.gmc.GMCConfiguration

Returns the anonymous section

getAssociatedNode(STATE) - Method in class dev.civl.gmc.dpor.DporNodeFactory

Get the node associated to the given state, null if there is no such a node.

getChildrenThreadsCounter() - Method in class dev.civl.gmc.concurrent.StackEntry

getConfiguration() - Method in class dev.civl.gmc.LogEntry

Returns the configuration which will be used to replay the trace.

getDebugOut() - Method in class dev.civl.gmc.dpor.DporDfsSearcher

Returns the stream used to print debugging output when the debugging flag is on.

getDebugOut() - Method in class dev.civl.gmc.seq.DfsSearcher

Returns the stream used to print debugging output when the debugging flag is on.

getDebugOut() - Method in interface dev.civl.gmc.seq.EnablerIF

Returns the debugging output stream.

getDebugOut() - Method in class dev.civl.gmc.smc.SMCEnabler

getDepth() - Method in class dev.civl.gmc.seq.SequentialNode

getDestState(Integer, String) - Method in class dev.civl.gmc.smc.MatrixDirectedGraph

Find the destination state with the given sourceState and transition.

getDirectory() - Method in class dev.civl.gmc.ErrorLog

Returns the directory in which trace files and the log will be stored.

getEnabledProcesses(Integer) - Method in class dev.civl.gmc.smc.SimpleStateManager

getEnabledProcesses(STATE) - Method in class dev.civl.gmc.seq.StateManager

getExpand() - Method in class dev.civl.gmc.concurrent.StackEntry

getExpand() - Method in class dev.civl.gmc.seq.SequentialNode

getFinalState() - Method in class dev.civl.gmc.smc.TraceStep

getFinalState() - Method in interface dev.civl.gmc.TraceStepIF

Returns the resulting state of the trace step.

getFreeArg(int) - Method in class dev.civl.gmc.GMCSection

Returns the i-th free argument, indexed from 0.

getFullyExpanded() - Method in class dev.civl.gmc.seq.SequentialNode

getHbSet() - Method in class dev.civl.gmc.dpor.DporStackEntry

Precondition: This entry is not on the top of the stack.

getHbSet(int) - Method in class dev.civl.gmc.dpor.DporSearchStack

getId() - Method in class dev.civl.gmc.dpor.DporNode

getId() - Method in class dev.civl.gmc.LogEntry

Retunrs the ID number of this log entry, which should be unique within the log to which it belongs.

getId() - Method in class dev.civl.gmc.seq.SequentialNode

getId(Integer) - Method in class dev.civl.gmc.smc.SimpleStateManager

getId(STATE) - Method in class dev.civl.gmc.dpor.DporNodeFactory

getId(STATE) - Method in interface dev.civl.gmc.GetIdFunction

getId(STATE) - Method in class dev.civl.gmc.seq.SequentialNodeFactory

getId(STATE) - Method in class dev.civl.gmc.seq.StateManager

Get the id of a normalizedState.

GetIdFunction<STATE> - Interface in dev.civl.gmc

getIgnoreErrors() - Method in class dev.civl.gmc.ErrorLog

getInitialNode(STATE) - Method in class dev.civl.gmc.dpor.DporNodeFactory

Get the

invalid reference

SequentialNode

associated with the initial state.

getInitialNode(STATE) - Method in class dev.civl.gmc.seq.SequentialNodeFactory

Get the SequentialNode associated with the initial state.

getLength() - Method in class dev.civl.gmc.GuidedTransitionChooser

Returns the length of this execution.

getLength() - Method in class dev.civl.gmc.LogEntry

Returns the length of the trace.

getLiveProcesses(Integer) - Method in class dev.civl.gmc.smc.SimpleStateManager

getLiveProcesses(STATE) - Method in class dev.civl.gmc.seq.StateManager

getLog() - Method in class dev.civl.gmc.Simulator

getLogFile() - Method in class dev.civl.gmc.ErrorLog

getMapEntry(Option, String) - Method in class dev.civl.gmc.GMCSection

Given an option of map type, and a key, this returns the value associated to the key in the map associated to option.

getMapValue(Option) - Method in class dev.civl.gmc.GMCSection

Gets the map value associated to an option of map type, or null if no value is associated to that option.

getMaxNumOfThread() - Method in class dev.civl.gmc.concurrent.MyThreadPool

getMinimalCounterexampleSize() - Method in class dev.civl.gmc.ErrorLog

Returns the minimal size of a counterexample reported to this logger, or -1 if no counterexamples have been logged.

getMinimize() - Method in class dev.civl.gmc.concurrent.ConcurrentDfsSearcher

getMinimize() - Method in class dev.civl.gmc.ErrorLog

Are we searching for a minimal counterexample?

getMinimize() - Method in class dev.civl.gmc.seq.DfsSearcher

getMinimumSuccessorStackIndex() - Method in class dev.civl.gmc.concurrent.StackEntry

getMinimumSuccessorStackIndex() - Method in class dev.civl.gmc.seq.StackEntry

getName() - Method in class dev.civl.gmc.GMCSection

Returns the name of this section.

getNode() - Method in class dev.civl.gmc.concurrent.StackEntry

getNode() - Method in class dev.civl.gmc.dpor.DporStackEntry

getNode() - Method in class dev.civl.gmc.seq.StackEntry

getNode(TraceStepIF<STATE>) - Method in class dev.civl.gmc.dpor.DporNodeFactory

Implements the fly-weight pattern and normalize a state.

getNode(TraceStepIF<STATE>) - Method in class dev.civl.gmc.seq.SequentialNodeFactory

Implements the fly-weight pattern and normalize a state.

getNode(STATE) - Method in class dev.civl.gmc.concurrent.ConcurrentNodeFactory

Implements the fly-weight pattern.

getNode(STATE) - Method in class dev.civl.gmc.seq.SequentialNodeFactory

Get the node associated to the given state, null there is no such a node.

getNumFreeArgs() - Method in class dev.civl.gmc.GMCSection

Returns the current number of free arguments associated to this configuration.

getNumSections() - Method in class dev.civl.gmc.GMCConfiguration

Returns the number of NON-anonymous sections.

getOption(String) - Method in class dev.civl.gmc.GMCConfiguration

Returns the option with the given name associated to this configuration, or null if there is none.

getOptions() - Method in class dev.civl.gmc.GMCConfiguration

Returns the set of options associated to this configuration.

getPid() - Method in class dev.civl.gmc.dpor.DporStackEntry

Precondition: !DporStackEntry.isDone()

getPid(String) - Method in class dev.civl.gmc.smc.SimpleStateManager

getPid(TRANSITION) - Method in class dev.civl.gmc.seq.StateManager

Gets the ID number of the process that is responsible for executing transition.

getPredicate() - Method in class dev.civl.gmc.Simulator

getPreemptionPid() - Method in class dev.civl.gmc.seq.StackEntry

If this step is preemptible, this method returns the PID of the process that executed the previous transition.

getPrevStackPosition() - Method in class dev.civl.gmc.dpor.DporStackEntry

Precondition: This entry is not the top of the stack.

getPrintAllStates() - Method in class dev.civl.gmc.Simulator

getProviso() - Method in class dev.civl.gmc.concurrent.ConcurrentNode

getRunningNum() - Method in class dev.civl.gmc.concurrent.MyThreadPool

getSaveStates() - Method in class dev.civl.gmc.GMCConfiguration

getSection(String) - Method in class dev.civl.gmc.GMCConfiguration

Returns the section with the given name, or null if there is none.

getSections() - Method in class dev.civl.gmc.GMCConfiguration

Returns an iterable object of the NON-anonymous sections.

getSeed() - Method in class dev.civl.gmc.RandomTransitionChooser

getSeen() - Method in class dev.civl.gmc.seq.SequentialNode

Returns the value of the seen flag associated to the given state.

getStackPosition() - Method in class dev.civl.gmc.dpor.DporNode

getStackPosition() - Method in class dev.civl.gmc.dpor.DporStackEntry

getStackPosition() - Method in class dev.civl.gmc.seq.SequentialNode

Get the position of this SequentialNode on dfs stack or -1 if it is not on stack.

getState() - Method in class dev.civl.gmc.concurrent.ConcurrentNode

getState() - Method in class dev.civl.gmc.concurrent.StackEntry

getState() - Method in class dev.civl.gmc.dpor.DporNode

getState() - Method in class dev.civl.gmc.dpor.DporStackEntry

getState() - Method in class dev.civl.gmc.seq.SequentialNode

getState() - Method in class dev.civl.gmc.seq.StackEntry

getTid() - Method in class dev.civl.gmc.concurrent.StackEntry

getTid() - Method in class dev.civl.gmc.dpor.DporStackEntry

getTid() - Method in class dev.civl.gmc.seq.StackEntry

getTraceFile() - Method in class dev.civl.gmc.LogEntry

Returns the file to which the trace is saved.

getTraceStepCache(TRANSITION) - Method in class dev.civl.gmc.dpor.DporNode

getTransitionIterator() - Method in class dev.civl.gmc.concurrent.StackEntry

getTransitionIterator() - Method in class dev.civl.gmc.seq.StackEntry

getTransitions() - Method in class dev.civl.gmc.concurrent.StackEntry

getTransitions() - Method in class dev.civl.gmc.seq.StackEntry

getTransitions(Integer, int) - Method in class dev.civl.gmc.smc.SimpleStateManager

getTransitions(STATE, int) - Method in class dev.civl.gmc.seq.StateManager

getValue(Option) - Method in class dev.civl.gmc.GMCSection

Gets the value associated to an option or null if no value is associated to that option.

getValueOrDefault(Option) - Method in class dev.civl.gmc.GMCSection

Returns the value associated to an option or the default value for that option if no value is associated to it.

GMCConfiguration - Class in dev.civl.gmc

A GMCConfiguration is composed of a number of GMCSection's, each of which encapsulates a set of key-value pairs, where the keys correspond to commandline parameters and the value is the value assigned to that parameter.

GMCConfiguration(Collection<Option>) - Constructor for class dev.civl.gmc.GMCConfiguration

Constructs new configuration with the set of options obtained from the given collection.

GMCSection - Class in dev.civl.gmc

A GMCSection has a unique name and it encapsulates a set of key-value pairs, where the keys correspond to commandline parameters and the value is the value assigned to that parameter.

GMCSection(GMCConfiguration, String) - Constructor for class dev.civl.gmc.GMCSection

Constructs a new instance of GMCSection with the given GMCConfiguration and name.

GMCSection(String) - Constructor for class dev.civl.gmc.GMCSection

Constructs a new GMCSection with the given name

GuidedTransitionChooser<STATE,TRANSITION> - Class in dev.civl.gmc

Transition Chooser which makes its choice using an explicit "guide".

GuidedTransitionChooser(EnablerIF<STATE, TRANSITION>, File) - Constructor for class dev.civl.gmc.GuidedTransitionChooser

H

hashCode() - Method in class dev.civl.gmc.Option
hasNext() - Method in class dev.civl.gmc.concurrent.StackEntry
hasNext() - Method in class dev.civl.gmc.seq.StackEntry
hbSet - Variable in class dev.civl.gmc.dpor.DporTransitionData: The DporHbSet of stack entries with transitions that happen-before this transition
holdsAt(Integer) - Method in class dev.civl.gmc.smc.Predicate: Does this predicate hold at the given state?
holdsAt(S) - Method in class dev.civl.gmc.FalsePredicate: Returns false.
holdsAt(S) - Method in interface dev.civl.gmc.StatePredicateIF: Does this predicate hold at the given state?

I

inAtomic(Integer) - Method in class dev.civl.gmc.smc.SMCEnabler
inAtomic(STATE) - Method in interface dev.civl.gmc.seq.EnablerIF: Is the given state in the middle of an atomic action? Such intermediate states should be ignored by some algorithms.
inBacktrack(int) - Method in class dev.civl.gmc.dpor.DporStackEntry
incrementCounter() - Method in class dev.civl.gmc.concurrent.StackEntry
incrementTotal() - Method in class dev.civl.gmc.concurrent.MyThreadPool
incrementWaiting() - Method in class dev.civl.gmc.concurrent.MyThreadPool: Increase the counter for waiting threads.
init() - Method in class dev.civl.gmc.Trace: Returns the initial state of this trace.
INTEGER - Enum constant in enum class dev.civl.gmc.Option.OptionType
isDepthBounded() - Method in class dev.civl.gmc.seq.DfsSearcher
isDone() - Method in class dev.civl.gmc.dpor.DporStackEntry
isEmpty() - Method in class dev.civl.gmc.dpor.DporSearchStack
isFull() - Method in class dev.civl.gmc.concurrent.StackEntry
isPreemptible() - Method in class dev.civl.gmc.seq.StackEntry: Is this step preemptible, i.e., does the set of outgoing transitions include at least one transition from the previous process as well as at least one transition from another process?
isQuiescent() - Method in class dev.civl.gmc.concurrent.MyThreadPool
isQuiet() - Method in class dev.civl.gmc.GMCConfiguration
isQuiet() - Method in class dev.civl.gmc.Simulator
isTrue(Option) - Method in class dev.civl.gmc.GMCSection: Determines whether the value associated to a boolean option should be construed as true in most circumstances.

L

lastEntryPos(int) - Method in class dev.civl.gmc.dpor.DporHbSet
lastState() - Method in class dev.civl.gmc.Trace: Returns the last state of this trace.
left - Variable in class dev.civl.gmc.util.Pair
LogEntry - Class in dev.civl.gmc: An entry in an error log.
LogEntry(GMCConfiguration) - Constructor for class dev.civl.gmc.LogEntry: Default construtor: does nothing.

M

makeStackTraversal(int) - Method in class dev.civl.gmc.dpor.DporSearchStack: Constructs a new DporSearchStack<STATE,TRANSITION>.StackTraversal object for traversing the interior entries of this stack in reverse order, skipping entries whose transition happens before some next transition of proc at the stack's current state.
MAP - Enum constant in enum class dev.civl.gmc.Option.OptionType
MatrixDirectedGraph - Class in dev.civl.gmc.smc: A simple directed graph implemented with a square matrix.
MatrixDirectedGraph(String[][]) - Constructor for class dev.civl.gmc.smc.MatrixDirectedGraph: Constructs a MatrixDirectedGraph with given squareMatrix.
MisguidedExecutionException - Exception Class in dev.civl.gmc
MisguidedExecutionException(String) - Constructor for exception class dev.civl.gmc.MisguidedExecutionException
MyThreadPool - Class in dev.civl.gmc.concurrent: The threadPool That is used to manage the threads used in the algorithm.
MyThreadPool() - Constructor for class dev.civl.gmc.concurrent.MyThreadPool
MyThreadPool(int) - Constructor for class dev.civl.gmc.concurrent.MyThreadPool

N

name() - Method in class dev.civl.gmc.concurrent.ConcurrentDfsSearcher

name() - Method in class dev.civl.gmc.Option

Returns the name of this option.

name() - Method in class dev.civl.gmc.seq.DfsSearcher

name() - Method in class dev.civl.gmc.Trace

Returns the name of this trace.

newConfig() - Method in class dev.civl.gmc.CommandLineParser

Returns new, empty configuration with option set equal to the set of options associated to this parser.

newMapOption(String, String) - Static method in class dev.civl.gmc.Option

Returns a new option of type MAP with default value the empty map.

newScalarOption(String, Option.OptionType, String, Object) - Static method in class dev.civl.gmc.Option

newStackEntry(ConcurrentNode<STATE>, Collection<TRANSITION>, boolean) - Method in class dev.civl.gmc.concurrent.ConcurrentNodeFactory

Construct a new stack entry which will be pushed onto the stack.

newStackEntry(SequentialNode<STATE>, Collection<TRANSITION>, int) - Method in class dev.civl.gmc.seq.SequentialNodeFactory

Construct a new stack entry which will be pushed onto the stack.

next() - Method in class dev.civl.gmc.concurrent.StackEntry

next() - Method in class dev.civl.gmc.dpor.DporSearchStack.StackTraversal

Traverses to the next stack entry and returns it.

next() - Method in class dev.civl.gmc.seq.StackEntry

nextState(Integer, String) - Method in class dev.civl.gmc.smc.SimpleStateManager

nextState(STATE, TRANSITION) - Method in class dev.civl.gmc.seq.StateManager

Given a state and a transition, returns the trace step after executing the transition at the given state.

nextTransition(StateManager<STATE, TRANSITION>) - Method in class dev.civl.gmc.dpor.DporStackEntry

Increments to the next outgoing transition to be explored from the current state, moving to the next process in the backtrack set if necessary.

normalize(TraceStepIF<Integer>) - Method in class dev.civl.gmc.smc.SimpleStateManager

normalize(TraceStepIF<STATE>) - Method in class dev.civl.gmc.seq.StateManager

Normalize/simplify a state.

normalize(STATE) - Method in class dev.civl.gmc.concurrent.ConcurrentStateManagerIF

numCrossTraceSteps() - Method in interface dev.civl.gmc.dpor.DependencyAnalyzer

Number of trace steps executed from a "cross state" (see

invalid reference

ImmutableStateFactory#crossState

) for the purposes of determining dependence.

numCrossTransitions() - Method in interface dev.civl.gmc.dpor.DependencyAnalyzer

Number of transitions executed from a "cross state" (see

invalid reference

ImmutableStateFactory#crossState

) for the purposes of determining dependence.

numEntries() - Method in class dev.civl.gmc.ErrorLog

numErrors() - Method in class dev.civl.gmc.ErrorLog

numErrors() - Method in exception class dev.civl.gmc.ExcessiveErrorException

Returns the number of errors encountered when this exception was thrown

numOfSearchNodeSaved() - Method in class dev.civl.gmc.concurrent.ConcurrentNodeFactory

numOfSearchNodeSaved() - Method in class dev.civl.gmc.dpor.DporDfsSearcher

numOfSearchNodeSaved() - Method in class dev.civl.gmc.dpor.DporNodeFactory

numOfSearchNodeSaved() - Method in class dev.civl.gmc.seq.DfsSearcher

numOfSearchNodeSaved() - Method in class dev.civl.gmc.seq.SequentialNodeFactory

numOfSteps() - Method in class dev.civl.gmc.Trace

Returns the number of trace steps in this trace.

numStatesMatched() - Method in class dev.civl.gmc.dpor.DporDfsSearcher

The number of states matched so far.

numStatesMatched() - Method in class dev.civl.gmc.dpor.DporSearchStack

numStatesMatched() - Method in class dev.civl.gmc.seq.DfsSearcher

The number of states matched so far.

numStatesSeen() - Method in class dev.civl.gmc.dpor.DporDfsSearcher

The number of states seen in this search.

numStatesSeen() - Method in class dev.civl.gmc.dpor.DporSearchStack

numStatesSeen() - Method in class dev.civl.gmc.seq.DfsSearcher

The number of states seen in this search.

numTraceSteps() - Method in class dev.civl.gmc.dpor.DporDfsSearcher

The number of transitions executed in the course of this search so far.

numTraceSteps() - Method in class dev.civl.gmc.dpor.DporSearchStack

numTraceStepsMatched() - Method in class dev.civl.gmc.dpor.DporDfsSearcher

numTraceStepsMatched() - Method in class dev.civl.gmc.dpor.DporSearchStack

numTransitions() - Method in class dev.civl.gmc.seq.DfsSearcher

The number of transitions executed in the course of this search so far.

O

onStack(int) - Method in class dev.civl.gmc.concurrent.ConcurrentNode: Indicate whether a STATE is on the stack of the thread with certain id.
Option - Class in dev.civl.gmc: An instance of this class represents a command-line parameter for a model checker.
Option.OptionType - Enum Class in dev.civl.gmc: The types of option.
out - Variable in class dev.civl.gmc.GMCConfiguration

P

Pair<L,R> - Class in dev.civl.gmc.util
Pair(L, R) - Constructor for class dev.civl.gmc.util.Pair
parse(GMCConfiguration, BufferedReader) - Method in class dev.civl.gmc.CommandLineParser: Parses the reader, interpreting lines as command line args, modifying given configuration accordingly.
parse(GMCConfiguration, File) - Method in class dev.civl.gmc.CommandLineParser: Parses a file containing a configuration section, using the command line arguments from that section to modify the given configuration.
parse(GMCConfiguration, Collection<String>) - Method in class dev.civl.gmc.CommandLineParser: Given a collection of strings and a configuration compatible with this parser, parses the strings and uses the resulting information to modify the configuration.
parse(Collection<String>) - Method in class dev.civl.gmc.CommandLineParser: Given a collection of strings, parses them in the order of their iterator to produce a new configuration.
peek() - Method in class dev.civl.gmc.concurrent.StackEntry
peek() - Method in class dev.civl.gmc.seq.StackEntry
play(STATE[], boolean[], String[], TransitionChooser<STATE, TRANSITION>, boolean) - Method in class dev.civl.gmc.Simulator: Plays the trace.
play(STATE, TransitionChooser<STATE, TRANSITION>, boolean) - Method in class dev.civl.gmc.Simulator
play(STATE, STATE, boolean, TransitionChooser<STATE, TRANSITION>, boolean) - Method in class dev.civl.gmc.Simulator
popTransition() - Method in class dev.civl.gmc.dpor.DporSearchStack: Pops the top entry from the stack.
predicate() - Method in class dev.civl.gmc.concurrent.ConcurrentDfsSearcher
predicate() - Method in class dev.civl.gmc.dpor.DporDfsSearcher
predicate() - Method in class dev.civl.gmc.seq.DfsSearcher
Predicate - Class in dev.civl.gmc.smc: The predicate used for detecting violation state defined in the given list states.
Predicate(Integer...) - Constructor for class dev.civl.gmc.smc.Predicate
prevStackPosition - Variable in class dev.civl.gmc.dpor.DporTransitionData: The previous position on the stack of an entry with a transition from this process
print(PrintStream) - Method in class dev.civl.gmc.ErrorLog
print(PrintStream) - Method in class dev.civl.gmc.GMCConfiguration: Prints the current state of this configuration in a manner similar to what would appear on a commandline.
print(PrintStream) - Method in class dev.civl.gmc.GMCSection: Prints the current state of this configuration in a manner similar to what would appear on a commandline.
print(PrintStream) - Method in class dev.civl.gmc.LogEntry: Prints this log entry to the given stream.
print(PrintStream) - Method in class dev.civl.gmc.Option
printAllStatesLong(PrintStream) - Method in class dev.civl.gmc.seq.StateManager: Prints out all the states, in long form, currently "held" by this manager.
printAllStatesLong(PrintStream) - Method in class dev.civl.gmc.smc.SimpleStateManager
printAllStatesShort(PrintStream) - Method in class dev.civl.gmc.seq.StateManager: Prints out all the states, in short form, currently "held" by this manager.
printAllStatesShort(PrintStream) - Method in class dev.civl.gmc.smc.SimpleStateManager
printBody(PrintStream) - Method in class dev.civl.gmc.LogEntry: Prints an explanation of the error.
printStack(PrintStream) - Method in class dev.civl.gmc.dpor.DporDfsSearcher: Prints the whole stack in a human readable form to the given stream.
printStack(PrintStream) - Method in class dev.civl.gmc.seq.DfsSearcher: Prints the whole stack in a human readable form to the given stream.
printStack(PrintStream, boolean, boolean) - Method in class dev.civl.gmc.dpor.DporDfsSearcher: Prints the current stack in a human-readable format.
printStack(PrintStream, boolean, boolean) - Method in class dev.civl.gmc.seq.DfsSearcher: Prints the current stack in a human-readable format.
printStateLong(PrintStream, Integer) - Method in class dev.civl.gmc.smc.SimpleStateManager
printStateLong(PrintStream, STATE) - Method in class dev.civl.gmc.seq.StateManager: Prints out a long human-readable representation of the state.
printStateShort(PrintStream, Integer) - Method in class dev.civl.gmc.smc.SimpleStateManager
printStateShort(PrintStream, STATE) - Method in class dev.civl.gmc.seq.StateManager: Prints out a short human-readable representation of the state.
printSummary(PrintStream) - Method in class dev.civl.gmc.dpor.DporDfsSearcher: Summarizes the current state of the search in a human-readable form printed to the given stream.
printSummary(PrintStream) - Method in class dev.civl.gmc.seq.DfsSearcher: Summarizes the current state of the search in a human-readable form printed to the given stream.
printTraceStep(Integer, TraceStepIF<Integer>) - Method in class dev.civl.gmc.smc.SimpleStateManager
printTraceStep(STATE, TraceStepIF<STATE>) - Method in class dev.civl.gmc.seq.StateManager: This method should print the source state id and transitions within this traceStep.
printTraceStepFinalState(Integer, int) - Method in class dev.civl.gmc.smc.SimpleStateManager
printTraceStepFinalState(STATE, int) - Method in class dev.civl.gmc.seq.StateManager: This method should print the final state of a trace step.
printTransitionLong(PrintStream, String) - Method in class dev.civl.gmc.smc.SimpleStateManager
printTransitionLong(PrintStream, TRANSITION) - Method in class dev.civl.gmc.seq.StateManager: Prints out a long human-readable representation of the transition.
printTransitions() - Method in class dev.civl.gmc.GMCConfiguration
printTransitionShort(PrintStream, String) - Method in class dev.civl.gmc.smc.SimpleStateManager
printTransitionShort(PrintStream, TRANSITION) - Method in class dev.civl.gmc.seq.StateManager: Prints out a short human-readable representation of the transition.
printUsage(PrintStream) - Method in class dev.civl.gmc.CommandLineParser: Prints the list of options in a human-readable format.
proceedToNewState() - Method in class dev.civl.gmc.seq.DfsSearcher: Proceeds with the search until we arrive at a state that has not been seen before (assuming there is one).
procSet() - Method in class dev.civl.gmc.dpor.DporHbSet
ProvisoValue - Enum Class in dev.civl.gmc.concurrent: This enumeration stores the result of checking "stack proviso" of a STATE in the STATE-TRANSITION system.
pushTransition() - Method in class dev.civl.gmc.dpor.DporSearchStack: Explores the current transition and pushes resulting state as a DporStackEntry onto the stack
putMapEntry(Option, String, Object) - Method in class dev.civl.gmc.GMCSection: Given an option of map type, adds or removes the key-value pair to the map corresponding to that option.

R

RandomTransitionChooser<STATE,TRANSITION> - Class in dev.civl.gmc: An implementation of TransitionChooser in which a transition is chosen randomly from the full set of the enabled transitions enabled at a state.
RandomTransitionChooser(EnablerIF<STATE, TRANSITION>) - Constructor for class dev.civl.gmc.RandomTransitionChooser
RandomTransitionChooser(EnablerIF<STATE, TRANSITION>, long) - Constructor for class dev.civl.gmc.RandomTransitionChooser
read(GMCConfiguration) - Method in class dev.civl.gmc.GMCConfiguration: Modifies this configuration by reading in the values of the given configuration and using those to set values of this one.
read(GMCSection) - Method in class dev.civl.gmc.GMCSection: Modifies this section by reading in the values of the given configuration and using those to set values of this one.
report(LogEntry) - Method in class dev.civl.gmc.ErrorLog
reportCycleAsViolation() - Method in class dev.civl.gmc.concurrent.ConcurrentDfsSearcher
reportCycleAsViolation() - Method in class dev.civl.gmc.seq.DfsSearcher
restrictDepth() - Method in class dev.civl.gmc.seq.DfsSearcher: Sets the depth bound to one less than the current stack size.
result() - Method in class dev.civl.gmc.Trace: Returns the verification result of this trace.
right - Variable in class dev.civl.gmc.util.Pair
run(MatrixDirectedGraph, StatePredicateIF<Integer>) - Method in class dev.civl.gmc.smc.SMCSimulator
run(MatrixDirectedGraph, StatePredicateIF<Integer>, GMCConfiguration) - Method in class dev.civl.gmc.smc.SMC: For a given MatrixDirectedGraph graph and a predicate implementing StatePredicateIF,
If the predicate is hold, true will be returned, else false.
Note that the default starting state is the state with id of 0
run(MatrixDirectedGraph, StatePredicateIF<Integer>, Integer) - Method in class dev.civl.gmc.smc.SMCSimulator
run(MatrixDirectedGraph, StatePredicateIF<Integer>, Integer, GMCConfiguration) - Method in class dev.civl.gmc.smc.SMC: For a given MatrixDirectedGraph graph, a predicate implementing StatePredicateIF and a starting state initialState,
If the predicate is hold, true will be returned, else false.

S

save() - Method in class dev.civl.gmc.ErrorLog
search() - Method in class dev.civl.gmc.seq.DfsSearcher: Resumes a depth-first search of the state space starting from the current state.
search(STATE) - Method in class dev.civl.gmc.concurrent.ConcurrentDfsSearcher: Start a concurrent dfs task from a given state
search(STATE) - Method in class dev.civl.gmc.seq.DfsSearcher: Performs a depth-first search starting from the given state.
searcher() - Method in class dev.civl.gmc.ErrorLog
searchForTransition() - Method in class dev.civl.gmc.dpor.DporSearchStack: Traverses to the next available transition to explore, popping from the stack as necessary.
SequentialNode<STATE> - Class in dev.civl.gmc.seq: A Node in the state graph for the sequential depth first search.
SequentialNode(STATE, int) - Constructor for class dev.civl.gmc.seq.SequentialNode
SequentialNodeFactory<STATE,TRANSITION> - Class in dev.civl.gmc.seq: The factory to get a GMC search SequentialNode, if the SequentialNode has been seen before, the seen SequentialNode will be returned, otherwise, a new SequentialNode will be created and returned.
SequentialNodeFactory(StateManager<STATE, TRANSITION>, boolean) - Constructor for class dev.civl.gmc.seq.SequentialNodeFactory
setAnonymousSection(GMCSection) - Method in class dev.civl.gmc.GMCConfiguration: Updates the anonymous section with the given section.
setConfiguration(GMCConfiguration) - Method in class dev.civl.gmc.GMCSection: Updates the configuration associates with this section.
setDebug(boolean) - Method in class dev.civl.gmc.smc.SMC: Set SMC to print debugging info, iff isDebug is true
setDebugging(boolean) - Method in class dev.civl.gmc.dpor.DporDfsSearcher: Set the debugging flag to the given value.
setDebugging(boolean) - Method in class dev.civl.gmc.seq.DfsSearcher: Set the debugging flag to the given value.
setDebugging(boolean) - Method in interface dev.civl.gmc.seq.EnablerIF: Set the debugging flag to the given value.
setDebugging(boolean) - Method in class dev.civl.gmc.smc.SMCEnabler
setDebugOut(PrintStream) - Method in class dev.civl.gmc.dpor.DporDfsSearcher: Sets the debugging output stream to the given stream.
setDebugOut(PrintStream) - Method in class dev.civl.gmc.seq.DfsSearcher: Sets the debugging output stream to the given stream.
setDebugOut(PrintStream) - Method in interface dev.civl.gmc.seq.EnablerIF: Set the debugging output stream to the given stream.
setDebugOut(PrintStream) - Method in class dev.civl.gmc.smc.SMCEnabler
setDepth(int) - Method in class dev.civl.gmc.seq.SequentialNode: Set SequentialNode.depth to a given value.
setErrorBound(int) - Method in class dev.civl.gmc.ErrorLog
setExpand(boolean) - Method in class dev.civl.gmc.concurrent.StackEntry
setExpand(boolean) - Method in class dev.civl.gmc.seq.SequentialNode: Set SequentialNode.expand to a given value.
setFairCycleCheck(boolean) - Method in class dev.civl.gmc.seq.DfsSearcher: Set the fairCycleCheck bit.
setFull(boolean) - Method in class dev.civl.gmc.concurrent.StackEntry
setFullyExpanded(boolean) - Method in class dev.civl.gmc.seq.SequentialNode: Set SequentialNode.fullyExpanded to a certain value.
setFullyExplored(boolean) - Method in class dev.civl.gmc.concurrent.ConcurrentNode: Set "fullyExplored" field of a STATE to a certain boolean value.
setGetIdFunction(GetIdFunction<STATE>) - Method in class dev.civl.gmc.seq.StateManager
setIgnoreErrors(boolean) - Method in class dev.civl.gmc.ErrorLog
setLog(ErrorLog) - Method in class dev.civl.gmc.Simulator
setMapValue(Option, Map<String, Object>) - Method in class dev.civl.gmc.GMCSection: Sets map value or removes map entry from this configuration.
setMinimize(boolean) - Method in class dev.civl.gmc.concurrent.ConcurrentDfsSearcher
setMinimize(boolean) - Method in class dev.civl.gmc.ErrorLog: Sets the minimize flag to given value.
setMinimize(boolean) - Method in class dev.civl.gmc.seq.DfsSearcher
setMinimumSuccessorStackIndex(int) - Method in class dev.civl.gmc.concurrent.StackEntry
setMinimumSuccessorStackIndex(int) - Method in class dev.civl.gmc.seq.StackEntry
setName(String) - Method in class dev.civl.gmc.concurrent.ConcurrentDfsSearcher
setName(String) - Method in class dev.civl.gmc.seq.DfsSearcher
setPredicate(StatePredicateIF<STATE>) - Method in class dev.civl.gmc.Simulator
setPreemptionBound(int) - Method in class dev.civl.gmc.seq.DfsSearcher
setPreemptionPid(int) - Method in class dev.civl.gmc.seq.StackEntry: Sets this entry to be preemptible, with the given pid to be the PID of the previous process.
setPrintAllStates(boolean) - Method in class dev.civl.gmc.Simulator
setPrintStream(PrintStream) - Method in class dev.civl.gmc.GMCConfiguration
setPrintTransition(boolean) - Method in class dev.civl.gmc.GMCConfiguration
setQuiet(boolean) - Method in class dev.civl.gmc.GMCConfiguration
setQuiet(boolean) - Method in class dev.civl.gmc.Simulator
setReportCycleAsViolation(boolean) - Method in class dev.civl.gmc.concurrent.ConcurrentDfsSearcher: If you want to check for cycles in the state space, and report the existence of a cycle as a violation, this flag should be set to true.
setReportCycleAsViolation(boolean) - Method in class dev.civl.gmc.seq.DfsSearcher: If you want to check for cycles in the state space, and report the existence of a cycle as a violation, this flag should be set to true.
setSaveStates(boolean) - Method in class dev.civl.gmc.GMCConfiguration
setScalarValue(Option, Object) - Method in class dev.civl.gmc.GMCSection: Adds the key-value pair for a scalar value to the parameter map.
setSearcher(DfsSearcher<?, ?>) - Method in class dev.civl.gmc.ErrorLog
setSeen(boolean) - Method in class dev.civl.gmc.seq.SequentialNode: Sets the "seen flag" to a given value.
setStackPosition(int) - Method in class dev.civl.gmc.dpor.DporNode: Set the stack position field of the DporNode.
setStackPosition(int) - Method in class dev.civl.gmc.seq.SequentialNode: Set the stack position field of the SequentialNode.
setViolation(boolean) - Method in class dev.civl.gmc.Trace: Updates the flag of violation.
shutdown() - Method in class dev.civl.gmc.concurrent.MyThreadPool
SimpleStateManager - Class in dev.civl.gmc.smc: The implementation of the interface StateManager used by SMC.
SimpleStateManager(MatrixDirectedGraph) - Constructor for class dev.civl.gmc.smc.SimpleStateManager
Simulator<STATE,TRANSITION> - Class in dev.civl.gmc: A Simulator is used to execute a transition system using a TransitionChooser to determine which transition to execute from each state.
Simulator(StateManager<STATE, TRANSITION>, PrintStream) - Constructor for class dev.civl.gmc.Simulator
size() - Method in class dev.civl.gmc.dpor.DporSearchStack
SMC - Class in dev.civl.gmc.smc: This is a simple sequential model checker (SMC) implementing general model checker (GMC).
SMC() - Constructor for class dev.civl.gmc.smc.SMC
SMCConstants - Class in dev.civl.gmc.smc
SMCConstants() - Constructor for class dev.civl.gmc.smc.SMCConstants
SMCEnabler - Class in dev.civl.gmc.smc: The implementation of EnablerIF used by SMC.
SMCEnabler(MatrixDirectedGraph) - Constructor for class dev.civl.gmc.smc.SMCEnabler
SMCSimulator - Class in dev.civl.gmc.smc
SMCSimulator(GMCConfiguration, PrintStream) - Constructor for class dev.civl.gmc.smc.SMCSimulator
source() - Method in class dev.civl.gmc.concurrent.StackEntry
source() - Method in class dev.civl.gmc.seq.StackEntry
stack() - Method in class dev.civl.gmc.dpor.DporDfsSearcher: Returns the stack used to perform the depth first search
stack() - Method in class dev.civl.gmc.seq.DfsSearcher: Returns the stack used to perform the depth first search
StackEntry<STATE,TRANSITION> - Class in dev.civl.gmc.concurrent: The stack entry that is going to be pushed onto the stack during the search.
StackEntry<STATE,TRANSITION> - Class in dev.civl.gmc.seq: The stack entry that is going to be pushed onto the stack during the search.
StackEntry(ConcurrentNode<STATE>, Collection<TRANSITION>, boolean) - Constructor for class dev.civl.gmc.concurrent.StackEntry
StackEntry(SequentialNode<STATE>, Collection<TRANSITION>, int) - Constructor for class dev.civl.gmc.seq.StackEntry
stackPos() - Method in exception class dev.civl.gmc.StateSpaceCycleException
StateManager<STATE,TRANSITION> - Class in dev.civl.gmc.seq: A StateManagerIF provides part of a generic interface to a state-transition system.
StateManager() - Constructor for class dev.civl.gmc.seq.StateManager
StatePredicateIF<S> - Interface in dev.civl.gmc: A state predicate is basically a function which returns either true or false at any state in the transition system.
StateSpaceCycleException - Exception Class in dev.civl.gmc: This is the Exception that will be thrown by the DfsSearcher if and only if 1) a cycle in state space detected; and 2) cycle violation is set to be reported.
StateSpaceCycleException(int) - Constructor for exception class dev.civl.gmc.StateSpaceCycleException
STRING - Enum constant in enum class dev.civl.gmc.Option.OptionType
submit(ForkJoinTask<Integer>) - Method in class dev.civl.gmc.concurrent.MyThreadPool
subtract(Collection<? extends Object>, Collection<? extends Object>) - Static method in class dev.civl.gmc.util.Utils

T

top() - Method in class dev.civl.gmc.dpor.DporSearchStack
toString() - Method in class dev.civl.gmc.FalsePredicate: Returns the string "FalsePredicate".
toString() - Method in class dev.civl.gmc.Option: Prints a human-readable description of this option, including its name, type, and default value.
toString() - Method in class dev.civl.gmc.smc.MatrixDirectedGraph
toString() - Method in class dev.civl.gmc.smc.Predicate
toString() - Method in class dev.civl.gmc.smc.TraceStep
toString() - Method in class dev.civl.gmc.Trace
toString() - Method in interface dev.civl.gmc.TraceStepIF
totalNumStatesMatched() - Method in class dev.civl.gmc.concurrent.ConcurrentDfsSearcher: The number of states matched so far.
totalNumStatesSeen() - Method in class dev.civl.gmc.concurrent.ConcurrentDfsSearcher: The number of states seen in this search.
totalNumTransitions() - Method in class dev.civl.gmc.concurrent.ConcurrentDfsSearcher: The number of transitions executed in the course of this search so far.
Trace<TRANSITION,STATE> - Class in dev.civl.gmc: This represents a trace of an execution of a given model.
Trace(String, STATE) - Constructor for class dev.civl.gmc.Trace: Creates a new instance of Trace.
traceStep(int) - Method in class dev.civl.gmc.Trace: Returns the i'th trace step of this trace.
TraceStep - Class in dev.civl.gmc.smc: The implementation of the interface TraceStepIF used by SMC.
TraceStep(String, Integer) - Constructor for class dev.civl.gmc.smc.TraceStep: Construct an instance of TraceStep with given transition and finalState
TraceStepIF<STATE> - Interface in dev.civl.gmc: A TraceStepIF represents the execution result of nextState of StateManagerIF.
traceSteps() - Method in class dev.civl.gmc.Trace: Returns the list of trace steps contained in this trace.
TransitionChooser<STATE,TRANSITION> - Interface in dev.civl.gmc: General interface for an object which can select one enabled transition from the set of enabled transitions at any state.
TRUE - Enum constant in enum class dev.civl.gmc.concurrent.ProvisoValue
tryNextState(Integer, String) - Method in class dev.civl.gmc.smc.SimpleStateManager
tryNextState(STATE, TRANSITION) - Method in class dev.civl.gmc.seq.StateManager: Same as StateManager.nextState(STATE,TRANSITION) except if an error is encountered then it is not reported and null is returned
type() - Method in class dev.civl.gmc.Option: Returns the type of this option

U

unboundDepth() - Method in class dev.civl.gmc.seq.DfsSearcher
UNKNOWN - Enum constant in enum class dev.civl.gmc.concurrent.ProvisoValue
Utils - Class in dev.civl.gmc.util
Utils() - Constructor for class dev.civl.gmc.util.Utils

V

valueOf(String) - Static method in enum class dev.civl.gmc.concurrent.ProvisoValue: Returns the enum constant of this class with the specified name.
valueOf(String) - Static method in enum class dev.civl.gmc.Option.OptionType: Returns the enum constant of this class with the specified name.
values() - Static method in enum class dev.civl.gmc.concurrent.ProvisoValue: Returns an array containing the constants of this enum class, in the order they are declared.
values() - Static method in enum class dev.civl.gmc.Option.OptionType: Returns an array containing the constants of this enum class, in the order they are declared.
violation() - Method in class dev.civl.gmc.Trace: Returns true iff a least one violations have been encountered.

W

writeStack(PrintStream) - Method in class dev.civl.gmc.dpor.DporDfsSearcher: Write the state of the current stack in a condensed form that can be used to replay the trace later.
writeStack(PrintStream) - Method in class dev.civl.gmc.seq.DfsSearcher: Write the state of the current stack in a condensed form that can be used to replay the trace later.

A B C D E F G H I L M N O P R S T U V W
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form