← Back to branch summary

~verifypn-maintainers/verifypn/emptyTracePrint

« back to all changes in this revision

Viewing changes to PetriEngine/PQL/Expressions.h

  • Committer: Jiri Srba
  • Date: 2018-04-18 10:58:36 UTC
  • mfrom: (197.3.78 cpn_ctlss)
  • Revision ID: srba.jiri@gmail.com-20180418105836-a5rha272u0om4u77
merged in branch lp:~verifypn-cpn/verifypn/cpn_ctlss/

CPN unfolding
CPN linear overapproximation
Export of reduced queries and model
parallel query simplification
TAR for P/T nets
Improved structural reduction rules

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriEngine/PQL/Expressions.h
37
37
        
38
38
        std::string generateTabs(uint32_t tabs);
39
39
        class CompareCondition;
 
40
        class NotCondition;
40
41
        /******************** EXPRESSIONS ********************/
41
42
 
42
43
        /** Base class for all binary expressions */
48
49
            NaryExpr(std::vector<Expr_ptr>&& exprs) : _exprs(std::move(exprs)) {
49
50
            }
50
51
            virtual void analyze(AnalysisContext& context) override;
51
 
            int evaluate(const EvaluationContext& context) const override;
 
52
            int evaluate(const EvaluationContext& context) override;
52
53
            int formulaSize() const override{
53
54
                size_t sum = 0;
54
55
                for(auto& e : _exprs) sum += e->formulaSize();
72
73
        public:
73
74
            friend CompareCondition;
74
75
            virtual void analyze(AnalysisContext& context) override;
75
 
            int evaluate(const EvaluationContext& context) const override;
 
76
            int evaluate(const EvaluationContext& context) override;
 
77
            void toBinary(std::ostream&) const override;
76
78
            int formulaSize() const override{
77
79
                size_t sum = _ids.size();
78
80
                for(auto& e : _exprs) sum += e->formulaSize();
101
103
            bool tk = false;
102
104
            void incr(ReducingSuccessorGenerator& generator) const override;
103
105
            void decr(ReducingSuccessorGenerator& generator) const override;
 
106
#ifdef ENABLE_TAR
 
107
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
 
108
#endif
104
109
        protected:
105
110
            int apply(int v1, int v2) const override;
106
111
            //int binaryOp() const;
119
124
            void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
120
125
            void incr(ReducingSuccessorGenerator& generator) const override;
121
126
            void decr(ReducingSuccessorGenerator& generator) const override;
 
127
#ifdef ENABLE_TAR
 
128
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
 
129
#endif
 
130
            void toBinary(std::ostream&) const override;
 
131
 
122
132
        protected:
123
133
            int apply(int v1, int v2) const override;
124
134
            //int binaryOp() const;
135
145
            void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
136
146
            void incr(ReducingSuccessorGenerator& generator) const override;
137
147
            void decr(ReducingSuccessorGenerator& generator) const override;
 
148
#ifdef ENABLE_TAR
 
149
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
 
150
#endif
138
151
        protected:
139
152
            int apply(int v1, int v2) const override;
140
153
            //int binaryOp() const;
149
162
                _expr = expr;
150
163
            }
151
164
            void analyze(AnalysisContext& context) override;
152
 
            int evaluate(const EvaluationContext& context) const override;
 
165
            int evaluate(const EvaluationContext& context) override;
153
166
            void toString(std::ostream&) const override;
154
167
            Expr::Types type() const override;
155
168
            Member constraint(SimplificationContext& context) const override;
156
169
            void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
 
170
            void toBinary(std::ostream&) const override;
157
171
            void incr(ReducingSuccessorGenerator& generator) const override;
158
172
            void decr(ReducingSuccessorGenerator& generator) const override;
159
173
            int formulaSize() const override{
160
174
                return _expr->formulaSize() + 1;
161
175
            }
 
176
#ifdef ENABLE_TAR
 
177
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
 
178
#endif
162
179
            bool placeFree() const override;
163
180
        private:
164
181
            Expr_ptr _expr;
171
188
            LiteralExpr(int value) : _value(value) {
172
189
            }
173
190
            void analyze(AnalysisContext& context) override;
174
 
            int evaluate(const EvaluationContext& context) const override;
 
191
            int evaluate(const EvaluationContext& context) override;
175
192
            void toString(std::ostream&) const override;
176
193
            Expr::Types type() const override;
177
194
            void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
 
195
            void toBinary(std::ostream&) const override;
178
196
            void incr(ReducingSuccessorGenerator& generator) const override;
179
197
            void decr(ReducingSuccessorGenerator& generator) const override;
180
198
            int formulaSize() const override{
184
202
                return _value;
185
203
            };
186
204
            Member constraint(SimplificationContext& context) const override;
 
205
#ifdef ENABLE_TAR
 
206
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
 
207
#endif
187
208
            bool placeFree() const override { return true; }
188
209
        private:
189
210
            int _value;
190
211
        };
191
212
 
 
213
 
 
214
        class IdentifierExpr : public Expr {
 
215
        public:
 
216
            IdentifierExpr(const std::string& name) : _name(name) {}
 
217
            void analyze(AnalysisContext& context) override;
 
218
            int evaluate(const EvaluationContext& context) override {
 
219
                return _compiled->evaluate(context);
 
220
            }
 
221
            void toString(std::ostream& os) const override {
 
222
                if(_compiled)
 
223
                    _compiled->toString(os);
 
224
                else
 
225
                    os << _name;
 
226
            }
 
227
            Expr::Types type() const override {
 
228
                if(_compiled) return _compiled->type();
 
229
                return Expr::IdentifierExpr;
 
230
            }
 
231
            void toXML(std::ostream& os, uint32_t tabs, bool tokencount = false) const override {
 
232
                _compiled->toXML(os, tabs, tokencount);
 
233
            }
 
234
            void incr(ReducingSuccessorGenerator& generator) const override {
 
235
                _compiled->incr(generator);
 
236
            }
 
237
            void decr(ReducingSuccessorGenerator& generator) const override {
 
238
                _compiled->decr(generator);
 
239
            }
 
240
            int formulaSize() const override {
 
241
                if(_compiled) return _compiled->formulaSize();
 
242
                return 1;
 
243
            }
 
244
            virtual bool placeFree() const override {
 
245
                if(_compiled) return _compiled->placeFree();
 
246
                return false;
 
247
            }
 
248
 
 
249
            Member constraint(SimplificationContext& context) const override {
 
250
                return _compiled->constraint(context);
 
251
            }
 
252
            
 
253
            void toBinary(std::ostream& s) const override {
 
254
                _compiled->toBinary(s);
 
255
            }
 
256
            
 
257
#ifdef ENABLE_TAR
 
258
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const
 
259
            {
 
260
                return _compiled->encodeSat(net, context, uses, incremented);
 
261
            }
 
262
#endif
 
263
        private:
 
264
            std::string _name;
 
265
            Expr_ptr _compiled;
 
266
        };
 
267
 
192
268
        /** Identifier expression */
193
 
        class IdentifierExpr : public Expr {
 
269
        class UnfoldedIdentifierExpr : public Expr {
194
270
        public:
195
 
            IdentifierExpr(const std::string& name, int offest) 
 
271
            UnfoldedIdentifierExpr(const std::string& name, int offest)
196
272
            : _offsetInMarking(offest), _name(name) {
197
273
            }
198
274
            
199
 
            IdentifierExpr(const std::string& name) : IdentifierExpr(name, -1) {
 
275
            UnfoldedIdentifierExpr(const std::string& name) : UnfoldedIdentifierExpr(name, -1) {
200
276
            }
201
277
            
202
278
            void analyze(AnalysisContext& context) override;
203
 
            int evaluate(const EvaluationContext& context) const override;
 
279
            int evaluate(const EvaluationContext& context) override;
204
280
            void toString(std::ostream&) const override;
205
281
            Expr::Types type() const override;
206
282
            void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
 
283
            void toBinary(std::ostream&) const override;
207
284
            void incr(ReducingSuccessorGenerator& generator) const override;
208
285
            void decr(ReducingSuccessorGenerator& generator) const override;
209
286
            int formulaSize() const override{
218
295
                return _name;
219
296
            }
220
297
            Member constraint(SimplificationContext& context) const override;
 
298
#ifdef ENABLE_TAR
 
299
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
 
300
#endif
221
301
            bool placeFree() const override { return false; }
222
302
        private:
223
303
            /** Offset in marking, -1 if undefined, should be resolved during analysis */
226
306
            std::string _name;
227
307
        };
228
308
        
229
 
        /******************** TEMPORAL OPERATORS ********************/
 
309
        /* Not condition */
 
310
        class NotCondition : public Condition {
 
311
        public:
230
312
 
 
313
            NotCondition(const Condition_ptr cond) {
 
314
                _cond = cond;
 
315
                _temporal = _cond->isTemporal();
 
316
                _loop_sensitive = _cond->isLoopSensitive();
 
317
            }
 
318
            int formulaSize() const override{
 
319
                return _cond->formulaSize() + 1;
 
320
            }
 
321
            void analyze(AnalysisContext& context) override;
 
322
            Result evaluate(const EvaluationContext& context) override;
 
323
            Result evalAndSet(const EvaluationContext& context) override;
 
324
            uint32_t distance(DistanceContext& context) const override;
 
325
            void toString(std::ostream&) const override;
 
326
            void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
 
327
            Retval simplify(SimplificationContext& context) const override;
 
328
            bool isReachability(uint32_t depth) const override;
 
329
            Condition_ptr prepareForReachability(bool negated) const override;
 
330
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
331
            void toXML(std::ostream&, uint32_t tabs) const override;
 
332
            void toBinary(std::ostream&) const override;
 
333
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
 
334
            Quantifier getQuantifier() const override { return Quantifier::NEG; }
 
335
            Path getPath() const override { return Path::pError; }
 
336
            CTLType getQueryType() const override { return CTLType::LOPERATOR; }
 
337
            const Condition_ptr& operator[](size_t i) const { return _cond; };
 
338
            virtual bool isTemporal() const override { return _temporal;}
 
339
            bool containsNext() const override { return _cond->containsNext(); }
 
340
#ifdef ENABLE_TAR
 
341
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
 
342
#endif
 
343
        private:
 
344
            Condition_ptr _cond;
 
345
            bool _temporal = false;
 
346
        };
 
347
        
 
348
        
 
349
        /******************** TEMPORAL OPERATORS ********************/        
 
350
        
231
351
        class QuantifierCondition : public Condition
232
352
        {
233
353
        public:
240
360
        public:
241
361
            SimpleQuantifierCondition(const Condition_ptr cond) {
242
362
                _cond = cond;
 
363
                _loop_sensitive = cond->isLoopSensitive();
243
364
            }
244
365
            int formulaSize() const override{
245
366
                return _cond->formulaSize() + 1;
246
367
            }
247
368
            
248
369
            void analyze(AnalysisContext& context) override;
249
 
            Result evaluate(const EvaluationContext& context) const override;
 
370
            Result evaluate(const EvaluationContext& context) override;
250
371
            Result evalAndSet(const EvaluationContext& context) override;
251
372
            void toString(std::ostream&) const override;
252
373
            void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
253
 
            bool isUpperBound() override;
 
374
            void toBinary(std::ostream& out) const override;
254
375
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
255
376
            virtual const Condition_ptr& operator[] (size_t i) const override { return _cond;}
256
377
            virtual bool containsNext() const override { return _cond->containsNext(); }
 
378
#ifdef ENABLE_TAR
 
379
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const
 
380
            {
 
381
                return _cond->encodeSat(net, context, uses, incremented);
 
382
            }
 
383
#endif
257
384
        private:
258
385
            virtual std::string op() const = 0;
259
386
            
267
394
            Retval simplify(SimplificationContext& context) const override;
268
395
            bool isReachability(uint32_t depth) const override;
269
396
            Condition_ptr prepareForReachability(bool negated) const override;
270
 
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated) const override;
 
397
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
271
398
            void toXML(std::ostream&, uint32_t tabs) const override;
272
399
            Quantifier getQuantifier() const override { return Quantifier::E; }
273
400
            Path getPath() const override             { return Path::X; }
274
401
            uint32_t distance(DistanceContext& context) const override;
275
402
            bool containsNext() const override { return true; }            
 
403
            virtual bool isLoopSensitive() const override { return true; }
276
404
        private:
277
405
            std::string op() const override;
278
406
        };
284
412
            Retval simplify(SimplificationContext& context) const override;
285
413
            bool isReachability(uint32_t depth) const override;
286
414
            Condition_ptr prepareForReachability(bool negated) const override;
287
 
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated) const override;
 
415
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
288
416
            void toXML(std::ostream&, uint32_t tabs) const override;
289
417
            Quantifier getQuantifier() const override { return Quantifier::E; }
290
418
            Path getPath() const override             { return Path::G; }            
291
419
            uint32_t distance(DistanceContext& context) const override;
292
 
            Result evaluate(const EvaluationContext& context) const override;
 
420
            Result evaluate(const EvaluationContext& context) override;
293
421
            Result evalAndSet(const EvaluationContext& context) override;
 
422
            virtual bool isLoopSensitive() const override { return true; }
294
423
        private:
295
424
            std::string op() const override;
296
425
        };
302
431
            Retval simplify(SimplificationContext& context) const override;
303
432
            bool isReachability(uint32_t depth) const override;
304
433
            Condition_ptr prepareForReachability(bool negated) const override;
305
 
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated) const override;
 
434
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
306
435
            void toXML(std::ostream&, uint32_t tabs) const override;
307
436
            Quantifier getQuantifier() const override { return Quantifier::E; }
308
437
            Path getPath() const override             { return Path::F; }            
309
438
            uint32_t distance(DistanceContext& context) const override;
310
 
            Result evaluate(const EvaluationContext& context) const override;
 
439
            Result evaluate(const EvaluationContext& context) override;
311
440
            Result evalAndSet(const EvaluationContext& context) override;
312
441
        private:
313
442
            std::string op() const override;
319
448
            Retval simplify(SimplificationContext& context) const override;
320
449
            bool isReachability(uint32_t depth) const override;
321
450
            Condition_ptr prepareForReachability(bool negated) const override;
322
 
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated) const override;
 
451
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
323
452
            void toXML(std::ostream&, uint32_t tabs) const override;
324
453
            Quantifier getQuantifier() const override { return Quantifier::A; }
325
454
            Path getPath() const override             { return Path::X; }
326
455
            uint32_t distance(DistanceContext& context) const override;
327
456
            bool containsNext() const override { return true; }
 
457
            virtual bool isLoopSensitive() const override { return true; }
328
458
        private:
329
459
            std::string op() const override;
330
460
        };
335
465
            Retval simplify(SimplificationContext& context) const override;
336
466
            bool isReachability(uint32_t depth) const override;
337
467
            Condition_ptr prepareForReachability(bool negated) const override;
338
 
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated) const override;
 
468
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
339
469
            void toXML(std::ostream&, uint32_t tabs) const override;
340
470
            Quantifier getQuantifier() const override { return Quantifier::A; }
341
471
            Path getPath() const override             { return Path::G; } 
342
472
            uint32_t distance(DistanceContext& context) const override;
343
 
            Result evaluate(const EvaluationContext& context) const override;
 
473
            Result evaluate(const EvaluationContext& context) override;
344
474
            Result evalAndSet(const EvaluationContext& context) override;
345
475
        private:
346
476
            std::string op() const override;
352
482
            Retval simplify(SimplificationContext& context) const override;
353
483
            bool isReachability(uint32_t depth) const override;
354
484
            Condition_ptr prepareForReachability(bool negated) const override;
355
 
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated) const override;
 
485
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
356
486
            void toXML(std::ostream&, uint32_t tabs) const override;
357
487
            Quantifier getQuantifier() const override { return Quantifier::A; }
358
488
            Path getPath() const override             { return Path::F; }            
359
489
            uint32_t distance(DistanceContext& context) const override;
360
 
            Result evaluate(const EvaluationContext& context) const override;
 
490
            Result evaluate(const EvaluationContext& context) override;
361
491
            Result evalAndSet(const EvaluationContext& context) override;
 
492
            virtual bool isLoopSensitive() const override { return true; }
362
493
        private:
363
494
            std::string op() const override;
364
495
        };     
368
499
            UntilCondition(const Condition_ptr cond1, const Condition_ptr cond2) {
369
500
                _cond1 = cond1;
370
501
                _cond2 = cond2;
 
502
                _loop_sensitive = _cond1->isLoopSensitive() || _cond2->isLoopSensitive();
371
503
            }
372
504
            int formulaSize() const override{
373
505
                return _cond1->formulaSize() + _cond2->formulaSize() + 1;
374
506
            }
375
507
            
376
508
            void analyze(AnalysisContext& context) override;
377
 
            Result evaluate(const EvaluationContext& context) const override;
 
509
            Result evaluate(const EvaluationContext& context) override;
 
510
#ifdef ENABLE_TAR
 
511
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const
 
512
            {
 
513
                return context.bool_val(true);
 
514
            }
 
515
#endif
378
516
            void toString(std::ostream&) const override;
379
517
            void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
 
518
            void toBinary(std::ostream& out) const override;            
380
519
            bool isReachability(uint32_t depth) const override;
381
 
            bool isUpperBound() override;
382
520
            Condition_ptr prepareForReachability(bool negated) const override;
383
521
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
384
522
            Result evalAndSet(const EvaluationContext& context) override;
401
539
            Retval simplify(SimplificationContext& context) const override;
402
540
            Quantifier getQuantifier() const override { return Quantifier::E; }
403
541
            uint32_t distance(DistanceContext& context) const override;
404
 
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated) const override;
 
542
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
405
543
            void toXML(std::ostream&, uint32_t tabs) const override;
406
544
            
407
545
        private:
415
553
            Quantifier getQuantifier() const override { return Quantifier::A; }            
416
554
            uint32_t distance(DistanceContext& context) const override;
417
555
            void toXML(std::ostream&, uint32_t tabs) const override;
418
 
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated) const override;
419
 
            
 
556
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
557
            virtual bool isLoopSensitive() const override { return true; }
420
558
        private:
421
559
            std::string op() const override;
422
560
        };
423
561
        
424
562
        /******************** CONDITIONS ********************/
425
563
 
426
 
                /* Fireable Condition -- placeholder, needs to be unfolded */
427
 
        class FireableCondition : public Condition {
 
564
 
 
565
        class ExpandableCondition : public Condition {
428
566
        public:
429
 
            FireableCondition(const std::string& tname) : _name(tname) {};
430
 
            void analyze(AnalysisContext& context) override;
431
 
            Result evaluate(const EvaluationContext& context) const override
 
567
            ExpandableCondition(const std::string& tname) : _name(tname) {};
 
568
            Result evaluate(const EvaluationContext& context) override
432
569
            { return _compiled->evaluate(context); }
433
570
            Result evalAndSet(const EvaluationContext& context) override
434
571
            { return _compiled->evalAndSet(context); }
435
572
            uint32_t distance(DistanceContext& context) const override
436
573
            { return _compiled->distance(context); }
437
574
            void toString(std::ostream& ss) const override
438
 
            { _compiled->toString(ss); } 
 
575
            { 
 
576
                if(_compiled) _compiled->toString(ss); 
 
577
                else ss << _name;
 
578
            } 
439
579
            void toTAPAALQuery(std::ostream& s,TAPAALConditionExportContext& context) const override
440
580
            { _compiled->toTAPAALQuery(s, context); }
 
581
            void toBinary(std::ostream& out) const override
 
582
            { _compiled->toBinary(out); }
 
583
 
441
584
            Retval simplify(SimplificationContext& context) const override
442
585
            { 
443
586
                return _compiled->simplify(context); 
444
587
            }
445
588
            bool isReachability(uint32_t depth) const override
446
 
            { return _compiled->isReachability(depth); }
447
 
            bool isUpperBound() override
448
 
            { return false; }
449
 
            Condition_ptr prepareForReachability(bool negated) const override
450
 
            { return _compiled->prepareForReachability(negated); }
451
 
            Condition_ptr pushNegation(negstat_t& stat, const EvaluationContext& context, bool nested, bool negated) const override 
452
 
            { 
453
 
                return _compiled->pushNegation(stat, context, nested, negated); 
454
 
            }
 
589
            { return true;}
 
590
 
455
591
            void toXML(std::ostream& ss, uint32_t tabs) const override 
456
592
            { _compiled->toXML(ss, tabs);};
457
593
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override 
458
594
            { _compiled->findInteresting(generator, negated); }
459
595
            Quantifier getQuantifier() const override 
460
 
            { return _compiled->getQuantifier(); }
 
596
            { 
 
597
                if(_compiled) return _compiled->getQuantifier(); 
 
598
                else          return Quantifier::AND;
 
599
            }
461
600
            Path getPath() const override 
462
601
            { return _compiled->getPath(); }
463
602
            CTLType getQueryType() const override 
466
605
            { return _compiled->formulaSize(); }
467
606
            bool containsNext() const override
468
607
            { return false; }
 
608
#ifdef ENABLE_TAR
 
609
            z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const override
 
610
            {
 
611
                assert(false);
 
612
                return context.bool_val(false);
 
613
            }
 
614
#endif
469
615
 
470
 
        private:
 
616
        protected:
471
617
            std::string _name;
472
618
            Condition_ptr _compiled;
473
619
        };
474
 
        
475
 
        
 
620
 
 
621
        /* Fireable Condition -- placeholder, needs to be unfolded */
 
622
        class UnfoldedFireableCondition : public ExpandableCondition {
 
623
        public:
 
624
            UnfoldedFireableCondition(const std::string& tname) : ExpandableCondition(tname) {};
 
625
            void analyze(AnalysisContext& context) override;
 
626
            Condition_ptr pushNegation(negstat_t& stat, const EvaluationContext& context, bool nested, bool negated, bool initrw) override 
 
627
            { 
 
628
                if(_compiled)
 
629
                    return _compiled->pushNegation(stat, context, nested, negated, initrw); 
 
630
                if(negated)
 
631
                {
 
632
                    stat.negated_fireability = true;
 
633
                    return std::make_shared<NotCondition>(std::make_shared<UnfoldedFireableCondition>(_name));
 
634
                }
 
635
                else
 
636
                    return std::make_shared<UnfoldedFireableCondition>(_name);
 
637
            }
 
638
 
 
639
            Condition_ptr prepareForReachability(bool negated) const override
 
640
            { 
 
641
                if(_compiled) return _compiled->prepareForReachability(negated); 
 
642
                return std::make_shared<UnfoldedFireableCondition>(_name);
 
643
            }
 
644
 
 
645
        };
 
646
 
 
647
        class FireableCondition : public ExpandableCondition {
 
648
        public:
 
649
            FireableCondition(const std::string& tname) : ExpandableCondition(tname) {};
 
650
            void analyze(AnalysisContext& context) override;
 
651
            Condition_ptr pushNegation(negstat_t& stat, const EvaluationContext& context, bool nested, bool negated, bool initrw) override 
 
652
            { 
 
653
                if(_compiled)
 
654
                    return _compiled->pushNegation(stat, context, nested, negated, initrw); 
 
655
                if(negated)
 
656
                {
 
657
                    stat.negated_fireability = true;
 
658
                    return std::make_shared<NotCondition>(std::make_shared<FireableCondition>(_name));
 
659
                }
 
660
                else
 
661
                    return std::make_shared<FireableCondition>(_name);
 
662
            }
 
663
 
 
664
            Condition_ptr prepareForReachability(bool negated) const override
 
665
            { 
 
666
                if(_compiled) return _compiled->prepareForReachability(negated); 
 
667
                return std::make_shared<FireableCondition>(_name);
 
668
            }
 
669
        };
 
670
 
476
671
        
477
672
        /* Logical conditon */
478
673
        class LogicalCondition : public Condition {
486
681
            
487
682
            uint32_t distance(DistanceContext& context) const override;
488
683
            void toString(std::ostream&) const override;
 
684
            void toBinary(std::ostream& out) const override;
489
685
            void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
490
686
            bool isReachability(uint32_t depth) const override;
491
 
            bool isUpperBound() override;
492
687
            Condition_ptr prepareForReachability(bool negated) const override;
493
688
            const Condition_ptr& operator[](size_t i) const
494
689
            { 
534
729
            AndCondition(Condition_ptr left, Condition_ptr right);
535
730
            
536
731
            Retval simplify(SimplificationContext& context) const override;
537
 
            Result evaluate(const EvaluationContext& context) const override;
 
732
            Result evaluate(const EvaluationContext& context) override;
538
733
            Result evalAndSet(const EvaluationContext& context) override;
539
734
 
540
735
            void toXML(std::ostream&, uint32_t tabs) const override;
541
736
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
542
737
            Quantifier getQuantifier() const override { return Quantifier::AND; }
543
 
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated) const override;
544
 
 
 
738
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
739
#ifdef ENABLE_TAR
 
740
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
 
741
#endif
545
742
        private:
546
743
            //int logicalOp() const;
547
744
            uint32_t delta(uint32_t d1, uint32_t d2, const DistanceContext& context) const override;
559
756
            OrCondition(Condition_ptr left, Condition_ptr right);
560
757
            
561
758
            Retval simplify(SimplificationContext& context) const override;
562
 
            Result evaluate(const EvaluationContext& context) const override;
 
759
            Result evaluate(const EvaluationContext& context) override;
563
760
            Result evalAndSet(const EvaluationContext& context) override;
564
761
 
565
762
            void toXML(std::ostream&, uint32_t tabs) const override;
566
763
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;   
567
764
            Quantifier getQuantifier() const override { return Quantifier::OR; }
568
 
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated) const override;
 
765
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
766
#ifdef ENABLE_TAR
 
767
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
 
768
#endif
569
769
        private:
570
770
            //int logicalOp() const;
571
771
            uint32_t delta(uint32_t d1, uint32_t d2, const DistanceContext& context) const override;
574
774
 
575
775
        class CompareConjunction : public Condition
576
776
        {
577
 
        private:
 
777
        public:
578
778
            struct cons_t {
579
779
                int32_t _place  = -1;
580
780
                uint32_t _upper = std::numeric_limits<uint32_t>::max();
586
786
                }
587
787
            };
588
788
 
589
 
 
590
 
        public:
591
789
            CompareConjunction(bool negated = false) 
592
790
                    : _negated(false) {};
593
791
            friend FireableCondition;
620
818
            uint32_t distance(DistanceContext& context) const override;
621
819
            void toString(std::ostream& stream) const override;
622
820
            void toTAPAALQuery(std::ostream& stream,TAPAALConditionExportContext& context) const override;
 
821
            void toBinary(std::ostream& out) const override;
623
822
            bool isReachability(uint32_t depth) const override { return depth > 0; };
624
 
            bool isUpperBound() override { return false; }
625
823
            Condition_ptr prepareForReachability(bool negated) const override;
626
824
            CTLType getQueryType() const override { return CTLType::LOPERATOR; }
627
825
            Path getPath() const override         { return Path::pError; }            
628
826
            virtual void toXML(std::ostream& stream, uint32_t tabs) const override;
629
827
            Retval simplify(SimplificationContext& context) const override;
630
 
            Result evaluate(const EvaluationContext& context) const override;
 
828
            Result evaluate(const EvaluationContext& context) override;
631
829
            Result evalAndSet(const EvaluationContext& context) override;
632
830
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;   
633
831
            Quantifier getQuantifier() const override { return _negated ? Quantifier::OR : Quantifier::AND; }
634
 
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated) const override;
 
832
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
635
833
            bool isNegated() const { return _negated; }
636
834
            bool singular() const 
637
835
            { 
640
838
                                     _constraints[0]._upper == std::numeric_limits<uint32_t>::max());
641
839
            };
642
840
            bool containsNext() const override { return false;}
643
 
 
 
841
#ifdef ENABLE_TAR
 
842
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
 
843
#endif
644
844
        private:
645
845
            std::vector<cons_t> _constraints;
646
846
            bool _negated = false;
659
859
                return _expr1->formulaSize() + _expr2->formulaSize() + 1;
660
860
            }
661
861
            void analyze(AnalysisContext& context) override;
662
 
            Result evaluate(const EvaluationContext& context) const override;
 
862
            Result evaluate(const EvaluationContext& context) override;
663
863
            Result evalAndSet(const EvaluationContext& context) override;
664
864
            void toString(std::ostream&) const override;
665
865
            void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
 
866
            void toBinary(std::ostream& out) const override;
666
867
            bool isReachability(uint32_t depth) const override;
667
 
            bool isUpperBound() override;
668
868
            Condition_ptr prepareForReachability(bool negated) const override;
669
869
            Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
670
870
            Path getPath() const override { return Path::pError; }
708
908
            void toXML(std::ostream&, uint32_t tabs) const override;
709
909
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
710
910
            uint32_t distance(DistanceContext& context) const override;
711
 
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated) const override;
712
 
 
 
911
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
912
#ifdef ENABLE_TAR
 
913
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
 
914
#endif
713
915
        private:
714
916
            bool apply(int v1, int v2) const override;
715
917
            std::string op() const override;
727
929
            void toXML(std::ostream&, uint32_t tabs) const override;
728
930
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
729
931
            uint32_t distance(DistanceContext& context) const override;
730
 
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated) const override;
731
 
 
 
932
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
933
#ifdef ENABLE_TAR
 
934
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
 
935
#endif
732
936
        private:
733
937
            bool apply(int v1, int v2) const override;
734
938
            std::string op() const override;
745
949
            void toXML(std::ostream&, uint32_t tabs) const override;
746
950
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
747
951
            uint32_t distance(DistanceContext& context) const override;
748
 
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated) const override;
 
952
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
953
#ifdef ENABLE_TAR
 
954
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
 
955
#endif
749
956
        private:
750
957
            bool apply(int v1, int v2) const override;
751
958
            std::string op() const override;
762
969
            void toXML(std::ostream&, uint32_t tabs) const override;
763
970
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
764
971
            uint32_t distance(DistanceContext& context) const override;
765
 
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated) const override;
766
 
 
 
972
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
973
#ifdef ENABLE_TAR
 
974
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
 
975
#endif
767
976
        private:
768
977
            bool apply(int v1, int v2) const override;
769
978
            std::string op() const override;
780
989
            void toXML(std::ostream&, uint32_t tabs) const override;
781
990
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
782
991
            uint32_t distance(DistanceContext& context) const override;
783
 
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated) const override;
784
 
 
 
992
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
993
#ifdef ENABLE_TAR
 
994
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
 
995
#endif
785
996
        private:
786
997
            bool apply(int v1, int v2) const override;
787
998
            std::string op() const override;
797
1008
            void toXML(std::ostream&, uint32_t tabs) const override;
798
1009
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
799
1010
            uint32_t distance(DistanceContext& context) const override;
800
 
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated) const override;
801
 
 
 
1011
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
1012
#ifdef ENABLE_TAR
 
1013
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
 
1014
#endif
802
1015
        private:
803
1016
            bool apply(int v1, int v2) const override;
804
1017
            std::string op() const override;
806
1019
            std::string sopTAPAAL() const override;
807
1020
        };
808
1021
 
809
 
        /* Not condition */
810
 
        class NotCondition : public Condition {
811
 
        public:
812
 
 
813
 
            NotCondition(const Condition_ptr cond) {
814
 
                _cond = cond;
815
 
                _temporal = _cond->isTemporal();
816
 
            }
817
 
            int formulaSize() const override{
818
 
                return _cond->formulaSize() + 1;
819
 
            }
820
 
            void analyze(AnalysisContext& context) override;
821
 
            Result evaluate(const EvaluationContext& context) const override;
822
 
            Result evalAndSet(const EvaluationContext& context) override;
823
 
            uint32_t distance(DistanceContext& context) const override;
824
 
            void toString(std::ostream&) const override;
825
 
            void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
826
 
            Retval simplify(SimplificationContext& context) const override;
827
 
            bool isReachability(uint32_t depth) const override;
828
 
            bool isUpperBound() override;
829
 
            Condition_ptr prepareForReachability(bool negated) const override;
830
 
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated) const override;
831
 
            void toXML(std::ostream&, uint32_t tabs) const override;
832
 
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
833
 
            Quantifier getQuantifier() const override { return Quantifier::NEG; }
834
 
            Path getPath() const override { return Path::pError; }
835
 
            CTLType getQueryType() const override { return CTLType::LOPERATOR; }
836
 
            const Condition_ptr& operator[](size_t i) const { return _cond; };
837
 
            virtual bool isTemporal() const override { return _temporal;}
838
 
            bool containsNext() const override { return _cond->containsNext(); }
839
 
 
840
 
        private:
841
 
            Condition_ptr _cond;
842
 
            bool _temporal = false;
843
 
        };
844
 
 
845
1022
        /* Bool condition */
846
1023
        class BooleanCondition : public Condition {
847
1024
        public:
857
1034
                return 0;
858
1035
            }
859
1036
            void analyze(AnalysisContext& context) override;
860
 
            Result evaluate(const EvaluationContext& context) const override;
 
1037
            Result evaluate(const EvaluationContext& context) override;
861
1038
            Result evalAndSet(const EvaluationContext& context) override;
862
1039
            uint32_t distance(DistanceContext& context) const override;
863
1040
            static Condition_ptr TRUE_CONSTANT;
867
1044
            static Condition_ptr getShared(bool val);
868
1045
            Retval simplify(SimplificationContext& context) const override;
869
1046
            bool isReachability(uint32_t depth) const override;
870
 
            bool isUpperBound() override;
871
1047
            Condition_ptr prepareForReachability(bool negated) const override;
872
 
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated) const override;
 
1048
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
873
1049
            void toXML(std::ostream&, uint32_t tabs) const override;
 
1050
            void toBinary(std::ostream&) const override;
874
1051
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
875
1052
            Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
876
1053
            Path getPath() const override { return Path::pError; }
877
1054
            CTLType getQueryType() const override { return CTLType::EVAL; }
878
1055
            bool containsNext() const override { return false; }
 
1056
#ifdef ENABLE_TAR
 
1057
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const
 
1058
            {
 
1059
                return context.bool_val(_value);
 
1060
            }
 
1061
#endif
879
1062
        private:
880
1063
            const bool _value;
881
1064
        };
885
1068
        public:
886
1069
 
887
1070
            DeadlockCondition() {
 
1071
                _loop_sensitive = true;
888
1072
            }
889
1073
            int formulaSize() const override{
890
1074
                return 1;
891
1075
            }
892
1076
            void analyze(AnalysisContext& context) override;
893
 
            Result evaluate(const EvaluationContext& context) const override;
 
1077
            Result evaluate(const EvaluationContext& context) override;
894
1078
            Result evalAndSet(const EvaluationContext& context) override;
895
1079
            uint32_t distance(DistanceContext& context) const override;
896
1080
            void toString(std::ostream&) const override;
897
1081
            void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
898
1082
            Retval simplify(SimplificationContext& context) const override;
899
1083
            bool isReachability(uint32_t depth) const override;
900
 
            bool isUpperBound() override;
901
1084
            Condition_ptr prepareForReachability(bool negated) const override;
902
 
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated) const override;
 
1085
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
903
1086
            void toXML(std::ostream&, uint32_t tabs) const override;
 
1087
            void toBinary(std::ostream&) const override;
904
1088
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
905
1089
            static Condition_ptr DEADLOCK;
906
1090
            Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
907
1091
            Path getPath() const override { return Path::pError; }
908
1092
            CTLType getQueryType() const override { return CTLType::EVAL; }
909
1093
            bool containsNext() const override { return false; }
 
1094
#ifdef ENABLE_TAR
 
1095
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
 
1096
#endif
 
1097
        };
 
1098
 
 
1099
        class UpperBoundsCondition : public Condition
 
1100
        {
 
1101
        public:
 
1102
            
 
1103
            UpperBoundsCondition(const std::vector<std::string>& places) : _places(places)
 
1104
            {
 
1105
            }
 
1106
 
 
1107
            int formulaSize() const override{
 
1108
                return _places.size();
 
1109
            }
 
1110
            void analyze(AnalysisContext& context) override;
 
1111
            Result evaluate(const EvaluationContext& context) override
 
1112
            { return _compiled->evaluate(context); }
 
1113
            Result evalAndSet(const EvaluationContext& context) override
 
1114
            { return _compiled->evalAndSet(context); }
 
1115
            uint32_t distance(DistanceContext& context) const override
 
1116
            { return _compiled->distance(context); }
 
1117
            void toString(std::ostream& out) const override;
 
1118
            void toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const override
 
1119
            { _compiled->toTAPAALQuery(out, context); }
 
1120
            void toBinary(std::ostream& out) const override
 
1121
            { return _compiled->toBinary(out); }
 
1122
            Retval simplify(SimplificationContext& context) const override
 
1123
            { return _compiled->simplify(context); }
 
1124
            bool isReachability(uint32_t depth) const override
 
1125
            { return true; }
 
1126
            Condition_ptr prepareForReachability(bool negated) const override
 
1127
            { return _compiled->prepareForReachability(negated); }
 
1128
            Condition_ptr pushNegation(negstat_t& neg, const EvaluationContext& context, bool nested, bool negated, bool initrw) override
 
1129
            { 
 
1130
                if(_compiled)
 
1131
                    return _compiled->pushNegation(neg, context, nested, negated, initrw); 
 
1132
                else
 
1133
                    return std::make_shared<UpperBoundsCondition>(_places);
 
1134
            }
 
1135
            void toXML(std::ostream& out, uint32_t tabs) const override
 
1136
            { _compiled->toXML(out, tabs); }
 
1137
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override
 
1138
            { _compiled->findInteresting(generator, negated);}
 
1139
            Quantifier getQuantifier() const override { return Quantifier::UPPERBOUNDS; }
 
1140
            Path getPath() const override { return Path::pError; }
 
1141
            CTLType getQueryType() const override { return CTLType::EVAL; }
 
1142
            bool containsNext() const override { return false; }
 
1143
#ifdef ENABLE_TAR
 
1144
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const 
 
1145
            { return _compiled->encodeSat(net, context, uses, incremented); }
 
1146
#endif
 
1147
        private:
 
1148
            std::vector<std::string> _places;
 
1149
            Condition_ptr _compiled;
 
1150
 
 
1151
        };
 
1152
        
 
1153
        class UnfoldedUpperBoundsCondition : public Condition
 
1154
        {
 
1155
        public:
 
1156
            struct place_t {
 
1157
                std::string _name;
 
1158
                uint32_t _place = 0;
 
1159
                place_t(const std::string& name)
 
1160
                {
 
1161
                    _name = name;
 
1162
                }
 
1163
                bool operator<(const place_t& other) const{
 
1164
                    return _place < other._place;
 
1165
                }
 
1166
            };
 
1167
            
 
1168
            UnfoldedUpperBoundsCondition(const std::vector<std::string>& places)
 
1169
            {
 
1170
                for(auto& s : places) _places.push_back(s);
 
1171
            }
 
1172
            UnfoldedUpperBoundsCondition(const std::vector<place_t>& places, size_t max)
 
1173
                    : _places(places), _max(max) {
 
1174
            };
 
1175
            int formulaSize() const override{
 
1176
                return _places.size();
 
1177
            }
 
1178
            void analyze(AnalysisContext& context) override;
 
1179
            Result evaluate(const EvaluationContext& context) override;
 
1180
            Result evalAndSet(const EvaluationContext& context) override;
 
1181
            uint32_t distance(DistanceContext& context) const override;
 
1182
            void toString(std::ostream&) const override;
 
1183
            void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
 
1184
            void toBinary(std::ostream&) const override;
 
1185
            Retval simplify(SimplificationContext& context) const override;
 
1186
            bool isReachability(uint32_t depth) const override;
 
1187
            Condition_ptr prepareForReachability(bool negated) const override;
 
1188
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
1189
            void toXML(std::ostream&, uint32_t tabs) const override;
 
1190
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
 
1191
            Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
 
1192
            Path getPath() const override { return Path::pError; }
 
1193
            CTLType getQueryType() const override { return CTLType::EVAL; }
 
1194
            bool containsNext() const override { return false; }
 
1195
            size_t bounds() const { return _bound; }
 
1196
#ifdef ENABLE_TAR
 
1197
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
 
1198
#endif
 
1199
            virtual void setUpperBound(size_t bound)
 
1200
            {
 
1201
                _bound = std::max(_bound, bound);
 
1202
            }
 
1203
        private:
 
1204
            std::vector<place_t> _places;
 
1205
            size_t _bound = 0;
 
1206
            size_t _max = std::numeric_limits<size_t>::max();
 
1207
 
910
1208
        };
911
1209
 
912
1210
    }