← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to src/CTL/PetriNets/OnTheFlyDG.cpp

  • Committer: srba.jiri at gmail
  • Date: 2020-09-11 14:23:39 UTC
  • mfrom: (213.1.151 interval_tar)
  • Revision ID: srba.jiri@gmail.com-20200911142339-bq9328s1gppw24uj
merged in lp:~verifypn-maintainers/verifypn/interval_tar doing 
- Implements TAR w/o z3, but using a simple integer inference engine for Hoare logic.
 - Replaces LP-Solve with GLPK, reduces computation-time and memory overhead
 - Implements new global properties, translated into CTL formulae.

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/CTL/PetriNets/OnTheFlyDG.cpp
 
1
#include "CTL/PetriNets/OnTheFlyDG.h"
 
2
 
 
3
#include <algorithm>
 
4
#include <string.h>
 
5
#include <iostream>
 
6
#include <queue>
 
7
#include <limits>
 
8
 
 
9
#include "PetriEngine/SuccessorGenerator.h"
 
10
#include "PetriEngine/PQL/Expressions.h"
 
11
#include "CTL/SearchStrategy/SearchStrategy.h"
 
12
 
 
13
 
 
14
using namespace PetriEngine::PQL;
 
15
using namespace DependencyGraph;
 
16
 
 
17
namespace PetriNets {
 
18
 
 
19
OnTheFlyDG::OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order) : encoder(t_net->numberOfPlaces(), 0), 
 
20
        edge_alloc(new linked_bucket_t<DependencyGraph::Edge,1024*10>(1)), 
 
21
        conf_alloc(new linked_bucket_t<char[sizeof(PetriConfig)], 1024*1024>(1)),
 
22
        _redgen(*t_net), _partial_order(partial_order) {
 
23
    net = t_net;
 
24
    n_places = t_net->numberOfPlaces();
 
25
    n_transitions = t_net->numberOfTransitions();
 
26
}
 
27
 
 
28
 
 
29
OnTheFlyDG::~OnTheFlyDG()
 
30
{
 
31
    cleanUp();
 
32
    //Note: initial marking is in the markings set, therefore it will be deleted by the for loop
 
33
    //TODO: Ensure we don't leak memory here, when code moving is done
 
34
    size_t s = conf_alloc->size();
 
35
    for(size_t i = 0; i < s; ++i)
 
36
    {
 
37
        ((PetriConfig*)&(*conf_alloc)[i])->~PetriConfig();
 
38
    }
 
39
    delete conf_alloc;
 
40
    delete edge_alloc;
 
41
}
 
42
 
 
43
Condition::Result OnTheFlyDG::initialEval()
 
44
{
 
45
    initialConfiguration();
 
46
    EvaluationContext e(query_marking.marking(), net);
 
47
    return query->evaluate(e);
 
48
}
 
49
 
 
50
Condition::Result OnTheFlyDG::fastEval(Condition* query, Marking* unfolded)
 
51
{
 
52
    EvaluationContext e(unfolded->marking(), net);
 
53
    return query->evaluate(e);
 
54
}
 
55
 
 
56
 
 
57
std::vector<DependencyGraph::Edge*> OnTheFlyDG::successors(Configuration *c)
 
58
{
 
59
    PetriEngine::PQL::DistanceContext context(net, query_marking.marking());
 
60
    PetriConfig *v = static_cast<PetriConfig*>(c);
 
61
    trie.unpack(v->marking, encoder.scratchpad().raw());
 
62
    encoder.decode(query_marking.marking(), encoder.scratchpad().raw());
 
63
    //    v->printConfiguration();
 
64
    std::vector<Edge*> succs;
 
65
    auto query_type = v->query->getQueryType();
 
66
    if(query_type == EVAL){
 
67
        assert(false);
 
68
        //assert(false && "Someone told me, this was a bad place to be.");
 
69
        if (fastEval(query, &query_marking) == Condition::RTRUE){
 
70
            succs.push_back(newEdge(*v, 0));///*v->query->distance(context))*/0);
 
71
        }
 
72
    }
 
73
    else if (query_type == LOPERATOR){
 
74
        if(v->query->getQuantifier() == NEG){
 
75
            // no need to try to evaluate here -- this is already transient in other evaluations.
 
76
            auto cond = static_cast<NotCondition*>(v->query);
 
77
            Configuration* c = createConfiguration(v->marking, v->owner, (*cond)[0]);
 
78
            Edge* e = newEdge(*v, /*v->query->distance(context)*/0);
 
79
            e->is_negated = true;
 
80
            e->addTarget(c);
 
81
            succs.push_back(e);
 
82
        }
 
83
        else if(v->query->getQuantifier() == AND){
 
84
            auto cond = static_cast<AndCondition*>(v->query);
 
85
            //Check if left is false
 
86
            std::vector<Condition*> conds;
 
87
            for(auto& c : *cond)
 
88
            {
 
89
                auto res = fastEval(c.get(), &query_marking);
 
90
                if(res == Condition::RFALSE)
 
91
                {
 
92
                    return succs;
 
93
                }
 
94
                if(res == Condition::RUNKNOWN)
 
95
                {
 
96
                    conds.push_back(c.get());
 
97
                }
 
98
            }
 
99
            
 
100
            Edge *e = newEdge(*v, /*cond->distance(context)*/0);
 
101
 
 
102
            //If we get here, then either both propositions are true (shouldn't be possible)
 
103
            //Or a temporal operator and a true proposition
 
104
            //Or both are temporal
 
105
            for(auto c : conds)
 
106
            {
 
107
                assert(c->isTemporal());
 
108
                e->addTarget(createConfiguration(v->marking, v->owner, c));
 
109
            }
 
110
            succs.push_back(e);
 
111
        }
 
112
        else if(v->query->getQuantifier() == OR){
 
113
            auto cond = static_cast<OrCondition*>(v->query);
 
114
            //Check if left is true
 
115
            std::vector<Condition*> conds;
 
116
            for(auto& c : *cond)
 
117
            {
 
118
                auto res = fastEval(c.get(), &query_marking);
 
119
                if(res == Condition::RTRUE)
 
120
                {
 
121
                    succs.push_back(newEdge(*v, 0));
 
122
                    return succs;
 
123
                }
 
124
                if(res == Condition::RUNKNOWN)
 
125
                {
 
126
                    conds.push_back(c.get());
 
127
                }
 
128
            }
 
129
 
 
130
            //If we get here, either both propositions are false
 
131
            //Or one is false and one is temporal
 
132
            //Or both temporal
 
133
            for(auto c : conds)
 
134
            {
 
135
                assert(c->isTemporal());
 
136
                Edge *e = newEdge(*v, /*cond->distance(context)*/0);
 
137
                e->addTarget(createConfiguration(v->marking, v->owner, c));
 
138
                succs.push_back(e);
 
139
            }
 
140
        }
 
141
        else{
 
142
            assert(false && "An unknown error occoured in the loperator-part of the successor generator");
 
143
        }
 
144
    }
 
145
    else if (query_type == PATHQEURY){
 
146
        if(v->query->getQuantifier() == A){
 
147
            if (v->query->getPath() == U){
 
148
                auto cond = static_cast<AUCondition*>(v->query);
 
149
                Edge *right = NULL;       
 
150
                auto r1 = fastEval((*cond)[1], &query_marking);
 
151
                if (r1 != Condition::RUNKNOWN){
 
152
                    //right side is not temporal, eval it right now!
 
153
                    if (r1 == Condition::RTRUE) {    //satisfied, no need to go through successors
 
154
                        succs.push_back(newEdge(*v, 0));
 
155
                        return succs;
 
156
                    }//else: It's not valid, no need to add any edge, just add successors
 
157
                }
 
158
                else {
 
159
                    //right side is temporal, we need to evaluate it as normal
 
160
                    Configuration* c = createConfiguration(v->marking, v->owner, (*cond)[1]);
 
161
                    right = newEdge(*v, /*(*cond)[1]->distance(context)*/0);
 
162
                    right->addTarget(c);
 
163
                }
 
164
                bool valid = false;
 
165
                Configuration *left = NULL;
 
166
                auto r0 = fastEval((*cond)[0], &query_marking);
 
167
                if (r0 != Condition::RUNKNOWN) {
 
168
                    //left side is not temporal, eval it right now!
 
169
                    valid = r0 == Condition::RTRUE;
 
170
                } else {
 
171
                    //left side is temporal, include it in the edge
 
172
                    left = createConfiguration(v->marking, v->owner, (*cond)[0]);
 
173
                }
 
174
                if (valid || left != NULL) {
 
175
                    //if left side is guaranteed to be not satisfied, skip successor generation
 
176
                    Edge* leftEdge = NULL;
 
177
                    nextStates (query_marking, cond,
 
178
                                [&](){ leftEdge = newEdge(*v, std::numeric_limits<uint32_t>::max());},
 
179
                                [&](Marking& mark){
 
180
                                    auto res = fastEval(cond, &mark);
 
181
                                    if(res == Condition::RTRUE) return true;
 
182
                                    if(res == Condition::RFALSE)
 
183
                                    {
 
184
                                        left = nullptr;
 
185
                                        leftEdge->targets.clear();
 
186
                                        leftEdge = nullptr;
 
187
                                        return false;
 
188
                                    }
 
189
                                    context.setMarking(mark.marking());
 
190
                                    leftEdge->weight = 0;//std::min(leftEdge->weight, /*cond->distance(context)*/0);
 
191
                                    Configuration* c = createConfiguration(createMarking(mark), owner(mark, cond), cond);
 
192
                                    leftEdge->addTarget(c);
 
193
                                    return true;
 
194
                                },
 
195
                                [&]()
 
196
                                {
 
197
                                    if(leftEdge)
 
198
                                    {
 
199
                                        if (left != NULL) {
 
200
                                            leftEdge->addTarget(left);
 
201
                                        }
 
202
                                        succs.push_back(leftEdge);                                    
 
203
                                    }
 
204
                                }
 
205
                            );
 
206
                } //else: Left side is not temporal and it's false, no way to succeed there...
 
207
 
 
208
                if (right != NULL) {
 
209
                    succs.push_back(right);
 
210
                }
 
211
            }
 
212
            else if(v->query->getPath() == F){
 
213
                auto cond = static_cast<AFCondition*>(v->query);
 
214
                Edge *subquery = NULL;
 
215
                auto r = fastEval((*cond)[0], &query_marking);
 
216
                if (r != Condition::RUNKNOWN) {
 
217
                    bool valid = r == Condition::RTRUE;
 
218
                    if (valid) {
 
219
                        succs.push_back(newEdge(*v, 0));
 
220
                        return succs;
 
221
                    }
 
222
                } else {
 
223
                    subquery = newEdge(*v, /*cond->distance(context)*/0);
 
224
                    Configuration* c = createConfiguration(v->marking, v->owner, (*cond)[0]);
 
225
                    subquery->addTarget(c);
 
226
                }
 
227
                Edge* e1 = NULL;
 
228
                nextStates(query_marking, cond,
 
229
                        [&](){e1 = newEdge(*v, std::numeric_limits<uint32_t>::max());},
 
230
                        [&](Marking& mark)
 
231
                        {
 
232
                            auto res = fastEval(cond, &mark);
 
233
                            if(res == Condition::RTRUE) return true;
 
234
                            if(res == Condition::RFALSE)
 
235
                            {
 
236
                                if(subquery)
 
237
                                {
 
238
                                    --subquery->refcnt;
 
239
                                    release(subquery);
 
240
                                    subquery = nullptr;
 
241
                                }
 
242
                                e1->targets.clear();
 
243
                                return false;
 
244
                            }
 
245
                            context.setMarking(mark.marking());
 
246
                            e1->weight = 0;//std::min(e1->weight, /*cond->distance(context)*/0);
 
247
                            Configuration* c = createConfiguration(createMarking(mark), owner(mark, cond), cond);
 
248
                            e1->addTarget(c);
 
249
                            return true;
 
250
                        },
 
251
                        [&]()
 
252
                        {
 
253
                            succs.push_back(e1);
 
254
                        }                    
 
255
                );
 
256
 
 
257
                if (subquery != nullptr) {
 
258
                    succs.push_back(subquery);
 
259
                }
 
260
            }
 
261
            else if(v->query->getPath() == X){
 
262
                auto cond = static_cast<AXCondition*>(v->query);
 
263
                Edge* e = newEdge(*v, std::numeric_limits<uint32_t>::max());
 
264
                Condition::Result allValid = Condition::RTRUE;
 
265
                nextStates(query_marking, cond,
 
266
                        [](){}, 
 
267
                        [&](Marking& mark){
 
268
                            auto res = fastEval((*cond)[0], &mark);
 
269
                            if(res != Condition::RUNKNOWN)
 
270
                            {
 
271
                                if (res == Condition::RFALSE) {
 
272
                                    allValid = Condition::RFALSE;
 
273
                                    return false;
 
274
                                }
 
275
                            }
 
276
                            else
 
277
                            {
 
278
                                allValid = Condition::RUNKNOWN;
 
279
                                context.setMarking(mark.marking());
 
280
                                e->weight = 0;//std::min(e->weight, /*cond->distance(context)*/0);
 
281
                                Configuration* c = createConfiguration(createMarking(mark), v->owner, (*cond)[0]);
 
282
                                e->addTarget(c);
 
283
                            }
 
284
                            return true;
 
285
                        }, 
 
286
                        [](){}
 
287
                    );
 
288
                    if(allValid == Condition::RUNKNOWN)
 
289
                    {
 
290
                        succs.push_back(e);
 
291
                    }
 
292
                    else if(allValid == Condition::RTRUE)
 
293
                    {
 
294
                        e->targets.clear();
 
295
                        succs.push_back(e);
 
296
                    }
 
297
                    else
 
298
                    {
 
299
                    }
 
300
            }
 
301
            else if(v->query->getPath() == G ){
 
302
                assert(false && "Path operator G had not been translated - Parse error detected in succ()");
 
303
            }
 
304
            else
 
305
                assert(false && "An unknown error occoured in the successor generator");
 
306
        }
 
307
        else if(v->query->getQuantifier() == E){
 
308
            if (v->query->getPath() == U){
 
309
                auto cond = static_cast<EUCondition*>(v->query);
 
310
                Edge *right = NULL;
 
311
                auto r1 = fastEval((*cond)[1], &query_marking);
 
312
                if (r1 == Condition::RUNKNOWN) {
 
313
                    Configuration* c = createConfiguration(v->marking, v->owner, (*cond)[1]);
 
314
                    right = newEdge(*v, /*(*cond)[1]->distance(context)*/0);
 
315
                    right->addTarget(c);
 
316
                } else {
 
317
                    bool valid = r1 == Condition::RTRUE;
 
318
                    if (valid) {
 
319
                        succs.push_back(newEdge(*v, 0));
 
320
                        return succs;
 
321
                    }   // else: right condition is not satisfied, no need to add an edge
 
322
                }
 
323
 
 
324
 
 
325
                Configuration *left = NULL;
 
326
                bool valid = false;
 
327
                nextStates(query_marking, cond,
 
328
                    [&](){
 
329
                        auto r0 = fastEval((*cond)[0], &query_marking);
 
330
                        if (r0 == Condition::RUNKNOWN) {
 
331
                            left = createConfiguration(v->marking, v->owner, (*cond)[0]);
 
332
                        } else {
 
333
                            valid = r0 == Condition::RTRUE;
 
334
                        }                        
 
335
                    },
 
336
                    [&](Marking& marking){
 
337
                        if(left == NULL && !valid) return false;
 
338
                        auto res = fastEval(cond, &marking);
 
339
                        if(res == Condition::RFALSE) return true;
 
340
                        if(res == Condition::RTRUE)
 
341
                        {
 
342
                            for(auto s : succs){ --s->refcnt; release(s);}
 
343
                            succs.clear();
 
344
                            succs.push_back(newEdge(*v, 0));    
 
345
                            if(right)
 
346
                            {
 
347
                                --right->refcnt;
 
348
                                release(right);
 
349
                                right = nullptr;
 
350
                            }
 
351
                            
 
352
                            if(left)
 
353
                            {
 
354
                                succs.back()->addTarget(left);                                
 
355
                            }
 
356
                            
 
357
                            return false;
 
358
                        }
 
359
                        context.setMarking(marking.marking());
 
360
                        Edge* e = newEdge(*v, /*cond->distance(context)*/0);
 
361
                        Configuration* c1 = createConfiguration(createMarking(marking), owner(marking, cond), cond);
 
362
                        e->addTarget(c1);
 
363
                        if (left != NULL) {
 
364
                            e->addTarget(left);
 
365
                        }
 
366
                        succs.push_back(e);
 
367
                        return true;
 
368
                }, [](){});
 
369
 
 
370
                if (right != nullptr) {
 
371
                    succs.push_back(right);
 
372
                }
 
373
            }
 
374
            else if(v->query->getPath() == F){
 
375
                auto cond = static_cast<EFCondition*>(v->query);
 
376
                Edge *subquery = NULL;
 
377
                auto r = fastEval((*cond)[0], &query_marking);
 
378
                if (r != Condition::RUNKNOWN) {
 
379
                    bool valid = r == Condition::RTRUE;
 
380
                    if (valid) {
 
381
                        succs.push_back(newEdge(*v, 0));
 
382
                        return succs;
 
383
                    }
 
384
                } else {
 
385
                    Configuration* c = createConfiguration(v->marking, v->owner, (*cond)[0]);
 
386
                    subquery = newEdge(*v, /*cond->distance(context)*/0);
 
387
                    subquery->addTarget(c);
 
388
                }
 
389
 
 
390
                nextStates(query_marking, cond,
 
391
                            [](){},
 
392
                            [&](Marking& mark){
 
393
                                auto res = fastEval(cond, &mark);
 
394
                                if(res == Condition::RFALSE) return true;
 
395
                                if(res == Condition::RTRUE)
 
396
                                {
 
397
                                    for(auto s : succs){ --s->refcnt; release(s);}
 
398
                                    succs.clear();
 
399
                                    succs.push_back(newEdge(*v, 0));
 
400
                                    if(subquery)
 
401
                                    {
 
402
                                        --subquery->refcnt;
 
403
                                        release(subquery);
 
404
                                    }
 
405
                                    subquery = nullptr;
 
406
                                    return false;
 
407
                                }
 
408
                                context.setMarking(mark.marking());
 
409
                                Edge* e = newEdge(*v, /*cond->distance(context)*/0);
 
410
                                Configuration* c = createConfiguration(createMarking(mark), owner(mark, cond), cond);
 
411
                                e->addTarget(c);
 
412
                                succs.push_back(e);
 
413
                                return true;
 
414
                            },
 
415
                            [](){}
 
416
                        );
 
417
 
 
418
                if (subquery != NULL) {
 
419
                    succs.push_back(subquery);
 
420
                }
 
421
            }
 
422
            else if(v->query->getPath() == X){
 
423
                auto cond = static_cast<EXCondition*>(v->query);
 
424
                auto query = (*cond)[0];
 
425
                nextStates(query_marking, cond,
 
426
                        [](){}, 
 
427
                        [&](Marking& marking) {
 
428
                            auto res = fastEval(query, &marking);
 
429
                            if(res == Condition::RTRUE)
 
430
                            {
 
431
                                for(auto s : succs){ --s->refcnt; release(s);}
 
432
                                succs.clear();
 
433
                                succs.push_back(newEdge(*v, 0));
 
434
                                return false;
 
435
                            }   //else: It can't hold there, no need to create an edge
 
436
                            else if(res == Condition::RUNKNOWN)
 
437
                            {
 
438
                                context.setMarking(marking.marking());
 
439
                                Edge* e = newEdge(*v, /*(*cond)[0]->distance(context)*/0);
 
440
                                Configuration* c = createConfiguration(createMarking(marking), v->owner, query);
 
441
                                e->addTarget(c);
 
442
                                succs.push_back(e);
 
443
                            }
 
444
                            return true;
 
445
                        },
 
446
                        [](){}
 
447
                    );
 
448
            }
 
449
            else if(v->query->getPath() == G ){
 
450
                assert(false && "Path operator G had not been translated - Parse error detected in succ()");
 
451
            }
 
452
            else
 
453
                assert(false && "An unknown error occoured in the successor generator");
 
454
        }
 
455
    }
 
456
    else
 
457
    {
 
458
        assert(false && "Should never happen");
 
459
    }
 
460
    if(succs.size() == 1 && succs[0]->targets.size() == 1)
 
461
    {
 
462
        ((PetriConfig*)succs[0]->targets[0])->owner = v->owner;
 
463
    }
 
464
    return succs;
 
465
}
 
466
 
 
467
Configuration* OnTheFlyDG::initialConfiguration()
 
468
{
 
469
    if(working_marking.marking() == nullptr)
 
470
    {
 
471
        working_marking.setMarking  (net->makeInitialMarking());
 
472
        query_marking.setMarking    (net->makeInitialMarking());
 
473
        auto o = owner(working_marking, this->query);
 
474
        initial_config = createConfiguration(createMarking(working_marking), o, this->query);
 
475
    }
 
476
    return initial_config;
 
477
}
 
478
 
 
479
 
 
480
void OnTheFlyDG::nextStates(Marking& t_marking, Condition* ptr,
 
481
    std::function<void ()> pre, 
 
482
    std::function<bool (Marking&)> foreach, 
 
483
    std::function<void ()> post)
 
484
{
 
485
    bool first = true;
 
486
    memcpy(working_marking.marking(), query_marking.marking(), n_places*sizeof(PetriEngine::MarkVal));    
 
487
    auto qf = static_cast<QuantifierCondition*>(ptr);
 
488
    if(!_partial_order || ptr->getQuantifier() != E || ptr->getPath() != F || (*qf)[0]->isTemporal())
 
489
    {
 
490
        PetriEngine::SuccessorGenerator PNGen(*net);
 
491
        dowork<PetriEngine::SuccessorGenerator>(PNGen, first, pre, foreach);
 
492
    }
 
493
    else
 
494
    {
 
495
        _redgen.setQuery(ptr);
 
496
        dowork<PetriEngine::ReducingSuccessorGenerator>(_redgen, first, pre, foreach);
 
497
    }
 
498
 
 
499
    if(!first) post();
 
500
}
 
501
 
 
502
void OnTheFlyDG::cleanUp()
 
503
{    
 
504
    while(!recycle.empty())
 
505
    {
 
506
        assert(recycle.top()->refcnt == -1);
 
507
        recycle.pop();
 
508
    }
 
509
    // TODO, implement proper cleanup
 
510
}
 
511
 
 
512
 
 
513
void OnTheFlyDG::setQuery(const Condition_ptr& query)
 
514
{
 
515
    this->query = query;
 
516
    delete[] working_marking.marking();
 
517
    delete[] query_marking.marking();
 
518
    working_marking.setMarking(nullptr);
 
519
    query_marking.setMarking(nullptr);
 
520
    initialConfiguration();
 
521
    assert(this->query);
 
522
}
 
523
 
 
524
size_t OnTheFlyDG::configurationCount() const
 
525
{
 
526
    return _configurationCount;
 
527
}
 
528
 
 
529
size_t OnTheFlyDG::markingCount() const
 
530
{
 
531
    return _markingCount;
 
532
}
 
533
 
 
534
PetriConfig *OnTheFlyDG::createConfiguration(size_t marking, size_t own, Condition* t_query)
 
535
{
 
536
    auto& configs = trie.get_data(marking);
 
537
    for(PetriConfig* c : configs){
 
538
        if(c->query == t_query)
 
539
            return c;
 
540
    }
 
541
 
 
542
    _configurationCount++;
 
543
    size_t id = conf_alloc->next(0);
 
544
    char* mem = (*conf_alloc)[id];
 
545
    PetriConfig* newConfig = new (mem) PetriConfig();
 
546
    newConfig->marking = marking;
 
547
    newConfig->query = t_query;
 
548
    newConfig->owner = own;
 
549
    configs.push_back(newConfig);
 
550
    return newConfig;
 
551
}
 
552
 
 
553
 
 
554
 
 
555
size_t OnTheFlyDG::createMarking(Marking& t_marking){
 
556
    size_t sum = 0;
 
557
    bool allsame = true;
 
558
    uint32_t val = 0;
 
559
    uint32_t active = 0;
 
560
    uint32_t last = 0;
 
561
    markingStats(t_marking.marking(), sum, allsame, val, active, last);
 
562
    unsigned char type = encoder.getType(sum, active, allsame, val);
 
563
    size_t length = encoder.encode(t_marking.marking(), type);
 
564
    binarywrapper_t w = binarywrapper_t(encoder.scratchpad().raw(), length*8);
 
565
    auto tit = trie.insert(w.raw(), w.size());
 
566
    if(tit.first){
 
567
        _markingCount++;
 
568
    }
 
569
 
 
570
    return tit.second;
 
571
}
 
572
 
 
573
void OnTheFlyDG::release(Edge* e)
 
574
{
 
575
    assert(e->refcnt == 0);
 
576
    e->is_negated = false;
 
577
    e->processed = false;
 
578
    e->source = nullptr;
 
579
    e->targets.clear();
 
580
    e->refcnt = -1;
 
581
    e->handled = false;
 
582
    recycle.push(e);
 
583
}
 
584
 
 
585
size_t OnTheFlyDG::owner(Marking& marking, Condition* cond) {
 
586
    // Used for distributed algorithm
 
587
    return 0;
 
588
}
 
589
 
 
590
 
 
591
Edge* OnTheFlyDG::newEdge(Configuration &t_source, uint32_t weight)
 
592
{
 
593
    Edge* e = nullptr;
 
594
    if(recycle.empty())
 
595
    {
 
596
        size_t n = edge_alloc->next(0);
 
597
        e = &(*edge_alloc)[n];
 
598
    }
 
599
    else
 
600
    {
 
601
        e = recycle.top();
 
602
        e->refcnt = 0;
 
603
        recycle.pop();
 
604
    }
 
605
    assert(e->targets.empty());
 
606
    e->source = &t_source;
 
607
    e->weight = weight;
 
608
    assert(e->refcnt == 0);
 
609
    ++e->refcnt;
 
610
    return e;
 
611
}
 
612
 
 
613
void OnTheFlyDG::markingStats(const uint32_t* marking, size_t& sum, 
 
614
        bool& allsame, uint32_t& val, uint32_t& active, uint32_t& last)
 
615
{
 
616
    uint32_t cnt = 0;
 
617
 
 
618
    for (uint32_t i = 0; i < n_places; i++)
 
619
    {
 
620
        uint32_t old = val;
 
621
        if(marking[i] != 0)
 
622
        {
 
623
            ++cnt;
 
624
            last = std::max(last, i);
 
625
            val = std::max(marking[i], val);
 
626
            if(old != 0 && marking[i] != old) allsame = false;
 
627
            ++active;
 
628
            sum += marking[i];
 
629
        }
 
630
    }
 
631
}
 
632
 
 
633
 
 
634
}//PetriNet