← Back to branch summary

~verifydtapn-contributers/verifydtapn/trunk

« back to all changes in this revision

Viewing changes to src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.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:
src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp
16
16
                findInOut();
17
17
        };
18
18
        
 
19
        WorkflowStrongSoundnessReachability::WorkflowStrongSoundnessReachability(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options)
 
20
        : Workflow(tapn, initialMarking, query, options), maxValue(-1), outPlace(NULL){
 
21
            findInOut();
 
22
        };
19
23
        
20
24
        void WorkflowStrongSoundnessReachability::findInOut()
21
25
        {
25
29
                    break;
26
30
                }
27
31
            }
28
 
        };
29
 
 
 
32
        }
 
33
        
 
34
        WorkflowStrongSoundnessPTrie::WorkflowStrongSoundnessPTrie(
 
35
                                TAPN::TimedArcPetriNet& tapn,
 
36
                                NonStrictMarking& initialMarking,
 
37
                                AST::Query* query,
 
38
                                VerificationOptions options,
 
39
                                WaitingList<ptriepointer_t<MetaData*> >* waiting_list) :
 
40
                                WorkflowStrongSoundnessReachability(
 
41
                                    tapn, 
 
42
                                    initialMarking, 
 
43
                                    query, 
 
44
                                    options)
 
45
        {
 
46
            pwList = new WorkflowPWListHybrid(  tapn,
 
47
                                                waiting_list, 
 
48
                                                options.getKBound(), 
 
49
                                                tapn.getNumberOfPlaces(), 
 
50
                                                tapn.getMaxConstant());
 
51
        }
 
52
       
30
53
        bool WorkflowStrongSoundnessReachability::verify() {
31
54
            
32
55
            if (outPlace == NULL)
53
76
                bool noDelay = false;
54
77
                Result res = successorGenerator.generateAndInsertSuccessors(*next_marking);
55
78
                if (res == ADDTOPW_RETURNED_TRUE) {
 
79
                    clearTrace();
56
80
                    return true;
57
81
                } else if (res == ADDTOPW_RETURNED_FALSE_URGENTENABLED) {
58
82
                    noDelay = true;
65
89
                    marking->setGeneratedBy(NULL);
66
90
                   
67
91
                    if (addToPW(marking, next_marking)) {
68
 
 
 
92
                        clearTrace();
69
93
                        lastMarking = marking;
70
94
                        return true;
71
95
                    }
77
101
                    // remove childless markings from stack
78
102
                    while(!trace.empty() && trace.top()->getNumberOfChildren() <= 1){
79
103
                            trace.top()->meta->inTrace = false;
 
104
                            deleteMarking(trace.top());
80
105
                            trace.pop();
81
106
                    }
82
107
                    if(trace.empty()){
108
133
            printXMLTrace(lastMarking, printStack, query, tapn);
109
134
        }
110
135
 
 
136
        void WorkflowStrongSoundnessPTrie::getTrace() {
 
137
 
 
138
            PWListHybrid* pwhlist = dynamic_cast<PWListHybrid*>(this->pwList);
 
139
            
 
140
            std::stack < NonStrictMarking*> printStack;
 
141
            
 
142
            NonStrictMarking* next = lastMarking;
 
143
            if(next != NULL)
 
144
            {
 
145
 
 
146
                printStack.push(next);
 
147
                MetaDataWithTraceAndEncoding* meta = 
 
148
                        static_cast<MetaDataWithTraceAndEncoding*>(next->meta);
 
149
 
 
150
                if(meta == NULL)
 
151
                {
 
152
                    // We assume the parent was not deleted on return
 
153
                    NonStrictMarking* parent = (NonStrictMarking*)lastMarking->getParent();                
 
154
                    if(parent != NULL) meta = 
 
155
                        static_cast<MetaDataWithTraceAndEncoding*>(parent->meta);
 
156
                    delete parent;
 
157
                }
 
158
                else
 
159
                {
 
160
                    meta = meta->parent;
 
161
                }
 
162
                                
 
163
                while(meta != NULL)
 
164
                {
 
165
                    next = pwhlist->decode(meta->ep);
 
166
                    next->setGeneratedBy(meta->generatedBy);
 
167
                    printStack.top()->setParent(next);
 
168
                    printStack.push(next);                    
 
169
                    meta = meta->parent;
 
170
                }
 
171
            }
 
172
#ifdef CLEANUP
 
173
            std::stack < NonStrictMarking*> cleanup = printStack;
 
174
#endif
 
175
            printXMLTrace(lastMarking, printStack, query, tapn);
 
176
            
 
177
#ifdef CLEANUP
 
178
            while(!cleanup.empty())
 
179
            {
 
180
                if(cleanup.top() != lastMarking) // deleted elsewhere
 
181
                {
 
182
                    delete cleanup.top();
 
183
                    cleanup.pop();
 
184
                }
 
185
                else
 
186
                {
 
187
                    break;
 
188
                }
 
189
            }
 
190
#endif
 
191
        }
 
192
        
 
193
        
111
194
        bool WorkflowStrongSoundnessReachability::addToPW(NonStrictMarking* marking, NonStrictMarking* parent) {
112
195
            marking->cut(placeStats);
113
196
            marking->setParent(parent);
135
218
                        // make sure we can print trace
136
219
                        marking->setNumberOfChildren(1);
137
220
                        maxValue = totalDelay;
 
221
                        deleteMarking(old);
138
222
                        return true;
139
223
                    } else {
140
224
                        // search again to find maxdelay
145
229
                        // fall through on purpose
146
230
                    }
147
231
                } else {
 
232
                    deleteMarking(old);
148
233
                    delete marking;
149
234
                    // already seen this maxage/marking combination
150
235
                    return false;
151
236
                }
152
237
            } else {
153
 
                marking->meta = new MetaData();
154
238
                marking->meta->totalDelay = totalDelay;
155
239
            }
156
240
            
166
250
                // if terminal, update max_value and last marking of trace
167
251
                if(maxValue < marking->meta->totalDelay) {
168
252
                    maxValue = marking->meta->totalDelay;
 
253
                    if(lastMarking != NULL) deleteMarking(lastMarking);
169
254
                    lastMarking = marking;
170
255
                    return false;
171
256
                }
172
257
            }
 
258
            
 
259
            deleteMarking(marking);
 
260
            
173
261
            return false;
174
262
        }
175
263
        
179
267
            old->setParent(marking->getParent());
180
268
        }
181
269
 
 
270
        void WorkflowStrongSoundnessPTrie::swapData(NonStrictMarking* marking, NonStrictMarking* parent)
 
271
        {
 
272
            PWListHybrid* pwhlist = dynamic_cast<PWListHybrid*>(this->pwList);
 
273
            MetaDataWithTraceAndEncoding* meta = 
 
274
                static_cast<MetaDataWithTraceAndEncoding*>(parent->meta);
 
275
 
 
276
            meta->generatedBy = marking->getGeneratedBy();
 
277
            meta->parent = pwhlist->parent;
 
278
        }
 
279
        
 
280
        void WorkflowStrongSoundnessPTrie::clearTrace()
 
281
        {
 
282
            if(!trace.empty()) trace.pop(); // pop parent, used in getTrace
 
283
            while(!trace.empty())
 
284
            {
 
285
                delete trace.top();
 
286
                trace.pop();
 
287
            }
 
288
        }
 
289
        
182
290
    } /* namespace DiscreteVerification */
183
291
} /* namespace VerifyTAPN */