Merge lp:~verifypn-maintainers/verifypn/sumoXMLparsing into lp:~verifypn-maintainers/verifypn/trunk

[Jiri Srba]

Adds a new flag -x query_number for parsing XML queries (model checking contest).

Adds a new flag -x query_number for parsing XML queries (model checking contest).

[Jonas Finnemann Jensen (jopsen)]

This looks good...

Things like transitionEnabledness and InhibitorArcList makes me very sad. We should have a Petri Net structure that carries this kind of information.

Anyways, that is not the state of the current codebase, and given what we have this is good.
The overhead of encoding a condition string for each transition is negligible anyways.
It is just a source for bugs and other pains, but it'll probably work fine :)

Comments for PetriParse/QueryXMLParser.cpp:

A)
stdout is consistently used for logging errors. I would strongly advice using stderr for communicating errors.
Personally, I prefer to use fprintf(stderr, "...", ...); but cerr works too. C++ streams are not the best for
formatting output, things get so obscure and for large datasets (not the case here) performance is an issue.
Hence, I try to stay away from cout/cerr as a rule of thumb.

B)
Exceptions is a feature in C++ that is rarely used. At least I've rarely seen people use it, and many projects outright forbid it: Gecko, LLVM, Google C++ guidelines...
Compiling with exceptions causes RTTI Run-Time Type Information to be encoded and prevents certain compiler optimizations.
Unless coding some sort of big enterprise project where correctness and stability is more important than speed, I wouldn't use exceptions. Both because they are complicated and because they have overhead.

Comments for PetriParse/QueryXMLParser.(h|cpp):

Please, add license header for consistency, I believe this would be appropriate:

/* VerifyPN - TAPAAL Petri Net Engine
 * Copyright (C) 2014 Jiri Srba <email address hidden>
 *
 * This program is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program. If not, see <http://www.gnu.org/licenses/>.
 */

Assuming you're okay with licensing it under GPLv3.
It's just nice to clear up any confusion.

[lp:~verifypn-maintainers/verifypn/sumoXMLparsing]

94. By Jiri Srba on 2014-05-13

added licence headers for query XML parsing

95. By Jiri Srba on 2014-05-13

fixed printing of errors in query XML parser to stderr

96. By Jiri Srba on 2014-05-13

changed query XML parser so that it does not throw any expections

[Jiri Srba (srba)]

Regarding A) the code now prints errors to stderr using fprintf.
Regarding B) the code is now clean of exception throws
Licence headers were added.

review: Needs Resubmitting

[Jonas Finnemann Jensen (jopsen)]

This looks good to me. Getting rid of exceptions makes me quite happy :)

Test cases would have been nice, but the current test setup is too hacked to cover -x at the moment...

review: Approve

[Jiri Srba (srba)]

review: Approve

=== modified file 'PetriEngine/PQL/PQLQueryTokens.l'
--- PetriEngine/PQL/PQLQueryTokens.l	2014-03-23 05:21:56 +0000
+++ PetriEngine/PQL/PQLQueryTokens.l	2014-05-13 20:18:53 +0000
@@ -14,7 +14,6 @@
 
 digit         [0-9]
 letter        [a-zA-Z_]
-
 %%
 
 [ \t\n\r]         ;

=== modified file 'PetriParse/PNMLParser.cpp'
--- PetriParse/PNMLParser.cpp	2014-03-22 19:59:08 +0000
+++ PetriParse/PNMLParser.cpp	2014-05-13 20:18:53 +0000
@@ -21,6 +21,7 @@
 #include <string>
 #include <stdio.h>
 #include <stdlib.h>
+#include <iostream>
 
 using namespace PetriEngine;
 using namespace XMLSP;
@@ -33,6 +34,7 @@
 	arcs.clear();
 	transitions.clear();
 	inhibarcs.clear();
+	transitionEnabledness.clear();
 
 	//Set the builder
 	this->builder = builder;
@@ -41,6 +43,11 @@
 	DOMElement* root = DOMElement::loadXML(xml);
 	parseElement(root);
 
+	// initialize transitionEnabledness
+	for(TransitionIter it = transitions.begin(); it != transitions.end(); it++){
+		transitionEnabledness[it->id]="(true";
+	}
+	
 	//Create inhibitor arcs
 	for(InhibitorArcIter inhb = inhibarcs.begin(); inhb != inhibarcs.end(); inhb++){
 		//Check that source id exists
@@ -68,6 +75,10 @@
 				char weight[sizeof(int) * 8 + 1];
 				sprintf(weight, "%i", inhb->weight);
 				
+				//cout << "INHIB ARC: " << source.id << " to " << target.id << " weight " << weight << endl;
+				string cond = " and \"" + source.id + "\" < " + weight;
+				transitionEnabledness[it->id]+=cond;
+				
 				if(it->cond.empty()){
 					it->cond = source.id + " < " + string(weight);
 				}else{
@@ -103,6 +114,14 @@
 
 		if(source.isPlace && !target.isPlace){
 			builder->addInputArc(source.id, target.id, it->weight);
+			
+			// cout << "ARC: " << source.id << " to " << target.id << " weight " << it->weight << endl;
+			char weight[sizeof(int) * 8 + 1];
+			sprintf(weight, "%i", it->weight);
+			
+			string cond = " and \"" + source.id + "\" >= " + weight;
+			transitionEnabledness[target.id]+=cond;
+		
 		}else if(!source.isPlace && target.isPlace){
 			builder->addOutputArc(source.id, target.id, it->weight);
 		}else{
@@ -113,6 +132,11 @@
 		}
 	}
 
+	// finalize transitionEnabledness
+	for(TransitionIter it = transitions.begin(); it != transitions.end(); it++){
+		transitionEnabledness[it->id]+=")";
+	}
+	
 	//Release DOM tree
 	delete root;
 
@@ -257,7 +281,6 @@
 			weight = atoi(text.c_str());
 		}
 	}
-
 	Arc arc;
 	arc.source = source;
 	arc.target = target;
@@ -300,14 +323,13 @@
 	builder->addVariable(name, initialValue, range);
 }
 
-
-void PNMLParser::parseValue(DOMElement* element, string& text){
+void PNMLParser::parseValue(DOMElement* element, string& text) {
 	DOMElements elements = element->getChilds();
 	DOMElements::iterator it;
-	for(it = elements.begin(); it != elements.end(); it++){
-		if((*it)->getElementName() == "value" || (*it)->getElementName() == "text")
+	for (it = elements.begin(); it != elements.end(); it++) {
+		if ((*it)->getElementName() == "value" || (*it)->getElementName() == "text") {
 			text = (*it)->getCData();
-		else
+		} else
 			parseValue(*it, text);
 	}
 }

=== modified file 'PetriParse/PNMLParser.h'
--- PetriParse/PNMLParser.h	2014-03-22 19:59:08 +0000
+++ PetriParse/PNMLParser.h	2014-05-13 20:18:53 +0000
@@ -48,6 +48,7 @@
 		bool isPlace;
 	};
 	typedef std::map<std::string, NodeName> NodeNameMap;
+        
 public:
 
 	struct Query{
@@ -61,6 +62,7 @@
 	};
 	typedef std::vector<InhibitorArc> InhibitorArcList;
         typedef InhibitorArcList::iterator InhibitorArcIter;
+        typedef std::map<std::string, std::string> TransitionEnablednessMap;
 
 	PNMLParser(){
 		builder = NULL;
@@ -75,6 +77,10 @@
         InhibitorArcList getInhibitorArcs(){
                 return inhibarcs;
         }
+        
+        TransitionEnablednessMap getTransitionEnabledness() {
+            return transitionEnabledness;
+        }
 
 private:
 	void parseElement(XMLSP::DOMElement* element);
@@ -93,6 +99,7 @@
 	TransitionList transitions;
 	InhibitorArcList inhibarcs;
 	std::vector<Query> queries;
+        TransitionEnablednessMap transitionEnabledness; // encodes the enabledness condition for each transition
 };
 
 #endif // PNMLPARSER_H

=== added file 'PetriParse/QueryXMLParser.cpp'
--- PetriParse/QueryXMLParser.cpp	1970-01-01 00:00:00 +0000
+++ PetriParse/QueryXMLParser.cpp	2014-05-13 20:18:53 +0000
@@ -0,0 +1,455 @@
+/* VerifyPN - TAPAAL Petri Net Engine
+ * Copyright (C) 2014 Jiri Srba <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#include "QueryXMLParser.h"
+
+#include <string>
+#include <stdio.h>
+#include <stdlib.h>
+#include <iostream>
+#include <sstream> 
+#include <algorithm> 
+
+using namespace XMLSP;
+using namespace std;
+
+QueryXMLParser::QueryXMLParser(const PNMLParser::TransitionEnablednessMap &transitionEnabledness) {
+	_transitionEnabledness = transitionEnabledness;
+};
+
+// QueryXMLParser::~QueryXMLParser() { };
+
+
+bool QueryXMLParser::parse(const std::string& xml){
+	//Parse the xml
+	DOMElement* root = DOMElement::loadXML(xml);
+	bool parsingOK;
+	if (root) {
+		parsingOK = parsePropertySet(root);
+	} else {
+		parsingOK=false;
+	}
+		
+	//Release DOM tree
+	delete root;
+	return parsingOK;
+}
+
+
+bool QueryXMLParser::parsePropertySet(DOMElement* element){
+	if (element->getElementName()!="property-set") {
+		fprintf(stderr,"ERROR missing property-set\n");
+		return false; // missing property-set element
+	}
+	DOMElements elements = element->getChilds();
+	DOMElements::iterator it;
+	for(it = elements.begin(); it != elements.end(); it++){
+		if (!parseProperty(*it)) {
+			return false;
+		};
+	}
+	return true;
+}
+
+bool QueryXMLParser::parseProperty(DOMElement* element){
+	if (element->getElementName()!="property") {
+		fprintf(stderr,"ERROR missing property\n");
+		return false; // unexpected element (only property is allowed)
+	}
+	string id;
+	string queryText;
+	bool negateResult=false;
+    bool isPlaceBound=false;
+	string placeNameForBound;
+	bool tagsOK=true;
+	
+	DOMElements elements = element->getChilds();
+	DOMElements::iterator it;
+	DOMElements::iterator formulaPtr;
+	for(it = elements.begin(); it != elements.end(); it++){
+		if ((*it)->getElementName()=="id") {
+			id = (*it)->getCData();
+		} else if ((*it)->getElementName()=="formula") {
+			formulaPtr=it;
+		} else if ((*it)->getElementName()=="tags") {
+			tagsOK=parseTags(*it);
+		}
+	}
+	
+	if (id=="") {
+		fprintf(stderr,"ERROR a query with empty id\n");
+		return false;
+	}
+	
+	QueryItem queryItem;
+	queryItem.id=id;
+	if (tagsOK && parseFormula(*formulaPtr, queryText, negateResult, isPlaceBound, placeNameForBound)) {
+		queryItem.queryText=queryText;
+		queryItem.negateResult=negateResult;
+        queryItem.isPlaceBound=isPlaceBound;
+		queryItem.placeNameForBound=placeNameForBound;
+		queryItem.parsingResult=QueryItem::PARSING_OK;
+	} else {
+		queryItem.queryText="";
+		queryItem.negateResult=false;
+        queryItem.isPlaceBound=false;
+		queryItem.placeNameForBound="";
+		queryItem.parsingResult=QueryItem::UNSUPPORTED_QUERY;
+	}	
+	queries.push_back(queryItem);
+	return true;
+}
+
+bool QueryXMLParser::parseTags(DOMElement* element){
+	// we can accept only reachability query
+	DOMElements elements = element->getChilds();
+	DOMElements::iterator it;
+	for(it = elements.begin(); it != elements.end(); it++){
+		if ((*it)->getElementName()=="is-reachability" && (*it)->getCData()!="true") {
+			return false;
+		}
+	}
+	return true;
+}
+
+bool QueryXMLParser::parseFormula(DOMElement* element, string &queryText, bool &negateResult, bool &isPlaceBound, string &placeNameForBound){
+	/*
+	 Describe here how to parse
+	 * INV phi =  AG phi =  not EF not phi
+	 * IMPOS phi = AG not phi = not EF phi
+	 * POS phi = EF phi
+	 * NEG INV phi = not AG phi = EF not phi
+	 * NEG IMPOS phi = not AG not phi = EF phi
+	 * NEG POS phi = not EF phi
+	 */
+	DOMElements elements = element->getChilds();
+	if (elements.size() != 1) {
+		return false;
+	}
+	DOMElements::iterator booleanFormula = elements.begin();
+	string elementName = (*booleanFormula)->getElementName(); 
+	if (elementName=="invariant") {
+		queryText="EF not(";
+		negateResult=true;
+	} else if (elementName=="impossibility") {
+		queryText="EF ( ";
+		negateResult=true;
+	} else if (elementName=="possibility") {
+		queryText="EF ( ";
+		negateResult=false;
+	} else if (elementName=="negation") {
+		DOMElements children = (*elements.begin())->getChilds();
+		if (children.size() !=1) {
+			return false;
+		}
+		booleanFormula = children.begin(); 
+		string negElementName = (*booleanFormula)->getElementName();
+		if (negElementName=="invariant") {
+			queryText="EF not( ";
+			negateResult=false;
+		} else if (negElementName=="impossibility") {
+			queryText="EF ( ";
+			negateResult=false;
+		} else if (negElementName=="possibility") {
+			queryText="EF ( ";
+			negateResult=true;
+		} else {
+			return false;
+		}
+    } else if (elementName == "place-bound") {
+        queryText = "EF ";
+        DOMElements children = (*booleanFormula)->getChilds();
+        if (children.size() != 1) {
+            return false; // we support only place-bound for one place
+        }
+        if (children[0]->getElementName() != "place") {
+            return false;
+        }
+        placeNameForBound = parsePlace(children[0]);
+		if (placeNameForBound=="") {
+			return false; // invalid place name
+		}
+        queryText += "\""+placeNameForBound+"\""+" < 0";
+        negateResult = false;
+        isPlaceBound = true;
+        return true;
+    } else {
+            return false;
+	}
+	DOMElements nextElements = (*booleanFormula)->getChilds();
+	if (nextElements.size() !=1 || !parseBooleanFormula(nextElements[0] , queryText)) {
+		return false;
+	}
+	queryText+=" )";
+    isPlaceBound=false;
+	placeNameForBound = "";
+	return true;
+}
+
+bool QueryXMLParser::parseBooleanFormula(DOMElement* element, string &queryText){
+		string elementName = element->getElementName();
+		if (elementName == "deadlock") {
+			queryText+="deadlock";
+			return true;
+		} else if (elementName == "true") {
+			queryText+="true";
+			return true;
+		} else if (elementName == "false") {
+			queryText+="false";
+			return true;
+		} else if (elementName == "negation") {
+			DOMElements children = element->getChilds();
+			queryText+="not(";
+			if (children.size()==1 && parseBooleanFormula(children[0], queryText)) {
+				queryText+=")";
+			} else {
+				return false;
+			}
+			return true;
+		} else if (elementName == "conjunction") {
+			DOMElements children = element->getChilds();
+			if (children.size()<2) {
+				return false;
+			}
+			if (!(parseBooleanFormula((children[0]), queryText))) {
+				return false;
+			}
+			DOMElements::iterator it;
+			for(it = (children.begin())+1; it != children.end(); it++) {
+				queryText+=" and ";
+				if (!(parseBooleanFormula(*it, queryText))) {
+					return false;
+				}
+			}
+			return true;
+		} else if (elementName == "disjunction") {
+			DOMElements children = element->getChilds();
+			if (children.size()<2) {
+				return false;
+			}
+			if (!(parseBooleanFormula(*children.begin(), queryText))) {
+				return false;
+			}
+			DOMElements::iterator it;
+			for(it = children.begin()+1; it != children.end(); it++) {
+				queryText+=" or ";
+				if (!(parseBooleanFormula(*it, queryText))) {
+					return false;	
+				}
+			}
+			return true;
+		} else if (elementName == "exclusive-disjunction") {
+			DOMElements children = element->getChilds();
+			if (children.size()!=2) { // we support only two subformulae here
+				return false;
+			}
+			string subformula1;
+			string subformula2;
+			if (!(parseBooleanFormula(*(children.begin()), subformula1))) {
+				return false;
+			}
+			if (!(parseBooleanFormula(*(children.begin()+1), subformula2))) {
+				return false;
+			}
+			queryText+= "(("+subformula1+" and not("+subformula2+")) or (not("+subformula1+") and "+subformula2+"))";
+			return true;
+		} else if (elementName == "implication") {
+			DOMElements children = element->getChilds();
+			if (children.size()!=2) { // implication has only two subformulae
+				return false;
+			}
+			string subformula1;
+			string subformula2;
+			if (!(parseBooleanFormula(*(children.begin()), subformula1))) {
+				return false;
+			}
+			if (!(parseBooleanFormula(*(children.begin()+1), subformula2))) {
+				return false;
+			}
+			queryText+= "not("+subformula1+") or ( "+subformula2+" )";
+			return true;
+		} else if (elementName == "equivalence") {
+			DOMElements children = element->getChilds();
+			if (children.size()!=2) { // we support only two subformulae here
+				return false;
+			}
+			string subformula1;
+			string subformula2;
+			if (!(parseBooleanFormula(*(children.begin()), subformula1))) {
+				return false;
+			}
+			if (!(parseBooleanFormula(*(children.begin()+1), subformula2))) {
+				return false;
+			}
+			queryText+= "(("+subformula1+" and "+subformula2+") or (not("+subformula1+") and not("+subformula2+")))";
+			return true;
+		} else if (	elementName == "integer-eq" || 
+					elementName == "integer-ne" || 
+					elementName == "integer-lt" || 
+					elementName == "integer-le" || 
+					elementName == "integer-gt" || 
+					elementName == "integer-ge") {
+			DOMElements children = element->getChilds();
+			if (children.size()!=2) { // exactly two integer subformulae are required
+				return false;
+			}
+			string subformula1;
+			string subformula2;
+			if (!(parseIntegerExpression(children[0], subformula1))) {
+				return false;
+			}
+			if (!(parseIntegerExpression(children[1], subformula2))) {
+				return false;
+			}
+			string mathoperator;
+			if		( elementName == "integer-eq") mathoperator=" == ";
+			else if ( elementName == "integer-ne") mathoperator=" != ";
+			else if ( elementName == "integer-lt") mathoperator=" < ";
+			else if ( elementName == "integer-le") mathoperator=" <= ";
+			else if ( elementName == "integer-gt") mathoperator=" > ";
+			else if ( elementName == "integer-ge") mathoperator=" >= ";
+			
+			queryText+="("+subformula1+mathoperator+subformula2+")";
+			return true;
+		} else if (elementName == "is-fireable") {
+			DOMElements children = element->getChilds();
+			if (children.size() == 0) {
+				return false;
+			}
+			if (children.size() > 1) {
+				queryText += "(";
+			}
+			for (int i = 0; i < children.size(); i++) {
+				if (children[i]->getElementName() != "transition") {
+					return false;
+				}
+				if (i > 0) {
+					queryText += " or ";
+				}
+				string transitionName = children[i]->getCData();
+				if(_transitionEnabledness.find(transitionName) == _transitionEnabledness.end()){
+					fprintf(stderr,
+						"XML Query Parsing error: Transition id=\"%s\" was not found!\n",
+					    transitionName.c_str());
+					return false;
+			    }
+				queryText += _transitionEnabledness[transitionName]; 
+			}
+			if (children.size() > 1) {
+				queryText += ")";
+			}
+			return true;
+		}
+	return false;
+}
+
+bool QueryXMLParser::parseIntegerExpression(DOMElement* element, string &queryText){
+	string elementName = element->getElementName();
+	if (elementName == "integer-constant") {
+		int i;
+		if(sscanf((element->getCData()).c_str(), "%d", &i)  == EOF ) { 
+			return false; // expected integer at this place
+		}
+		 stringstream ss;//create a stringstream
+         ss << i;//add number to the stream
+         queryText+=ss.str();
+		return true;
+	} else if (elementName == "tokens-count") {
+		DOMElements children = element->getChilds();
+		if (children.size()==0) {
+			return false;
+		}
+		if (children.size()>1) {
+			queryText+="(";
+		}
+		for (int i = 0; i < children.size(); i++) {
+			if (children[i]->getElementName() != "place") {
+				return false;
+			}
+			if (i > 0) {
+				queryText += " + ";
+			}
+			string placeName = parsePlace(children[i]);
+			if (placeName == "") {
+				return false; // invalid place name
+			}
+			queryText+="\""+placeName+"\"";
+		}
+		if (children.size()>1) {
+			queryText+=")";
+		}
+		return true;
+	} else if (	elementName == "integer-sum" ||
+				elementName == "integer-product" ) {
+		DOMElements children = element->getChilds();
+		if (children.size() < 2) { // at least two integer subexpression are required
+			return false;
+		}
+		string mathoperator;
+		if (	 elementName == "integer-sum") mathoperator = " + ";
+		else if (elementName == "integer-product") mathoperator = " * ";
+		queryText+="(";
+		for (int i = 0; i < children.size(); i++) {
+			if (i > 0) {
+				queryText+= mathoperator;
+			}
+			if (!parseIntegerExpression(children[i], queryText)) {
+				return false;
+			}
+		}
+		queryText+=")";
+		return true;
+	} else if (elementName == "integer-difference" ) {
+		DOMElements children = element->getChilds();
+		if (children.size() != 2) { // at least two integer subexpression are required
+			return false;
+		}
+		queryText+="(";
+		if (!parseIntegerExpression(children[0], queryText)) {
+			return false;
+		}
+		queryText+=" - ";
+		if (!parseIntegerExpression(children[1], queryText)) {
+			return false;
+		}
+		queryText+=")";
+		return true;
+	}
+	return false;
+}
+
+string QueryXMLParser::parsePlace(XMLSP::DOMElement* element) {
+	if (element->getElementName() != "place") {
+		return ""; // missing place tag
+	}
+	string placeName = element->getCData();
+	placeName.erase(std::remove_if(placeName.begin(), placeName.end(), ::isspace), placeName.end());
+	return placeName;
+}
+ 
+
+void QueryXMLParser::printQueries() {
+	QueryXMLParser::QueriesIterator it;
+	for(it = queries.begin(); it != queries.end(); it++){
+			cout << it->id << ": " << (it->isPlaceBound ? "\tplace-bound " : "");
+			if (it->parsingResult == QueryItem::UNSUPPORTED_QUERY) {
+				cout << "\t---------- unsupported query ----------" << endl;
+			} else {
+			cout << "\t" << (it->negateResult ? "not " : "") << it->queryText << endl;
+			}
+	}	
+}

=== added file 'PetriParse/QueryXMLParser.h'
--- PetriParse/QueryXMLParser.h	1970-01-01 00:00:00 +0000
+++ PetriParse/QueryXMLParser.h	2014-05-13 20:18:53 +0000
@@ -0,0 +1,68 @@
+/* VerifyPN - TAPAAL Petri Net Engine
+ * Copyright (C) 2014 Jiri Srba <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef QUERYXMLPARSER_H
+#define	QUERYXMLPARSER_H
+
+#include "xmlsp/xmlsp_dom.h"
+#include "PNMLParser.h"
+
+#include <map>
+#include <string>
+#include <string.h>
+#include <vector>
+#include <sstream> 
+
+using namespace std;
+
+class QueryXMLParser {
+public:    
+	QueryXMLParser(const PNMLParser::TransitionEnablednessMap &transitionEnabledness);
+ //      ~QueryXMLParser();
+    
+        struct QueryItem {
+            string id; // query name
+            string queryText; // only EF queries will be here
+            bool negateResult; // true if the final result should be negated
+            bool isPlaceBound; // true if the query is a place-bound one (returns integer)
+            string placeNameForBound;
+            enum { 
+                PARSING_OK,
+                UNSUPPORTED_QUERY,
+            } parsingResult;
+        };
+
+        typedef vector<QueryItem> Queries;
+        typedef Queries::iterator QueriesIterator;
+        Queries queries;
+
+	bool parse(const string& xml);
+        void printQueries();
+        
+private:
+        bool parsePropertySet(XMLSP::DOMElement* element);
+        bool parseProperty(XMLSP::DOMElement* element);
+        bool parseTags(XMLSP::DOMElement* element);
+        bool parseFormula(XMLSP::DOMElement* element, string &queryText, bool &negateResult, bool &isPlaceBound, string &placeNameForBound);
+        bool parseBooleanFormula(XMLSP::DOMElement* element, string &queryText);
+        bool parseIntegerExpression(XMLSP::DOMElement* element, string &queryText);
+        string parsePlace(XMLSP::DOMElement* element);
+        PNMLParser::TransitionEnablednessMap _transitionEnabledness;
+};
+
+#endif	/* QUERYXMLPARSER_H */
+

=== modified file 'README.mkd'
--- README.mkd	2013-10-21 09:24:49 +0000
+++ README.mkd	2014-05-13 20:18:53 +0000
@@ -55,3 +55,4 @@
   * Jonas Finnemann Jensen
   * Thomas Søndersø Nielsen
   * Lars Kærlund Østergaard
+  * Jiri Srba

=== added directory 'Scripts'
=== added file 'Scripts/BenchKit_head.sh'
--- Scripts/BenchKit_head.sh	1970-01-01 00:00:00 +0000
+++ Scripts/BenchKit_head.sh	2014-05-13 20:18:53 +0000
@@ -0,0 +1,106 @@
+#!/bin/bash
+
+# This is the initialization script for the participation of TAPAAL
+# untimed engine verifypn in the Petri net competition 2014.
+
+# BK_EXAMINATION: it is a string that identifies your "examination"
+
+export PATH="$PATH:/home/mcc/BenchKit/bin/"
+VERIFYPN=$HOME/BenchKit/bin/verifypn
+#VERIFYPN=/Users/srba/dev/sumoXMLparsing/verifypn-osx64
+TIMEOUT=10
+
+if [ ! -f iscolored ]; then
+    	echo "File 'iscolored' not found!"
+else
+	if [ "TRUE" = `cat iscolored` ]; then
+		echo "TAPAAL does not support colored nets."
+		echo "DO_NOT_COMPETE" 
+		exit 0
+	fi
+fi
+
+if [ ! -f model.pnml ]; then
+    	echo "File 'model.pnml' not found!"
+	exit 1
+fi
+
+function verify {
+	if [ ! -f $2 ]; then
+    		echo "File '$2' not found!" 
+		exit 1 
+	fi
+	local NUMBER=`cat $2 | grep "<property>" | wc -l`
+        for (( QUERY=1; QUERY<=$NUMBER; QUERY++ ))
+	do
+		echo
+		echo "verifypn" $1 "-x" $QUERY "model.pnml" $2
+		if [ $TIMEOUT = 0 ]; then
+			$VERIFYPN $1 "-x" $QUERY "model.pnml" $2
+		else
+			timeout $TIMEOUT $VERIFYPN $1 "-x" $QUERY "model.pnml" $2
+			RETVAL=$?
+			if [ $RETVAL = 124 ] || [ $RETVAL =  125 ] || [ $RETVAL =  126 ] || [ $RETVAL =  127 ] || [ $RETVAL =  137 ] ; then
+				echo -ne "CANNOT_COMPUTE\n"
+			fi
+		fi
+	done
+} 
+
+
+case "$BK_EXAMINATION" in
+
+	StateSpace)
+		echo		
+		echo "*****************************************"
+		echo "*  TAPAAL performing StateSpace search  *"
+		echo "*****************************************"
+		$VERIFYPN -n -d -e model.pnml 
+		;;
+
+	ReachabilityComputeBounds)	
+		echo		
+		echo "***********************************************"
+		echo "*  TAPAAL verifying ReachabilityComputeBounds *"
+		echo "***********************************************"
+		verify "-n -r 1" "ReachabilityComputeBounds.xml"
+		;;
+
+	ReachabilityDeadlock)
+		echo		
+		echo "**********************************************"
+		echo "*  TAPAAL checking for ReachabilityDeadlock  *"
+		echo "**********************************************"
+		TIMEOUT=0
+		verify "-n -r 1" "ReachabilityDeadlock.xml"
+		;;
+
+	ReachabilityCardinality)
+		echo		
+		echo "**********************************************"
+		echo "*  TAPAAL verifying ReachabilityCardinality  *"
+		echo "**********************************************"
+		verify "-n -r 1" "ReachabilityCardinality.xml"
+		;;
+
+	ReachabilityFireability)
+		echo		
+		echo "**********************************************"
+		echo "*  TAPAAL verifying ReachabilityFireability  *"
+		echo "**********************************************"
+		verify "-n -r 1" "ReachabilityFireability.xml"
+		;;
+
+	ReachabilityFireabilitySimple)
+                echo
+                echo "****************************************************"
+                echo "*  TAPAAL verifying ReachabilityFireabilitySimple  *"
+                echo "****************************************************"
+                verify "-n -r 1" "ReachabilityFireabilitySimple.xml"
+                ;;
+
+	*)
+		echo "DO_NOT_COMPETE"	
+		exit 0
+		;;
+esac

=== added file 'Scripts/run.sh'
--- Scripts/run.sh	1970-01-01 00:00:00 +0000
+++ Scripts/run.sh	2014-05-13 20:18:53 +0000
@@ -0,0 +1,20 @@
+for D in $(find INPUTS -mindepth 1 -maxdepth 1 -type d) ; do
+    echo;
+    echo "####################################################################";
+    echo $D ;
+    cp BenchKit_head.sh $D ;
+    cd $D ;
+    export BK_EXAMINATION=StateSpace ;
+    ./BenchKit_head.sh 
+    export BK_EXAMINATION=ReachabilityComputeBounds ;
+    ./BenchKit_head.sh 
+    export BK_EXAMINATION=ReachabilityDeadlock ;
+    ./BenchKit_head.sh 
+    export BK_EXAMINATION=ReachabilityCardinality ;
+    ./BenchKit_head.sh 
+    export BK_EXAMINATION=ReachabilityFireability ;
+    ./BenchKit_head.sh 
+    export BK_EXAMINATION=ReachabilityFireabilitySimple ;
+    ./BenchKit_head.sh 
+    cd ../..
+done

=== modified file 'VerifyPN.cpp'
--- VerifyPN.cpp	2014-03-18 07:13:31 +0000
+++ VerifyPN.cpp	2014-05-13 20:18:53 +0000
@@ -1,8 +1,8 @@
 /* PeTe - Petri Engine exTremE
- * Copyright (C) 2011  Jonas Finnemann Jensen <[e-mail]>,
- *                     Thomas Søndersø Nielsen <[e-mail]>,
- *                     Lars Kærlund Østergaard <[e-mail]>,
- *					   Jiri Srba <[e-mail]>
+ * Copyright (C) 2011-2014  Jonas Finnemann Jensen <[e-mail]>,
+ *                          Thomas Søndersø Nielsen <[e-mail]>,
+ *                          Lars Kærlund Østergaard <[e-mail]>,
+ *					        Jiri Srba <[e-mail]>
  * 
  * This program is free software: you can redistribute it and/or modify
  * it under the terms of the GNU General Public License as published by
@@ -39,6 +39,7 @@
 #include <PetriEngine/Reachability/BreadthFirstReachabilitySearch.h>
 
 #include "PetriEngine/Reducer.h"
+#include "PetriParse/QueryXMLParser.h"
 
 
 using namespace std;
@@ -74,8 +75,13 @@
 	char* modelfile = NULL;
 	char* queryfile = NULL;
 	bool disableoverapprox = false;
-        int enablereduction = 0; // 0 ... disabled (default),  1 ... aggresive, 2 ... k-boundedness preserving
+  	int enablereduction = 0; // 0 ... disabled (default),  1 ... aggresive, 2 ... k-boundedness preserving
+	int xmlquery = -1; // if value is nonnegative then input query file is in xml format and we verify query 
+						 // number xmlquery
+	bool statespaceexploration = false;
+	bool printstatistics = true;
 
+        
 	//----------------------- Parse Arguments -----------------------//
 
 	// Parse command line arguments
@@ -111,27 +117,40 @@
 				fprintf(stderr, "Argument Error: Unrecognized search strategy \"%s\"\n", s);
 				return ErrorCode;
 			}
-		}else if(strcmp(argv[i], "-m") == 0 || strcmp(argv[i], "--memory-limit") == 0){
-                        if (i==argc-1) {
-                                fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
-				return ErrorCode;                           
-                        }
-			if(sscanf(argv[++i], "%d", &memorylimit) != 1 || memorylimit < 0){
+		} else if (strcmp(argv[i], "-m") == 0 || strcmp(argv[i], "--memory-limit") == 0) {
+			if (i == argc - 1) {
+				fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
+				return ErrorCode;
+			}
+			if (sscanf(argv[++i], "%d", &memorylimit) != 1 || memorylimit < 0) {
 				fprintf(stderr, "Argument Error: Invalid memory limit \"%s\"\n", argv[i]);
 				return ErrorCode;
 			}
-		}else if(strcmp(argv[i], "-d") == 0 || strcmp(argv[i], "--disable-overapprox") == 0){
+		} else if (strcmp(argv[i], "-d") == 0 || strcmp(argv[i], "--disable-overapprox") == 0) {
 			disableoverapprox = true;
-                }else if(strcmp(argv[i], "-r") == 0 || strcmp(argv[i], "--reduction") == 0){
-                        if (i==argc-1) {
-                                fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
-				return ErrorCode;                           
-                        }
-                        if(sscanf(argv[++i], "%d", &enablereduction) != 1 || enablereduction < 0 || enablereduction > 2){
-				fprintf(stderr, "Argument Error: Invalid reduction argument \"%s\"\n", argv[i]);
+		} else if (strcmp(argv[i], "-e") == 0 || strcmp(argv[i], "--state-space-exploration") == 0) {
+			statespaceexploration = true;
+		} else if (strcmp(argv[i], "-n") == 0 || strcmp(argv[i], "--no-statistics") == 0) {
+			printstatistics = false;
+		} else if (strcmp(argv[i], "-x") == 0 || strcmp(argv[i], "--xml-queries") == 0) {
+			if (i == argc - 1) {
+				fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
 				return ErrorCode;
 			}
-		}else if(strcmp(argv[i], "-h") == 0 || strcmp(argv[i], "--help") == 0){
+			if (sscanf(argv[++i], "%d", &xmlquery) != 1 || xmlquery <= 0) {
+				fprintf(stderr, "Argument Error: Query index to verify \"%s\"\n", argv[i]);
+				return ErrorCode;
+			} 
+		}else if (strcmp(argv[i], "-r") == 0 || strcmp(argv[i], "--reduction") == 0) {
+				if (i == argc - 1) {
+					fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
+					return ErrorCode;
+				}
+				if (sscanf(argv[++i], "%d", &enablereduction) != 1 || enablereduction < 0 || enablereduction > 2) {
+					fprintf(stderr, "Argument Error: Invalid reduction argument \"%s\"\n", argv[i]);
+					return ErrorCode;
+				}
+		} else if (strcmp(argv[i], "-h") == 0 || strcmp(argv[i], "--help") == 0){
 			printf(	"Usage: verifypn [options] model-file query-file\n"
 					"A tool for answering reachability of place cardinality queries (including deadlock)\n" 
                                         "for weighted P/T Petri nets extended with inhibitor arcs.\n"
@@ -144,14 +163,17 @@
 					"                                     - BFS          Breadth first search\n"
 					"                                     - DFS          Depth first search\n"
 					"                                     - RDFS         Random depth first search\n"
-					"                                     - OverApprox   Linear Over Approx.\n"
+					"                                     - OverApprox   Linear Over Approx\n"
 					"  -m, --memory-limit <megabyte>      Memory limit for the state space search in MB,\n"
 					"                                     0 for unlimited (default)\n"
+					"  -e, --state-space-exploration      State-space exploration only (query-file is irrelevant)\n"
+					"  -x, --xml-query <query index>      Parse XML query file and verify query of a given index\n"
 					"  -d, --disable-over-approximation   Disable linear over approximation\n"
-                                        "  -r, --reduction                    Enable structural net reduction:\n"
-                                        "                                     - 0  disabled (default)\n"
-                                        "                                     - 1  aggressive reduction\n"
-                                        "                                     - 2  reduction preserving k-boundedness\n"
+                    "  -r, --reduction                    Enable structural net reduction:\n"
+                    "                                     - 0  disabled (default)\n"
+                    "                                     - 1  aggressive reduction\n"
+                    "                                     - 2  reduction preserving k-boundedness\n"
+					"  -n, --no-statistics                Do not display any statistics (default is to display it)\n"
 					"  -h, --help                         Display this help message\n"
 					"  -v, --version                      Display version information\n"
 					"\n"
@@ -169,7 +191,7 @@
 			printf("VerifyPN (untimed verification engine for TAPAAL) %s\n", VERSION);
 			printf("Copyright (C) 2011-2014 Jonas Finnemann Jensen <[e-mail]>,\n");
 			printf("                        Thomas Søndersø Nielsen <[e-mail]>,\n");
-			printf("                        Lars Kærlund Østergaard <[e-mail]>\n");
+			printf("                        Lars Kærlund Østergaard <[e-mail]>,\n");
 			printf("                        Jiri Srba <[e-mail]>\n");
                         printf("GNU GPLv3 or later <http://gnu.org/licenses/gpl.html>\n");
 			return 0;
@@ -182,6 +204,15 @@
 			return ErrorCode;
 		}
 	}
+	if (statespaceexploration) { 
+		// for state-space exploration some options are mandatory
+		disableoverapprox = true; 
+		enablereduction = 0;
+		kbound = 0;
+		outputtrace = false;
+		searchstrategy = BFS;
+	}
+	
 
 	//----------------------- Validate Arguments -----------------------//
 
@@ -192,7 +223,7 @@
 	}
 
 	//Check for query file
-	if(!modelfile){
+	if(!modelfile && !statespaceexploration){
 		fprintf(stderr, "Argument Error: No query-file provided\n");
 		return ErrorCode;
 	}
@@ -204,14 +235,15 @@
 	MarkVal* m0 = NULL;
 	VarVal* v0 = NULL;
                   
-        // List of inhibitor arcs
-        PNMLParser::InhibitorArcList inhibarcs;
-        
+    // List of inhibitor arcs and transition enabledness
+    PNMLParser::InhibitorArcList inhibarcs;
+    PNMLParser::TransitionEnablednessMap transitionEnabledness;
 	{
 		//Load the model
 		ifstream mfile(modelfile, ifstream::in);
 		if(!mfile){
 			fprintf(stderr, "Error: Model file \"%s\" couldn't be opened\n", modelfile);
+			fprintf(stdout, "CANNOT_COMPUTE\n");
 			return ErrorCode;
 		}
 
@@ -225,8 +257,9 @@
 		parser.parse(buffer.str(), &builder);
 		parser.makePetriNet();
                 
-                inhibarcs = parser.getInhibitorArcs(); // Remember inhibitor arcs
-
+        inhibarcs = parser.getInhibitorArcs(); // Remember inhibitor arcs
+		transitionEnabledness = parser.getTransitionEnabledness(); // Remember conditions for transitions
+				
 		//Build the petri net
 		net = builder.makePetriNet();
 		m0 = builder.makeInitialMarking();
@@ -235,50 +268,84 @@
 		// Close the file
 		mfile.close();
 	}
-
+	
 	//----------------------- Parse Query -----------------------//
 
 	//Condition to check
 	Condition* query = NULL;
 	bool isInvariant = false;
-
+	QueryXMLParser XMLparser(transitionEnabledness); // parser for XML queries
 	//Read query file, begin scope to release memory
 	{
-		//Open query file
-		ifstream qfile(queryfile, ifstream::in);
-		if(!qfile){
-			fprintf(stderr, "Error: Query file \"%s\" couldn't be opened\n", queryfile);
-			return ErrorCode;
-		}
-
-		//Read everything
-		stringstream buffer;
-		buffer << qfile.rdbuf();
-		string querystr = buffer.str();
-
-		//Validate query type
-		if(querystr.substr(0, 2) != "EF" && querystr.substr(0, 2) != "AG"){
-			fprintf(stderr, "Error: Query type \"%s\" not supported, only (EF and AG is supported)\n", querystr.substr(0, 2).c_str());
-			return ErrorCode;
-		}
-
-		//Check if is invariant
-		isInvariant = querystr.substr(0, 2) == "AG";
-
-		//Warp in not if isInvariant
-		string querystring = querystr.substr(2);
-		if(isInvariant)
-			querystring = "not ( " + querystring + " )";
-
+		string querystring; // excluding EF and AG
+		if (!statespaceexploration) {
+			//Open query file
+			ifstream qfile(queryfile, ifstream::in);
+			if (!qfile) {
+				fprintf(stderr, "Error: Query file \"%s\" couldn't be opened\n", queryfile);
+				fprintf(stdout, "CANNOT_COMPUTE\n");
+				return ErrorCode;
+			}
+
+			//Read everything
+			stringstream buffer;
+			buffer << qfile.rdbuf();
+			string querystr = buffer.str(); // including EF and AG
+			//Parse XML the queries and querystr let be the index of xmlquery 		
+			if (xmlquery > 0) {
+				if (!XMLparser.parse(querystr)) {
+					fprintf(stderr, "Error: Failed parsing XML query file\n");
+					fprintf(stdout, "DO_NOT_COMPETE\n");
+					return ErrorCode;
+				}
+				// XMLparser.printQueries();
+				if (XMLparser.queries.size() < xmlquery) {
+					fprintf(stderr, "Error: Wrong index of query in the XML query file\n");
+					fprintf(stdout, "CANNOT_COMPUTE\n");
+					return ErrorCode;
+				}
+				if (XMLparser.queries[xmlquery - 1].parsingResult == QueryXMLParser::QueryItem::UNSUPPORTED_QUERY) {
+					fprintf(stdout, "The selected query in the XML query file is not supported\n");
+					fprintf(stdout, "FORMULA %s CANNOT_COMPUTE\n", XMLparser.queries[xmlquery-1].id.c_str());
+					return ErrorCode;
+				}
+				// fprintf(stdout, "Index of the selected query: %d\n\n", xmlquery);
+				querystr = XMLparser.queries[xmlquery - 1].queryText;
+				querystring = querystr.substr(2);
+				isInvariant = XMLparser.queries[xmlquery - 1].negateResult;
+                
+                if (xmlquery>0) {
+                    fprintf(stdout, "FORMULA %s ", XMLparser.queries[xmlquery-1].id.c_str());
+                    fflush(stdout);
+                }
+
+			} else { // standard textual query
+				//Validate query type
+				if (querystr.substr(0, 2) != "EF" && querystr.substr(0, 2) != "AG") {
+					fprintf(stderr, "Error: Query type \"%s\" not supported, only (EF and AG is supported)\n", querystr.substr(0, 2).c_str());
+					return ErrorCode;
+				}
+				//Check if is invariant
+				isInvariant = querystr.substr(0, 2) == "AG";
+
+				//Warp in not if isInvariant
+				querystring = querystr.substr(2);
+				if (isInvariant)
+					querystring = "not ( " + querystring + " )";
+			}
+			//Close query file
+			qfile.close();
+		} else { // state-space exploration
+			querystring = "false";
+			isInvariant = false;
+		}
+	
 		//Parse query
 		query = ParseQuery(querystring);
 		if(!query){
-			fprintf(stderr, "Error: Failed to parse query \"%s\"\n", querystr.substr(2).c_str());
+			fprintf(stderr, "Error: Failed to parse query \"%s\"\n", querystring.c_str()); //querystr.substr(2).c_str());
 			return ErrorCode;
 		}
-
-		//Close query file
-		qfile.close();
 	}
 
 	//----------------------- Context Analysis -----------------------//
@@ -298,8 +365,9 @@
 		}
 	}
 
-        //--------------------- Apply Net Reduction ---------------//
-        
+	
+    //--------------------- Apply Net Reduction ---------------//
+
     Reducer reducer = Reducer(net); // reduced is needed also in trace generation (hence the extended scope)
 	if (enablereduction == 1 or enablereduction == 2) {
 		// Compute how many times each place appears in the query
@@ -355,12 +423,12 @@
 	ReachabilityResult result = strategy->reachable(*net, m0, v0, query);
 
 	//----------------------- Output Trace -----------------------//
-        const std::vector<unsigned int>& trace = (enablereduction==0 ? result.trace() : reducer.NonreducedTrace(net,result.trace()));
-	const std::vector<std::string>& tnames = net->transitionNames();
+    const std::vector<std::string>& tnames = net->transitionNames();
 	const std::vector<std::string>& pnames = net->placeNames();
-
+	
 	//Print result to stderr
 	if(outputtrace && result.result() == ReachabilityResult::Satisfied){
+		const std::vector<unsigned int>& trace = (enablereduction==0 ? result.trace() : reducer.NonreducedTrace(net,result.trace()));
 		fprintf(stderr, "Trace:\n<trace>\n");
 		for(size_t i = 0; i < trace.size(); i++){
 			fprintf(stderr, "\t<transition id=\"%s\">\n", tnames[trace[i]].c_str());
@@ -378,6 +446,7 @@
 
 	//----------------------- Output Statistics -----------------------//
 
+	if (printstatistics) {
 	//Print statistics
 	fprintf(stdout, "STATS:\n");
 	fprintf(stdout, "\tdiscovered states: %lli\n", result.discoveredStates());
@@ -412,11 +481,22 @@
 		}
 	}
 	fprintf(stdout,"\n\n");
+	}
 	
 	//----------------------- Output Result -----------------------//
 
 	ReturnValues retval = ErrorCode;
 
+	if (statespaceexploration) {
+		retval = UnknownCode;
+		unsigned int placeBound = 0;
+		for(size_t p = 0; p < result.maxPlaceBound().size(); p++) { 
+			placeBound = std::max<unsigned int>(placeBound,result.maxPlaceBound()[p]);
+		}
+		fprintf(stdout,"STATE_SPACE %lli -1 %d %d TECHNIQUES EXPLICIT\n", result.exploredStates(), result.maxTokens(), placeBound);
+		return retval;
+	}
+	
 	//Find result code
 	if(result.result() == ReachabilityResult::Unknown)
 		retval = UnknownCode;
@@ -428,10 +508,29 @@
 	//Print result
 	if(retval == UnknownCode)
 		fprintf(stdout, "Unable to decide if query is satisfied.\n");
-	else if(retval == SuccessCode)
-		fprintf(stdout, "Query is satisfied.\n");
-	else if(retval == FailedCode)
-		fprintf(stdout, "Query is NOT satisfied.\n");
+	else if(retval == SuccessCode) {
+		if (xmlquery>0) {
+			fprintf(stdout, "TRUE TECHNIQUES EXPLICIT STRUCTURAL_REDUCTION\n");
+		}
+        fprintf(stdout, "Query is satisfied.\n");
+	} else if(retval == FailedCode) {
+		if (xmlquery>0 && XMLparser.queries[xmlquery-1].isPlaceBound) {
+			// find index of the place for reporting place bound
+			for(size_t p = 0; p < result.maxPlaceBound().size(); p++) { 
+				if (pnames[p]==XMLparser.queries[xmlquery-1].placeNameForBound) {
+					fprintf(stdout, "%d TECHNIQUES EXPLICIT STRUCTURAL_REDUCTION\n", result.maxPlaceBound()[p]);
+					fprintf(stdout, "Maximum number of tokens in place %s: %d\n",XMLparser.queries[xmlquery-1].placeNameForBound.c_str(),result.maxPlaceBound()[p]);
+                    retval = UnknownCode;
+                    			break;
+				}
+			}
+		} else {
+			if (xmlquery>0) {
+				fprintf(stdout, "FALSE TECHNIQUES EXPLICIT STRUCTURAL_REDUCTION\n");
+			}
+            fprintf(stdout, "Query is NOT satisfied.\n");
+		}
+	}
 
 	return retval;
 }