Uses of Package
uk.ac.man.cs.rainbow.wvmc

Packages that use uk.ac.man.cs.rainbow.wvmc

uk.ac.man.cs.rainbow.deadlock	Deadlock and temporal model checking.
uk.ac.man.cs.rainbow.rapa.abstraction	This package provides classes that support abstract interpretation of GCL derived from RAPA.
uk.ac.man.cs.rainbow.wvmc	Classes implementing a model-checker.
uk.ac.man.cs.rainbow.wvmc.parser	CTL*-NNF and LTL parsers.

Classes in uk.ac.man.cs.rainbow.wvmc used by uk.ac.man.cs.rainbow.deadlock

StateEngine.CannotBacktrack
Thrown to indicate that a backtrack is impossible.

StateEngine.Engine
All state generators look like this.

StateEngine.Execed
The result of an execute operation.

StateEngine.Looped
When a loop is detected, extra information must be returned.

StateEngine.Popped
The data returned when an action happens that removes a state from the stack.

StateEngine.Repeated
When an old state is detected, extra information must be returned.

WVMCException

Classes in uk.ac.man.cs.rainbow.wvmc used by uk.ac.man.cs.rainbow.rapa.abstraction

StateEngine.CannotBacktrack
Thrown to indicate that a backtrack is impossible.

StateEngine.Engine
All state generators look like this.

StateEngine.Execed
The result of an execute operation.

StateEngine.Popped
The data returned when an action happens that removes a state from the stack.

Classes in uk.ac.man.cs.rainbow.wvmc used by uk.ac.man.cs.rainbow.wvmc

AutomataBuilder
Buchi-automata construction site.

Constants
Assorted constants.

Formula
A CTL* formula fragment.

FormulaSet
A set of formulae organised as a linked list.

RemoteModelChecker
The interface exported by the model checker over Java RMI.

StateEngine
Wrapper code to convert a sensible interface into the form required by the model checker.

StateEngine.CannotBacktrack
Thrown to indicate that a backtrack is impossible.

StateEngine.Engine
All state generators look like this.

StateEngine.Execed
The result of an execute operation.

StateEngine.Popped
The data returned when an action happens that removes a state from the stack.

WVMCException

Classes in uk.ac.man.cs.rainbow.wvmc used by uk.ac.man.cs.rainbow.wvmc.parser

AutomataBuilder
Buchi-automata construction site.

Constants
Assorted constants.

Formula
A CTL* formula fragment.