uk.ac.man.cs.rainbow.deadlock
Class Propositions

java.lang.Object
  |
  +--uk.ac.man.cs.rainbow.deadlock.Propositions

All Implemented Interfaces:

ModelCheck.Evaluator, Serializable

public class Propositions

extends Object

implements ModelCheck.Evaluator, Serializable

Proposition evaluation engine. Given a list of strings that define the propositions (a simultaneously augmented and cut-down Rainbow expression) and a way of mapping from device labels to register keys, this class will be able to evaluate either a single proposition or the whole set of them to deliver a labelling for the whole state of the system.

Augmented operations are:

Arbitrates

Chosen, direction, left, and right. The left and right operations are equivalent to testing the direction for equality to 0 and 1 respectively.

Buffers

Empty, full and contents.

Probes

Idle, busy and value.

For example, to test buffer foobar contains the value 42, you'd do the following (the other operations follow equivalently.)

 buffer foobar full /\ buffer foobar contents == 42
 

Note that only device names that are valid identifiers according to the rules of Rainbow can be used; invalid names in the mapping will be ignored, and invalid names in the propositions will cause a syntax error.

This class can be debugged with the aid of the boolean property rainbow.props.debugEval.

See Also:

Grammar Recognised, Scheduler.readKeyedRegister(Integer), Serialized Form

Constructor Summary

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

Propositions(String[] propositions, Introspector introspector)
Create a new proposition evaluation engine.

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

Method Summary

void	dump() Print the ASTs for the propositions to System.out.
int	evaluate() Evaluate the list of propositions.
boolean	evaluate(int idx) Evaluate the idxth proposition.
int	evaluatePropositions() Evaluate the list of propositions.
Introspector	getIntrospector()

Methods inherited from class java.lang.Object

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

Constructor Detail

Propositions

public Propositions(String[] propositions,
                    Hashtable lookup,
                    Scheduler sched)
             throws ParseException

Create a new proposition evaluation engine.

Parameters:

propositions - The propositions to evaluate.

lookup - A mapping from device names to keyed register ids (instances of Integer.) Device names consist of the type of the device (arbitrate, buffer, or probe), a comma and then the name of the device.

sched - The scheduler in which to look up register contents.

Throws:

ParseException - If any of the strings do not describe a valid proposition.

Propositions

public Propositions(String[] propositions,
                    String[] lookup,
                    Scheduler sched)
             throws ParseException,
                    RainbowException,
                    NumberFormatException

Create a new proposition evaluation engine.

Parameters:

propositions - The propositions to evaluate.

lookup - A mapping from device names to keyed register ids (really an array of keys and values.) Device names consist of the type of the device (arbitrate, buffer, or probe), a comma and then the name of the device.

sched - The scheduler in which to look up register contents.

Throws:

ParseException - If any of the proposition strings do not describe a valid proposition.

RainbowException - If there are an odd number of strings in the lookup array.

NumberFormatException - If any of the strings at odd-numbered indices in the lookup array are not valid integers in base-10 format.

See Also:

Utils.makeHashInt(String[])

Propositions

public Propositions(String[] propositions,
                    Introspector introspector)
             throws ParseException

Create a new proposition evaluation engine.

Parameters:

propositions - The propositions to evaluate.

introspector - The introspection engine in which to look up register values.

Throws:

ParseException - If any of the strings do not describe a valid proposition.

Method Detail

evaluatePropositions

public int evaluatePropositions()

Description copied from interface: ModelCheck.Evaluator

Evaluate the list of propositions. There may be up to 32 propositions (formulae normally have far fewer.)

Specified by:

evaluatePropositions in interface ModelCheck.Evaluator

Following copied from interface: uk.ac.man.cs.rainbow.deadlock.ModelCheck.Evaluator

Returns:

A bit-encoding of the proposition values, with bit-0 (the first bit) corresponding to proposition p₁, bit-1 (the second bit) corresponding to proposition p₂, and so on.

See Also:

StateEngine.Engine.getPropositionDescriptor()

getIntrospector

public Introspector getIntrospector()

evaluate

public boolean evaluate(int idx)
                 throws TypeException,
                        RainbowException,
                        ClassCastException

Evaluate the idx^th proposition.

Returns:

A valuation of the proposition, given the current state of the devices associated with this class (via their scheduler.)

Throws:

TypeException - If an attempt to compare incomparable types, build an invalid array, use the wrong kind of structure dereference, or cast to an incompatible type is made.

RainbowException - If an attempt to access the register for a non-existant device is made, or if a proposition attempts to return a non-boolean value.

evaluate

public int evaluate()
             throws TypeException,
                    RainbowException,
                    ClassCastException

Evaluate the list of propositions. There may be up to 32 propositions (formulæ normally have far fewer.) Like evaluatePropositions() except this can throw exceptions, making it more useful for debugging.

Returns:

A bit-encoding of the proposition values, with bit-0 (the first bit) corresponding to proposition p₁, bit-1 (the second bit) corresponding to proposition p₂, and so on.

Throws:

TypeException - If an attempt to compare incomparable types, build an invalid array, use the wrong kind of structure dereference, or cast to an incompatible type is made.

RainbowException - If an attempt to access the register for a non-existant device is made, or if a proposition attempts to return a non-boolean value.

dump

public void dump()

Print the ASTs for the propositions to System.out. Intended for use debugging only.