← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to PetriParse/QueryBinaryParser.cpp

  • 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:
PetriParse/QueryBinaryParser.cpp
1
 
/* VerifyPN - TAPAAL Petri Net Engine
2
 
 * Copyright (C) 2017 Peter Gjøl Jensen <root@petergjoel.dk>
3
 
 * This program is free software: you can redistribute it and/or modify
4
 
 * it under the terms of the GNU General Public License as published by
5
 
 * the Free Software Foundation, either version 3 of the License, or
6
 
 * (at your option) any later version.
7
 
 *
8
 
 * This program is distributed in the hope that it will be useful,
9
 
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
10
 
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
11
 
 * GNU General Public License for more details.
12
 
 *
13
 
 * You should have received a copy of the GNU General Public License
14
 
 * along with this program. If not, see <http://www.gnu.org/licenses/>.
15
 
 */
16
 
 
17
 
#include <memory>
18
 
 
19
 
#include "QueryBinaryParser.h"
20
 
#include "PetriEngine/PQL/Expressions.h"
21
 
 
22
 
bool QueryBinaryParser::parse(std::ifstream& bin, const std::set<size_t>& parse_only) {
23
 
    //Parse the xml
24
 
    uint32_t numq;
25
 
    bin.read(reinterpret_cast<char*>(&numq), sizeof(uint32_t));
26
 
    std::vector<std::string> names;
27
 
    uint32_t nnames;
28
 
    bin.read(reinterpret_cast<char*>(&nnames), sizeof(uint32_t));
29
 
    names.resize(nnames);
30
 
    for(uint32_t i = 0; i < nnames; ++i)
31
 
    {
32
 
        uint32_t id;
33
 
        bin.read(reinterpret_cast<char*>(&id), sizeof(uint32_t));
34
 
        std::getline(bin, names[id], '\0');
35
 
    }
36
 
 
37
 
    bool parsingOK = true;
38
 
    for(uint32_t i = 0; i < numq; ++i)
39
 
    {
40
 
        queries.emplace_back();
41
 
        std::getline(bin, queries.back().id, '\0');
42
 
        queries.back().query = parseQuery(bin, names);
43
 
        if(queries.back().query == nullptr)
44
 
        {
45
 
            queries.back().parsingResult = QueryItem::UNSUPPORTED_QUERY;
46
 
            parsingOK = false;
47
 
        }
48
 
        else
49
 
            queries.back().parsingResult = QueryItem::PARSING_OK;
50
 
    }
51
 
    //Release DOM tree
52
 
    return parsingOK;
53
 
}
54
 
 
55
 
Condition_ptr QueryBinaryParser::parseQuery(std::ifstream& binary, const std::vector<std::string>& names)
56
 
{
57
 
    Path p;
58
 
    binary.read(reinterpret_cast<char*>(&p), sizeof(Path));
59
 
    Quantifier q;
60
 
    binary.read(reinterpret_cast<char*>(&q), sizeof(Quantifier));
61
 
    if(p == pError)
62
 
    {
63
 
        if(q == Quantifier::NEG)
64
 
        {
65
 
            auto c = parseQuery(binary, names);
66
 
            if(c == nullptr)
67
 
            {
68
 
                assert(false);
69
 
                return nullptr;
70
 
            }
71
 
            return std::make_shared<NotCondition>(c);
72
 
        }
73
 
        else if(q == Quantifier::DEADLOCK)
74
 
        {
75
 
            return DeadlockCondition::DEADLOCK;
76
 
        }
77
 
        else if(q == Quantifier::PN_BOOLEAN)
78
 
        {
79
 
            bool val;
80
 
            binary.read(reinterpret_cast<char*>(&val), sizeof(bool));
81
 
            return BooleanCondition::getShared(val);
82
 
        }
83
 
        else if(q == Quantifier::AND || q == Quantifier::OR)
84
 
        {
85
 
            uint32_t size;
86
 
            binary.read(reinterpret_cast<char*>(&size), sizeof(uint32_t));
87
 
            std::vector<Condition_ptr> conds;
88
 
            for(uint32_t i = 0; i < size; ++i)
89
 
            {
90
 
                conds.push_back(parseQuery(binary, names));
91
 
                if(conds.back() == nullptr) return nullptr;
92
 
            }
93
 
            if(q == Quantifier::AND)
94
 
                return std::make_shared<AndCondition>(std::move(conds));
95
 
            else
96
 
                return std::make_shared<OrCondition>(std::move(conds));
97
 
        }
98
 
        else if(q == Quantifier::COMPCONJ)
99
 
        {
100
 
            bool neg;
101
 
            binary.read(reinterpret_cast<char*>(&neg), sizeof(bool));   
102
 
            std::vector<CompareConjunction::cons_t> cons;
103
 
            uint32_t size;
104
 
            binary.read(reinterpret_cast<char*>(&size), sizeof(uint32_t));            
105
 
            for(uint32_t i = 0; i < size; ++i)
106
 
            {
107
 
                cons.emplace_back();
108
 
                binary.read(reinterpret_cast<char*>(&cons.back()._place), sizeof(uint32_t));
109
 
                binary.read(reinterpret_cast<char*>(&cons.back()._lower), sizeof(uint32_t));
110
 
                binary.read(reinterpret_cast<char*>(&cons.back()._upper), sizeof(uint32_t));
111
 
                cons.back()._name = names[cons.back()._place];
112
 
            }
113
 
            return std::make_shared<CompareConjunction>(std::move(cons), neg);
114
 
        }
115
 
        else if(q == Quantifier::EMPTY)
116
 
        {
117
 
            std::string sop;
118
 
            std::getline(binary, sop, '\0');
119
 
            auto e1 = parseExpr(binary, names);
120
 
            auto e2 = parseExpr(binary, names);
121
 
            if(e1 == nullptr || e2 == nullptr)
122
 
            {
123
 
                assert(false);
124
 
                return nullptr;
125
 
            }
126
 
            if(sop == "<")
127
 
                return std::make_shared<LessThanCondition>(e1, e2);
128
 
            else if(sop == "<=")
129
 
                return std::make_shared<LessThanOrEqualCondition>(e1, e2);
130
 
            else if(sop == ">=")
131
 
                return std::make_shared<GreaterThanOrEqualCondition>(e1, e2);
132
 
            else if(sop == ">")
133
 
                return std::make_shared<GreaterThanCondition>(e1, e2);
134
 
            else if(sop == "==")
135
 
                return std::make_shared<EqualCondition>(e1, e2);
136
 
            else if(sop == "!=")
137
 
                return std::make_shared<NotEqualCondition>(e1, e2);
138
 
            else
139
 
            {
140
 
                assert(false);
141
 
                return nullptr;
142
 
            }
143
 
        }
144
 
        else if(q == Quantifier::UPPERBOUNDS)
145
 
        {
146
 
            uint32_t size;
147
 
            size_t max;
148
 
            binary.read(reinterpret_cast<char*>(&size), sizeof(uint32_t));            
149
 
            binary.read(reinterpret_cast<char*>(&max), sizeof(size_t));            
150
 
            std::vector<UnfoldedUpperBoundsCondition::place_t> places;
151
 
            for(size_t i = 0; i < size; ++i)
152
 
            {
153
 
                uint32_t id;
154
 
                binary.read(reinterpret_cast<char*>(&id), sizeof(uint32_t));
155
 
                places.emplace_back(names[id]);
156
 
                places.back()._place = id;
157
 
            }
158
 
            return std::make_shared<UnfoldedUpperBoundsCondition>(places, max);
159
 
        }
160
 
        else
161
 
        {
162
 
            assert(false);
163
 
            return nullptr;
164
 
        }
165
 
    }
166
 
    else
167
 
    {
168
 
        Condition_ptr cond1 = parseQuery(binary, names);
169
 
        assert(cond1);
170
 
        if(!cond1) return nullptr;
171
 
        if(p == Path::X)
172
 
        {
173
 
            if(q == Quantifier::A)
174
 
                return std::make_shared<AXCondition>(cond1);
175
 
            else
176
 
                return std::make_shared<EXCondition>(cond1);
177
 
        }
178
 
        else if(p == Path::F)
179
 
        {
180
 
            if(q == Quantifier::A)
181
 
                return std::make_shared<AFCondition>(cond1);
182
 
            else
183
 
                return std::make_shared<EFCondition>(cond1);
184
 
        }
185
 
        else if(p == Path::G)
186
 
        {
187
 
            if(q == Quantifier::A)
188
 
                return std::make_shared<AGCondition>(cond1);
189
 
            else
190
 
                return std::make_shared<EGCondition>(cond1);
191
 
        }
192
 
        else if(p == Path::U)
193
 
        {
194
 
            auto cond2 = parseQuery(binary, names);
195
 
            if(cond2 == nullptr)
196
 
            {
197
 
                assert(false);
198
 
                return nullptr;
199
 
            }
200
 
            if(q == Quantifier::A)
201
 
                return std::make_shared<AUCondition>(cond1, cond2);
202
 
            else
203
 
                return std::make_shared<EUCondition>(cond1, cond2);
204
 
        }
205
 
        else
206
 
        {
207
 
            assert(false);
208
 
            return nullptr;
209
 
        }
210
 
    }
211
 
    assert(false);
212
 
    return nullptr;
213
 
}
214
 
 
215
 
Expr_ptr QueryBinaryParser::parseExpr(std::ifstream& bin, const std::vector<std::string>& names) {
216
 
    char t;
217
 
    bin.read(&t, sizeof(char));
218
 
    if(t == 'l')
219
 
    {
220
 
        int val;
221
 
        bin.read(reinterpret_cast<char*>(&val), sizeof(int));
222
 
        return std::make_shared<LiteralExpr>(val);
223
 
    }
224
 
    else if(t == 'i')
225
 
    {
226
 
        int offset;
227
 
        bin.read(reinterpret_cast<char*>(&offset), sizeof(int));
228
 
        return std::make_shared<UnfoldedIdentifierExpr>(names[offset], offset);
229
 
    }
230
 
    else if(t == '-')
231
 
    {
232
 
        uint32_t size;
233
 
        bin.read(reinterpret_cast<char*>(&size), sizeof(uint32_t));  
234
 
        std::vector<Expr_ptr> exprs;
235
 
        for(uint32_t i = 0; i < size; ++i)
236
 
        {
237
 
            exprs.push_back(parseExpr(bin, names));
238
 
            if(exprs.back() == nullptr)
239
 
            {
240
 
                assert(false);
241
 
                return nullptr;
242
 
            }
243
 
        }
244
 
        return std::make_shared<SubtractExpr>(std::move(exprs));
245
 
    }
246
 
    else if(t == '*' || t == '+')
247
 
    {
248
 
        int32_t constant;
249
 
        uint32_t idsize;
250
 
        uint32_t exprssize;
251
 
        bin.read(reinterpret_cast<char*>(&constant), sizeof(int32_t));  
252
 
        bin.read(reinterpret_cast<char*>(&idsize), sizeof(uint32_t));  
253
 
        bin.read(reinterpret_cast<char*>(&exprssize), sizeof(uint32_t));  
254
 
        std::vector<uint32_t> ids(idsize);
255
 
        bin.read(reinterpret_cast<char*>(ids.data()), sizeof(uint32_t)*idsize);
256
 
        std::vector<Expr_ptr> exprs;
257
 
        exprs.push_back(std::make_shared<LiteralExpr>(constant));
258
 
        for(auto i : ids)
259
 
        {
260
 
            exprs.push_back(std::make_shared<UnfoldedIdentifierExpr>(names[i], i));
261
 
        }
262
 
        for(uint32_t i = 0; i < exprssize; ++i)
263
 
        {
264
 
            exprs.push_back(parseExpr(bin, names));
265
 
            if(exprs.back() == nullptr)
266
 
            {
267
 
                assert(false);
268
 
                return nullptr;
269
 
            }
270
 
        }
271
 
        if(t == '*')
272
 
            return std::make_shared<MultiplyExpr>(std::move(exprs));
273
 
        else
274
 
            return std::make_shared<PlusExpr>(std::move(exprs));
275
 
        
276
 
    }
277
 
    else
278
 
    {
279
 
        std::cerr << "An error occurred parsing the binary input." << std::endl;
280
 
        std::cerr << t << std::endl;
281
 
        assert(false);
282
 
        exit(ErrorCode);
283
 
        return nullptr;
284
 
    }
285
 
}