Rainbow
Class SessionHandler

java.lang.Object
  |
  +--java.rmi.server.RemoteObject
        |
        +--java.rmi.server.RemoteServer
              |
              +--java.rmi.server.UnicastRemoteObject
                    |
                    +--Rainbow.SessionHandler

All Implemented Interfaces:

Remote, Serializable, Session

Direct Known Subclasses:

AuthorizedSessionHandler

public class SessionHandler

extends UnicastRemoteObject

implements Session

Implementation of a Rainbow server session.

Supported debugging properties:

• rainbow.debug.printRapa
• rainbow.debug.printGcl
• rainbow.debug.printStates

See Also:

Serialized Form

Fields inherited from class java.rmi.server.RemoteObject

ref

Method Summary

protected void	addCodeBlock(RASMCode block) Add a block of code to the list to link and execute.
protected void	addCodeThreads(Scheduler s, String msgbit) Add all current code blocks to the given scheduler.
void	assemble(String rasmtext) Assemble the RASM source into a module and add it to the list of things to execute.
void	clear() Initialise this session object.
void	compile(String rainbowSource) Compile the Rainbow source into a module and add it to the list of things to execute.
void	compileAbstract(String rainbowSource, String abstraction) Compile the Rainbow source into GCL and apply an abstract interpretation to its dataspace.
DeadlockResult	deadlock(ProgressWatcher watcher) Check the current modules for deadlock.
DeadlockResult	deadlockAbstract(ProgressWatcher watcher) Check the abstract system for deadlock.
Status	initialise() Initialise the simulator.
void	link() Link the list of modules to execute.
ModelcheckResult	modelcheck(String ctlStarFormula, String[] propositions, String[] deviceMap, ProgressWatcher watcher) Check the current modules to see if the given temporal formula is satisfied.
ModelcheckResult	modelcheckAbstract(String ltlFormula, String[] propositions, ProgressWatcher watcher) Check the abstract system to see if it satisfies a temporal formula.
Data	read(Integer key) Read the register indexed by the given key.
protected void	reducePriority() Reduce the priority of this thread.
protected void	reset() Reset the state of this session.
Type	resolveType(String type) Resolve the string to a type against the list of modules to execute.
protected void	restorePriority() Restore the priority of this thread.
void	setExecHandler(ExecHandler execHandler) Set the execution callback handler.
protected void	setupExecCallback(Scheduler sched) Connect an external callback executor to the given scheduler.
Status	step() Perform one simulation step.
Status	stepAbstract() Perform one step of an abstract simulation.
String	toString()

Methods inherited from class java.rmi.server.UnicastRemoteObject

clone, exportObject, exportObject, exportObject, unexportObject

Methods inherited from class java.rmi.server.RemoteServer

getClientHost, getLog, setLog

Methods inherited from class java.rmi.server.RemoteObject

equals, getRef, hashCode, toStub

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

Method Detail

reset

protected void reset()

Reset the state of this session.

addCodeBlock

protected void addCodeBlock(RASMCode block)

Add a block of code to the list to link and execute.

addCodeThreads

protected void addCodeThreads(Scheduler s,
                              String msgbit)
                       throws RainbowException

Add all current code blocks to the given scheduler.

setupExecCallback

protected void setupExecCallback(Scheduler sched)

Connect an external callback executor to the given scheduler.

See Also:

setExecHandler(ExecHandler), Scheduler.setExternalExecutionServer(Scheduler.ExternalExecutionServer)

reducePriority

protected final void reducePriority()

Reduce the priority of this thread. Long running operations (like deadlock or model-checking) should do this to allow other users to get a fair use of the server.

restorePriority

protected final void restorePriority()

Restore the priority of this thread. Long running operations (like deadlock or model-checking) should do this on completion to get fair performance when communicating with their client.

clear

public void clear()
           throws RemoteException,
                  RainbowException

Description copied from interface: Session

Initialise this session object.

Specified by:

clear in interface Session

assemble

public void assemble(String rasmtext)
              throws RainbowException

Description copied from interface: Session

Assemble the RASM source into a module and add it to the list of things to execute.

Specified by:

assemble in interface Session

compile

public void compile(String rainbowSource)
             throws RainbowException

Description copied from interface: Session

Compile the Rainbow source into a module and add it to the list of things to execute.

Specified by:

compile in interface Session

resolveType

public Type resolveType(String type)
                 throws RainbowException

Description copied from interface: Session

Resolve the string to a type against the list of modules to execute.

Specified by:

resolveType in interface Session

link

public void link()
          throws RainbowException

Description copied from interface: Session

Link the list of modules to execute. Resolves all remaining inter-module references to concrete addresses (if possible.)

Specified by:

link in interface Session

setExecHandler

public void setExecHandler(ExecHandler execHandler)

Description copied from interface: Session

Set the execution callback handler.

Specified by:

setExecHandler in interface Session

Following copied from interface: Rainbow.Session

See Also:

TclExec

initialise

public Status initialise()
                  throws RainbowException

Description copied from interface: Session

Initialise the simulator.

Specified by:

initialise in interface Session

step

public Status step()
            throws RainbowException

Description copied from interface: Session

Perform one simulation step.

Specified by:

step in interface Session

read

public Data read(Integer key)
          throws RainbowException

Description copied from interface: Session

Read the register indexed by the given key.

Specified by:

read in interface Session

deadlock

public DeadlockResult deadlock(ProgressWatcher watcher)
                        throws RainbowException

Description copied from interface: Session

Check the current modules for deadlock. Note that the system must not have been initialised first.

Specified by:

deadlock in interface Session

Following copied from interface: Rainbow.Session

Parameters:

watcher - Object to receive progress notifications, or null if you don't want to receive them.

modelcheck

public ModelcheckResult modelcheck(String ctlStarFormula,
                                   String[] propositions,
                                   String[] deviceMap,
                                   ProgressWatcher watcher)
                            throws RainbowException

Description copied from interface: Session

Check the current modules to see if the given temporal formula is satisfied.

Specified by:

modelcheck in interface Session

Following copied from interface: Rainbow.Session

Parameters:

ctlStarFormula - The temporal formula to check in CTL^*.

propositions - Array of propositions referred to in the formula, each of which will be parsed by Propositions.

deviceMap - Description of what device/register is referred to by what name in the propositions.

watcher - Object to receive progress notifications, or null if you don't want to receive them.

See Also:

SpecParse

compileAbstract

public void compileAbstract(String rainbowSource,
                            String abstraction)
                     throws RainbowException

Description copied from interface: Session

Compile the Rainbow source into GCL and apply an abstract interpretation to its dataspace.

Specified by:

compileAbstract in interface Session

Following copied from interface: Rainbow.Session

Parameters:

rainbowSource - The source to the Rainbow code to be abstractly interpreted.

abstraction - The abstraction to be applied (which will be parsed by Parse.)

stepAbstract

public Status stepAbstract()
                    throws RainbowException

Description copied from interface: Session

Perform one step of an abstract simulation.

Specified by:

stepAbstract in interface Session

deadlockAbstract

public DeadlockResult deadlockAbstract(ProgressWatcher watcher)
                                throws RainbowException

Description copied from interface: Session

Check the abstract system for deadlock. Note that a deadlock may exist in the concrete system which the abstracted version does not find if the abstraction is not carefully selected.

Specified by:

deadlockAbstract in interface Session

Following copied from interface: Rainbow.Session

Parameters:

watcher - Object to receive progress notifications, or null if you don't want to receive them.

modelcheckAbstract

public ModelcheckResult modelcheckAbstract(String ltlFormula,
                                           String[] propositions,
                                           ProgressWatcher watcher)
                                    throws RainbowException,
                                           RemoteException

Description copied from interface: Session

Check the abstract system to see if it satisfies a temporal formula. Note that failure of the abstract system to satisfy the formula does not mean that the negation of the formula will be satisfied, and that the formula is to be written in LTL as opposed to CTL^* (this change follows from the details of the abstraction process.)

Specified by:

modelcheckAbstract in interface Session

Following copied from interface: Rainbow.Session

Parameters:

LTLFormula - Temporal formula to check.

propositions - Array of propositions referred to in the formula, each of which will be parsed by Propositions.

watcher - Object to receive progress notifications, or null if you don't want to receive them.

See Also:

SpecParse

toString

public String toString()

Overrides:

toString in class RemoteObject