← Back to branch summary

~verifypn-stub/verifypn/deadlock-hotfix-2.2

« back to all changes in this revision

Viewing changes to CTL/PetriNets/OnTheFlyDG.cpp

  • Committer: Jiri Srba
  • Date: 2017-12-04 14:01:52 UTC
  • mfrom: (181.4.11 nctl)
  • Revision ID: srba.jiri@gmail.com-20171204140152-3tjzqq6xusfq0wyj
merged in branch lp:~verifypn-stub/verifypn/new-ctl

Show diffs side-by-side

added added

removed removed

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