1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0//EN">
<HTML><HEAD>
<TITLE>The format of the disk-based reachability graph files</TITLE>
<LINK REV=MADE HREF="mailto:msmakela@tcs.hut.fi">
</HEAD>
<BODY>
<H1>The format of the disk-based reachability graph files</H1>
<P>The machine-dependent disk-based reachability graph files are
handled by the class <CODE>Graph</CODE>. There are four files: a <A
HREF="#rgd">directory</A> (having a suffix <CODE>.rgd</CODE>), a <A
HREF="#rgs">state file</A> (<CODE>.rgs</CODE>), containing the global
marking of the Petri Net in each state (node of the reachability
graph), an <A HREF="#rga">arc file</A> (<CODE>.rga</CODE>), containing
the events leading from one state to another, and a <A
HREF="#rgh">hash map</A> (<CODE>.rgh</CODE>) of generated states.</P>
<H2><A NAME="rgd">The reachability graph directory</A> (<CODE>.rgd</CODE>)</H2>
<P>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.</P>
<TABLE>
<TR><TH>Item</TH><TH>Size</TH></TR>
<TR>
<TD>magic cookie (text)</TD>
<TD><CODE>sizeof magic</CODE></TD>
</TR>
<TR>
<TD>name of the Petri Net</TD>
<TD>a NUL-terminated string</TD>
</TR>
<TR>
<TD>optional padding to make the rest of the file word-aligned</TD>
<TD><CODE>0</CODE> to <CODE>sizeof (Graph::fpos_t)-</CODE></TD>
</TR>
<TR>
<TD>number of states</TD>
<TD><CODE>sizeof (unsigned)</CODE></TD>
</TR>
<TR>
<TD>number of arcs</TD>
<TD><CODE>sizeof (unsigned)</CODE></TD>
</TR>
<TR>
<TD>offsets in the <A HREF="#rgs">state</A>,
<A HREF="#rga">arc</A> and <A HREF="#rgp">predecessor state</A> files<BR>
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.</TD>
<TD><CODE>numStates * (3 * sizeof (fpos_t))</CODE></TD>
</TR>
</TABLE>
<H2><A NAME="rgs">The state file</A> (<CODE>.rgs</CODE>)</H2>
<P>The state file contains the encoded representations of the states
(contents of <CODE>BitPacker::myBuf</CODE>), stored as bytes. The
file is accessed by seeking to the offset recorded in the <A
HREF="#rgd">graph directory</A>.</P>
<H2><A NAME="rga">The arc file</A> (<CODE>.rga</CODE>)</H2>
<P>The arc file contains the events (transition instances) between
states. Each event has a source state (implicit from the <A
HREF="#rgd">graph directory</A>) and a target state.</P>
<P>An offset in the <A HREF="#rgd">graph directory</A> 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
<CODE>card_t</CODE> specifies the target state numbers of the arcs.
This array is followed by a bit string that contains the encoded
transition instances.</P>
<H2><A NAME="rgp">The predecessor state file</A> (<CODE>.rgp</CODE>)</H2>
<P>The predecessor state file is a singly linked list of state numbers
and file offsets. The records are pairs of file offsets
(<CODE>fpos_t</CODE>) and state numbers (<CODE>card_t</CODE>). An
offset of -1 (all bits set) indicates the end of the list.</P>
<H2><A NAME="rgh">The hash map of generated states</A> (<CODE>.rgh</CODE>)</H2>
<P>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.</P>
<P>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).</P>
<P>Words 1 through 255 contain the keys, hash values of encoded
states, in ascending order. Unused entries are zeros.</P>
<P>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.</P>
<P>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.</P>
</BODY></HTML>
|
