Overview | Package | Class | Tree | Deprecated | Index | Help
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## 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)`

Method Summary
`int` | `getNumStates()`
`int` | `getNumTransitions()`
`long` | `getOffsetToTransitions()`
`int` | `getStateArraySize()`
`int` | `getTransitionRecordSize()`
`void` | `read(java.io.RandomAccessFile inputfile)`
`void` | `write(java.io.RandomAccessFile outputfile)`

Methods inherited from class java.lang.Object
`clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait`

Constructor Detail

### 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

Method Detail

### 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()

Overview | Package | Class | Tree | Deprecated | Index | Help
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD