-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathSCIndetVal.h
193 lines (159 loc) · 9.97 KB
/
SCIndetVal.h
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
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
/*-----------------------------------------------------------------------------+
| |
| SCL - Simulation Class Library |
| |
| (c) 1994-98 Marc Diefenbruch, Wolfgang Textor |
| University of Essen, Germany |
| |
+---------------+-------------------+---------------+-------------------+------+
| Module | File | Created | Project | |
+---------------+-------------------+---------------+-------------------+------+
| SCIndetVal | SCIndetVal.h | 25. Apr 1996 | SCL | |
+---------------+-------------------+---------------+-------------------+------+
| |
| Change Log |
| |
| Nr. Date Description |
| ----- -------- ------------------------------------------------------ |
| 001 |
| 000 --.--.-- Neu angelegt |
| |
+-----------------------------------------------------------------------------*/
/* Lineal
00000000001111111111222222222233333333334444444444555555555566666666667777777777
01234567890123456789012345678901234567890123456789012345678901234567890123456789
*/
#ifndef __SCINDETVAL__
#define __SCINDETVAL__
#include "SCBasicTypes.h"
#include "SCIndet.h"
#include "SCActiveRunnableList.h"
class SCIndetVal : public SCIndet
{
public:
SCIndetVal (SCTime stopTime,
SCBoolean errors,
SCNatural maxNumOfErrors,
SCBoolean deadCode,
SCBoolean doCycleDetection,
class SCStateSpace *stateSpace,
class SCStateSpace *cycleStateSpace,
SCNatural maxValDepth = kSCMaxDepth,
SCNatural maxNumOfCreatedInstances = kSCMaxCreatedInstances,
SCName2PropFuncPtr * qAtom = NULL,
SCIndetType = scIndetValidation);
virtual ~SCIndetVal (void);
SCNatural NonDetChoice (const SCNatural range);
SCNatural ChooseOneTrue (const SCNatural choiceSize,
const SCNatural numOfTrues,
const SCNatural singleTrue,
const SCBoolean *choiceSet);
class SCRunnable * ChooseRunnable (SCTimeEventSaveList *activeQueue);
class SCEnabledTransition * ChooseTransition (void);
void StartMessage (void);
void EndMessage (void);
void SwitchToNestedDFS (void);
void SwitchToOrigDFS (SCBoolean cycleFound);
// The following three methods classify the reached system
// state:
SCErrorCode IsErrorState (SCTimeEventSaveList *activeQueue);
SCBoolean IsLimitingState (SCTimeEventSaveList *activeQueue);
virtual SCBoolean IsCycleStartState (void) const;
virtual SCBoolean IsCycleEndState (SCMem *state);
SCBoolean Create (SCProcessID offspring);
class SCStack * GetStack (void) const;
class SCStack * GetFirstStack (void) const;
class SCStack * GetSecondStack (void) const;
class SCStateSpace * GetCurrentStateSpace (void) const;
class SCStateSpace * GetStateSpace (void) const;
class SCStateSpace * GetCycleStateSpace (void) const;
SCErrorCode GetLastError (void) const;
SCNatural GetLastSuccessor (void) const;
class SCStackElem * GetCycleClosingElem (void) const;
// Virtual method for reporting current exploration depth
// default implementation in SCIndet return number of executed
// transition, but SCIndetVal must redefine it to report
// current stack length (-1):
SCNatural CurrentDepth (void) const;
SCBoolean LogError (SCErrorCode errorCode); // deadlock
SCBoolean LogError (SCErrorCode errorCode, // signal drop or
const class SCProcess *process, // signal rejected
const class SCSignal *signal);
SCBoolean LogError (SCErrorCode errorCode, // no receiver
const class SCProcess *process,
const class SCSignalType *signal);
SCBoolean LogError (SCErrorCode errorCode, // process creation
const class SCProcess *parent, // failed
const class SCProcessType *offspringType);
friend SCStream & operator<< (SCStream& pStream,
const SCIndetVal& pData);
virtual SCStream & Display (SCStream &pStream) const;
protected:
virtual void SystemStateSize (SCSize *pSize) const;
virtual SCBoolean StoreSystemState(class SCMem *state) const;
virtual SCBoolean RestoreSystemState(class SCMem *state) const;
class SCStack * currentStack;
class SCStack * theFirstStack;
class SCStack * theSecondStack;
class SCStateSpace * currentStateSpace;
class SCStateSpace * theStateSpace;
class SCStateSpace * theCycleStateSpace;
SCBitSet fulfilledAcceptanceSets; // This bit-field has one bit for every
// set of acceptance states.
// If all bits are set, it means
// that at least one state of
// every acceptance has been
// explored. In this
// case, all bits are reset to
// zero. This way, the set
// "counts modulo". At a given
// state one can store the
// current value of
// fulfilledAcceptanceSets, before it
// is updated. If a state with the
// same value for leftObligations
// is reached, this
// means that in the meantime, at
// least one state out of every
// acceptance state set has been
// reached. Useful for cycle
// detection.
SCNatural flipCounter; // counts how often the bits
// of fulfilledAcceptanceSets are
// reset to zero
SCErrorCode lastError; // last occured error
private:
/* Alle weiteren Datenmember sind privat */
SCProcessID * createdInstances; // IDs of created processes
SCNatural numOfCreatedInstances; // num of already created Inst.
SCNatural maxNumOfCreatedInstances; // max num of created Inst.
SCNatural truncatedPathes; // num of truncated pathes
SCBoolean cycleDetection; // detect cycles in reachability
// graph?
SCBoolean isInCycleDetection; // currently doing nested DFS for
// cycle detection?
SCBoolean lastRunnableIsAutomaton; // active runnable is automaton
SCProcessID lastRunnableID; // stores ID of the runnable
// which executed the transition
// leading to the current state
// (for process)
class SCRunnable * lastRunnable; // stores pointer to the runnable
// which executed the transition
// leading to the current state
// (for timer or machine)
class SCEnabledTransition * lastTransition; // stores pointer to the transition
// leading to the current state
// together with signal ID
SCNatural lastSuccessor; // Buechi-Successor
class SCIndetStackTrace * theIndetStack; // special indet object for
// trace generation
SCNatural minStateSize;
SCNatural maxStateSize;
class SCStackElem * cycleClosingElem;
SCNatural numOfCycleStartStates; // number of nested DFS
friend class SCIndetStackTrace;
};
#if !_SC_NOINLINES
#include "SCIndetVal.inl.h"
#endif
#endif // __SCINDETVAL__