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