← Back to branch summary

~verifydtapn-contributers/verifydtapn/d2.1

« back to all changes in this revision

Viewing changes to src/DiscreteVerification/DataStructures/PTrie.h

  • Committer: Jiri Srba
  • Date: 2013-08-29 18:03:55 UTC
  • mfrom: (276.4.20 nonBoostNonLeak)
  • Revision ID: srba@cs.aau.dk-20130829180355-8jrwr9hmcf1nplin
merged in branch removing memory leaks in the nonboost version 

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/DiscreteVerification/DataStructures/PTrie.h
31
31
            // The encoding is cloned as it is not persistant in the PTrie
32
32
            EncodingPointer(EncodingStructure<T*> &en, unsigned int n) : encoding(en.clone()), node(n) {
33
33
            }
 
34
            
 
35
            ~EncodingPointer(){
 
36
 
 
37
            }
 
38
            
34
39
        };
35
40
        
36
41
        template<typename T>
48
53
                };
49
54
            };
50
55
 
51
 
            struct PNode {
52
 
                MarkingEncoding* data;
 
56
            class PNode {
 
57
            public:
 
58
                PNode() : highpos(0), lowpos(0), highCount(-1), lowCount(-1), parent(0), data(NULL) {
 
59
                }
 
60
                
 
61
                inline void replaceData(MarkingEncoding* newData){
 
62
                    delete[] data;
 
63
                    data = newData;
 
64
                }
 
65
                inline MarkingEncoding* getData(){
 
66
                    return data;
 
67
                }
 
68
                
53
69
                uint highpos;
54
70
                uint lowpos;
55
71
                short int highCount;
56
72
                short int lowCount;
57
73
                uint parent;
 
74
            private:
 
75
                MarkingEncoding* data;
58
76
            };
59
77
 
60
78
 
72
90
                stored = 0;
73
91
                totalSize = blockSize;
74
92
                this->pnodeArray.push_back(new PNode[this->totalSize]);
75
 
                memset(this->pnodeArray[0], 0xffffffff, this->totalSize * sizeof (PNode));
76
 
                pnodeArray[0][0].data = NULL;
77
93
                pnodeArray[0][0].highCount = pnodeArray[0][0].lowCount = 0;
78
94
                pnodeArray[0][0].lowpos = pnodeArray[0][0].highpos = 0;
79
95
                pnodeArray[0][0].parent = 0;
288
304
            int ins = 0;
289
305
 
290
306
            for (; ins < listsize; ins++) {
291
 
                if (prev_node->data[ins] == en) {
 
307
                if (prev_node->getData()[ins] == en) {
292
308
                    break;
293
309
                }
294
310
            }
295
311
            if (ins != listsize) {
296
 
                return Result(false, prev_node->data[ins], prev_count);
 
312
                return Result(false, prev_node->getData()[ins], prev_count);
297
313
            }
298
314
 
299
315
            en = MarkingEncoding(encoding, size, var, encsize);
303
319
            nlist[listsize] = en;
304
320
 
305
321
            for (int i = 0; i < listsize; i++) {
306
 
                nlist[i] = prev_node->data[i];
 
322
                nlist[i] = prev_node->getData()[i];
307
323
            }
308
 
            delete[] prev_node->data;
309
 
            prev_node->data = nlist;
 
324
            prev_node->replaceData(nlist);
310
325
 
311
326
 
312
327
            bool branch = encoding.at(var);
324
339
                PNode* c_node = &this->pnodeArray[floor(this->nextFree / this->blockSize)][this->nextFree % this->blockSize];
325
340
                if (branch) {
326
341
                    prev_node->highpos = this->nextFree;
327
 
                    c_node->data = new MarkingEncoding[testclist = prev_node->highCount];
 
342
                    c_node->replaceData(new MarkingEncoding[testclist = prev_node->highCount]);
328
343
                    prev_node->highCount = -1;
329
344
                    if (prev_node->lowCount > 0)
330
345
                        nlist = new MarkingEncoding[testnlist = prev_node->lowCount];
332
347
                        nlist = NULL;
333
348
                } else {
334
349
                    prev_node->lowpos = this->nextFree;
335
 
                    c_node->data = new MarkingEncoding[testclist = prev_node->lowCount];
 
350
                    c_node->replaceData(new MarkingEncoding[testclist = prev_node->lowCount]);
336
351
                    prev_node->lowCount = -1;
337
352
                    if (prev_node->highCount > 0)
338
353
                        nlist = new MarkingEncoding[testnlist = prev_node->highCount];
350
365
                int clistcount = 0;
351
366
                int nlistcount = 0;
352
367
                for (int i = 0; i < listsize + 1; i++) {
353
 
                    if (prev_node->data[i].at(npos) == branch) {
 
368
                    if (prev_node->getData()[i].at(npos) == branch) {
354
369
                        if (!(size % 8)) {
355
 
                            nee = MarkingEncoding(prev_node->data[i], 8);
 
370
                            nee = MarkingEncoding(prev_node->getData()[i], 8);
356
371
                            if (i == ins) {
357
372
                                en = nee;
358
373
                            }
359
 
                            prev_node->data[i].release();
 
374
                            prev_node->getData()[i].release();
360
375
                        } else {
361
 
                            nee = prev_node->data[i];
 
376
                            nee = prev_node->getData()[i];
362
377
                        }
363
378
                        if (nee.at((npos + 1) % 8)) {
364
379
                            c_node->highCount++;
365
380
                        } else {
366
381
                            c_node->lowCount++;
367
382
                        }
368
 
                        c_node->data[clistcount] = nee;
 
383
                        c_node->getData()[clistcount] = nee;
369
384
                        clistcount++;
370
385
                    } else {
371
 
                        nlist[nlistcount] = prev_node->data[i];
 
386
                        nlist[nlistcount] = prev_node->getData()[i];
372
387
                        nlistcount++;
373
388
                    }
374
389
 
375
390
                }
376
 
                delete[] prev_node->data;
377
 
                prev_node->data = nlist;
 
391
                prev_node->replaceData(nlist);
378
392
 
379
393
                if (prev_node->highCount == -1 && prev_node->lowCount == -1) {
380
394
                    blockCount--;
381
 
                    delete[] prev_node->data;
 
395
                    prev_node->replaceData(NULL);
382
396
                }
383
397
 
384
398
                this->nextFree++;
385
399
                if (this->nextFree == this->totalSize) {
386
400
                    this->totalSize += this->blockSize;
387
401
                    this->pnodeArray.push_back(new PNode[this->blockSize]);
388
 
                    memset(this->pnodeArray[floor(this->totalSize / this->blockSize) - 1], 0xffffffff, (this->blockSize) * sizeof (PNode));
389
402
                }
390
403
            }
391
404