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
|
// Dummy reporter of successor states in unfolding -*- c++ -*-
#ifndef DUMMYREPORTER_H_
# define DUMMYREPORTER_H_
# ifdef __GNUC__
# pragma interface
# endif // __GNUC__
# include "StateReporter.h"
# include "Search.h"
/** @file DummyReporter.h
* Interface for reporting successor states in unfolding
*/
/* Copyright 2002-2003 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. */
/** Dummy reporter of successor states in unfolding */
class DummyReporter : public StateReporter
{
public:
/** Constructor
* @param net_ the net that is being analysed
* @param printer_ printer object for diagnostic output
* @param maxerrors maximum number of allowed errors (0=infinity)
*/
DummyReporter (const class Net& net_,
const class Printer& printer_,
unsigned maxerrors) :
StateReporter (
# ifdef EXPR_COMPILE
0,
# endif // EXPR_COMPILE
net_, printer_, maxerrors, false, false, true) {}
private:
/** Copy constructor */
DummyReporter (const class DummyReporter& old);
/** Assignment operator */
class DummyReporter& operator= (const class DummyReportert& other);
public:
/** Destructor */
~DummyReporter () {}
private:
/** Add an encoded state to the state space
* @param state the encoded state
* @param size length of the encoded state in bytes
* @return true if the state was new
*/
bool do_addState (const void* state,
size_t size);
/** 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, or NULL if none available
*/
word_t* do_popState (bool tail, size_t& size);
/** Dequeue an unprocessed state
* @param breadth true=dequeue (FIFO, queue), false=pop (LIFO, stack)
* @return an unprocessed state, or NULL if all processed
*/
class GlobalMarking* pop (bool breadth);
# ifdef EXPR_COMPILE
/** Dequeue an unprocessed state
* @param breadth true=dequeue (FIFO, queue), false=pop (LIFO, stack)
* @return true if a state was found, or false if all processed
*/
bool popCompiled (bool breadth);
# endif // EXPR_COMPILE
/** Report a successor state
* @param transition the transition fired
* @param valuation the binding of the transition
* @param marking the resulting marking
* @param rejected flag: is the state rejected?
* @return true if analysis should proceed; false on fatal error
*/
bool report (const class Transition& transition,
const class Valuation& valuation,
const class GlobalMarking& marking,
bool rejected);
/** Report a deadlock or an error in the current state
* @param deadlock flag: is this a deadlock?
*/
void reportError (bool deadlock);
public:
# ifdef EXPR_COMPILE
/** Report a successor state
* @param state the resulting encoded deflated state (mandatory)
* @param size length of the encoded state, in bytes
* @param rejected flag: is the state rejected?
* @param hidden flag: is the transition to the state hidden?
* @return true if analysis should proceed; false on error
*/
bool report (const void* state,
size_t size,
bool rejected,
bool hidden);
# endif // EXPR_COMPILE
private:
/** Report an inconsistent successor state */
void reject ();
};
#endif // DUMMYREPORTER_H_
|
