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

[Jiri Srba]

Added the possiblity to check for multiple place bounds.

Added possibliy to check for multiple place bounds.

[Jiri Srba (srba)]

tested and seems to work

review: Approve

=== modified file 'PetriEngine/Structures/StateSet.h'
--- PetriEngine/Structures/StateSet.h	2016-03-24 11:11:38 +0000
+++ PetriEngine/Structures/StateSet.h	2016-04-06 13:32:00 +0000
@@ -23,6 +23,9 @@
 #include <iostream>
 #include "State.h"
 
+extern unsigned int maxplacesbound;
+extern std::vector<size_t>* placelistboundindex;
+
 namespace PetriEngine { namespace Structures {
 
 // Big int used for state space statistics
@@ -70,8 +73,17 @@
 		std::pair<iter, bool> result = this->insert(state);
                 // update the max token bound for each place in the net (only for newly discovered markings)
                 if (result.second) {
-                    for(size_t i = 0; i < _places; i++) {
-                    _maxPlaceBound[i] = std::max<unsigned int>(state->marking()[i],_maxPlaceBound[i]);
+                    
+                     if (placelistboundindex == NULL) { // single places in the place bound check
+                        for (size_t i = 0; i < _places; i++) {
+                            _maxPlaceBound[i] = std::max<unsigned int>(state->marking()[i], _maxPlaceBound[i]);
+                        }
+                    } else { // multiple places in the place bound check
+                        unsigned int sum = 0;
+                        for (int i=0; i < (*placelistboundindex).size(); i++) {
+                            sum += state->marking()[(*placelistboundindex)[i]];
+                        }
+                        maxplacesbound = std::max<unsigned int>(sum, maxplacesbound);
                     }
                 }
 		return result.second;

=== modified file 'PetriParse/QueryXMLParser.cpp'
--- PetriParse/QueryXMLParser.cpp	2015-04-21 20:16:43 +0000
+++ PetriParse/QueryXMLParser.cpp	2016-04-06 13:32:00 +0000
@@ -34,12 +34,12 @@
 // QueryXMLParser::~QueryXMLParser() { };
 
 
-bool QueryXMLParser::parse(const std::string& xml){
+bool QueryXMLParser::parse(const std::string& xml, int query){
 	//Parse the xml
 	DOMElement* root = DOMElement::loadXML(xml);
 	bool parsingOK;
 	if (root) {
-		parsingOK = parsePropertySet(root);
+		parsingOK = parsePropertySet(root, query);
 	} else {
 		parsingOK=false;
 	}
@@ -50,17 +50,30 @@
 }
 
 
-bool QueryXMLParser::parsePropertySet(DOMElement* element){
+bool QueryXMLParser::parsePropertySet(DOMElement* element, int query){
 	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;
+        int count=1;
 	for(it = elements.begin(); it != elements.end(); it++){
+            if (count == query) {
 		if (!parseProperty(*it)) {
 			return false;
 		};
+            } else {
+                QueryItem queryItem;
+                queryItem.id = "";
+                queryItem.queryText = "";
+                queryItem.negateResult = false;
+                queryItem.isPlaceBound = false;
+                queryItem.placeNameForBound = "X";
+                queryItem.parsingResult = QueryItem::UNSUPPORTED_QUERY;
+                queries.push_back(queryItem);
+            }
+            count++;
 	}
 	return true;
 }
@@ -73,7 +86,7 @@
 	string id;
 	string queryText;
 	bool negateResult=false;
-    bool isPlaceBound=false;
+        bool isPlaceBound=false;
 	string placeNameForBound;
 	bool tagsOK=true;
 	
@@ -199,20 +212,42 @@
     } 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;
+        if (children.size() == 0) {
+            return false; 
+        }
+        
+        if (children.size() == 1) {
+            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;
+            placelistbound = NULL;
+            return true;
+        } else {
+            placelistbound = new std::vector<std::string>;
+            for (int i = 0; i < children.size(); i++) {
+                if (children[i]->getElementName() != "place") {
+                    return false;
+                }
+                placeNameForBound = parsePlace(children[i]);
+                if (placeNameForBound == "") {
+                    return false; // invalid place name
+                }
+                queryText += "(\"" + placeNameForBound + "\"" + " < 0)";
+                if (i<children.size()-1) queryText += " and ";
+                placelistbound->push_back(placeNameForBound);
+            }
+            placeNameForBound = "Multiple Place Bound";
+            negateResult = false;
+            isPlaceBound = true;
+            return true;
+        }
     } else {
             return false;
 	}

=== modified file 'PetriParse/QueryXMLParser.h'
--- PetriParse/QueryXMLParser.h	2014-07-06 11:12:11 +0000
+++ PetriParse/QueryXMLParser.h	2016-04-06 13:32:00 +0000
@@ -29,6 +29,8 @@
 
 using namespace std;
 
+extern std::vector<std::string>* placelistbound;
+
 class QueryXMLParser {
 public:    
 	QueryXMLParser(const PNMLParser::TransitionEnablednessMap &transitionEnabledness);
@@ -50,12 +52,12 @@
         typedef Queries::iterator QueriesIterator;
         Queries queries;
 
-	bool parse(const string& xml);
+	bool parse(const string& xml, int query);
         void printQueries();
         void printQueries(int i);
         
 private:
-        bool parsePropertySet(XMLSP::DOMElement* element);
+        bool parsePropertySet(XMLSP::DOMElement* element, int query);
         bool parseProperty(XMLSP::DOMElement* element);
         bool parseTags(XMLSP::DOMElement* element);
         bool parseFormula(XMLSP::DOMElement* element, string &queryText, bool &negateResult, bool &isPlaceBound, string &placeNameForBound);

=== modified file 'VerifyPN.cpp'
--- VerifyPN.cpp	2016-04-06 11:43:13 +0000
+++ VerifyPN.cpp	2016-04-06 13:32:00 +0000
@@ -94,6 +94,10 @@
 
 bool printstatistics;
 
+std::vector<std::string>* placelistbound = NULL; // for multiple place bounds
+std::vector<size_t>* placelistboundindex = NULL; // list of place indexes in multiple place bounds
+unsigned int maxplacesbound = 0;
+
 double diffclock(clock_t clock1, clock_t clock2){
     double diffticks = clock1 - clock2;
     double diffms = (diffticks*1000)/CLOCKS_PER_SEC;
@@ -465,7 +469,7 @@
 		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
@@ -528,7 +532,7 @@
 			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)) {
+				if (!XMLparser.parse(querystr, xmlquery)) {
 					fprintf(stderr, "Error: Failed parsing XML query file\n");
 					fprintf(stdout, "DO_NOT_COMPETE\n");
 					return ErrorCode;
@@ -666,16 +670,26 @@
 //-------------------------------------------------------------------//
 //----------------------- Reachability search -----------------------//
 //-------------------------------------------------------------------//
+        
+        const std::vector<std::string>& tnames = net->transitionNames();
+        const std::vector<std::string>& pnames = net->placeNames();
+
+        if (placelistbound != NULL) {
+            placelistboundindex = new std::vector<size_t>;
+            for (int i = 0; i < placelistbound->size(); i++) {
+                for (size_t j = 0; j < pnames.size(); j++) {
+                    if (((*placelistbound)[i]) == pnames[j]) {
+                        placelistboundindex->push_back(j);
+                    }
+                }
+            }
+        }
+        
 	ReachabilityResult result = strategy->reachable(*net, m0, v0, query);
 
 	
 	//----------------------- Output Result -----------------------//
 	
-	const std::vector<std::string>& tnames = net->transitionNames();
-	const std::vector<std::string>& pnames = net->placeNames();
-
-	
-
 	if (statespaceexploration) {
 		retval = UnknownCode;
 		unsigned int placeBound = 0;
@@ -707,15 +721,27 @@
         fprintf(stdout, "\nQuery is satisfied.\n\n");
 	} else if(retval == FailedCode) {
 		if (xmlquery>0 && XMLparser.queries[xmlquery-1].isPlaceBound) {
+                    if (placelistbound == NULL) {
 			// 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, "FORMULA %s %d TECHNIQUES SEQUENTIAL_PROCESSING EXPLICIT STRUCTURAL_REDUCTION\n", XMLparser.queries[xmlquery-1].id.c_str(), result.maxPlaceBound()[p]);
 					fprintf(stdout, "\nMaximum number of tokens in place %s: %d\n\n",XMLparser.queries[xmlquery-1].placeNameForBound.c_str(),result.maxPlaceBound()[p]);
-                    retval = UnknownCode;
+                                        retval = UnknownCode;
                     			break;
 				}
 			}
+                    } else {
+                        fprintf(stdout, "FORMULA %s %d  TECHNIQUES SEQUENTIAL_PROCESSING EXPLICIT STRUCTURAL_REDUCTION\n", XMLparser.queries[xmlquery-1].id.c_str(), maxplacesbound);
+                        fprintf(stdout, "\nMaximum number of tokens in places");
+                        for (int i = 0; i < placelistboundindex->size(); i++) {
+                            size_t index = (*placelistboundindex)[i];
+                            fprintf(stdout, " %s", pnames[index].c_str());
+                            if (i < placelistboundindex->size() - 2) fprintf(stdout, ",");
+                            if (i == placelistboundindex->size() - 2) fprintf(stdout, " and");
+                        }
+                        fprintf(stdout, ": %d\n\n", maxplacesbound);
+                    }
 		} else {
 			if (xmlquery>0) {
 				fprintf(stdout, "FORMULA %s FALSE TECHNIQUES SEQUENTIAL_PROCESSING EXPLICIT STRUCTURAL_REDUCTION\n", XMLparser.queries[xmlquery-1].id.c_str());