~verifydtapn-contributers/verifydtapn/trunk

« back to all changes in this revision

Viewing changes to src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp

  • Committer: Jiri Srba
  • Date: 2015-08-31 12:39:10 UTC
  • mfrom: (324.3.24 PTrieWorkflow)
  • Revision ID: srba@cs.aau.dk-20150831123910-qwr9g6pq7zntajhe
merged in a big branch implementing PTrie for workflow analysis

Show diffs side-by-side

added added

removed removed

Lines of Context:
6
6
 */
7
7
 
8
8
#include "WorkflowSoundness.hpp"
 
9
#include <limits>
9
10
 
10
11
namespace VerifyTAPN {
11
12
namespace DiscreteVerification {
13
14
WorkflowSoundness::WorkflowSoundness(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking*>* waiting_list)
14
15
: Workflow(tapn, initialMarking, query, options), passedStack(), minExec(INT_MAX), linearSweepTreshold(3), coveredMarking(NULL), modelType(calculateModelType()){
15
16
    pwList = new WorkflowPWList(waiting_list);
 
17
 
16
18
}
17
19
 
18
20
 
21
23
    
22
24
};
23
25
 
 
26
WorkflowSoundnessPTrie::WorkflowSoundnessPTrie(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<ptriepointer_t<MetaData*> >* waiting_list)
 
27
: WorkflowSoundness(tapn, initialMarking, query, options) {
 
28
    int kbound = modelType == MTAWFN ? (std::numeric_limits<int>::max() - 1) : options.getKBound();
 
29
    pwList = new WorkflowPWListHybrid(  tapn,
 
30
                                        waiting_list, 
 
31
                                        kbound, 
 
32
                                        tapn.getNumberOfPlaces(), 
 
33
                                        tapn.getMaxConstant());
 
34
 
 
35
}
 
36
 
24
37
 
25
38
bool WorkflowSoundness::verify(){
26
39
        if(addToPW(&initialMarking, NULL)){
50
63
                                return false;
51
64
                        }
52
65
                }
 
66
                deleteMarking(next_marking);
53
67
        }
54
68
 
55
69
        // Phase 2
82
96
    return passed;
83
97
}
84
98
 
 
99
int WorkflowSoundnessPTrie::numberOfPassed()
 
100
{
 
101
    int passed = 0;
 
102
    while(passedStack.size()){
 
103
        WorkflowSoundnessMetaDataWithEncoding* next = 
 
104
        static_cast<WorkflowSoundnessMetaDataWithEncoding*>(passedStack.top());
 
105
        
 
106
        passedStack.pop();
 
107
        if(next->passed) continue;
 
108
        next->passed = true;
 
109
        ++passed;
 
110
        for(vector<MetaData*>::iterator iter = next->parents.begin();
 
111
                iter != next->parents.end(); iter++){
 
112
                passedStack.push(*iter);
 
113
        }
 
114
    }
 
115
    return passed;
 
116
}
 
117
 
85
118
 
86
119
bool WorkflowSoundness::addToPW(NonStrictMarking* marking, NonStrictMarking* parent){
87
120
        marking->cut(placeStats);
91
124
        // Check K-bound
92
125
        pwList->setMaxNumTokensIfGreater(size);
93
126
        if(modelType == ETAWFN && size > options.getKBound()) {
94
 
                lastMarking = marking;
 
127
                if(lastMarking != NULL) deleteMarking(lastMarking);
 
128
                lastMarking = marking;
 
129
                setMetaParent(lastMarking);
95
130
                return true;    // Terminate false
96
131
        }
97
132
 
101
136
        NonStrictMarking* old = pwList->addToPassed(marking, false);
102
137
        if(old == NULL){
103
138
                isNew = true;
104
 
                marking->meta = new WorkflowSoundnessMetaData();
105
 
                marking->setParent(parent);
106
139
        } else  {
107
140
            delete marking;
108
141
            marking = old;
130
163
                        marking->meta->totalDelay = min(marking->meta->totalDelay, parent->meta->totalDelay);   // Transition
131
164
                        // keep track of shortest trace
132
165
                        if (marking->meta->totalDelay < minExec) {
 
166
                            if(lastMarking != NULL) deleteMarking(lastMarking);
 
167
 
133
168
                            minExec = marking->meta->totalDelay;
134
169
                            lastMarking = marking;
135
170
                            return false;
136
171
                        }
137
172
                }else{
 
173
                        if(lastMarking != NULL) deleteMarking(lastMarking);
138
174
                        lastMarking = marking;
139
175
                        return true;    // Terminate false
140
176
                }
143
179
                if(isNew){
144
180
                        pwList->addLastToWaiting();
145
181
                        if(parent != NULL && marking->canDeadlock(tapn, 0)){
 
182
                                if(lastMarking != NULL) deleteMarking(lastMarking);
146
183
                                lastMarking = marking;
147
184
                                return true;
148
185
                        }
149
186
                        if(modelType == MTAWFN && checkForCoveredMarking(marking)){
150
 
                                lastMarking = marking;
 
187
                                if(lastMarking != NULL) deleteMarking(lastMarking);
 
188
                                lastMarking = marking;
151
189
                                return true;    // Terminate false
152
190
                        }
153
191
                }
154
192
        }
 
193
        deleteMarking(marking);
155
194
        return false;
156
195
}
157
196
 
162
201
 
163
202
}
164
203
 
 
204
void WorkflowSoundnessPTrie::addParentMeta(MetaData* meta, MetaData* parent)
 
205
{
 
206
    assert(meta != NULL);
 
207
    assert(parent != NULL);
 
208
    WorkflowSoundnessMetaDataWithEncoding* markingmeta = ((WorkflowSoundnessMetaDataWithEncoding*)meta);
 
209
    markingmeta->parents.push_back(parent);
 
210
 
 
211
}
165
212
 
166
213
bool WorkflowSoundness::checkForCoveredMarking(NonStrictMarking* marking){
167
214
        if(marking->size() <= options.getKBound()){
193
240
}
194
241
 
195
242
 
 
243
void WorkflowSoundnessPTrie::getTrace(NonStrictMarking* marking){
 
244
 
 
245
        PWListHybrid* pwhlist = dynamic_cast<PWListHybrid*>(this->pwList);
 
246
 
 
247
        stack < NonStrictMarking*> printStack;
 
248
 
 
249
        if(marking != NULL){
 
250
            printStack.push(marking);
 
251
            
 
252
            MetaDataWithTraceAndEncoding* meta = 
 
253
                static_cast<MetaDataWithTraceAndEncoding*>(marking->meta);
 
254
            if(meta)
 
255
            {
 
256
                marking->setGeneratedBy(meta->generatedBy);
 
257
 
 
258
                meta = meta->parent;
 
259
                while(meta != NULL)
 
260
                {
 
261
                    NonStrictMarking* next = pwhlist->decode(meta->ep);
 
262
                    printStack.push(next);
 
263
                    next->setGeneratedBy(meta->generatedBy);
 
264
                    printStack.top()->setParent(next);
 
265
                    meta = meta->parent;
 
266
                }
 
267
            }
 
268
            printStack.top()->setGeneratedBy(NULL);
 
269
        }
 
270
 
 
271
#ifdef CLEANUP
 
272
        stack < NonStrictMarking*> clearStack = printStack;
 
273
#endif
 
274
        printXMLTrace(marking, printStack, query, tapn);
 
275
#ifdef CLEANUP
 
276
        while(!clearStack.empty())
 
277
        {
 
278
            if(clearStack.top() == lastMarking) break;  // deleted elsewhere
 
279
            delete clearStack.top();
 
280
            clearStack.pop();
 
281
        }
 
282
#endif
 
283
}
 
284
 
 
285
 
 
286
void WorkflowSoundnessPTrie::setMetaParent(NonStrictMarking* marking){
 
287
    PWListHybrid* pwhlist = dynamic_cast<PWListHybrid*>(this->pwList);
 
288
    
 
289
    if(marking->meta == NULL)
 
290
    {
 
291
        marking->meta = new MetaDataWithTraceAndEncoding();
 
292
    }
 
293
 
 
294
    MetaDataWithTraceAndEncoding* mte = 
 
295
                static_cast<MetaDataWithTraceAndEncoding*>(marking->meta);
 
296
    mte->parent = pwhlist->parent;
 
297
    mte->generatedBy = marking->getGeneratedBy();
 
298
}
 
299
 
 
300
 
196
301
 
197
302
WorkflowSoundness::ModelType WorkflowSoundness::calculateModelType() {
198
303
            bool isin, isout;