Package uk.ac.man.cs.rainbow.deadlock

Deadlock and temporal model checking.

See:
Description

Interface Summary

DeadlockChecker.ExplorationObserver	Allows the watching of the progress of a deadlock check.
Introspector	Basic introspection interface for getting the state when evaluating propositions.
ModelCheck.Evaluator	Provides a proposition evaluation service to the model checker.
StateEngine.EntryStack	Path storage mechanism spec.
StateEngine.EventStack	A stack of channel events.

Class Summary

AutomataState	A package of the major and minor state of a state automata.
AutomataState.Major	State automata should contain a subclass of this class if their state affects the behaviour of the state enumeration system.
AutomataState.Minor	State automata should contain a subclass of this class if they have state that they want stored in the state engine but which does not affect the behaviour of the system.
DeadlockChecker	Check a scheduling system for deadlock.
ModelCheck	Checks a transition system against a CTL* formula.
PODeadlockChecker	Check a scheduling system for deadlock.
Propositions	Proposition evaluation engine.
StateEngine	Rewindable state system enumeration engine.
StateEngine.ChannelEvent	Events that happen on channels during state enumeration.
StateEngine.Debug	For debugging.
StateEngine.EntryStore	Visited state storage mechanism.
StateEngine.ExecuteResult	Used to indicate what happened during an execute step.
StateEngine.ExecuteResult.End	Indicates that there are no more transitions out of the current state.
StateEngine.ExecuteResult.Loop	Indicates that there was a transition to a state on the sequence of states that lead to the current state.
StateEngine.ExecuteResult.New	Indicates that a transition to a new state was performed.
StateEngine.ExecuteResult.Old	Indicates that there was a transition to a state that had previously been backtracked out of.
StateEngine.MajorState	Major state.
StateEngine.StackEntry	An entry on the stack.

Exception Summary

ParseException	This exception is thrown when parse errors are encountered.
StateEngine.AlreadyInitialisedException
TokenMgrError	Lexical analyser errors.

Package uk.ac.man.cs.rainbow.deadlock Description

Deadlock and temporal model checking. These classes work by using on-the-fly state-space exploration to check (for deadlock) whether all states have a successor state, or (for model-checking) whether the product of the temporal automata and the state space of the system is empty or not. Anyone interested in the model-checking side should refer to Willem's thesis for more info.