Rainbow
Interface Session

All Superinterfaces:

Remote

All Known Subinterfaces:

AuthorizedSession

All Known Implementing Classes:

SessionHandler

public interface Session

extends Remote

A session (over RMI) with a Rainbow server. Must be called in a single-threaded fashion or Bad Things Will Happen. Obtain sessions from a Server object (like SimServer) over RMI.

Example Sessions

(Note that the purpose of clear() is to remove any saved state hanging around and initialise a number of internal variables. It must be used initially and between runs, which also forces a recompilation every time, and it is good behaviour to use it before finishing with the session object to ensure that the server cleans up any surplus resources in a timely fashion.)

A compilation run

clear()
compile(rainbowModule)
compile(anotherRainbowModule)
link()

A simulation run

...all the compilation run from above...
setExecHandler(handler)
initialise()
step()
step()
...
step()
clear()

Notes:

• The client should perform a 'Run'-like action by displaying the results of a step, pausing a while, and then getting another step.
• 'Until'-like actions should be done by continually executing steps until the simulator clock (which is not guaranteed to advance every step or even by the same value each time it does advance) reaches or exceeds the requested value. Bear in mind that it is possible to have designs that can cause an 'Until' to never terminate, so care should be taken to ensure that users can cancel the 'Until' while it is running...

A deadlock check

...all the compilation run from above...
deadlock(progressWatcher)
clear()

Note that most designs that require an exec-handler are also not readily amenable to deadlock (or model-) checking.

A model-check

...all the compilation run from above...
modelcheck(formula,props,devMap,progressWatcher)
clear()

Notes:

• The above is a fairly complex list of arguments, but the old Tcl client generated them so you should just copy from there...
• Most designs that require an exec-handler are also not readily amenable to deadlock (or model-) checking.

An abstract simulation

clear()
compileAbstract(rainbowModule,abstraction)
stepAbstract()
stepAbstract()
...
stepAbstract()
clear()

Note that this does not use the standard compilation sequence.

An abstract deadlock check

clear()
compileAbstract(rainbowModule,abstraction)
deadlockAbstract(progressWatcher)
clear()

Note that this does not use the standard compilation sequence.

An abstract model-check

clear()
compileAbstract(rainbowModule,abstraction)
modelcheckAbstract(formula,props,progressWatcher)
clear()

Note that this does not use the standard compilation sequence.

The other methods

assemble()

Useful only when working directly with RASM text.

resolveType()

Useful for discovering what a named type actually is.

read()

Useful for reading the contents of a state register and so finding out what is actually happening inside selected devices (the default standard library configures buffers, arbitrates and probes to provide access via this feature.)

A more complete example

    Server server = (Server)Naming.lookup("//somehost/RainbowServer");
    System.out.println("Connected to " + server.getVersion());
    Session s = server.getSession();
    s.clear();
    s.compile(design.getRainbowCode(...));
    s.link();
    s.setExecHandler(new MyExecHandlerImpl());
    Status status = s.initialise();
    updateWireLabels(status.events);
    // ... now I'll illustrate an action like run_until(42) ...
    while (status.time < 42) {
       status = s.step();
    }
    updateWireLabels(status.events);
 

Method Summary

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.
Type	resolveType(String type) Resolve the string to a type against the list of modules to execute.
void	setExecHandler(ExecHandler execHandler) Set the execution callback handler.
Status	step() Perform one simulation step.
Status	stepAbstract() Perform one step of an abstract simulation.

Method Detail

clear

public void clear()
           throws RemoteException,
                  RainbowException

Initialise this session object.

assemble

public void assemble(String rasmtext)
              throws RemoteException,
                     RainbowException

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

compile

public void compile(String rainbowSource)
             throws RemoteException,
                    RainbowException

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

resolveType

public Type resolveType(String type)
                 throws RemoteException,
                        RainbowException

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

link

public void link()
          throws RemoteException,
                 RainbowException

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

setExecHandler

public void setExecHandler(ExecHandler execHandler)
                    throws RemoteException

Set the execution callback handler.

See Also:

TclExec

initialise

public Status initialise()
                  throws RemoteException,
                         RainbowException

Initialise the simulator.

step

public Status step()
            throws RemoteException,
                   RainbowException

Perform one simulation step.

read

public Data read(Integer key)
          throws RemoteException,
                 RainbowException

Read the register indexed by the given key.

deadlock

public DeadlockResult deadlock(ProgressWatcher watcher)
                        throws RemoteException,
                               RainbowException

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

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 RemoteException,
                                   RainbowException

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

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 RemoteException,
                            RainbowException

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

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 RemoteException,
                           RainbowException

Perform one step of an abstract simulation.

deadlockAbstract

public DeadlockResult deadlockAbstract(ProgressWatcher watcher)
                                throws RemoteException,
                                       RainbowException

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.

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 RemoteException,
                                           RainbowException

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.)

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