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
|
// Hash compacted storage of a reachable state set -*- c++ -*-
#ifndef COMPACTSET_H_
# define COMPACTSET_H_
# ifdef __GNUC__
# pragma interface
# endif // __GNUC__
# include "StateSet.h"
/** @file CompactSet.h
* Transient, hash compacted reachability set storage
*/
/* Copyright 2002 Marko Mkel (msmakela@tcs.hut.fi).
This file is part of MARIA, a reachability analyzer and model checker
for high-level Petri nets.
MARIA is free software; you can redistribute it and/or modify it
under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2, or (at your option)
any later version.
MARIA is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
General Public License for more details.
The GNU General Public License is often shipped with GNU software, and
is generally kept in a file called COPYING or LICENSE. If you do not
have a copy of the license, write to the Free Software Foundation,
59 Temple Place, Suite 330, Boston, MA 02111 USA. */
/** Hash compacted storage of a set of reachable states */
class CompactSet : public StateSet
{
public:
/** Constructor
* @param size number of elements in the hash table
* @param width length of the compacted hash values in bytes
*/
CompactSet (unsigned size,
unsigned width);
private:
/** Copy constructor */
CompactSet (const class CompactSet& old);
/** Assignment operator */
class CompactSet& operator= (const class CompactSet& old);
public:
/** Destructor */
~CompactSet ();
/** Initialize the hash tables
* @return true if the initialization succeeded
*/
bool init ();
/** Get the number of hash collisions */
unsigned getNumCollisions () const { return myNumCollisions; }
/** Get the size of the hash table */
unsigned getHashSize () const { return myHashSize; }
private:
/** Add a state to the graph
* @param state the encoded state
* @param size length of the encoded state, in bytes
* @return true if the state was enqueued to mySearch
*/
bool do_add (const void* state,
size_t size);
protected:
/** Get a deflated state from myPathFile
* @param pos file offset to the state
* @param size (output) length of the encoded state
*/
word_t* getState (long pos, size_t* size) const;
public:
/** Fetch an encoded state
* @param tail flag: retrieve from tail of list instead of head
* @param size (output) length of the encoded stream
* @return the encoded state
*/
word_t* pop (bool tail, size_t& size);
private:
/** Fetch a state from a counterexample path
* @param u cursor to the counterexample path
* @return the encoded state, inflated
*/
word_t* getState (class ByteUnpacker& u) const;
/** Number of hash collisions */
unsigned myNumCollisions;
/** Number of elements in the hash tables (a prime close to a power of 2) */
const unsigned myHashSize;
/** Length of the compacted hash values in bytes */
const unsigned myHashWidth;
/** The word-aligned part of hash table */
unsigned* myMajorHash;
/** The octet-aligned part of the hash table */
unsigned char* myMinorHash;
};
#endif // COMPACTSET_H_
|
