Rainbow
Class ModelcheckResult

java.lang.Object
  |
  +--Rainbow.ModelcheckResult

All Implemented Interfaces:

Serializable

public class ModelcheckResult

extends Object

implements Serializable

Used to report results of model checking.

See Also:

Serialized Form

Inner Class Summary

static class

ModelcheckResult.AutomataState An automata state on the path to a failed model-check.

Field Summary

long	actionsPerformed How many transitions between states were performed.
ModelcheckResult.AutomataState[]	automataTrace The automata states on the path to a failure state.
long	elapsedTime How long did the search take in milliseconds.
ChannelEvent[][]	failureTrace The path to a failure state.
int	loopingPoint At what depth did the Büchi Automaton start looking for a loop.
int	maximumPathLength How deep did the search venture.
long	minorActionsPerformed How many transitions from state to state (including self-loops) were performed.
boolean	satisfied Was the model satisfied.
int	statesFound How many unique states were found.

Methods inherited from class java.lang.Object

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

Field Detail

satisfied

public boolean satisfied

Was the model satisfied.

elapsedTime

public long elapsedTime

How long did the search take in milliseconds.

maximumPathLength

public int maximumPathLength

How deep did the search venture.

statesFound

public int statesFound

How many unique states were found.

actionsPerformed

public long actionsPerformed

How many transitions between states were performed.

minorActionsPerformed

public long minorActionsPerformed

How many transitions from state to state (including self-loops) were performed.

loopingPoint

public int loopingPoint

At what depth did the Büchi Automaton start looking for a loop.

failureTrace

public ChannelEvent[][] failureTrace

The path to a failure state. Each subarray describes the events that happened on a channel in a particular step of the execution. NB: is null if satisfied is false, and the path is not guaranteed to be useful if there are existential path quantifiers in the temporal formula.

automataTrace

public ModelcheckResult.AutomataState[] automataTrace

The automata states on the path to a failure state. Each subarray describes the state during a particular step of the execution. NB: is null if satisfied is false, and the details is not guaranteed to be useful if there are existential path quantifiers in the temporal formula.