avrora.stack
Class AbstractState

java.lang.Object
  avrora.stack.AbstractState

All Implemented Interfaces:

IORegisterConstants

Direct Known Subclasses:

MutableState, StateCache.State

public abstract class AbstractState

extends java.lang.Object

implements IORegisterConstants

The AbstractState class represents an abstract state within the state space. The program counter, the status register, the registers, and the interrupt mask register are modelled.

Field Summary

protected char	av_EIMSK
protected char[]	av_REGISTERS
protected char	av_SREG
protected char	av_TIMSK
protected int	pc
static int[]	primes The primes field stores the first 32 prime integers that follow 2.

Fields inherited from interface avrora.stack.IORegisterConstants

ACSR, ADCH, ADCL, ADCSRA, ADMUX, ASSR, DDRA, DDRB, DDRC, DDRD, DDRE, DDRF, DDRG, EEARH, EEARL, EECR, EEDR, EICRA, EICRB, EIFR, EIMSK, ETIFR, ETIMSK, ICR1H, ICR1L, ICR3H, ICR3L, MCUCR, MCUCSR, NUM_REGS, OCDR, OCR0, OCR1AH, OCR1AL, OCR1BH, OCR1BL, OCR1CH, OCR1CL, OCR2, OCR3AH, OCR3AL, OCR3BH, OCR3BL, OCR3CH, OCR3CL, OSCCAL, PINA, PINB, PINC, PIND, PINE, PINF, PING, PORTA, PORTB, PORTC, PORTD, PORTE, PORTF, PORTG, RAMPZ, SFIOR, SPCR, SPDR, SPH, SPL, SPMCSR, SPSR, SREG, SREG_C, SREG_H, SREG_I, SREG_N, SREG_S, SREG_T, SREG_V, SREG_Z, TCCR0, TCCR1A, TCCR1B, TCCR1C, TCCR2, TCCR3A, TCCR3B, TCCR3C, TCNT0, TCNT1H, TCNT1L, TCNT2, TCNT3H, TCNT3L, TIFR, TIMSK, TWAR, TWBR, TWCR, TWDR, TWSR, UBRR0H, UBRR0L, UBRR1H, UBRR1L, UCSR0A, UCSR0B, UCSR0C, UCSR1A, UCSR1B, UCSR1C, UDR0, UDR1, WDTCR, XDIV, XMCRA, XMCRB

Method Summary

protected int	computeHashCode()
MutableState	copy() The copy() method returns a deep copy of this state.
protected boolean	deepCompare(StateCache.State i)
abstract boolean	equals(java.lang.Object o)
char	getFlag_C() The getFlag_C() method returns the abstract value of the C flag.
char	getFlag_H() The getFlag_H() method returns the abstract value of the H flag.
char	getFlag_I() The getFlag_I() method returns the abstract value of the I flag.
char	getFlag_N() The getFlag_N() method returns the abstract value of the N flag.
char	getFlag_S() The getFlag_S() method returns the abstract value of the S flag.
char	getFlag_T() The getFlag_T() method returns the abstract value of the T flag.
char	getFlag_V() The getFlag_V() method returns the abstract value of the V flag.
char	getFlag_Z() The getFlag_Z() method returns the abstract value of the Z flag.
char	getIORegisterAV(int num) The getIORegisterByte() method reads the abstract value of an IO register from the abstract state.
int	getPC() The getPC() method returns the concrete value of the program counter.
char	getRegisterAV(int num)
char	getRegisterAV(Register r) The getRegisterByte() method reads the abstract value of a register in the abstract state.
char	getSREG() The getSREG() method reads the abstract value of the status register.
abstract int	hashCode()
java.lang.String	toString()

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

pc

protected int pc

av_SREG

protected char av_SREG

av_EIMSK

protected char av_EIMSK

av_TIMSK

protected char av_TIMSK

av_REGISTERS

protected char[] av_REGISTERS

primes

public static final int[] primes

The primes field stores the first 32 prime integers that follow 2. This is used in the computation of the hash code.

Method Detail

computeHashCode

protected int computeHashCode()

hashCode

public abstract int hashCode()

equals

public abstract boolean equals(java.lang.Object o)

getPC

public int getPC()

The getPC() method returns the concrete value of the program counter. The program counter is known in every abstract state.

Returns:

the concrete value of the program counter

getSREG

public char getSREG()

The getSREG() method reads the abstract value of the status register.

Returns:

the abstract value of the status register

getFlag_I

public char getFlag_I()

The getFlag_I() method returns the abstract value of the I flag.

Returns:

the new abstract bit of the flag

getFlag_T

public char getFlag_T()

The getFlag_T() method returns the abstract value of the T flag.

Returns:

the new abstract bit of the flag

getFlag_H

public char getFlag_H()

The getFlag_H() method returns the abstract value of the H flag.

Returns:

the new abstract bit of the flag

getFlag_S

public char getFlag_S()

The getFlag_S() method returns the abstract value of the S flag.

Returns:

the new abstract bit of the flag

getFlag_V

public char getFlag_V()

The getFlag_V() method returns the abstract value of the V flag.

Returns:

the new abstract bit of the flag

getFlag_N

public char getFlag_N()

The getFlag_N() method returns the abstract value of the N flag.

Returns:

the new abstract bit of the flag

getFlag_Z

public char getFlag_Z()

The getFlag_Z() method returns the abstract value of the Z flag.

Returns:

the new abstract bit of the flag

getFlag_C

public char getFlag_C()

The getFlag_C() method returns the abstract value of the C flag.

Returns:

the new abstract bit of the flag

getIORegisterAV

public char getIORegisterAV(int num)

The getIORegisterByte() method reads the abstract value of an IO register from the abstract state. For those registers being modelled, this will return an abstract value that represents the current value of the IO register. For IO registers that are not being modelled, it will return the abstract value corresponding to all bits being unknown.

Parameters:

num - the IO register number to read

Returns:

the (abstract) value of the specified IO register

getRegisterAV

public char getRegisterAV(Register r)

The getRegisterByte() method reads the abstract value of a register in the abstract state.

Parameters:

r - the register to read

Returns:

the abstract value of the register

getRegisterAV

public char getRegisterAV(int num)

copy

public MutableState copy()

The copy() method returns a deep copy of this state. This is generally used for forking operations and for storing internal copies within the StateSpace.

Returns:

a new deep copy of this abstract state

toString

public java.lang.String toString()

deepCompare

protected boolean deepCompare(StateCache.State i)