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.
.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.
Item | Size |
---|---|
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)) |
.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.
.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.
.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.
.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.