Uses of Class
uk.ac.man.cs.rainbow.wvmc.WVMCException

Packages that use WVMCException

uk.ac.man.cs.rainbow.deadlock	Deadlock and temporal model checking.
uk.ac.man.cs.rainbow.wvmc	Classes implementing a model-checker.

Uses of WVMCException in uk.ac.man.cs.rainbow.deadlock

Methods in uk.ac.man.cs.rainbow.deadlock that throw WVMCException

boolean

ModelCheck.checkModel() Check the state engine against the temporal formula.

Uses of WVMCException in uk.ac.man.cs.rainbow.wvmc

Methods in uk.ac.man.cs.rainbow.wvmc that throw WVMCException

Formula	TemporalModel.check() Check whether the model and this formula-derived automaton correspond.
Formula	Formula.getLeft() Get the left subexpression.
Formula	Formula.getRight() Get the right subexpression.
int	Formula.getLQuant() Get the left quantifier.
int	Formula.getRQuant() Get the right quantifier.
static void	Examiner.examineFormula(Formula f, int maxfs)
boolean	RemoteModelChecker.checkModel(String formula, int language, StateEngine.Engine stateEngine) Check the given temporal model against the given state space.
boolean	Checker.check(StateEngine.Engine engine) Check the temporal model against a state generator.
boolean	RMIServer.checkModel(String formula, int language, StateEngine.Engine stateEngine) Check the given temporal model against the given state space.

Constructors in uk.ac.man.cs.rainbow.wvmc that throw WVMCException

Checker(String formula, int language)
Create a new model checker.