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: