uk.ac.man.cs.rainbow.rapa
Class Call.Named

java.lang.Object
  |
  +--uk.ac.man.cs.rainbow.rapa.ProcessTerm
        |
        +--uk.ac.man.cs.rainbow.rapa.Call
              |
              +--uk.ac.man.cs.rainbow.rapa.Call.Named

All Implemented Interfaces:

Serializable

Enclosing class:

Call

public static class Call.Named

extends Call

Named call of a process definition. These refer to objects which can be examined via propositions during the checking of properties over an abstract interpretation of some RAPA.

See Also:

Explorer, Propositions, Serialized Form

Inner classes inherited from class uk.ac.man.cs.rainbow.rapa.Call

Call.Named, Call.SignatureMismatch

Field Summary

static String	ARBITRATE The kind of arbitrates.
static String	BUFFER The kind of buffers.
static String	PROBE The kind of probes.

Constructor Summary

Call.Named(NamingContext.Mapping definition, String kind, String propositionName, Argument[] arguments, Channel[] inputs, Channel[] outputs)

Call.Named(String name, NamingContext context, String kind, String propositionName, Argument[] arguments, Channel[] inputs, Channel[] outputs)

Method Summary

protected GINRet	getGCL(ProgramCounterFactory factory, int i, int n, int t, Value[] c) Get a (g,i,n) triple representing the GCL rules for this process term.
ProcessTerm	subst(GeneralSubstitution s) Apply a substitution to all arguments in the process term.
ProcessTerm	subst(Substitution s) Apply a substitution to all expressions in the process term.

Methods inherited from class uk.ac.man.cs.rainbow.rapa.Call

equals, getArguments, getArguments, getDefinition, getInputs, getInputs, getName, getOutputs, getOutputs, getSequenceHead, toString

Methods inherited from class uk.ac.man.cs.rainbow.rapa.ProcessTerm

getGCL, getGCL

Methods inherited from class java.lang.Object

clone, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

ARBITRATE

public static final String ARBITRATE

The kind of arbitrates.

BUFFER

public static final String BUFFER

The kind of buffers.

PROBE

public static final String PROBE

The kind of probes.

Constructor Detail

Call.Named

public Call.Named(String name,
                  NamingContext context,
                  String kind,
                  String propositionName,
                  Argument[] arguments,
                  Channel[] inputs,
                  Channel[] outputs)

Parameters:

name - The name of the definition to call.

context - Where to look up the RAPA definition.

kind - What kind of named device is this calling. Should be one of ARBITRATE, BUFFER or PROBE.

propositionName - What is the name of the device.

arguments - Non-channel arguments to the device.

inputs - Input channels to the device.

outputs - Output channels from the device.

Call.Named

public Call.Named(NamingContext.Mapping definition,
                  String kind,
                  String propositionName,
                  Argument[] arguments,
                  Channel[] inputs,
                  Channel[] outputs)

Parameters:

definition - The definition to call.

kind - What kind of named device is this calling. Should be one of ARBITRATE, BUFFER or PROBE.

propositionName - What is the name of the device.

arguments - Non-channel arguments to the device.

inputs - Input channels to the device.

outputs - Output channels from the device.

Method Detail

getGCL

protected GINRet getGCL(ProgramCounterFactory factory,
                        int i,
                        int n,
                        int t,
                        Value[] c)

Description copied from class: ProcessTerm

Get a (g,i,n) triple representing the GCL rules for this process term.

Overrides:

getGCL in class Call

Following copied from class: uk.ac.man.cs.rainbow.rapa.ProcessTerm

Parameters:

factory - Generator for new program counters.

i - Current thread number.

n - Current PC value.

t - Terminating PC value (-1 for sequence and loop stitching, 0 for thread-end.)

c - Superthread context vector.

subst

public ProcessTerm subst(Substitution s)

Description copied from class: ProcessTerm

Apply a substitution to all expressions in the process term.

Overrides:

subst in class Call

subst

public ProcessTerm subst(GeneralSubstitution s)

Description copied from class: ProcessTerm

Apply a substitution to all arguments in the process term.

Overrides:

subst in class Call

Following copied from class: uk.ac.man.cs.rainbow.rapa.ProcessTerm

See Also:

Argument