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

Classes implementing a model-checker.

See:
Description

Interface Summary

Constants	Assorted constants.
RemoteModelChecker	The interface exported by the model checker over Java RMI.
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.Repeated	When an old state is detected, extra information must be returned.

Class Summary

AutomataBuilder	Buchi-automata construction site.
Checker	The model checker.
Examiner	Formula representation optimiser.
Formula	A CTL* formula fragment.
FormulaSet	A set of formulae organised as a linked list.
RMIServer	A simple server object that exports the model checker via Java RMI.
Set	Code for manipulating sets of numbers.
StateEngine	Wrapper code to convert a sensible interface into the form required by the model checker.
StateEngine.Popped	The data returned when an action happens that removes a state from the stack.
TemporalModel	Model Checker core.

Exception Summary

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

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

Classes implementing a model-checker. Converted from Willem's model checker.

The most interesting classes are:

• Checker which is the main local interface to the model checker.
• RemoteModelChecker which is the version exported via Java RMI.