← Back to branch summary

~tapaal-dist/verifypn/LTSmin

« back to all changes in this revision

Viewing changes to PetriParse/QueryXMLParser.cpp

  • Committer: Jiri Srba
  • Date: 2014-05-18 17:03:05 UTC
  • mfrom: (44.2.52 sumoXMLparsing)
  • Revision ID: srba@cs.aau.dk-20140518170305-jzggi1p4r4n32ydp
merged in a branch adding a parser for XMP competition queries
launch script is added too

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriParse/QueryXMLParser.cpp
 
1
/* VerifyPN - TAPAAL Petri Net Engine
 
2
 * Copyright (C) 2014 Jiri Srba <srba.jiri@gmail.com>
 
3
 *
 
4
 * This program is free software: you can redistribute it and/or modify
 
5
 * it under the terms of the GNU General Public License as published by
 
6
 * the Free Software Foundation, either version 3 of the License, or
 
7
 * (at your option) any later version.
 
8
 *
 
9
 * This program is distributed in the hope that it will be useful,
 
10
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 
11
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 
12
 * GNU General Public License for more details.
 
13
 *
 
14
 * You should have received a copy of the GNU General Public License
 
15
 * along with this program. If not, see <http://www.gnu.org/licenses/>.
 
16
 */
 
17
 
 
18
#include "QueryXMLParser.h"
 
19
 
 
20
#include <string>
 
21
#include <stdio.h>
 
22
#include <stdlib.h>
 
23
#include <iostream>
 
24
#include <sstream> 
 
25
#include <algorithm> 
 
26
 
 
27
using namespace XMLSP;
 
28
using namespace std;
 
29
 
 
30
QueryXMLParser::QueryXMLParser(const PNMLParser::TransitionEnablednessMap &transitionEnabledness) {
 
31
        _transitionEnabledness = transitionEnabledness;
 
32
};
 
33
 
 
34
// QueryXMLParser::~QueryXMLParser() { };
 
35
 
 
36
 
 
37
bool QueryXMLParser::parse(const std::string& xml){
 
38
        //Parse the xml
 
39
        DOMElement* root = DOMElement::loadXML(xml);
 
40
        bool parsingOK;
 
41
        if (root) {
 
42
                parsingOK = parsePropertySet(root);
 
43
        } else {
 
44
                parsingOK=false;
 
45
        }
 
46
                
 
47
        //Release DOM tree
 
48
        delete root;
 
49
        return parsingOK;
 
50
}
 
51
 
 
52
 
 
53
bool QueryXMLParser::parsePropertySet(DOMElement* element){
 
54
        if (element->getElementName()!="property-set") {
 
55
                fprintf(stderr,"ERROR missing property-set\n");
 
56
                return false; // missing property-set element
 
57
        }
 
58
        DOMElements elements = element->getChilds();
 
59
        DOMElements::iterator it;
 
60
        for(it = elements.begin(); it != elements.end(); it++){
 
61
                if (!parseProperty(*it)) {
 
62
                        return false;
 
63
                };
 
64
        }
 
65
        return true;
 
66
}
 
67
 
 
68
bool QueryXMLParser::parseProperty(DOMElement* element){
 
69
        if (element->getElementName()!="property") {
 
70
                fprintf(stderr,"ERROR missing property\n");
 
71
                return false; // unexpected element (only property is allowed)
 
72
        }
 
73
        string id;
 
74
        string queryText;
 
75
        bool negateResult=false;
 
76
    bool isPlaceBound=false;
 
77
        string placeNameForBound;
 
78
        bool tagsOK=true;
 
79
        
 
80
        DOMElements elements = element->getChilds();
 
81
        DOMElements::iterator it;
 
82
        DOMElements::iterator formulaPtr;
 
83
        for(it = elements.begin(); it != elements.end(); it++){
 
84
                if ((*it)->getElementName()=="id") {
 
85
                        id = (*it)->getCData();
 
86
                } else if ((*it)->getElementName()=="formula") {
 
87
                        formulaPtr=it;
 
88
                } else if ((*it)->getElementName()=="tags") {
 
89
                        tagsOK=parseTags(*it);
 
90
                }
 
91
        }
 
92
        
 
93
        if (id=="") {
 
94
                fprintf(stderr,"ERROR a query with empty id\n");
 
95
                return false;
 
96
        }
 
97
        
 
98
        QueryItem queryItem;
 
99
        queryItem.id=id;
 
100
        if (tagsOK && parseFormula(*formulaPtr, queryText, negateResult, isPlaceBound, placeNameForBound)) {
 
101
                queryItem.queryText=queryText;
 
102
                queryItem.negateResult=negateResult;
 
103
        queryItem.isPlaceBound=isPlaceBound;
 
104
                queryItem.placeNameForBound=placeNameForBound;
 
105
                queryItem.parsingResult=QueryItem::PARSING_OK;
 
106
        } else {
 
107
                queryItem.queryText="";
 
108
                queryItem.negateResult=false;
 
109
        queryItem.isPlaceBound=false;
 
110
                queryItem.placeNameForBound="";
 
111
                queryItem.parsingResult=QueryItem::UNSUPPORTED_QUERY;
 
112
        }       
 
113
        queries.push_back(queryItem);
 
114
        return true;
 
115
}
 
116
 
 
117
bool QueryXMLParser::parseTags(DOMElement* element){
 
118
        // we can accept only reachability query
 
119
        DOMElements elements = element->getChilds();
 
120
        DOMElements::iterator it;
 
121
        for(it = elements.begin(); it != elements.end(); it++){
 
122
                if ((*it)->getElementName()=="is-reachability" && (*it)->getCData()!="true") {
 
123
                        return false;
 
124
                }
 
125
        }
 
126
        return true;
 
127
}
 
128
 
 
129
bool QueryXMLParser::parseFormula(DOMElement* element, string &queryText, bool &negateResult, bool &isPlaceBound, string &placeNameForBound){
 
130
        /*
 
131
         Describe here how to parse
 
132
         * INV phi =  AG phi =  not EF not phi
 
133
         * IMPOS phi = AG not phi = not EF phi
 
134
         * POS phi = EF phi
 
135
         * NEG INV phi = not AG phi = EF not phi
 
136
         * NEG IMPOS phi = not AG not phi = EF phi
 
137
         * NEG POS phi = not EF phi
 
138
         */
 
139
        DOMElements elements = element->getChilds();
 
140
        if (elements.size() != 1) {
 
141
                return false;
 
142
        }
 
143
        DOMElements::iterator booleanFormula = elements.begin();
 
144
        string elementName = (*booleanFormula)->getElementName(); 
 
145
        if (elementName=="invariant") {
 
146
                queryText="EF not(";
 
147
                negateResult=true;
 
148
        } else if (elementName=="impossibility") {
 
149
                queryText="EF ( ";
 
150
                negateResult=true;
 
151
        } else if (elementName=="possibility") {
 
152
                queryText="EF ( ";
 
153
                negateResult=false;
 
154
        } else if (elementName=="negation") {
 
155
                DOMElements children = (*elements.begin())->getChilds();
 
156
                if (children.size() !=1) {
 
157
                        return false;
 
158
                }
 
159
                booleanFormula = children.begin(); 
 
160
                string negElementName = (*booleanFormula)->getElementName();
 
161
                if (negElementName=="invariant") {
 
162
                        queryText="EF not( ";
 
163
                        negateResult=false;
 
164
                } else if (negElementName=="impossibility") {
 
165
                        queryText="EF ( ";
 
166
                        negateResult=false;
 
167
                } else if (negElementName=="possibility") {
 
168
                        queryText="EF ( ";
 
169
                        negateResult=true;
 
170
                } else {
 
171
                        return false;
 
172
                }
 
173
    } else if (elementName == "place-bound") {
 
174
        queryText = "EF ";
 
175
        DOMElements children = (*booleanFormula)->getChilds();
 
176
        if (children.size() != 1) {
 
177
            return false; // we support only place-bound for one place
 
178
        }
 
179
        if (children[0]->getElementName() != "place") {
 
180
            return false;
 
181
        }
 
182
        placeNameForBound = parsePlace(children[0]);
 
183
                if (placeNameForBound=="") {
 
184
                        return false; // invalid place name
 
185
                }
 
186
        queryText += "\""+placeNameForBound+"\""+" < 0";
 
187
        negateResult = false;
 
188
        isPlaceBound = true;
 
189
        return true;
 
190
    } else {
 
191
            return false;
 
192
        }
 
193
        DOMElements nextElements = (*booleanFormula)->getChilds();
 
194
        if (nextElements.size() !=1 || !parseBooleanFormula(nextElements[0] , queryText)) {
 
195
                return false;
 
196
        }
 
197
        queryText+=" )";
 
198
    isPlaceBound=false;
 
199
        placeNameForBound = "";
 
200
        return true;
 
201
}
 
202
 
 
203
bool QueryXMLParser::parseBooleanFormula(DOMElement* element, string &queryText){
 
204
                string elementName = element->getElementName();
 
205
                if (elementName == "deadlock") {
 
206
                        queryText+="deadlock";
 
207
                        return true;
 
208
                } else if (elementName == "true") {
 
209
                        queryText+="true";
 
210
                        return true;
 
211
                } else if (elementName == "false") {
 
212
                        queryText+="false";
 
213
                        return true;
 
214
                } else if (elementName == "negation") {
 
215
                        DOMElements children = element->getChilds();
 
216
                        queryText+="not(";
 
217
                        if (children.size()==1 && parseBooleanFormula(children[0], queryText)) {
 
218
                                queryText+=")";
 
219
                        } else {
 
220
                                return false;
 
221
                        }
 
222
                        return true;
 
223
                } else if (elementName == "conjunction") {
 
224
                        DOMElements children = element->getChilds();
 
225
                        if (children.size()<2) {
 
226
                                return false;
 
227
                        }
 
228
                        if (!(parseBooleanFormula((children[0]), queryText))) {
 
229
                                return false;
 
230
                        }
 
231
                        DOMElements::iterator it;
 
232
                        for(it = (children.begin())+1; it != children.end(); it++) {
 
233
                                queryText+=" and ";
 
234
                                if (!(parseBooleanFormula(*it, queryText))) {
 
235
                                        return false;
 
236
                                }
 
237
                        }
 
238
                        return true;
 
239
                } else if (elementName == "disjunction") {
 
240
                        DOMElements children = element->getChilds();
 
241
                        if (children.size()<2) {
 
242
                                return false;
 
243
                        }
 
244
                        if (!(parseBooleanFormula(*children.begin(), queryText))) {
 
245
                                return false;
 
246
                        }
 
247
                        DOMElements::iterator it;
 
248
                        for(it = children.begin()+1; it != children.end(); it++) {
 
249
                                queryText+=" or ";
 
250
                                if (!(parseBooleanFormula(*it, queryText))) {
 
251
                                        return false;   
 
252
                                }
 
253
                        }
 
254
                        return true;
 
255
                } else if (elementName == "exclusive-disjunction") {
 
256
                        DOMElements children = element->getChilds();
 
257
                        if (children.size()!=2) { // we support only two subformulae here
 
258
                                return false;
 
259
                        }
 
260
                        string subformula1;
 
261
                        string subformula2;
 
262
                        if (!(parseBooleanFormula(*(children.begin()), subformula1))) {
 
263
                                return false;
 
264
                        }
 
265
                        if (!(parseBooleanFormula(*(children.begin()+1), subformula2))) {
 
266
                                return false;
 
267
                        }
 
268
                        queryText+= "(("+subformula1+" and not("+subformula2+")) or (not("+subformula1+") and "+subformula2+"))";
 
269
                        return true;
 
270
                } else if (elementName == "implication") {
 
271
                        DOMElements children = element->getChilds();
 
272
                        if (children.size()!=2) { // implication has only two subformulae
 
273
                                return false;
 
274
                        }
 
275
                        string subformula1;
 
276
                        string subformula2;
 
277
                        if (!(parseBooleanFormula(*(children.begin()), subformula1))) {
 
278
                                return false;
 
279
                        }
 
280
                        if (!(parseBooleanFormula(*(children.begin()+1), subformula2))) {
 
281
                                return false;
 
282
                        }
 
283
                        queryText+= "not("+subformula1+") or ( "+subformula2+" )";
 
284
                        return true;
 
285
                } else if (elementName == "equivalence") {
 
286
                        DOMElements children = element->getChilds();
 
287
                        if (children.size()!=2) { // we support only two subformulae here
 
288
                                return false;
 
289
                        }
 
290
                        string subformula1;
 
291
                        string subformula2;
 
292
                        if (!(parseBooleanFormula(*(children.begin()), subformula1))) {
 
293
                                return false;
 
294
                        }
 
295
                        if (!(parseBooleanFormula(*(children.begin()+1), subformula2))) {
 
296
                                return false;
 
297
                        }
 
298
                        queryText+= "(("+subformula1+" and "+subformula2+") or (not("+subformula1+") and not("+subformula2+")))";
 
299
                        return true;
 
300
                } else if (     elementName == "integer-eq" || 
 
301
                                        elementName == "integer-ne" || 
 
302
                                        elementName == "integer-lt" || 
 
303
                                        elementName == "integer-le" || 
 
304
                                        elementName == "integer-gt" || 
 
305
                                        elementName == "integer-ge") {
 
306
                        DOMElements children = element->getChilds();
 
307
                        if (children.size()!=2) { // exactly two integer subformulae are required
 
308
                                return false;
 
309
                        }
 
310
                        string subformula1;
 
311
                        string subformula2;
 
312
                        if (!(parseIntegerExpression(children[0], subformula1))) {
 
313
                                return false;
 
314
                        }
 
315
                        if (!(parseIntegerExpression(children[1], subformula2))) {
 
316
                                return false;
 
317
                        }
 
318
                        string mathoperator;
 
319
                        if              ( elementName == "integer-eq") mathoperator=" == ";
 
320
                        else if ( elementName == "integer-ne") mathoperator=" != ";
 
321
                        else if ( elementName == "integer-lt") mathoperator=" < ";
 
322
                        else if ( elementName == "integer-le") mathoperator=" <= ";
 
323
                        else if ( elementName == "integer-gt") mathoperator=" > ";
 
324
                        else if ( elementName == "integer-ge") mathoperator=" >= ";
 
325
                        
 
326
                        queryText+="("+subformula1+mathoperator+subformula2+")";
 
327
                        return true;
 
328
                } else if (elementName == "is-fireable") {
 
329
                        DOMElements children = element->getChilds();
 
330
                        if (children.size() == 0) {
 
331
                                return false;
 
332
                        }
 
333
                        if (children.size() > 1) {
 
334
                                queryText += "(";
 
335
                        }
 
336
                        for (int i = 0; i < children.size(); i++) {
 
337
                                if (children[i]->getElementName() != "transition") {
 
338
                                        return false;
 
339
                                }
 
340
                                if (i > 0) {
 
341
                                        queryText += " or ";
 
342
                                }
 
343
                                string transitionName = children[i]->getCData();
 
344
                                if(_transitionEnabledness.find(transitionName) == _transitionEnabledness.end()){
 
345
                                        fprintf(stderr,
 
346
                                                "XML Query Parsing error: Transition id=\"%s\" was not found!\n",
 
347
                                            transitionName.c_str());
 
348
                                        return false;
 
349
                            }
 
350
                                queryText += _transitionEnabledness[transitionName]; 
 
351
                        }
 
352
                        if (children.size() > 1) {
 
353
                                queryText += ")";
 
354
                        }
 
355
                        return true;
 
356
                }
 
357
        return false;
 
358
}
 
359
 
 
360
bool QueryXMLParser::parseIntegerExpression(DOMElement* element, string &queryText){
 
361
        string elementName = element->getElementName();
 
362
        if (elementName == "integer-constant") {
 
363
                int i;
 
364
                if(sscanf((element->getCData()).c_str(), "%d", &i)  == EOF ) { 
 
365
                        return false; // expected integer at this place
 
366
                }
 
367
                 stringstream ss;//create a stringstream
 
368
         ss << i;//add number to the stream
 
369
         queryText+=ss.str();
 
370
                return true;
 
371
        } else if (elementName == "tokens-count") {
 
372
                DOMElements children = element->getChilds();
 
373
                if (children.size()==0) {
 
374
                        return false;
 
375
                }
 
376
                if (children.size()>1) {
 
377
                        queryText+="(";
 
378
                }
 
379
                for (int i = 0; i < children.size(); i++) {
 
380
                        if (children[i]->getElementName() != "place") {
 
381
                                return false;
 
382
                        }
 
383
                        if (i > 0) {
 
384
                                queryText += " + ";
 
385
                        }
 
386
                        string placeName = parsePlace(children[i]);
 
387
                        if (placeName == "") {
 
388
                                return false; // invalid place name
 
389
                        }
 
390
                        queryText+="\""+placeName+"\"";
 
391
                }
 
392
                if (children.size()>1) {
 
393
                        queryText+=")";
 
394
                }
 
395
                return true;
 
396
        } else if (     elementName == "integer-sum" ||
 
397
                                elementName == "integer-product" ) {
 
398
                DOMElements children = element->getChilds();
 
399
                if (children.size() < 2) { // at least two integer subexpression are required
 
400
                        return false;
 
401
                }
 
402
                string mathoperator;
 
403
                if (     elementName == "integer-sum") mathoperator = " + ";
 
404
                else if (elementName == "integer-product") mathoperator = " * ";
 
405
                queryText+="(";
 
406
                for (int i = 0; i < children.size(); i++) {
 
407
                        if (i > 0) {
 
408
                                queryText+= mathoperator;
 
409
                        }
 
410
                        if (!parseIntegerExpression(children[i], queryText)) {
 
411
                                return false;
 
412
                        }
 
413
                }
 
414
                queryText+=")";
 
415
                return true;
 
416
        } else if (elementName == "integer-difference" ) {
 
417
                DOMElements children = element->getChilds();
 
418
                if (children.size() != 2) { // at least two integer subexpression are required
 
419
                        return false;
 
420
                }
 
421
                queryText+="(";
 
422
                if (!parseIntegerExpression(children[0], queryText)) {
 
423
                        return false;
 
424
                }
 
425
                queryText+=" - ";
 
426
                if (!parseIntegerExpression(children[1], queryText)) {
 
427
                        return false;
 
428
                }
 
429
                queryText+=")";
 
430
                return true;
 
431
        }
 
432
        return false;
 
433
}
 
434
 
 
435
string QueryXMLParser::parsePlace(XMLSP::DOMElement* element) {
 
436
        if (element->getElementName() != "place") {
 
437
                return ""; // missing place tag
 
438
        }
 
439
        string placeName = element->getCData();
 
440
        placeName.erase(std::remove_if(placeName.begin(), placeName.end(), ::isspace), placeName.end());
 
441
        return placeName;
 
442
}
 
443
 
 
444
 
 
445
void QueryXMLParser::printQueries() {
 
446
        QueryXMLParser::QueriesIterator it;
 
447
        for(it = queries.begin(); it != queries.end(); it++){
 
448
                        cout << it->id << ": " << (it->isPlaceBound ? "\tplace-bound " : "");
 
449
                        if (it->parsingResult == QueryItem::UNSUPPORTED_QUERY) {
 
450
                                cout << "\t---------- unsupported query ----------" << endl;
 
451
                        } else {
 
452
                        cout << "\t" << (it->negateResult ? "not " : "") << it->queryText << endl;
 
453
                        }
 
454
        }       
 
455
}