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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
|
// Storage of encoded states -*- c++ -*-
#ifndef STATESET_H_
# define STATESET_H_
# ifdef __GNUC__
# pragma interface
# endif // __GNUC__
# include "StateList.h"
# include <stdio.h>
/** @file StateSet.h
* Set of reached states, represented with bit vectors
*/
/* 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. */
/** Set of reached states */
class StateSet
{
public:
/** codes reported from worker to server */
enum Code {
initialState, //< report the initial state
addStates, //< add successor states
deadlockState, //< notify of a rejected deadlock state
deadlockFatal, //< notify of a fatally rejected deadlock
rejectState, //< notify of a rejected state
rejectFatal, //< notify of a fatally rejected state
propertyError, //< notify of property evaluation error
inconsistent //< notify of an inconsistent successor state
};
/** Constructor */
StateSet () :
myNumStates (0), myNumArcs (0), mySearch (),
myPathFile (0), myPathFileLength (0), myOffset (0) {}
private:
/** Copy constructor */
StateSet (const class StateSet& old);
/** Assignment operator */
class StateSet& operator= (const class StateSet& old);
public:
/** Destructor */
virtual ~StateSet () {
if (myPathFile) fclose (myPathFile);
}
/** Get the number of states */
unsigned getNumStates () const { return myNumStates; }
/** Get the number of arcs (number of add () invocations) */
unsigned getNumArcs () const { return myNumArcs - 1; }
/** Get the number of unprocessed states */
unsigned getNumPending () const { return mySearch.size (); }
/** Open the counterexample path file
* @return true on success; false on failure
*/
bool openFile ();
/** Display path to a rejected state
* @param dstate the encoded rejected state
* @param dlen length of dstate in bytes
* @param reporter the state reporter
* @param reason reason for rejecting the state
* @param reduced flag: is this a reduced state space?
*/
virtual void reject (const void* dstate,
size_t dlen,
const class StateSetReporter& reporter,
enum Code reason,
bool reduced) const;
/** Display subpath to a state in a recovered state space
* @param dstate the encoded rejected state (0=deadlock)
* @param dlen length of dstate in bytes
* @param reporter the state reporter
*/
void displayPath (const void* dstate, size_t dlen,
const class StateSetReporter& reporter) const;
/** Add a state to the set
* @param state the encoded state
* @param size length of the encoded state, in bytes
* @return true if the state was enqueued to mySearch
*/
bool add (const void* state,
size_t size) {
myNumArcs++;
return do_add (state, size);
}
private:
/** Add a state to the set
* @param state the encoded state
* @param size length of the encoded state, in bytes
* @return true if the state was enqueued to mySearch
*/
virtual bool do_add (const void* state,
size_t size) = 0;
protected:
/** Increment the state count */
void newState () { myNumStates++; }
/** Get a deflated state from myPathFile
* @param pos file offset to the state
* @param size (output) length of the encoded state
*/
virtual 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
*/
virtual word_t* pop (bool tail, size_t& size) = 0;
/** Set the offset to the counterexample path file */
void setOffset (long offset) { myOffset = offset; }
/** Read the offset to the counterexample path file */
long getOffset () const { return myOffset; }
private:
/** Number of generated states */
unsigned myNumStates;
/** Number of generated arcs (invocations to add ()) */
unsigned myNumArcs;
protected:
/** The search list of states */
class StateList mySearch;
/** Counterexample path file */
FILE* myPathFile;
/** Used length of counterexample path file */
long myPathFileLength;
/** Current state offset in the counterexample path file */
long myOffset;
# if defined __sgi && !defined __GNUC__
public:
# endif // MIPS CC bug work-around
};
#endif // STATESET_H_
|
