~verifypn-cpn/verifypn/unfoldTACPN : contents of PetriParse/QueryXMLParser.cpp at revision 225

~verifypn-cpn/verifypn/unfoldTACPN : (revision 225)

/* VerifyPN - TAPAAL Petri Net Engine
 * Copyright (C) 2014 Jiri Srba <srba.jiri@gmail.com>,
 *                    Peter Gjøl Jensen <root@petergjoel.dk>
 *
 * 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 "PetriEngine/PQL/Expressions.h"

#include <string>
#include <stdio.h>
#include <stdlib.h>
#include <iostream>
#include <sstream> 
#include <algorithm> 

using namespace std;

int getChildCount(rapidxml::xml_node<> *n)
{
  int c = 0;
  for (rapidxml::xml_node<> *child = n->first_node(); child != NULL; child = child->next_sibling())
  {
    c++;
  } 
  return c;
} 

QueryXMLParser::QueryXMLParser() {
}

QueryXMLParser::~QueryXMLParser() { }

bool QueryXMLParser::parse(std::ifstream& xml, const std::set<size_t>& parse_only) {
    //Parse the xml
    rapidxml::xml_document<> doc;
    vector<char> buffer((istreambuf_iterator<char>(xml)), istreambuf_iterator<char>());
    buffer.push_back('\0');
    doc.parse<0>(&buffer[0]);
    rapidxml::xml_node<>*  root = doc.first_node();
    bool parsingOK;
    if (root) {
        parsingOK = parsePropertySet(root, parse_only);
    } else {
        parsingOK = false;
    }

    //Release DOM tree
    return parsingOK;
}

bool QueryXMLParser::parsePropertySet(rapidxml::xml_node<>*  element, const std::set<size_t>& parse_only) {
    if (strcmp(element->name(), "property-set") != 0) {
        fprintf(stderr, "ERROR missing property-set\n");
        return false; // missing property-set element
    }
    
    size_t i = 0;
    for (auto it = element->first_node(); it; it = it->next_sibling()) {
        if(parse_only.size() == 0 || parse_only.count(i) > 0)
        {
            if (!parseProperty(it)) {
                return false;
            }
        }
        else
        {
            QueryItem queryItem;
            queryItem.query = nullptr;
            queryItem.parsingResult = QueryItem::PARSING_OK;
            queries.push_back(queryItem);
        }
        ++i;
    }
    return true;
}

bool QueryXMLParser::parseProperty(rapidxml::xml_node<>*  element) {
    if (strcmp(element->name(), "property") != 0) {
        fprintf(stderr, "ERROR missing property\n");
        return false; // unexpected element (only property is allowed)
    }
    string id;
    bool tagsOK = true;
    rapidxml::xml_node<>* formulaPtr = NULL;
    for (auto it = element->first_node(); it; it = it->next_sibling()) {
        if (strcmp(it->name(), "id") == 0) {
            id = it->value();
        } else if (strcmp(it->name(), "formula") == 0) {
            formulaPtr = it;
        } else if (strcmp(it->name(), "tags") == 0) {
            tagsOK = parseTags(it);
        }
    }

    if (id == "") {
        fprintf(stderr, "ERROR a query with empty id\n");
        return false;
    }

    QueryItem queryItem;
    queryItem.id = id;
    if(tagsOK)
    {
        queryItem.query = parseFormula(formulaPtr);
        assert(queryItem.query);
        queryItem.parsingResult = QueryItem::PARSING_OK;
    } else {
        queryItem.query = nullptr;
        queryItem.parsingResult = QueryItem::UNSUPPORTED_QUERY;
    }
    queries.push_back(queryItem);
    return true;
}

bool QueryXMLParser::parseTags(rapidxml::xml_node<>*  element) {
    // we can accept only reachability query
    for (auto it = element->first_node(); it; it = it->next_sibling()) {
        if (strcmp(it->name(), "is-reachability") == 0 && strcmp(it->value(), "true") == 0) {
            return false;
        }
    }
    return true;
}

Condition_ptr QueryXMLParser::parseFormula(rapidxml::xml_node<>*  element) {
    if (getChildCount(element) != 1) 
    {
        assert(false);
        return nullptr;    
    }
    auto child = element->first_node();
    string childName = child->name();
    Condition_ptr cond = nullptr;
    
    // Formula is either a place-bound or CTL/reachability formula
    if (childName == "place-bound") {
        std::vector<std::string> places;
        for (auto it = child->first_node(); it ; it = it->next_sibling()) {
            if (strcmp(it->name(), "place") != 0) 
            {
                assert(false);
                return nullptr;
            }
            auto place = parsePlace(it);
            if (place == "") 
            {             
                assert(false);
                return nullptr; // invalid place name
            }
            places.push_back(place);
        }
        auto bnds = std::make_shared<UpperBoundsCondition>(places);
        return std::make_shared<EFCondition>(bnds);
    } else if ((cond = parseBooleanFormula(child)) != nullptr) {
        return cond;
    } else {
        assert(false);
        return nullptr;
    }
}


Condition_ptr QueryXMLParser::parseBooleanFormula(rapidxml::xml_node<>*  element) {
    /*
     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
     */
    
    string elementName = element->name();
    Condition_ptr cond = nullptr, cond2 = nullptr;
    
    if (elementName == "invariant") {
        if ((cond = parseBooleanFormula(element->first_node())) != nullptr)
            return std::make_shared<NotCondition>(std::make_shared<EFCondition>(std::make_shared<NotCondition>(cond)));
    } else if (elementName == "impossibility") {
        if ((cond = parseBooleanFormula(element->first_node())) != nullptr)
            return std::make_shared<NotCondition>(std::make_shared<EFCondition>(cond));
    } else if (elementName == "possibility") {
        if ((cond = parseBooleanFormula(element->first_node())) != nullptr)
            return std::make_shared<EFCondition>(cond);
    } else if (elementName == "exists-path") {
        if (getChildCount(element) != 1) 
        {
            assert(false);
            return nullptr;
        }
        auto child = element->first_node();
        if (strcmp(child->name(), "next") == 0) {
            if (getChildCount(child) != 1) 
            {
                assert(false);
                return nullptr;
            }
            if ((cond = parseBooleanFormula(child->first_node())) != nullptr)
                return std::make_shared<EXCondition>(cond);
        } else if (strcmp(child->name(), "globally") == 0) {
            if (getChildCount(child) != 1) 
            {
                assert(false);
                return nullptr;
            }
            if ((cond = parseBooleanFormula(child->first_node())) != nullptr)
                return std::make_shared<EGCondition>(cond);
        } else if (strcmp(child->name(), "finally") == 0) {
            if (getChildCount(child) != 1) 
            {
                assert(false);
                return nullptr;
            }
            if ((cond = parseBooleanFormula(child->first_node())) != nullptr)
                return std::make_shared<EFCondition>(cond);
        } else if (strcmp(child->name(), "until") == 0) {
            if (getChildCount(child) != 2) 
            {
                assert(false);
                return nullptr;
            }
            auto before = child->first_node();
            auto reach = before->next_sibling();
            if (getChildCount(before) != 1 || getChildCount(reach) != 1 ||
                    strcmp(before->name(), "before") != 0 || strcmp(reach->name(), "reach") != 0) 
                {
                    assert(false);
                    return nullptr;
                }
            if ((cond = parseBooleanFormula(before->first_node())) != nullptr) {
                if ((cond2 = parseBooleanFormula(reach->first_node())) != nullptr) {
                    return std::make_shared<EUCondition>(cond, cond2);
                }
            }
        }
    } else if (elementName == "all-paths") {
        if (getChildCount(element) != 1) 
        {
            assert(false);
            return nullptr;
        }
        auto child = element->first_node();
        if (strcmp(child->name(), "next") == 0) {
            if (getChildCount(child) != 1) 
            {
                assert(false);
                return nullptr;
            }
            if ((cond = parseBooleanFormula(child->first_node())) != nullptr)
                return std::make_shared<AXCondition>(cond);
        } else if (strcmp(child->name(), "globally") == 0) {
            if (getChildCount(child) != 1) 
            {
                assert(false);
                return nullptr;
            }
            if ((cond = parseBooleanFormula(child->first_node())) != nullptr)
                return std::make_shared<AGCondition>(cond);
        } else if (strcmp(child->name(), "finally") == 0) {
            if (getChildCount(child) != 1) 
            {
                assert(false);
                return nullptr;
            }
            if ((cond = parseBooleanFormula(child->first_node())) != nullptr)
                return std::make_shared<AFCondition>(cond);
        } else if (strcmp(child->name(), "until") == 0) {
            if (getChildCount(child) != 2) 
            {
                assert(false);
                return nullptr;
            }
            auto before = child->first_node();
            auto reach = before->next_sibling();
            if (getChildCount(before) != 1 || getChildCount(reach) != 1 ||
                    strcmp(before->name(), "before") != 0 || strcmp(reach->name(), "reach") != 0)
            {
                assert(false);
                return nullptr;
            }
            if ((cond = parseBooleanFormula(before->first_node())) != nullptr){
                if ((cond2 = parseBooleanFormula(reach->first_node())) != nullptr) {
                    return std::make_shared<AUCondition>(cond, cond2);
                }
            }
        }
    } else if (elementName == "deadlock") {
        return std::make_shared<DeadlockCondition>();
    } else if (elementName == "true") {
        return BooleanCondition::TRUE_CONSTANT;
    } else if (elementName == "false") {
        return BooleanCondition::FALSE_CONSTANT;
    } else if (elementName == "negation") {
        if (getChildCount(element) != 1) 
        {
            assert(false);
            return nullptr;
        }
        auto child = element->first_node();
        if (strcmp(child->name(), "invariant") == 0) {
            if ((cond = parseBooleanFormula(child->first_node())) != nullptr) {
                return std::make_shared<EFCondition>(std::make_shared<NotCondition>(cond));
            }
        } else if (strcmp(child->name(), "impossibility") == 0) {
            if ((cond = parseBooleanFormula(child->first_node())) != nullptr) {
                return std::make_shared<EFCondition>(cond);
            }
        } else if (strcmp(child->name(), "possibility") == 0) {
            if ((cond = parseBooleanFormula(child->first_node())) != nullptr) {
                return std::make_shared<NotCondition>(std::make_shared<EFCondition>(cond));
            }
        } else {
            if ((cond = parseBooleanFormula(child)) != nullptr) {
                return std::make_shared<NotCondition>(cond);
            }
        }
    } else if (elementName == "conjunction") {
        auto children = element->first_node();
        if (getChildCount(element) < 2) 
        {
            assert(false);
            return nullptr;
        }
        auto it = children;
        cond = parseBooleanFormula(it);
        // skip a sibling
        for (it = it->next_sibling(); it; it = it->next_sibling()) {
            Condition_ptr child = parseBooleanFormula(it);
            if(child == nullptr || cond == nullptr) 
            {
                assert(false);
                return nullptr;
            }
            cond = std::make_shared<AndCondition>(cond, child);
        }
        return cond;
    } else if (elementName == "disjunction") {
        auto children = element->first_node();
        if (getChildCount(element) < 2) 
        {
            assert(false);
            return nullptr;
        }
        auto it = children;
        cond = parseBooleanFormula(it);
        // skip a sibling
        for (it = it->next_sibling(); it; it = it->next_sibling()) {
            Condition_ptr child = parseBooleanFormula(it);
            if(child == nullptr || cond == nullptr) 
            {
                assert(false);
                return nullptr;
            }
            cond = std::make_shared<OrCondition>(cond, child);
        }
        return cond;
    } else if (elementName == "exclusive-disjunction") {
        auto children = element->first_node();
        if (getChildCount(element) != 2) 
        {
            assert(false);
            return nullptr;
        }
        cond = parseBooleanFormula(children);
        cond2 = parseBooleanFormula(children->next_sibling());
        if (cond == nullptr || cond2 == nullptr)    
        {
            assert(false);
            return nullptr;
        }
        return std::make_shared<OrCondition>(
                std::make_shared<AndCondition>(cond, std::make_shared<NotCondition>(cond2)),
                std::make_shared<AndCondition>(std::make_shared<NotCondition>(cond), cond2));
    } else if (elementName == "implication") {
        auto children = element->first_node();
        if (getChildCount(element) != 2)             
        {
            assert(false);
            return nullptr;
        }
        cond = parseBooleanFormula(children);
        cond2 = parseBooleanFormula(children->next_sibling());
        if (cond == nullptr || cond2 == nullptr)
        {
            assert(false);
            return nullptr;       
        }
        return std::make_shared<OrCondition>(std::make_shared<NotCondition>(cond), cond2);
    } else if (elementName == "equivalence") {
        auto children = element->first_node();
        if (getChildCount(element) != 2) 
        {
            assert(false);
            return nullptr;       
        }
        cond = parseBooleanFormula(children);
        cond2 = parseBooleanFormula(children->next_sibling());
        if (cond == nullptr || cond2 == nullptr) return nullptr;
        return std::make_shared<OrCondition>(std::make_shared<AndCondition>(cond, cond2),
                std::make_shared<AndCondition>(std::make_shared<NotCondition>(cond), 
                std::make_shared<NotCondition>(cond2)));
    } else if (elementName == "integer-eq" || elementName == "integer-ne" ||
            elementName == "integer-lt" || elementName == "integer-le" ||
            elementName == "integer-gt" || elementName == "integer-ge") {
        auto children = element->first_node();
        if (getChildCount(element) != 2) 
        {
            assert(false);
            return nullptr;       
        }
        Expr_ptr expr1 = parseIntegerExpression(children);
        Expr_ptr expr2 = parseIntegerExpression(children->next_sibling());
        if(expr1 == nullptr || expr2 == nullptr) 
        {
            assert(false);
            return nullptr;       
        }
        if (elementName == "integer-eq") return std::make_shared<EqualCondition>(expr1, expr2);
        else if (elementName == "integer-ne") return std::make_shared<NotEqualCondition>(expr1, expr2);
        else if (elementName == "integer-lt") return std::make_shared<LessThanCondition>(expr1, expr2);
        else if (elementName == "integer-le") return std::make_shared<LessThanOrEqualCondition>(expr1, expr2);
        else if (elementName == "integer-gt") return std::make_shared<GreaterThanCondition>(expr1, expr2);
        else if (elementName == "integer-ge") return std::make_shared<GreaterThanOrEqualCondition>(expr1, expr2);        
    } else if (elementName == "is-fireable") {
        size_t nrOfChildren = getChildCount(element);
        if (nrOfChildren == 0) 
        {
            assert(false);
            return nullptr;       
        }
        std::vector<Condition_ptr> conds;
        for (auto it = element->first_node(); it; it = it->next_sibling()) {
            if (strcmp(it->name(), "transition") != 0) 
            {
                assert(false);
                return nullptr;       
            }
            conds.emplace_back(std::make_shared<FireableCondition>(it->value()));
        }
        return std::make_shared<OrCondition>(conds);
    }
    std::cerr << "An error occurred while parsing the query." << std::endl;
    std::cerr << elementName << std::endl;
    assert(false);
    exit(ErrorCode);
    return nullptr;
}

Expr_ptr QueryXMLParser::parseIntegerExpression(rapidxml::xml_node<>*  element) {
    string elementName = element->name();
    if (elementName == "integer-constant") {
        int i;
        if (sscanf(element->value(), "%d", &i) == EOF) 
        {
            assert(false);
            return nullptr;       
        }
        return std::make_shared<LiteralExpr>(i);
    } else if (elementName == "tokens-count") {
        auto children = element->first_node();
        std::vector<Expr_ptr> ids;        
        for (auto it = children; it; it = it->next_sibling()) {
            if (strcmp(it->name(), "place") != 0)
            {
                assert(false);
                return nullptr;
            }
            string placeName = parsePlace(it);
            if (placeName == "")
            {
                assert(false);
                return nullptr; // invalid place name
            }
            auto id = std::make_shared<IdentifierExpr>(placeName);
            ids.emplace_back(id);
        }
        
        if (ids.size() == 0) 
        {
            assert(false);
            return nullptr;       
        }
        if (ids.size() == 1) return ids[0];
        
        return std::make_shared<PlusExpr>(std::move(ids), true);
    } else if (elementName == "integer-sum" || elementName == "integer-product") {
        auto children = element->first_node();
        bool isMult = false;
        if (elementName == "integer-sum") isMult = false;
        else if (elementName == "integer-product") isMult = true;

        std::vector<Expr_ptr> els;
        auto it = children;
       
        for (; it; it = it->next_sibling()) {
            els.emplace_back(parseIntegerExpression(it));
            if(!els.back())  
        {
            assert(false);
            return nullptr;       
        }
        }

        if (els.size() < 2) 
        {
            assert(false);
            return nullptr;       
        }

        return  isMult ? 
                std::dynamic_pointer_cast<Expr>(std::make_shared<MultiplyExpr>(std::move(els))) :
                std::dynamic_pointer_cast<Expr>(std::make_shared<PlusExpr>(std::move(els)));
;
    } else if (elementName == "integer-difference") {
        auto children = element->first_node();
        std::vector<Expr_ptr> els;
        for (auto it = children; it; it = it->next_sibling()) {
            els.emplace_back(parseIntegerExpression(it));
        }
        if(els.size() == 1) 
            els.emplace(els.begin(), std::make_shared<LiteralExpr>(0));
        return std::make_shared<SubtractExpr>(std::move(els));
    }
    assert(false);
    return nullptr;
}

string QueryXMLParser::parsePlace(rapidxml::xml_node<>*  element) {
    if (strcmp(element->name(), "place"))  return ""; // missing place tag
    string placeName = element->value();
    placeName.erase(std::remove_if(placeName.begin(), placeName.end(), ::isspace), placeName.end());
    return placeName;
}

void QueryXMLParser::printQueries(size_t i) {
    //	QueryXMLParser::QueriesIterator it;
    if (i <= 0 || i > queries.size()) {
        cout << "In printQueries the query index is out of scope\n\n";
        return;
    }
    QueryItem it = queries[i - 1];
    cout << it.id << ": " ;
    if (it.parsingResult == QueryItem::UNSUPPORTED_QUERY) {
        cout << "\t---------- unsupported query ----------" << endl;
    } else {
        cout << "\t";
        it.query->toString(cout);
        cout << std::endl;
    }
}

void QueryXMLParser::printQueries() {
    for (size_t i = 1; i <= queries.size(); i++) {
        printQueries(i);
    }
}

218.1.13 by Mark Glavind WIP on unfolding queries	1	/* VerifyPN - TAPAAL Petri Net Engine
	2	* Copyright (C) 2014 Jiri Srba <srba.jiri@gmail.com>,
	3	* Peter Gjøl Jensen <root@petergjoel.dk>
	4	*
	5	* This program is free software: you can redistribute it and/or modify
	6	* it under the terms of the GNU General Public License as published by
	7	* the Free Software Foundation, either version 3 of the License, or
	8	* (at your option) any later version.
	9	*
	10	* This program is distributed in the hope that it will be useful,
	11	* but WITHOUT ANY WARRANTY; without even the implied warranty of
	12	* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
	13	* GNU General Public License for more details.
	14	*
	15	* You should have received a copy of the GNU General Public License
	16	* along with this program. If not, see <http://www.gnu.org/licenses/>.
	17	*/
	18
	19	#include "QueryXMLParser.h"
225 by Mark Glavind made include path changes and added lpsolve in order to crosscompile to windows	20	#include "PetriEngine/PQL/Expressions.h"
218.1.13 by Mark Glavind WIP on unfolding queries	21
	22	#include <string>
	23	#include <stdio.h>
	24	#include <stdlib.h>
	25	#include <iostream>
	26	#include <sstream>
	27	#include <algorithm>
	28
	29	using namespace std;
	30
	31	int getChildCount(rapidxml::xml_node<> *n)
	32	{
	33	int c = 0;
	34	for (rapidxml::xml_node<> *child = n->first_node(); child != NULL; child = child->next_sibling())
	35	{
	36	c++;
	37	}
	38	return c;
	39	}
	40
	41	QueryXMLParser::QueryXMLParser() {
	42	}
	43
	44	QueryXMLParser::~QueryXMLParser() { }
	45
	46	bool QueryXMLParser::parse(std::ifstream& xml, const std::set<size_t>& parse_only) {
	47	//Parse the xml
	48	rapidxml::xml_document<> doc;
	49	vector<char> buffer((istreambuf_iterator<char>(xml)), istreambuf_iterator<char>());
	50	buffer.push_back('\0');
	51	doc.parse<0>(&buffer[0]);
	52	rapidxml::xml_node<>* root = doc.first_node();
	53	bool parsingOK;
	54	if (root) {
	55	parsingOK = parsePropertySet(root, parse_only);
	56	} else {
	57	parsingOK = false;
	58	}
	59
	60	//Release DOM tree
	61	return parsingOK;
	62	}
	63
	64	bool QueryXMLParser::parsePropertySet(rapidxml::xml_node<>* element, const std::set<size_t>& parse_only) {
	65	if (strcmp(element->name(), "property-set") != 0) {
	66	fprintf(stderr, "ERROR missing property-set\n");
	67	return false; // missing property-set element
	68	}
	69
	70	size_t i = 0;
	71	for (auto it = element->first_node(); it; it = it->next_sibling()) {
	72	if(parse_only.size() == 0 \|\| parse_only.count(i) > 0)
	73	{
	74	if (!parseProperty(it)) {
	75	return false;
218.1.21 by Mark Glavind Missing evaluate for PlusExpr and MultiplyExpr constructors	76	}
218.1.13 by Mark Glavind WIP on unfolding queries	77	}
	78	else
	79	{
	80	QueryItem queryItem;
	81	queryItem.query = nullptr;
	82	queryItem.parsingResult = QueryItem::PARSING_OK;
	83	queries.push_back(queryItem);
	84	}
	85	++i;
	86	}
	87	return true;
	88	}
	89
	90	bool QueryXMLParser::parseProperty(rapidxml::xml_node<>* element) {
	91	if (strcmp(element->name(), "property") != 0) {
	92	fprintf(stderr, "ERROR missing property\n");
	93	return false; // unexpected element (only property is allowed)
	94	}
	95	string id;
	96	bool tagsOK = true;
	97	rapidxml::xml_node<>* formulaPtr = NULL;
	98	for (auto it = element->first_node(); it; it = it->next_sibling()) {
	99	if (strcmp(it->name(), "id") == 0) {
	100	id = it->value();
	101	} else if (strcmp(it->name(), "formula") == 0) {
	102	formulaPtr = it;
	103	} else if (strcmp(it->name(), "tags") == 0) {
	104	tagsOK = parseTags(it);
	105	}
	106	}
	107
	108	if (id == "") {
	109	fprintf(stderr, "ERROR a query with empty id\n");
	110	return false;
	111	}
	112
	113	QueryItem queryItem;
	114	queryItem.id = id;
	115	if(tagsOK)
	116	{
	117	queryItem.query = parseFormula(formulaPtr);
	118	assert(queryItem.query);
	119	queryItem.parsingResult = QueryItem::PARSING_OK;
	120	} else {
	121	queryItem.query = nullptr;
	122	queryItem.parsingResult = QueryItem::UNSUPPORTED_QUERY;
	123	}
	124	queries.push_back(queryItem);
	125	return true;
	126	}
	127
	128	bool QueryXMLParser::parseTags(rapidxml::xml_node<>* element) {
	129	// we can accept only reachability query
	130	for (auto it = element->first_node(); it; it = it->next_sibling()) {
	131	if (strcmp(it->name(), "is-reachability") == 0 && strcmp(it->value(), "true") == 0) {
	132	return false;
	133	}
	134	}
	135	return true;
	136	}
	137
	138	Condition_ptr QueryXMLParser::parseFormula(rapidxml::xml_node<>* element) {
	139	if (getChildCount(element) != 1)
	140	{
141	assert(false);
142	return nullptr;
143	}
144	auto child = element->first_node();
145	string childName = child->name();
146	Condition_ptr cond = nullptr;
147
148	// Formula is either a place-bound or CTL/reachability formula
149	if (childName == "place-bound") {
150	std::vector<std::string> places;
151	for (auto it = child->first_node(); it ; it = it->next_sibling()) {
152	if (strcmp(it->name(), "place") != 0)
153	{
154	assert(false);
155	return nullptr;
156	}
157	auto place = parsePlace(it);
158	if (place == "")
159	{
160	assert(false);
161	return nullptr; // invalid place name
162	}
163	places.push_back(place);
164	}
165	auto bnds = std::make_shared<UpperBoundsCondition>(places);
166	return std::make_shared<EFCondition>(bnds);
167	} else if ((cond = parseBooleanFormula(child)) != nullptr) {
168	return cond;
169	} else {
170	assert(false);
171	return nullptr;
172	}
173	}
174
175
176	Condition_ptr QueryXMLParser::parseBooleanFormula(rapidxml::xml_node<>* element) {
177	/*
178	Describe here how to parse
179	* INV phi = AG phi = not EF not phi
180	* IMPOS phi = AG not phi = not EF phi
181	* POS phi = EF phi
182	* NEG INV phi = not AG phi = EF not phi
183	* NEG IMPOS phi = not AG not phi = EF phi
184	* NEG POS phi = not EF phi
185	*/
186
187	string elementName = element->name();
188	Condition_ptr cond = nullptr, cond2 = nullptr;
189
190	if (elementName == "invariant") {
191	if ((cond = parseBooleanFormula(element->first_node())) != nullptr)
192	return std::make_shared<NotCondition>(std::make_shared<EFCondition>(std::make_shared<NotCondition>(cond)));
193	} else if (elementName == "impossibility") {
194	if ((cond = parseBooleanFormula(element->first_node())) != nullptr)
195	return std::make_shared<NotCondition>(std::make_shared<EFCondition>(cond));
196	} else if (elementName == "possibility") {
197	if ((cond = parseBooleanFormula(element->first_node())) != nullptr)
198	return std::make_shared<EFCondition>(cond);
199	} else if (elementName == "exists-path") {
200	if (getChildCount(element) != 1)
201	{
202	assert(false);
203	return nullptr;
204	}
205	auto child = element->first_node();
206	if (strcmp(child->name(), "next") == 0) {
207	if (getChildCount(child) != 1)
208	{
209	assert(false);
210	return nullptr;
211	}
212	if ((cond = parseBooleanFormula(child->first_node())) != nullptr)
213	return std::make_shared<EXCondition>(cond);
214	} else if (strcmp(child->name(), "globally") == 0) {
215	if (getChildCount(child) != 1)
216	{
217	assert(false);
218	return nullptr;
219	}
220	if ((cond = parseBooleanFormula(child->first_node())) != nullptr)
221	return std::make_shared<EGCondition>(cond);
222	} else if (strcmp(child->name(), "finally") == 0) {
223	if (getChildCount(child) != 1)
224	{
225	assert(false);
226	return nullptr;
227	}
228	if ((cond = parseBooleanFormula(child->first_node())) != nullptr)
229	return std::make_shared<EFCondition>(cond);
230	} else if (strcmp(child->name(), "until") == 0) {
231	if (getChildCount(child) != 2)
232	{
233	assert(false);
234	return nullptr;
235	}
236	auto before = child->first_node();
237	auto reach = before->next_sibling();
238	if (getChildCount(before) != 1 \|\| getChildCount(reach) != 1 \|\|
239	strcmp(before->name(), "before") != 0 \|\| strcmp(reach->name(), "reach") != 0)
240	{
241	assert(false);
242	return nullptr;
243	}
244	if ((cond = parseBooleanFormula(before->first_node())) != nullptr) {
245	if ((cond2 = parseBooleanFormula(reach->first_node())) != nullptr) {
246	return std::make_shared<EUCondition>(cond, cond2);
247	}
248	}
249	}
250	} else if (elementName == "all-paths") {
251	if (getChildCount(element) != 1)
252	{
253	assert(false);
254	return nullptr;
255	}
256	auto child = element->first_node();
257	if (strcmp(child->name(), "next") == 0) {
258	if (getChildCount(child) != 1)
259	{
260	assert(false);
261	return nullptr;
262	}
263	if ((cond = parseBooleanFormula(child->first_node())) != nullptr)
264	return std::make_shared<AXCondition>(cond);
265	} else if (strcmp(child->name(), "globally") == 0) {
266	if (getChildCount(child) != 1)
267	{
268	assert(false);
269	return nullptr;
270	}
271	if ((cond = parseBooleanFormula(child->first_node())) != nullptr)
272	return std::make_shared<AGCondition>(cond);
273	} else if (strcmp(child->name(), "finally") == 0) {
274	if (getChildCount(child) != 1)
275	{
276	assert(false);
277	return nullptr;
278	}
279	if ((cond = parseBooleanFormula(child->first_node())) != nullptr)
280	return std::make_shared<AFCondition>(cond);
281	} else if (strcmp(child->name(), "until") == 0) {
282	if (getChildCount(child) != 2)
283	{
284	assert(false);
285	return nullptr;
286	}
287	auto before = child->first_node();
288	auto reach = before->next_sibling();
289	if (getChildCount(before) != 1 \|\| getChildCount(reach) != 1 \|\|
290	strcmp(before->name(), "before") != 0 \|\| strcmp(reach->name(), "reach") != 0)
291	{
292	assert(false);
293	return nullptr;
294	}
295	if ((cond = parseBooleanFormula(before->first_node())) != nullptr){
296	if ((cond2 = parseBooleanFormula(reach->first_node())) != nullptr) {
297	return std::make_shared<AUCondition>(cond, cond2);
298	}
299	}
300	}
301	} else if (elementName == "deadlock") {
302	return std::make_shared<DeadlockCondition>();
303	} else if (elementName == "true") {
304	return BooleanCondition::TRUE_CONSTANT;
305	} else if (elementName == "false") {
306	return BooleanCondition::FALSE_CONSTANT;
307	} else if (elementName == "negation") {
308	if (getChildCount(element) != 1)
309	{
310	assert(false);
311	return nullptr;
312	}
313	auto child = element->first_node();
314	if (strcmp(child->name(), "invariant") == 0) {
315	if ((cond = parseBooleanFormula(child->first_node())) != nullptr) {
316	return std::make_shared<EFCondition>(std::make_shared<NotCondition>(cond));
317	}
318	} else if (strcmp(child->name(), "impossibility") == 0) {
319	if ((cond = parseBooleanFormula(child->first_node())) != nullptr) {
320	return std::make_shared<EFCondition>(cond);
321	}
322	} else if (strcmp(child->name(), "possibility") == 0) {
323	if ((cond = parseBooleanFormula(child->first_node())) != nullptr) {
324	return std::make_shared<NotCondition>(std::make_shared<EFCondition>(cond));
325	}
326	} else {
327	if ((cond = parseBooleanFormula(child)) != nullptr) {
328	return std::make_shared<NotCondition>(cond);
329	}
330	}
331	} else if (elementName == "conjunction") {
332	auto children = element->first_node();
333	if (getChildCount(element) < 2)
334	{
335	assert(false);
336	return nullptr;
337	}
338	auto it = children;
339	cond = parseBooleanFormula(it);
340	// skip a sibling
341	for (it = it->next_sibling(); it; it = it->next_sibling()) {
342	Condition_ptr child = parseBooleanFormula(it);
343	if(child == nullptr \|\| cond == nullptr)
344	{
345	assert(false);
346	return nullptr;
347	}
348	cond = std::make_shared<AndCondition>(cond, child);
349	}
350	return cond;
351	} else if (elementName == "disjunction") {
352	auto children = element->first_node();
353	if (getChildCount(element) < 2)
354	{
355	assert(false);
356	return nullptr;
357	}
358	auto it = children;
359	cond = parseBooleanFormula(it);
360	// skip a sibling
361	for (it = it->next_sibling(); it; it = it->next_sibling()) {
362	Condition_ptr child = parseBooleanFormula(it);
363	if(child == nullptr \|\| cond == nullptr)
364	{
365	assert(false);
366	return nullptr;
367	}
368	cond = std::make_shared<OrCondition>(cond, child);
369	}
370	return cond;
371	} else if (elementName == "exclusive-disjunction") {
372	auto children = element->first_node();
373	if (getChildCount(element) != 2)
374	{
375	assert(false);
376	return nullptr;
377	}
378	cond = parseBooleanFormula(children);
379	cond2 = parseBooleanFormula(children->next_sibling());
380	if (cond == nullptr \|\| cond2 == nullptr)
381	{
382	assert(false);
383	return nullptr;
384	}
385	return std::make_shared<OrCondition>(
386	std::make_shared<AndCondition>(cond, std::make_shared<NotCondition>(cond2)),
387	std::make_shared<AndCondition>(std::make_shared<NotCondition>(cond), cond2));
388	} else if (elementName == "implication") {
389	auto children = element->first_node();
390	if (getChildCount(element) != 2)
391	{
392	assert(false);
393	return nullptr;
394	}
395	cond = parseBooleanFormula(children);
396	cond2 = parseBooleanFormula(children->next_sibling());
397	if (cond == nullptr \|\| cond2 == nullptr)
398	{
399	assert(false);
400	return nullptr;
401	}
402	return std::make_shared<OrCondition>(std::make_shared<NotCondition>(cond), cond2);
403	} else if (elementName == "equivalence") {
404	auto children = element->first_node();
405	if (getChildCount(element) != 2)
406	{
407	assert(false);
408	return nullptr;
409	}
410	cond = parseBooleanFormula(children);
411	cond2 = parseBooleanFormula(children->next_sibling());
412	if (cond == nullptr \|\| cond2 == nullptr) return nullptr;
413	return std::make_shared<OrCondition>(std::make_shared<AndCondition>(cond, cond2),
414	std::make_shared<AndCondition>(std::make_shared<NotCondition>(cond),
415	std::make_shared<NotCondition>(cond2)));
416	} else if (elementName == "integer-eq" \|\| elementName == "integer-ne" \|\|
417	elementName == "integer-lt" \|\| elementName == "integer-le" \|\|
418	elementName == "integer-gt" \|\| elementName == "integer-ge") {
419	auto children = element->first_node();
420	if (getChildCount(element) != 2)
421	{
422	assert(false);
423	return nullptr;
424	}
425	Expr_ptr expr1 = parseIntegerExpression(children);
426	Expr_ptr expr2 = parseIntegerExpression(children->next_sibling());
427	if(expr1 == nullptr \|\| expr2 == nullptr)
428	{
429	assert(false);
430	return nullptr;
431	}
432	if (elementName == "integer-eq") return std::make_shared<EqualCondition>(expr1, expr2);
433	else if (elementName == "integer-ne") return std::make_shared<NotEqualCondition>(expr1, expr2);
434	else if (elementName == "integer-lt") return std::make_shared<LessThanCondition>(expr1, expr2);
435	else if (elementName == "integer-le") return std::make_shared<LessThanOrEqualCondition>(expr1, expr2);
436	else if (elementName == "integer-gt") return std::make_shared<GreaterThanCondition>(expr1, expr2);
437	else if (elementName == "integer-ge") return std::make_shared<GreaterThanOrEqualCondition>(expr1, expr2);
438	} else if (elementName == "is-fireable") {
439	size_t nrOfChildren = getChildCount(element);
440	if (nrOfChildren == 0)
441	{
442	assert(false);
443	return nullptr;
444	}
445	std::vector<Condition_ptr> conds;
446	for (auto it = element->first_node(); it; it = it->next_sibling()) {
447	if (strcmp(it->name(), "transition") != 0)
448	{
449	assert(false);
450	return nullptr;
451	}
452	conds.emplace_back(std::make_shared<FireableCondition>(it->value()));
453	}
454	return std::make_shared<OrCondition>(conds);
455	}
456	std::cerr << "An error occurred while parsing the query." << std::endl;
457	std::cerr << elementName << std::endl;
458	assert(false);
459	exit(ErrorCode);
460	return nullptr;
461	}
462
463	Expr_ptr QueryXMLParser::parseIntegerExpression(rapidxml::xml_node<>* element) {
464	string elementName = element->name();
465	if (elementName == "integer-constant") {
466	int i;
467	if (sscanf(element->value(), "%d", &i) == EOF)
468	{
469	assert(false);
470	return nullptr;
471	}
472	return std::make_shared<LiteralExpr>(i);
473	} else if (elementName == "tokens-count") {
474	auto children = element->first_node();
475	std::vector<Expr_ptr> ids;
476	for (auto it = children; it; it = it->next_sibling()) {
477	if (strcmp(it->name(), "place") != 0)
478	{
479	assert(false);
480	return nullptr;
481	}
482	string placeName = parsePlace(it);
483	if (placeName == "")
484	{
485	assert(false);
486	return nullptr; // invalid place name
487	}
488	auto id = std::make_shared<IdentifierExpr>(placeName);
489	ids.emplace_back(id);
490	}
491
492	if (ids.size() == 0)
493	{
494	assert(false);
495	return nullptr;
496	}
497	if (ids.size() == 1) return ids[0];
498
499	return std::make_shared<PlusExpr>(std::move(ids), true);
500	} else if (elementName == "integer-sum" \|\| elementName == "integer-product") {
501	auto children = element->first_node();
502	bool isMult = false;
503	if (elementName == "integer-sum") isMult = false;
504	else if (elementName == "integer-product") isMult = true;
505
506	std::vector<Expr_ptr> els;
507	auto it = children;
508
509	for (; it; it = it->next_sibling()) {
510	els.emplace_back(parseIntegerExpression(it));
511	if(!els.back())
512	{
513	assert(false);
514	return nullptr;
515	}
516	}
517
518	if (els.size() < 2)
519	{
520	assert(false);
521	return nullptr;
522	}
523
524	return isMult ?
525	std::dynamic_pointer_cast<Expr>(std::make_shared<MultiplyExpr>(std::move(els))) :
526	std::dynamic_pointer_cast<Expr>(std::make_shared<PlusExpr>(std::move(els)));
527	;
528	} else if (elementName == "integer-difference") {
529	auto children = element->first_node();
530	std::vector<Expr_ptr> els;
531	for (auto it = children; it; it = it->next_sibling()) {
532	els.emplace_back(parseIntegerExpression(it));
533	}
534	if(els.size() == 1)
535	els.emplace(els.begin(), std::make_shared<LiteralExpr>(0));
536	return std::make_shared<SubtractExpr>(std::move(els));
537	}
538	assert(false);
539	return nullptr;
540	}
541
542	string QueryXMLParser::parsePlace(rapidxml::xml_node<>* element) {
543	if (strcmp(element->name(), "place")) return ""; // missing place tag
544	string placeName = element->value();
545	placeName.erase(std::remove_if(placeName.begin(), placeName.end(), ::isspace), placeName.end());
546	return placeName;
547	}
548
549	void QueryXMLParser::printQueries(size_t i) {
550	// QueryXMLParser::QueriesIterator it;
551	if (i <= 0 \|\| i > queries.size()) {
552	cout << "In printQueries the query index is out of scope\n\n";
553	return;
554	}
555	QueryItem it = queries[i - 1];
556	cout << it.id << ": " ;
557	if (it.parsingResult == QueryItem::UNSUPPORTED_QUERY) {
558	cout << "\t---------- unsupported query ----------" << endl;
559	} else {
560	cout << "\t";
561	it.query->toString(cout);
562	cout << std::endl;
563	}
564	}
565
566	void QueryXMLParser::printQueries() {
567	for (size_t i = 1; i <= queries.size(); i++) {
568	printQueries(i);
569	}
570	}