← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to include/PetriEngine/Simplification/Member.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/Simplification/Member.h
 
1
#ifndef MEMBER_H
 
2
#define MEMBER_H
 
3
#include <algorithm>
 
4
#include <functional>
 
5
#include <cassert>
 
6
#include <cstring>
 
7
//#include "../PQL/PQL.h"
 
8
 
 
9
namespace PetriEngine {
 
10
    namespace Simplification {
 
11
        enum Trivial { False=0, True=1, Indeterminate=2 };
 
12
        enum MemberType { Constant, Input, Output, Regular };
 
13
        class Member {
 
14
            std::vector<int> _variables;
 
15
            int _constant = 0;
 
16
            bool _canAnalyze = false;
 
17
 
 
18
        public:
 
19
 
 
20
            Member(std::vector<int>&& vec, int constant, bool canAnalyze = true) 
 
21
                    : _variables(vec), _constant(constant), _canAnalyze(canAnalyze) {
 
22
            }
 
23
            Member(int constant, bool canAnalyse = true) 
 
24
                    : _constant(constant), _canAnalyze(canAnalyse) {
 
25
            }
 
26
            Member(){}
 
27
 
 
28
            virtual ~Member(){}
 
29
            
 
30
            int constant() const    { return _constant; };
 
31
            bool canAnalyze() const { return _canAnalyze; };
 
32
            size_t size() const     { return _variables.size(); }
 
33
            std::vector<int>& variables() { return _variables; }
 
34
            const std::vector<int>& variables() const { return _variables; }
 
35
            
 
36
            Member& operator+=(const Member& m) { 
 
37
                auto tc = _constant + m._constant;
 
38
                auto ca = _canAnalyze && m._canAnalyze;                
 
39
                addVariables(m);
 
40
                _constant = tc;
 
41
                _canAnalyze = ca;
 
42
                return *this;
 
43
            }
 
44
            
 
45
            Member& operator-=(const Member& m) { 
 
46
                auto tc = _constant - m._constant;
 
47
                auto ca = _canAnalyze && m._canAnalyze;                
 
48
                subtractVariables(m);
 
49
                _constant = tc;
 
50
                _canAnalyze = ca;
 
51
                return *this;
 
52
            }
 
53
            
 
54
            Member& operator*=(const Member& m) { 
 
55
                if(!isZero() && !m.isZero()){
 
56
                    _canAnalyze = false;
 
57
                    _constant = 0;
 
58
                    _variables.clear();
 
59
                } else{
 
60
                    auto tc = _constant * m._constant;
 
61
                    auto ca = _canAnalyze && m._canAnalyze;
 
62
                    multiply(m);
 
63
                    _constant = tc;
 
64
                    _canAnalyze = ca;
 
65
                }
 
66
                return *this;
 
67
            }            
 
68
 
 
69
            bool substrationIsZero(const Member& m2) const
 
70
            {
 
71
                uint32_t min = std::min(_variables.size(), m2._variables.size());
 
72
                uint32_t i = 0;
 
73
                for(; i < min; i++) {
 
74
                    if(_variables[i] != m2._variables[i]) return false;
 
75
                }
 
76
                
 
77
                for(; i < _variables.size(); ++i)
 
78
                {
 
79
                    if(_variables[i] != 0) return false;
 
80
                }
 
81
 
 
82
                for(; i < m2._variables.size(); ++i)
 
83
                {
 
84
                    if(m2._variables[i] != 0) return false;
 
85
                }
 
86
                return true;
 
87
            }
 
88
            
 
89
            bool isZero() const {
 
90
                for(const int& v : _variables){
 
91
                    if(v != 0) return false;
 
92
                }
 
93
                return true;
 
94
            }
 
95
            
 
96
            MemberType getType() const {
 
97
                bool isConstant = true;
 
98
                bool isInput = true;
 
99
                bool isOutput = true;
 
100
                for(const int& v : _variables){
 
101
                    if(v < 0){
 
102
                        isConstant = false;
 
103
                        isOutput = false;
 
104
                    } else if(v > 0){
 
105
                        isConstant = false;
 
106
                        isInput = false;
 
107
                    }
 
108
                }
 
109
                if(isConstant) return MemberType::Constant;
 
110
                else if(isInput) return MemberType::Input;
 
111
                else if(isOutput) return MemberType::Output;
 
112
                else return MemberType::Regular;
 
113
            }
 
114
            
 
115
            bool operator==(const Member& m) const {
 
116
                size_t min = std::min(_variables.size(), m.size());
 
117
                size_t max = std::max(_variables.size(), m.size());
 
118
                if(memcmp(_variables.data(), m._variables.data(), sizeof(int)*min) != 0)
 
119
                {
 
120
                    return false;
 
121
                }
 
122
                for (uint32_t i = min; i < max; i++) {
 
123
                    if (i >= _variables.size()) {
 
124
                        if(m._variables[i] != 0) return false;
 
125
                    } else if (i >= m._variables.size()) {
 
126
                        if(_variables[i] != 0) return false;
 
127
                    } else {
 
128
                        assert(false);
 
129
                        if(_variables[i] - m._variables[i] != 0) return false;
 
130
                    }
 
131
                }
 
132
                return true;
 
133
            }
 
134
 
 
135
            Trivial operator<(const Member& m) const {
 
136
                return trivialLessThan(m, std::less<int>());
 
137
            }
 
138
            Trivial operator<=(const Member& m) const {
 
139
                return trivialLessThan(m, std::less_equal<int>());
 
140
            }
 
141
            Trivial operator>(const Member& m) const {
 
142
                return m.trivialLessThan(*this, std::less<int>());
 
143
            }
 
144
            Trivial operator>=(const Member& m) const {
 
145
                return m.trivialLessThan(*this, std::less_equal<int>());
 
146
            }
 
147
            
 
148
        private:
 
149
            void addVariables(const Member& m2) {
 
150
                uint32_t size = std::max(_variables.size(), m2._variables.size());
 
151
                _variables.resize(size, 0);
 
152
 
 
153
                for (uint32_t i = 0; i < size; i++) {
 
154
                    if (i >= m2._variables.size()) {
 
155
                        break;
 
156
                    } else {
 
157
                        _variables[i] += m2._variables[i];
 
158
                    }
 
159
                }
 
160
            }
 
161
 
 
162
            void subtractVariables(const Member& m2) {
 
163
                uint32_t size = std::max(_variables.size(), m2._variables.size());
 
164
                _variables.resize(size, 0);
 
165
                
 
166
                for (uint32_t i = 0; i < size; i++) {
 
167
                    if (i >= m2._variables.size()) {
 
168
                        break;
 
169
                    } else {
 
170
                        _variables[i] -= m2._variables[i];
 
171
                    }
 
172
                }           
 
173
            }
 
174
 
 
175
            void multiply(const Member& m2) {
 
176
 
 
177
                if (isZero() != m2.isZero()){
 
178
                    if (!isZero()){
 
179
                        for(auto& v : _variables) v *= m2._constant;
 
180
                        return;
 
181
                    } else if (!m2.isZero()){
 
182
                        _variables = m2._variables;
 
183
                        for(auto& v : _variables) v *= _constant;
 
184
                        return;
 
185
                    }
 
186
                }
 
187
                _variables.clear();
 
188
            }
 
189
            
 
190
            Trivial trivialLessThan(const Member& m2, std::function<bool (int, int)> compare) const {
 
191
                MemberType type1 = getType();
 
192
                MemberType type2 = m2.getType();
 
193
                
 
194
                // self comparison
 
195
                if (*this == m2)
 
196
                    return compare(_constant, m2._constant) ? Trivial::True : Trivial::False;
 
197
                    
 
198
                // constant < constant/input/output
 
199
                if (type1 == MemberType::Constant){
 
200
                    if(type2 == MemberType::Constant){
 
201
                        return compare(_constant, m2._constant) ? Trivial::True : Trivial::False;
 
202
                    }
 
203
                    else if(type2 == MemberType::Input && !compare(_constant, m2._constant)){
 
204
                        return Trivial::False;
 
205
                    } 
 
206
                    else if(type2 == MemberType::Output && compare(_constant, m2._constant)){
 
207
                        return Trivial::True;
 
208
                    } 
 
209
                } 
 
210
                // input < output/constant
 
211
                else if (type1 == MemberType::Input 
 
212
                        && (type2 == MemberType::Constant || type2 == MemberType::Output) 
 
213
                        && compare(_constant, m2._constant)) {
 
214
                    return Trivial::True;
 
215
                } 
 
216
                // output < input/constant
 
217
                else if (type1 == MemberType::Output 
 
218
                        && (type2 == MemberType::Constant || type2 == MemberType::Input) 
 
219
                        && !compare(_constant, m2._constant)) {
 
220
                    return Trivial::False;
 
221
                } 
 
222
                return Trivial::Indeterminate;
 
223
            }
 
224
 
 
225
        };
 
226
    }
 
227
}
 
228
 
 
229
#endif /* MEMBER_H */