|
||||||||||
PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES |
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 |
Classes implementing a model-checker. Converted from Willem's model checker.
The most interesting classes are:
|
||||||||||
PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES |