← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to PetriEngine/PQL/Contexts.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/Contexts.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 CONTEXTS_H
21
 
#define CONTEXTS_H
22
 
 
23
 
 
24
 
#include <string>
25
 
#include <vector>
26
 
#include <list>
27
 
#include <map>
28
 
#include <chrono>
29
 
 
30
 
#include "../PetriNet.h"
31
 
#include "PetriEngine/Simplification/LPCache.h"
32
 
#include "PQL.h"
33
 
#include "../NetStructures.h"
34
 
 
35
 
namespace PetriEngine {
36
 
    namespace PQL {
37
 
 
38
 
        /** Context provided for context analysis */
39
 
        class AnalysisContext {
40
 
        protected:
41
 
            const unordered_map<std::string, uint32_t>& _placeNames;
42
 
            const unordered_map<std::string, uint32_t>& _transitionNames;
43
 
            const PetriNet* _net;
44
 
            std::vector<ExprError> _errors;
45
 
        public:
46
 
 
47
 
            /** A resolution result */
48
 
            struct ResolutionResult {
49
 
                /** Offset in relevant vector */
50
 
                int offset;
51
 
                /** True, if the resolution was successful */
52
 
                bool success;
53
 
            };
54
 
 
55
 
            AnalysisContext(const std::unordered_map<std::string, uint32_t>& places, const std::unordered_map<std::string, uint32_t>& tnames, const PetriNet* net)
56
 
            : _placeNames(places), _transitionNames(tnames), _net(net) {
57
 
 
58
 
            }
59
 
            
60
 
            virtual void setHasDeadlock(){};
61
 
            
62
 
            const PetriNet* net() const
63
 
            {
64
 
                return _net;
65
 
            }
66
 
            
67
 
            /** Resolve an identifier */
68
 
            virtual ResolutionResult resolve(const std::string& identifier, bool place = true) {
69
 
                ResolutionResult result;
70
 
                result.offset = -1;
71
 
                result.success = false;
72
 
                auto& map = place ? _placeNames : _transitionNames;
73
 
                auto it = map.find(identifier);
74
 
                if(it != map.end())
75
 
                {
76
 
                    result.offset = (int)it->second;
77
 
                    result.success = true;
78
 
                    return result;
79
 
                }                
80
 
                return result;
81
 
            }
82
 
 
83
 
            /** Report error */
84
 
            void reportError(const ExprError& error) {
85
 
                _errors.push_back(error);
86
 
            }
87
 
 
88
 
            /** Get list of errors */
89
 
            const std::vector<ExprError>& errors() const {
90
 
                return _errors;
91
 
            }
92
 
        };
93
 
 
94
 
        class ColoredAnalysisContext : public AnalysisContext {
95
 
        protected:
96
 
            const std::unordered_map<std::string, std::unordered_map<uint32_t , std::string>>& _coloredPlaceNames;
97
 
            const std::unordered_map<std::string, std::vector<std::string>>& _coloredTransitionNames;
98
 
 
99
 
            bool _colored;
100
 
 
101
 
        public:
102
 
            ColoredAnalysisContext(const std::unordered_map<std::string, uint32_t>& places,
103
 
                                   const std::unordered_map<std::string, uint32_t>& tnames,
104
 
                                   const PetriNet* net,
105
 
                                   const std::unordered_map<std::string, std::unordered_map<uint32_t , std::string>>& cplaces,
106
 
                                   const std::unordered_map<std::string, std::vector<std::string>>& ctnames,
107
 
                                   bool colored)
108
 
                    : AnalysisContext(places, tnames, net),
109
 
                      _coloredPlaceNames(cplaces),
110
 
                      _coloredTransitionNames(ctnames),
111
 
                      _colored(colored)
112
 
            {}
113
 
 
114
 
            bool resolvePlace(const std::string& place, std::unordered_map<uint32_t,std::string>& out) {
115
 
                auto it = _coloredPlaceNames.find(place);
116
 
                if (it != _coloredPlaceNames.end()) {
117
 
                    out = it->second;
118
 
                    return true;
119
 
                }
120
 
                return false;
121
 
            }
122
 
 
123
 
            bool resolveTransition(const std::string& transition, std::vector<std::string>& out) {
124
 
                auto it = _coloredTransitionNames.find(transition);
125
 
                if (it != _coloredTransitionNames.end()) {
126
 
                    out = it->second;
127
 
                    return true;
128
 
                }
129
 
                return false;
130
 
            }
131
 
 
132
 
            bool isColored() const {
133
 
                return _colored;
134
 
            }
135
 
        };
136
 
 
137
 
        /** Context provided for evalation */
138
 
        class EvaluationContext {
139
 
        public:
140
 
 
141
 
            /** Create evaluation context, this doesn't take ownership */
142
 
            EvaluationContext(const MarkVal* marking,
143
 
                    const PetriNet* net) {
144
 
                _marking = marking;
145
 
                _net = net;
146
 
            }
147
 
            
148
 
            EvaluationContext() {};
149
 
 
150
 
            const MarkVal* marking() const {
151
 
                return _marking;
152
 
            }
153
 
            
154
 
            void setMarking(MarkVal* marking) {
155
 
                _marking = marking;
156
 
            }
157
 
 
158
 
            const PetriNet* net() const {
159
 
                return _net;
160
 
            }
161
 
        private:
162
 
            const MarkVal* _marking = nullptr;
163
 
            const PetriNet* _net = nullptr;
164
 
        };
165
 
 
166
 
        /** Context for distance computation */
167
 
        class DistanceContext : public EvaluationContext {
168
 
        public:
169
 
 
170
 
            DistanceContext(const PetriNet* net,
171
 
                    const MarkVal* marking)
172
 
            : EvaluationContext(marking, net) {
173
 
                _negated = false;
174
 
            }
175
 
 
176
 
 
177
 
            void negate() {
178
 
                _negated = !_negated;
179
 
            }
180
 
 
181
 
            bool negated() const {
182
 
                return _negated;
183
 
            }
184
 
 
185
 
        private:
186
 
            bool _negated;
187
 
        };
188
 
 
189
 
        /** Context for condition to TAPAAL export */
190
 
        class TAPAALConditionExportContext {
191
 
        public:
192
 
            bool failed;
193
 
            std::string netName;
194
 
        };
195
 
 
196
 
        class SimplificationContext {
197
 
        public:
198
 
 
199
 
            SimplificationContext(const MarkVal* marking,
200
 
                    const PetriNet* net, uint32_t queryTimeout, uint32_t lpTimeout,
201
 
                    LPCache* cache)
202
 
                    : _queryTimeout(queryTimeout), _lpTimeout(lpTimeout) {
203
 
                _negated = false;
204
 
                _marking = marking;
205
 
                _net = net;
206
 
                _start = std::chrono::high_resolution_clock::now();
207
 
                _cache = cache;
208
 
            }
209
 
 
210
 
            const MarkVal* marking() const {
211
 
                return _marking;
212
 
            }
213
 
 
214
 
            const PetriNet* net() const {
215
 
                return _net;
216
 
            }
217
 
 
218
 
            void negate() {
219
 
                _negated = !_negated;
220
 
            }
221
 
 
222
 
            bool negated() const {
223
 
                return _negated;
224
 
            }
225
 
            
226
 
            void setNegate(bool b){
227
 
                _negated = b;
228
 
            }
229
 
            
230
 
            double getReductionTime(){
231
 
                // duration in seconds
232
 
                auto end = std::chrono::high_resolution_clock::now();
233
 
                return (std::chrono::duration_cast<std::chrono::microseconds>(end - _start).count())*0.000001;
234
 
            }
235
 
            
236
 
            bool timeout() const {
237
 
                auto end = std::chrono::high_resolution_clock::now();
238
 
                auto diff = std::chrono::duration_cast<std::chrono::seconds>(end - _start);
239
 
                return (diff.count() >= _queryTimeout);
240
 
            }
241
 
            
242
 
            uint32_t getLpTimeout() const {
243
 
                return _lpTimeout;
244
 
            }
245
 
            
246
 
            LPCache* cache() const
247
 
            {
248
 
                return _cache;
249
 
            }
250
 
 
251
 
        private:
252
 
            bool _negated;
253
 
            const MarkVal* _marking;
254
 
            const PetriNet* _net;
255
 
            uint32_t _queryTimeout, _lpTimeout;
256
 
            std::chrono::high_resolution_clock::time_point _start;
257
 
            LPCache* _cache;
258
 
        };
259
 
 
260
 
    } // PQL
261
 
} // PetriEngine
262
 
 
263
 
#endif // CONTEXTS_H