korat.testing.impl
Class StateSpaceExplorer

java.lang.Object
  korat.testing.impl.StateSpaceExplorer

All Implemented Interfaces:

IKoratSearchStrategy

public class StateSpaceExplorer
extends Object
implements IKoratSearchStrategy

StateSpaceExplorer implements Korat search strategy

Author:

Sasa Misailovic

Field Summary

protected IIntList	accessedFields
protected CandidateBuilder	candidateBuilder
protected int[]	candidateVector
protected IIntList	changedFields
protected int[]	endCV
protected boolean	firstTestCase
protected int[]	startCV
protected StateSpace	stateSpace
(package private) Map<Object,Object>	visited

Constructor Summary

StateSpaceExplorer(IFinitization ifin)

Method Summary

IIntList	getAccessedFields() Gets the list of accessed fields during the last search.
int[]	getCandidateVector() Gets candidate vector that corresponds to the test case returned last.
protected boolean	getNextCandidate()
Object	nextTestCase() Searches for next test case.
private boolean	reachedEndCV()
void	reportCurrentAsValid() Reports the current test case as valid structure The current test case is the last one returned with nextTestCase.
void	setEndCandidateVector(int[] endCV)
void	setStartCandidateVector(int[] startCV)
protected void	touch(Object obj)
private void	touchArray(Object obj)
private void	touchField(int fldIndex)

Methods inherited from class java.lang.Object

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

Field Detail

stateSpace

protected StateSpace stateSpace

candidateBuilder

protected CandidateBuilder candidateBuilder

candidateVector

protected int[] candidateVector

startCV

protected int[] startCV

endCV

protected int[] endCV

accessedFields

protected IIntList accessedFields

changedFields

protected IIntList changedFields

firstTestCase

protected boolean firstTestCase

visited

Map<Object,Object> visited

Constructor Detail

StateSpaceExplorer

public StateSpaceExplorer(IFinitization ifin)

Method Detail

getAccessedFields

public IIntList getAccessedFields()

Description copied from interface: IKoratSearchStrategy

Gets the list of accessed fields during the last search.

Specified by:

getAccessedFields in interface IKoratSearchStrategy

Returns:

accessed fields

getCandidateVector

public int[] getCandidateVector()

Description copied from interface: IKoratSearchStrategy

Gets candidate vector that corresponds to the test case returned last.

Specified by:

getCandidateVector in interface IKoratSearchStrategy

Returns:

candidate vector

setEndCandidateVector

public void setEndCandidateVector(int[] endCV)

Specified by:

setEndCandidateVector in interface IKoratSearchStrategy

setStartCandidateVector

public void setStartCandidateVector(int[] startCV)

Specified by:

setStartCandidateVector in interface IKoratSearchStrategy

nextTestCase

public Object nextTestCase()

Description copied from interface: IKoratSearchStrategy

Searches for next test case. If state space has been exausted, returns null.

Specified by:

nextTestCase in interface IKoratSearchStrategy

Returns:

next test case

getNextCandidate

protected boolean getNextCandidate()

reachedEndCV

private boolean reachedEndCV()

reportCurrentAsValid

public void reportCurrentAsValid()

Description copied from interface: IKoratSearchStrategy

Reports the current test case as valid structure The current test case is the last one returned with nextTestCase. If this method is executed before first nextTestCase, the behaviour is undefined

Specified by:

reportCurrentAsValid in interface IKoratSearchStrategy

touch

protected void touch(Object obj)

touchField

private void touchField(int fldIndex)

touchArray

private void touchArray(Object obj)