Index (API for GMC trunk r367)

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

addFreeArg(String) - Method in class edu.udel.cis.vsl.gmc.GMCSection: Adds a free argument to the list of free arguments associated to this configuration.
addSection(GMCSection) - Method in class edu.udel.cis.vsl.gmc.GMCConfiguration: Adds a section to the NON-anonymous section map.
addTraceStep(TraceStepIF<STATE>) - Method in class edu.udel.cis.vsl.gmc.Trace: Adds a new trace step to this trace.
allTransitions(Integer) - Method in class edu.udel.cis.vsl.gmc.smc.MatrixDirectedGraph: Get all outgoing transitions from the given source state to all other states in this graph.
ampleSet(Integer) - Method in class edu.udel.cis.vsl.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 edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.GMCConfiguration: The reserved name of the anonymous GMCSection of a configuration.

B

BOOLEAN - Enum constant in enum class edu.udel.cis.vsl.gmc.Option.OptionType
boundDepth(int) - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher

C

checkStackTrace(StackEntry<STATE, TRANSITION>) - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher
chooseEnabledTransition(STATE) - Method in class edu.udel.cis.vsl.gmc.GuidedTransitionChooser
chooseEnabledTransition(STATE) - Method in class edu.udel.cis.vsl.gmc.RandomTransitionChooser
chooseEnabledTransition(STATE) - Method in interface edu.udel.cis.vsl.gmc.TransitionChooser: Using some protocol, chooses one of the transitions enabled at the given state.
clone() - Method in class edu.udel.cis.vsl.gmc.GMCConfiguration: Returns a deep copy of this configuration.
clone() - Method in class edu.udel.cis.vsl.gmc.GMCSection: Returns a deep copy of this configuration.
CommandLineException - Exception in edu.udel.cis.vsl.gmc: An exception that is thrown if the command line arguments are not formatted correctly.
CommandLineException(String) - Constructor for exception edu.udel.cis.vsl.gmc.CommandLineException: Constructs new instance with given message.
CommandLineParser - Class in edu.udel.cis.vsl.gmc: A tool for parsing a command line and generating a GMCConfiguration.
CommandLineParser(Collection<Option>) - Constructor for class edu.udel.cis.vsl.gmc.CommandLineParser: Constructs a new parser from the given collection of options.
compareTo(LogEntry) - Method in class edu.udel.cis.vsl.gmc.LogEntry: Compares this with another log entry in the natural order.
ConcurrentDfsSearcher<STATE,TRANSITION> - Class in edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.concurrent.ConcurrentDfsSearcher
ConcurrentNode<STATE> - Class in edu.udel.cis.vsl.gmc.concurrent
ConcurrentNode(STATE) - Constructor for class edu.udel.cis.vsl.gmc.concurrent.ConcurrentNode
ConcurrentNodeFactory<STATE,TRANSITION> - Class in edu.udel.cis.vsl.gmc.concurrent
ConcurrentNodeFactory(ConcurrentStateManagerIF<STATE, TRANSITION>) - Constructor for class edu.udel.cis.vsl.gmc.concurrent.ConcurrentNodeFactory
ConcurrentStateManagerIF<STATE,TRANSITION> - Class in edu.udel.cis.vsl.gmc.concurrent: A ConcurrentStateManager is used by a ConcurrentDfsSearcher which encapsulates all methods that are needed by ConcurrentDfsSearcher on STATE.
ConcurrentStateManagerIF() - Constructor for class edu.udel.cis.vsl.gmc.concurrent.ConcurrentStateManagerIF
currentState() - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher: Returns the state at the top of the stack, without modifying the stack.
cycleFound() - Method in class edu.udel.cis.vsl.gmc.concurrent.ConcurrentDfsSearcher
cycleFound() - Method in class edu.udel.cis.vsl.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

debugging() - Method in interface edu.udel.cis.vsl.gmc.seq.EnablerIF: Returns the current value of the debugging flag.
debugging() - Method in class edu.udel.cis.vsl.gmc.smc.SMCEnabler
decrementTotal() - Method in class edu.udel.cis.vsl.gmc.concurrent.MyThreadPool
decrementWaiting() - Method in class edu.udel.cis.vsl.gmc.concurrent.MyThreadPool: Decrease the counter for waiting threads.
defaultValue() - Method in class edu.udel.cis.vsl.gmc.Option: Returns the default value for this option
description() - Method in class edu.udel.cis.vsl.gmc.Option: Returns the human-readable description of this option.
DfsSearcher<STATE,TRANSITION> - Class in edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.seq.DfsSearcher
DfsSearcher(EnablerIF<STATE, TRANSITION>, StateManager<STATE, TRANSITION>, StatePredicateIF<STATE>, GMCConfiguration, PrintStream) - Constructor for class edu.udel.cis.vsl.gmc.seq.DfsSearcher: Constructs a new depth first search searcher.
DOUBLE - Enum constant in enum class edu.udel.cis.vsl.gmc.Option.OptionType

E

edu.udel.cis.vsl.gmc - package edu.udel.cis.vsl.gmc: The root package of generic model checking is used to construct model checking applications, either sequential or concurrent.
edu.udel.cis.vsl.gmc.concurrent - package edu.udel.cis.vsl.gmc.concurrent: This package provides concurrent generic model checking functionality.
edu.udel.cis.vsl.gmc.seq - package edu.udel.cis.vsl.gmc.seq: This package provides sequential generic model checking functionality.
edu.udel.cis.vsl.gmc.smc - package edu.udel.cis.vsl.gmc.smc: A simple implementation of General Model Checker (GMC) is used by a set of code coverage test cases.
edu.udel.cis.vsl.gmc.util - package edu.udel.cis.vsl.gmc.util: The utility package for GMC, providing a set of utility classes and functions used by GMC.
EnablerIF<STATE,TRANSITION> - Interface in edu.udel.cis.vsl.gmc.seq: An EnablerIF tells you which transitions should be explored from a given state.
equals(Object) - Method in class edu.udel.cis.vsl.gmc.LogEntry: Determines whether this log entry is equal to the given object.
equals(Object) - Method in class edu.udel.cis.vsl.gmc.Option
errorBound() - Method in class edu.udel.cis.vsl.gmc.ErrorLog
ErrorLog - Class in edu.udel.cis.vsl.gmc: A log for recording errors and corresponding traces encountered during a model checking run.
ErrorLog(File, String, PrintStream) - Constructor for class edu.udel.cis.vsl.gmc.ErrorLog: Creates new ErrorLog.
ExcessiveErrorException - Exception in edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.ExcessiveErrorException: Constructs new instance with given numErrors.
existingTransitions(Integer) - Method in class edu.udel.cis.vsl.gmc.smc.MatrixDirectedGraph: Get all existing outgoing transitions from the given sourceState in this graph.
explanation() - Method in class edu.udel.cis.vsl.gmc.FalsePredicate: Returns the string "The false predicate is always false."
explanation() - Method in class edu.udel.cis.vsl.gmc.smc.Predicate
explanation() - Method in interface edu.udel.cis.vsl.gmc.StatePredicateIF: Returns a human-readable explanation of why the predicate does or does not hold, after method StatePredicateIF.holdsAt(S) has been called.

F

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

G

getActiveNum() - Method in class edu.udel.cis.vsl.gmc.concurrent.MyThreadPool
getAllOptions() - Static method in class edu.udel.cis.vsl.gmc.smc.SMCConstants
getAnonymousSection() - Method in class edu.udel.cis.vsl.gmc.GMCConfiguration: Returns the anonymous section
getChildrenThreadsCounter() - Method in class edu.udel.cis.vsl.gmc.concurrent.StackEntry
getConfiguration() - Method in class edu.udel.cis.vsl.gmc.LogEntry: Returns the configuration which will be used to replay the trace.
getDebugOut() - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher: Returns the stream used to print debugging output when the debugging flag is on.
getDebugOut() - Method in interface edu.udel.cis.vsl.gmc.seq.EnablerIF: Returns the debugging output stream.
getDebugOut() - Method in class edu.udel.cis.vsl.gmc.smc.SMCEnabler
getDepth() - Method in class edu.udel.cis.vsl.gmc.seq.SequentialNode
getDestState(Integer, String) - Method in class edu.udel.cis.vsl.gmc.smc.MatrixDirectedGraph: Find the destination state with the given sourceState and transition.
getDirectory() - Method in class edu.udel.cis.vsl.gmc.ErrorLog: Returns the directory in which trace files and the log will be stored.
getExpand() - Method in class edu.udel.cis.vsl.gmc.concurrent.StackEntry
getExpand() - Method in class edu.udel.cis.vsl.gmc.seq.SequentialNode
getFinalState() - Method in class edu.udel.cis.vsl.gmc.smc.TraceStep
getFinalState() - Method in interface edu.udel.cis.vsl.gmc.TraceStepIF: Returns the resulting state of the trace step.
getFreeArg(int) - Method in class edu.udel.cis.vsl.gmc.GMCSection: Returns the i-th free argument, indexed from 0.
getFullyExpanded() - Method in class edu.udel.cis.vsl.gmc.seq.SequentialNode
getId() - Method in class edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.seq.SequentialNode
getId(Integer) - Method in class edu.udel.cis.vsl.gmc.smc.SimpleStateManager
getId(STATE) - Method in class edu.udel.cis.vsl.gmc.seq.StateManager: Get the id of a normalizedState.
getInitialNode(STATE) - Method in class edu.udel.cis.vsl.gmc.seq.SequentialNodeFactory: Get the SequentialNode associated with the initial state.
getLength() - Method in class edu.udel.cis.vsl.gmc.GuidedTransitionChooser: Returns the length of this execution.
getLength() - Method in class edu.udel.cis.vsl.gmc.LogEntry: Returns the length of the trace.
getLog() - Method in class edu.udel.cis.vsl.gmc.Simulator
getLogFile() - Method in class edu.udel.cis.vsl.gmc.ErrorLog
getMapEntry(Option, String) - Method in class edu.udel.cis.vsl.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 edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.concurrent.MyThreadPool
getMinimalCounterexampleSize() - Method in class edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.concurrent.ConcurrentDfsSearcher
getMinimize() - Method in class edu.udel.cis.vsl.gmc.ErrorLog: Are we searching for a minimal counterexample?
getMinimize() - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher
getMinimumSuccessorStackIndex() - Method in class edu.udel.cis.vsl.gmc.concurrent.StackEntry
getMinimumSuccessorStackIndex() - Method in class edu.udel.cis.vsl.gmc.seq.StackEntry
getName() - Method in class edu.udel.cis.vsl.gmc.GMCSection: Returns the name of this section.
getNode() - Method in class edu.udel.cis.vsl.gmc.concurrent.StackEntry
getNode() - Method in class edu.udel.cis.vsl.gmc.seq.StackEntry
getNode(TraceStepIF<STATE>) - Method in class edu.udel.cis.vsl.gmc.seq.SequentialNodeFactory: Implements the fly-weight pattern and normalize a state.
getNode(STATE) - Method in class edu.udel.cis.vsl.gmc.concurrent.ConcurrentNodeFactory: Implements the fly-weight pattern.
getNode(STATE) - Method in class edu.udel.cis.vsl.gmc.seq.SequentialNodeFactory: Get the node associated to the given state, null there is no such a node.
getNumFreeArgs() - Method in class edu.udel.cis.vsl.gmc.GMCSection: Returns the current number of free arguments associated to this configuration.
getNumSections() - Method in class edu.udel.cis.vsl.gmc.GMCConfiguration: Returns the number of NON-anonymous sections.
getOption(String) - Method in class edu.udel.cis.vsl.gmc.GMCConfiguration: Returns the option with the given name associated to this configuration, or null if there is none.
getOptions() - Method in class edu.udel.cis.vsl.gmc.GMCConfiguration: Returns the set of options associated to this configuration.
getPid(String) - Method in class edu.udel.cis.vsl.gmc.smc.SimpleStateManager
getPid(TRANSITION) - Method in class edu.udel.cis.vsl.gmc.seq.StateManager: Gets the ID number of the process that is responsible for executing transition.
getPredicate() - Method in class edu.udel.cis.vsl.gmc.Simulator
getPreemptionPid() - Method in class edu.udel.cis.vsl.gmc.seq.StackEntry: If this step is preemptible, this method returns the PID of the process that executed the previous transition.
getPrintAllStates() - Method in class edu.udel.cis.vsl.gmc.Simulator
getProviso() - Method in class edu.udel.cis.vsl.gmc.concurrent.ConcurrentNode
getRunningNum() - Method in class edu.udel.cis.vsl.gmc.concurrent.MyThreadPool
getSaveStates() - Method in class edu.udel.cis.vsl.gmc.GMCConfiguration
getSection(String) - Method in class edu.udel.cis.vsl.gmc.GMCConfiguration: Returns the section with the given name, or null if there is none.
getSections() - Method in class edu.udel.cis.vsl.gmc.GMCConfiguration: Returns an iterable object of the NON-anonymous sections.
getSeed() - Method in class edu.udel.cis.vsl.gmc.RandomTransitionChooser
getSeen() - Method in class edu.udel.cis.vsl.gmc.seq.SequentialNode: Returns the value of the seen flag associated to the given state.
getStackPosition() - Method in class edu.udel.cis.vsl.gmc.seq.SequentialNode: Get the position of this SequentialNode on dfs stack or -1 if it is not on stack.
getState() - Method in class edu.udel.cis.vsl.gmc.concurrent.ConcurrentNode
getState() - Method in class edu.udel.cis.vsl.gmc.concurrent.StackEntry
getState() - Method in class edu.udel.cis.vsl.gmc.seq.SequentialNode
getState() - Method in class edu.udel.cis.vsl.gmc.seq.StackEntry
getTid() - Method in class edu.udel.cis.vsl.gmc.concurrent.StackEntry
getTid() - Method in class edu.udel.cis.vsl.gmc.seq.StackEntry
getTraceFile() - Method in class edu.udel.cis.vsl.gmc.LogEntry: Returns the file to which the trace is saved.
getTransitionIterator() - Method in class edu.udel.cis.vsl.gmc.concurrent.StackEntry
getTransitionIterator() - Method in class edu.udel.cis.vsl.gmc.seq.StackEntry
getTransitions() - Method in class edu.udel.cis.vsl.gmc.concurrent.StackEntry
getTransitions() - Method in class edu.udel.cis.vsl.gmc.seq.StackEntry
getValue(Option) - Method in class edu.udel.cis.vsl.gmc.GMCSection: Gets the value associated to an option or null if no value is associated to that option.
getValueOrDefault(Option) - Method in class edu.udel.cis.vsl.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 edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.GMCConfiguration: Constructs new configuration with the set of options obtained from the given collection.
GMCSection - Class in edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.GMCSection: Constructs a new instance of GMCSection with the given GMCConfiguration and name.
GMCSection(String) - Constructor for class edu.udel.cis.vsl.gmc.GMCSection: Constructs a new GMCSection with the given name
GuidedTransitionChooser<STATE,TRANSITION> - Class in edu.udel.cis.vsl.gmc: Transition Chooser which makes its choice using an explicit "guide".
GuidedTransitionChooser(EnablerIF<STATE, TRANSITION>, GuidedTransitionChooser.Guide) - Constructor for class edu.udel.cis.vsl.gmc.GuidedTransitionChooser
GuidedTransitionChooser(EnablerIF<STATE, TRANSITION>, File) - Constructor for class edu.udel.cis.vsl.gmc.GuidedTransitionChooser

H

hashCode() - Method in class edu.udel.cis.vsl.gmc.Option
hasNext() - Method in class edu.udel.cis.vsl.gmc.concurrent.StackEntry
hasNext() - Method in class edu.udel.cis.vsl.gmc.seq.StackEntry
holdsAt(Integer) - Method in class edu.udel.cis.vsl.gmc.smc.Predicate: Does this predicate hold at the given state?
holdsAt(S) - Method in class edu.udel.cis.vsl.gmc.FalsePredicate: Returns false.
holdsAt(S) - Method in interface edu.udel.cis.vsl.gmc.StatePredicateIF: Does this predicate hold at the given state?

I

incrementCounter() - Method in class edu.udel.cis.vsl.gmc.concurrent.StackEntry
incrementTotal() - Method in class edu.udel.cis.vsl.gmc.concurrent.MyThreadPool
incrementWaiting() - Method in class edu.udel.cis.vsl.gmc.concurrent.MyThreadPool: Increase the counter for waiting threads.
init() - Method in class edu.udel.cis.vsl.gmc.Trace: Returns the initial state of this trace.
INTEGER - Enum constant in enum class edu.udel.cis.vsl.gmc.Option.OptionType
isDepthBounded() - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher
isFull() - Method in class edu.udel.cis.vsl.gmc.concurrent.StackEntry
isPreemptible() - Method in class edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.concurrent.MyThreadPool
isQuiet() - Method in class edu.udel.cis.vsl.gmc.GMCConfiguration
isQuiet() - Method in class edu.udel.cis.vsl.gmc.Simulator
isTrue(Option) - Method in class edu.udel.cis.vsl.gmc.GMCSection: Determines whether the value associated to a boolean option should be construed as true in most circumstances.

L

lastState() - Method in class edu.udel.cis.vsl.gmc.Trace: Returns the last state of this trace.
left - Variable in class edu.udel.cis.vsl.gmc.util.Pair
LogEntry - Class in edu.udel.cis.vsl.gmc: An entry in an error log.
LogEntry(GMCConfiguration) - Constructor for class edu.udel.cis.vsl.gmc.LogEntry: Default construtor: does nothing.

M

makeGuide(BufferedReader) - Static method in class edu.udel.cis.vsl.gmc.GuidedTransitionChooser: Creates a guide by parsing from the given buffered reader.
makeGuide(File) - Static method in class edu.udel.cis.vsl.gmc.GuidedTransitionChooser: Creates a guide by parsing a file which is a newline-separated list of integers.
MAP - Enum constant in enum class edu.udel.cis.vsl.gmc.Option.OptionType
MatrixDirectedGraph - Class in edu.udel.cis.vsl.gmc.smc: A simple directed graph implemented with a square matrix.
MatrixDirectedGraph(String[][]) - Constructor for class edu.udel.cis.vsl.gmc.smc.MatrixDirectedGraph: Constructs a MatrixDirectedGraph with given squareMatrix.
MisguidedExecutionException - Exception in edu.udel.cis.vsl.gmc
MisguidedExecutionException(String) - Constructor for exception edu.udel.cis.vsl.gmc.MisguidedExecutionException
MyThreadPool - Class in edu.udel.cis.vsl.gmc.concurrent: The threadPool That is used to manage the threads used in the algorithm.
MyThreadPool() - Constructor for class edu.udel.cis.vsl.gmc.concurrent.MyThreadPool
MyThreadPool(int) - Constructor for class edu.udel.cis.vsl.gmc.concurrent.MyThreadPool

N

name() - Method in class edu.udel.cis.vsl.gmc.concurrent.ConcurrentDfsSearcher
name() - Method in class edu.udel.cis.vsl.gmc.Option: Returns the name of this option.
name() - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher
name() - Method in class edu.udel.cis.vsl.gmc.Trace: Returns the name of this trace.
newConfig() - Method in class edu.udel.cis.vsl.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 edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.Option
newStackEntry(ConcurrentNode<STATE>, Collection<TRANSITION>, boolean) - Method in class edu.udel.cis.vsl.gmc.concurrent.ConcurrentNodeFactory: Construct a new stack entry which will be pushed onto the stack.
newStackEntry(SequentialNode<STATE>, Collection<TRANSITION>, int) - Method in class edu.udel.cis.vsl.gmc.seq.SequentialNodeFactory: Construct a new stack entry which will be pushed onto the stack.
next() - Method in class edu.udel.cis.vsl.gmc.concurrent.StackEntry
next() - Method in class edu.udel.cis.vsl.gmc.seq.StackEntry
nextState(Integer, String) - Method in class edu.udel.cis.vsl.gmc.smc.SimpleStateManager
nextState(STATE, TRANSITION) - Method in class edu.udel.cis.vsl.gmc.seq.StateManager: Given a state and a transition, returns the trace step after executing the transition at the given state.
normalize(TraceStepIF<Integer>) - Method in class edu.udel.cis.vsl.gmc.smc.SimpleStateManager
normalize(TraceStepIF<STATE>) - Method in class edu.udel.cis.vsl.gmc.seq.StateManager: Normalize/simplify a state.
normalize(STATE) - Method in class edu.udel.cis.vsl.gmc.concurrent.ConcurrentStateManagerIF
numEntries() - Method in class edu.udel.cis.vsl.gmc.ErrorLog
numErrors() - Method in class edu.udel.cis.vsl.gmc.ErrorLog
numErrors() - Method in exception edu.udel.cis.vsl.gmc.ExcessiveErrorException: Returns the number of errors encountered when this exception was thrown
numOfSearchNodeSaved() - Method in class edu.udel.cis.vsl.gmc.concurrent.ConcurrentNodeFactory
numOfSearchNodeSaved() - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher
numOfSearchNodeSaved() - Method in class edu.udel.cis.vsl.gmc.seq.SequentialNodeFactory
numOfSteps() - Method in class edu.udel.cis.vsl.gmc.Trace: Returns the number of trace steps in this trace.
numStatesMatched() - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher: The number of states matched so far.
numStatesSeen() - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher: The number of states seen in this search.
numTransitions() - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher: The number of transitions executed in the course of this search so far.

O

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

P

Pair<L,R> - Class in edu.udel.cis.vsl.gmc.util
Pair(L, R) - Constructor for class edu.udel.cis.vsl.gmc.util.Pair
parse(GMCConfiguration, BufferedReader) - Method in class edu.udel.cis.vsl.gmc.CommandLineParser: Parses the reader, interpreting lines as command line args, modifying given configuration accordingly.
parse(GMCConfiguration, File) - Method in class edu.udel.cis.vsl.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 edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.CommandLineParser: Given a collection of strings, parses them in the order of their iterator to produce a new configuration.
peek() - Method in class edu.udel.cis.vsl.gmc.concurrent.StackEntry
peek() - Method in class edu.udel.cis.vsl.gmc.seq.StackEntry
play(STATE[], boolean[], String[], TransitionChooser<STATE, TRANSITION>, boolean) - Method in class edu.udel.cis.vsl.gmc.Simulator: Plays the trace.
play(STATE, TransitionChooser<STATE, TRANSITION>, boolean) - Method in class edu.udel.cis.vsl.gmc.Simulator
play(STATE, STATE, boolean, TransitionChooser<STATE, TRANSITION>, boolean) - Method in class edu.udel.cis.vsl.gmc.Simulator
predicate() - Method in class edu.udel.cis.vsl.gmc.concurrent.ConcurrentDfsSearcher
predicate() - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher
Predicate - Class in edu.udel.cis.vsl.gmc.smc: The predicate used for detecting violation state defined in the given list states.
Predicate(Integer...) - Constructor for class edu.udel.cis.vsl.gmc.smc.Predicate
print(PrintStream) - Method in class edu.udel.cis.vsl.gmc.ErrorLog
print(PrintStream) - Method in class edu.udel.cis.vsl.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 edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.LogEntry: Prints this log entry to the given stream.
print(PrintStream) - Method in class edu.udel.cis.vsl.gmc.Option
printAllStatesLong(PrintStream) - Method in class edu.udel.cis.vsl.gmc.seq.StateManager: Prints out all the states, in long form, currently "held" by this manager.
printAllStatesLong(PrintStream) - Method in class edu.udel.cis.vsl.gmc.smc.SimpleStateManager
printAllStatesShort(PrintStream) - Method in class edu.udel.cis.vsl.gmc.seq.StateManager: Prints out all the states, in short form, currently "held" by this manager.
printAllStatesShort(PrintStream) - Method in class edu.udel.cis.vsl.gmc.smc.SimpleStateManager
printBody(PrintStream) - Method in class edu.udel.cis.vsl.gmc.LogEntry: Prints an explanation of the error.
printStack(PrintStream) - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher: Prints the whole stack in a human readable form to the given stream.
printStack(PrintStream, boolean, boolean) - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher: Prints the current stack in a human-readable format.
printStateLong(PrintStream, Integer) - Method in class edu.udel.cis.vsl.gmc.smc.SimpleStateManager
printStateLong(PrintStream, STATE) - Method in class edu.udel.cis.vsl.gmc.seq.StateManager: Prints out a long human-readable representation of the state.
printStateShort(PrintStream, Integer) - Method in class edu.udel.cis.vsl.gmc.smc.SimpleStateManager
printStateShort(PrintStream, STATE) - Method in class edu.udel.cis.vsl.gmc.seq.StateManager: Prints out a short human-readable representation of the state.
printSummary(PrintStream) - Method in class edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.smc.SimpleStateManager
printTraceStep(STATE, TraceStepIF<STATE>) - Method in class edu.udel.cis.vsl.gmc.seq.StateManager: This method should print the source state id and transitions within this traceStep.
printTraceStepFinalState(Integer, int) - Method in class edu.udel.cis.vsl.gmc.smc.SimpleStateManager
printTraceStepFinalState(STATE, int) - Method in class edu.udel.cis.vsl.gmc.seq.StateManager: This method should print the final state of a trace step.
printTransitionLong(PrintStream, String) - Method in class edu.udel.cis.vsl.gmc.smc.SimpleStateManager
printTransitionLong(PrintStream, TRANSITION) - Method in class edu.udel.cis.vsl.gmc.seq.StateManager: Prints out a long human-readable representation of the transition.
printTransitions() - Method in class edu.udel.cis.vsl.gmc.GMCConfiguration
printTransitionShort(PrintStream, String) - Method in class edu.udel.cis.vsl.gmc.smc.SimpleStateManager
printTransitionShort(PrintStream, TRANSITION) - Method in class edu.udel.cis.vsl.gmc.seq.StateManager: Prints out a short human-readable representation of the transition.
printUsage(PrintStream) - Method in class edu.udel.cis.vsl.gmc.CommandLineParser: Prints the list of options in a human-readable format.
proceedToNewState() - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher: Proceeds with the search until we arrive at a state that has not been seen before (assuming there is one).
ProvisoValue - Enum Class in edu.udel.cis.vsl.gmc.concurrent: This enumeration stores the result of checking "stack proviso" of a STATE in the STATE-TRANSITION system.
putMapEntry(Option, String, Object) - Method in class edu.udel.cis.vsl.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 edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.RandomTransitionChooser
RandomTransitionChooser(EnablerIF<STATE, TRANSITION>, long) - Constructor for class edu.udel.cis.vsl.gmc.RandomTransitionChooser
read(GMCConfiguration) - Method in class edu.udel.cis.vsl.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 edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.ErrorLog
reportCycleAsViolation() - Method in class edu.udel.cis.vsl.gmc.concurrent.ConcurrentDfsSearcher
reportCycleAsViolation() - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher
restrictDepth() - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher: Sets the depth bound to one less than the current stack size.
result() - Method in class edu.udel.cis.vsl.gmc.Trace: Returns the verification result of this trace.
right - Variable in class edu.udel.cis.vsl.gmc.util.Pair
run(MatrixDirectedGraph, StatePredicateIF<Integer>) - Method in class edu.udel.cis.vsl.gmc.smc.SMCSimulator
run(MatrixDirectedGraph, StatePredicateIF<Integer>, GMCConfiguration) - Method in class edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.smc.SMCSimulator
run(MatrixDirectedGraph, StatePredicateIF<Integer>, Integer, GMCConfiguration) - Method in class edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.ErrorLog
search() - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher: Resumes a depth-first search of the state space starting from the current state.
search(STATE) - Method in class edu.udel.cis.vsl.gmc.concurrent.ConcurrentDfsSearcher: Start a concurrent dfs task from a given state
search(STATE) - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher: Performs a depth-first search starting from the given state.
searcher() - Method in class edu.udel.cis.vsl.gmc.ErrorLog
SequentialNode<STATE> - Class in edu.udel.cis.vsl.gmc.seq: A Node in the state graph for the sequential depth first search.
SequentialNode(STATE, int) - Constructor for class edu.udel.cis.vsl.gmc.seq.SequentialNode
SequentialNodeFactory<STATE,TRANSITION> - Class in edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.seq.SequentialNodeFactory
setAnonymousSection(GMCSection) - Method in class edu.udel.cis.vsl.gmc.GMCConfiguration: Updates the anonymous section with the given section.
setConfiguration(GMCConfiguration) - Method in class edu.udel.cis.vsl.gmc.GMCSection: Updates the configuration associates with this section.
setDebug(boolean) - Method in class edu.udel.cis.vsl.gmc.smc.SMC: Set SMC to print debugging info, iff isDebug is true
setDebugging(boolean) - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher: Set the debugging flag to the given value.
setDebugging(boolean) - Method in interface edu.udel.cis.vsl.gmc.seq.EnablerIF: Set the debugging flag to the given value.
setDebugging(boolean) - Method in class edu.udel.cis.vsl.gmc.smc.SMCEnabler
setDebugOut(PrintStream) - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher: Sets the debugging output stream to the given stream.
setDebugOut(PrintStream) - Method in interface edu.udel.cis.vsl.gmc.seq.EnablerIF: Set the debugging output stream to the given stream.
setDebugOut(PrintStream) - Method in class edu.udel.cis.vsl.gmc.smc.SMCEnabler
setDepth(int) - Method in class edu.udel.cis.vsl.gmc.seq.SequentialNode: Set SequentialNode.depth to a given value.
setErrorBound(int) - Method in class edu.udel.cis.vsl.gmc.ErrorLog
setExpand(boolean) - Method in class edu.udel.cis.vsl.gmc.concurrent.StackEntry
setExpand(boolean) - Method in class edu.udel.cis.vsl.gmc.seq.SequentialNode: Set SequentialNode.expand to a given value.
setFull(boolean) - Method in class edu.udel.cis.vsl.gmc.concurrent.StackEntry
setFullyExpanded(boolean) - Method in class edu.udel.cis.vsl.gmc.seq.SequentialNode: Set SequentialNode.fullyExpanded to a certain value.
setFullyExplored(boolean) - Method in class edu.udel.cis.vsl.gmc.concurrent.ConcurrentNode: Set "fullyExplored" field of a STATE to a certain boolean value.
setLog(ErrorLog) - Method in class edu.udel.cis.vsl.gmc.Simulator
setMapValue(Option, Map<String, Object>) - Method in class edu.udel.cis.vsl.gmc.GMCSection: Sets map value or removes map entry from this configuration.
setMinimize(boolean) - Method in class edu.udel.cis.vsl.gmc.concurrent.ConcurrentDfsSearcher
setMinimize(boolean) - Method in class edu.udel.cis.vsl.gmc.ErrorLog: Sets the minimize flag to given value.
setMinimize(boolean) - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher
setMinimumSuccessorStackIndex(int) - Method in class edu.udel.cis.vsl.gmc.concurrent.StackEntry
setMinimumSuccessorStackIndex(int) - Method in class edu.udel.cis.vsl.gmc.seq.StackEntry
setName(String) - Method in class edu.udel.cis.vsl.gmc.concurrent.ConcurrentDfsSearcher
setName(String) - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher
setPredicate(StatePredicateIF<STATE>) - Method in class edu.udel.cis.vsl.gmc.Simulator
setPreemptionBound(int) - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher
setPreemptionPid(int) - Method in class edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.Simulator
setPrintStream(PrintStream) - Method in class edu.udel.cis.vsl.gmc.GMCConfiguration
setPrintTransition(boolean) - Method in class edu.udel.cis.vsl.gmc.GMCConfiguration
setQuiet(boolean) - Method in class edu.udel.cis.vsl.gmc.GMCConfiguration
setQuiet(boolean) - Method in class edu.udel.cis.vsl.gmc.Simulator
setReportCycleAsViolation(boolean) - Method in class edu.udel.cis.vsl.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 edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.GMCConfiguration
setScalarValue(Option, Object) - Method in class edu.udel.cis.vsl.gmc.GMCSection: Adds the key-value pair for a scalar value to the parameter map.
setSearcher(DfsSearcher<?, ?>) - Method in class edu.udel.cis.vsl.gmc.ErrorLog
setSeen(boolean) - Method in class edu.udel.cis.vsl.gmc.seq.SequentialNode: Sets the "seen flag" to a given value.
setSequentialNodeFactory(SequentialNodeFactory<STATE, TRANSITION>) - Method in class edu.udel.cis.vsl.gmc.seq.StateManager
setStackPosition(int) - Method in class edu.udel.cis.vsl.gmc.seq.SequentialNode: Set the stack position field of the SequentialNode.
setViolation(boolean) - Method in class edu.udel.cis.vsl.gmc.Trace: Updates the flag of violation.
shutdown() - Method in class edu.udel.cis.vsl.gmc.concurrent.MyThreadPool
SimpleStateManager - Class in edu.udel.cis.vsl.gmc.smc: The implementation of the interface StateManager used by SMC.
SimpleStateManager(MatrixDirectedGraph) - Constructor for class edu.udel.cis.vsl.gmc.smc.SimpleStateManager
Simulator<STATE,TRANSITION> - Class in edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.Simulator
SMC - Class in edu.udel.cis.vsl.gmc.smc: This is a simple sequential model checker (SMC) implementing general model checker (GMC).
SMC() - Constructor for class edu.udel.cis.vsl.gmc.smc.SMC
SMCConstants - Class in edu.udel.cis.vsl.gmc.smc
SMCConstants() - Constructor for class edu.udel.cis.vsl.gmc.smc.SMCConstants
SMCEnabler - Class in edu.udel.cis.vsl.gmc.smc: The implementation of EnablerIF used by SMC.
SMCEnabler(MatrixDirectedGraph) - Constructor for class edu.udel.cis.vsl.gmc.smc.SMCEnabler
SMCSimulator - Class in edu.udel.cis.vsl.gmc.smc
SMCSimulator(GMCConfiguration, PrintStream) - Constructor for class edu.udel.cis.vsl.gmc.smc.SMCSimulator
source() - Method in class edu.udel.cis.vsl.gmc.concurrent.StackEntry
source() - Method in class edu.udel.cis.vsl.gmc.seq.StackEntry
stack() - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher: Returns the stack used to perform the depth first search
StackEntry<STATE,TRANSITION> - Class in edu.udel.cis.vsl.gmc.concurrent: The stack entry that is going to be pushed onto the stack during the search.
StackEntry<STATE,TRANSITION> - Class in edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.concurrent.StackEntry
StackEntry(SequentialNode<STATE>, Collection<TRANSITION>, int) - Constructor for class edu.udel.cis.vsl.gmc.seq.StackEntry
stackPos() - Method in exception edu.udel.cis.vsl.gmc.StateSpaceCycleException
StateManager<STATE,TRANSITION> - Class in edu.udel.cis.vsl.gmc.seq: A StateManagerIF provides part of a generic interface to a state-transition system.
StateManager() - Constructor for class edu.udel.cis.vsl.gmc.seq.StateManager
StatePredicateIF<S> - Interface in edu.udel.cis.vsl.gmc: A state predicate is basically a function which returns either true or false at any state in the transition system.
StateSpaceCycleException - Exception in edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.StateSpaceCycleException
STRING - Enum constant in enum class edu.udel.cis.vsl.gmc.Option.OptionType
submit(ForkJoinTask<Integer>) - Method in class edu.udel.cis.vsl.gmc.concurrent.MyThreadPool
subtract(Collection<? extends Object>, Collection<? extends Object>) - Static method in class edu.udel.cis.vsl.gmc.util.Utils

T

toString() - Method in class edu.udel.cis.vsl.gmc.FalsePredicate: Returns the string "FalsePredicate".
toString() - Method in class edu.udel.cis.vsl.gmc.Option: Prints a human-readable description of this option, including its name, type, and default value.
toString() - Method in class edu.udel.cis.vsl.gmc.smc.MatrixDirectedGraph
toString() - Method in class edu.udel.cis.vsl.gmc.smc.Predicate
toString() - Method in class edu.udel.cis.vsl.gmc.smc.TraceStep
toString() - Method in class edu.udel.cis.vsl.gmc.Trace
toString() - Method in interface edu.udel.cis.vsl.gmc.TraceStepIF
totalNumStatesMatched() - Method in class edu.udel.cis.vsl.gmc.concurrent.ConcurrentDfsSearcher: The number of states matched so far.
totalNumStatesSeen() - Method in class edu.udel.cis.vsl.gmc.concurrent.ConcurrentDfsSearcher: The number of states seen in this search.
totalNumTransitions() - Method in class edu.udel.cis.vsl.gmc.concurrent.ConcurrentDfsSearcher: The number of transitions executed in the course of this search so far.
Trace<TRANSITION,STATE> - Class in edu.udel.cis.vsl.gmc: This represents a trace of an execution of a given model.
Trace(String, STATE) - Constructor for class edu.udel.cis.vsl.gmc.Trace: Creates a new instance of Trace.
traceStep(int) - Method in class edu.udel.cis.vsl.gmc.Trace: Returns the i'th trace step of this trace.
TraceStep - Class in edu.udel.cis.vsl.gmc.smc: The implementation of the interface TraceStepIF used by SMC.
TraceStep(String, Integer) - Constructor for class edu.udel.cis.vsl.gmc.smc.TraceStep: Construct an instance of TraceStep with given transition and finalState
TraceStepIF<STATE> - Interface in edu.udel.cis.vsl.gmc: A TraceStepIF represents the execution result of nextState of StateManagerIF.
traceSteps() - Method in class edu.udel.cis.vsl.gmc.Trace: Returns the list of trace steps contained in this trace.
TransitionChooser<STATE,TRANSITION> - Interface in edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.concurrent.ProvisoValue
type() - Method in class edu.udel.cis.vsl.gmc.Option: Returns the type of this option

U

unboundDepth() - Method in class edu.udel.cis.vsl.gmc.seq.DfsSearcher
UNKNOWN - Enum constant in enum class edu.udel.cis.vsl.gmc.concurrent.ProvisoValue
Utils - Class in edu.udel.cis.vsl.gmc.util
Utils() - Constructor for class edu.udel.cis.vsl.gmc.util.Utils

V

valueOf(String) - Static method in enum class edu.udel.cis.vsl.gmc.concurrent.ProvisoValue: Returns the enum constant of this class with the specified name.
valueOf(String) - Static method in enum class edu.udel.cis.vsl.gmc.Option.OptionType: Returns the enum constant of this class with the specified name.
values() - Static method in enum class edu.udel.cis.vsl.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 edu.udel.cis.vsl.gmc.Option.OptionType: Returns an array containing the constants of this enum class, in the order they are declared.
violation() - Method in class edu.udel.cis.vsl.gmc.Trace: Returns true iff a least one violations have been encountered.

W

writeStack(PrintStream) - Method in class edu.udel.cis.vsl.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