← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to include/PetriEngine/PQL/Expressions.h

  • 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:
include/PetriEngine/PQL/Expressions.h
 
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
#ifndef EXPRESSIONS_H
 
21
#define EXPRESSIONS_H
 
22
 
 
23
 
 
24
#include <iostream>
 
25
#include <fstream>
 
26
#include <algorithm>
 
27
#include "PQL.h"
 
28
#include "Contexts.h"
 
29
#include "..//Simplification/Member.h"
 
30
#include "../Simplification/LinearPrograms.h"
 
31
#include "../Simplification/Retval.h"
 
32
 
 
33
using namespace PetriEngine::Simplification;
 
34
 
 
35
namespace PetriEngine {
 
36
    namespace PQL {
 
37
        
 
38
        std::string generateTabs(uint32_t tabs);
 
39
        class CompareCondition;
 
40
        class NotCondition;
 
41
        /******************** EXPRESSIONS ********************/
 
42
 
 
43
        /** Base class for all binary expressions */
 
44
        class NaryExpr : public Expr {
 
45
        protected:
 
46
            NaryExpr() {};
 
47
        public:
 
48
 
 
49
            NaryExpr(std::vector<Expr_ptr>&& exprs) : _exprs(std::move(exprs)) {
 
50
            }
 
51
            virtual void analyze(AnalysisContext& context) override;
 
52
            int evaluate(const EvaluationContext& context) override;
 
53
            int formulaSize() const override{
 
54
                size_t sum = 0;
 
55
                for(auto& e : _exprs) sum += e->formulaSize();
 
56
                return sum + 1;
 
57
            }
 
58
            void toString(std::ostream&) const override;
 
59
            bool placeFree() const override;
 
60
            auto& expressions() const { return _exprs; }
 
61
        protected:
 
62
            virtual int apply(int v1, int v2) const = 0;
 
63
            virtual std::string op() const = 0;
 
64
            std::vector<Expr_ptr> _exprs;
 
65
            virtual int32_t preOp(const EvaluationContext& context) const;
 
66
        };
 
67
        
 
68
        class PlusExpr;
 
69
        class MultiplyExpr;
 
70
        
 
71
        class CommutativeExpr : public NaryExpr
 
72
        {
 
73
        public:
 
74
            friend CompareCondition;
 
75
            virtual void analyze(AnalysisContext& context) override;
 
76
            int evaluate(const EvaluationContext& context) override;
 
77
            void toBinary(std::ostream&) const override;
 
78
            int formulaSize() const override{
 
79
                size_t sum = _ids.size();
 
80
                for(auto& e : _exprs) sum += e->formulaSize();
 
81
                return sum + 1;
 
82
            }
 
83
            void toString(std::ostream&) const override;            
 
84
            bool placeFree() const override;
 
85
            auto constant() const { return _constant; }
 
86
            auto& places() const { return _ids; }
 
87
        protected:
 
88
            CommutativeExpr(int constant): _constant(constant) {};
 
89
            void init(std::vector<Expr_ptr>&& exprs);
 
90
            virtual int32_t preOp(const EvaluationContext& context) const override;
 
91
            int32_t _constant;
 
92
            std::vector<std::pair<uint32_t,std::string>> _ids;
 
93
            Member commutativeCons(int constant, SimplificationContext& context, std::function<void(Member& a, Member b)> op) const;
 
94
        };
 
95
 
 
96
        /** Binary plus expression */
 
97
        class PlusExpr : public CommutativeExpr {
 
98
        public:
 
99
 
 
100
            PlusExpr(std::vector<Expr_ptr>&& exprs, bool tk = false);
 
101
            
 
102
            Expr::Types type() const override;
 
103
            Member constraint(SimplificationContext& context) const override;
 
104
            void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
 
105
            bool tk = false;
 
106
            void incr(ReducingSuccessorGenerator& generator) const override;
 
107
            void decr(ReducingSuccessorGenerator& generator) const override;
 
108
            void visit(Visitor& visitor) const override;
 
109
        protected:
 
110
            int apply(int v1, int v2) const override;
 
111
            //int binaryOp() const;
 
112
            std::string op() const override;
 
113
        };
 
114
 
 
115
        /** Binary minus expression */
 
116
        class SubtractExpr : public NaryExpr {
 
117
        public:
 
118
 
 
119
            SubtractExpr(std::vector<Expr_ptr>&& exprs) : NaryExpr(std::move(exprs))
 
120
            {
 
121
            }
 
122
            Expr::Types type() const override;
 
123
            Member constraint(SimplificationContext& context) const override;
 
124
            void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
 
125
            void incr(ReducingSuccessorGenerator& generator) const override;
 
126
            void decr(ReducingSuccessorGenerator& generator) const override;
 
127
            void toBinary(std::ostream&) const override;
 
128
            void visit(Visitor& visitor) const override;
 
129
        protected:
 
130
            int apply(int v1, int v2) const override;
 
131
            //int binaryOp() const;
 
132
            std::string op() const override;
 
133
        };
 
134
 
 
135
        /** Binary multiplication expression **/
 
136
        class MultiplyExpr : public CommutativeExpr {
 
137
        public:
 
138
 
 
139
            MultiplyExpr(std::vector<Expr_ptr>&& exprs);
 
140
            Expr::Types type() const override;
 
141
            Member constraint(SimplificationContext& context) const override;
 
142
            void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
 
143
            void incr(ReducingSuccessorGenerator& generator) const override;
 
144
            void decr(ReducingSuccessorGenerator& generator) const override;
 
145
            void visit(Visitor& visitor) const override;
 
146
        protected:
 
147
            int apply(int v1, int v2) const override;
 
148
            //int binaryOp() const;
 
149
            std::string op() const override;
 
150
        };
 
151
 
 
152
        /** Unary minus expression*/
 
153
        class MinusExpr : public Expr {
 
154
        public:
 
155
 
 
156
            MinusExpr(const Expr_ptr expr) {
 
157
                _expr = expr;
 
158
            }
 
159
            void analyze(AnalysisContext& context) override;
 
160
            int evaluate(const EvaluationContext& context) override;
 
161
            void toString(std::ostream&) const override;
 
162
            Expr::Types type() const override;
 
163
            Member constraint(SimplificationContext& context) const override;
 
164
            void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
 
165
            void toBinary(std::ostream&) const override;
 
166
            void incr(ReducingSuccessorGenerator& generator) const override;
 
167
            void decr(ReducingSuccessorGenerator& generator) const override;
 
168
            void visit(Visitor& visitor) const override;
 
169
            int formulaSize() const override{
 
170
                return _expr->formulaSize() + 1;
 
171
            }
 
172
            bool placeFree() const override;
 
173
            const Expr_ptr& operator[](size_t i) const { return _expr; };
 
174
        private:
 
175
            Expr_ptr _expr;
 
176
        };
 
177
 
 
178
        /** Literal integer value expression */
 
179
        class LiteralExpr : public Expr {
 
180
        public:
 
181
 
 
182
            LiteralExpr(int value) : _value(value) {
 
183
            }
 
184
            void analyze(AnalysisContext& context) override;
 
185
            int evaluate(const EvaluationContext& context) override;
 
186
            void toString(std::ostream&) const override;
 
187
            Expr::Types type() const override;
 
188
            void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
 
189
            void toBinary(std::ostream&) const override;
 
190
            void incr(ReducingSuccessorGenerator& generator) const override;
 
191
            void decr(ReducingSuccessorGenerator& generator) const override;
 
192
            void visit(Visitor& visitor) const override;
 
193
            int formulaSize() const override{
 
194
                return 1;
 
195
            }
 
196
            int value() const {
 
197
                return _value;
 
198
            };
 
199
            Member constraint(SimplificationContext& context) const override;
 
200
            bool placeFree() const override { return true; }
 
201
        private:
 
202
            int _value;
 
203
        };
 
204
 
 
205
 
 
206
        class IdentifierExpr : public Expr {
 
207
        public:
 
208
            IdentifierExpr(const std::string& name) : _name(name) {}
 
209
            void analyze(AnalysisContext& context) override;
 
210
            int evaluate(const EvaluationContext& context) override {
 
211
                return _compiled->evaluate(context);
 
212
            }
 
213
            void toString(std::ostream& os) const override {
 
214
                if(_compiled)
 
215
                    _compiled->toString(os);
 
216
                else
 
217
                    os << _name;
 
218
            }
 
219
            Expr::Types type() const override {
 
220
                if(_compiled) return _compiled->type();
 
221
                return Expr::IdentifierExpr;
 
222
            }
 
223
            void toXML(std::ostream& os, uint32_t tabs, bool tokencount = false) const override {
 
224
                _compiled->toXML(os, tabs, tokencount);
 
225
            }
 
226
            void incr(ReducingSuccessorGenerator& generator) const override {
 
227
                _compiled->incr(generator);
 
228
            }
 
229
            void decr(ReducingSuccessorGenerator& generator) const override {
 
230
                _compiled->decr(generator);
 
231
            }
 
232
            int formulaSize() const override {
 
233
                if(_compiled) return _compiled->formulaSize();
 
234
                return 1;
 
235
            }
 
236
            virtual bool placeFree() const override {
 
237
                if(_compiled) return _compiled->placeFree();
 
238
                return false;
 
239
            }
 
240
 
 
241
            Member constraint(SimplificationContext& context) const override {
 
242
                return _compiled->constraint(context);
 
243
            }
 
244
            
 
245
            void toBinary(std::ostream& s) const override {
 
246
                _compiled->toBinary(s);
 
247
            }
 
248
            void visit(Visitor& visitor) const override;            
 
249
        private:
 
250
            std::string _name;
 
251
            Expr_ptr _compiled;
 
252
        };
 
253
 
 
254
        /** Identifier expression */
 
255
        class UnfoldedIdentifierExpr : public Expr {
 
256
        public:
 
257
            UnfoldedIdentifierExpr(const std::string& name, int offest)
 
258
            : _offsetInMarking(offest), _name(name) {
 
259
            }
 
260
            
 
261
            UnfoldedIdentifierExpr(const std::string& name) : UnfoldedIdentifierExpr(name, -1) {
 
262
            }
 
263
            
 
264
            void analyze(AnalysisContext& context) override;
 
265
            int evaluate(const EvaluationContext& context) override;
 
266
            void toString(std::ostream&) const override;
 
267
            Expr::Types type() const override;
 
268
            void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
 
269
            void toBinary(std::ostream&) const override;
 
270
            void incr(ReducingSuccessorGenerator& generator) const override;
 
271
            void decr(ReducingSuccessorGenerator& generator) const override;
 
272
            int formulaSize() const override{
 
273
                return 1;
 
274
            }
 
275
            /** Offset in marking or valuation */
 
276
            int offset() const {
 
277
                return _offsetInMarking;
 
278
            }
 
279
            const std::string& name()
 
280
            {
 
281
                return _name;
 
282
            }
 
283
            Member constraint(SimplificationContext& context) const override;
 
284
            bool placeFree() const override { return false; }
 
285
            void visit(Visitor& visitor) const override;
 
286
        private:
 
287
            /** Offset in marking, -1 if undefined, should be resolved during analysis */
 
288
            int _offsetInMarking;
 
289
            /** Identifier text */
 
290
            std::string _name;
 
291
        };
 
292
 
 
293
        class ShallowCondition : public Condition
 
294
        {
 
295
            Result evaluate(const EvaluationContext& context) override
 
296
            { return _compiled->evaluate(context); }
 
297
            Result evalAndSet(const EvaluationContext& context) override
 
298
            { return _compiled->evalAndSet(context); }
 
299
            uint32_t distance(DistanceContext& context) const override
 
300
            { return _compiled->distance(context); }
 
301
            void toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const override
 
302
            { _compiled->toTAPAALQuery(out, context); }
 
303
            void toBinary(std::ostream& out) const override
 
304
            { return _compiled->toBinary(out); }
 
305
            Retval simplify(SimplificationContext& context) const override
 
306
            { return _compiled->simplify(context); }
 
307
            Condition_ptr prepareForReachability(bool negated) const override
 
308
            { return _compiled->prepareForReachability(negated); }
 
309
            bool isReachability(uint32_t depth) const override
 
310
            { return _compiled->isReachability(depth); }
 
311
 
 
312
            void toXML(std::ostream& out, uint32_t tabs) const override
 
313
            { _compiled->toXML(out, tabs); }
 
314
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override
 
315
            { _compiled->findInteresting(generator, negated);}
 
316
            Quantifier getQuantifier() const override
 
317
            { return _compiled->getQuantifier(); }
 
318
            Path getPath() const override { return _compiled->getPath(); }
 
319
            CTLType getQueryType() const override { return _compiled->getQueryType(); }
 
320
            bool containsNext() const override { return _compiled->containsNext(); }
 
321
            bool nestedDeadlock() const override { return _compiled->nestedDeadlock(); }
 
322
#ifdef VERIFYPN_TAR
 
323
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const
 
324
            { return _compiled->encodeSat(net, context, uses, incremented); }
 
325
#endif
 
326
            int formulaSize() const override{
 
327
                return _compiled->formulaSize();
 
328
            }
 
329
 
 
330
            virtual Condition_ptr pushNegation(negstat_t& neg, const EvaluationContext& context, bool nested, bool negated, bool initrw) override
 
331
            {
 
332
                if(_compiled)
 
333
                    return _compiled->pushNegation(neg, context, nested, negated, initrw);
 
334
                else {
 
335
                    if(negated)
 
336
                        return std::static_pointer_cast<Condition>(std::make_shared<NotCondition>(clone()));
 
337
                    else
 
338
                        return clone();
 
339
                }
 
340
            }
 
341
 
 
342
            void analyze(AnalysisContext& context) override
 
343
            {
 
344
                if (_compiled) _compiled->analyze(context);
 
345
                else _analyze(context);
 
346
            }
 
347
            void toString(std::ostream &out) const {
 
348
                if (_compiled) _compiled->toString(out);
 
349
                else _toString(out);
 
350
            }
 
351
 
 
352
        protected:
 
353
            virtual void _analyze(AnalysisContext& context) = 0;
 
354
            virtual void _toString(std::ostream& out) const = 0;
 
355
            virtual Condition_ptr clone() = 0;
 
356
            Condition_ptr _compiled = nullptr;
 
357
        };
 
358
 
 
359
        /* Not condition */
 
360
        class NotCondition : public Condition {
 
361
        public:
 
362
 
 
363
            NotCondition(const Condition_ptr cond) {
 
364
                _cond = cond;
 
365
                _temporal = _cond->isTemporal();
 
366
                _loop_sensitive = _cond->isLoopSensitive();
 
367
            }
 
368
            int formulaSize() const override{
 
369
                return _cond->formulaSize() + 1;
 
370
            }
 
371
            void analyze(AnalysisContext& context) override;
 
372
            Result evaluate(const EvaluationContext& context) override;
 
373
            Result evalAndSet(const EvaluationContext& context) override;
 
374
            void visit(Visitor&) const override;
 
375
            uint32_t distance(DistanceContext& context) const override;
 
376
            void toString(std::ostream&) const override;
 
377
            void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
 
378
            Retval simplify(SimplificationContext& context) const override;
 
379
            bool isReachability(uint32_t depth) const override;
 
380
            Condition_ptr prepareForReachability(bool negated) const override;
 
381
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
382
            void toXML(std::ostream&, uint32_t tabs) const override;
 
383
            void toBinary(std::ostream&) const override;
 
384
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
 
385
            Quantifier getQuantifier() const override { return Quantifier::NEG; }
 
386
            Path getPath() const override { return Path::pError; }
 
387
            CTLType getQueryType() const override { return CTLType::LOPERATOR; }
 
388
            const Condition_ptr& operator[](size_t i) const { return _cond; };
 
389
            virtual bool isTemporal() const override { return _temporal;}
 
390
            bool containsNext() const override { return _cond->containsNext(); }
 
391
            bool nestedDeadlock() const override { return _cond->nestedDeadlock(); }
 
392
        private:
 
393
            Condition_ptr _cond;
 
394
            bool _temporal = false;
 
395
        };
 
396
        
 
397
        
 
398
        /******************** TEMPORAL OPERATORS ********************/        
 
399
        
 
400
        class QuantifierCondition : public Condition
 
401
        {
 
402
        public:
 
403
            virtual bool isTemporal() const override { return true;}
 
404
            CTLType getQueryType() const override { return CTLType::PATHQEURY; }
 
405
            virtual const Condition_ptr& operator[] (size_t i) const = 0;
 
406
        };
 
407
        
 
408
        class SimpleQuantifierCondition : public QuantifierCondition {
 
409
        public:
 
410
            SimpleQuantifierCondition(const Condition_ptr cond) {
 
411
                _cond = cond;
 
412
                _loop_sensitive = cond->isLoopSensitive();
 
413
            }
 
414
            int formulaSize() const override{
 
415
                return _cond->formulaSize() + 1;
 
416
            }
 
417
            
 
418
            void analyze(AnalysisContext& context) override;
 
419
            Result evaluate(const EvaluationContext& context) override;
 
420
            Result evalAndSet(const EvaluationContext& context) override;
 
421
            void toString(std::ostream&) const override;
 
422
            void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
 
423
            void toBinary(std::ostream& out) const override;
 
424
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
 
425
            virtual const Condition_ptr& operator[] (size_t i) const override { return _cond;}
 
426
            virtual bool containsNext() const override { return _cond->containsNext(); }
 
427
            bool nestedDeadlock() const override { return _cond->nestedDeadlock(); }
 
428
        private:
 
429
            virtual std::string op() const = 0;
 
430
            
 
431
        protected:
 
432
            Condition_ptr _cond;
 
433
        };
 
434
        
 
435
        class EXCondition : public SimpleQuantifierCondition {
 
436
        public:
 
437
            using SimpleQuantifierCondition::SimpleQuantifierCondition;
 
438
            Retval simplify(SimplificationContext& context) const override;
 
439
            bool isReachability(uint32_t depth) const override;
 
440
            Condition_ptr prepareForReachability(bool negated) const override;
 
441
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
442
            void toXML(std::ostream&, uint32_t tabs) const override;
 
443
            Quantifier getQuantifier() const override { return Quantifier::E; }
 
444
            Path getPath() const override             { return Path::X; }
 
445
            uint32_t distance(DistanceContext& context) const override;
 
446
            bool containsNext() const override { return true; }            
 
447
            virtual bool isLoopSensitive() const override { return true; }
 
448
            void visit(Visitor&) const override;
 
449
        private:
 
450
            std::string op() const override;
 
451
        };
 
452
        
 
453
        class EGCondition : public SimpleQuantifierCondition {
 
454
        public:
 
455
            using SimpleQuantifierCondition::SimpleQuantifierCondition;
 
456
 
 
457
            Retval simplify(SimplificationContext& context) const override;
 
458
            bool isReachability(uint32_t depth) const override;
 
459
            Condition_ptr prepareForReachability(bool negated) const override;
 
460
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
461
            void toXML(std::ostream&, uint32_t tabs) const override;
 
462
            Quantifier getQuantifier() const override { return Quantifier::E; }
 
463
            Path getPath() const override             { return Path::G; }            
 
464
            uint32_t distance(DistanceContext& context) const override;
 
465
            Result evaluate(const EvaluationContext& context) override;
 
466
            Result evalAndSet(const EvaluationContext& context) override;
 
467
            virtual bool isLoopSensitive() const override { return true; }
 
468
            void visit(Visitor&) const override;
 
469
        private:
 
470
            std::string op() const override;
 
471
        };
 
472
        
 
473
        class EFCondition : public SimpleQuantifierCondition {
 
474
        public:
 
475
            using SimpleQuantifierCondition::SimpleQuantifierCondition;
 
476
 
 
477
            Retval simplify(SimplificationContext& context) const override;
 
478
            bool isReachability(uint32_t depth) const override;
 
479
            Condition_ptr prepareForReachability(bool negated) const override;
 
480
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
481
            void toXML(std::ostream&, uint32_t tabs) const override;
 
482
            Quantifier getQuantifier() const override { return Quantifier::E; }
 
483
            Path getPath() const override             { return Path::F; }            
 
484
            uint32_t distance(DistanceContext& context) const override;
 
485
            Result evaluate(const EvaluationContext& context) override;
 
486
            Result evalAndSet(const EvaluationContext& context) override;
 
487
            void visit(Visitor&) const override;
 
488
        private:
 
489
            std::string op() const override;
 
490
        };
 
491
 
 
492
        class AXCondition : public SimpleQuantifierCondition {
 
493
        public:
 
494
            using SimpleQuantifierCondition::SimpleQuantifierCondition;
 
495
            Retval simplify(SimplificationContext& context) const override;
 
496
            bool isReachability(uint32_t depth) const override;
 
497
            Condition_ptr prepareForReachability(bool negated) const override;
 
498
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
499
            void toXML(std::ostream&, uint32_t tabs) const override;
 
500
            Quantifier getQuantifier() const override { return Quantifier::A; }
 
501
            Path getPath() const override             { return Path::X; }
 
502
            uint32_t distance(DistanceContext& context) const override;
 
503
            bool containsNext() const override { return true; }
 
504
            virtual bool isLoopSensitive() const override { return true; }
 
505
            void visit(Visitor&) const override;
 
506
        private:
 
507
            std::string op() const override;
 
508
        };
 
509
        
 
510
        class AGCondition : public SimpleQuantifierCondition {
 
511
        public:
 
512
            using SimpleQuantifierCondition::SimpleQuantifierCondition;
 
513
            Retval simplify(SimplificationContext& context) const override;
 
514
            bool isReachability(uint32_t depth) const override;
 
515
            Condition_ptr prepareForReachability(bool negated) const override;
 
516
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
517
            void toXML(std::ostream&, uint32_t tabs) const override;
 
518
            Quantifier getQuantifier() const override { return Quantifier::A; }
 
519
            Path getPath() const override             { return Path::G; } 
 
520
            uint32_t distance(DistanceContext& context) const override;
 
521
            Result evaluate(const EvaluationContext& context) override;
 
522
            Result evalAndSet(const EvaluationContext& context) override;
 
523
            void visit(Visitor&) const override;
 
524
        private:
 
525
            std::string op() const override;
 
526
        };
 
527
        
 
528
        class AFCondition : public SimpleQuantifierCondition {
 
529
        public:
 
530
            using SimpleQuantifierCondition::SimpleQuantifierCondition;
 
531
            Retval simplify(SimplificationContext& context) const override;
 
532
            bool isReachability(uint32_t depth) const override;
 
533
            Condition_ptr prepareForReachability(bool negated) const override;
 
534
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
535
            void toXML(std::ostream&, uint32_t tabs) const override;
 
536
            Quantifier getQuantifier() const override { return Quantifier::A; }
 
537
            Path getPath() const override             { return Path::F; }            
 
538
            uint32_t distance(DistanceContext& context) const override;
 
539
            Result evaluate(const EvaluationContext& context) override;
 
540
            Result evalAndSet(const EvaluationContext& context) override;
 
541
            void visit(Visitor&) const override;
 
542
            virtual bool isLoopSensitive() const override { return true; }
 
543
        private:
 
544
            std::string op() const override;
 
545
        };     
 
546
        
 
547
        class UntilCondition : public QuantifierCondition {
 
548
        public:
 
549
            UntilCondition(const Condition_ptr cond1, const Condition_ptr cond2) {
 
550
                _cond1 = cond1;
 
551
                _cond2 = cond2;
 
552
                _loop_sensitive = _cond1->isLoopSensitive() || _cond2->isLoopSensitive();
 
553
            }
 
554
            int formulaSize() const override{
 
555
                return _cond1->formulaSize() + _cond2->formulaSize() + 1;
 
556
            }
 
557
            
 
558
            void analyze(AnalysisContext& context) override;
 
559
            Result evaluate(const EvaluationContext& context) override;
 
560
            void toString(std::ostream&) const override;
 
561
            void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
 
562
            void toBinary(std::ostream& out) const override;            
 
563
            bool isReachability(uint32_t depth) const override;
 
564
            Condition_ptr prepareForReachability(bool negated) const override;
 
565
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
 
566
            Result evalAndSet(const EvaluationContext& context) override;
 
567
 
 
568
            virtual const Condition_ptr& operator[] (size_t i) const override
 
569
            { if(i == 0) return _cond1; return _cond2;}
 
570
            Path getPath() const override             
 
571
            { return Path::U; }
 
572
            bool containsNext() const override { return _cond1->containsNext() || _cond2->containsNext(); }
 
573
            bool nestedDeadlock() const override { return _cond1->nestedDeadlock() || _cond2->nestedDeadlock(); }
 
574
        private:
 
575
            virtual std::string op() const = 0; 
 
576
            
 
577
        protected:
 
578
            Condition_ptr _cond1;
 
579
            Condition_ptr _cond2;
 
580
        };
 
581
        
 
582
        class EUCondition : public UntilCondition {
 
583
        public:
 
584
            using UntilCondition::UntilCondition;  
 
585
            Retval simplify(SimplificationContext& context) const override;
 
586
            Quantifier getQuantifier() const override { return Quantifier::E; }
 
587
            void visit(Visitor&) const override;
 
588
            uint32_t distance(DistanceContext& context) const override;
 
589
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
590
            void toXML(std::ostream&, uint32_t tabs) const override;
 
591
            
 
592
        private:
 
593
            std::string op() const override;
 
594
        };
 
595
        
 
596
        class AUCondition : public UntilCondition {
 
597
        public:
 
598
            using UntilCondition::UntilCondition;
 
599
            Retval simplify(SimplificationContext& context) const override;
 
600
            Quantifier getQuantifier() const override { return Quantifier::A; }            
 
601
            void visit(Visitor&) const override;
 
602
            uint32_t distance(DistanceContext& context) const override;
 
603
            void toXML(std::ostream&, uint32_t tabs) const override;
 
604
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
605
            virtual bool isLoopSensitive() const override { return true; }
 
606
        private:
 
607
            std::string op() const override;
 
608
        };
 
609
        
 
610
        /******************** CONDITIONS ********************/
 
611
 
 
612
        class UnfoldedFireableCondition : public ShallowCondition {
 
613
        public:
 
614
            UnfoldedFireableCondition(const std::string& tname) : ShallowCondition(), _name(tname) {};
 
615
            Condition_ptr pushNegation(negstat_t& stat, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
616
            void visit(Visitor&) const override;
 
617
        protected:
 
618
            void _analyze(AnalysisContext& context) override;
 
619
            virtual void _toString(std::ostream& out) const;
 
620
            Condition_ptr clone() { return std::make_shared<UnfoldedFireableCondition>(_name); }
 
621
        private:
 
622
            const std::string _name;
 
623
        };
 
624
 
 
625
        class FireableCondition : public ShallowCondition {
 
626
        public:
 
627
            FireableCondition(const std::string& tname) : _name(tname) {};
 
628
            Condition_ptr pushNegation(negstat_t& stat, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
629
            void visit(Visitor&) const override;
 
630
        protected:
 
631
            void _analyze(AnalysisContext& context) override;
 
632
            virtual void _toString(std::ostream& out) const;
 
633
            Condition_ptr clone() { return std::make_shared<FireableCondition>(_name); }
 
634
        private:
 
635
            const std::string _name;
 
636
        };
 
637
 
 
638
        /* Logical conditon */
 
639
        class LogicalCondition : public Condition {
 
640
        public:
 
641
            int formulaSize() const override {
 
642
                size_t i = 1;
 
643
                for(auto& c : _conds) i += c->formulaSize();
 
644
                return i;
 
645
            }
 
646
            void analyze(AnalysisContext& context) override;
 
647
            
 
648
            uint32_t distance(DistanceContext& context) const override;
 
649
            void toString(std::ostream&) const override;
 
650
            void toBinary(std::ostream& out) const override;
 
651
            void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
 
652
            bool isReachability(uint32_t depth) const override;
 
653
            Condition_ptr prepareForReachability(bool negated) const override;
 
654
            const Condition_ptr& operator[](size_t i) const
 
655
            { 
 
656
                return _conds[i];
 
657
            };            
 
658
            CTLType getQueryType() const override { return CTLType::LOPERATOR; }
 
659
            Path getPath() const override         { return Path::pError; }
 
660
            
 
661
            bool isTemporal() const override
 
662
            {
 
663
                return _temporal;
 
664
            }
 
665
            auto begin() { return _conds.begin(); }
 
666
            auto end() { return _conds.end(); }
 
667
            auto begin() const { return _conds.begin(); }
 
668
            auto end() const { return _conds.end(); }
 
669
            bool empty() const { return _conds.size() == 0; }
 
670
            bool singular() const { return _conds.size() == 1; }
 
671
            size_t size() const { return _conds.size(); }
 
672
            bool containsNext() const override 
 
673
            { return std::any_of(begin(), end(), [](auto& a){return a->containsNext();}); }
 
674
            bool nestedDeadlock() const override;
 
675
 
 
676
        protected:
 
677
            LogicalCondition() {};
 
678
            Retval simplifyOr(SimplificationContext& context) const;
 
679
            Retval simplifyAnd(SimplificationContext& context) const;                  
 
680
 
 
681
        private:
 
682
            virtual uint32_t delta(uint32_t d1, uint32_t d2, const DistanceContext& context) const = 0;
 
683
            virtual std::string op() const = 0;
 
684
            
 
685
        protected:
 
686
            bool _temporal = false;
 
687
            std::vector<Condition_ptr> _conds;
 
688
        };
 
689
 
 
690
        /* Conjunctive and condition */
 
691
        class AndCondition : public LogicalCondition {
 
692
        public:
 
693
 
 
694
            AndCondition(std::vector<Condition_ptr>&& conds);
 
695
 
 
696
            AndCondition(const std::vector<Condition_ptr>& conds);
 
697
            
 
698
            AndCondition(Condition_ptr left, Condition_ptr right);
 
699
            
 
700
            Retval simplify(SimplificationContext& context) const override;
 
701
            Result evaluate(const EvaluationContext& context) override;
 
702
            Result evalAndSet(const EvaluationContext& context) override;
 
703
            void visit(Visitor&) const override;
 
704
            void toXML(std::ostream&, uint32_t tabs) const override;
 
705
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
 
706
            Quantifier getQuantifier() const override { return Quantifier::AND; }
 
707
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
708
        private:
 
709
            //int logicalOp() const;
 
710
            uint32_t delta(uint32_t d1, uint32_t d2, const DistanceContext& context) const override;
 
711
            std::string op() const override;
 
712
        };
 
713
 
 
714
        /* Disjunctive or conditon */
 
715
        class OrCondition : public LogicalCondition {
 
716
        public:
 
717
 
 
718
            OrCondition(std::vector<Condition_ptr>&& conds);
 
719
 
 
720
            OrCondition(const std::vector<Condition_ptr>& conds);
 
721
 
 
722
            OrCondition(Condition_ptr left, Condition_ptr right);
 
723
            
 
724
            Retval simplify(SimplificationContext& context) const override;
 
725
            Result evaluate(const EvaluationContext& context) override;
 
726
            Result evalAndSet(const EvaluationContext& context) override;
 
727
            void visit(Visitor&) const override;
 
728
            void toXML(std::ostream&, uint32_t tabs) const override;
 
729
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;   
 
730
            Quantifier getQuantifier() const override { return Quantifier::OR; }
 
731
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
732
        private:
 
733
            //int logicalOp() const;
 
734
            uint32_t delta(uint32_t d1, uint32_t d2, const DistanceContext& context) const override;
 
735
            std::string op() const override;
 
736
        };
 
737
 
 
738
        class CompareConjunction : public Condition
 
739
        {
 
740
        public:
 
741
            struct cons_t {
 
742
                int32_t _place  = -1;
 
743
                uint32_t _upper = std::numeric_limits<uint32_t>::max();
 
744
                uint32_t _lower = 0;
 
745
                std::string _name;
 
746
                bool operator<(const cons_t& other) const
 
747
                {
 
748
                    return _place < other._place;
 
749
                }
 
750
                
 
751
                void invert()
 
752
                {
 
753
                    if(_lower == 0 && _upper == std::numeric_limits<uint32_t>::max())
 
754
                        return;
 
755
                    assert(_lower == 0 || _upper == std::numeric_limits<uint32_t>::max());
 
756
                    if(_lower == 0)
 
757
                    {
 
758
                        _lower = _upper + 1;
 
759
                        _upper = std::numeric_limits<uint32_t>::max();
 
760
                    }
 
761
                    else if(_upper == std::numeric_limits<uint32_t>::max())
 
762
                    {
 
763
                        _upper = _lower - 1;
 
764
                        _lower = 0;
 
765
                    }
 
766
                    else
 
767
                    {
 
768
                        assert(false);
 
769
                    }
 
770
                }
 
771
                
 
772
                void intersect(const cons_t& other)
 
773
                {
 
774
                    _lower = std::max(_lower, other._lower);
 
775
                    _upper = std::min(_upper, other._upper);
 
776
                }
 
777
            };
 
778
 
 
779
            CompareConjunction(bool negated = false) 
 
780
                    : _negated(false) {};
 
781
            friend FireableCondition;
 
782
            CompareConjunction(const std::vector<cons_t>&& cons, bool negated) 
 
783
                    : _constraints(cons), _negated(negated) {};
 
784
            CompareConjunction(const std::vector<Condition_ptr>&, bool negated);
 
785
            CompareConjunction(const CompareConjunction& other, bool negated = false)
 
786
            : _constraints(other._constraints), _negated(other._negated != negated)
 
787
            {
 
788
            };
 
789
 
 
790
            void merge(const CompareConjunction& other);
 
791
            void merge(const std::vector<Condition_ptr>&, bool negated);
 
792
            
 
793
            int formulaSize() const override{
 
794
                int sum = 0;
 
795
                for(auto& c : _constraints)
 
796
                {
 
797
                    assert(c._place >= 0);
 
798
                    if(c._lower == c._upper) ++sum;
 
799
                    else {
 
800
                        if(c._lower != 0) ++sum;
 
801
                        if(c._upper != std::numeric_limits<uint32_t>::max()) ++sum;
 
802
                    }
 
803
                }
 
804
                if(sum == 1) return 2;
 
805
                else return (sum*2) + 1;
 
806
            }
 
807
            void analyze(AnalysisContext& context) override;
 
808
            uint32_t distance(DistanceContext& context) const override;
 
809
            void toString(std::ostream& stream) const override;
 
810
            void toTAPAALQuery(std::ostream& stream,TAPAALConditionExportContext& context) const override;
 
811
            void toBinary(std::ostream& out) const override;
 
812
            bool isReachability(uint32_t depth) const override { return depth > 0; };
 
813
            Condition_ptr prepareForReachability(bool negated) const override;
 
814
            CTLType getQueryType() const override { return CTLType::LOPERATOR; }
 
815
            Path getPath() const override         { return Path::pError; }            
 
816
            virtual void toXML(std::ostream& stream, uint32_t tabs) const override;
 
817
            Retval simplify(SimplificationContext& context) const override;
 
818
            Result evaluate(const EvaluationContext& context) override;
 
819
            Result evalAndSet(const EvaluationContext& context) override;
 
820
            void visit(Visitor&) const override;
 
821
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;   
 
822
            Quantifier getQuantifier() const override { return _negated ? Quantifier::OR : Quantifier::AND; }
 
823
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
824
            bool isNegated() const { return _negated; }
 
825
            bool singular() const 
 
826
            { 
 
827
                return _constraints.size() == 1 && 
 
828
                                    (_constraints[0]._lower == 0 || 
 
829
                                     _constraints[0]._upper == std::numeric_limits<uint32_t>::max());
 
830
            };
 
831
            bool containsNext() const override { return false;}
 
832
            bool nestedDeadlock() const override { return false; }
 
833
            const std::vector<cons_t>& constraints() const { return _constraints; }
 
834
            std::vector<cons_t>::const_iterator begin() const { return _constraints.begin(); }
 
835
            std::vector<cons_t>::const_iterator end() const { return _constraints.end(); }
 
836
        private:
 
837
            std::vector<cons_t> _constraints;
 
838
            bool _negated = false;
 
839
        };
 
840
 
 
841
 
 
842
        /* Comparison conditon */
 
843
        class CompareCondition : public Condition {
 
844
        public:
 
845
 
 
846
            CompareCondition(const Expr_ptr expr1, const Expr_ptr expr2)
 
847
            : _expr1(expr1), _expr2(expr2) {}
 
848
 
 
849
            int formulaSize() const override{
 
850
                return _expr1->formulaSize() + _expr2->formulaSize() + 1;
 
851
            }
 
852
            void analyze(AnalysisContext& context) override;
 
853
            Result evaluate(const EvaluationContext& context) override;
 
854
            Result evalAndSet(const EvaluationContext& context) override;
 
855
            void toString(std::ostream&) const override;
 
856
            void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
 
857
            void toBinary(std::ostream& out) const override;
 
858
            bool isReachability(uint32_t depth) const override;
 
859
            Condition_ptr prepareForReachability(bool negated) const override;
 
860
            Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
 
861
            Path getPath() const override { return Path::pError; }
 
862
            CTLType getQueryType() const override { return CTLType::EVAL; }
 
863
            const Expr_ptr& operator[](uint32_t id) const
 
864
            {
 
865
                if(id == 0) return _expr1;
 
866
                else return _expr2;
 
867
            }
 
868
            bool containsNext() const override { return false; }
 
869
            bool nestedDeadlock() const override { return false; }
 
870
            bool isTrivial() const;
 
871
        protected:
 
872
            uint32_t _distance(DistanceContext& c, 
 
873
                    std::function<uint32_t(uint32_t, uint32_t, bool)> d) const
 
874
            {
 
875
                return d(_expr1->evaluate(c), _expr2->evaluate(c), c.negated());
 
876
            }
 
877
        private:
 
878
            virtual bool apply(int v1, int v2) const = 0;
 
879
            virtual std::string op() const = 0;
 
880
            /** Operator when exported to TAPAAL */
 
881
            virtual std::string opTAPAAL() const = 0;
 
882
            /** Swapped operator when exported to TAPAAL, e.g. operator when operands are swapped */
 
883
            virtual std::string sopTAPAAL() const = 0;
 
884
 
 
885
        protected:
 
886
            Expr_ptr _expr1;
 
887
            Expr_ptr _expr2;
 
888
        };
 
889
 
 
890
        /* delta */
 
891
        template<typename T>
 
892
        uint32_t delta(int v1, int v2, bool negated)
 
893
        { return 0; }
 
894
        
 
895
        class EqualCondition : public CompareCondition {
 
896
        public:
 
897
 
 
898
            using CompareCondition::CompareCondition;
 
899
            Retval simplify(SimplificationContext& context) const override;
 
900
            void toXML(std::ostream&, uint32_t tabs) const override;
 
901
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
 
902
            uint32_t distance(DistanceContext& context) const override;
 
903
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
904
            void visit(Visitor&) const override;
 
905
        private:
 
906
            bool apply(int v1, int v2) const override;
 
907
            std::string op() const override;
 
908
            std::string opTAPAAL() const override;
 
909
            std::string sopTAPAAL() const override;
 
910
        };
 
911
 
 
912
        /* None equality conditon */
 
913
        class NotEqualCondition : public CompareCondition {
 
914
        public:
 
915
 
 
916
            using CompareCondition::CompareCondition;
 
917
            void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
 
918
            Retval simplify(SimplificationContext& context) const override;
 
919
            void toXML(std::ostream&, uint32_t tabs) const override;
 
920
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
 
921
            uint32_t distance(DistanceContext& context) const override;
 
922
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
923
            void visit(Visitor&) const override;
 
924
        private:
 
925
            bool apply(int v1, int v2) const override;
 
926
            std::string op() const override;
 
927
            std::string opTAPAAL() const override;
 
928
            std::string sopTAPAAL() const override;
 
929
        };
 
930
 
 
931
        /* Less-than conditon */
 
932
        class LessThanCondition : public CompareCondition {
 
933
        public:
 
934
 
 
935
            using CompareCondition::CompareCondition;
 
936
            Retval simplify(SimplificationContext& context) const override;
 
937
            void toXML(std::ostream&, uint32_t tabs) const override;
 
938
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
 
939
            uint32_t distance(DistanceContext& context) const override;
 
940
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
941
            void visit(Visitor&) const override;
 
942
        private:
 
943
            bool apply(int v1, int v2) const override;
 
944
            std::string op() const override;
 
945
            std::string opTAPAAL() const override;
 
946
            std::string sopTAPAAL() const override;
 
947
        };
 
948
 
 
949
        /* Less-than-or-equal conditon */
 
950
        class LessThanOrEqualCondition : public CompareCondition {
 
951
        public:
 
952
 
 
953
            using CompareCondition::CompareCondition;
 
954
            Retval simplify(SimplificationContext& context) const override;
 
955
            void toXML(std::ostream&, uint32_t tabs) const override;
 
956
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
 
957
            uint32_t distance(DistanceContext& context) const override;
 
958
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
959
            void visit(Visitor&) const override;
 
960
        private:
 
961
            bool apply(int v1, int v2) const override;
 
962
            std::string op() const override;
 
963
            std::string opTAPAAL() const override;
 
964
            std::string sopTAPAAL() const override;
 
965
        };
 
966
 
 
967
        /* Greater-than conditon */
 
968
        class GreaterThanCondition : public CompareCondition {
 
969
        public:
 
970
 
 
971
            using CompareCondition::CompareCondition;
 
972
            Retval simplify(SimplificationContext& context) const override;
 
973
            void toXML(std::ostream&, uint32_t tabs) const override;
 
974
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
 
975
            uint32_t distance(DistanceContext& context) const override;
 
976
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
977
            void visit(Visitor&) const override;
 
978
        private:
 
979
            bool apply(int v1, int v2) const override;
 
980
            std::string op() const override;
 
981
            std::string opTAPAAL() const override;
 
982
            std::string sopTAPAAL() const override;
 
983
        };
 
984
 
 
985
        /* Greater-than-or-equal conditon */
 
986
        class GreaterThanOrEqualCondition : public CompareCondition {
 
987
        public:
 
988
            using CompareCondition::CompareCondition;
 
989
            Retval simplify(SimplificationContext& context) const override;
 
990
            void toXML(std::ostream&, uint32_t tabs) const override;
 
991
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
 
992
            uint32_t distance(DistanceContext& context) const override;
 
993
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
994
            void visit(Visitor&) const override;
 
995
        private:
 
996
            bool apply(int v1, int v2) const override;
 
997
            std::string op() const override;
 
998
            std::string opTAPAAL() const override;
 
999
            std::string sopTAPAAL() const override;
 
1000
        };
 
1001
 
 
1002
        /* Bool condition */
 
1003
        class BooleanCondition : public Condition {
 
1004
        public:
 
1005
 
 
1006
            BooleanCondition(bool value) : _value(value) {
 
1007
                if (value) {
 
1008
                    trivial = 1;
 
1009
                } else {
 
1010
                    trivial = 2;
 
1011
                }
 
1012
            }
 
1013
            int formulaSize() const override{
 
1014
                return 0;
 
1015
            }
 
1016
            void analyze(AnalysisContext& context) override;
 
1017
            Result evaluate(const EvaluationContext& context) override;
 
1018
            Result evalAndSet(const EvaluationContext& context) override;
 
1019
            void visit(Visitor&) const override;           
 
1020
            uint32_t distance(DistanceContext& context) const override;
 
1021
            static Condition_ptr TRUE_CONSTANT;
 
1022
            static Condition_ptr FALSE_CONSTANT;
 
1023
            void toString(std::ostream&) const override;
 
1024
            void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
 
1025
            static Condition_ptr getShared(bool val);
 
1026
            Retval simplify(SimplificationContext& context) const override;
 
1027
            bool isReachability(uint32_t depth) const override;
 
1028
            Condition_ptr prepareForReachability(bool negated) const override;
 
1029
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
1030
            void toXML(std::ostream&, uint32_t tabs) const override;
 
1031
            void toBinary(std::ostream&) const override;
 
1032
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
 
1033
            Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
 
1034
            Path getPath() const override { return Path::pError; }
 
1035
            CTLType getQueryType() const override { return CTLType::EVAL; }
 
1036
            bool containsNext() const override { return false; }
 
1037
            bool nestedDeadlock() const override { return false; }
 
1038
        private:
 
1039
            const bool _value;
 
1040
        };
 
1041
 
 
1042
        /* Deadlock condition */
 
1043
        class DeadlockCondition : public Condition {
 
1044
        public:
 
1045
 
 
1046
            DeadlockCondition() {
 
1047
                _loop_sensitive = true;
 
1048
            }
 
1049
            int formulaSize() const override{
 
1050
                return 1;
 
1051
            }
 
1052
            void analyze(AnalysisContext& context) override;
 
1053
            Result evaluate(const EvaluationContext& context) override;
 
1054
            Result evalAndSet(const EvaluationContext& context) override;
 
1055
            void visit(Visitor&) const override;
 
1056
            uint32_t distance(DistanceContext& context) const override;
 
1057
            void toString(std::ostream&) const override;
 
1058
            void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
 
1059
            Retval simplify(SimplificationContext& context) const override;
 
1060
            bool isReachability(uint32_t depth) const override;
 
1061
            Condition_ptr prepareForReachability(bool negated) const override;
 
1062
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
1063
            void toXML(std::ostream&, uint32_t tabs) const override;
 
1064
            void toBinary(std::ostream&) const override;
 
1065
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
 
1066
            static Condition_ptr DEADLOCK;
 
1067
            Quantifier getQuantifier() const override { return Quantifier::DEADLOCK; }
 
1068
            Path getPath() const override { return Path::pError; }
 
1069
            CTLType getQueryType() const override { return CTLType::EVAL; }
 
1070
            bool containsNext() const override { return false; }
 
1071
            bool nestedDeadlock() const override { return false; }
 
1072
        };
 
1073
 
 
1074
        class KSafeCondition : public ShallowCondition
 
1075
        {
 
1076
        public:
 
1077
            KSafeCondition(const Expr_ptr& expr1) : _bound(expr1)
 
1078
            {}
 
1079
 
 
1080
        protected:
 
1081
            void _analyze(AnalysisContext& context) override;
 
1082
            void _toString(std::ostream& out) const override;
 
1083
            void visit(Visitor&) const override;
 
1084
            Condition_ptr clone() override
 
1085
            {
 
1086
                return std::make_shared<KSafeCondition>(_bound);
 
1087
            }
 
1088
        private:
 
1089
            Expr_ptr _bound = nullptr;
 
1090
        };
 
1091
 
 
1092
        class LivenessCondition : public ShallowCondition
 
1093
        {
 
1094
        public:
 
1095
            LivenessCondition() {}
 
1096
        protected:
 
1097
            void _analyze(AnalysisContext& context) override;
 
1098
            void _toString(std::ostream& out) const override;
 
1099
            void visit(Visitor&) const override;
 
1100
            Condition_ptr clone() override { return std::make_shared<LivenessCondition>(); }
 
1101
        };
 
1102
 
 
1103
        class QuasiLivenessCondition : public ShallowCondition
 
1104
        {
 
1105
        public:
 
1106
            QuasiLivenessCondition() {}
 
1107
        protected:
 
1108
            void _analyze(AnalysisContext& context) override;
 
1109
            void _toString(std::ostream& out) const override;
 
1110
            void visit(Visitor&) const override;
 
1111
            Condition_ptr clone() override { return std::make_shared<QuasiLivenessCondition>(); }
 
1112
        };
 
1113
 
 
1114
        class StableMarkingCondition : public ShallowCondition
 
1115
        {
 
1116
        public:
 
1117
            StableMarkingCondition() {}
 
1118
        protected:
 
1119
            void _analyze(AnalysisContext& context) override;
 
1120
            void _toString(std::ostream& out) const override;
 
1121
            void visit(Visitor&) const override;
 
1122
            Condition_ptr clone() override { return std::make_shared<StableMarkingCondition>(); }
 
1123
        };
 
1124
 
 
1125
        class UpperBoundsCondition : public ShallowCondition
 
1126
        {
 
1127
        public:
 
1128
            
 
1129
            UpperBoundsCondition(const std::vector<std::string>& places) : _places(places)
 
1130
            {}
 
1131
        protected:
 
1132
            void _toString(std::ostream& out) const override;
 
1133
            void _analyze(AnalysisContext& context) override;
 
1134
            void visit(Visitor&) const override;
 
1135
            Condition_ptr clone() override
 
1136
            {
 
1137
                return std::make_shared<UpperBoundsCondition>(_places);
 
1138
            }
 
1139
 
 
1140
        private:
 
1141
            std::vector<std::string> _places;
 
1142
        };
 
1143
 
 
1144
        class UnfoldedUpperBoundsCondition : public Condition
 
1145
        {
 
1146
        public:
 
1147
            struct place_t {
 
1148
                std::string _name;
 
1149
                uint32_t _place = 0;
 
1150
                double _max = std::numeric_limits<double>::infinity();
 
1151
                bool _maxed_out = false;
 
1152
                place_t(const std::string& name)
 
1153
                {
 
1154
                    _name = name;
 
1155
                }
 
1156
                place_t(const place_t& other, double max)
 
1157
                {
 
1158
                    _name = other._name;
 
1159
                    _place = other._place;
 
1160
                    _max = max;
 
1161
                }
 
1162
                bool operator<(const place_t& other) const{
 
1163
                    return _place < other._place;
 
1164
                }
 
1165
            };
 
1166
            
 
1167
            UnfoldedUpperBoundsCondition(const std::vector<std::string>& places)
 
1168
            {
 
1169
                for(auto& s : places) _places.push_back(s);
 
1170
            }
 
1171
            UnfoldedUpperBoundsCondition(const std::vector<place_t>& places, double max, double offset)
 
1172
                    : _places(places), _max(max), _offset(offset) {
 
1173
            };
 
1174
            int formulaSize() const override{
 
1175
                return _places.size();
 
1176
            }
 
1177
            void analyze(AnalysisContext& context) override;
 
1178
            size_t value(const MarkVal*);
 
1179
            Result evaluate(const EvaluationContext& context) override;
 
1180
            Result evalAndSet(const EvaluationContext& context) override;
 
1181
            void visit(Visitor&) const override;
 
1182
            uint32_t distance(DistanceContext& context) const override;
 
1183
            void toString(std::ostream&) const override;
 
1184
            void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
 
1185
            void toBinary(std::ostream&) const override;
 
1186
            Retval simplify(SimplificationContext& context) const override;
 
1187
            bool isReachability(uint32_t depth) const override;
 
1188
            Condition_ptr prepareForReachability(bool negated) const override;
 
1189
            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
 
1190
            void toXML(std::ostream&, uint32_t tabs) const override;
 
1191
            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
 
1192
            Quantifier getQuantifier() const override { return Quantifier::UPPERBOUNDS; }
 
1193
            Path getPath() const override { return Path::pError; }
 
1194
            CTLType getQueryType() const override { return CTLType::EVAL; }
 
1195
            bool containsNext() const override { return false; }
 
1196
            bool nestedDeadlock() const override { return false; }
 
1197
            
 
1198
            double bounds(bool add_offset = true) const { 
 
1199
                return (add_offset ? _offset : 0 ) + _bound; 
 
1200
            }
 
1201
            
 
1202
            virtual void setUpperBound(size_t bound)
 
1203
            {
 
1204
                _bound = std::max(_bound, bound);
 
1205
            }
 
1206
            
 
1207
            const std::vector<place_t>& places() const { return _places; }
 
1208
            
 
1209
        private:
 
1210
            std::vector<place_t> _places;
 
1211
            size_t _bound = 0;
 
1212
            double _max = std::numeric_limits<double>::infinity();
 
1213
            double _offset = 0;
 
1214
        };
 
1215
 
 
1216
    }
 
1217
}
 
1218
 
 
1219
 
 
1220
 
 
1221
#endif // EXPRESSIONS_H