---

Status Class Reference

Inheritance diagram for Status:[legend]Collaboration diagram for Status:[legend]List of all members.

Public Methods
	Status ()
	Status (Status s)
void	add (Status s)
void	print ()
int	report (long deltaTime, int lastReportTransitions)
void	updateMemoryUsage ()
Public Attributes
int	states = 0
int	transitions = 0
int	instructions = 0
long	memory = 0
long	memoryGC = 0
int	storageMemory = 0
int	GCRuns = 0
int	GCs = 0
int	maxStackDepth = 0
int	intermediateTransitions = 0
int	unique = 0
Static Public Attributes
long	startingTime = System.currentTimeMillis()

---

Detailed Description

This class represents the status of the model checker.

Definition at line 15 of file Status.java.

---

Constructor & Destructor Documentation

Status::Status (    )  [inline]

Initializes the status. Definition at line 166 of file Status.java.

Status::Status (  Status   s )  [inline]

Creates a copy of a Status object. Parameters: s   a Status object Definition at line 173 of file Status.java.

---

Member Function Documentation

void Status::add (  Status   s )  [inline]

Adds the status of a node to the state of the system. Definition at line 210 of file Status.java.

void Status::print (    )  [inline]

Prints the current status to the console. Definition at line 259 of file Status.java. Referenced by JPF::printResults().

void Status::updateMemoryUsage (    )  [inline]

Updates the information regarding memory usage. Definition at line 344 of file Status.java.

---

Member Data Documentation

int Status::GCRuns = 0

Number of types the garbage collector has been activated. Definition at line 106 of file Status.java.

int Status::GCs = 0

Number of objects collected by the garbage collector. Definition at line 116 of file Status.java.

int Status::instructions = 0

Number of instruction that has been executed. Definition at line 29 of file Status.java.

int Status::intermediateTransitions = 0

Number of intermediate transitions. Definition at line 152 of file Status.java.

int Status::maxStackDepth = 0

Current maximum depth searched by the stack. Definition at line 128 of file Status.java.

long Status::memory = 0

Size of the heap used to store objects. Definition at line 34 of file Status.java.

long Status::memoryGC = 0

Size of the heap after running the garbage collector. Definition at line 40 of file Status.java.

long Status::startingTime = System.currentTimeMillis() [static]

Time the verification was started. Definition at line 123 of file Status.java.

int Status::states = 0

Number of states that has been visited. Definition at line 19 of file Status.java.

int Status::storageMemory = 0

Memory used to store states in the hash table. Definition at line 45 of file Status.java.

int Status::transitions = 0

Number of transitions that has been executed. Definition at line 24 of file Status.java.

int Status::unique = 0

Number of unique states stored. Definition at line 159 of file Status.java.

---

The documentation for this class was generated from the following file:

• Status.java

---