pipe.io
Class RGFileHeader
java.lang.Object
pipe.io.RGFileHeader
public class RGFileHeader
- extends java.lang.Object
Constructor Summary |
RGFileHeader()
Sets up a blank Reachability Graph File Header Object |
RGFileHeader(int ns,
int ss,
int nt,
int trs,
long offset)
Sets up a Reachability Graph File Header Object ready
for writing. |
RGFileHeader(java.io.RandomAccessFile input)
|
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
RGFileHeader
public RGFileHeader(int ns,
int ss,
int nt,
int trs,
long offset)
- Sets up a Reachability Graph File Header Object ready
for writing.
RGFileHeader
public RGFileHeader(java.io.RandomAccessFile input)
throws IncorrectFileFormatException,
java.io.IOException
- Throws:
IncorrectFileFormatException
java.io.IOException
RGFileHeader
public RGFileHeader()
- Sets up a blank Reachability Graph File Header Object
write
public void write(java.io.RandomAccessFile outputfile)
throws java.io.IOException
- Throws:
java.io.IOException
read
public void read(java.io.RandomAccessFile inputfile)
throws java.io.IOException,
IncorrectFileFormatException
- Throws:
java.io.IOException
IncorrectFileFormatException
getNumStates
public int getNumStates()
getStateArraySize
public int getStateArraySize()
getNumTransitions
public int getNumTransitions()
getTransitionRecordSize
public int getTransitionRecordSize()
getOffsetToTransitions
public long getOffsetToTransitions()