~verifydtapn-contributers/verifydtapn/trunk

« back to all changes in this revision

Viewing changes to src/DiscreteVerification/DataStructures/WorkflowPWList.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:
88
88
                }
89
89
 
90
90
                bool isFirst = true;
91
 
                for (vector<NonStrictMarking*>::iterator iter = coveredMarkings.begin(); iter != coveredMarkings.end(); ++iter) {
 
91
                for (vector<NonStrictMarking*>::iterator iter = coveredMarkings.begin(); 
 
92
                        iter != coveredMarkings.end(); ++iter) {
92
93
                    if (isFirst) {
93
94
                        isFirst = false;
94
95
                        continue;
96
97
                    NonStrictMarking* covered = lookup(*iter);
97
98
                    if (covered != NULL) {
98
99
                        // cleanup
99
 
                        for (vector<NonStrictMarking*>::iterator del = coveredMarkings.begin();
100
 
                                del != coveredMarkings.end(); ++del)
 
100
                        for (;iter != coveredMarkings.end(); ++iter)
101
101
                        {
102
 
                            delete *del;
 
102
                            delete *iter;
103
103
                        }
104
104
                        return covered;
105
105
                    }
106
106
                    delete *iter;
107
107
                }
108
108
                
109
 
                // Cleanup
110
 
                for (vector<NonStrictMarking*>::iterator del = coveredMarkings.begin();
111
 
                    del != coveredMarkings.end(); ++del)
112
 
                {
113
 
                    delete *del;
114
 
                }
115
109
            }
116
110
            return NULL;
117
111
        }
163
157
        }
164
158
 
165
159
 
 
160
        WorkflowPWListHybrid::WorkflowPWListHybrid(
 
161
                            TAPN::TimedArcPetriNet& tapn,  
 
162
                            WaitingList<ptriepointer_t<MetaData*> >* w_l, 
 
163
                            int knumber, 
 
164
                            int nplaces, 
 
165
                            int mage) 
 
166
            : PWListHybrid(tapn, w_l, knumber, nplaces, mage, false, true),
 
167
                visitor(encoder)
 
168
        {
 
169
            
 
170
        }
 
171
        
 
172
        WorkflowPWListHybrid::~WorkflowPWListHybrid()
 
173
        {
 
174
            ptriepointer_t<MetaData*> begin = passed.begin();
 
175
            while(begin != passed.end())
 
176
            {
 
177
                delete begin.get_meta();
 
178
                ++ begin;
 
179
            }
 
180
        }
 
181
        
 
182
        NonStrictMarking* WorkflowPWListHybrid::getCoveredMarking
 
183
                                (NonStrictMarking* marking, bool useLinearSweep)
 
184
        {
 
185
            visitor.set_target(marking, last_pointer);
 
186
            passed.visit(visitor);
 
187
            if(visitor.found())
 
188
            {
 
189
                NonStrictMarking* m = visitor.decode();
 
190
                return m;
 
191
            }
 
192
            else
 
193
            {
 
194
                return NULL;
 
195
            }
 
196
        }
 
197
        
 
198
        NonStrictMarking* WorkflowPWListHybrid::getUnpassed()
 
199
        {
 
200
            ptriepointer_t<MetaData*> it = passed.last();
 
201
            for(; it != passed.rend(); --it)
 
202
            {
 
203
                if(!it.get_meta()->passed)
 
204
                {
 
205
                    NonStrictMarking* m = encoder.decode(it);
 
206
                    m->meta = it.get_meta();
 
207
                    return m;
 
208
                }
 
209
            }
 
210
            return NULL;
 
211
        }
 
212
        
 
213
        bool WorkflowPWListHybrid::add(NonStrictMarking* marking)
 
214
        {
 
215
            discoveredMarkings++;
 
216
            std::pair<bool, ptriepointer_t<MetaData*> > res = 
 
217
                                        passed.insert(encoder.encode(marking));
 
218
            
 
219
            if (!res.first) {
 
220
                return false;
 
221
            }
 
222
            else
 
223
            {
 
224
                MetaDataWithTraceAndEncoding* meta = 
 
225
                                        new MetaDataWithTraceAndEncoding();
 
226
                meta->generatedBy = marking->getGeneratedBy();
 
227
                meta->ep = res.second;
 
228
                meta->parent = parent;
 
229
                meta->totalDelay = marking->calculateTotalDelay();
 
230
                
 
231
                res.second.set_meta(meta);
 
232
                
 
233
                stored++;
 
234
                
 
235
                // using min first waiting-list, weight is allready in pointer
 
236
                waiting_list->add(NULL, res.second);
 
237
                return true;           
 
238
            }
 
239
        }
 
240
        
 
241
        NonStrictMarking* WorkflowPWListHybrid::addToPassed
 
242
                                    (NonStrictMarking* marking, bool strong)
 
243
        {
 
244
            discoveredMarkings++;
 
245
            std::pair<bool, ptriepointer_t<MetaData*> > res = 
 
246
                                        passed.insert(encoder.encode(marking));
 
247
 
 
248
 
 
249
            
 
250
            if (!res.first) {
 
251
                NonStrictMarking* old = encoder.decode(res.second);
 
252
                
 
253
                MetaDataWithTraceAndEncoding* meta = 
 
254
                        (MetaDataWithTraceAndEncoding*)res.second.get_meta();
 
255
                old->setGeneratedBy(meta->generatedBy);
 
256
                old->meta = meta;
 
257
                last_pointer = res.second;
 
258
                return old;
 
259
            } else {
 
260
                stored++;
 
261
 
 
262
                if(strong) marking->meta = new MetaDataWithTraceAndEncoding();
 
263
                else marking->meta = new WorkflowSoundnessMetaDataWithEncoding();
 
264
                
 
265
                MetaDataWithTraceAndEncoding* meta = 
 
266
                                (MetaDataWithTraceAndEncoding*) marking->meta;
 
267
                meta->ep = res.second;
 
268
                meta->parent = this->parent;
 
269
                meta->generatedBy = marking->getGeneratedBy();
 
270
                meta->totalDelay = marking->meta->totalDelay;
 
271
                
 
272
                res.second.set_meta(meta);
 
273
                last_pointer = res.second;
 
274
                return NULL;
 
275
            }
 
276
        }
 
277
        
 
278
        void WorkflowPWListHybrid::addLastToWaiting()
 
279
        {
 
280
            // using min first waiting-list, weight is allready in pointer
 
281
            waiting_list->add(NULL, last_pointer);
 
282
        }
 
283
        
 
284
        
 
285
        
166
286
 
167
287
    }
168
288
}