Uses of Class
uk.ac.man.cs.rainbow.RainbowException

Packages that use RainbowException

Rainbow	Entry points, RMI service classes and application-level wrappers.
uk.ac.man.cs.rainbow	Core and general utility classes.
uk.ac.man.cs.rainbow.compiler
uk.ac.man.cs.rainbow.datamodel	Data model for Rainbow simulation.
uk.ac.man.cs.rainbow.deadlock	Deadlock and temporal model checking.
uk.ac.man.cs.rainbow.rapa.abstraction	This package provides classes that support abstract interpretation of GCL derived from RAPA.
uk.ac.man.cs.rainbow.rapa.data	This package provides common datatypes for RAPA and GCL.
uk.ac.man.cs.rainbow.simulator	Rainbow simulation system.
uk.ac.man.cs.rainbow.simulator.rasm	RASM instructions.
uk.ac.man.cs.rainbow.temp	Temporary classes.
uk.ac.man.cs.rainbow.wvmc	Classes implementing a model-checker.

Uses of RainbowException in Rainbow

Methods in Rainbow that throw RainbowException

void	Session.clear() Initialise this session object.
void	Session.assemble(String rasmtext) Assemble the RASM source into a module and add it to the list of things to execute.
void	Session.compile(String rainbowSource) Compile the Rainbow source into a module and add it to the list of things to execute.
Type	Session.resolveType(String type) Resolve the string to a type against the list of modules to execute.
void	Session.link() Link the list of modules to execute.
Status	Session.initialise() Initialise the simulator.
Status	Session.step() Perform one simulation step.
Data	Session.read(Integer key) Read the register indexed by the given key.
DeadlockResult	Session.deadlock(ProgressWatcher watcher) Check the current modules for deadlock.
ModelcheckResult	Session.modelcheck(String ctlStarFormula, String[] propositions, String[] deviceMap, ProgressWatcher watcher) Check the current modules to see if the given temporal formula is satisfied.
void	Session.compileAbstract(String rainbowSource, String abstraction) Compile the Rainbow source into GCL and apply an abstract interpretation to its dataspace.
Status	Session.stepAbstract() Perform one step of an abstract simulation.
DeadlockResult	Session.deadlockAbstract(ProgressWatcher watcher) Check the abstract system for deadlock.
ModelcheckResult	Session.modelcheckAbstract(String LTLFormula, String[] propositions, ProgressWatcher watcher) Check the abstract system to see if it satisfies a temporal formula.
Session	SimServer.getSession()
AuthorizedSession	SimServer.getSession(String username, String password)
protected void	SessionHandler.addCodeThreads(Scheduler s, String msgbit) Add all current code blocks to the given scheduler.
void	SessionHandler.clear()
void	SessionHandler.assemble(String rasmtext)
void	SessionHandler.compile(String rainbowSource)
Type	SessionHandler.resolveType(String type)
void	SessionHandler.link()
Status	SessionHandler.initialise()
Status	SessionHandler.step()
Data	SessionHandler.read(Integer key)
DeadlockResult	SessionHandler.deadlock(ProgressWatcher watcher)
ModelcheckResult	SessionHandler.modelcheck(String ctlStarFormula, String[] propositions, String[] deviceMap, ProgressWatcher watcher)
void	SessionHandler.compileAbstract(String rainbowSource, String abstraction)
Status	SessionHandler.stepAbstract()
DeadlockResult	SessionHandler.deadlockAbstract(ProgressWatcher watcher)
ModelcheckResult	SessionHandler.modelcheckAbstract(String ltlFormula, String[] propositions, ProgressWatcher watcher)
void	AuthorizedSessionHandler.load(String filename)
void	AuthorizedSessionHandler.dump()
void	AuthorizedSession.load(String filename) Assemble the RASM source in the given file on the server into a module and add it to the list of things to execute.
void	AuthorizedSession.dump() Write a human-readable version of the RASM for the most recently compiled/assembled module to System.out.
Session	Server.getSession() Get a new session object.
AuthorizedSession	Server.getSession(String username, String password) Get a new session object that is authorized to perform insecure operations.

Uses of RainbowException in uk.ac.man.cs.rainbow

Subclasses of RainbowException in uk.ac.man.cs.rainbow

static class	Compiler.Errors When there are compiler errors, this class is thrown.
static class	Compiler.Exception Exceptions generated by the compilation stage itself.
class	TclFormatException Signals that an error occurred when trying to convert to or from a Tcl-formatted string.

Methods in uk.ac.man.cs.rainbow that throw RainbowException

static Hashtable	Utils.makeHash(String[] strings) Convert an array of strings into a hashtable.
static Hashtable	Utils.makeHashInt(String[] strings) Convert an array of strings into a hashtable.
static Compiler	Compiler.getInstance() Manufacture a standard compiler.
abstract String	Compiler.rainbow2rif(String rainbow) Convert Rainbow text to RIF text.
abstract String	Compiler.rif2rasm(String rif) Convert RIF text to RASM text.
RASMCode	Compiler.rasm2code(String rasm, Hashtable context) Assemble RASM text into a code block.
RASMCode	Compiler.rainbow2code(String rainbow, Hashtable context) Compile and assemble Rainbow text into a block of code.
ProcessTerm	Compiler.rainbow2rapa(String rainbow) Compile Rainbow text into a RAPA process term.
RASMCode	Compiler.rif2code(String rif, Hashtable context) Compile and assemble RIF text into a block of code.
String	Compiler.rainbow2rasm(String rainbow) Compile Rainbow text into RASM text.

Uses of RainbowException in uk.ac.man.cs.rainbow.compiler

Methods in uk.ac.man.cs.rainbow.compiler that throw RainbowException

static Compiler	RainbowToRASM.getInstance()
static void	RainbowToRASM.main(String[] args)
ProcessTerm	RainbowToRASM.rainbow2rapa(String rainbow)

Uses of RainbowException in uk.ac.man.cs.rainbow.datamodel

Subclasses of RainbowException in uk.ac.man.cs.rainbow.datamodel

class

TypeException Exceptions caused by type problems

Uses of RainbowException in uk.ac.man.cs.rainbow.deadlock

Subclasses of RainbowException in uk.ac.man.cs.rainbow.deadlock

class	ParseException This exception is thrown when parse errors are encountered.
static class	StateEngine.AlreadyInitialisedException

Methods in uk.ac.man.cs.rainbow.deadlock that throw RainbowException

protected Data[]	StateEngine.advanceEpsilons() Advance the system over epsilon steps.
StateEngine.ExecuteResult	StateEngine.execute(boolean resetCounter) Try to execute a non-empty transition to a new state.
StateEngine.ExecuteResult	StateEngine.execute() Try to execute a non-empty transition to a new state.
void	StateEngine.pop() Pop a state from the stack.
boolean	StateEngine.backtrack() Make the system backtrack.
boolean	StateEngine.backtrack(boolean stateValue) Make the system backtrack.
void	StateEngine.stepPastEnd() Generate extra state to demonstrate unwanted loop.
void	StateEngine.EntryStack.advancePastEnd() Restore the trace to the failure point.
void	StateEngine.EntryStackEager.advancePastEnd()
void	StateEngine.EntryStackLazy.advancePastEnd()
boolean	ModelCheck.checkModel() Check the state engine against the temporal formula.
StateEngine.Execed	ModelCheck.Engine.execute(boolean reset, int op, int quant, int gb, boolean ctl, int bad, int good, boolean dfs)
int	DeadlockChecker.step() Perform a single deadlock step.
int	DeadlockChecker.step(int count) Perform several steps.
StateEngine.ChannelEvent[][]	DeadlockChecker.canDeadlock(int steps) Search the entire state space for deadlock.
StateEngine.ChannelEvent[][]	DeadlockChecker.canDeadlock() Search the entire state space for deadlock.
int	PODeadlockChecker.step() Perform a single deadlock step.
boolean	Propositions.evaluate(int idx) Evaluate the idxth proposition.
int	Propositions.evaluate() Evaluate the list of propositions.

Constructors in uk.ac.man.cs.rainbow.deadlock that throw RainbowException

StateEngine(StateEnumerator enumerator)
Create a new state enumeration engine with no automata attached.

StateEngine(StateEnumerator enumerator, AutomataState automata)
Create a new state enumeration engine attached to control automata.

StateEngine(StateEnumerator enumerator, AutomataState automata, int popStyle)
Create a new state enumeration engine attached to control automata.

ModelCheck(StateEnumerator enumerator, String formula)
Create a system that can check a system against a CTL* formula.

DeadlockChecker(StateEnumerator enumerator)
Create a new deadlock-checker.

PODeadlockChecker(StateEnumerator enum)
Create a new deadlock-checker.

Propositions(String[] propositions, String[] lookup, Scheduler sched)
Create a new proposition evaluation engine.

Uses of RainbowException in uk.ac.man.cs.rainbow.rapa.abstraction

Subclasses of RainbowException in uk.ac.man.cs.rainbow.rapa.abstraction

static class

NAry.LengthMismatchException

Uses of RainbowException in uk.ac.man.cs.rainbow.rapa.data

Subclasses of RainbowException in uk.ac.man.cs.rainbow.rapa.data

class

NotUnifiable Indicates where two values are not unifiable with each other for some reason.

Uses of RainbowException in uk.ac.man.cs.rainbow.simulator

Subclasses of RainbowException in uk.ac.man.cs.rainbow.simulator

static class	RainbowThread.IllegalChannelStateException Indicate an attempt to do something naughty with a channel.
static class	RainbowThread.IllegalThreadTerminationException Indicate an attempt to do exit a top-level thread.
static class	RASMCode.Exception Exceptions thrown due to bad assembly code.
static class	RASMThread.Exception Exceptions due to problems during the execution of a thread.
static class	RASMThread.InvokationException Thrown when an exception occurs in some externally referenced code.
static class	RASMThread.PopFailureException Thrown to indicate a problem during a pop operation.
static class	Simulator.DeadlockedException

Methods in uk.ac.man.cs.rainbow.simulator that throw RainbowException

abstract void	Scheduler.initialise() Initialise the scheduler and scheduled system.
Data	Scheduler.readKeyedRegister(int key) Request the contents of the register indexed by the given key.
Data	Scheduler.readKeyedRegister(Integer key) Request the contents of the register indexed by the given key.
void	Simulator.initialise() Initialise the simulation.
void	Simulator.execute() Execute a full simulation step.
void	RainbowThread.execute(int direction) Make this thread execute in the specified direction.
protected abstract void	RainbowThread.execute() Make this thread execute in the current direction.
void	RainbowThread.exitSelf() Make the current thread terminate.
Data	RASMThread.execExtern(String externString) Pass a string to the client for external execution.
protected void	RASMThread.execute() Execute this thread according to where it is in its block of code.
protected abstract boolean	Instruction.execute(RASMThread t) Make this instruction execute in the given context.
protected boolean	RASM.Comparison.execute(RASMThread thread)
protected boolean	RASM.Leq.execute(RASMThread thread) Deprecated.
protected boolean	RASM.Lt.execute(RASMThread thread) Deprecated.
protected boolean	RASM.Geq.execute(RASMThread thread) Deprecated.
protected boolean	RASM.Gt.execute(RASMThread thread) Deprecated.
protected boolean	RASM.Pop.execute(RASMThread thread) Deprecated.
protected boolean	RASM.Exch.execute(RASMThread thread) Deprecated.
protected boolean	RASM.Dup.execute(RASMThread thread) Deprecated.
protected boolean	RASM.Roll.execute(RASMThread thread) Deprecated.
protected boolean	RASM.Index.execute(RASMThread thread) Deprecated.
protected boolean	RASM.KillStackRange.execute(RASMThread thread) Deprecated.
protected boolean	RASM.GetType.execute(RASMThread thread) Deprecated.
protected boolean	RASM.SetType.execute(RASMThread thread) Deprecated.
protected boolean	RASM.Parallel.execute(RASMThread thread) Deprecated.
protected boolean	RASM.Exit.execute(RASMThread thread) Deprecated.
protected boolean	RASM.MakeList.execute(RASMThread thread) Deprecated.
protected boolean	RASM.Split.execute(RASMThread thread) Deprecated.
protected boolean	RASM.Length.execute(RASMThread thread) Deprecated.
protected boolean	RASM.Project.execute(RASMThread thread) Deprecated.
protected boolean	RASM.Insert.execute(RASMThread thread) Deprecated.
protected boolean	RASM.BuildList.execute(RASMThread thread) Deprecated.
protected boolean	RASM.MakeUnion.execute(RASMThread thread) Deprecated.
protected boolean	RASM.OpenUnion.execute(RASMThread thread) Deprecated.
protected boolean	RASM.Error.execute(RASMThread thread) Deprecated.
protected boolean	RASM.TclExec.execute(RASMThread thread) Deprecated.
protected boolean	RASM.Concat.execute(RASMThread thread) Deprecated.
protected boolean	RASM.NDChoice.execute(RASMThread thread) Deprecated.
protected boolean	RASM.NDValue.execute(RASMThread thread) Deprecated.
void	StateEnumerator.restoreState(SavedState saved) Reload a saved state.
void	StateEnumerator.initialise() Initialise the scheduler.
boolean	StateEnumerator.executeTransition(int transitionIndex) Execute a transition.

Constructors in uk.ac.man.cs.rainbow.simulator that throw RainbowException

StateEnumerator(File rainbowSourceFile)
Create a new state enumerator with the compiled version of the given file installed.

Uses of RainbowException in uk.ac.man.cs.rainbow.simulator.rasm

Methods in uk.ac.man.cs.rainbow.simulator.rasm that throw RainbowException

protected boolean	Error.execute(RASMThread thread)
protected boolean	SetType.execute(RASMThread thread)
protected boolean	Exit.execute(RASMThread thread)
protected boolean	TclExec.execute(RASMThread thread)
protected boolean	BuildList.execute(RASMThread thread)
protected boolean	MakeList.execute(RASMThread thread)
protected boolean	MakeUnion.execute(RASMThread thread)
protected boolean	Insert.execute(RASMThread thread)

Uses of RainbowException in uk.ac.man.cs.rainbow.temp

Subclasses of RainbowException in uk.ac.man.cs.rainbow.temp

protected static class

JSCompiler.JSSemanticErrors Specialised error parsing and generating subclass.

Methods in uk.ac.man.cs.rainbow.temp that throw RainbowException

String	JSCompiler.rainbow2rif(String rainbow) Convert Rainbow text to RIF text.
String	JSCompiler.rif2rasm(String rif) Convert RIF text into RASM text.

Uses of RainbowException in uk.ac.man.cs.rainbow.wvmc

Subclasses of RainbowException in uk.ac.man.cs.rainbow.wvmc

static class	StateEngine.CannotBacktrack Thrown to indicate that a backtrack is impossible.
class	WVMCException

Methods in uk.ac.man.cs.rainbow.wvmc that throw RainbowException

Formula	TemporalModel.check() Check whether the model and this formula-derived automaton correspond.
boolean	RemoteModelChecker.checkModel(String formula, int language, StateEngine.Engine stateEngine) Check the given temporal model against the given state space.
StateEngine.Execed	StateEngine.Engine.execute(boolean reset, int op, int quant, int gb, boolean ctl, int bad, int good, boolean dfs) Try to perform a transition.
boolean	Checker.check(StateEngine.Engine engine) Check the temporal model against a state generator.
boolean	RMIServer.checkModel(String formula, int language, StateEngine.Engine stateEngine) Check the given temporal model against the given state space.