← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to include/PetriEngine/TAR/ContainsVisitor.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/TAR/ContainsVisitor.h
 
1
/*
 
2
 *  Copyright Peter G. Jensen, all rights reserved.
 
3
 */
 
4
 
 
5
/* 
 
6
 * File:   ContainsVisitor.h
 
7
 * Author: Peter G. Jensen <root@petergjoel.dk>
 
8
 *
 
9
 * Created on April 21, 2020, 10:44 PM
 
10
 */
 
11
 
 
12
#ifndef CONTAINSVISITOR_H
 
13
#define CONTAINSVISITOR_H
 
14
 
 
15
#include "PetriEngine/TAR/range.h"
 
16
#include "PetriEngine/PetriNet.h"
 
17
#include "PetriEngine/PQL/Expressions.h"
 
18
#include "PetriEngine/PQL/Visitor.h"
 
19
 
 
20
#include <type_traits>
 
21
 
 
22
namespace PetriEngine
 
23
{
 
24
    using namespace Reachability;
 
25
 
 
26
    using namespace PQL;
 
27
    template<typename T>
 
28
    class ContainsVisitor : public Visitor {
 
29
    public:
 
30
        ContainsVisitor() {}
 
31
        bool does_contain() const { return _value; }
 
32
    private:
 
33
        bool _value = false;
 
34
    protected:
 
35
 
 
36
        template<typename K>
 
37
        bool found_type(K element)
 
38
        {
 
39
            if(std::is_same<const T*,K>::value)
 
40
                _value = true;
 
41
            return _value;
 
42
        }
 
43
        
 
44
        virtual void _accept(const NotCondition* element) override 
 
45
        { 
 
46
            if(found_type(element)) return;
 
47
            (*element)[0]->visit(*this);
 
48
        }
 
49
        virtual void _accept(const PetriEngine::PQL::AndCondition* element) override
 
50
        { 
 
51
            if(found_type(element)) return;
 
52
            for(auto& e : *element)
 
53
            {
 
54
                e->visit(*this);
 
55
                if(_value) return;
 
56
            }
 
57
        }
 
58
 
 
59
        virtual void _accept(const OrCondition* element) override
 
60
        { 
 
61
            if(found_type(element)) return;
 
62
            for(auto& e : *element)
 
63
            {
 
64
                e->visit(*this);
 
65
                if(_value) return;
 
66
            }
 
67
        }
 
68
        
 
69
        template<typename K>
 
70
        void handleCompare(const CompareCondition* element)
 
71
        {
 
72
            if(found_type(element)) return;
 
73
            (*element)[0]->visit(*this);
 
74
            if(_value) return;
 
75
            (*element)[1]->visit(*this);            
 
76
        }
 
77
 
 
78
        virtual void _accept(const LessThanCondition* element) override
 
79
        { 
 
80
            handleCompare<decltype(element)>(element);
 
81
        }
 
82
        
 
83
        virtual void _accept(const LessThanOrEqualCondition* element) override
 
84
        { 
 
85
            handleCompare<decltype(element)>(element);
 
86
        }
 
87
        
 
88
        virtual void _accept(const GreaterThanCondition* element) override
 
89
        { 
 
90
            handleCompare<decltype(element)>(element);
 
91
        }
 
92
        
 
93
        virtual void _accept(const GreaterThanOrEqualCondition* element) override
 
94
        { 
 
95
            handleCompare<decltype(element)>(element);
 
96
        }
 
97
        
 
98
        virtual void _accept(const NotEqualCondition* element) override
 
99
        { 
 
100
            handleCompare<decltype(element)>(element);
 
101
        }
 
102
 
 
103
        virtual void _accept(const EqualCondition* element) override
 
104
        { 
 
105
            handleCompare<decltype(element)>(element);
 
106
        }        
 
107
        
 
108
        virtual void _accept(const IdentifierExpr* element) override
 
109
        { 
 
110
            if(found_type(element)) return;
 
111
        }        
 
112
 
 
113
        virtual void _accept(const LiteralExpr* element) override
 
114
        { 
 
115
            if(found_type(element)) return;
 
116
        }
 
117
        
 
118
        virtual void _accept(const UnfoldedIdentifierExpr* element) override
 
119
        { 
 
120
            if(found_type(element)) return;
 
121
        }
 
122
        
 
123
        template<typename K>
 
124
        void handleNaryExpr(K element)
 
125
        {
 
126
            if(found_type(element)) return;
 
127
            for(auto& e : element->expressions())
 
128
            {
 
129
                e->visit(*this);
 
130
                if(_value) return;
 
131
            }            
 
132
        }
 
133
        
 
134
        virtual void _accept(const PlusExpr* element) override
 
135
        { 
 
136
            handleNaryExpr<decltype(element)>(element);
 
137
        }
 
138
 
 
139
        virtual void _accept(const MultiplyExpr* element) override
 
140
        { 
 
141
            handleNaryExpr<decltype(element)>(element);
 
142
        }
 
143
        
 
144
        virtual void _accept(const MinusExpr* element) override
 
145
        { 
 
146
            if(found_type(element)) return;
 
147
            (*element)[0]->visit(*this);
 
148
        }
 
149
        
 
150
        virtual void _accept(const SubtractExpr* element) override
 
151
        { 
 
152
            handleNaryExpr<decltype(element)>(element);
 
153
        }
 
154
 
 
155
        virtual void _accept(const DeadlockCondition* element) override
 
156
        { 
 
157
            if(found_type(element)) return;
 
158
        }        
 
159
        
 
160
        virtual void _accept(const CompareConjunction* element) override
 
161
        { 
 
162
            if(found_type(element)) return;
 
163
        }        
 
164
        
 
165
        virtual void _accept(const UnfoldedUpperBoundsCondition* element) override
 
166
        { 
 
167
            if(found_type(element)) return;
 
168
        }
 
169
 
 
170
        template<typename K>
 
171
        void handleSimpleQuantifierCondition(K element)
 
172
        {
 
173
            if(found_type(element)) return;
 
174
            (*element)[0]->visit(*this);
 
175
        }
 
176
        
 
177
        virtual void _accept(const EFCondition* el)
 
178
        {   handleSimpleQuantifierCondition(el); }
 
179
        virtual void _accept(const EGCondition* el)
 
180
        {   handleSimpleQuantifierCondition(el); }
 
181
        virtual void _accept(const AGCondition* el)
 
182
        {   handleSimpleQuantifierCondition(el); }
 
183
        virtual void _accept(const AFCondition* el)
 
184
        {   handleSimpleQuantifierCondition(el); }
 
185
        virtual void _accept(const EXCondition* el)
 
186
        {   handleSimpleQuantifierCondition(el); }
 
187
        virtual void _accept(const AXCondition* el)
 
188
        {   handleSimpleQuantifierCondition(el); }
 
189
        
 
190
        virtual void _accept(const EUCondition* el)
 
191
        {   
 
192
            if(found_type(el)) return;
 
193
            (*el)[0]->visit(*this);
 
194
            if(_value) return;
 
195
            (*el)[1]->visit(*this);
 
196
        }
 
197
        
 
198
        virtual void _accept(const AUCondition* el)
 
199
        {   
 
200
            if(found_type(el)) return;
 
201
            (*el)[0]->visit(*this);
 
202
            if(_value) return;
 
203
            (*el)[1]->visit(*this);
 
204
        }
 
205
 
 
206
        // shallow elements, neither of these should exist in a compiled expression
 
207
        virtual void _accept(const UnfoldedFireableCondition* element) 
 
208
        {   found_type(element); };
 
209
        virtual void _accept(const FireableCondition* element)
 
210
        {   found_type(element); };
 
211
        virtual void _accept(const UpperBoundsCondition* element)
 
212
        {   found_type(element); };
 
213
        virtual void _accept(const LivenessCondition* element)
 
214
        {   found_type(element); };
 
215
        virtual void _accept(const KSafeCondition* element)
 
216
        {   found_type(element); };
 
217
        virtual void _accept(const QuasiLivenessCondition* element)
 
218
        {   found_type(element); };
 
219
        virtual void _accept(const StableMarkingCondition* element)
 
220
        {   found_type(element); };
 
221
        virtual void _accept(const BooleanCondition* element)
 
222
        {   found_type(element); };
 
223
        
 
224
        
 
225
    };
 
226
}
 
227
 
 
228
 
 
229
#endif /* CONTAINSVISITOR_H */
 
230