uk.ac.man.cs.rainbow.wvmc
Class TemporalModel

java.lang.Object
  |
  +--uk.ac.man.cs.rainbow.wvmc.TemporalModel

All Implemented Interfaces:

Constants

public abstract class TemporalModel

extends Object

implements Constants

Model Checker core.

Field Summary

AutomataBuilder	builder
StateEngine	engine The state engine to check against.
static int	nstates The number of states seen (started).
static int	vstates The number of visited (finished) states.

Fields inherited from interface uk.ac.man.cs.rainbow.wvmc.Constants

A, AND, AU, AV, AX, BAD_LOOP, E, EU, EV, EX, Existential, Expand, False, GOOD_LOOP, LOOP_STATE, MAX_BUCHI_TABLE, MAX_TABLE, NEW_STATE, NO_MORE_SUCCS, NOT_LOOP, NUMOPS, OLD_STATE, opToName, OR, q_0, q_1, q_10, q_11, q_12, q_13, q_14, q_15, q_2, q_3, q_4, q_5, q_6, q_7, q_8, q_9, quantToName, True, U, Universal, V, X

Constructor Summary

protected

TemporalModel(StateEngine engine, AutomataBuilder builder)

Method Summary

Formula	check() Check whether the model and this formula-derived automaton correspond.
abstract void	printAltState() Print this automaton state to System.out.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

engine

public StateEngine engine

The state engine to check against.

builder

public AutomataBuilder builder

vstates

public static int vstates

The number of visited (finished) states.

nstates

public static int nstates

The number of states seen (started).

Constructor Detail

TemporalModel

protected TemporalModel(StateEngine engine,
                        AutomataBuilder builder)

Method Detail

check

public Formula check()
              throws WVMCException,
                     RainbowException,
                     RemoteException

Check whether the model and this formula-derived automaton correspond. Note that we're ignoring the memory management (as is Good And Proper when working with Java) and we've removed the tail-recursion stuff too. I could factor all that rot back in, but I'll leave it to the optimiser(s) instead.

The stuff with left and right has been consigned to a subclass.

Throws:

RainbowException - If the state engine fails.

printAltState

public abstract void printAltState()

Print this automaton state to System.out.