← Back to branch summary

~peter-gjoel/verifydtapn/PTrieWorkflow

« back to all changes in this revision

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

  • Committer: Peter Gjøl Jensen
  • Date: 2015-06-22 14:45:39 UTC
  • Revision ID: peter.gjoel@gmail.com-20150622144539-skkruwkgsx3gnuao
strong-workflow + ptrie checked for leaks and memmory-corruption. Has controlled leak of two markings, not fixed as this would clutter up the code even more

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp
118
118
        // Check K-bound
119
119
        pwList->setMaxNumTokensIfGreater(size);
120
120
        if(modelType == ETAWFN && size > options.getKBound()) {
121
 
                lastMarking = marking;
 
121
                if(lastMarking != NULL) deleteMarking(lastMarking);
 
122
                lastMarking = marking;
122
123
                setMetaParent(lastMarking);
123
124
                return true;    // Terminate false
124
125
        }
154
155
                        marking->meta->totalDelay = min(marking->meta->totalDelay, parent->meta->totalDelay);   // Transition
155
156
                        // keep track of shortest trace
156
157
                        if (marking->meta->totalDelay < minExec) {
 
158
                            if(lastMarking != NULL) deleteMarking(lastMarking);
157
159
                            minExec = marking->meta->totalDelay;
158
160
                            lastMarking = marking;
 
161
                            return false;
159
162
                        }
160
163
                        
161
164
                }else{
 
165
                        if(lastMarking != NULL) deleteMarking(lastMarking);
162
166
                        lastMarking = marking;
163
167
                        return true;    // Terminate false
164
168
                }
167
171
                if(isNew){
168
172
                        pwList->addLastToWaiting();
169
173
                        if(parent != NULL && marking->canDeadlock(tapn, 0)){
 
174
                                if(lastMarking != NULL) deleteMarking(lastMarking);
170
175
                                lastMarking = marking;
171
176
                                return true;
172
177
                        }
173
178
                        if(modelType == MTAWFN && checkForCoveredMarking(marking)){
174
 
                                lastMarking = marking;
 
179
                                if(lastMarking != NULL) deleteMarking(lastMarking);
 
180
                                lastMarking = marking;
175
181
                                return true;    // Terminate false
176
182
                        }
177
183
                }
178
184
        }
 
185
        deleteMarking(marking);
179
186
        return false;
180
187
}
181
188
 
370
377
        }
371
378
 
372
379
WorkflowSoundness::~WorkflowSoundness() {
 
380
    pwList->deleteWaitingList();
 
381
    delete pwList;
373
382
}
374
383
 
375
384
} /* namespace DiscreteVerification */