The format of the disk-based reachability graph files

The machine-dependent disk-based reachability graph files are handled by the class Graph. There are four files: a directory (having a suffix .rgd), a state file (.rgs), containing the global marking of the Petri Net in each state (node of the reachability graph), an arc file (.rga), containing the events leading from one state to another, and a hash map (.rgh) of generated states.

The reachability graph directory (.rgd)

The directory begins with a magic cookie and the file name of the model being analyzed. Following them is an index to all states of the net.

ItemSize
magic cookie (text) sizeof magic
name of the Petri Net a NUL-terminated string
optional padding to make the rest of the file word-aligned 0 to sizeof (Graph::fpos_t)-
number of states sizeof (unsigned)
number of arcs sizeof (unsigned)
offsets in the state, arc and predecessor state files
Setting the most significant bit of the state offset indicates an erroneous state. An arc offset of -2 (all except the least significant bit set) indicates that the state has no successors. An arc offset of -1 (all bits set) indicates that the successors have not been generated. A predecessor state offset of -1 indicates that no predecessors have been stored for the state.
numStates * (3 * sizeof (fpos_t))

The state file (.rgs)

The state file contains the encoded representations of the states (contents of BitPacker::myBuf), stored as bytes. The file is accessed by seeking to the offset recorded in the graph directory.

The arc file (.rga)

The arc file contains the events (transition instances) between states. Each event has a source state (implicit from the graph directory) and a target state.

An offset in the graph directory points to an encoded successor arc record. The length of the encoded transition instances (in bytes) and the number of successor states are stored using a byte-aligned variable-length code. An following array of card_t specifies the target state numbers of the arcs. This array is followed by a bit string that contains the encoded transition instances.

The predecessor state file (.rgp)

The predecessor state file is a singly linked list of state numbers and file offsets. The records are pairs of file offsets (fpos_t) and state numbers (card_t). An offset of -1 (all bits set) indicates the end of the list.

The hash map of generated states (.rgh)

The hash file, implemented as a 256-degree B-tree, maps hash values of encoded states to state numbers. The file consists of blocks of 512 words.

The first word, word 0, contains the number of keys (0 to 255) and a flag that indicates whether the B-tree node is internal (containing links to further B-tree nodes), or a leaf node (containing state numbers).

Words 1 through 255 contain the keys, hash values of encoded states, in ascending order. Unused entries are zeros.

In an internal node, words 256 through 511 contain links to B-trees, zero-based node numbers. Node 0 is the root of the tree. The nodes are stored sequentially in the B-tree file.

In a leaf node, word 256 is unused, and words 257 through 511 contain state numbers. Word 257 contains the state number corresponding the hash value in word 1; the state number in word 258 is associated with the key in word 2, and so on. A leaf node may contain up to 255 state numbers.