← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to src/PetriEngine/PQL/Expressions.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/PetriEngine/PQL/Expressions.cpp
 
1
/* PeTe - Petri Engine exTremE
 
2
 * Copyright (C) 2011  Jonas Finnemann Jensen <jopsen@gmail.com>,
 
3
 *                     Thomas Søndersø Nielsen <primogens@gmail.com>,
 
4
 *                     Lars Kærlund Østergaard <larsko@gmail.com>,
 
5
 *                     Peter Gjøl Jensen <root@petergjoel.dk>
 
6
 * 
 
7
 * This program is free software: you can redistribute it and/or modify
 
8
 * it under the terms of the GNU General Public License as published by
 
9
 * the Free Software Foundation, either version 3 of the License, or
 
10
 * (at your option) any later version.
 
11
 * 
 
12
 * This program is distributed in the hope that it will be useful,
 
13
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 
14
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
15
 * GNU General Public License for more details.
 
16
 * 
 
17
 * You should have received a copy of the GNU General Public License
 
18
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
19
 */
 
20
#include "PetriEngine/PQL/Contexts.h"
 
21
#include "PetriEngine/PQL/Expressions.h"
 
22
#include "PetriEngine/errorcodes.h"
 
23
#include "PetriEngine/PQL/Visitor.h"
 
24
 
 
25
#include <sstream>
 
26
#include <assert.h>
 
27
#include <string.h>
 
28
#include <stdio.h>
 
29
#include <iostream>
 
30
#include <set>
 
31
#include <cmath>
 
32
#include <numeric>
 
33
 
 
34
using namespace PetriEngine::Simplification;
 
35
 
 
36
namespace PetriEngine {
 
37
    namespace PQL {
 
38
        
 
39
        std::ostream& generateTabs(std::ostream& out, uint32_t tabs) {
 
40
 
 
41
            for(uint32_t i = 0; i < tabs; i++) {
 
42
                out << "  ";
 
43
            }
 
44
            return out;
 
45
        }
 
46
        
 
47
        /** FOR COMPILING AND CONSTRUCTING LOGICAL OPERATORS **/
 
48
 
 
49
        template<typename T>
 
50
        void tryMerge(std::vector<Condition_ptr>& _conds, const Condition_ptr& ptr, bool aggressive = false)
 
51
        {
 
52
            if(auto lor = std::dynamic_pointer_cast<T>(ptr))
 
53
            {
 
54
                for(auto& c : *lor) tryMerge<T>(_conds, c, aggressive);
 
55
            }
 
56
            else if (!aggressive)
 
57
            {
 
58
                _conds.emplace_back(ptr);
 
59
            }
 
60
            else if (auto comp = std::dynamic_pointer_cast<CompareCondition>(ptr))
 
61
            {                
 
62
                if((std::is_same<T, AndCondition>::value && std::dynamic_pointer_cast<NotEqualCondition>(ptr)) ||
 
63
                   (std::is_same<T, OrCondition>::value && std::dynamic_pointer_cast<EqualCondition>(ptr)))
 
64
                {
 
65
                    _conds.emplace_back(ptr);
 
66
                }
 
67
                else
 
68
                {
 
69
                    if(! ((dynamic_cast<UnfoldedIdentifierExpr*>((*comp)[0].get()) && (*comp)[1]->placeFree()) ||
 
70
                          (dynamic_cast<UnfoldedIdentifierExpr*>((*comp)[1].get()) && (*comp)[0]->placeFree())))
 
71
                    {
 
72
                        _conds.emplace_back(ptr);
 
73
                        return;
 
74
                    }
 
75
 
 
76
                    std::vector<Condition_ptr> cnds{ptr};
 
77
                    auto cmp = std::make_shared<CompareConjunction>(cnds, std::is_same<T, OrCondition>::value);
 
78
                    tryMerge<T>(_conds, cmp, aggressive);
 
79
                }
 
80
            }
 
81
            else if (auto conj = std::dynamic_pointer_cast<CompareConjunction>(ptr))
 
82
            {
 
83
                if((std::is_same<T, OrCondition>::value  && ( conj->isNegated() || conj->singular())) ||
 
84
                   (std::is_same<T, AndCondition>::value && (!conj->isNegated() || conj->singular())))
 
85
                {
 
86
                    if(auto lc = std::dynamic_pointer_cast<CompareConjunction>(_conds.size() == 0 ? nullptr : _conds[0]))
 
87
                    {
 
88
                        if(lc->isNegated() == std::is_same<T, OrCondition>::value)
 
89
                        {
 
90
                            auto cpy = std::make_shared<CompareConjunction>(*lc);
 
91
                            cpy->merge(*conj);
 
92
                            _conds[0] = cpy;
 
93
                        }
 
94
                        else
 
95
                        {
 
96
                            if(conj->isNegated() == std::is_same<T, OrCondition>::value)
 
97
                                _conds.insert(_conds.begin(), conj);
 
98
                            else
 
99
                            {
 
100
                                auto next = std::make_shared<CompareConjunction>(std::is_same<T, OrCondition>::value);
 
101
                                next->merge(*conj);
 
102
                                _conds.insert(_conds.begin(), next);
 
103
                            }
 
104
                        }
 
105
                    }
 
106
                    else
 
107
                    {
 
108
                        _conds.insert(_conds.begin(), conj);
 
109
                    }
 
110
                }
 
111
                else
 
112
                {
 
113
                    _conds.emplace_back(ptr);                    
 
114
                }
 
115
            }
 
116
            else
 
117
            {
 
118
                _conds.emplace_back(ptr);
 
119
            }
 
120
 
 
121
        }
 
122
        
 
123
        template<typename T, bool K>
 
124
        Condition_ptr makeLog(const std::vector<Condition_ptr>& conds, bool aggressive)
 
125
        {
 
126
            if(conds.size() == 0) return BooleanCondition::getShared(K);
 
127
            if(conds.size() == 1) return conds[0];
 
128
 
 
129
            std::vector<Condition_ptr> cnds;
 
130
            for(auto& c : conds) tryMerge<T>(cnds, c, aggressive);
 
131
            auto res = std::make_shared<T>(cnds);
 
132
            if(res->singular()) return *res->begin();
 
133
            if(res->empty()) return BooleanCondition::getShared(K);
 
134
            return res;
 
135
        }
 
136
        
 
137
        Condition_ptr makeOr(const std::vector<Condition_ptr>& cptr) 
 
138
        { return makeLog<OrCondition,false>(cptr, true); }
 
139
        Condition_ptr makeAnd(const std::vector<Condition_ptr>& cptr) 
 
140
        { return makeLog<AndCondition,true>(cptr, true); }
 
141
        Condition_ptr makeOr(const Condition_ptr& a, const Condition_ptr& b) {  
 
142
            std::vector<Condition_ptr> cnds{a,b};
 
143
            return makeLog<OrCondition,false>(cnds, true); 
 
144
        }
 
145
        Condition_ptr makeAnd(const Condition_ptr& a, const Condition_ptr& b) 
 
146
        {             
 
147
            std::vector<Condition_ptr> cnds{a,b};
 
148
            return makeLog<AndCondition,true>(cnds, true); 
 
149
        }
 
150
        
 
151
        
 
152
        // CONSTANTS
 
153
        Condition_ptr BooleanCondition::FALSE_CONSTANT = std::make_shared<BooleanCondition>(false);
 
154
        Condition_ptr BooleanCondition::TRUE_CONSTANT = std::make_shared<BooleanCondition>(true);
 
155
        Condition_ptr DeadlockCondition::DEADLOCK = std::make_shared<DeadlockCondition>();
 
156
        
 
157
        
 
158
        Condition_ptr BooleanCondition::getShared(bool val)
 
159
        {
 
160
            if(val)
 
161
            {
 
162
                return TRUE_CONSTANT;
 
163
            }
 
164
            else
 
165
            {
 
166
                return FALSE_CONSTANT;
 
167
            }
 
168
        }
 
169
        
 
170
        /******************** To String ********************/
 
171
 
 
172
        void LiteralExpr::toString(std::ostream& out) const {
 
173
            out << _value;
 
174
        }
 
175
 
 
176
        void UnfoldedIdentifierExpr::toString(std::ostream& out) const {
 
177
            out << _name << "(P" << _offsetInMarking << ")";
 
178
        }
 
179
 
 
180
        void NaryExpr::toString(std::ostream& ss) const {
 
181
            ss << "(";
 
182
            _exprs[0]->toString(ss);
 
183
            for(size_t i = 1; i < _exprs.size(); ++i)
 
184
            {
 
185
                ss << " " << op() << " ";
 
186
                _exprs[i]->toString(ss);
 
187
            }
 
188
            ss << ")";
 
189
        }
 
190
 
 
191
        void CommutativeExpr::toString(std::ostream& ss) const {
 
192
            ss << "( " << _constant;
 
193
            for(auto& i : _ids)
 
194
                ss << " " << op() << " " << i.second;
 
195
            for(auto& e : _exprs)
 
196
            {
 
197
                ss << " " << op() << " ";
 
198
                e->toString(ss);
 
199
            }
 
200
            ss << ")";
 
201
        }
 
202
 
 
203
 
 
204
        void MinusExpr::toString(std::ostream& out) const {
 
205
            out << "-";
 
206
            _expr->toString(out);
 
207
        }
 
208
 
 
209
        void SimpleQuantifierCondition::toString(std::ostream& out) const {
 
210
            out << op() << " ";
 
211
            _cond->toString(out);
 
212
        }
 
213
        
 
214
        void UntilCondition::toString(std::ostream& out) const {
 
215
            out << op() << " (";
 
216
            _cond1->toString(out);
 
217
            out << " U ";
 
218
            _cond2->toString(out);
 
219
            out << ")";
 
220
        }
 
221
        
 
222
        void LogicalCondition::toString(std::ostream& out) const {
 
223
            out << "(";
 
224
            _conds[0]->toString(out);
 
225
            for(size_t i = 1; i < _conds.size(); ++i)
 
226
            {
 
227
                out << " " << op() << " ";
 
228
                _conds[i]->toString(out);
 
229
            }
 
230
            out << ")";
 
231
        }
 
232
        
 
233
        void CompareConjunction::toString(std::ostream& out) const {
 
234
            out << "(";
 
235
            if(_negated) out << "not";
 
236
            bool first = true;
 
237
            for(auto& c : _constraints)
 
238
            {
 
239
                if(!first) out << " and ";
 
240
                if(c._lower != 0) 
 
241
                    out << "(" << c._lower << " <= " << c._name << ")";
 
242
                if(c._lower != 0 && c._upper != std::numeric_limits<uint32_t>::max()) 
 
243
                    out << " and ";
 
244
                if(c._upper != std::numeric_limits<uint32_t>::max()) 
 
245
                    out << "(" << c._upper << " >= " << c._name << ")";
 
246
                first = false;
 
247
            }
 
248
            out << ")";
 
249
        }
 
250
 
 
251
        void CompareCondition::toString(std::ostream& out) const {
 
252
            out << "(";
 
253
            _expr1->toString(out);
 
254
            out << " " << op() << " ";
 
255
            _expr2->toString(out);
 
256
            out <<")";
 
257
        }
 
258
 
 
259
        void NotCondition::toString(std::ostream& out) const {
 
260
            out << "(not ";
 
261
            _cond->toString(out);
 
262
            out << ")";
 
263
        }
 
264
 
 
265
        void BooleanCondition::toString(std::ostream& out) const {
 
266
            if (_value)
 
267
                out << "true";
 
268
            else
 
269
                out << "false";
 
270
        }
 
271
 
 
272
        void DeadlockCondition::toString(std::ostream& out) const {
 
273
            out << "deadlock";
 
274
        }
 
275
 
 
276
        void StableMarkingCondition::_toString(std::ostream &out) const {
 
277
            if(_compiled) _compiled->toString(out);
 
278
            else out << "stable-marking";
 
279
        }
 
280
 
 
281
        void LivenessCondition::_toString(std::ostream &out) const {
 
282
            if(_compiled) _compiled->toString(out);
 
283
            else out << "liveness";
 
284
        }
 
285
 
 
286
        void QuasiLivenessCondition::_toString(std::ostream &out) const {
 
287
            if(_compiled) _compiled->toString(out);
 
288
            else out << "liveness";
 
289
        }
 
290
 
 
291
        void KSafeCondition::_toString(std::ostream &out) const {
 
292
            if(_compiled) _compiled->toString(out);
 
293
            else
 
294
            {
 
295
                out << "k-safe(";
 
296
                _bound->toString(out);
 
297
                out << ")";
 
298
            }
 
299
        }
 
300
 
 
301
        void UpperBoundsCondition::_toString(std::ostream& out) const {
 
302
            if(_compiled) _compiled->toString(out);
 
303
            else
 
304
            {
 
305
                out << "bounds (";
 
306
                for(size_t i = 0; i < _places.size(); ++i)
 
307
                {
 
308
                    if(i != 0) out << ", ";
 
309
                    out << _places[i];
 
310
                }
 
311
                out << ")";            
 
312
            }
 
313
        }
 
314
        
 
315
        void UnfoldedUpperBoundsCondition::toString(std::ostream& out) const {
 
316
            out << "bounds (";
 
317
            for(size_t i = 0; i < _places.size(); ++i)
 
318
            {
 
319
                if(i != 0) out << ", ";
 
320
                out << _places[i]._name;
 
321
            }
 
322
            out << ")";
 
323
        }
 
324
 
 
325
        void FireableCondition::_toString(std::ostream &out) const {
 
326
            out << "is-fireable(" << _name << ")";
 
327
        }
 
328
 
 
329
        void UnfoldedFireableCondition::_toString(std::ostream &out) const {
 
330
            out << "is-fireable(" << _name << ")";
 
331
        }
 
332
 
 
333
        /******************** To TAPAAL Query ********************/
 
334
 
 
335
        void SimpleQuantifierCondition::toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const {
 
336
            out << op() << " ";
 
337
            _cond->toTAPAALQuery(out,context);
 
338
        }
 
339
        
 
340
        void UntilCondition::toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const {
 
341
            out << op() << " (";
 
342
            _cond1->toTAPAALQuery(out, context);
 
343
            out << " U ";
 
344
            _cond2->toTAPAALQuery(out,context);
 
345
            out << ")";
 
346
        }
 
347
        
 
348
        void LogicalCondition::toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const {
 
349
            out << "(";
 
350
            _conds[0]->toTAPAALQuery(out, context);
 
351
            for(size_t i = 1; i < _conds.size(); ++i)
 
352
            {
 
353
                out << " " << op() << " ";
 
354
                _conds[i]->toTAPAALQuery(out, context);
 
355
            }
 
356
            out << ")";
 
357
        }
 
358
        
 
359
        void CompareConjunction::toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const {
 
360
            out << "(";
 
361
            if(_negated) out << "!";
 
362
            bool first = true;
 
363
            for(auto& c : _constraints)
 
364
            {
 
365
                if(!first) out << " and ";
 
366
                if(c._lower != 0) 
 
367
                    out << "(" << c._lower << " <= " << context.netName << "." << c._name << ")";
 
368
                if(c._lower != 0 && c._upper != std::numeric_limits<uint32_t>::max()) 
 
369
                    out << " and ";
 
370
                if(c._lower != 0) 
 
371
                    out << "(" << c._upper << " >= " << context.netName << "." << c._name << ")";
 
372
                first = false;
 
373
            }
 
374
            out << ")";
 
375
        }
 
376
 
 
377
        void CompareCondition::toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const {
 
378
            //If <id> <op> <literal>
 
379
            if (_expr1->type() == Expr::IdentifierExpr && _expr2->type() == Expr::LiteralExpr) {
 
380
                out << " ( " << context.netName << ".";
 
381
                _expr1->toString(out);
 
382
                out << " " << opTAPAAL() << " ";
 
383
                _expr2->toString(out);
 
384
                out << " ) ";
 
385
                //If <literal> <op> <id>
 
386
            } else if (_expr2->type() == Expr::IdentifierExpr && _expr1->type() == Expr::LiteralExpr) {
 
387
                out << " ( ";
 
388
                _expr1->toString(out);
 
389
                out << " " << sopTAPAAL() << " " << context.netName << ".";
 
390
                _expr2->toString(out);
 
391
                out << " ) ";
 
392
            } else {
 
393
                context.failed = true;
 
394
                out << " false ";
 
395
            }
 
396
        }
 
397
 
 
398
        void NotEqualCondition::toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const {
 
399
            out << " !( ";
 
400
            CompareCondition::toTAPAALQuery(out,context);
 
401
            out << " ) ";
 
402
        }
 
403
 
 
404
        void NotCondition::toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const {
 
405
            out << " !( ";
 
406
            _cond->toTAPAALQuery(out,context);
 
407
            out << " ) ";
 
408
        }
 
409
 
 
410
        void BooleanCondition::toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext&) const {
 
411
            if (_value)
 
412
                out << "true";
 
413
            else
 
414
                out << "false";
 
415
        }
 
416
 
 
417
        void DeadlockCondition::toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext&) const {
 
418
            out << "deadlock";
 
419
        }
 
420
 
 
421
        void UnfoldedUpperBoundsCondition::toTAPAALQuery(std::ostream& out, TAPAALConditionExportContext&) const {
 
422
            out << "bounds (";
 
423
            for(size_t i = 0; i < _places.size(); ++i)
 
424
            {
 
425
                if(i != 0) out << ", ";
 
426
                out << _places[i]._name;
 
427
            }
 
428
            out << ")";
 
429
        }
 
430
        
 
431
        /******************** opTAPAAL ********************/
 
432
 
 
433
        std::string EqualCondition::opTAPAAL() const {
 
434
            return "=";
 
435
        }
 
436
 
 
437
        std::string NotEqualCondition::opTAPAAL() const {
 
438
            return "=";
 
439
        } //Handled with hack in NotEqualCondition::toTAPAALQuery
 
440
 
 
441
        std::string LessThanCondition::opTAPAAL() const {
 
442
            return "<";
 
443
        }
 
444
 
 
445
        std::string LessThanOrEqualCondition::opTAPAAL() const {
 
446
            return "<=";
 
447
        }
 
448
 
 
449
        std::string GreaterThanCondition::opTAPAAL() const {
 
450
            return ">";
 
451
        }
 
452
 
 
453
        std::string GreaterThanOrEqualCondition::opTAPAAL() const {
 
454
            return ">=";
 
455
        }
 
456
 
 
457
        std::string EqualCondition::sopTAPAAL() const {
 
458
            return "=";
 
459
        }
 
460
 
 
461
        std::string NotEqualCondition::sopTAPAAL() const {
 
462
            return "=";
 
463
        } //Handled with hack in NotEqualCondition::toTAPAALQuery
 
464
 
 
465
        std::string LessThanCondition::sopTAPAAL() const {
 
466
            return ">=";
 
467
        }
 
468
 
 
469
        std::string LessThanOrEqualCondition::sopTAPAAL() const {
 
470
            return ">";
 
471
        }
 
472
 
 
473
        std::string GreaterThanCondition::sopTAPAAL() const {
 
474
            return "<=";
 
475
        }
 
476
 
 
477
        std::string GreaterThanOrEqualCondition::sopTAPAAL() const {
 
478
            return "<";
 
479
        }
 
480
 
 
481
        /******************** Context Analysis ********************/
 
482
 
 
483
        void NaryExpr::analyze(AnalysisContext& context) {
 
484
            for(auto& e : _exprs) e->analyze(context);
 
485
        }
 
486
 
 
487
        void CommutativeExpr::analyze(AnalysisContext& context) {
 
488
            for(auto& i : _ids)
 
489
            {
 
490
                AnalysisContext::ResolutionResult result = context.resolve(i.second);
 
491
                if (result.success) {
 
492
                    i.first = result.offset;
 
493
                } else {
 
494
                    ExprError error("Unable to resolve identifier \"" + i.second + "\"",
 
495
                            i.second.length());
 
496
                    context.reportError(error);
 
497
                }
 
498
            }
 
499
            NaryExpr::analyze(context);
 
500
            std::sort(_ids.begin(), _ids.end(), [](auto& a, auto& b){ return a.first < b.first; });
 
501
            std::sort(_exprs.begin(), _exprs.end(), [](auto& a, auto& b)
 
502
            {
 
503
                auto ida = dynamic_pointer_cast<PQL::UnfoldedIdentifierExpr>(a);
 
504
                auto idb = dynamic_pointer_cast<PQL::UnfoldedIdentifierExpr>(b);
 
505
                if(ida == NULL) return false;
 
506
                if(ida && !idb) return true;
 
507
                return ida->offset() < idb->offset();
 
508
            });
 
509
        }
 
510
 
 
511
        void MinusExpr::analyze(AnalysisContext& context) {
 
512
            _expr->analyze(context);
 
513
        }
 
514
 
 
515
        void LiteralExpr::analyze(AnalysisContext&) {
 
516
            return;
 
517
        }
 
518
 
 
519
        uint32_t getPlace(AnalysisContext& context, const std::string& name)
 
520
        {
 
521
            AnalysisContext::ResolutionResult result = context.resolve(name);
 
522
            if (result.success) {
 
523
                return result.offset;
 
524
            } else {
 
525
                ExprError error("Unable to resolve identifier \"" + name + "\"",
 
526
                                name.length());
 
527
                context.reportError(error);
 
528
            }
 
529
            return -1;
 
530
        }
 
531
 
 
532
        Expr_ptr generateUnfoldedIdentifierExpr(ColoredAnalysisContext& context, std::unordered_map<uint32_t,std::string>& names, uint32_t colorIndex) {
 
533
            std::string& place = names[colorIndex];
 
534
            return std::make_shared<UnfoldedIdentifierExpr>(place, getPlace(context, place));
 
535
        }
 
536
 
 
537
        void IdentifierExpr::analyze(AnalysisContext &context) {
 
538
            if (_compiled) {
 
539
                _compiled->analyze(context);
 
540
                return;
 
541
            }
 
542
 
 
543
            auto coloredContext = dynamic_cast<ColoredAnalysisContext*>(&context);
 
544
            if(coloredContext != nullptr && coloredContext->isColored())
 
545
            {
 
546
                std::unordered_map<uint32_t,std::string> names;
 
547
                if (!coloredContext->resolvePlace(_name, names)) {
 
548
                    ExprError error("Unable to resolve colored identifier \"" + _name + "\"", _name.length());
 
549
                    coloredContext->reportError(error);
 
550
                }
 
551
 
 
552
                if (names.size() == 1) {
 
553
                    _compiled = generateUnfoldedIdentifierExpr(*coloredContext, names, 0);
 
554
                } else {
 
555
                    std::vector<Expr_ptr> identifiers;
 
556
                    for (auto& unfoldedName : names) {
 
557
                        identifiers.push_back(generateUnfoldedIdentifierExpr(*coloredContext,names,unfoldedName.first));
 
558
                    }
 
559
                    _compiled = std::make_shared<PQL::PlusExpr>(std::move(identifiers));
 
560
                }
 
561
            } else {
 
562
                _compiled = std::make_shared<UnfoldedIdentifierExpr>(_name, getPlace(context, _name));
 
563
            }
 
564
            _compiled->analyze(context);
 
565
        }
 
566
 
 
567
        void UnfoldedIdentifierExpr::analyze(AnalysisContext& context) {
 
568
            AnalysisContext::ResolutionResult result = context.resolve(_name);
 
569
            if (result.success) {
 
570
                _offsetInMarking = result.offset;
 
571
            } else {
 
572
                ExprError error("Unable to resolve identifier \"" + _name + "\"",
 
573
                        _name.length());
 
574
                context.reportError(error);
 
575
            }
 
576
        }
 
577
 
 
578
        void SimpleQuantifierCondition::analyze(AnalysisContext& context) {
 
579
            _cond->analyze(context);
 
580
        }
 
581
        
 
582
        void UntilCondition::analyze(AnalysisContext& context) {
 
583
            _cond1->analyze(context);
 
584
            _cond2->analyze(context);
 
585
        }
 
586
        
 
587
        void LogicalCondition::analyze(AnalysisContext& context) {
 
588
            for(auto& c : _conds) c->analyze(context);
 
589
        }
 
590
        
 
591
        void UnfoldedFireableCondition::_analyze(AnalysisContext& context)
 
592
        {
 
593
            std::vector<Condition_ptr> conds;
 
594
            AnalysisContext::ResolutionResult result = context.resolve(_name, false);
 
595
            if (!result.success)
 
596
            {
 
597
                ExprError error("Unable to resolve identifier \"" + _name + "\"",
 
598
                        _name.length());
 
599
                context.reportError(error);
 
600
            }            
 
601
 
 
602
            assert(_name.compare(context.net()->transitionNames()[result.offset]) == 0);
 
603
            auto preset = context.net()->preset(result.offset);
 
604
            for(; preset.first != preset.second; ++preset.first)
 
605
            {
 
606
                assert(preset.first->place != std::numeric_limits<uint32_t>::max());
 
607
                assert(preset.first->place != -1);
 
608
                auto id = std::make_shared<UnfoldedIdentifierExpr>(context.net()->placeNames()[preset.first->place], preset.first->place);
 
609
                auto lit = std::make_shared<LiteralExpr>(preset.first->tokens);
 
610
 
 
611
                if(!preset.first->inhibitor)
 
612
                {
 
613
                    conds.emplace_back(std::make_shared<GreaterThanOrEqualCondition>(id, lit));
 
614
                }
 
615
                else if(preset.first->tokens > 0)
 
616
                {
 
617
                    conds.emplace_back(std::make_shared<LessThanCondition>(id, lit));
 
618
                }
 
619
            }
 
620
            if(conds.size() == 1) _compiled = conds[0];
 
621
            else _compiled = std::make_shared<AndCondition>(conds);
 
622
            _compiled->analyze(context);
 
623
        }
 
624
 
 
625
        void FireableCondition::_analyze(AnalysisContext &context) {
 
626
 
 
627
            auto coloredContext = dynamic_cast<ColoredAnalysisContext*>(&context);
 
628
            if(coloredContext != nullptr && coloredContext->isColored()) {
 
629
                std::vector<std::string> names;
 
630
                if (!coloredContext->resolveTransition(_name, names)) {
 
631
                    ExprError error("Unable to resolve colored identifier \"" + _name + "\"", _name.length());
 
632
                    coloredContext->reportError(error);
 
633
                }
 
634
 
 
635
                if (names.size() == 1) {
 
636
                    _compiled = std::make_shared<UnfoldedFireableCondition>(names[0]);
 
637
                } else {
 
638
                    std::vector<Condition_ptr> identifiers;
 
639
                    for (auto& unfoldedName : names) {
 
640
                        identifiers.push_back(std::make_shared<UnfoldedFireableCondition>(unfoldedName));
 
641
                    }
 
642
                    _compiled = std::make_shared<OrCondition>(std::move(identifiers));
 
643
                }
 
644
            } else {
 
645
                _compiled = std::make_shared<UnfoldedFireableCondition>(_name);
 
646
            }
 
647
            _compiled->analyze(context);
 
648
        }
 
649
 
 
650
        void CompareConjunction::analyze(AnalysisContext& context) {
 
651
            for(auto& c : _constraints){
 
652
                c._place = getPlace(context, c._name);
 
653
                assert(c._place >= 0);
 
654
            }
 
655
            std::sort(std::begin(_constraints), std::end(_constraints));
 
656
        }
 
657
 
 
658
        void CompareCondition::analyze(AnalysisContext& context) {
 
659
            _expr1->analyze(context);
 
660
            _expr2->analyze(context);
 
661
        }
 
662
        
 
663
        void NotCondition::analyze(AnalysisContext& context) {
 
664
            _cond->analyze(context);
 
665
        }
 
666
 
 
667
        void BooleanCondition::analyze(AnalysisContext&) {
 
668
        }
 
669
 
 
670
        void DeadlockCondition::analyze(AnalysisContext& c) {
 
671
            c.setHasDeadlock();
 
672
        }
 
673
 
 
674
        void KSafeCondition::_analyze(AnalysisContext &context) {
 
675
            auto coloredContext = dynamic_cast<ColoredAnalysisContext*>(&context);
 
676
            std::vector<Condition_ptr> k_safe;
 
677
            if(coloredContext != nullptr && coloredContext->isColored())
 
678
            {
 
679
                for(auto& p : coloredContext->allColoredPlaceNames())
 
680
                    k_safe.emplace_back(std::make_shared<LessThanOrEqualCondition>(std::make_shared<IdentifierExpr>(p.first), _bound));
 
681
            }
 
682
            else
 
683
            {
 
684
                for(auto& p : context.allPlaceNames())
 
685
                    k_safe.emplace_back(std::make_shared<LessThanOrEqualCondition>(std::make_shared<UnfoldedIdentifierExpr>(p.first), _bound));
 
686
            }
 
687
            _compiled = std::make_shared<AGCondition>(std::make_shared<AndCondition>(std::move(k_safe)));
 
688
            _compiled->analyze(context);
 
689
        }
 
690
 
 
691
        void QuasiLivenessCondition::_analyze(AnalysisContext &context)
 
692
        {
 
693
            auto coloredContext = dynamic_cast<ColoredAnalysisContext*>(&context);
 
694
            std::vector<Condition_ptr> quasi;
 
695
            if(coloredContext != nullptr && coloredContext->isColored())
 
696
            {
 
697
                for(auto& n : coloredContext->allColoredTransitionNames())
 
698
                {
 
699
                    std::vector<Condition_ptr> disj;
 
700
                    for(auto& tn : n.second)
 
701
                        disj.emplace_back(std::make_shared<UnfoldedFireableCondition>(tn));
 
702
                    quasi.emplace_back(std::make_shared<EFCondition>(std::make_shared<OrCondition>(std::move(disj))));
 
703
                }
 
704
            }
 
705
            else
 
706
            {
 
707
                for(auto& n : context.allTransitionNames())
 
708
                {
 
709
                    quasi.emplace_back(std::make_shared<EFCondition>(std::make_shared<UnfoldedFireableCondition>(n.first)));
 
710
                }
 
711
            }
 
712
            _compiled = std::make_shared<AndCondition>(std::move(quasi));
 
713
            _compiled->analyze(context);
 
714
        }
 
715
 
 
716
        void LivenessCondition::_analyze(AnalysisContext &context)
 
717
        {
 
718
            auto coloredContext = dynamic_cast<ColoredAnalysisContext*>(&context);
 
719
            std::vector<Condition_ptr> liveness;
 
720
            if(coloredContext != nullptr && coloredContext->isColored())
 
721
            {
 
722
                for(auto& n : coloredContext->allColoredTransitionNames())
 
723
                {
 
724
                    std::vector<Condition_ptr> disj;
 
725
                    for(auto& tn : n.second)
 
726
                        disj.emplace_back(std::make_shared<UnfoldedFireableCondition>(tn));
 
727
                    liveness.emplace_back(std::make_shared<AGCondition>(std::make_shared<EFCondition>(std::make_shared<OrCondition>(std::move(disj)))));
 
728
                }
 
729
            }
 
730
            else
 
731
            {
 
732
                for(auto& n : context.allTransitionNames())
 
733
                {
 
734
                    liveness.emplace_back(std::make_shared<AGCondition>(std::make_shared<EFCondition>(std::make_shared<UnfoldedFireableCondition>(n.first))));
 
735
                }
 
736
            }
 
737
            _compiled = std::make_shared<AndCondition>(std::move(liveness));
 
738
            _compiled->analyze(context);
 
739
        }
 
740
 
 
741
        void StableMarkingCondition::_analyze(AnalysisContext &context)
 
742
        {
 
743
            auto coloredContext = dynamic_cast<ColoredAnalysisContext*>(&context);
 
744
            std::vector<Condition_ptr> stable_check;
 
745
            if(coloredContext != nullptr && coloredContext->isColored())
 
746
            {
 
747
                for(auto& cpn : coloredContext->allColoredPlaceNames())
 
748
                {
 
749
                    std::vector<Expr_ptr> sum;
 
750
                    MarkVal init_marking = 0;
 
751
                    for(auto& pn : cpn.second)
 
752
                    {
 
753
                        auto id = std::make_shared<UnfoldedIdentifierExpr>(pn.second);
 
754
                        id->analyze(context);
 
755
                        init_marking += context.net()->initial(id->offset());
 
756
                        sum.emplace_back(std::move(id));
 
757
 
 
758
                    }
 
759
                    stable_check.emplace_back(std::make_shared<AGCondition>(std::make_shared<EqualCondition>(
 
760
                            std::make_shared<PlusExpr>(std::move(sum)),
 
761
                            std::make_shared<LiteralExpr>(init_marking))));
 
762
                }
 
763
            }
 
764
            else
 
765
            {
 
766
                size_t i = 0;
 
767
                for(auto& p : context.net()->placeNames())
 
768
                {
 
769
                    stable_check.emplace_back(std::make_shared<AGCondition>(std::make_shared<EqualCondition>(
 
770
                            std::make_shared<UnfoldedIdentifierExpr>(p, i),
 
771
                            std::make_shared<LiteralExpr>(context.net()->initial(i)))));
 
772
                    ++i;
 
773
                }
 
774
            }
 
775
            _compiled = std::make_shared<OrCondition>(std::move(stable_check));
 
776
            _compiled->analyze(context);
 
777
        }
 
778
 
 
779
        void UpperBoundsCondition::_analyze(AnalysisContext& context)
 
780
        {
 
781
            auto coloredContext = dynamic_cast<ColoredAnalysisContext*>(&context);
 
782
            if(coloredContext != nullptr && coloredContext->isColored())
 
783
            {
 
784
                std::vector<std::string> uplaces;
 
785
                for(auto& p : _places)
 
786
                {
 
787
                    std::unordered_map<uint32_t,std::string> names;
 
788
                    if (!coloredContext->resolvePlace(p, names)) {
 
789
                        ExprError error("Unable to resolve colored identifier \"" + p + "\"", p.length());
 
790
                        coloredContext->reportError(error);
 
791
                    }
 
792
 
 
793
                    for(auto& id : names)
 
794
                    {
 
795
                        uplaces.push_back(names[id.first]);
 
796
                    }
 
797
                }
 
798
                _compiled = std::make_shared<UnfoldedUpperBoundsCondition>(uplaces);
 
799
            } else {
 
800
                _compiled = std::make_shared<UnfoldedUpperBoundsCondition>(_places);
 
801
            }
 
802
            _compiled->analyze(context);
 
803
        }
 
804
        
 
805
        void UnfoldedUpperBoundsCondition::analyze(AnalysisContext& c)
 
806
        {
 
807
            for(auto& p : _places)
 
808
            {
 
809
                AnalysisContext::ResolutionResult result = c.resolve(p._name);
 
810
                if (result.success) {
 
811
                    p._place = result.offset;
 
812
                } else {
 
813
                    ExprError error("Unable to resolve identifier \"" + p._name + "\"",
 
814
                            p._name.length());
 
815
                    c.reportError(error);
 
816
                }
 
817
            }
 
818
            std::sort(_places.begin(), _places.end());
 
819
        }
 
820
 
 
821
        /******************** Evaluation ********************/
 
822
 
 
823
        int NaryExpr::evaluate(const EvaluationContext& context) {
 
824
            int32_t r = preOp(context);
 
825
            for(size_t i = 1; i < _exprs.size(); ++i)
 
826
            {
 
827
                r = apply(r, _exprs[i]->evalAndSet(context));
 
828
            }
 
829
            return r;
 
830
        }
 
831
        
 
832
        int32_t NaryExpr::preOp(const EvaluationContext& context) const {
 
833
            return _exprs[0]->evaluate(context);
 
834
        }
 
835
 
 
836
        int32_t CommutativeExpr::preOp(const EvaluationContext& context) const {
 
837
            int32_t res = _constant;
 
838
            for(auto& i : _ids) res = this->apply(res, context.marking()[i.first]);
 
839
            if(_exprs.size() > 0) res = this->apply(res, _exprs[0]->evalAndSet(context));
 
840
            return res;
 
841
        }
 
842
 
 
843
        int CommutativeExpr::evaluate(const EvaluationContext& context) {
 
844
            if(_exprs.size() == 0) return preOp(context);
 
845
            return NaryExpr::evaluate(context);
 
846
        }
 
847
        
 
848
        int MinusExpr::evaluate(const EvaluationContext& context) {
 
849
            return -(_expr->evaluate(context));
 
850
        }
 
851
 
 
852
        int LiteralExpr::evaluate(const EvaluationContext&) {
 
853
            return _value;
 
854
        }
 
855
 
 
856
        int UnfoldedIdentifierExpr::evaluate(const EvaluationContext& context) {
 
857
            assert(_offsetInMarking != -1);
 
858
            return context.marking()[_offsetInMarking];
 
859
        }
 
860
 
 
861
        Condition::Result SimpleQuantifierCondition::evaluate(const EvaluationContext& context) {
 
862
            return RUNKNOWN;
 
863
        }
 
864
 
 
865
        Condition::Result EGCondition::evaluate(const EvaluationContext& context) {
 
866
            if(_cond->evaluate(context) == RFALSE) return RFALSE;
 
867
            return RUNKNOWN;
 
868
        }
 
869
 
 
870
        Condition::Result AGCondition::evaluate(const EvaluationContext& context) 
 
871
        {
 
872
            if(_cond->evaluate(context) == RFALSE) return RFALSE;
 
873
            return RUNKNOWN;
 
874
        }
 
875
 
 
876
        Condition::Result EFCondition::evaluate(const EvaluationContext& context) {
 
877
            if(_cond->evaluate(context) == RTRUE) return RTRUE;
 
878
            return RUNKNOWN;
 
879
        }
 
880
 
 
881
        Condition::Result AFCondition::evaluate(const EvaluationContext& context) {
 
882
            if(_cond->evaluate(context) == RTRUE) return RTRUE;
 
883
            return RUNKNOWN;
 
884
        }
 
885
 
 
886
        
 
887
        Condition::Result UntilCondition::evaluate(const EvaluationContext& context) {
 
888
            auto r2 = _cond2->evaluate(context);
 
889
            if(r2 != RFALSE) return r2;
 
890
            auto r1 = _cond1->evaluate(context);
 
891
            if(r1 == RFALSE)
 
892
            {
 
893
                return RFALSE;
 
894
            }
 
895
            return RUNKNOWN;
 
896
        }
 
897
        
 
898
 
 
899
        
 
900
        Condition::Result AndCondition::evaluate(const EvaluationContext& context) {
 
901
            auto res = RTRUE;            
 
902
            for(auto& c : _conds)
 
903
            {
 
904
                auto r = c->evaluate(context);
 
905
                if(r == RFALSE) return RFALSE;
 
906
                else if(r == RUNKNOWN) res = RUNKNOWN;
 
907
            }
 
908
            return res;
 
909
        }
 
910
 
 
911
        Condition::Result OrCondition::evaluate(const EvaluationContext& context) {
 
912
            auto res = RFALSE;            
 
913
            for(auto& c : _conds)
 
914
            {
 
915
                auto r = c->evaluate(context);
 
916
                if(r == RTRUE) return RTRUE;
 
917
                else if(r == RUNKNOWN) res = RUNKNOWN;
 
918
            }
 
919
            return res;
 
920
        }
 
921
        
 
922
        Condition::Result CompareConjunction::evaluate(const EvaluationContext& context){
 
923
//            auto rres = _org->evaluate(context);
 
924
            bool res = true;
 
925
            for(auto& c : _constraints)
 
926
            {
 
927
                res = res && context.marking()[c._place] <= c._upper &&
 
928
                             context.marking()[c._place] >= c._lower;
 
929
                if(!res) break;
 
930
            }
 
931
            return (_negated xor res) ? RTRUE : RFALSE;
 
932
        }
 
933
        
 
934
        Condition::Result CompareCondition::evaluate(const EvaluationContext& context) {
 
935
            int v1 = _expr1->evaluate(context);
 
936
            int v2 = _expr2->evaluate(context);
 
937
            return apply(v1, v2) ? RTRUE : RFALSE;
 
938
        }
 
939
 
 
940
        Condition::Result NotCondition::evaluate(const EvaluationContext& context) {
 
941
            auto res = _cond->evaluate(context);
 
942
            if(res != RUNKNOWN) return res == RFALSE ? RTRUE : RFALSE;
 
943
            return RUNKNOWN;
 
944
        }
 
945
 
 
946
        Condition::Result BooleanCondition::evaluate(const EvaluationContext&) {
 
947
            return _value ? RTRUE : RFALSE;
 
948
        }
 
949
 
 
950
        Condition::Result DeadlockCondition::evaluate(const EvaluationContext& context) {
 
951
            if (!context.net())
 
952
                return RFALSE;
 
953
            if (!context.net()->deadlocked(context.marking())) {
 
954
                return RFALSE;
 
955
            }
 
956
            return RTRUE;
 
957
        }
 
958
        
 
959
        size_t UnfoldedUpperBoundsCondition::value(const MarkVal* marking)
 
960
        {
 
961
            size_t tmp = 0;
 
962
            for(auto& p : _places)
 
963
            {
 
964
                auto val = marking[p._place];
 
965
                p._maxed_out = (p._max <= val);
 
966
                tmp += val;
 
967
            }
 
968
            return tmp;
 
969
        }
 
970
        
 
971
        Condition::Result UnfoldedUpperBoundsCondition::evaluate(const EvaluationContext& context) {
 
972
            setUpperBound(value(context.marking()));
 
973
            return _max <= _bound ? RTRUE : RUNKNOWN;
 
974
        }
 
975
        
 
976
        /******************** Evaluation - save result ********************/
 
977
        Condition::Result SimpleQuantifierCondition::evalAndSet(const EvaluationContext& context) {
 
978
            return RUNKNOWN;
 
979
        }
 
980
 
 
981
        Condition::Result EGCondition::evalAndSet(const EvaluationContext& context) {
 
982
            auto res = _cond->evalAndSet(context);
 
983
            if(res != RFALSE) res = RUNKNOWN;
 
984
            setSatisfied(res);
 
985
            return res;
 
986
        }
 
987
 
 
988
        Condition::Result AGCondition::evalAndSet(const EvaluationContext& context) {
 
989
            auto res = _cond->evalAndSet(context);
 
990
            if(res != RFALSE) res = RUNKNOWN;
 
991
            setSatisfied(res);
 
992
            return res;
 
993
        }
 
994
 
 
995
        Condition::Result EFCondition::evalAndSet(const EvaluationContext& context) {
 
996
            auto res = _cond->evalAndSet(context);
 
997
            if(res != RTRUE) res = RUNKNOWN;
 
998
            setSatisfied(res);
 
999
            return res;
 
1000
        }
 
1001
 
 
1002
        Condition::Result AFCondition::evalAndSet(const EvaluationContext& context) {
 
1003
            auto res = _cond->evalAndSet(context);
 
1004
            if(res != RTRUE) res = RUNKNOWN;
 
1005
            setSatisfied(res);
 
1006
            return res;
 
1007
        }
 
1008
        
 
1009
        Condition::Result UntilCondition::evalAndSet(const EvaluationContext& context) {
 
1010
            auto r2 = _cond2->evalAndSet(context);
 
1011
            if(r2 != RFALSE) return r2;
 
1012
            auto r1 = _cond1->evalAndSet(context);
 
1013
            if(r1 == RFALSE) return RFALSE;
 
1014
            return RUNKNOWN;
 
1015
        }        
 
1016
 
 
1017
        int Expr::evalAndSet(const EvaluationContext& context) {
 
1018
            int r = evaluate(context);
 
1019
            setEval(r);
 
1020
            return r;
 
1021
        }
 
1022
 
 
1023
        Condition::Result AndCondition::evalAndSet(const EvaluationContext& context) {
 
1024
            Result res = RTRUE;
 
1025
            for(auto& c : _conds)
 
1026
            {
 
1027
                auto r = c->evalAndSet(context);
 
1028
                if(r == RFALSE)
 
1029
                {
 
1030
                    res = RFALSE;
 
1031
                    break;
 
1032
                }
 
1033
                else if(r == RUNKNOWN)
 
1034
                {
 
1035
                    res = RUNKNOWN;
 
1036
                }
 
1037
            }
 
1038
            setSatisfied(res);
 
1039
            return res;
 
1040
        }
 
1041
 
 
1042
        Condition::Result OrCondition::evalAndSet(const EvaluationContext& context) {
 
1043
            Result res = RFALSE;
 
1044
            for(auto& c : _conds)
 
1045
            {
 
1046
                auto r = c->evalAndSet(context);
 
1047
                if(r == RTRUE)
 
1048
                {
 
1049
                    res = RTRUE;
 
1050
                    break;
 
1051
                }
 
1052
                else if(r == RUNKNOWN)
 
1053
                {
 
1054
                    res = RUNKNOWN;
 
1055
                }
 
1056
            }
 
1057
            setSatisfied(res);
 
1058
            return res;
 
1059
        }
 
1060
 
 
1061
        Condition::Result CompareConjunction::evalAndSet(const EvaluationContext& context)
 
1062
        {
 
1063
            auto res = evaluate(context);
 
1064
            setSatisfied(res);
 
1065
            return res;
 
1066
        }
 
1067
        
 
1068
        Condition::Result CompareCondition::evalAndSet(const EvaluationContext& context) {
 
1069
            int v1 = _expr1->evalAndSet(context);
 
1070
            int v2 = _expr2->evalAndSet(context);
 
1071
            bool res = apply(v1, v2);
 
1072
            setSatisfied(res);
 
1073
            return res ? RTRUE : RFALSE;
 
1074
        }
 
1075
 
 
1076
        Condition::Result NotCondition::evalAndSet(const EvaluationContext& context) {
 
1077
            auto res = _cond->evalAndSet(context);
 
1078
            if(res != RUNKNOWN) res = res == RFALSE ? RTRUE : RFALSE;
 
1079
            setSatisfied(res);
 
1080
            return res;
 
1081
        }
 
1082
 
 
1083
        Condition::Result BooleanCondition::evalAndSet(const EvaluationContext&) {
 
1084
            setSatisfied(_value);
 
1085
            return _value ? RTRUE : RFALSE;
 
1086
        }
 
1087
 
 
1088
        Condition::Result DeadlockCondition::evalAndSet(const EvaluationContext& context) {
 
1089
            if (!context.net())
 
1090
                return RFALSE;
 
1091
            setSatisfied(context.net()->deadlocked(context.marking()));
 
1092
            return isSatisfied() ? RTRUE : RFALSE;
 
1093
        }
 
1094
        
 
1095
        Condition::Result UnfoldedUpperBoundsCondition::evalAndSet(const EvaluationContext& context)
 
1096
        {
 
1097
            auto res = evaluate(context);
 
1098
            setSatisfied(res);
 
1099
            return res;
 
1100
        }
 
1101
 
 
1102
        /******************** Range Contexts ********************/
 
1103
 
 
1104
 
 
1105
        void EGCondition::visit(Visitor& ctx) const
 
1106
        {
 
1107
            ctx.accept<decltype(this)>(this);
 
1108
        }
 
1109
 
 
1110
        void EUCondition::visit(Visitor& ctx) const
 
1111
        {
 
1112
            ctx.accept<decltype(this)>(this);
 
1113
        }
 
1114
        
 
1115
        void EXCondition::visit(Visitor& ctx) const
 
1116
        {
 
1117
            ctx.accept<decltype(this)>(this);
 
1118
        }
 
1119
        
 
1120
        void EFCondition::visit(Visitor& ctx) const
 
1121
        {
 
1122
            ctx.accept<decltype(this)>(this);
 
1123
        }
 
1124
 
 
1125
        void AUCondition::visit(Visitor& ctx) const
 
1126
        {
 
1127
            ctx.accept<decltype(this)>(this);
 
1128
        }        
 
1129
 
 
1130
        void AXCondition::visit(Visitor& ctx) const
 
1131
        {
 
1132
            ctx.accept<decltype(this)>(this);
 
1133
        }
 
1134
 
 
1135
        void AFCondition::visit(Visitor& ctx) const
 
1136
        {
 
1137
            ctx.accept<decltype(this)>(this);
 
1138
        } 
 
1139
 
 
1140
        void AGCondition::visit(Visitor& ctx) const
 
1141
        {
 
1142
            ctx.accept<decltype(this)>(this);
 
1143
        }
 
1144
        
 
1145
        void AndCondition::visit(Visitor& ctx) const
 
1146
        {
 
1147
            ctx.accept<decltype(this)>(this);
 
1148
        }
 
1149
 
 
1150
        void OrCondition::visit(Visitor& ctx) const
 
1151
        {
 
1152
            ctx.accept<decltype(this)>(this);
 
1153
        }
 
1154
 
 
1155
        void NotCondition::visit(Visitor& ctx) const
 
1156
        {
 
1157
            ctx.accept<decltype(this)>(this);
 
1158
        }
 
1159
        
 
1160
        void EqualCondition::visit(Visitor& ctx) const
 
1161
        {
 
1162
            ctx.accept<decltype(this)>(this);
 
1163
        }
 
1164
 
 
1165
        void NotEqualCondition::visit(Visitor& ctx) const
 
1166
        {
 
1167
            ctx.accept<decltype(this)>(this);
 
1168
        }
 
1169
 
 
1170
        void CompareConjunction::visit(Visitor& ctx) const
 
1171
        {
 
1172
            ctx.accept<decltype(this)>(this);
 
1173
        }
 
1174
        
 
1175
        void GreaterThanOrEqualCondition::visit(Visitor& ctx) const
 
1176
        {
 
1177
            ctx.accept<decltype(this)>(this);
 
1178
        }
 
1179
 
 
1180
        void LessThanOrEqualCondition::visit(Visitor& ctx) const
 
1181
        {
 
1182
            ctx.accept<decltype(this)>(this);
 
1183
        }
 
1184
        
 
1185
        void GreaterThanCondition::visit(Visitor& ctx) const
 
1186
        {
 
1187
            ctx.accept<decltype(this)>(this);
 
1188
        }
 
1189
 
 
1190
        void LessThanCondition::visit(Visitor& ctx) const
 
1191
        {
 
1192
            ctx.accept<decltype(this)>(this);
 
1193
        }
 
1194
        
 
1195
        void BooleanCondition::visit(Visitor& ctx) const
 
1196
        {
 
1197
            ctx.accept<decltype(this)>(this);
 
1198
        }
 
1199
        
 
1200
        void DeadlockCondition::visit(Visitor& ctx) const
 
1201
        {
 
1202
            ctx.accept<decltype(this)>(this);
 
1203
        }
 
1204
 
 
1205
        void StableMarkingCondition::visit(Visitor& ctx) const
 
1206
        {
 
1207
            if(_compiled)
 
1208
                _compiled->visit(ctx);
 
1209
            else
 
1210
                ctx.accept<decltype(this)>(this);
 
1211
        }
 
1212
 
 
1213
        void QuasiLivenessCondition::visit(Visitor& ctx) const
 
1214
        {
 
1215
            if(_compiled)
 
1216
                _compiled->visit(ctx);
 
1217
            else
 
1218
                ctx.accept<decltype(this)>(this);
 
1219
        }
 
1220
 
 
1221
        void KSafeCondition::visit(Visitor& ctx) const
 
1222
        {
 
1223
            if(_compiled)
 
1224
                _compiled->visit(ctx);
 
1225
            else
 
1226
                ctx.accept<decltype(this)>(this);
 
1227
        }
 
1228
 
 
1229
        void LivenessCondition::visit(Visitor& ctx) const
 
1230
        {
 
1231
            if(_compiled)
 
1232
                _compiled->visit(ctx);
 
1233
            else
 
1234
                ctx.accept<decltype(this)>(this);
 
1235
        }
 
1236
 
 
1237
        void FireableCondition::visit(Visitor& ctx) const
 
1238
        {
 
1239
            if(_compiled)
 
1240
                _compiled->visit(ctx);
 
1241
            else
 
1242
                ctx.accept<decltype(this)>(this);
 
1243
        }
 
1244
 
 
1245
        void UpperBoundsCondition::visit(Visitor& ctx) const
 
1246
        {
 
1247
            if(_compiled)
 
1248
                _compiled->visit(ctx);
 
1249
            else
 
1250
                ctx.accept<decltype(this)>(this);
 
1251
        }
 
1252
        
 
1253
        void UnfoldedFireableCondition::visit(Visitor& ctx) const
 
1254
        {
 
1255
            if(_compiled)
 
1256
                _compiled->visit(ctx);
 
1257
            else
 
1258
                ctx.accept<decltype(this)>(this);
 
1259
        }
 
1260
 
 
1261
               
 
1262
        void UnfoldedUpperBoundsCondition::visit(Visitor& ctx) const
 
1263
        {
 
1264
            ctx.accept<decltype(this)>(this);
 
1265
        }
 
1266
        
 
1267
        void LiteralExpr::visit(Visitor& ctx) const
 
1268
        {
 
1269
            ctx.accept<decltype(this)>(this);
 
1270
        }
 
1271
 
 
1272
        void IdentifierExpr::visit(Visitor& ctx) const
 
1273
        {
 
1274
            if(_compiled)
 
1275
                _compiled->visit(ctx);
 
1276
            else
 
1277
                ctx.accept<decltype(this)>(this);
 
1278
        }
 
1279
 
 
1280
        void UnfoldedIdentifierExpr::visit(Visitor& ctx) const
 
1281
        {
 
1282
            ctx.accept<decltype(this)>(this);
 
1283
        }
 
1284
 
 
1285
        void MinusExpr::visit(Visitor& ctx) const
 
1286
        {
 
1287
            ctx.accept<decltype(this)>(this);
 
1288
        }
 
1289
 
 
1290
        void SubtractExpr::visit(Visitor& ctx) const
 
1291
        {
 
1292
            ctx.accept<decltype(this)>(this);
 
1293
        }
 
1294
 
 
1295
        void PlusExpr::visit(Visitor& ctx) const
 
1296
        {
 
1297
            ctx.accept<decltype(this)>(this);
 
1298
        }
 
1299
 
 
1300
        void MultiplyExpr::visit(Visitor& ctx) const
 
1301
        {
 
1302
            ctx.accept<decltype(this)>(this);
 
1303
        }
 
1304
 
 
1305
        /******************** Apply (BinaryExpr subclasses) ********************/
 
1306
 
 
1307
        int PlusExpr::apply(int v1, int v2) const {
 
1308
            return v1 + v2;
 
1309
        }
 
1310
 
 
1311
        int SubtractExpr::apply(int v1, int v2) const {
 
1312
            return v1 - v2;
 
1313
        }
 
1314
 
 
1315
        int MultiplyExpr::apply(int v1, int v2) const {
 
1316
            return v1 * v2;
 
1317
        }
 
1318
        
 
1319
        /******************** Apply (CompareCondition subclasses) ********************/
 
1320
 
 
1321
        bool EqualCondition::apply(int v1, int v2) const {
 
1322
            return v1 == v2;
 
1323
        }
 
1324
 
 
1325
        bool NotEqualCondition::apply(int v1, int v2) const {
 
1326
            return v1 != v2;
 
1327
        }
 
1328
 
 
1329
        bool LessThanCondition::apply(int v1, int v2) const {
 
1330
            return v1 < v2;
 
1331
        }
 
1332
 
 
1333
        bool LessThanOrEqualCondition::apply(int v1, int v2) const {
 
1334
            return v1 <= v2;
 
1335
        }
 
1336
 
 
1337
        bool GreaterThanCondition::apply(int v1, int v2) const {
 
1338
            return v1 > v2;
 
1339
        }
 
1340
 
 
1341
        bool GreaterThanOrEqualCondition::apply(int v1, int v2) const {
 
1342
            return v1 >= v2;
 
1343
        }
 
1344
 
 
1345
        /******************** Op (BinaryExpr subclasses) ********************/
 
1346
 
 
1347
        std::string PlusExpr::op() const {
 
1348
            return "+";
 
1349
        }
 
1350
 
 
1351
        std::string SubtractExpr::op() const {
 
1352
            return "-";
 
1353
        }
 
1354
 
 
1355
        std::string MultiplyExpr::op() const {
 
1356
            return "*";
 
1357
        }
 
1358
        
 
1359
        /******************** Op (QuantifierCondition subclasses) ********************/
 
1360
        
 
1361
        std::string EXCondition::op() const {
 
1362
            return "EX";
 
1363
        }
 
1364
        
 
1365
        std::string EGCondition::op() const {
 
1366
            return "EG";
 
1367
        }
 
1368
        
 
1369
        std::string EFCondition::op() const {
 
1370
            return "EF";
 
1371
        }
 
1372
        
 
1373
        std::string AXCondition::op() const {
 
1374
            return "AX";
 
1375
        }
 
1376
        
 
1377
        std::string AGCondition::op() const {
 
1378
            return "AG";
 
1379
        }
 
1380
        
 
1381
        std::string AFCondition::op() const {
 
1382
            return "AF";
 
1383
        }
 
1384
        
 
1385
        /******************** Op (UntilCondition subclasses) ********************/
 
1386
 
 
1387
        std::string EUCondition::op() const {
 
1388
            return "E";
 
1389
        }
 
1390
        
 
1391
        std::string AUCondition::op() const {
 
1392
            return "A";
 
1393
        }
 
1394
        
 
1395
        /******************** Op (LogicalCondition subclasses) ********************/
 
1396
 
 
1397
        std::string AndCondition::op() const {
 
1398
            return "and";
 
1399
        }
 
1400
 
 
1401
        std::string OrCondition::op() const {
 
1402
            return "or";
 
1403
        }
 
1404
 
 
1405
        /******************** Op (CompareCondition subclasses) ********************/
 
1406
 
 
1407
        std::string EqualCondition::op() const {
 
1408
            return "==";
 
1409
        }
 
1410
 
 
1411
        std::string NotEqualCondition::op() const {
 
1412
            return "!=";
 
1413
        }
 
1414
 
 
1415
        std::string LessThanCondition::op() const {
 
1416
            return "<";
 
1417
        }
 
1418
 
 
1419
        std::string LessThanOrEqualCondition::op() const {
 
1420
            return "<=";
 
1421
        }
 
1422
 
 
1423
        std::string GreaterThanCondition::op() const {
 
1424
            return ">";
 
1425
        }
 
1426
 
 
1427
        std::string GreaterThanOrEqualCondition::op() const {
 
1428
            return ">=";
 
1429
        }
 
1430
 
 
1431
        /******************** free of places ********************/        
 
1432
 
 
1433
        bool NaryExpr::placeFree() const
 
1434
        {
 
1435
            for(auto& e : _exprs)
 
1436
                if(!e->placeFree())
 
1437
                    return false;
 
1438
            return true;
 
1439
        }
 
1440
        
 
1441
        bool CommutativeExpr::placeFree() const
 
1442
        {
 
1443
            if(_ids.size() > 0) return false;
 
1444
            return NaryExpr::placeFree();
 
1445
        }
 
1446
        
 
1447
        bool MinusExpr::placeFree() const
 
1448
        {
 
1449
            return _expr->placeFree();
 
1450
        }
 
1451
        
 
1452
        /******************** Expr::type() implementation ********************/
 
1453
 
 
1454
        Expr::Types PlusExpr::type() const {
 
1455
            return Expr::PlusExpr;
 
1456
        }
 
1457
 
 
1458
        Expr::Types SubtractExpr::type() const {
 
1459
            return Expr::SubtractExpr;
 
1460
        }
 
1461
 
 
1462
        Expr::Types MultiplyExpr::type() const {
 
1463
            return Expr::MinusExpr;
 
1464
        }
 
1465
 
 
1466
        Expr::Types MinusExpr::type() const {
 
1467
            return Expr::MinusExpr;
 
1468
        }
 
1469
 
 
1470
        Expr::Types LiteralExpr::type() const {
 
1471
            return Expr::LiteralExpr;
 
1472
        }
 
1473
 
 
1474
        Expr::Types UnfoldedIdentifierExpr::type() const {
 
1475
            return Expr::IdentifierExpr;
 
1476
        }
 
1477
 
 
1478
        /******************** Distance Condition ********************/
 
1479
 
 
1480
#define MAX(v1, v2)  (v1 > v2 ? v1 : v2)
 
1481
#define MIN(v1, v2)  (v1 < v2 ? v1 : v2)
 
1482
 
 
1483
        template<>
 
1484
        uint32_t delta<EqualCondition>(int v1, int v2, bool negated) {
 
1485
            if (!negated)
 
1486
                return std::abs(v1 - v2);
 
1487
            else
 
1488
                return v1 == v2 ? 1 : 0;
 
1489
        }
 
1490
 
 
1491
        template<>
 
1492
        uint32_t delta<NotEqualCondition>(int v1, int v2, bool negated) {
 
1493
            return delta<EqualCondition>(v1, v2, !negated);
 
1494
        }
 
1495
 
 
1496
        template<>
 
1497
        uint32_t delta<LessThanCondition>(int v1, int v2, bool negated) {
 
1498
            if (!negated)
 
1499
                return v1 < v2 ? 0 : v1 - v2 + 1;
 
1500
            else
 
1501
                return v1 >= v2 ? 0 : v2 - v1;
 
1502
        }
 
1503
 
 
1504
        template<>
 
1505
        uint32_t delta<LessThanOrEqualCondition>(int v1, int v2, bool negated) {
 
1506
            if (!negated)
 
1507
                return v1 <= v2 ? 0 : v1 - v2;
 
1508
            else
 
1509
                return v1 > v2 ? 0 : v2 - v1 + 1;
 
1510
        }
 
1511
 
 
1512
        template<>
 
1513
        uint32_t delta<GreaterThanCondition>(int v1, int v2, bool negated) {
 
1514
            return delta<LessThanOrEqualCondition>(v1, v2, !negated);
 
1515
        }
 
1516
 
 
1517
        template<>
 
1518
        uint32_t delta<GreaterThanOrEqualCondition>(int v1, int v2, bool negated) {
 
1519
            return delta<LessThanCondition>(v1, v2, !negated);
 
1520
        }
 
1521
 
 
1522
        uint32_t NotCondition::distance(DistanceContext& context) const {
 
1523
            context.negate();
 
1524
            uint32_t retval = _cond->distance(context);
 
1525
            context.negate();
 
1526
            return retval;
 
1527
        }
 
1528
 
 
1529
        uint32_t BooleanCondition::distance(DistanceContext& context) const {
 
1530
            if (context.negated() != _value)
 
1531
                return 0;
 
1532
            return std::numeric_limits<uint32_t>::max();
 
1533
        }
 
1534
 
 
1535
        uint32_t DeadlockCondition::distance(DistanceContext& context) const {
 
1536
            return 0;
 
1537
        }
 
1538
 
 
1539
        uint32_t UnfoldedUpperBoundsCondition::distance(DistanceContext& context) const 
 
1540
        {
 
1541
            size_t tmp = 0;
 
1542
            for(auto& p : _places)
 
1543
            {
 
1544
                tmp += context.marking()[p._place];
 
1545
            }
 
1546
            
 
1547
            return _max - tmp;
 
1548
        }
 
1549
        
 
1550
        uint32_t EFCondition::distance(DistanceContext& context) const {
 
1551
            return _cond->distance(context);
 
1552
        }
 
1553
 
 
1554
        uint32_t EGCondition::distance(DistanceContext& context) const {
 
1555
            return _cond->distance(context);
 
1556
        }
 
1557
 
 
1558
        uint32_t EXCondition::distance(DistanceContext& context) const {
 
1559
            return _cond->distance(context);
 
1560
        }
 
1561
 
 
1562
        uint32_t EUCondition::distance(DistanceContext& context) const {
 
1563
            return _cond2->distance(context);
 
1564
        }
 
1565
        
 
1566
        uint32_t AFCondition::distance(DistanceContext& context) const {
 
1567
            context.negate();
 
1568
            uint32_t retval = _cond->distance(context);
 
1569
            context.negate();
 
1570
            return retval;
 
1571
        }
 
1572
        
 
1573
        uint32_t AXCondition::distance(DistanceContext& context) const {
 
1574
            context.negate();
 
1575
            uint32_t retval = _cond->distance(context);
 
1576
            context.negate();
 
1577
            return retval;
 
1578
        }
 
1579
 
 
1580
        uint32_t AGCondition::distance(DistanceContext& context) const {
 
1581
            context.negate();
 
1582
            uint32_t retval = _cond->distance(context);
 
1583
            context.negate();
 
1584
            return retval;
 
1585
        }
 
1586
 
 
1587
        uint32_t AUCondition::distance(DistanceContext& context) const {
 
1588
            context.negate();
 
1589
            auto r1 = _cond1->distance(context);
 
1590
            auto r2 = _cond2->distance(context);
 
1591
            context.negate();
 
1592
            return r1 + r2;
 
1593
        }
 
1594
        
 
1595
        uint32_t LogicalCondition::distance(DistanceContext& context) const {
 
1596
            uint32_t d = _conds[0]->distance(context);
 
1597
            for(size_t i = 1; i < _conds.size(); ++i) d = delta(d, _conds[i]->distance(context), context);
 
1598
            return d;
 
1599
        }
 
1600
        
 
1601
        uint32_t CompareConjunction::distance(DistanceContext& context) const {
 
1602
            uint32_t d = 0;
 
1603
            auto neg = context.negated() != _negated;
 
1604
            if(!neg)
 
1605
            {
 
1606
                for(auto& c : _constraints)
 
1607
                {
 
1608
                    auto pv = context.marking()[c._place];
 
1609
                    d += (c._upper == std::numeric_limits<uint32_t>::max() ? 0 : delta<LessThanOrEqualCondition>(pv, c._upper, neg)) +
 
1610
                         (c._lower == 0 ? 0 : delta<GreaterThanOrEqualCondition>(pv, c._lower, neg));
 
1611
                }
 
1612
            }
 
1613
            else
 
1614
            {
 
1615
                bool first = true;
 
1616
                for(auto& c : _constraints)
 
1617
                {
 
1618
                    auto pv = context.marking()[c._place];
 
1619
                    if(c._upper != std::numeric_limits<uint32_t>::max())
 
1620
                    {
 
1621
                        auto d2 = delta<LessThanOrEqualCondition>(pv, c._upper, neg);
 
1622
                        if(first) d = d2;
 
1623
                        else      d = MIN(d, d2);
 
1624
                        first = false;
 
1625
                    }
 
1626
                    
 
1627
                    if(c._lower != 0)
 
1628
                    {
 
1629
                        auto d2 = delta<GreaterThanOrEqualCondition>(pv, c._upper, neg);
 
1630
                        if(first) d = d2;
 
1631
                        else      d = MIN(d, d2);
 
1632
                        first = false;
 
1633
                    }
 
1634
                }
 
1635
            }
 
1636
            return d;
 
1637
        }
 
1638
 
 
1639
        uint32_t AndCondition::delta(uint32_t d1,
 
1640
                uint32_t d2,
 
1641
                const DistanceContext& context) const {
 
1642
                return d1 + d2;
 
1643
        }
 
1644
 
 
1645
        uint32_t OrCondition::delta(uint32_t d1,
 
1646
                uint32_t d2,
 
1647
                const DistanceContext& context) const {
 
1648
            if (context.negated())
 
1649
                return MAX(d1, d2);
 
1650
            else
 
1651
                return MIN(d1, d2);
 
1652
        }
 
1653
 
 
1654
        struct S {
 
1655
            int d;
 
1656
            unsigned int p;
 
1657
        };
 
1658
       
 
1659
        uint32_t LessThanOrEqualCondition::distance(DistanceContext& context) const {
 
1660
            return _distance(context, delta<LessThanOrEqualCondition>);
 
1661
        }
 
1662
        
 
1663
        uint32_t GreaterThanOrEqualCondition::distance(DistanceContext& context) const {
 
1664
            return _distance(context, delta<GreaterThanOrEqualCondition>);
 
1665
        }
 
1666
       
 
1667
        uint32_t LessThanCondition::distance(DistanceContext& context) const {
 
1668
            return _distance(context, delta<LessThanCondition>);
 
1669
        }
 
1670
       
 
1671
        uint32_t GreaterThanCondition::distance(DistanceContext& context) const {
 
1672
            return _distance(context, delta<GreaterThanCondition>);
 
1673
        }
 
1674
       
 
1675
        uint32_t NotEqualCondition::distance(DistanceContext& context) const {
 
1676
            return _distance(context, delta<NotEqualCondition>);
 
1677
        }
 
1678
       
 
1679
        uint32_t EqualCondition::distance(DistanceContext& context) const {
 
1680
            return _distance(context, delta<EqualCondition>);
 
1681
        }
 
1682
 
 
1683
        /******************** BIN output ********************/
 
1684
        
 
1685
        void LiteralExpr::toBinary(std::ostream& out) const {
 
1686
            out.write("l", sizeof(char));
 
1687
            out.write(reinterpret_cast<const char*>(&_value), sizeof(int));
 
1688
        }
 
1689
        
 
1690
        void UnfoldedIdentifierExpr::toBinary(std::ostream& out) const {
 
1691
            out.write("i", sizeof(char));
 
1692
            out.write(reinterpret_cast<const char*>(&_offsetInMarking), sizeof(int));            
 
1693
        }
 
1694
        
 
1695
        void MinusExpr::toBinary(std::ostream& out) const
 
1696
        {
 
1697
            auto e1 = std::make_shared<PQL::LiteralExpr>(0);
 
1698
            std::vector<Expr_ptr> exprs;
 
1699
            exprs.push_back(e1);
 
1700
            exprs.push_back(_expr);
 
1701
            PQL::SubtractExpr(std::move(exprs)).toBinary(out);
 
1702
        }
 
1703
        
 
1704
        void SubtractExpr::toBinary(std::ostream& out) const {
 
1705
            out.write("-", sizeof(char));
 
1706
            uint32_t size = _exprs.size();
 
1707
            out.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
 
1708
            for(auto& e : _exprs)
 
1709
                e->toBinary(out);
 
1710
        }
 
1711
 
 
1712
        void CommutativeExpr::toBinary(std::ostream& out) const
 
1713
        {
 
1714
            auto sop = op();
 
1715
            out.write(&sop[0], sizeof(char));
 
1716
            out.write(reinterpret_cast<const char*>(&_constant), sizeof(int32_t));
 
1717
            uint32_t size = _ids.size();
 
1718
            out.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
 
1719
            size = _exprs.size();
 
1720
            out.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
 
1721
            for(auto& id : _ids)
 
1722
                out.write(reinterpret_cast<const char*>(&id.first), sizeof(uint32_t));
 
1723
            for(auto& e : _exprs)
 
1724
                e->toBinary(out);
 
1725
        }
 
1726
        
 
1727
        void SimpleQuantifierCondition::toBinary(std::ostream& out) const
 
1728
        {
 
1729
            auto path = getPath();
 
1730
            auto quant = getQuantifier();
 
1731
            out.write(reinterpret_cast<const char*>(&path), sizeof(Path));
 
1732
            out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
 
1733
            _cond->toBinary(out);
 
1734
        }
 
1735
        
 
1736
        void UntilCondition::toBinary(std::ostream& out) const
 
1737
        {
 
1738
            auto path = getPath();
 
1739
            auto quant = getQuantifier();
 
1740
            out.write(reinterpret_cast<const char*>(&path), sizeof(Path));
 
1741
            out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
 
1742
            _cond1->toBinary(out);
 
1743
            _cond2->toBinary(out);
 
1744
        }
 
1745
        
 
1746
        void LogicalCondition::toBinary(std::ostream& out) const
 
1747
        {
 
1748
            auto path = getPath();
 
1749
            auto quant = getQuantifier();
 
1750
            out.write(reinterpret_cast<const char*>(&path), sizeof(Path));
 
1751
            out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
 
1752
            uint32_t size = _conds.size();
 
1753
            out.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
 
1754
            for(auto& c : _conds) c->toBinary(out);
 
1755
        }
 
1756
        
 
1757
        void CompareConjunction::toBinary(std::ostream& out) const
 
1758
        {
 
1759
            auto path = getPath();
 
1760
            auto quant = Quantifier::COMPCONJ;
 
1761
            out.write(reinterpret_cast<const char*>(&path), sizeof(Path));
 
1762
            out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
 
1763
            out.write(reinterpret_cast<const char*>(&_negated), sizeof(bool));
 
1764
            uint32_t size = _constraints.size();
 
1765
            out.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
 
1766
            for(auto& c : _constraints)
 
1767
            {
 
1768
                out.write(reinterpret_cast<const char*>(&c._place), sizeof(int32_t));                
 
1769
                out.write(reinterpret_cast<const char*>(&c._lower), sizeof(uint32_t));
 
1770
                out.write(reinterpret_cast<const char*>(&c._upper), sizeof(uint32_t));
 
1771
            }
 
1772
        }
 
1773
        
 
1774
        void CompareCondition::toBinary(std::ostream& out) const
 
1775
        {
 
1776
            auto path = getPath();
 
1777
            auto quant = getQuantifier();
 
1778
            out.write(reinterpret_cast<const char*>(&path), sizeof(Path));
 
1779
            out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
 
1780
            std::string sop = op();
 
1781
            out.write(sop.data(), sop.size());
 
1782
            out.write("\0", sizeof(char));
 
1783
            _expr1->toBinary(out);
 
1784
            _expr2->toBinary(out);
 
1785
        }
 
1786
        
 
1787
        void DeadlockCondition::toBinary(std::ostream& out) const
 
1788
        {
 
1789
            auto path = getPath();
 
1790
            auto quant = Quantifier::DEADLOCK;
 
1791
            out.write(reinterpret_cast<const char*>(&path), sizeof(Path));
 
1792
            out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
 
1793
        }
 
1794
        
 
1795
        void BooleanCondition::toBinary(std::ostream& out) const
 
1796
        {
 
1797
            auto path = getPath();
 
1798
            auto quant = Quantifier::PN_BOOLEAN;
 
1799
            out.write(reinterpret_cast<const char*>(&path), sizeof(Path));
 
1800
            out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
 
1801
            out.write(reinterpret_cast<const char*>(&_value), sizeof(bool));
 
1802
        }
 
1803
        
 
1804
        void UnfoldedUpperBoundsCondition::toBinary(std::ostream& out) const
 
1805
        {
 
1806
            auto path = getPath();
 
1807
            auto quant = Quantifier::UPPERBOUNDS;
 
1808
            out.write(reinterpret_cast<const char*>(&path), sizeof(Path));
 
1809
            out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));            
 
1810
            uint32_t size = _places.size();
 
1811
            out.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));                        
 
1812
            out.write(reinterpret_cast<const char*>(&_max), sizeof(double));     
 
1813
            out.write(reinterpret_cast<const char*>(&_offset), sizeof(double));     
 
1814
            for(auto& b : _places)
 
1815
            {
 
1816
                out.write(reinterpret_cast<const char*>(&b._place), sizeof(uint32_t));                        
 
1817
                out.write(reinterpret_cast<const char*>(&b._max), sizeof(double));
 
1818
            }
 
1819
        }
 
1820
        
 
1821
        void NotCondition::toBinary(std::ostream& out) const
 
1822
        {
 
1823
            auto path = getPath();
 
1824
            auto quant = getQuantifier();
 
1825
            out.write(reinterpret_cast<const char*>(&path), sizeof(Path));
 
1826
            out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
 
1827
            _cond->toBinary(out);
 
1828
        }
 
1829
        
 
1830
        /******************** CTL Output ********************/ 
 
1831
        
 
1832
        void LiteralExpr::toXML(std::ostream& out,uint32_t tabs, bool tokencount) const {
 
1833
            generateTabs(out,tabs) << "<integer-constant>" + std::to_string(_value) + "</integer-constant>\n";
 
1834
        }
 
1835
        
 
1836
        void UnfoldedIdentifierExpr::toXML(std::ostream& out,uint32_t tabs, bool tokencount) const {
 
1837
            if (tokencount) {
 
1838
                generateTabs(out,tabs) << "<place>" << _name << "</place>\n";
 
1839
            }
 
1840
            else
 
1841
            {
 
1842
                generateTabs(out,tabs) << "<tokens-count>\n"; 
 
1843
                generateTabs(out,tabs+1) << "<place>" << _name << "</place>\n";
 
1844
                generateTabs(out,tabs) << "</tokens-count>\n";
 
1845
            }
 
1846
        }
 
1847
        
 
1848
        void PlusExpr::toXML(std::ostream& ss,uint32_t tabs, bool tokencount) const {
 
1849
            if (tokencount) {
 
1850
                for(auto& e : _exprs) e->toXML(ss,tabs, tokencount);
 
1851
                return;
 
1852
            }
 
1853
            
 
1854
            if(tk) {
 
1855
                generateTabs(ss,tabs) << "<tokens-count>\n";
 
1856
                for(auto& e : _ids) generateTabs(ss,tabs+1) << "<place>" << e.second << "</place>\n";
 
1857
                for(auto& e : _exprs) e->toXML(ss,tabs+1, true);
 
1858
                generateTabs(ss,tabs) << "</tokens-count>\n";
 
1859
                return;
 
1860
            }
 
1861
            generateTabs(ss,tabs) << "<integer-sum>\n";
 
1862
            generateTabs(ss,tabs+1) << "<integer-constant>" + std::to_string(_constant) + "</integer-constant>\n";
 
1863
            for(auto& i : _ids)
 
1864
            {
 
1865
                generateTabs(ss,tabs+1) << "<tokens-count>\n"; 
 
1866
                generateTabs(ss,tabs+2) << "<place>" << i.second << "</place>\n";
 
1867
                generateTabs(ss,tabs+1) << "</tokens-count>\n";                
 
1868
            }
 
1869
            for(auto& e : _exprs) e->toXML(ss,tabs+1, tokencount);
 
1870
            generateTabs(ss,tabs) << "</integer-sum>\n";
 
1871
        }
 
1872
        
 
1873
        void SubtractExpr::toXML(std::ostream& ss,uint32_t tabs, bool tokencount) const {
 
1874
            generateTabs(ss,tabs) << "<integer-difference>\n";
 
1875
            for(auto& e : _exprs) e->toXML(ss,tabs+1);
 
1876
            generateTabs(ss,tabs) << "</integer-difference>\n";
 
1877
        }
 
1878
        
 
1879
        void MultiplyExpr::toXML(std::ostream& ss,uint32_t tabs, bool tokencount) const {
 
1880
            generateTabs(ss,tabs) << "<integer-product>\n";
 
1881
            for(auto& e : _exprs) e->toXML(ss,tabs+1);
 
1882
            generateTabs(ss,tabs) << "</integer-product>\n";
 
1883
        }
 
1884
        
 
1885
        void MinusExpr::toXML(std::ostream& out,uint32_t tabs, bool tokencount) const {
 
1886
            
 
1887
            generateTabs(out,tabs) << "<integer-product>\n";
 
1888
            _expr->toXML(out,tabs+1);
 
1889
            generateTabs(out,tabs+1) << "<integer-difference>\n" ; generateTabs(out,tabs+2) <<
 
1890
                    "<integer-constant>0</integer-constant>\n" ; generateTabs(out,tabs+2) << 
 
1891
                    "<integer-constant>1</integer-constant>\n" ; generateTabs(out,tabs+1) <<
 
1892
                    "</integer-difference>\n" ; generateTabs(out,tabs) << "</integer-product>\n";
 
1893
        }
 
1894
        
 
1895
        void EXCondition::toXML(std::ostream& out,uint32_t tabs) const {
 
1896
            generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<next>\n";
 
1897
            _cond->toXML(out,tabs+2);
 
1898
            generateTabs(out,tabs+1) << "</next>\n" ; generateTabs(out,tabs) << "</exists-path>\n";
 
1899
        }
 
1900
 
 
1901
        void AXCondition::toXML(std::ostream& out,uint32_t tabs) const {           
 
1902
            generateTabs(out,tabs) << "<all-paths>\n"; generateTabs(out,tabs+1) << "<next>\n";
 
1903
            _cond->toXML(out,tabs+2);            
 
1904
            generateTabs(out,tabs+1) << "</next>\n"; generateTabs(out,tabs) << "</all-paths>\n";
 
1905
        }
 
1906
        
 
1907
        void EFCondition::toXML(std::ostream& out,uint32_t tabs) const {
 
1908
            generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<finally>\n";
 
1909
            _cond->toXML(out,tabs+2);
 
1910
            generateTabs(out,tabs+1) << "</finally>\n" ; generateTabs(out,tabs) << "</exists-path>\n";
 
1911
        }
 
1912
        
 
1913
        void AFCondition::toXML(std::ostream& out,uint32_t tabs) const {
 
1914
            generateTabs(out,tabs) << "<all-paths>\n" ; generateTabs(out,tabs+1) << "<finally>\n";
 
1915
            _cond->toXML(out,tabs+2);
 
1916
            generateTabs(out,tabs+1) << "</finally>\n" ; generateTabs(out,tabs) << "</all-paths>\n";
 
1917
        }
 
1918
        
 
1919
        void EGCondition::toXML(std::ostream& out,uint32_t tabs) const {            
 
1920
            generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<globally>\n";
 
1921
            _cond->toXML(out,tabs+2);            
 
1922
            generateTabs(out,tabs+1) <<  "</globally>\n" ; generateTabs(out,tabs) << "</exists-path>\n";
 
1923
        }
 
1924
        
 
1925
        void AGCondition::toXML(std::ostream& out,uint32_t tabs) const {            
 
1926
            generateTabs(out,tabs) << "<all-paths>\n" ; generateTabs(out,tabs+1) << "<globally>\n";
 
1927
            _cond->toXML(out,tabs+2);
 
1928
            generateTabs(out,tabs+1) << "</globally>\n" ; generateTabs(out,tabs) << "</all-paths>\n";
 
1929
        }
 
1930
        
 
1931
        void EUCondition::toXML(std::ostream& out,uint32_t tabs) const {
 
1932
            generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<until>\n" ; generateTabs(out,tabs+2) << "<before>\n";
 
1933
            _cond1->toXML(out,tabs+3);
 
1934
            generateTabs(out,tabs+2) << "</before>\n" ; generateTabs(out,tabs+2) << "<reach>\n";
 
1935
            _cond2->toXML(out,tabs+3);
 
1936
            generateTabs(out,tabs+2) << "</reach>\n" ; generateTabs(out,tabs+1) << "</until>\n" ; generateTabs(out,tabs) << "</exists-path>\n";
 
1937
        }
 
1938
        
 
1939
        void AUCondition::toXML(std::ostream& out,uint32_t tabs) const {
 
1940
            generateTabs(out,tabs) << "<all-paths>\n" ; generateTabs(out,tabs+1) << "<until>\n" ; generateTabs(out,tabs+2) << "<before>\n";
 
1941
            _cond1->toXML(out,tabs+3);
 
1942
            generateTabs(out,tabs+2) << "</before>\n" ; generateTabs(out,tabs+2) << "<reach>\n";
 
1943
            _cond2->toXML(out,tabs+3);
 
1944
            generateTabs(out,tabs+2) << "</reach>\n" ; generateTabs(out,tabs+1) << "</until>\n" ; generateTabs(out,tabs) << "</all-paths>\n";
 
1945
        }
 
1946
        
 
1947
        void AndCondition::toXML(std::ostream& out,uint32_t tabs) const {
 
1948
            if(_conds.size() == 0)
 
1949
            {
 
1950
                BooleanCondition::TRUE_CONSTANT->toXML(out, tabs);
 
1951
                return;
 
1952
            }
 
1953
            if(_conds.size() == 1)
 
1954
            {
 
1955
                _conds[0]->toXML(out, tabs);
 
1956
                return;
 
1957
            }
 
1958
            generateTabs(out,tabs) << "<conjunction>\n";
 
1959
            _conds[0]->toXML(out, tabs + 1);
 
1960
            for(size_t i = 1; i < _conds.size(); ++i)
 
1961
            {
 
1962
                if(i + 1 == _conds.size())
 
1963
                {
 
1964
                    _conds[i]->toXML(out, tabs + i + 1);
 
1965
                }
 
1966
                else
 
1967
                {
 
1968
                    generateTabs(out,tabs + i) << "<conjunction>\n";
 
1969
                    _conds[i]->toXML(out, tabs + i + 1);
 
1970
                }
 
1971
            }
 
1972
            for(size_t i = _conds.size() - 1; i > 1; --i)
 
1973
            {
 
1974
                generateTabs(out,tabs + i) << "</conjunction>\n";                
 
1975
            }
 
1976
            generateTabs(out,tabs) << "</conjunction>\n";              
 
1977
        }
 
1978
        
 
1979
        void OrCondition::toXML(std::ostream& out,uint32_t tabs) const {
 
1980
            if(_conds.size() == 0)
 
1981
            {
 
1982
                BooleanCondition::FALSE_CONSTANT->toXML(out, tabs);
 
1983
                return;
 
1984
            }
 
1985
            if(_conds.size() == 1)
 
1986
            {
 
1987
                _conds[0]->toXML(out, tabs);
 
1988
                return;
 
1989
            }
 
1990
            generateTabs(out,tabs) << "<disjunction>\n";
 
1991
            _conds[0]->toXML(out, tabs + 1);
 
1992
            for(size_t i = 1; i < _conds.size(); ++i)
 
1993
            {
 
1994
                if(i + 1 == _conds.size())
 
1995
                {
 
1996
                    _conds[i]->toXML(out, tabs + i + 1);
 
1997
                }
 
1998
                else
 
1999
                {
 
2000
                    generateTabs(out,tabs + i) << "<disjunction>\n";
 
2001
                    _conds[i]->toXML(out, tabs + i + 1);
 
2002
                }
 
2003
            }
 
2004
            for(size_t i = _conds.size() - 1; i > 1; --i)
 
2005
            {
 
2006
                generateTabs(out,tabs + i) << "</disjunction>\n";                
 
2007
            }
 
2008
            generateTabs(out,tabs) << "</disjunction>\n";               
 
2009
        }
 
2010
 
 
2011
        void CompareConjunction::toXML(std::ostream& out, uint32_t tabs) const
 
2012
        {
 
2013
            if(_negated) generateTabs(out,tabs++) << "<negation>";
 
2014
            if(_constraints.size() == 0) BooleanCondition::TRUE_CONSTANT->toXML(out, tabs);
 
2015
            else
 
2016
            {
 
2017
                bool single = _constraints.size() == 1 && 
 
2018
                                (_constraints[0]._lower == 0 ||
 
2019
                                 _constraints[0]._upper == std::numeric_limits<uint32_t>::max());
 
2020
                if(!single) 
 
2021
                    generateTabs(out,tabs) << "<conjunction>\n";
 
2022
                for(auto& c : _constraints)
 
2023
                {
 
2024
                    if(c._lower != 0)
 
2025
                    {
 
2026
                        generateTabs(out,tabs+1) << "<integer-ge>\n";
 
2027
                        generateTabs(out,tabs+2) << "<tokens-count>\n";
 
2028
                        generateTabs(out,tabs+3) << "<place>" << c._name << "</place>\n";
 
2029
                        generateTabs(out,tabs+2) << "</tokens-count>\n";
 
2030
                        generateTabs(out,tabs+2) << "<integer-constant>" << c._lower << "</integer-constant>\n";
 
2031
                        generateTabs(out,tabs+1) << "</integer-ge>\n";  
 
2032
                    }
 
2033
                    if(c._upper != std::numeric_limits<uint32_t>::max())
 
2034
                    {
 
2035
                        generateTabs(out,tabs+1) << "<integer-le>\n";
 
2036
                        generateTabs(out,tabs+2) << "<tokens-count>\n";
 
2037
                        generateTabs(out,tabs+3) << "<place>" << c._name << "</place>\n";
 
2038
                        generateTabs(out,tabs+2) << "</tokens-count>\n";
 
2039
                        generateTabs(out,tabs+2) << "<integer-constant>" << c._upper << "</integer-constant>\n";
 
2040
                        generateTabs(out,tabs+1) << "</integer-le>\n";                      
 
2041
                    }
 
2042
                }
 
2043
                if(!single)
 
2044
                    generateTabs(out,tabs) << "</conjunction>\n";
 
2045
            }
 
2046
            if(_negated) generateTabs(out,--tabs) << "</negation>";
 
2047
        }
 
2048
 
 
2049
        void EqualCondition::toXML(std::ostream& out,uint32_t tabs) const {
 
2050
            generateTabs(out,tabs) << "<integer-eq>\n";
 
2051
            _expr1->toXML(out,tabs+1);
 
2052
            _expr2->toXML(out,tabs+1);
 
2053
            generateTabs(out,tabs) << "</integer-eq>\n";  
 
2054
        }
 
2055
        
 
2056
        void NotEqualCondition::toXML(std::ostream& out,uint32_t tabs) const {
 
2057
            generateTabs(out,tabs) << "<integer-ne>\n";
 
2058
            _expr1->toXML(out,tabs+1);
 
2059
            _expr2->toXML(out,tabs+1);
 
2060
            generateTabs(out,tabs) << "</integer-ne>\n";  
 
2061
        }
 
2062
        
 
2063
        void LessThanCondition::toXML(std::ostream& out,uint32_t tabs) const {
 
2064
            generateTabs(out,tabs) << "<integer-lt>\n";
 
2065
            _expr1->toXML(out,tabs+1);
 
2066
            _expr2->toXML(out,tabs+1);
 
2067
            generateTabs(out,tabs) << "</integer-lt>\n";  
 
2068
        }
 
2069
        
 
2070
        void LessThanOrEqualCondition::toXML(std::ostream& out,uint32_t tabs) const {
 
2071
            generateTabs(out,tabs) << "<integer-le>\n";
 
2072
            _expr1->toXML(out,tabs+1);
 
2073
            _expr2->toXML(out,tabs+1);
 
2074
            generateTabs(out,tabs) << "</integer-le>\n";  
 
2075
        }
 
2076
        
 
2077
        void GreaterThanCondition::toXML(std::ostream& out,uint32_t tabs) const {
 
2078
            generateTabs(out,tabs) << "<integer-gt>\n";
 
2079
            _expr1->toXML(out,tabs+1);
 
2080
            _expr2->toXML(out,tabs+1);
 
2081
            generateTabs(out,tabs) << "</integer-gt>\n";  
 
2082
        }
 
2083
        
 
2084
        void GreaterThanOrEqualCondition::toXML(std::ostream& out,uint32_t tabs) const {
 
2085
            
 
2086
            generateTabs(out,tabs) << "<integer-ge>\n";
 
2087
            _expr1->toXML(out,tabs+1);
 
2088
            _expr2->toXML(out,tabs+1);
 
2089
            generateTabs(out,tabs) << "</integer-ge>\n";  
 
2090
        }
 
2091
        
 
2092
        void NotCondition::toXML(std::ostream& out,uint32_t tabs) const {
 
2093
            
 
2094
            generateTabs(out,tabs) << "<negation>\n";
 
2095
            _cond->toXML(out,tabs+1);
 
2096
            generateTabs(out,tabs) << "</negation>\n";  
 
2097
        }
 
2098
        
 
2099
        void BooleanCondition::toXML(std::ostream& out,uint32_t tabs) const {            
 
2100
            generateTabs(out,tabs) << "<" << 
 
2101
                    (_value ? "true" : "false") 
 
2102
                    << "/>\n"; 
 
2103
        }
 
2104
        
 
2105
        void DeadlockCondition::toXML(std::ostream& out,uint32_t tabs) const {
 
2106
            generateTabs(out,tabs) << "<deadlock/>\n"; 
 
2107
        }
 
2108
        
 
2109
        void UnfoldedUpperBoundsCondition::toXML(std::ostream& out, uint32_t tabs) const {
 
2110
            generateTabs(out, tabs) << "<place-bound>\n";
 
2111
            for(auto& p : _places)
 
2112
                generateTabs(out, tabs + 1) << "<place>" << p._name << "</place>\n";
 
2113
            generateTabs(out, tabs) << "</place-bound>\n";
 
2114
        }
 
2115
        
 
2116
        /******************** Query Simplification ********************/       
 
2117
        
 
2118
        Member LiteralExpr::constraint(SimplificationContext& context) const {
 
2119
            return Member(_value);
 
2120
        }
 
2121
        
 
2122
        Member memberForPlace(size_t p, SimplificationContext& context) 
 
2123
        {
 
2124
            std::vector<int> row(context.net()->numberOfTransitions(), 0);
 
2125
            row.shrink_to_fit();
 
2126
            for (size_t t = 0; t < context.net()->numberOfTransitions(); t++) {
 
2127
                row[t] = context.net()->outArc(t, p) - context.net()->inArc(p, t);
 
2128
            }
 
2129
            return Member(std::move(row), context.marking()[p]);            
 
2130
        }
 
2131
        
 
2132
        Member UnfoldedIdentifierExpr::constraint(SimplificationContext& context) const {
 
2133
            return memberForPlace(_offsetInMarking, context);
 
2134
        }
 
2135
        
 
2136
        Member CommutativeExpr::commutativeCons(int constant, SimplificationContext& context, std::function<void(Member& a, Member b)> op) const
 
2137
        {
 
2138
            Member res;
 
2139
            bool first = true;
 
2140
            if(_constant != constant || (_exprs.size() == 0 && _ids.size() == 0))
 
2141
            {
 
2142
                first = false;
 
2143
                res = Member(_constant);
 
2144
            }
 
2145
            
 
2146
            for(auto& i : _ids)
 
2147
            {
 
2148
                if(first) res = memberForPlace(i.first, context);
 
2149
                else op(res, memberForPlace(i.first, context));
 
2150
                first = false;
 
2151
            }
 
2152
 
 
2153
            for(auto& e : _exprs)
 
2154
            {
 
2155
                if(first) res = e->constraint(context);
 
2156
                else op(res, e->constraint(context));
 
2157
                first = false;
 
2158
            }
 
2159
            return res;            
 
2160
        }
 
2161
        
 
2162
        Member PlusExpr::constraint(SimplificationContext& context) const {
 
2163
            return commutativeCons(0, context, [](auto& a , auto b){ a += b;});
 
2164
        }
 
2165
        
 
2166
        Member SubtractExpr::constraint(SimplificationContext& context) const {
 
2167
            Member res = _exprs[0]->constraint(context);
 
2168
            for(size_t i = 1; i < _exprs.size(); ++i) res -= _exprs[i]->constraint(context);
 
2169
            return res;
 
2170
        }
 
2171
        
 
2172
        Member MultiplyExpr::constraint(SimplificationContext& context) const {
 
2173
            return commutativeCons(1, context, [](auto& a , auto b){ a *= b;});
 
2174
        }
 
2175
        
 
2176
        Member MinusExpr::constraint(SimplificationContext& context) const {
 
2177
            Member neg(-1);
 
2178
            return _expr->constraint(context) *= neg;
 
2179
        }
 
2180
        
 
2181
        Retval simplifyEX(Retval& r, SimplificationContext& context) {
 
2182
            if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)) {
 
2183
                return Retval(std::make_shared<NotCondition>(
 
2184
                        std::make_shared<DeadlockCondition>()));
 
2185
            } else if(r.formula->isTriviallyFalse() || !r.lps->satisfiable(context)) {
 
2186
                return Retval(BooleanCondition::FALSE_CONSTANT);
 
2187
            } else {
 
2188
                return Retval(std::make_shared<EXCondition>(r.formula));
 
2189
            }
 
2190
        }
 
2191
        
 
2192
        Retval simplifyAX(Retval& r, SimplificationContext& context) {
 
2193
            if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)){
 
2194
                return Retval(BooleanCondition::TRUE_CONSTANT);
 
2195
            } else if(r.formula->isTriviallyFalse() || !r.lps->satisfiable(context)){
 
2196
                return Retval(std::make_shared<DeadlockCondition>());
 
2197
            } else{
 
2198
                return Retval(std::make_shared<AXCondition>(r.formula));
 
2199
            }
 
2200
        }
 
2201
        
 
2202
        Retval simplifyEF(Retval& r, SimplificationContext& context){
 
2203
            if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)){
 
2204
                return Retval(BooleanCondition::TRUE_CONSTANT);
 
2205
            } else if(r.formula->isTriviallyFalse() || !r.lps->satisfiable(context)){
 
2206
                return Retval(BooleanCondition::FALSE_CONSTANT);
 
2207
            } else {
 
2208
                return Retval(std::make_shared<EFCondition>(r.formula));
 
2209
            }
 
2210
        }
 
2211
        
 
2212
        Retval simplifyAF(Retval& r, SimplificationContext& context){
 
2213
            if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)){
 
2214
                return Retval(BooleanCondition::TRUE_CONSTANT);
 
2215
            } else if(r.formula->isTriviallyFalse() || !r.lps->satisfiable(context)){
 
2216
                return Retval(BooleanCondition::FALSE_CONSTANT);
 
2217
            } else {
 
2218
                return Retval(std::make_shared<AFCondition>(r.formula));
 
2219
            }
 
2220
        }
 
2221
        
 
2222
        Retval simplifyEG(Retval& r, SimplificationContext& context){
 
2223
            if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)){
 
2224
                return Retval(BooleanCondition::TRUE_CONSTANT);
 
2225
            } else if(r.formula->isTriviallyFalse() || !r.lps->satisfiable(context)){
 
2226
                return Retval(BooleanCondition::FALSE_CONSTANT);
 
2227
            } else {
 
2228
                return Retval(std::make_shared<EGCondition>(r.formula));
 
2229
            }
 
2230
        }
 
2231
        
 
2232
        Retval simplifyAG(Retval& r, SimplificationContext& context){
 
2233
            if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)){
 
2234
                return Retval(BooleanCondition::TRUE_CONSTANT);
 
2235
            } else if(r.formula->isTriviallyFalse() || !r.lps->satisfiable(context)){
 
2236
                return Retval(BooleanCondition::FALSE_CONSTANT);
 
2237
            } else {
 
2238
                return Retval(std::make_shared<AGCondition>(r.formula));
 
2239
            }
 
2240
        }
 
2241
        
 
2242
        Retval EXCondition::simplify(SimplificationContext& context) const {
 
2243
            Retval r = _cond->simplify(context);
 
2244
            return context.negated() ? simplifyAX(r, context) : simplifyEX(r, context);
 
2245
        }
 
2246
        
 
2247
        Retval AXCondition::simplify(SimplificationContext& context) const {
 
2248
            Retval r = _cond->simplify(context);
 
2249
            return context.negated() ? simplifyEX(r, context) : simplifyAX(r, context);
 
2250
        }  
 
2251
        
 
2252
        Retval EFCondition::simplify(SimplificationContext& context) const {
 
2253
            Retval r = _cond->simplify(context);
 
2254
            return context.negated() ? simplifyAG(r, context) : simplifyEF(r, context);  
 
2255
        }
 
2256
        
 
2257
        Retval AFCondition::simplify(SimplificationContext& context) const {
 
2258
            Retval r = _cond->simplify(context);
 
2259
            return context.negated() ? simplifyEG(r, context) : simplifyAF(r, context);  
 
2260
        }
 
2261
        
 
2262
        Retval EGCondition::simplify(SimplificationContext& context) const {
 
2263
            Retval r = _cond->simplify(context);
 
2264
            return context.negated() ? simplifyAF(r, context) : simplifyEG(r, context);  
 
2265
        }
 
2266
        
 
2267
        Retval AGCondition::simplify(SimplificationContext& context) const {
 
2268
            Retval r = _cond->simplify(context);
 
2269
            return context.negated() ? simplifyEF(r, context) : simplifyAG(r, context);  
 
2270
        }
 
2271
        
 
2272
        Retval EUCondition::simplify(SimplificationContext& context) const {
 
2273
            // cannot push negation any further
 
2274
            bool neg = context.negated();
 
2275
            context.setNegate(false);
 
2276
            Retval r2 = _cond2->simplify(context);
 
2277
            if(r2.formula->isTriviallyTrue() || !r2.neglps->satisfiable(context))
 
2278
            {
 
2279
                context.setNegate(neg);
 
2280
                return neg ? 
 
2281
                            Retval(BooleanCondition::FALSE_CONSTANT) :
 
2282
                            Retval(BooleanCondition::TRUE_CONSTANT);
 
2283
            }
 
2284
            else if(r2.formula->isTriviallyFalse() || !r2.lps->satisfiable(context))
 
2285
            {
 
2286
                context.setNegate(neg);
 
2287
                return neg ? 
 
2288
                            Retval(BooleanCondition::TRUE_CONSTANT) :
 
2289
                            Retval(BooleanCondition::FALSE_CONSTANT);                
 
2290
            }
 
2291
            Retval r1 = _cond1->simplify(context);
 
2292
            context.setNegate(neg);
 
2293
            
 
2294
            if(context.negated()){
 
2295
                if(r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(context)){
 
2296
                    return Retval(std::make_shared<NotCondition>(
 
2297
                            std::make_shared<EFCondition>(r2.formula)));
 
2298
                } else if(r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(context)){
 
2299
                    return Retval(std::make_shared<NotCondition>(r2.formula));
 
2300
                } else {
 
2301
                    return Retval(std::make_shared<NotCondition>(
 
2302
                            std::make_shared<EUCondition>(r1.formula, r2.formula)));
 
2303
                }
 
2304
            } else {
 
2305
                if(r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(context)){
 
2306
                    return Retval(std::make_shared<EFCondition>(r2.formula));
 
2307
                } else if(r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(context)){
 
2308
                    return r2;
 
2309
                } else {
 
2310
                    return Retval(std::make_shared<EUCondition>(r1.formula, r2.formula));
 
2311
                }
 
2312
            }
 
2313
        }
 
2314
        
 
2315
        Retval AUCondition::simplify(SimplificationContext& context) const {
 
2316
            // cannot push negation any further
 
2317
            bool neg = context.negated();
 
2318
            context.setNegate(false);
 
2319
            Retval r2 = _cond2->simplify(context);
 
2320
            if(r2.formula->isTriviallyTrue() || !r2.neglps->satisfiable(context))
 
2321
            {
 
2322
                context.setNegate(neg);
 
2323
                return neg ? 
 
2324
                            Retval(BooleanCondition::FALSE_CONSTANT) :
 
2325
                            Retval(BooleanCondition::TRUE_CONSTANT);
 
2326
            }
 
2327
            else if(r2.formula->isTriviallyFalse() || !r2.lps->satisfiable(context))
 
2328
            {
 
2329
                context.setNegate(neg);
 
2330
                return neg ? 
 
2331
                            Retval(BooleanCondition::TRUE_CONSTANT) :
 
2332
                            Retval(BooleanCondition::FALSE_CONSTANT);                
 
2333
            }
 
2334
            Retval r1 = _cond1->simplify(context);
 
2335
            context.setNegate(neg);
 
2336
            
 
2337
            if(context.negated()){
 
2338
                if(r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(context)){
 
2339
                    return Retval(std::make_shared<NotCondition>(
 
2340
                            std::make_shared<AFCondition>(r2.formula)));
 
2341
                } else if(r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(context)){
 
2342
                    return Retval(std::make_shared<NotCondition>(r2.formula));
 
2343
                } else {
 
2344
                    return Retval(std::make_shared<NotCondition>(
 
2345
                            std::make_shared<AUCondition>(r1.formula, r2.formula)));
 
2346
                }
 
2347
            } else {
 
2348
                if(r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(context)){
 
2349
                    return Retval(std::make_shared<AFCondition>(r2.formula));
 
2350
                } else if(r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(context)){
 
2351
                    return r2;
 
2352
                } else {
 
2353
                    return Retval(std::make_shared<AUCondition>(r1.formula, r2.formula));
 
2354
                }
 
2355
            }
 
2356
        }
 
2357
        
 
2358
        AbstractProgramCollection_ptr mergeLps(std::vector<AbstractProgramCollection_ptr>&& lps)
 
2359
        {
 
2360
            if(lps.size() == 0) return nullptr;
 
2361
            int j = 0;
 
2362
            int i = lps.size() - 1;
 
2363
            while(i > 0)
 
2364
            {
 
2365
                if(i <= j) j = 0;
 
2366
                else
 
2367
                {
 
2368
                    lps[j] = std::make_shared<MergeCollection>(lps[j], lps[i]);
 
2369
                    --i;
 
2370
                    ++j;
 
2371
                }
 
2372
            }
 
2373
            return lps[0];
 
2374
        }
 
2375
        
 
2376
        Retval LogicalCondition::simplifyAnd(SimplificationContext& context) const {
 
2377
 
 
2378
            std::vector<Condition_ptr> conditions;
 
2379
            std::vector<AbstractProgramCollection_ptr> lpsv;
 
2380
            std::vector<AbstractProgramCollection_ptr>  neglps;
 
2381
            for(auto& c : _conds)
 
2382
            {
 
2383
                auto r = c->simplify(context);
 
2384
                if(r.formula->isTriviallyFalse())
 
2385
                {
 
2386
                    return Retval(BooleanCondition::FALSE_CONSTANT);
 
2387
                }
 
2388
                else if(r.formula->isTriviallyTrue())
 
2389
                {
 
2390
                    continue;
 
2391
                }
 
2392
                
 
2393
                conditions.push_back(r.formula);
 
2394
                lpsv.emplace_back(r.lps);
 
2395
                neglps.emplace_back(r.neglps);
 
2396
            }
 
2397
            
 
2398
            if(conditions.size() == 0)
 
2399
            {
 
2400
                return Retval(BooleanCondition::TRUE_CONSTANT);
 
2401
            }
 
2402
 
 
2403
            auto lps = mergeLps(std::move(lpsv));
 
2404
 
 
2405
            try {
 
2406
                if(!context.timeout() && !lps->satisfiable(context))
 
2407
                {
 
2408
                    return Retval(BooleanCondition::FALSE_CONSTANT);
 
2409
                }           
 
2410
             }
 
2411
             catch(std::bad_alloc& e)
 
2412
             {
 
2413
                // we are out of memory, deal with it.
 
2414
                std::cout<<"Query reduction: memory exceeded during LPS merge."<<std::endl;
 
2415
             }
 
2416
            
 
2417
            // Lets try to see if the r1 AND r2 can ever be false at the same time
 
2418
            // If not, then we know that r1 || r2 must be true.
 
2419
            // we check this by checking if !r1 && !r2 is unsat
 
2420
            
 
2421
            return Retval(
 
2422
                    makeAnd(conditions), 
 
2423
                    std::move(lps),
 
2424
                    std::make_shared<UnionCollection>(std::move(neglps)));
 
2425
        }
 
2426
        
 
2427
        Retval LogicalCondition::simplifyOr(SimplificationContext& context) const {
 
2428
 
 
2429
            std::vector<Condition_ptr> conditions;
 
2430
            std::vector<AbstractProgramCollection_ptr> lps, neglpsv;
 
2431
            for(auto& c : _conds)
 
2432
            {
 
2433
                auto r = c->simplify(context);
 
2434
                assert(r.neglps);
 
2435
                assert(r.lps);
 
2436
 
 
2437
                if(r.formula->isTriviallyTrue())
 
2438
                {
 
2439
                    return Retval(BooleanCondition::TRUE_CONSTANT);
 
2440
                }
 
2441
                else if(r.formula->isTriviallyFalse())
 
2442
                {
 
2443
                    continue;
 
2444
                }
 
2445
                conditions.push_back(r.formula);
 
2446
                lps.push_back(r.lps);
 
2447
                neglpsv.emplace_back(r.neglps);
 
2448
            }
 
2449
            
 
2450
            AbstractProgramCollection_ptr  neglps = mergeLps(std::move(neglpsv));
 
2451
 
 
2452
            if(conditions.size() == 0)
 
2453
            {
 
2454
                return Retval(BooleanCondition::FALSE_CONSTANT);
 
2455
            }
 
2456
 
 
2457
            try {
 
2458
               if(!context.timeout() && !neglps->satisfiable(context))
 
2459
               {
 
2460
                   return Retval(BooleanCondition::TRUE_CONSTANT);
 
2461
               }           
 
2462
            }
 
2463
            catch(std::bad_alloc& e)
 
2464
            {
 
2465
               // we are out of memory, deal with it.
 
2466
               std::cout<<"Query reduction: memory exceeded during LPS merge."<<std::endl;
 
2467
            }
 
2468
 
 
2469
            // Lets try to see if the r1 AND r2 can ever be false at the same time
 
2470
            // If not, then we know that r1 || r2 must be true.
 
2471
            // we check this by checking if !r1 && !r2 is unsat
 
2472
          
 
2473
            return Retval(
 
2474
                    makeOr(conditions), 
 
2475
                    std::make_shared<UnionCollection>(std::move(lps)), 
 
2476
                    std::move(neglps));            
 
2477
        }
 
2478
        
 
2479
        Retval AndCondition::simplify(SimplificationContext& context) const {
 
2480
            if(context.timeout())
 
2481
            {
 
2482
                if(context.negated()) 
 
2483
                    return Retval(std::make_shared<NotCondition>(
 
2484
                            makeAnd(_conds)));
 
2485
                else                  
 
2486
                    return Retval(
 
2487
                            makeAnd(_conds));
 
2488
            }
 
2489
 
 
2490
            if(context.negated())
 
2491
                return simplifyOr(context);
 
2492
            else
 
2493
                return simplifyAnd(context);
 
2494
            
 
2495
        }
 
2496
        
 
2497
        Retval OrCondition::simplify(SimplificationContext& context) const {            
 
2498
            if(context.timeout())
 
2499
            {
 
2500
                if(context.negated()) 
 
2501
                    return Retval(std::make_shared<NotCondition>(
 
2502
                            makeOr(_conds)));
 
2503
                else                 
 
2504
                    return Retval(makeOr(_conds));
 
2505
            }
 
2506
            if(context.negated())
 
2507
                return simplifyAnd(context);
 
2508
            else
 
2509
                return simplifyOr(context);
 
2510
        }
 
2511
        
 
2512
        Retval CompareConjunction::simplify(SimplificationContext& context) const {
 
2513
            if(context.timeout())
 
2514
            {
 
2515
                return Retval(std::make_shared<CompareConjunction>(*this, context.negated()));
 
2516
            }
 
2517
            std::vector<AbstractProgramCollection_ptr>  neglps, lpsv;
 
2518
            auto neg = context.negated() != _negated;
 
2519
            std::vector<cons_t> nconstraints;
 
2520
            for(auto& c : _constraints) 
 
2521
            {
 
2522
                nconstraints.push_back(c);
 
2523
                if(c._lower != 0 /*&& !context.timeout()*/ )
 
2524
                {
 
2525
                    auto m2 = memberForPlace(c._place, context);
 
2526
                    Member m1(c._lower);
 
2527
                    // test for trivial comparison
 
2528
                    Trivial eval = m1 <= m2;
 
2529
                    if(eval != Trivial::Indeterminate) {
 
2530
                        if(eval == Trivial::False)
 
2531
                            return Retval(BooleanCondition::getShared(neg));
 
2532
                        else
 
2533
                            nconstraints.back()._lower = 0;
 
2534
                    } else { // if no trivial case
 
2535
                        int constant = m2.constant() - m1.constant();
 
2536
                        m1 -= m2;
 
2537
                        m2 = m1;
 
2538
                        auto lp = std::make_shared<SingleProgram>(context.cache(), std::move(m1), constant, Simplification::OP_LE);
 
2539
                        auto nlp = std::make_shared<SingleProgram>(context.cache(), std::move(m2), constant, Simplification::OP_GT);
 
2540
                        lpsv.push_back(lp);
 
2541
                        neglps.push_back(nlp);
 
2542
                   }
 
2543
                }
 
2544
         
 
2545
                if(c._upper != std::numeric_limits<uint32_t>::max() /*&& !context.timeout()*/)
 
2546
                {
 
2547
                    auto m1 = memberForPlace(c._place, context);
 
2548
                    Member m2(c._upper);
 
2549
                    // test for trivial comparison
 
2550
                    Trivial eval = m1 <= m2;
 
2551
                    if(eval != Trivial::Indeterminate) {
 
2552
                        if(eval == Trivial::False)
 
2553
                            return Retval(BooleanCondition::getShared(neg));
 
2554
                        else
 
2555
                            nconstraints.back()._upper = std::numeric_limits<uint32_t>::max();
 
2556
                    } else { // if no trivial case
 
2557
                        int constant = m2.constant() - m1.constant();
 
2558
                        m1 -= m2;
 
2559
                        m2 = m1;
 
2560
                        auto lp = std::make_shared<SingleProgram>(context.cache(), std::move(m1), constant, Simplification::OP_LE);
 
2561
                        auto nlp = std::make_shared<SingleProgram>(context.cache(), std::move(m2), constant, Simplification::OP_GT);
 
2562
                        lpsv.push_back(lp);
 
2563
                        neglps.push_back(nlp);
 
2564
                   }
 
2565
                }
 
2566
                
 
2567
                assert(nconstraints.size() > 0);
 
2568
                if(nconstraints.back()._lower == 0 && nconstraints.back()._upper == std::numeric_limits<uint32_t>::max())
 
2569
                    nconstraints.pop_back();
 
2570
 
 
2571
                assert(nconstraints.size() <= neglps.size()*2);
 
2572
            }
 
2573
            
 
2574
            auto lps = mergeLps(std::move(lpsv));
 
2575
            
 
2576
            if(lps == nullptr && !context.timeout()) 
 
2577
            {
 
2578
                return Retval(BooleanCondition::getShared(!neg));
 
2579
            }
 
2580
            
 
2581
            try {
 
2582
                if(!context.timeout() && lps &&  !lps->satisfiable(context))
 
2583
                {
 
2584
                    return Retval(BooleanCondition::getShared(neg));
 
2585
                }           
 
2586
             }
 
2587
             catch(std::bad_alloc& e)
 
2588
             {
 
2589
                // we are out of memory, deal with it.
 
2590
                std::cout<<"Query reduction: memory exceeded during LPS merge."<<std::endl;
 
2591
             }
 
2592
            // Lets try to see if the r1 AND r2 can ever be false at the same time
 
2593
            // If not, then we know that r1 || r2 must be true.
 
2594
            // we check this by checking if !r1 && !r2 is unsat
 
2595
            try {
 
2596
                // remove trivial rules from neglp
 
2597
                int ncnt = neglps.size() - 1;
 
2598
                for(int i = nconstraints.size() - 1; i >= 0; --i) 
 
2599
                {
 
2600
                    if(context.timeout()) break;
 
2601
                    assert(ncnt >= 0);
 
2602
                    size_t cnt = 0;
 
2603
                    auto& c = nconstraints[i];
 
2604
                    if(c._lower != 0) ++cnt;
 
2605
                    if(c._upper != std::numeric_limits<uint32_t>::max()) ++cnt;
 
2606
                    for(size_t j = 0; j < cnt ; ++j)
 
2607
                    {
 
2608
                        assert(ncnt >= 0);
 
2609
                        if(!neglps[ncnt]->satisfiable(context))
 
2610
                        {
 
2611
                            if(j == 1 || c._upper == std::numeric_limits<uint32_t>::max())
 
2612
                                c._lower = 0;
 
2613
                            else if(j == 0)
 
2614
                                c._upper = std::numeric_limits<uint32_t>::max();
 
2615
                            neglps.erase(neglps.begin() + ncnt);
 
2616
                        }
 
2617
                        if(c._upper == std::numeric_limits<uint32_t>::max() && c._lower == 0) 
 
2618
                            nconstraints.erase(nconstraints.begin() + i);
 
2619
                        --ncnt;
 
2620
                    }
 
2621
                }
 
2622
            }
 
2623
            catch(std::bad_alloc& e)
 
2624
            {
 
2625
               // we are out of memory, deal with it.
 
2626
               std::cout<<"Query reduction: memory exceeded during LPS merge."<<std::endl;
 
2627
            }            
 
2628
            if(nconstraints.size() == 0)
 
2629
            {
 
2630
                return Retval(BooleanCondition::getShared(!neg));                
 
2631
            }
 
2632
 
 
2633
            
 
2634
            Condition_ptr rc = [&]() -> Condition_ptr {
 
2635
                if(nconstraints.size() == 1)
 
2636
                {
 
2637
                    auto& c = nconstraints[0];
 
2638
                    auto id = std::make_shared<UnfoldedIdentifierExpr>(c._name, c._place);
 
2639
                    auto ll = std::make_shared<LiteralExpr>(c._lower);
 
2640
                    auto lu = std::make_shared<LiteralExpr>(c._upper);
 
2641
                    if(c._lower == c._upper)
 
2642
                    {
 
2643
                        if(c._lower != 0)
 
2644
                            if(neg) return std::make_shared<NotEqualCondition>(id, lu);
 
2645
                            else    return std::make_shared<EqualCondition>(id, lu);
 
2646
                        else
 
2647
                            if(neg) return std::make_shared<GreaterThanCondition>(id, lu);
 
2648
                            else    return std::make_shared<LessThanOrEqualCondition>(id, lu);
 
2649
                    }
 
2650
                    else
 
2651
                    {
 
2652
                        if(c._lower != 0 && c._upper != std::numeric_limits<uint32_t>::max())
 
2653
                        {
 
2654
                            if(neg) return makeOr(std::make_shared<LessThanCondition>(id, ll),std::make_shared<GreaterThanCondition>(id, lu));
 
2655
                            else    return makeAnd(std::make_shared<GreaterThanOrEqualCondition>(id, ll),std::make_shared<LessThanOrEqualCondition>(id, lu));
 
2656
                        }
 
2657
                        else if(c._lower != 0)
 
2658
                        {
 
2659
                            if(neg) return std::make_shared<LessThanCondition>(id, ll);
 
2660
                            else    return std::make_shared<GreaterThanOrEqualCondition>(id, ll);                       
 
2661
                        }
 
2662
                        else
 
2663
                        {
 
2664
                            if(neg) return std::make_shared<GreaterThanCondition>(id, lu);
 
2665
                            else    return std::make_shared<LessThanOrEqualCondition>(id, lu);                        
 
2666
                        }
 
2667
                    }
 
2668
                }
 
2669
                else
 
2670
                {
 
2671
                    return std::make_shared<CompareConjunction>(std::move(nconstraints), context.negated() != _negated);
 
2672
                }
 
2673
            }();
 
2674
            
 
2675
 
 
2676
            if(!neg)
 
2677
            {
 
2678
                return Retval(
 
2679
                    rc, 
 
2680
                    std::move(lps),
 
2681
                    std::make_shared<UnionCollection>(std::move(neglps)));
 
2682
            }
 
2683
            else
 
2684
            {
 
2685
                return Retval(
 
2686
                    rc, 
 
2687
                    std::make_shared<UnionCollection>(std::move(neglps)),
 
2688
                    std::move(lps));                
 
2689
            }
 
2690
        }
 
2691
 
 
2692
        Retval EqualCondition::simplify(SimplificationContext& context) const {
 
2693
            
 
2694
            Member m1 = _expr1->constraint(context);
 
2695
            Member m2 = _expr2->constraint(context);
 
2696
            std::shared_ptr<AbstractProgramCollection> lps, neglps;
 
2697
            if (!context.timeout() && m1.canAnalyze() && m2.canAnalyze()) {
 
2698
                if ((m1.isZero() && m2.isZero()) || m1.substrationIsZero(m2)) {
 
2699
                    return Retval(BooleanCondition::getShared(
 
2700
                        context.negated() ? (m1.constant() != m2.constant()) : (m1.constant() == m2.constant())));
 
2701
                } else {
 
2702
                    int constant = m2.constant() - m1.constant();
 
2703
                    m1 -= m2;
 
2704
                    m2 = m1;
 
2705
                    neglps = 
 
2706
                            std::make_shared<UnionCollection>(
 
2707
                            std::make_shared<SingleProgram>(context.cache(), std::move(m1), constant, Simplification::OP_GT),
 
2708
                            std::make_shared<SingleProgram>(context.cache(), std::move(m2), constant, Simplification::OP_LT));
 
2709
                    Member m3 = m2;
 
2710
                    lps = std::make_shared<SingleProgram>(context.cache(), std::move(m3), constant, Simplification::OP_EQ);
 
2711
                    
 
2712
                    if(context.negated()) lps.swap(neglps);
 
2713
                }
 
2714
            } else {
 
2715
                lps = std::make_shared<SingleProgram>();
 
2716
                neglps = std::make_shared<SingleProgram>();
 
2717
            }
 
2718
            
 
2719
            if (!context.timeout() && !lps->satisfiable(context)) {
 
2720
                return Retval(BooleanCondition::FALSE_CONSTANT);
 
2721
            } 
 
2722
            else if(!context.timeout() && !neglps->satisfiable(context))
 
2723
            {
 
2724
                return Retval(BooleanCondition::TRUE_CONSTANT);            
 
2725
            } 
 
2726
            else {
 
2727
                if (context.negated()) {
 
2728
                    return Retval(std::make_shared<NotEqualCondition>(_expr1, _expr2), std::move(lps), std::move(neglps));
 
2729
                } else {
 
2730
                    return Retval(std::make_shared<EqualCondition>(_expr1, _expr2), std::move(lps), std::move(neglps));
 
2731
                }
 
2732
            }
 
2733
        }
 
2734
        
 
2735
        Retval NotEqualCondition::simplify(SimplificationContext& context) const {
 
2736
            Member m1 = _expr1->constraint(context);
 
2737
            Member m2 = _expr2->constraint(context);
 
2738
            std::shared_ptr<AbstractProgramCollection> lps, neglps;
 
2739
            if (!context.timeout() && m1.canAnalyze() && m2.canAnalyze()) {
 
2740
                if ((m1.isZero() && m2.isZero()) || m1.substrationIsZero(m2)) {
 
2741
                    return Retval(std::make_shared<BooleanCondition>(
 
2742
                        context.negated() ? (m1.constant() == m2.constant()) : (m1.constant() != m2.constant())));
 
2743
                } else{ 
 
2744
                    int constant = m2.constant() - m1.constant();
 
2745
                    m1 -= m2;
 
2746
                    m2 = m1;
 
2747
                    lps = 
 
2748
                            std::make_shared<UnionCollection>(
 
2749
                            std::make_shared<SingleProgram>(context.cache(), std::move(m1), constant, Simplification::OP_GT),
 
2750
                            std::make_shared<SingleProgram>(context.cache(), std::move(m2), constant, Simplification::OP_LT));
 
2751
                    Member m3 = m2;
 
2752
                    neglps = std::make_shared<SingleProgram>(context.cache(), std::move(m3), constant, Simplification::OP_EQ); 
 
2753
                    
 
2754
                    if(context.negated()) lps.swap(neglps);
 
2755
                }
 
2756
            } else {
 
2757
                lps = std::make_shared<SingleProgram>();
 
2758
                neglps = std::make_shared<SingleProgram>();
 
2759
            }
 
2760
            if (!context.timeout() && !lps->satisfiable(context)) {
 
2761
                return Retval(BooleanCondition::FALSE_CONSTANT);
 
2762
            } 
 
2763
            else if(!context.timeout() && !neglps->satisfiable(context))
 
2764
            {
 
2765
                return Retval(BooleanCondition::TRUE_CONSTANT);            
 
2766
            }
 
2767
            else {
 
2768
                if (context.negated()) {
 
2769
                    return Retval(std::make_shared<EqualCondition>(_expr1, _expr2), std::move(lps), std::move(neglps));
 
2770
                } else {
 
2771
                    return Retval(std::make_shared<NotEqualCondition>(_expr1, _expr2), std::move(lps), std::move(neglps));
 
2772
                }                         
 
2773
            }
 
2774
        }
 
2775
            
 
2776
        Retval LessThanCondition::simplify(SimplificationContext& context) const {
 
2777
            Member m1 = _expr1->constraint(context);
 
2778
            Member m2 = _expr2->constraint(context);
 
2779
            AbstractProgramCollection_ptr lps, neglps;
 
2780
            if (!context.timeout() && m1.canAnalyze() && m2.canAnalyze()) {
 
2781
                // test for trivial comparison
 
2782
                Trivial eval = context.negated() ? m1 >= m2 : m1 < m2;
 
2783
                if(eval != Trivial::Indeterminate) {
 
2784
                    return Retval(BooleanCondition::getShared(eval == Trivial::True));
 
2785
                } else { // if no trivial case
 
2786
                    int constant = m2.constant() - m1.constant();
 
2787
                    m1 -= m2;
 
2788
                    m2 = m1;
 
2789
                    lps = std::make_shared<SingleProgram>(context.cache(), std::move(m1), constant, (context.negated() ? Simplification::OP_GE : Simplification::OP_LT));
 
2790
                    neglps = std::make_shared<SingleProgram>(context.cache(), std::move(m2), constant, (!context.negated() ? Simplification::OP_GE : Simplification::OP_LT));
 
2791
                }
 
2792
            } else {
 
2793
                lps = std::make_shared<SingleProgram>();
 
2794
                neglps = std::make_shared<SingleProgram>();
 
2795
            }
 
2796
            
 
2797
            if (!context.timeout() && !lps->satisfiable(context)) {
 
2798
                return Retval(BooleanCondition::FALSE_CONSTANT);
 
2799
            }
 
2800
            else if(!context.timeout() && !neglps->satisfiable(context))
 
2801
            {
 
2802
                return Retval(BooleanCondition::TRUE_CONSTANT);                
 
2803
            }
 
2804
            else {
 
2805
                if (context.negated()) {
 
2806
                    return Retval(std::make_shared<GreaterThanOrEqualCondition>(_expr1, _expr2), std::move(lps), std::move(neglps));
 
2807
                } else {
 
2808
                    return Retval(std::make_shared<LessThanCondition>(_expr1, _expr2), std::move(lps), std::move(neglps));
 
2809
                }                         
 
2810
            }
 
2811
        }        
 
2812
        
 
2813
        Retval LessThanOrEqualCondition::simplify(SimplificationContext& context) const {
 
2814
            Member m1 = _expr1->constraint(context);
 
2815
            Member m2 = _expr2->constraint(context);
 
2816
            
 
2817
            AbstractProgramCollection_ptr lps, neglps;
 
2818
            if (!context.timeout() && m1.canAnalyze() && m2.canAnalyze()) {
 
2819
                // test for trivial comparison
 
2820
                Trivial eval = context.negated() ? m1 > m2 : m1 <= m2;
 
2821
                if(eval != Trivial::Indeterminate) {
 
2822
                    return Retval(BooleanCondition::getShared(eval == Trivial::True));
 
2823
                } else { // if no trivial case
 
2824
                    int constant = m2.constant() - m1.constant();
 
2825
                    m1 -= m2;
 
2826
                    m2 = m1;
 
2827
                    lps = std::make_shared<SingleProgram>(context.cache(), std::move(m1), constant, (context.negated() ? Simplification::OP_GT : Simplification::OP_LE));
 
2828
                    neglps = std::make_shared<SingleProgram>(context.cache(), std::move(m2), constant, (context.negated() ? Simplification::OP_LE : Simplification::OP_GT));
 
2829
                }
 
2830
            } else {
 
2831
                lps = std::make_shared<SingleProgram>();
 
2832
                neglps = std::make_shared<SingleProgram>();
 
2833
            }
 
2834
            
 
2835
            assert(lps);
 
2836
            assert(neglps);
 
2837
 
 
2838
            if(!context.timeout() && !neglps->satisfiable(context)){
 
2839
                return Retval(BooleanCondition::TRUE_CONSTANT);
 
2840
            } else if (!context.timeout() && !lps->satisfiable(context)) {
 
2841
                return Retval(BooleanCondition::FALSE_CONSTANT);
 
2842
            } else {
 
2843
                if (context.negated()) {
 
2844
                    return Retval(std::make_shared<GreaterThanCondition>(_expr1, _expr2), std::move(lps), std::move(neglps));
 
2845
                } else {
 
2846
                    return Retval(std::make_shared<LessThanOrEqualCondition>(_expr1, _expr2), 
 
2847
                            std::move(lps), std::move(neglps));
 
2848
                }                         
 
2849
            }
 
2850
        }
 
2851
        
 
2852
        Retval GreaterThanCondition::simplify(SimplificationContext& context) const {
 
2853
            Member m1 = _expr1->constraint(context);
 
2854
            Member m2 = _expr2->constraint(context);
 
2855
            
 
2856
            AbstractProgramCollection_ptr lps, neglps;
 
2857
            if (!context.timeout() && m1.canAnalyze() && m2.canAnalyze()) {
 
2858
                // test for trivial comparison
 
2859
                Trivial eval = context.negated() ? m1 <= m2 : m1 > m2;
 
2860
                if(eval != Trivial::Indeterminate) {
 
2861
                    return Retval(BooleanCondition::getShared(eval == Trivial::True));
 
2862
                } else { // if no trivial case
 
2863
                    int constant = m2.constant() - m1.constant();
 
2864
                    m1 -= m2;
 
2865
                    m2 = m1;
 
2866
                    lps = std::make_shared<SingleProgram>(context.cache(), std::move(m1), constant, (context.negated() ? Simplification::OP_LE : Simplification::OP_GT));
 
2867
                    neglps = std::make_shared<SingleProgram>(context.cache(), std::move(m2), constant, (context.negated() ? Simplification::OP_GT : Simplification::OP_LE));
 
2868
                }
 
2869
            } else {
 
2870
                lps = std::make_shared<SingleProgram>();
 
2871
                neglps = std::make_shared<SingleProgram>();
 
2872
            }
 
2873
            
 
2874
            if(!context.timeout() && !neglps->satisfiable(context)) {
 
2875
                return Retval(BooleanCondition::TRUE_CONSTANT);
 
2876
            }else if(!context.timeout() && !lps->satisfiable(context)) {
 
2877
                return Retval(BooleanCondition::FALSE_CONSTANT);
 
2878
            } else {
 
2879
                if (context.negated()) {
 
2880
                    return Retval(std::make_shared<LessThanOrEqualCondition>(_expr1, _expr2), std::move(lps), std::move(neglps));
 
2881
                } else {
 
2882
                    return Retval(std::make_shared<GreaterThanCondition>(_expr1, _expr2), std::move(lps), std::move(neglps));
 
2883
                }                         
 
2884
            }
 
2885
        }
 
2886
        
 
2887
        Retval GreaterThanOrEqualCondition::simplify(SimplificationContext& context) const {  
 
2888
            Member m1 = _expr1->constraint(context);
 
2889
            Member m2 = _expr2->constraint(context);
 
2890
            
 
2891
            AbstractProgramCollection_ptr lps, neglps;
 
2892
            if (!context.timeout() && m1.canAnalyze() && m2.canAnalyze()) {
 
2893
                // test for trivial comparison
 
2894
                Trivial eval = context.negated() ? m1 < m2 : m1 >= m2;
 
2895
                if(eval != Trivial::Indeterminate) {
 
2896
                    return Retval(BooleanCondition::getShared(eval == Trivial::True));
 
2897
                } else { // if no trivial case
 
2898
                    int constant = m2.constant() - m1.constant();
 
2899
                    m1 -= m2;
 
2900
                    m2 = m1;
 
2901
                    lps = std::make_shared<SingleProgram>(context.cache(), std::move(m1), constant, (context.negated() ? Simplification::OP_LT : Simplification::OP_GE));
 
2902
                    neglps = std::make_shared<SingleProgram>(context.cache(), std::move(m2), constant, (!context.negated() ? Simplification::OP_LT : Simplification::OP_GE));
 
2903
                }
 
2904
            } else {
 
2905
                lps = std::make_shared<SingleProgram>();
 
2906
                neglps = std::make_shared<SingleProgram>();
 
2907
            }
 
2908
            if (!context.timeout() && !lps->satisfiable(context)) 
 
2909
            {
 
2910
                return Retval(BooleanCondition::FALSE_CONSTANT);
 
2911
            } 
 
2912
            else if(!context.timeout() && !neglps->satisfiable(context))
 
2913
            {
 
2914
                return Retval(BooleanCondition::TRUE_CONSTANT);
 
2915
            }
 
2916
            else {
 
2917
                if (context.negated()) {
 
2918
                    return Retval(std::make_shared<LessThanCondition>(_expr1, _expr2), std::move(lps), std::move(neglps));
 
2919
                } else {
 
2920
                    return Retval(std::make_shared<GreaterThanOrEqualCondition>(_expr1, _expr2), std::move(lps), std::move(neglps));
 
2921
                }                         
 
2922
            }
 
2923
        }
 
2924
        
 
2925
        Retval NotCondition::simplify(SimplificationContext& context) const {
 
2926
            context.negate();
 
2927
            Retval r = _cond->simplify(context);
 
2928
            context.negate();
 
2929
            return r;
 
2930
        }
 
2931
        
 
2932
        Retval BooleanCondition::simplify(SimplificationContext& context) const {
 
2933
            if (context.negated()) {
 
2934
                return Retval(getShared(!_value));
 
2935
            } else {
 
2936
                return Retval(getShared(_value));
 
2937
            }
 
2938
        }
 
2939
        
 
2940
        Retval DeadlockCondition::simplify(SimplificationContext& context) const {
 
2941
            if (context.negated()) {
 
2942
                return Retval(std::make_shared<NotCondition>(DeadlockCondition::DEADLOCK));
 
2943
            } else {
 
2944
                return Retval(DeadlockCondition::DEADLOCK);
 
2945
            }
 
2946
        }
 
2947
        
 
2948
        Retval UnfoldedUpperBoundsCondition::simplify(SimplificationContext& context) const 
 
2949
        {
 
2950
            std::vector<place_t> next;
 
2951
            std::vector<uint32_t> places;
 
2952
            for(auto& p : _places)
 
2953
                places.push_back(p._place);
 
2954
            const auto nplaces = _places.size();
 
2955
            const auto bounds = LinearProgram::bounds(context, context.getLpTimeout(), places);
 
2956
            double offset = _offset;
 
2957
            for(size_t i = 0; i < nplaces; ++i)
 
2958
            {
 
2959
                if(bounds[i].first != 0 && !bounds[i].second)
 
2960
                    next.emplace_back(_places[i], bounds[i].first);
 
2961
                if(bounds[i].second)
 
2962
                    offset += bounds[i].first;
 
2963
            }
 
2964
            if(bounds[nplaces].second)
 
2965
            {
 
2966
                next.clear();
 
2967
                return Retval(std::make_shared<UnfoldedUpperBoundsCondition>(next, 0, bounds[nplaces].first + _offset));
 
2968
            }
 
2969
            return Retval(std::make_shared<UnfoldedUpperBoundsCondition>(next, bounds[nplaces].first-offset, offset));
 
2970
        }
 
2971
        
 
2972
        /******************** Check if query is a reachability query ********************/
 
2973
        
 
2974
        bool EXCondition::isReachability(uint32_t depth) const {
 
2975
            return false;
 
2976
        }
 
2977
        
 
2978
        bool EGCondition::isReachability(uint32_t depth) const {
 
2979
            return false;
 
2980
        }
 
2981
        
 
2982
        bool EFCondition::isReachability(uint32_t depth) const {
 
2983
            return depth > 0 ? false : _cond->isReachability(depth + 1);
 
2984
        }
 
2985
        
 
2986
        bool AXCondition::isReachability(uint32_t depth) const {
 
2987
            return false;
 
2988
        }
 
2989
        
 
2990
        bool AGCondition::isReachability(uint32_t depth) const {
 
2991
            return depth > 0 ? false : _cond->isReachability(depth + 1);
 
2992
        }
 
2993
        
 
2994
        bool AFCondition::isReachability(uint32_t depth) const {
 
2995
            return false;
 
2996
        }
 
2997
        
 
2998
        bool UntilCondition::isReachability(uint32_t depth) const {
 
2999
            return false;
 
3000
        }
 
3001
        
 
3002
        bool LogicalCondition::isReachability(uint32_t depth) const {
 
3003
            if(depth == 0) return false;
 
3004
            bool reachability = true;
 
3005
            for(auto& c : _conds)
 
3006
            {
 
3007
                reachability = reachability && c->isReachability(depth + 1);
 
3008
                if(!reachability) break;
 
3009
            }
 
3010
            return reachability;
 
3011
        }
 
3012
        
 
3013
        bool CompareCondition::isReachability(uint32_t depth) const {
 
3014
            return depth > 0;
 
3015
        }
 
3016
        
 
3017
        bool NotCondition::isReachability(uint32_t depth) const {
 
3018
            return _cond->isReachability(depth);
 
3019
        }
 
3020
        
 
3021
        bool BooleanCondition::isReachability(uint32_t depth) const {
 
3022
            return depth > 0;
 
3023
        }
 
3024
        
 
3025
        bool DeadlockCondition::isReachability(uint32_t depth) const {
 
3026
            return depth > 0;
 
3027
        }
 
3028
        
 
3029
        bool UnfoldedUpperBoundsCondition::isReachability(uint32_t depth) const {
 
3030
            return depth > 0;
 
3031
        }
 
3032
                
 
3033
        /******************** Prepare Reachability Queries ********************/
 
3034
        
 
3035
        Condition_ptr EXCondition::prepareForReachability(bool negated) const {
 
3036
            return NULL;
 
3037
        }
 
3038
        
 
3039
        Condition_ptr EGCondition::prepareForReachability(bool negated) const {
 
3040
            return NULL;
 
3041
        }
 
3042
        
 
3043
        Condition_ptr EFCondition::prepareForReachability(bool negated) const {
 
3044
            _cond->setInvariant(negated);
 
3045
            return _cond;
 
3046
        }
 
3047
        
 
3048
        Condition_ptr AXCondition::prepareForReachability(bool negated) const {
 
3049
            return NULL;
 
3050
        }
 
3051
        
 
3052
        Condition_ptr AGCondition::prepareForReachability(bool negated) const {
 
3053
            Condition_ptr cond = std::make_shared<NotCondition>(_cond);
 
3054
            cond->setInvariant(!negated);
 
3055
            return cond;
 
3056
        }
 
3057
        
 
3058
        Condition_ptr AFCondition::prepareForReachability(bool negated) const {
 
3059
            return NULL;
 
3060
        }
 
3061
        
 
3062
        Condition_ptr UntilCondition::prepareForReachability(bool negated) const {
 
3063
            return NULL;
 
3064
        }
 
3065
        
 
3066
        Condition_ptr LogicalCondition::prepareForReachability(bool negated) const {
 
3067
            return NULL;
 
3068
        }
 
3069
 
 
3070
        Condition_ptr CompareConjunction::prepareForReachability(bool negated) const {
 
3071
            return NULL;
 
3072
        }
 
3073
        
 
3074
        Condition_ptr CompareCondition::prepareForReachability(bool negated) const {
 
3075
            return NULL;
 
3076
        }
 
3077
        
 
3078
        Condition_ptr NotCondition::prepareForReachability(bool negated) const {
 
3079
            return _cond->prepareForReachability(!negated);
 
3080
        }
 
3081
        
 
3082
        Condition_ptr BooleanCondition::prepareForReachability(bool negated) const {
 
3083
            return NULL;
 
3084
        }
 
3085
        
 
3086
        Condition_ptr DeadlockCondition::prepareForReachability(bool negated) const {
 
3087
            return NULL;
 
3088
        }
 
3089
 
 
3090
        Condition_ptr UnfoldedUpperBoundsCondition::prepareForReachability(bool negated) const {
 
3091
            return NULL;
 
3092
        }
 
3093
        
 
3094
/******************** Prepare CTL Queries ********************/
 
3095
        
 
3096
        Condition_ptr EGCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
 
3097
            ++stats[0];
 
3098
            return AFCondition(std::make_shared<NotCondition>(_cond)).pushNegation(stats, context, nested, !negated, initrw);
 
3099
        }
 
3100
 
 
3101
        Condition_ptr AGCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
 
3102
            ++stats[1];
 
3103
            return EFCondition(std::make_shared<NotCondition>(_cond)).pushNegation(stats, context, nested, !negated, initrw);
 
3104
        }
 
3105
        
 
3106
        Condition_ptr EXCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
 
3107
            return initialMarkingRW([&]() -> Condition_ptr {
 
3108
            auto a = _cond->pushNegation(stats, context, true, negated, initrw);
 
3109
            if(negated)
 
3110
            {
 
3111
                ++stats[2];
 
3112
                return AXCondition(a).pushNegation(stats, context, nested, false, initrw);
 
3113
            }
 
3114
            else
 
3115
            {
 
3116
                if(a == BooleanCondition::FALSE_CONSTANT) 
 
3117
                { ++stats[3]; return a;}
 
3118
                if(a == BooleanCondition::TRUE_CONSTANT)  
 
3119
                { ++stats[4]; return std::make_shared<NotCondition>(DeadlockCondition::DEADLOCK); }
 
3120
                a = std::make_shared<EXCondition>(a);
 
3121
            }
 
3122
            return a;
 
3123
            }, stats, context, nested, negated, initrw);
 
3124
        }
 
3125
 
 
3126
        Condition_ptr AXCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
 
3127
            return initialMarkingRW([&]() -> Condition_ptr {
 
3128
            auto a = _cond->pushNegation(stats, context, true, negated, initrw);
 
3129
            if(negated)
 
3130
            {
 
3131
                ++stats[5];
 
3132
                return EXCondition(a).pushNegation(stats, context, nested, false, initrw);
 
3133
            }
 
3134
            else
 
3135
            {
 
3136
                if(a == BooleanCondition::TRUE_CONSTANT) 
 
3137
                { ++stats[6]; return a;}
 
3138
                if(a == BooleanCondition::FALSE_CONSTANT)  
 
3139
                { ++stats[7]; return DeadlockCondition::DEADLOCK; }
 
3140
                a = std::make_shared<AXCondition>(a);
 
3141
            }
 
3142
            return a;
 
3143
            }, stats, context, nested, negated, initrw);
 
3144
        }
 
3145
 
 
3146
        
 
3147
        Condition_ptr EFCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
 
3148
            return initialMarkingRW([&]() -> Condition_ptr {
 
3149
            auto a = _cond->pushNegation(stats, context, true, false, initrw);
 
3150
 
 
3151
            if(auto cond = dynamic_cast<NotCondition*>(a.get()))
 
3152
            {
 
3153
                if((*cond)[0] == DeadlockCondition::DEADLOCK)
 
3154
                {
 
3155
                    ++stats[8];
 
3156
                    return a->pushNegation(stats, context, nested, negated, initrw);
 
3157
                }                
 
3158
            }
 
3159
 
 
3160
            if(!a->isTemporal())
 
3161
            {
 
3162
                auto res = std::make_shared<EFCondition>(a);
 
3163
                if(negated) return std::make_shared<NotCondition>(res);
 
3164
                return res;
 
3165
            }
 
3166
            
 
3167
            if( dynamic_cast<EFCondition*>(a.get()))
 
3168
            {
 
3169
                ++stats[9];
 
3170
                if(negated) a = std::make_shared<NotCondition>(a);
 
3171
                return a;
 
3172
            }
 
3173
            else if(auto cond = dynamic_cast<AFCondition*>(a.get()))
 
3174
            {
 
3175
                ++stats[10];
 
3176
                a = EFCondition((*cond)[0]).pushNegation(stats, context, nested, negated, initrw);
 
3177
                return a;
 
3178
            }
 
3179
            else if(auto cond = dynamic_cast<EUCondition*>(a.get()))
 
3180
            {
 
3181
                ++stats[11];
 
3182
                a = EFCondition((*cond)[1]).pushNegation(stats, context, nested, negated, initrw);
 
3183
                return a;
 
3184
            }
 
3185
            else if(auto cond = dynamic_cast<AUCondition*>(a.get()))
 
3186
            {
 
3187
                ++stats[12];
 
3188
                a = EFCondition((*cond)[1]).pushNegation(stats, context, nested, negated, initrw);
 
3189
                return a;
 
3190
            }
 
3191
            else if(auto cond = dynamic_cast<OrCondition*>(a.get()))
 
3192
            {
 
3193
                if(!cond->isTemporal())
 
3194
                {
 
3195
                    Condition_ptr b = std::make_shared<EFCondition>(a);
 
3196
                    if(negated) b = std::make_shared<NotCondition>(b);
 
3197
                    return b;
 
3198
                }
 
3199
                ++stats[13];
 
3200
                std::vector<Condition_ptr> pef, atomic;
 
3201
                for(auto& i : *cond) 
 
3202
                {
 
3203
                    pef.push_back(std::make_shared<EFCondition>(i));
 
3204
                }
 
3205
                a = makeOr(pef)->pushNegation(stats, context, nested, negated, initrw);
 
3206
                return a;
 
3207
            }
 
3208
            else
 
3209
            {        
 
3210
                Condition_ptr b = std::make_shared<EFCondition>(a);
 
3211
                if(negated) b = std::make_shared<NotCondition>(b);
 
3212
                return b;
 
3213
            }
 
3214
            }, stats, context, nested, negated, initrw);
 
3215
        }
 
3216
 
 
3217
 
 
3218
        Condition_ptr AFCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
 
3219
            return initialMarkingRW([&]() -> Condition_ptr {
 
3220
            auto a = _cond->pushNegation(stats, context, true, false, initrw);
 
3221
            if(auto cond = dynamic_cast<NotCondition*>(a.get()))
 
3222
            {
 
3223
                if((*cond)[0] == DeadlockCondition::DEADLOCK)
 
3224
                {
 
3225
                    ++stats[14];
 
3226
                    return a->pushNegation(stats, context, nested, negated, initrw);
 
3227
                }                
 
3228
            }
 
3229
            
 
3230
            if(dynamic_cast<AFCondition*>(a.get()))
 
3231
            {
 
3232
                ++stats[15];
 
3233
                if(negated) return std::make_shared<NotCondition>(a);
 
3234
                return a;
 
3235
 
 
3236
            }
 
3237
            else if(dynamic_cast<EFCondition*>(a.get()))
 
3238
            {
 
3239
                ++stats[16];
 
3240
                if(negated) return std::make_shared<NotCondition>(a);
 
3241
                return a;
 
3242
            }
 
3243
            else if(auto cond = dynamic_cast<OrCondition*>(a.get()))
 
3244
            {
 
3245
 
 
3246
                std::vector<Condition_ptr> pef, npef;
 
3247
                for(auto& i : *cond)
 
3248
                {
 
3249
                    if(dynamic_cast<EFCondition*>(i.get()))
 
3250
                    {
 
3251
                        pef.push_back(i);
 
3252
                    }
 
3253
                    else
 
3254
                    {
 
3255
                        npef.push_back(i);
 
3256
                    }
 
3257
                }
 
3258
                if(pef.size() > 0)
 
3259
                {
 
3260
                    stats[17] += pef.size();
 
3261
                    pef.push_back(std::make_shared<AFCondition>(makeOr(npef)));
 
3262
                    return makeOr(pef)->pushNegation(stats, context, nested, negated, initrw);
 
3263
                }
 
3264
            }
 
3265
            else if(auto cond = dynamic_cast<AUCondition*>(a.get()))
 
3266
            {
 
3267
                ++stats[18];
 
3268
                return AFCondition((*cond)[1]).pushNegation(stats, context, nested, negated, initrw);
 
3269
            }
 
3270
            auto b = std::make_shared<AFCondition>(a);
 
3271
            if(negated) return std::make_shared<NotCondition>(b);
 
3272
            return b;
 
3273
            }, stats, context, nested, negated, initrw);
 
3274
        }
 
3275
 
 
3276
        Condition_ptr AUCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
 
3277
            return initialMarkingRW([&]() -> Condition_ptr {
 
3278
            auto b = _cond2->pushNegation(stats, context, true, false, initrw);
 
3279
            auto a = _cond1->pushNegation(stats, context, true, false, initrw);
 
3280
            if(auto cond = dynamic_cast<NotCondition*>(b.get()))
 
3281
            {
 
3282
                if((*cond)[0] == DeadlockCondition::DEADLOCK)
 
3283
                {
 
3284
                    ++stats[19];
 
3285
                    return b->pushNegation(stats, context, nested, negated, initrw);
 
3286
                }
 
3287
            }
 
3288
            else if(a == DeadlockCondition::DEADLOCK)
 
3289
            {
 
3290
                ++stats[20];
 
3291
                return b->pushNegation(stats, context, nested, negated, initrw);
 
3292
            }
 
3293
            else if(auto cond = dynamic_cast<NotCondition*>(a.get()))
 
3294
            {
 
3295
                if((*cond)[0] == DeadlockCondition::DEADLOCK)
 
3296
                {
 
3297
                    ++stats[21];
 
3298
                    return AFCondition(b).pushNegation(stats, context, nested, negated, initrw);
 
3299
                }
 
3300
            }
 
3301
            
 
3302
            if(auto cond = dynamic_cast<AFCondition*>(b.get()))
 
3303
            {
 
3304
                ++stats[22];
 
3305
                return cond->pushNegation(stats, context, nested, negated, initrw);
 
3306
            }
 
3307
            else if(dynamic_cast<EFCondition*>(b.get()))
 
3308
            {
 
3309
                ++stats[23];
 
3310
                if(negated) return std::make_shared<NotCondition>(b);
 
3311
                return b;
 
3312
            }
 
3313
            else if(auto cond = dynamic_cast<OrCondition*>(b.get()))
 
3314
            {
 
3315
                std::vector<Condition_ptr> pef, npef;
 
3316
                for(auto& i : *cond)
 
3317
                {
 
3318
                    if(dynamic_cast<EFCondition*>(i.get()))
 
3319
                    {
 
3320
                        pef.push_back(i);
 
3321
                    }
 
3322
                    else
 
3323
                    {
 
3324
                        npef.push_back(i);
 
3325
                    }
 
3326
                }
 
3327
                if(pef.size() > 0)
 
3328
                {
 
3329
                    stats[24] += pef.size();
 
3330
                    if(npef.size() != 0)
 
3331
                    {
 
3332
                        pef.push_back(std::make_shared<AUCondition>(_cond1, makeOr(npef)));
 
3333
                    }
 
3334
                    else
 
3335
                    {
 
3336
                        ++stats[23];
 
3337
                        --stats[24];
 
3338
                    }
 
3339
                    return makeOr(pef)->pushNegation(stats, context, nested, negated, initrw);
 
3340
                }
 
3341
            }
 
3342
            
 
3343
            auto c = std::make_shared<AUCondition>(a, b);
 
3344
            if(negated) return std::make_shared<NotCondition>(c);
 
3345
            return c;
 
3346
            }, stats, context, nested, negated, initrw);
 
3347
        }
 
3348
 
 
3349
 
 
3350
        Condition_ptr EUCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
 
3351
            return initialMarkingRW([&]() -> Condition_ptr {
 
3352
            auto b = _cond2->pushNegation(stats, context, true, false, initrw);
 
3353
            auto a = _cond1->pushNegation(stats, context, true, false, initrw);
 
3354
 
 
3355
            if(auto cond = dynamic_cast<NotCondition*>(b.get()))
 
3356
            {
 
3357
                if((*cond)[0] == DeadlockCondition::DEADLOCK)
 
3358
                {
 
3359
                    ++stats[25];
 
3360
                    return b->pushNegation(stats, context, nested, negated, initrw);
 
3361
                }
 
3362
            }
 
3363
            else if(a == DeadlockCondition::DEADLOCK)
 
3364
            {
 
3365
                ++stats[26];
 
3366
                return b->pushNegation(stats, context, nested, negated, initrw);
 
3367
            }
 
3368
            else if(auto cond = dynamic_cast<NotCondition*>(a.get()))
 
3369
            {
 
3370
                if((*cond)[0] == DeadlockCondition::DEADLOCK)
 
3371
                {
 
3372
                    ++stats[27];
 
3373
                    return EFCondition(b).pushNegation(stats, context, nested, negated, initrw);
 
3374
                }
 
3375
            }
 
3376
            
 
3377
            if(dynamic_cast<EFCondition*>(b.get()))
 
3378
            {
 
3379
                ++stats[28];
 
3380
                if(negated) return std::make_shared<NotCondition>(b);
 
3381
                return b;
 
3382
            }
 
3383
            else if(auto cond = dynamic_cast<OrCondition*>(b.get()))
 
3384
            {
 
3385
                std::vector<Condition_ptr> pef, npef;
 
3386
                for(auto& i : *cond)
 
3387
                {
 
3388
                    if(dynamic_cast<EFCondition*>(i.get()))
 
3389
                    {
 
3390
                        pef.push_back(i);
 
3391
                    }
 
3392
                    else
 
3393
                    {
 
3394
                        npef.push_back(i);
 
3395
                    }
 
3396
                }
 
3397
                if(pef.size() > 0)
 
3398
                {
 
3399
                    stats[29] += pef.size();
 
3400
                    if(npef.size() != 0)
 
3401
                    {
 
3402
                        pef.push_back(std::make_shared<EUCondition>(_cond1, makeOr(npef)));
 
3403
                        ++stats[28];
 
3404
                        --stats[29];
 
3405
                    }
 
3406
                    return makeOr(pef)->pushNegation(stats, context, nested, negated, initrw);
 
3407
                }
 
3408
            }
 
3409
            auto c = std::make_shared<EUCondition>(a, b);
 
3410
            if(negated) return std::make_shared<NotCondition>(c);
 
3411
            return c;
 
3412
            }, stats, context, nested, negated, initrw);
 
3413
        }
 
3414
 
 
3415
        
 
3416
        Condition_ptr pushAnd(const std::vector<Condition_ptr>& _conds, negstat_t& stats, const EvaluationContext& context, bool nested, bool negate_children, bool initrw)
 
3417
        {
 
3418
            std::vector<Condition_ptr> nef, other;            
 
3419
            for(auto& c : _conds)
 
3420
            {
 
3421
                auto n = c->pushNegation(stats, context, nested, negate_children, initrw);
 
3422
                if(n->isTriviallyFalse()) return n;
 
3423
                if(n->isTriviallyTrue()) continue;
 
3424
                if(auto neg = dynamic_cast<NotCondition*>(n.get()))
 
3425
                {
 
3426
                    if(auto ef = dynamic_cast<EFCondition*>((*neg)[0].get()))
 
3427
                    {
 
3428
                        nef.push_back((*ef)[0]);
 
3429
                    }
 
3430
                    else
 
3431
                    {
 
3432
                        other.emplace_back(n);
 
3433
                    }
 
3434
                }
 
3435
                else
 
3436
                {
 
3437
                    other.emplace_back(n);
 
3438
                }
 
3439
            }         
 
3440
            if(nef.size() + other.size() == 0) return BooleanCondition::TRUE_CONSTANT;
 
3441
            if(nef.size() + other.size() == 1) 
 
3442
            { 
 
3443
                return nef.size() == 0 ? 
 
3444
                    other[0] : 
 
3445
                    std::make_shared<NotCondition>(std::make_shared<EFCondition>(nef[0]));
 
3446
            }
 
3447
            if(nef.size() != 0) other.push_back(
 
3448
                    std::make_shared<NotCondition>(
 
3449
                    std::make_shared<EFCondition>(
 
3450
                    makeOr(nef)))); 
 
3451
            if(other.size() == 1) return other[0];
 
3452
            auto res = makeAnd(other);
 
3453
            return res;
 
3454
        }
 
3455
        
 
3456
        Condition_ptr pushOr(const std::vector<Condition_ptr>& _conds, negstat_t& stats, const EvaluationContext& context, bool nested, bool negate_children, bool initrw)
 
3457
        {
 
3458
            std::vector<Condition_ptr> nef, other;       
 
3459
            for(auto& c : _conds)
 
3460
            {
 
3461
                auto n = c->pushNegation(stats, context, nested, negate_children, initrw);
 
3462
                if(n->isTriviallyTrue())
 
3463
                {
 
3464
                    return n;
 
3465
                }
 
3466
                if(n->isTriviallyFalse()) continue;
 
3467
                if(auto ef = dynamic_cast<EFCondition*>(n.get()))
 
3468
                {
 
3469
                    nef.push_back((*ef)[0]);
 
3470
                }
 
3471
                else
 
3472
                {
 
3473
                    other.emplace_back(n);
 
3474
                }
 
3475
            }
 
3476
            if(nef.size() + other.size() == 0) return BooleanCondition::FALSE_CONSTANT;
 
3477
            if(nef.size() + other.size() == 1) { return nef.size() == 0 ? other[0] : std::make_shared<EFCondition>(nef[0]);}
 
3478
            if(nef.size() != 0) other.push_back(
 
3479
                    std::make_shared<EFCondition>(
 
3480
                    makeOr(nef))); 
 
3481
            if(other.size() == 1) return other[0];
 
3482
            return makeOr(other);
 
3483
        }
 
3484
 
 
3485
        Condition_ptr OrCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
 
3486
            return initialMarkingRW([&]() -> Condition_ptr {
 
3487
            return negated ? pushAnd(_conds, stats, context, nested, true, initrw) :
 
3488
                             pushOr (_conds, stats, context, nested, false, initrw);
 
3489
            }, stats, context, nested, negated, initrw);
 
3490
        }
 
3491
 
 
3492
        
 
3493
        Condition_ptr AndCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
 
3494
            return initialMarkingRW([&]() -> Condition_ptr {
 
3495
            return negated ? pushOr (_conds, stats, context, nested, true, initrw) :
 
3496
                             pushAnd(_conds, stats, context, nested, false, initrw);
 
3497
 
 
3498
            }, stats, context, nested, negated, initrw);
 
3499
        }
 
3500
        
 
3501
        Condition_ptr CompareConjunction::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
 
3502
            return initialMarkingRW([&]() -> Condition_ptr {
 
3503
            return std::make_shared<CompareConjunction>(*this, negated);
 
3504
            }, stats, context, nested, negated, initrw);
 
3505
        }
 
3506
 
 
3507
        
 
3508
        Condition_ptr NotCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
 
3509
            return initialMarkingRW([&]() -> Condition_ptr {
 
3510
            if(negated) ++stats[30];
 
3511
            return _cond->pushNegation(stats, context, nested, !negated, initrw);
 
3512
            }, stats, context, nested, negated, initrw);
 
3513
        }
 
3514
 
 
3515
        template<typename T>
 
3516
        Condition_ptr pushFireableNegation(negstat_t& stat, const EvaluationContext& context, bool nested, bool negated, bool initrw, const std::string& name, const Condition_ptr& compiled)
 
3517
        {
 
3518
            if(compiled)
 
3519
                return compiled->pushNegation(stat, context, nested, negated, initrw);
 
3520
            if(negated)
 
3521
            {
 
3522
                stat.negated_fireability = true;
 
3523
                return std::make_shared<NotCondition>(std::make_shared<T>(name));
 
3524
            }
 
3525
            else
 
3526
                return std::make_shared<T>(name);
 
3527
        }
 
3528
 
 
3529
        Condition_ptr UnfoldedFireableCondition::pushNegation(negstat_t& stat, const EvaluationContext& context, bool nested, bool negated, bool initrw)
 
3530
        {
 
3531
            return pushFireableNegation<UnfoldedFireableCondition>(stat, context, nested, negated, initrw, _name, _compiled);
 
3532
        }
 
3533
 
 
3534
        Condition_ptr FireableCondition::pushNegation(negstat_t& stat, const EvaluationContext& context, bool nested, bool negated, bool initrw)
 
3535
        {
 
3536
            return pushFireableNegation<FireableCondition>(stat, context, nested, negated, initrw, _name, _compiled);
 
3537
        }
 
3538
 
 
3539
        bool CompareCondition::isTrivial() const
 
3540
        {
 
3541
            auto remdup = [](auto& a, auto& b){
 
3542
                auto ai = a->_ids.begin();
 
3543
                auto bi = b->_ids.begin();
 
3544
                while(ai != a->_ids.end() && bi != b->_ids.end())
 
3545
                {
 
3546
                    while(ai != a->_ids.end() && ai->first < bi->first) ++ai;
 
3547
                    if(ai == a->_ids.end()) break;
 
3548
                    if(ai->first == bi->first)
 
3549
                    {
 
3550
                        ai = a->_ids.erase(ai);
 
3551
                        bi = b->_ids.erase(bi);
 
3552
                    }
 
3553
                    else
 
3554
                    {
 
3555
                        ++bi;
 
3556
                    }
 
3557
                    if(bi == b->_ids.end() || ai == a->_ids.end()) break;
 
3558
                }
 
3559
            };
 
3560
            if(auto p1 = dynamic_pointer_cast<PlusExpr>(_expr1))
 
3561
                if(auto p2 = dynamic_pointer_cast<PlusExpr>(_expr2))
 
3562
                    remdup(p1, p2);
 
3563
            
 
3564
            if(auto m1 = dynamic_pointer_cast<MultiplyExpr>(_expr1))
 
3565
                if(auto m2 = dynamic_pointer_cast<MultiplyExpr>(_expr2))
 
3566
                    remdup(m1, m2);                    
 
3567
            
 
3568
            if(auto p1 = dynamic_pointer_cast<CommutativeExpr>(_expr1))
 
3569
                if(auto p2 = dynamic_pointer_cast<CommutativeExpr>(_expr2))            
 
3570
                    return p1->_exprs.size() + p1->_ids.size() + p2->_exprs.size() + p2->_ids.size() == 0;
 
3571
            return _expr1->placeFree() && _expr2->placeFree();
 
3572
        }        
 
3573
        
 
3574
        Condition_ptr LessThanCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
 
3575
            return initialMarkingRW([&]() -> Condition_ptr {
 
3576
            if(isTrivial()) return BooleanCondition::getShared(evaluate(context) xor negated);                
 
3577
            if(negated) return std::make_shared<GreaterThanOrEqualCondition>(_expr1, _expr2);
 
3578
            else        return std::make_shared<LessThanCondition>(_expr1, _expr2);
 
3579
            }, stats, context, nested, negated, initrw);
 
3580
        }
 
3581
 
 
3582
        
 
3583
        Condition_ptr GreaterThanOrEqualCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
 
3584
            return initialMarkingRW([&]() -> Condition_ptr {
 
3585
            if(isTrivial()) return BooleanCondition::getShared(evaluate(context) xor negated);                
 
3586
            if(negated) return std::make_shared<LessThanCondition>(_expr1, _expr2);
 
3587
            else        return std::make_shared<GreaterThanOrEqualCondition>(_expr1, _expr2);
 
3588
            }, stats, context, nested, negated, initrw);
 
3589
        }
 
3590
 
 
3591
        
 
3592
        Condition_ptr LessThanOrEqualCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
 
3593
            return initialMarkingRW([&]() -> Condition_ptr {
 
3594
            if(isTrivial()) return BooleanCondition::getShared(evaluate(context) xor negated);                
 
3595
            if(negated) return std::make_shared<GreaterThanCondition>(_expr1, _expr2);
 
3596
            else        return std::make_shared<LessThanOrEqualCondition>(_expr1, _expr2);
 
3597
            }, stats, context, nested, negated, initrw);
 
3598
        }
 
3599
 
 
3600
        
 
3601
        Condition_ptr GreaterThanCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
 
3602
            return initialMarkingRW([&]() -> Condition_ptr {
 
3603
            if(isTrivial()) return BooleanCondition::getShared(evaluate(context) xor negated);
 
3604
            if(negated) return std::make_shared<LessThanOrEqualCondition>(_expr1, _expr2);
 
3605
            else        return std::make_shared<GreaterThanCondition>(_expr1, _expr2);
 
3606
            }, stats, context, nested, negated, initrw);
 
3607
        }
 
3608
                
 
3609
        Condition_ptr pushEqual(CompareCondition* org, bool negated, bool noteq, const EvaluationContext& context)
 
3610
        {
 
3611
            if(org->isTrivial()) return BooleanCondition::getShared(org->evaluate(context) xor negated);
 
3612
            for(auto i : {0,1})
 
3613
            {
 
3614
                if((*org)[i]->placeFree() && (*org)[i]->evaluate(context) == 0)
 
3615
                {
 
3616
                    if(negated == noteq) return std::make_shared<LessThanOrEqualCondition>((*org)[(i + 1) % 2], std::make_shared<LiteralExpr>(0));
 
3617
                    else                 return std::make_shared<GreaterThanOrEqualCondition>((*org)[(i + 1) % 2], std::make_shared<LiteralExpr>(1));
 
3618
                }
 
3619
            }
 
3620
            if(negated == noteq) return std::make_shared<EqualCondition>((*org)[0], (*org)[1]);
 
3621
            else                 return std::make_shared<NotEqualCondition>((*org)[0], (*org)[1]);
 
3622
        }
 
3623
        
 
3624
        Condition_ptr NotEqualCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
 
3625
            return initialMarkingRW([&]() -> Condition_ptr {
 
3626
                return pushEqual(this, negated, true, context);
 
3627
            }, stats, context, nested, negated, initrw);
 
3628
        }
 
3629
 
 
3630
        
 
3631
        Condition_ptr EqualCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
 
3632
            return initialMarkingRW([&]() -> Condition_ptr {
 
3633
                return pushEqual(this, negated, false, context);
 
3634
            }, stats, context, nested, negated, initrw);
 
3635
        }
 
3636
                
 
3637
        Condition_ptr BooleanCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
 
3638
            return initialMarkingRW([&]() -> Condition_ptr {
 
3639
            if(negated) return getShared(!_value);
 
3640
            else        return getShared( _value);
 
3641
            }, stats, context, nested, negated, initrw);
 
3642
        }
 
3643
        
 
3644
        Condition_ptr DeadlockCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
 
3645
            return initialMarkingRW([&]() -> Condition_ptr {
 
3646
            if(negated) return std::make_shared<NotCondition>(DEADLOCK);
 
3647
            else        return DEADLOCK;
 
3648
            }, stats, context, nested, negated, initrw);
 
3649
        }
 
3650
        
 
3651
        Condition_ptr UnfoldedUpperBoundsCondition::pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
 
3652
            if(negated)
 
3653
            {
 
3654
                std::cerr << "UPPER BOUNDS CANNOT BE NEGATED!" << std::endl;
 
3655
                exit(ErrorCode);
 
3656
            }
 
3657
            return std::make_shared<UnfoldedUpperBoundsCondition>(_places, _max, _offset);
 
3658
        }
 
3659
 
 
3660
        
 
3661
        /******************** Stubborn reduction interesting transitions ********************/
 
3662
        
 
3663
        void PlusExpr::incr(ReducingSuccessorGenerator& generator) const { 
 
3664
            for(auto& i : _ids) generator.presetOf(i.first, true);
 
3665
            for(auto& e : _exprs) e->incr(generator);
 
3666
        }
 
3667
        
 
3668
        void PlusExpr::decr(ReducingSuccessorGenerator& generator) const {
 
3669
            for(auto& i : _ids) generator.postsetOf(i.first, true);
 
3670
            for(auto& e : _exprs) e->decr(generator);
 
3671
        }
 
3672
        
 
3673
        void SubtractExpr::incr(ReducingSuccessorGenerator& generator) const {
 
3674
            bool first = true;
 
3675
            for(auto& e : _exprs)
 
3676
            {
 
3677
                if(first)
 
3678
                    e->incr(generator);
 
3679
                else
 
3680
                    e->decr(generator);
 
3681
                first = false;
 
3682
            }
 
3683
        }
 
3684
        
 
3685
        void SubtractExpr::decr(ReducingSuccessorGenerator& generator) const {
 
3686
            bool first = true;
 
3687
            for(auto& e : _exprs)
 
3688
            {
 
3689
                if(first)
 
3690
                    e->decr(generator);
 
3691
                else
 
3692
                    e->incr(generator);
 
3693
                first = false;
 
3694
            }
 
3695
        }
 
3696
        
 
3697
        void MultiplyExpr::incr(ReducingSuccessorGenerator& generator) const {
 
3698
            if((_ids.size() + _exprs.size()) == 1)
 
3699
            {
 
3700
                for(auto& i : _ids) generator.presetOf(i.first, true);
 
3701
                for(auto& e : _exprs) e->incr(generator);                
 
3702
            }
 
3703
            else
 
3704
            {
 
3705
                for(auto& i : _ids)
 
3706
                {
 
3707
                    generator.presetOf(i.first, true);
 
3708
                    generator.postsetOf(i.first, true);
 
3709
                }
 
3710
                for(auto& e : _exprs)
 
3711
                {
 
3712
                    e->incr(generator);
 
3713
                    e->decr(generator);
 
3714
                }
 
3715
            }
 
3716
        }
 
3717
        
 
3718
        void MultiplyExpr::decr(ReducingSuccessorGenerator& generator) const {
 
3719
            if((_ids.size() + _exprs.size()) == 1)
 
3720
            {
 
3721
                for(auto& i : _ids) generator.postsetOf(i.first, true);
 
3722
                for(auto& e : _exprs) e->decr(generator);            
 
3723
            }
 
3724
            else
 
3725
                incr(generator);
 
3726
        }
 
3727
        
 
3728
        void MinusExpr::incr(ReducingSuccessorGenerator& generator) const {
 
3729
            // TODO not implemented
 
3730
        }
 
3731
        
 
3732
        void MinusExpr::decr(ReducingSuccessorGenerator& generator) const {
 
3733
            // TODO not implemented
 
3734
        }
 
3735
 
 
3736
        void LiteralExpr::incr(ReducingSuccessorGenerator& generator) const {
 
3737
            // Add nothing
 
3738
        }
 
3739
        
 
3740
        void LiteralExpr::decr(ReducingSuccessorGenerator& generator) const {
 
3741
            // Add nothing
 
3742
        }
 
3743
 
 
3744
        void UnfoldedIdentifierExpr::incr(ReducingSuccessorGenerator& generator) const {
 
3745
            generator.presetOf(_offsetInMarking, true);
 
3746
        }
 
3747
        
 
3748
        void UnfoldedIdentifierExpr::decr(ReducingSuccessorGenerator& generator) const {
 
3749
             generator.postsetOf(_offsetInMarking, true);
 
3750
        }
 
3751
        
 
3752
        void SimpleQuantifierCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const{
 
3753
            _cond->findInteresting(generator, negated);
 
3754
        }
 
3755
        
 
3756
        void UntilCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const{
 
3757
            _cond1->findInteresting(generator, negated);
 
3758
            _cond1->findInteresting(generator, !negated);
 
3759
            _cond2->findInteresting(generator, negated);
 
3760
        }
 
3761
        
 
3762
        void AndCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
 
3763
            if(!negated){               // and
 
3764
                for(auto& c : _conds)
 
3765
                {
 
3766
                    if(!c->isSatisfied())
 
3767
                    {
 
3768
                        c->findInteresting(generator, negated);
 
3769
                        break;
 
3770
                    }
 
3771
                }
 
3772
            } else {                    // or
 
3773
                for(auto& c : _conds) c->findInteresting(generator, negated);
 
3774
            }
 
3775
        }
 
3776
        
 
3777
        void OrCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
 
3778
            if(!negated){               // or
 
3779
                for(auto& c : _conds) c->findInteresting(generator, negated);
 
3780
            } else {                    // and
 
3781
                for(auto& c : _conds)
 
3782
                {
 
3783
                    if(c->isSatisfied())
 
3784
                    {
 
3785
                        c->findInteresting(generator, negated);
 
3786
                        break;
 
3787
                    }
 
3788
                }
 
3789
            }
 
3790
        }
 
3791
        
 
3792
        void CompareConjunction::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const{
 
3793
             
 
3794
            auto neg = negated != _negated;
 
3795
            int32_t cand = std::numeric_limits<int32_t>::max();
 
3796
            bool pre = false;
 
3797
            for(auto& c : _constraints)
 
3798
            {
 
3799
                auto val = generator.parent()[c._place];
 
3800
                if(c._lower == c._upper)
 
3801
                {
 
3802
                    if(neg)
 
3803
                    {
 
3804
                        if(val != c._lower) continue;
 
3805
                        generator.postsetOf(c._place, true);
 
3806
                        generator.presetOf(c._place, true);
 
3807
                    }
 
3808
                    else
 
3809
                    {
 
3810
                        if(val == c._lower) continue;
 
3811
                        if(val > c._lower) {
 
3812
                            cand = c._place;
 
3813
                            pre = false;
 
3814
                        } else {
 
3815
                            cand = c._place;
 
3816
                            pre = true;
 
3817
                        }   
 
3818
                    }
 
3819
                }
 
3820
                else
 
3821
                {
 
3822
                    if(!neg)
 
3823
                    {
 
3824
                        if(val < c._lower && c._lower != 0)
 
3825
                        {
 
3826
                            assert(!neg);
 
3827
                            cand = c._place;
 
3828
                            pre = true;
 
3829
                        }
 
3830
                        
 
3831
                        if(val > c._upper && c._upper != std::numeric_limits<uint32_t>::max())
 
3832
                        {
 
3833
                            assert(!neg);
 
3834
                            cand = c._place;
 
3835
                            pre = false;
 
3836
                        }
 
3837
                    }
 
3838
                    else
 
3839
                    {
 
3840
                        if(val >= c._lower && c._lower != 0)
 
3841
                        {
 
3842
                            generator.postsetOf(c._place, true);
 
3843
                        }
 
3844
                        
 
3845
                        if(val <= c._upper && c._upper != std::numeric_limits<uint32_t>::max())
 
3846
                        {
 
3847
                            generator.presetOf(c._place, true);
 
3848
                        }
 
3849
                    }
 
3850
                }
 
3851
                if(cand != std::numeric_limits<int32_t>::max())
 
3852
                {
 
3853
                    if(pre && generator.seenPre(cand))
 
3854
                        return;
 
3855
                    else if(!pre && generator.seenPost(cand))
 
3856
                        return;
 
3857
                }
 
3858
            }
 
3859
            if(cand != std::numeric_limits<int32_t>::max())
 
3860
            {
 
3861
                if(pre)
 
3862
                {
 
3863
                    generator.presetOf(cand, true);
 
3864
                }
 
3865
                else if(!pre)
 
3866
                {
 
3867
                    generator.postsetOf(cand, true);
 
3868
                }
 
3869
            }
 
3870
        }
 
3871
        
 
3872
        void EqualCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
 
3873
            if(!negated){               // equal
 
3874
                if(_expr1->getEval() == _expr2->getEval()) { return; }
 
3875
                if(_expr1->getEval() > _expr2->getEval()){
 
3876
                    _expr1->decr(generator);
 
3877
                    _expr2->incr(generator);
 
3878
                } else {
 
3879
                    _expr1->incr(generator);
 
3880
                    _expr2->decr(generator);
 
3881
                }   
 
3882
            } else {                    // not equal
 
3883
                if(_expr1->getEval() != _expr2->getEval()) { return; }
 
3884
                _expr1->incr(generator);
 
3885
                _expr1->decr(generator);
 
3886
                _expr2->incr(generator);
 
3887
                _expr2->decr(generator);
 
3888
            }
 
3889
        }
 
3890
        
 
3891
        void NotEqualCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
 
3892
            if(!negated){               // not equal
 
3893
                if(_expr1->getEval() != _expr2->getEval()) { return; }
 
3894
                _expr1->incr(generator);
 
3895
                _expr1->decr(generator);
 
3896
                _expr2->incr(generator);
 
3897
                _expr2->decr(generator);
 
3898
            } else {                    // equal
 
3899
                if(_expr1->getEval() == _expr2->getEval()) { return; }
 
3900
                if(_expr1->getEval() > _expr2->getEval()){
 
3901
                    _expr1->decr(generator);
 
3902
                    _expr2->incr(generator);
 
3903
                } else {
 
3904
                    _expr1->incr(generator);
 
3905
                    _expr2->decr(generator);
 
3906
                }   
 
3907
            }
 
3908
        }
 
3909
        
 
3910
        void LessThanCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {                
 
3911
            if(!negated){               // less than
 
3912
                if(_expr1->getEval() < _expr2->getEval()) { return; }
 
3913
                _expr1->decr(generator);
 
3914
                _expr2->incr(generator);
 
3915
            } else {                    // greater than or equal
 
3916
                if(_expr1->getEval() >= _expr2->getEval()) { return; }
 
3917
                _expr1->incr(generator);
 
3918
                _expr2->decr(generator);
 
3919
            }
 
3920
        }
 
3921
        
 
3922
        void LessThanOrEqualCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
 
3923
            if(!negated){               // less than or equal
 
3924
                if(_expr1->getEval() <= _expr2->getEval()) { return; }
 
3925
                _expr1->decr(generator);
 
3926
                _expr2->incr(generator);
 
3927
            } else {                    // greater than
 
3928
                if(_expr1->getEval() > _expr2->getEval()) { return; }
 
3929
                _expr1->incr(generator);
 
3930
                _expr2->decr(generator);
 
3931
            }
 
3932
        }
 
3933
        
 
3934
        void GreaterThanCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
 
3935
            if(!negated){               // greater than
 
3936
                if(_expr1->getEval() > _expr2->getEval()) { return; }
 
3937
                _expr1->incr(generator);
 
3938
                _expr2->decr(generator);
 
3939
            } else {                    // less than or equal
 
3940
                if(_expr1->getEval() <= _expr2->getEval()) { return; }
 
3941
                _expr1->decr(generator);
 
3942
                _expr2->incr(generator);
 
3943
            }
 
3944
        }
 
3945
        
 
3946
        void GreaterThanOrEqualCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
 
3947
            if(!negated){               // greater than or equal
 
3948
                if(_expr1->getEval() >= _expr2->getEval()) { return; }
 
3949
                _expr1->incr(generator);
 
3950
                _expr2->decr(generator); 
 
3951
            } else {                    // less than
 
3952
                if(_expr1->getEval() < _expr2->getEval()) { return; }
 
3953
                _expr1->decr(generator);
 
3954
                _expr2->incr(generator);
 
3955
            }
 
3956
        }
 
3957
        
 
3958
        void NotCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
 
3959
            _cond->findInteresting(generator, !negated);
 
3960
        }
 
3961
        
 
3962
        void BooleanCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
 
3963
            // Add nothing
 
3964
        }
 
3965
        
 
3966
        void DeadlockCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
 
3967
            if(!isSatisfied()){
 
3968
                generator.postPresetOf(generator.leastDependentEnabled(), true);
 
3969
            } // else add nothing
 
3970
        }
 
3971
 
 
3972
        void UnfoldedUpperBoundsCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
 
3973
            for(auto& p : _places)
 
3974
                if(!p._maxed_out)
 
3975
                    generator.presetOf(p._place);
 
3976
        }
 
3977
        
 
3978
        
 
3979
/********************** CONSTRUCTORS *********************************/
 
3980
 
 
3981
        template<typename T>
 
3982
        void postMerge(std::vector<Condition_ptr>& conds) {
 
3983
            std::sort(std::begin(conds), std::end(conds),
 
3984
                    [](auto& a, auto& b) {
 
3985
                        return a->isTemporal() < b->isTemporal(); 
 
3986
                    });
 
3987
        } 
 
3988
        
 
3989
        AndCondition::AndCondition(std::vector<Condition_ptr>&& conds) {
 
3990
            for (auto& c : conds) tryMerge<AndCondition>(_conds, c);
 
3991
            for (auto& c : _conds) _temporal = _temporal || c->isTemporal();
 
3992
            for (auto& c : _conds) _loop_sensitive = _loop_sensitive || c->isLoopSensitive();
 
3993
            postMerge<AndCondition>(_conds);
 
3994
        }
 
3995
        
 
3996
        AndCondition::AndCondition(const std::vector<Condition_ptr>& conds) {
 
3997
            for (auto& c : conds) tryMerge<AndCondition>(_conds, c);
 
3998
            for (auto& c : _conds) _temporal = _temporal || c->isTemporal();
 
3999
            for (auto& c : _conds) _loop_sensitive = _loop_sensitive || c->isLoopSensitive();
 
4000
            postMerge<AndCondition>(_conds);
 
4001
        }
 
4002
       
 
4003
        AndCondition::AndCondition(Condition_ptr left, Condition_ptr right) {
 
4004
            tryMerge<AndCondition>(_conds, left);
 
4005
            tryMerge<AndCondition>(_conds, right);
 
4006
            for (auto& c : _conds) _temporal = _temporal || c->isTemporal();
 
4007
            for (auto& c : _conds) _loop_sensitive = _loop_sensitive || c->isLoopSensitive();
 
4008
            postMerge<AndCondition>(_conds);
 
4009
        }
 
4010
       
 
4011
        OrCondition::OrCondition(std::vector<Condition_ptr>&& conds) {
 
4012
            for (auto& c : conds) tryMerge<OrCondition>(_conds, c);
 
4013
            for (auto& c : _conds) _temporal = _temporal || c->isTemporal();
 
4014
            for (auto& c : _conds) _loop_sensitive = _loop_sensitive || c->isLoopSensitive();
 
4015
            postMerge<AndCondition>(_conds);
 
4016
        }
 
4017
       
 
4018
        OrCondition::OrCondition(const std::vector<Condition_ptr>& conds) {
 
4019
            for (auto& c : conds) tryMerge<OrCondition>(_conds, c);
 
4020
            for (auto& c : _conds) _temporal = _temporal || c->isTemporal();
 
4021
            for (auto& c : _conds) _loop_sensitive = _loop_sensitive || c->isLoopSensitive();
 
4022
            postMerge<AndCondition>(_conds);
 
4023
        }
 
4024
       
 
4025
        OrCondition::OrCondition(Condition_ptr left, Condition_ptr right) {
 
4026
            tryMerge<OrCondition>(_conds, left);
 
4027
            tryMerge<OrCondition>(_conds, right);
 
4028
            for (auto& c : _conds) _temporal = _temporal || c->isTemporal();
 
4029
            for (auto& c : _conds) _loop_sensitive = _loop_sensitive || c->isLoopSensitive();
 
4030
            postMerge<AndCondition>(_conds);
 
4031
        }
 
4032
        
 
4033
 
 
4034
        CompareConjunction::CompareConjunction(const std::vector<Condition_ptr>& conditions, bool negated)
 
4035
        {
 
4036
            _negated = negated;
 
4037
            merge(conditions, negated);
 
4038
        }
 
4039
        
 
4040
        void CompareConjunction::merge(const CompareConjunction& other)
 
4041
        {
 
4042
            auto neg = _negated != other._negated;
 
4043
            if(neg && other._constraints.size() > 1)
 
4044
            {
 
4045
                std::cerr << "MERGE OF CONJUNCT AND DISJUNCT NOT ALLOWED" << std::endl;
 
4046
                assert(false);
 
4047
                exit(ErrorCode);
 
4048
            }
 
4049
            auto il = _constraints.begin();
 
4050
            for(auto c : other._constraints)
 
4051
            {
 
4052
                if(neg)
 
4053
                    c.invert();
 
4054
                                
 
4055
                if(c._upper == std::numeric_limits<uint32_t>::max() && c._lower == 0)
 
4056
                {
 
4057
                    continue;
 
4058
                }
 
4059
                else if (c._upper != std::numeric_limits<uint32_t>::max() && c._lower != 0 && neg)
 
4060
                {
 
4061
                    std::cerr << "MERGE OF CONJUNCT AND DISJUNCT NOT ALLOWED" << std::endl;
 
4062
                    assert(false);
 
4063
                    exit(ErrorCode);
 
4064
                }
 
4065
                
 
4066
                il = std::lower_bound(_constraints.begin(), _constraints.end(), c);
 
4067
                if(il == _constraints.end() || il->_place != c._place)
 
4068
                {
 
4069
                    il = _constraints.insert(il, c);
 
4070
                }
 
4071
                else
 
4072
                {
 
4073
                    il->_lower = std::max(il->_lower, c._lower);
 
4074
                    il->_upper = std::min(il->_upper, c._upper);
 
4075
                }
 
4076
            }
 
4077
        }
 
4078
        
 
4079
        void CompareConjunction::merge(const std::vector<Condition_ptr>& conditions, bool negated)
 
4080
        {
 
4081
            for(auto& c : conditions)
 
4082
            {
 
4083
                auto cmp = dynamic_cast<CompareCondition*>(c.get());
 
4084
                assert(cmp);
 
4085
                auto id = dynamic_cast<UnfoldedIdentifierExpr*>((*cmp)[0].get());
 
4086
                uint32_t val;
 
4087
                bool inverted = false;
 
4088
                EvaluationContext context;
 
4089
                if(!id)
 
4090
                {
 
4091
                    id = dynamic_cast<UnfoldedIdentifierExpr*>((*cmp)[1].get());
 
4092
                    val = (*cmp)[0]->evaluate(context);
 
4093
                    inverted = true;
 
4094
                }
 
4095
                else
 
4096
                {
 
4097
                    val = (*cmp)[1]->evaluate(context);
 
4098
                }
 
4099
                assert(id);
 
4100
                cons_t next;
 
4101
                next._place = id->offset();
 
4102
 
 
4103
                if(dynamic_cast<LessThanOrEqualCondition*>(c.get()))
 
4104
                    if(inverted) next._lower = val;
 
4105
                    else         next._upper = val;
 
4106
                else if(dynamic_cast<LessThanCondition*>(c.get()))
 
4107
                    if(inverted) next._lower = val+1;
 
4108
                    else         next._upper = val-1;
 
4109
                else if(dynamic_cast<GreaterThanOrEqualCondition*>(c.get()))
 
4110
                    if(inverted) next._upper = val;
 
4111
                    else         next._lower = val;
 
4112
                else if(dynamic_cast<GreaterThanCondition*>(c.get()))
 
4113
                    if(inverted) next._upper = val-1;
 
4114
                    else         next._lower = val+1;
 
4115
                else if(dynamic_cast<EqualCondition*>(c.get()))
 
4116
                {
 
4117
                    assert(!negated);
 
4118
                    next._lower = val;
 
4119
                    next._upper = val;
 
4120
                }
 
4121
                else if(dynamic_cast<NotEqualCondition*>(c.get()))
 
4122
                {
 
4123
                    assert(negated);
 
4124
                    next._lower = val;
 
4125
                    next._upper = val;
 
4126
                    negated = false; // we already handled negation here!
 
4127
                }
 
4128
                else
 
4129
                {
 
4130
                    std::cerr << "UNKNOWN " << std::endl;
 
4131
                    assert(false);
 
4132
                    exit(ErrorCode);
 
4133
                }
 
4134
                if(negated)
 
4135
                    next.invert();
 
4136
                
 
4137
                auto lb = std::lower_bound(std::begin(_constraints), std::end(_constraints), next);
 
4138
                if(lb == std::end(_constraints) || lb->_place != next._place)
 
4139
                {
 
4140
                    next._name = id->name();
 
4141
                    _constraints.insert(lb, next);
 
4142
                }  
 
4143
                else
 
4144
                {
 
4145
                    assert(id->name().compare(lb->_name) == 0);
 
4146
                    lb->intersect(next);
 
4147
                }
 
4148
            }            
 
4149
        }
 
4150
       
 
4151
        void CommutativeExpr::init(std::vector<Expr_ptr>&& exprs)
 
4152
        {
 
4153
            for (auto& e : exprs) {
 
4154
                if (e->placeFree())
 
4155
                {
 
4156
                    EvaluationContext c;
 
4157
                    _constant = apply(_constant, e->evaluate(c));
 
4158
                }
 
4159
                else if (auto id = dynamic_pointer_cast<PQL::UnfoldedIdentifierExpr>(e)) {
 
4160
                    _ids.emplace_back(id->offset(), id->name());
 
4161
                } 
 
4162
                else if(auto c = dynamic_pointer_cast<CommutativeExpr>(e))
 
4163
                {
 
4164
                    // we should move up plus/multiply here when possible;
 
4165
                    if(c->_ids.size() == 0 && c->_exprs.size() == 0)
 
4166
                    {
 
4167
                        _constant = apply(_constant, c->_constant);
 
4168
                    }
 
4169
                    else
 
4170
                    {
 
4171
                        _exprs.emplace_back(std::move(e));                        
 
4172
                    }
 
4173
                } else {
 
4174
                    _exprs.emplace_back(std::move(e));
 
4175
                }
 
4176
            }
 
4177
        }
 
4178
        
 
4179
        PlusExpr::PlusExpr(std::vector<Expr_ptr>&& exprs, bool tk) : CommutativeExpr(0), tk(tk)
 
4180
        {
 
4181
            init(std::move(exprs));
 
4182
        }
 
4183
        
 
4184
        MultiplyExpr::MultiplyExpr(std::vector<Expr_ptr>&& exprs) : CommutativeExpr(1)
 
4185
        {
 
4186
            init(std::move(exprs));
 
4187
        }
 
4188
 
 
4189
        bool LogicalCondition::nestedDeadlock() const {
 
4190
            for(auto& c : _conds)
 
4191
            {
 
4192
                if(c->getQuantifier() == PQL::DEADLOCK ||
 
4193
                   c->nestedDeadlock() ||
 
4194
                    (c->getQuantifier() == PQL::NEG &&
 
4195
                     (*static_cast<NotCondition*>(c.get()))[0]->getQuantifier() == PQL::DEADLOCK
 
4196
                        ))
 
4197
                {
 
4198
                    return true;
 
4199
                }
 
4200
            }
 
4201
            return false;
 
4202
        }
 
4203
 
 
4204
 
 
4205
    } // PQL
 
4206
} // PetriEngine
 
4207