← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to PetriEngine/PQL/PQL.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:
PetriEngine/PQL/PQL.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
 
 * 
6
 
 * This program is free software: you can redistribute it and/or modify
7
 
 * it under the terms of the GNU General Public License as published by
8
 
 * the Free Software Foundation, either version 3 of the License, or
9
 
 * (at your option) any later version.
10
 
 * 
11
 
 * This program is distributed in the hope that it will be useful,
12
 
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
13
 
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
14
 
 * GNU General Public License for more details.
15
 
 * 
16
 
 * You should have received a copy of the GNU General Public License
17
 
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
18
 
 */
19
 
#ifndef PQL_H
20
 
#define PQL_H
21
 
#include <string>
22
 
#include <list>
23
 
#include <vector>
24
 
#include <algorithm>
25
 
#include <unordered_map>
26
 
#include <memory>
27
 
 
28
 
#ifdef ENABLE_TAR
29
 
#include <z3++.h>
30
 
#endif
31
 
 
32
 
#include "../PetriNet.h"
33
 
#include "../Structures/State.h"
34
 
#include "../ReducingSuccessorGenerator.h"
35
 
#include "../Simplification/LPCache.h"
36
 
 
37
 
namespace PetriEngine {
38
 
    class ReducingSuccessorGenerator;
39
 
    namespace Simplification
40
 
    {
41
 
        class Member;
42
 
        struct Retval;
43
 
    }
44
 
    namespace PQL {
45
 
        
46
 
        enum CTLType {PATHQEURY = 1, LOPERATOR = 2, EVAL = 3, TYPE_ERROR = -1};
47
 
        enum Quantifier { AND = 1, OR = 2, A = 3, E = 4, NEG = 5, COMPCONJ = 6, DEADLOCK = 7, UPPERBOUNDS = 8, PN_BOOLEAN = 9, EMPTY = -1 };
48
 
        enum Path { G = 1, X = 2, F = 3, U = 4, pError = -1 };
49
 
        
50
 
        
51
 
        class AnalysisContext;
52
 
        class EvaluationContext;
53
 
        class DistanceContext;
54
 
        class TAPAALConditionExportContext;
55
 
        class SimplificationContext;
56
 
 
57
 
        /** Representation of a PQL error */
58
 
        class ExprError {
59
 
            std::string _text;
60
 
            int _length;
61
 
        public:
62
 
 
63
 
            ExprError(std::string text = "", int length = 0) {
64
 
                _text = text;
65
 
                _length = length;
66
 
            }
67
 
 
68
 
            /** Human readable explaination of the error */
69
 
            const std::string& text() const {
70
 
                return _text;
71
 
            }
72
 
 
73
 
            /** length in the source, 0 if not applicable */
74
 
            int length() const {
75
 
                return _length;
76
 
            }
77
 
 
78
 
            /** Convert error to string */
79
 
            std::string toString() const {
80
 
                return "Parsing error \"" + text() + "\"";
81
 
            }
82
 
 
83
 
            /** True, if this is a default created ExprError without any information */
84
 
            bool isEmpty() const {
85
 
                return _text.empty() && _length == 0;
86
 
            }
87
 
        };
88
 
 
89
 
        /** Representation of an expression */
90
 
        class Expr {
91
 
            int _eval = 0;
92
 
        public:
93
 
            /** Types of expressions */
94
 
            enum Types {
95
 
                /** Binary addition expression */
96
 
                PlusExpr,
97
 
                /** Binary subtraction expression */
98
 
                SubtractExpr,
99
 
                /** Binary multiplication expression */
100
 
                MultiplyExpr,
101
 
                /** Unary minus expression */
102
 
                MinusExpr,
103
 
                /** Literal integer expression */
104
 
                LiteralExpr,
105
 
                /** Identifier expression */
106
 
                IdentifierExpr
107
 
            };
108
 
        public:
109
 
            /** Virtual destructor, an expression should know it subexpressions */
110
 
            virtual ~Expr();
111
 
            /** Perform context analysis */
112
 
            virtual void analyze(AnalysisContext& context) = 0;
113
 
            /** Evaluate the expression given marking and assignment */
114
 
            virtual int evaluate(const EvaluationContext& context) = 0;
115
 
            int evalAndSet(const EvaluationContext& context);
116
 
#ifdef ENABLE_TAR
117
 
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const = 0;
118
 
#endif
119
 
            /** Generate LLVM intermediate code for this expr  */
120
 
            //virtual llvm::Value* codegen(CodeGenerationContext& context) const = 0;
121
 
            /** Convert expression to string */
122
 
            virtual void toString(std::ostream&) const = 0;
123
 
            /** Expression type */
124
 
            virtual Types type() const = 0;
125
 
            /** Construct left/right side of equations used in query simplification */
126
 
            virtual Simplification::Member constraint(SimplificationContext& context) const = 0;
127
 
            /** Output the expression as it currently is to a file in XML */
128
 
            virtual void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const = 0;
129
 
            virtual void toBinary(std::ostream&) const = 0;
130
 
            /** Stubborn reduction: increasing and decreasing sets */
131
 
            virtual void incr(ReducingSuccessorGenerator& generator) const = 0;
132
 
            virtual void decr(ReducingSuccessorGenerator& generator) const = 0;
133
 
            /** Count size of the entire formula in number of nodes */
134
 
            virtual int formulaSize() const = 0;
135
 
            
136
 
            virtual bool placeFree() const = 0;
137
 
            
138
 
            void setEval(int eval) {
139
 
                _eval = eval;
140
 
            }
141
 
            
142
 
            int getEval() {
143
 
                return _eval;
144
 
            }
145
 
        };
146
 
/******************* NEGATION PUSH STATS  *******************/
147
 
        
148
 
        struct negstat_t
149
 
        {
150
 
            negstat_t()
151
 
            {
152
 
                for(size_t i = 0; i < 31; ++i) _used[i] = 0;
153
 
            }
154
 
            void print(std::ostream& stream)
155
 
            {
156
 
                for(size_t i = 0; i < 31; ++i) stream << _used[i] << ",";                
157
 
            }
158
 
            void printRules(std::ostream& stream)
159
 
            {
160
 
                for(size_t i = 0; i < 31; ++i) stream << _rulename[i] << ",";                
161
 
            }
162
 
            int _used[31];
163
 
            const std::vector<const char*> _rulename = {
164
 
                "EG p-> !EF !p",
165
 
                "AG p-> !AF !p",
166
 
                "!EX p -> AX p",
167
 
                "EX false -> false",
168
 
                "EX true -> !deadlock",
169
 
                "!AX p -> EX p",
170
 
                "AX false -> deadlock",
171
 
                "AX true -> true",             
172
 
                "EF !deadlock -> !deadlock",
173
 
                "EF EF p -> EF p",
174
 
                "EF AF p -> AF p",
175
 
                "EF E p U q -> EF q",
176
 
                "EF A p U q -> EF q",
177
 
                "EF .. or .. -> EF .. or EF ..",
178
 
                "AF !deadlock -> !deadlock",
179
 
                "AF AF p -> AF p",
180
 
                "AF EF p -> EF p",
181
 
                "AF .. or EF p -> EF p or AF ..",
182
 
                "AF A p U q -> AF q",
183
 
                "A p U !deadlock -> !deadlock",
184
 
                "A deadlock U q -> q",
185
 
                "A !deadlock U q -> AF q",
186
 
                "A p U AF q -> AF q",
187
 
                "A p U EF q -> EF q",
188
 
                "A p U .. or EF q -> EF q or A p U ..",
189
 
                "E p U !deadlock -> !deadlock",
190
 
                "E deadlock U q -> q",
191
 
                "E !deadlock U q -> EF q",
192
 
                "E p U EF q -> EF q",
193
 
                "E p U .. or EF q -> EF q or E p U ..",
194
 
                "!! p -> p"
195
 
                
196
 
            };
197
 
            int& operator[](size_t i) { return _used[i]; }
198
 
            bool negated_fireability = false;
199
 
        };
200
 
        
201
 
        /** Base condition */
202
 
        class Condition {
203
 
        public:
204
 
            enum Result {RUNKNOWN=-1,RFALSE=0,RTRUE=1};
205
 
        private:
206
 
            bool _inv = false;
207
 
            Result _eval = RUNKNOWN;
208
 
        protected:
209
 
            bool _loop_sensitive = false;            
210
 
        public:
211
 
            /** Virtual destructor */
212
 
            virtual ~Condition();
213
 
            /** Perform context analysis  */
214
 
            virtual void analyze(AnalysisContext& context) = 0;
215
 
            /** Evaluate condition */
216
 
            virtual Result evaluate(const EvaluationContext& context) = 0;
217
 
            virtual Result evalAndSet(const EvaluationContext& context) = 0;
218
 
            
219
 
#ifdef ENABLE_TAR
220
 
            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const = 0;
221
 
#endif
222
 
            
223
 
            /** Generate LLVM intermediate code for this condition  */
224
 
            //virtual llvm::Value* codegen(CodeGenerationContext& context) const = 0;
225
 
            /** Convert condition to string */
226
 
            virtual void toString(std::ostream&) const = 0;
227
 
            /** Export condition to TAPAAL query (add EF manually!) */
228
 
            virtual void toTAPAALQuery(std::ostream&, TAPAALConditionExportContext& context) const = 0;
229
 
            /** Get distance to query */
230
 
            virtual uint32_t distance(DistanceContext& context) const = 0;
231
 
            /** Query Simplification */
232
 
            virtual Simplification::Retval simplify(SimplificationContext& context) const = 0;
233
 
            /** Check if query is a reachability query */
234
 
            virtual bool isReachability(uint32_t depth = 0) const = 0;
235
 
 
236
 
            virtual bool isLoopSensitive() const { return _loop_sensitive; };
237
 
            /** Prepare reachability queries */
238
 
            virtual std::shared_ptr<Condition> prepareForReachability(bool negated = false) const = 0;
239
 
            virtual std::shared_ptr<Condition> pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated = false, bool initrw = true) = 0;
240
 
            
241
 
            /** Output the condition as it currently is to a file in XML */
242
 
            virtual void toXML(std::ostream&, uint32_t tabs) const = 0;
243
 
            virtual void toBinary(std::ostream& out) const = 0;
244
 
 
245
 
            /** Find interesting transitions in stubborn reduction*/
246
 
            virtual void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const = 0;
247
 
            /** Checks if the condition is trivially true */
248
 
            bool isTriviallyTrue();
249
 
            /*** Checks if the condition is trivially false */
250
 
            bool isTriviallyFalse();
251
 
            /** Count size of the entire formula in number of nodes */
252
 
            virtual int formulaSize() const = 0;
253
 
 
254
 
            bool isSatisfied() const
255
 
            {
256
 
                return _eval == RTRUE;
257
 
            }
258
 
            
259
 
            void setSatisfied(bool isSatisfied)
260
 
            {
261
 
                _eval = isSatisfied ? RTRUE : RFALSE;
262
 
            }
263
 
            
264
 
            void setSatisfied(Result isSatisfied)
265
 
            {
266
 
                _eval = isSatisfied;
267
 
            }
268
 
            
269
 
            void setInvariant(bool isInvariant)
270
 
            {
271
 
                _inv = isInvariant;
272
 
            }
273
 
           
274
 
            bool isInvariant()
275
 
            {
276
 
                return _inv;
277
 
            }
278
 
            
279
 
            virtual bool isTemporal() const { return false;}
280
 
            virtual CTLType getQueryType() const = 0;
281
 
            virtual Quantifier getQuantifier() const = 0;
282
 
            virtual Path getPath() const = 0;
283
 
            static std::shared_ptr<Condition> 
284
 
            initialMarkingRW(std::function<std::shared_ptr<Condition> ()> func, negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw);
285
 
            virtual bool containsNext() const = 0;   
286
 
            virtual bool nestedDeadlock() const = 0;
287
 
        protected:
288
 
            //Value for checking if condition is trivially true or false.
289
 
            //0 is undecided (default), 1 is true, 2 is false.
290
 
            uint32_t trivial = 0;
291
 
        };
292
 
        typedef std::shared_ptr<Condition> Condition_ptr;
293
 
        typedef std::shared_ptr<Expr> Expr_ptr;
294
 
    } // PQL
295
 
} // PetriEngine
296
 
 
297
 
#endif // PQL_H