Serialized Form
readObject
private void readObject(ObjectInputStream stream)
throws IOException,
ClassNotFoundException
type
String type
- What sort of event was it. Will be one of
ChannelEvent.REQUEST,
ChannelEvent.ACKNOWLEDGE, ChannelEvent.TRANSITION or ChannelEvent.BLOCKED
and may be compared safely by pointer.
label
String label
- Which channel was it.
data
Object data
- What value was passed on the channel.
time
long time
- When did the event happen.
deadlocked
boolean deadlocked
- Was a deadlock found.
elapsedTime
long elapsedTime
- How long did the search take in milliseconds.
maximumPathLength
int maximumPathLength
- How deep did the search venture.
statesFound
int statesFound
- How many unique states were found.
actionsPerformed
long actionsPerformed
- How many transitions between states were performed.
minorActionsPerformed
long minorActionsPerformed
- How many transitions from state to state (including self-loops)
were performed.
deadlockTrace
ChannelEvent[][] deadlockTrace
- The path to a deadlock. Each subarray describes the events
that happened on a channel in a particular step of the
execution. NB: is null if
DeadlockResult.deadlocked
is false.
satisfied
boolean satisfied
- Was the model satisfied.
elapsedTime
long elapsedTime
- How long did the search take in milliseconds.
maximumPathLength
int maximumPathLength
- How deep did the search venture.
statesFound
int statesFound
- How many unique states were found.
actionsPerformed
long actionsPerformed
- How many transitions between states were performed.
minorActionsPerformed
long minorActionsPerformed
- How many transitions from state to state (including self-loops)
were performed.
loopingPoint
int loopingPoint
- At what depth did the Büchi Automaton start looking for a
loop.
failureTrace
ChannelEvent[][] failureTrace
- The path to a failure state. Each subarray describes the
events that happened on a channel in a particular step of the
execution. NB: is null if
ModelcheckResult.satisfied
is false, and the path is not guaranteed to be useful if there
are existential path quantifiers in the temporal formula.
automataTrace
ModelcheckResult.AutomataState[] automataTrace
- The automata states on the path to a failure state. Each
subarray describes the state during a particular step of the
execution. NB: is null if
ModelcheckResult.satisfied
is false, and the details is not guaranteed to be useful if
there are existential path quantifiers in the temporal formula.
propositionValuation
int propositionValuation
- What is the (bit-coded) proposition valuation.
- See Also:
ModelCheck.Evaluator
operator
String operator
- What is the current temporal operator.
loopType
String loopType
- What kind of loop is currently expected.
sessionNumber
int sessionNumber
time
long time
- What is the simulator time.
events
ChannelEvent[] events
- What events happened in this simulator step.
|
Package uk.ac.man.cs.rainbow |
line
int line
- Where did this error happen. This is an approximate location.
- The line number of this particular error.
message
String message
- What was the error. The standard error handler in the client
will format this string differently from the
detail field. - The body of the message.
detail
String[] detail
- Anything else of interest relating to the error. You might
wish to put details of how you are recovering from the problem
(if at all) in this. You may expect that each of the strings
in the array will be formatted as a separate line.
- Additional information.
errors
Compiler.Error[] errors
- Information about the semantic errors.
column
int column
- Narrow the location of the error to the exact column.
- What column triggered the error?
detail
Throwable detail
- Where this exception was triggered by another, this
is what that exception was...
augment
String augment
- Used to fill in extra details not available in the
throwing context.
|
Package uk.ac.man.cs.rainbow.compiler.expressions |
op
String op
left
Expression left
right
Expression right
value
boolean value
fId
Identifier fId
argList
Expression argList
casted_exp
Expression casted_exp
casted_to
CompilerType casted_to
tguardList
TagGuard tguardList
if_exp
Expression if_exp
then_exp
Expression then_exp
else_exp
Expression else_exp
nm
String nm
ordinal_value
int ordinal_value
spec
CompilerType spec
tguardList
TagGuard tguardList
exp
Expression exp
id
Identifier id
isRegister
boolean isRegister
isVariable
boolean isVariable
value
int value
components
Constant components
fieldList
Expression fieldList
record
Expression record
fieldname
String fieldname
repeated
Expression repeated
count
Expression count
countval
int countval
op
String op
exp
Expression exp
tag
String tag
exp
Expression exp
elems
Constant elems
elemList
Expression elemList
vec
Expression vec
index
Expression index
|
Package uk.ac.man.cs.rainbow.compiler.parser |
specialConstructor
boolean specialConstructor
- This variable determines which constructor was used to create
this object and thereby affects the semantics of the
"getMessage" method (see below).
currentToken
Token currentToken
- This is the last token that has been consumed successfully. If
this object has been created due to a parse error, the token
followng this token will (therefore) be the first error token.
expectedTokenSequences
int[][] expectedTokenSequences
- Each entry in this array is an array of integers. Each array
of integers represents a sequence of tokens (by their ordinal
values) that is expected at this point of the parse.
tokenImage
String[] tokenImage
- This is a reference to the "tokenImage" array of the generated
parser within which the parse error occurred. This array is
defined in the generated ...Constants interface.
eol
String eol
- The end of line string for this machine.
errorCode
int errorCode
- Indicates the reason why the exception is thrown. It will have
one of the above 4 values.
|
Package uk.ac.man.cs.rainbow.datamodel |
type
Type type
- The type of the data value.
contents
Expression[] contents
- The contents of the list type.
contents
Expression contents
- The contents of the union.
index
int index
- The discriminator for the union. Or, in other words,
which tag does the union have.
value
int value
- The value that this word represents.
contents
String contents
- The contents of the string.
idents
String[] idents
- The (ordered) list of identifiers that make up the members of
the enumeration.
- The identifiers making up the enumeration.
types
Type[] types
- The types of the tuple fields.
tags
String[] tags
- The tags on the tuple fields.
types
Type[] types
- The types of the union members.
tags
String[] tags
- The tags for the union members.
memberType
Type memberType
- The type of the members of the vector.
memberCount
int memberCount
- How many members does the vector have.
contents
Type contents
- The type that the data value represents.
|
Package uk.ac.man.cs.rainbow.deadlock |
this$0
ModelCheck this$0
propositions
int propositions
- This state's proposition descriptor
specialConstructor
boolean specialConstructor
- This variable determines which constructor was used to create
this object and thereby affects the semantics of the
"getMessage" method (see below).
currentToken
uk.ac.man.cs.rainbow.deadlock.Token currentToken
- This is the last token that has been consumed successfully. If
this object has been created due to a parse error, the token
followng this token will (therefore) be the first error token.
expectedTokenSequences
int[][] expectedTokenSequences
- Each entry in this array is an array of integers. Each array
of integers represents a sequence of tokens (by their ordinal
values) that is expected at this point of the parse.
tokenImage
String[] tokenImage
- This is a reference to the "tokenImage" array of the generated
parser within which the parse error occurred. This array is
defined in the generated ...Constants interface.
eol
String eol
- The end of line string for this machine.
readObject
private void readObject(ObjectInputStream in)
throws IOException,
ClassNotFoundException
- Rebuild the internal representations of everything upon
deserialization.
exprs
String[] exprs
- The string version of the propositions.
lookup
Hashtable lookup
- The hashtable used to convert device names to register ids, or
null if the introspector field is non-null.
sched
Scheduler sched
- The scheduler to look up registers in, or null if the
introspector field is non-null.
introspector
Introspector introspector
- The introspector to look up registers in, or null if
the lookup and sched fields are non-null.
isReq
boolean isReq
- Is this a request?
time
long time
- When did this happen?
val
Data val
- What was the data being passed?
label
String label
- Which channel was it?
depth
int depth
- Depth on stack of the loop state.
flag
boolean flag
- The valuation of the previously seen state.
errorCode
int errorCode
- Indicates the reason why the exception is thrown. It will have
one of the above 4 values.
|
Package uk.ac.man.cs.rainbow.rapa |
action
Action[] action
body
ProcessTerm body
reg
Register reg
exp
Value exp
definition
NamingContext.Mapping definition
arguments
Argument[] arguments
inputs
Channel[] inputs
outputs
Channel[] outputs
kind
String kind
propositionName
String propositionName
call
Call call
definition
NamingContext.Mapping definition
p1
ProcessTerm p1
p2
ProcessTerm p2
guard
Value guard
proc
ProcessTerm proc
proc
ProcessTerm proc
hide
Channel[] hide
bool
Value[] bool
proc
ProcessTerm[] proc
body
ProcessTerm body
name
String name
parameters
Argument[] parameters
inputs
Channel[] inputs
outputs
Channel[] outputs
readObject
private void readObject(ObjectInputStream stream)
throws IOException,
ClassNotFoundException
action
Action[] action
proc
ProcessTerm[] proc
reg
Register reg
type
Type type
proc
ProcessTerm proc
p1
ProcessTerm p1
p2
ProcessTerm p2
readObject
private void readObject(ObjectInputStream stream)
throws IOException,
ClassNotFoundException
action
Action[] action
body
ProcessTerm body
var
Variable.Named var
type
Type type
proc
ProcessTerm proc
|
Package uk.ac.man.cs.rainbow.rapa.abstraction |
specialConstructor
boolean specialConstructor
- This variable determines which constructor was used to create
this object and thereby affects the semantics of the
"getMessage" method (see below).
currentToken
Token currentToken
- This is the last token that has been consumed successfully. If
this object has been created due to a parse error, the token
followng this token will (therefore) be the first error token.
expectedTokenSequences
int[][] expectedTokenSequences
- Each entry in this array is an array of integers. Each array
of integers represents a sequence of tokens (by their ordinal
values) that is expected at this point of the parse.
tokenImage
String[] tokenImage
- This is a reference to the "tokenImage" array of the generated
parser within which the parse error occurred. This array is
defined in the generated ...Constants interface.
eol
String eol
- The end of line string for this machine.
errorCode
int errorCode
- Indicates the reason why the exception is thrown. It will have
one of the above 4 values.
|
Package uk.ac.man.cs.rainbow.rapa.data |
name
String name
names
String[] names
values
Value[] values
top
Value top
nametoval
Map nametoval
chan
Channel chan
value
Value value
kind
int kind
args
Value[] args
name
String name
resultType
Type resultType
e1
Value e1
e2
Value e2
isTrue
boolean isTrue
readObject
private void readObject(ObjectInputStream stream)
throws IOException,
ClassNotFoundException
name
String name
uid
int uid
from
Argument from
to
Argument to
name
String name
type
Type type
name
String name
num
int num
readObject
private void readObject(ObjectInputStream stream)
throws IOException,
ClassNotFoundException
uid
int uid
name
String name
type
Type type
i
int i
n
int n
exprs
Value[] exprs
e
Value e
subst
Map subst
readObject
private void readObject(ObjectInputStream stream)
throws IOException,
ClassNotFoundException
uid
int uid
type
Type type
name
String name
|
Package uk.ac.man.cs.rainbow.rapa.gcl |
reg
Register reg
exp
Value exp
i
int i
n
int n
i
int i
n
int n
guards
Value[] guards
actions
Action[] actions
updates
Assignment[] updates
rules
Rule[] rules
namingMap
Map namingMap
|
Package uk.ac.man.cs.rainbow.simulator |
activated
boolean activated
- Is the channel actiated?
writer
RainbowThread writer
- What thread wrote to the channel?
reader
RainbowThread reader
- What thread is interested in writes to the channel?
name
String name
- What is the name of the channel?
contents
Data contents
- What value is being passed along the channel?
listeners
Vector listeners
- What objects are interested in events on this channel?
chan
Channel chan
- The channel referred to by this data value.
reverseAtSleep
boolean reverseAtSleep
- Do we change direction when we hit a sleep?
isActive
boolean isActive
- Are we active?
activeChildren
int activeChildren
- How many children are active?
choice
int choice
- What choice have we had made?
choiceRange
int choiceRange
- Over what range was the choice made?
saver
RainbowThread saver
- What thread saved this state?
comment
String comment
- Deprecated.
- The body of the comment
i
Integer i
- Deprecated.
- When an argument was passed to the instruction at
creation time, this is where the argument is stored.
where
String where
- Deprecated.
- The line identification info.
value
Data value
- Deprecated.
- The value to push.
readObject
private void readObject(ObjectInputStream in)
throws IOException,
ClassNotFoundException
writeObject
private void writeObject(ObjectOutputStream out)
throws IOException,
RASMCode.Exception
instrs
Stack instrs
- The list of instructions that make up the code block.
labels
Hashtable labels
- The labels in the code block
name
String name
- The name of this code block.
nameContext
Hashtable nameContext
- A context for looking names up in when parsing values
relating to this code block
block
String block
- The name of the block where the exception occurred.
label
String label
- The name of the label which triggered the exception.
code
RASMCode code
- Which block of code does the label lie within?
location
int location
- Where in that block of code does the label point to?
name
String name
- What is the name of the label?
label
RASMCode.Label label
- The label referred to by this data value.
s
Stack s
- We're implemented using a stack for convenience.
this$0
RASMThread this$0
codes
RASMCode[] codes
- What code blocks does this call chain pass through?
pcs
int[] pcs
- What locations does this call chain pass through?
hashcode
int hashcode
- What is the hashCode? Easier to store than to recalc.
where
RASMThread.CallChain where
- Where the thread is working...
registerContents
Data[] registerContents
- What is in the thread's registers...
children
Data[] children
- What are the characterisations of the thread's kids...
idx
Integer idx
- The stack index that triggered the exception, if known.
t
Throwable t
- The exception or error that really ocurred.
reader
RainbowThread reader
- What thread is trying to read from this channel?
writer
RainbowThread writer
- What thread is trying to write to this channel?
contents
Data contents
- What value is on the channel?
active
boolean active
- Is the channel active?
self
RASMThread.SavedRASMThreadState.This self
- The easily cacheable parts of the state of this
thread; i.e. those parts that can only be changed
by the execution of the thread, and not any of
its children.
children
SavedState[] children
- The state of the descendents of this thread.
regContents
Data[] regContents
- The state of the registers created by this thread.
Note that we assume that registers are never changed
by non-sibling threads, an assumption that is correct
for programs that are compiled from Rainbow source.
chanwatchers
RASMThread.ReaderWriter[] chanwatchers
- What is going on on the channels.
code
RASMCode code
- The code block we're executing in.
pc
int pc
- The program counter.
stackFrame
int stackFrame
- The index of the base of the current stack frame.
stack
Object[] stack
- The stack.
context
Object context
- The temporary context. Used to implement restartable
instructions.
superState
SavedState superState
- The state of our superclass.
exn
Exception exn
- The exception that caused the problem.
name
String name
- The name of the register.
contents
Data contents
- The contents of the register.
reg
Register reg
- The register represented by this data value.
initialised
boolean initialised
- Has the simulator been initialised yet?
forward
ThreadSet forward
- Threads to schedule in the forward direction.
backward
ThreadSet backward
- Threads to schedule in the backward direction.
thisWay
ThreadSet thisWay
- Either forward or backward!
thatWay
ThreadSet thatWay
- Either backward or forward!
timer
Simulator.Timer timer
- Threads that are delayed, waiting for some future time.
now
long now
- The current time.
chooser
Random chooser
- The random number generator.
schedulingStyle
int schedulingStyle
- The style of scheduling used.
readObject
private void readObject(ObjectInputStream in)
throws IOException,
ClassNotFoundException
- Rebuild the fast access hash tables and the tail pointer
during deserialization.
chain
Simulator.Timer.timeBucket chain
- The list of buckets holding threads to be woken.
readObject
private void readObject(ObjectInputStream in)
throws IOException,
ClassNotFoundException
time
long time
- The wakeup time of the threads in this bucket.
threads
ThreadSet threads
- The collection of threads in this bucket.
next
Simulator.Timer.timeBucket next
- The next (later) bucket.
initialised
boolean initialised
- Has the simulator been initialised yet?
toplevelThreads
Stack toplevelThreads
- All the initial threads so that the whole system can be
properly serialized, and not just the active parts.
forward
ThreadSet forward
- Threads to schedule in the forward direction.
backward
ThreadSet backward
- Threads to schedule in the backward direction.
transitions
ThreadSet transitions
- Threads that can start a transition (which might be an
empty transition, of course.)
thisWay
ThreadSet thisWay
- Forward, backward or transitions.
thatWay
ThreadSet thatWay
- Forward, backward or transitions.
choiceThread
RainbowThread choiceThread
- Which threads are undergoing non-deterministic choice.
seqNum
long seqNum
- A "time" substitute.
characterisationThreads
RainbowThread[] characterisationThreads
- Which threads are to be characterised.
t
RainbowThread t
allThreads
SavedState[] allThreads
- The state of the threads.
runnableThreads
ThreadSet runnableThreads
- The state of the scheduler. Excludes the thread that
is in the throes of non-deterministic choice.
choosingThread
RainbowThread choosingThread
- What thread is non-deterministic now.
time
long time
- The timestamp.
generator
StateEnumerator generator
- Stamp with the generator. A saved state can only be
reloaded into the scheduler that generated it.
readObject
private void readObject(ObjectInputStream in)
throws IOException,
ClassNotFoundException
- Rebuilds an internal hashtable used for fast identification of
the presence and location of a thread.
v
Vector v
- Make sure you only ever access this vector read-only from outside
this class.
- We use a vector to implement the storage scheme.
|
Package uk.ac.man.cs.rainbow.simulator.rasm |
comment
String comment
- The body of the comment
i
Integer i
- When an argument was passed to the instruction at
creation time, this is where the argument is stored.
where
String where
- The line identification info.
value
Data value
- The value to push.
|
Package uk.ac.man.cs.rainbow.temp |
text
TextArea text
- The text area to put log messages into.
|
Package uk.ac.man.cs.rainbow.wvmc |
op
int op
- Temporal operator index.
quantifier
int quantifier
- Path quantifier.
gb
int gb
- Loop kind indicator.
B_depth
int B_depth
- Point of entry to bad loop.
G_depth
int G_depth
- Point of entry to good loop.
ctl
boolean ctl
- CTL flag.
dfs
boolean dfs
- Search mode.
|
Package uk.ac.man.cs.rainbow.wvmc.parser |
specialConstructor
boolean specialConstructor
- This variable determines which constructor was used to create
this object and thereby affects the semantics of the
"getMessage" method (see below).
- Do we have proper parse info available?
currentToken
Token currentToken
- This is the last token that has been consumed successfully. If
this object has been created due to a parse error, the token
followng this token will (therefore) be the first error token.
- The last successfully consumed token.
expectedTokenSequences
int[][] expectedTokenSequences
- Each entry in this array is an array of integers. Each array
of integers represents a sequence of tokens (by their ordinal
values) that is expected at this point of the parse.
- The expected token sequences.
tokenImage
String[] tokenImage
- This is a reference to the "tokenImage" array of the generated
parser within which the parse error occurred. This array is
defined in the generated ...Constants interface.
- Used for rendering the expected token sequences.
kind
int kind
- An integer that describes the kind of this token. This numbering
system is determined by JavaCCParser, and a table of these numbers is
stored in the file ...Constants.java.
beginLine
int beginLine
- beginLine and beginColumn describe the position of the first character
of this token; endLine and endColumn describe the position of the
last character of this token.
beginColumn
int beginColumn
- beginLine and beginColumn describe the position of the first character
of this token; endLine and endColumn describe the position of the
last character of this token.
endLine
int endLine
- beginLine and beginColumn describe the position of the first character
of this token; endLine and endColumn describe the position of the
last character of this token.
endColumn
int endColumn
- beginLine and beginColumn describe the position of the first character
of this token; endLine and endColumn describe the position of the
last character of this token.
image
String image
- The string image of the token.
next
Token next
- A reference to the next regular (non-special) token from the input
stream. If this is the last token from the input stream, or if the
token manager has not read tokens beyond this one, this field is
set to null. This is true only if this token is also a regular
token. Otherwise, see below for a description of the contents of
this field.
specialToken
Token specialToken
- This field is used to access special tokens that occur prior to this
token, but after the immediately preceding regular (non-special) token.
If there are no such special tokens, this field is set to null.
When there are more than one such special token, this field refers
to the last of these special tokens, which in turn refers to the next
previous special token through its specialToken field, and so on
until the first special token (whose specialToken field is null).
The next fields of special tokens refer to other special tokens that
immediately follow it (without an intervening regular token). If there
is no such token, this field is null.
errorCode
int errorCode
- Indicates the reason why the exception is thrown. It will have
one of the above 4 values.
- Why did the error occur?