gov.nasa.jpf.vm

Class DefaultBacktracker<KState>

java.lang.Object

gov.nasa.jpf.vm.DefaultBacktracker<KState>

All Implemented Interfaces:

Backtracker

public class DefaultBacktracker<KState>
extends java.lang.Object
implements Backtracker

Nested Class Summary

Nested classes/interfaces inherited from interface gov.nasa.jpf.vm.Backtracker

Backtracker.RestorableState

Field Summary

Fields

Modifier and Type	Field and Description
protected ImmutableList<KState>	kstack where we keep the saved KernelState head
protected StateRestorer<KState>	restorer
protected SystemState	ss
protected ImmutableList<java.lang.Object>	sstack and that adds the SystemState specifics

Constructor Summary

Constructors

Constructor and Description
DefaultBacktracker()

Method Summary

Modifier and Type	Method and Description
void	attach(VM vm)
boolean	backtrack() Moves one step backward.
protected void	backtrackKernelState()
protected void	backtrackSystemState()
Backtracker.RestorableState	getRestorableState()
void	pushKernelState() Saves the state of the system.
void	pushSystemState() Saves the backtracking information.
void	restoreState(Backtracker.RestorableState state)

Methods inherited from class java.lang.Object

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

Field Detail

kstack

protected ImmutableList<KState> kstack

where we keep the saved KernelState head

sstack

protected ImmutableList<java.lang.Object> sstack

and that adds the SystemState specifics

ss

protected SystemState ss

restorer

protected StateRestorer<KState> restorer

Constructor Detail

DefaultBacktracker

public DefaultBacktracker()

Method Detail

attach

public void attach(VM vm)

Specified by:

attach in interface Backtracker

backtrackKernelState

protected void backtrackKernelState()

backtrackSystemState

protected void backtrackSystemState()

backtrack

public boolean backtrack()

Moves one step backward. This method and forward() are the main methods used by the search object. Note this is called with the state that caused the backtrack still being on the stack, so we have to remove that one first (i.e. popping two states and restoring the second one)

Specified by:

backtrack in interface Backtracker

pushKernelState

public void pushKernelState()

Saves the state of the system.

Specified by:

pushKernelState in interface Backtracker

pushSystemState

public void pushSystemState()

Saves the backtracking information.

Specified by:

pushSystemState in interface Backtracker

restoreState

public void restoreState(Backtracker.RestorableState state)

Specified by:

restoreState in interface Backtracker

getRestorableState

public Backtracker.RestorableState getRestorableState()

Specified by:

getRestorableState in interface Backtracker