diff --git a/include/PetriEngine/PQL/Contexts.h b/include/PetriEngine/PQL/Contexts.h index 3d4188313..2e2e6fc95 100644 --- a/include/PetriEngine/PQL/Contexts.h +++ b/include/PetriEngine/PQL/Contexts.h @@ -3,17 +3,17 @@ * Thomas Søndersø Nielsen , * Lars Kærlund Østergaard , * Peter Gjøl Jensen - * + * * 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 . */ @@ -41,7 +41,6 @@ namespace PetriEngine { const std::unordered_map& _placeNames; const std::unordered_map& _transitionNames; const PetriNet* _net; - std::vector _errors; public: /** A resolution result */ @@ -56,26 +55,17 @@ namespace PetriEngine { : _placeNames(places), _transitionNames(tnames), _net(net) { } - + virtual void setHasDeadlock(){}; - + const PetriNet* net() const { return _net; } - + /** Resolve an identifier */ virtual ResolutionResult resolve(const std::string& identifier, bool place = true); - /** Report error */ - void reportError(const ExprError& error) { - _errors.push_back(error); - } - - /** Get list of errors */ - const std::vector& errors() const { - return _errors; - } auto& allPlaceNames() const { return _placeNames; } auto& allTransitionNames() const { return _transitionNames; } @@ -122,13 +112,13 @@ namespace PetriEngine { _marking = marking; _net = net; } - + EvaluationContext() {}; const MarkVal* marking() const { return _marking; } - + void setMarking(MarkVal* marking) { _marking = marking; } @@ -185,7 +175,7 @@ namespace PetriEngine { _start = std::chrono::high_resolution_clock::now(); _cache = cache; } - + virtual ~SimplificationContext() { if(_base_lp != nullptr) glp_delete_prob(_base_lp); @@ -208,27 +198,27 @@ namespace PetriEngine { bool negated() const { return _negated; } - + void setNegate(bool b){ _negated = b; } - + double getReductionTime(); - + bool timeout() const { auto end = std::chrono::high_resolution_clock::now(); auto diff = std::chrono::duration_cast(end - _start); return (diff.count() >= _queryTimeout); } - + uint32_t getLpTimeout() const; Simplification::LPCache* cache() const { return _cache; } - - + + glp_prob* makeBaseLP() const; private: diff --git a/include/PetriEngine/PQL/Expressions.h b/include/PetriEngine/PQL/Expressions.h index 0b0d00537..0b3571f24 100644 --- a/include/PetriEngine/PQL/Expressions.h +++ b/include/PetriEngine/PQL/Expressions.h @@ -218,11 +218,10 @@ namespace PetriEngine { } bool placeFree() const override; auto& expressions() const { return _exprs; } - size_t operands() const { return _exprs.size(); } + size_t size() const { return _exprs.size(); } const Expr_ptr &operator[](size_t i) const { return _exprs[i]; } - virtual std::string op() const = 0; protected: std::vector _exprs; @@ -261,8 +260,6 @@ namespace PetriEngine { protected: int64_t apply(int64_t a, int64_t b) const { return a + b; } - std::string op() const override; - }; /** Binary minus expression */ @@ -276,8 +273,6 @@ namespace PetriEngine { Member constraint(SimplificationContext& context) const override; protected: - //int binaryOp() const; - std::string op() const override; }; /** Binary multiplication expression **/ @@ -290,7 +285,6 @@ namespace PetriEngine { protected: int64_t apply(int64_t a, int64_t b) const { return a * b; } - std::string op() const override; }; /** Unary minus expression*/ @@ -677,10 +671,7 @@ namespace PetriEngine { { return _conds[i]; }; - size_t operands() const { - return _conds.size(); - } - const std::vector& getOperands() const { return _conds; } + const std::vector& operands() const { return _conds; } CTLType getQueryType() const override { return CTLType::LOPERATOR; } Path getPath() const override { return Path::pError; } @@ -828,14 +819,6 @@ namespace PetriEngine { [[nodiscard]] const Expr_ptr &getExpr2() const { return _expr2; } - virtual std::string op() const = 0; - - /** Operator when exported to TAPAAL */ - virtual std::string opTAPAAL() const = 0; - - /** Swapped operator when exported to TAPAAL, e.g. operator when operands are swapped */ - virtual std::string sopTAPAAL() const = 0; - protected: uint32_t _distance(DistanceContext& c, std::function d) const; @@ -856,10 +839,6 @@ namespace PetriEngine { uint32_t distance(DistanceContext& context) const override; virtual type_id_t type() const { return PQL::type_id(); }; - private: - std::string op() const override; - std::string opTAPAAL() const override; - std::string sopTAPAAL() const override; }; /* None equality conditon */ @@ -869,10 +848,6 @@ namespace PetriEngine { using CompareCondition::CompareCondition; uint32_t distance(DistanceContext& context) const override; virtual type_id_t type() const { return PQL::type_id(); }; - private: - std::string op() const override; - std::string opTAPAAL() const override; - std::string sopTAPAAL() const override; }; /* Less-than conditon */ @@ -882,10 +857,6 @@ namespace PetriEngine { using CompareCondition::CompareCondition; uint32_t distance(DistanceContext& context) const override; virtual type_id_t type() const { return PQL::type_id(); }; - private: - std::string op() const override; - std::string opTAPAAL() const override; - std::string sopTAPAAL() const override; }; /* Less-than-or-equal conditon */ @@ -896,10 +867,6 @@ namespace PetriEngine { uint32_t distance(DistanceContext& context) const override; virtual type_id_t type() const { return PQL::type_id(); }; - private: - std::string op() const override; - std::string opTAPAAL() const override; - std::string sopTAPAAL() const override; }; /* Bool condition */ @@ -907,11 +874,6 @@ namespace PetriEngine { public: BooleanCondition(bool value) : value(value) { - if (value) { - trivial = 1; - } else { - trivial = 2; - } } uint32_t distance(DistanceContext& context) const override; static Condition_ptr TRUE_CONSTANT; diff --git a/include/PetriEngine/PQL/PQL.h b/include/PetriEngine/PQL/PQL.h index d22d7ec54..ce3ea2f0f 100644 --- a/include/PetriEngine/PQL/PQL.h +++ b/include/PetriEngine/PQL/PQL.h @@ -59,52 +59,29 @@ namespace PetriEngine { } } + bool is_true(const Condition& c); + bool is_false(const Condition& c); + template + bool is_true(const C* c) { return is_true(*c); } + template + bool is_false(const C* c) { return is_false(*c); } + template + bool is_true(const std::shared_ptr& c) { return is_true(c.get()); } + template + bool is_false(const std::shared_ptr& c) { return is_false(c.get()); } + enum CTLType {PATHQEURY = 1, LOPERATOR = 2, EVAL = 3, TYPE_ERROR = -1}; enum Quantifier { AND = 1, OR = 2, A = 3, E = 4, NEG = 5, COMPCONJ = 6, DEADLOCK = 7, UPPERBOUNDS = 8, PN_BOOLEAN = 9, BControl = 10, EMPTY = -1 }; enum Path { G = 1, X = 2, F = 3, U = 4, PControl = 5, pError = -1 }; - class AnalysisContext; - class EvaluationContext; class DistanceContext; class SimplificationContext; - /** Representation of a PQL error */ - class ExprError { - std::string _text; - int _length; - public: - - ExprError(std::string text = "", int length = 0) { - _text = text; - _length = length; - } - - /** Human readable explaination of the error */ - const std::string& text() const { - return _text; - } - - /** length in the source, 0 if not applicable */ - int length() const { - return _length; - } - - /** Convert error to string */ - std::string toString() const { - return "Parsing error \"" + text() + "\""; - } - - /** True, if this is a default created ExprError without any information */ - bool isEmpty() const { - return _text.empty() && _length == 0; - } - }; - /** Representation of an expression */ class Expr { - int _eval = 0; + int64_t _eval = 0; public: /** Virtual destructor, an expression should know it subexpressions */ virtual ~Expr(); @@ -115,11 +92,11 @@ namespace PetriEngine { [[nodiscard]] virtual bool placeFree() const = 0; - void setEval(int eval) { + void setEval(int64_t eval) { _eval = eval; } - [[nodiscard]] int getEval() const { + [[nodiscard]] int64_t getEval() const { return _eval; } }; @@ -197,11 +174,6 @@ namespace PetriEngine { /** Get distance to query */ [[nodiscard]] virtual uint32_t distance(DistanceContext& context) const = 0; - /** Checks if the condition is trivially true */ - [[nodiscard]] bool isTriviallyTrue(); - /*** Checks if the condition is trivially false */ - [[nodiscard]] bool isTriviallyFalse(); - [[nodiscard]] bool isSatisfied() const { return _eval == RTRUE; @@ -237,10 +209,6 @@ namespace PetriEngine { [[nodiscard]] virtual Path getPath() const = 0; void toString(std::ostream& os = std::cout); virtual type_id_t type() const = 0; - protected: - //Value for checking if condition is trivially true or false. - //0 is undecided (default), 1 is true, 2 is false. - uint32_t trivial = 0; }; typedef std::shared_ptr Condition_ptr; using Condition_constptr = std::shared_ptr; diff --git a/src/PetriEngine/PQL/Analyze.cpp b/src/PetriEngine/PQL/Analyze.cpp index b5f910afd..e6212e607 100644 --- a/src/PetriEngine/PQL/Analyze.cpp +++ b/src/PetriEngine/PQL/Analyze.cpp @@ -50,9 +50,7 @@ namespace PetriEngine::PQL { if (result.success) { i.first = result.offset; } else { - ExprError error("Unable to resolve identifier \"" + i.second + "\"", - i.second.length()); - _context.reportError(error); + throw base_error("Unable to resolve identifier \"", i.second, "\""); } } for(auto& e : element->expressions()) @@ -84,9 +82,7 @@ namespace PetriEngine::PQL { if (result.success) { return result.offset; } else { - ExprError error("Unable to resolve identifier \"" + name + "\"", - name.length()); - context.reportError(error); + throw base_error("Unable to resolve identifier \"", name, "\""); } return -1; } @@ -107,8 +103,7 @@ namespace PetriEngine::PQL { { std::unordered_map names; if (!coloredContext->resolvePlace(element->name(), names)) { - ExprError error("Unable to resolve colored identifier \"" + element->name() + "\"", element->name().length()); - coloredContext->reportError(error); + throw base_error("Unable to resolve colored identifier \"", element->name(), "\""); } if (names.size() == 1) { @@ -132,8 +127,7 @@ namespace PetriEngine::PQL { if (result.success) { element->_offsetInMarking = result.offset; } else { - ExprError error("Unable to resolve identifier \"" + element->name() + "\"", element->name().length()); - _context.reportError(error); + throw base_error("Unable to resolve identifier \"", element->name(), "\""); } } @@ -144,8 +138,7 @@ namespace PetriEngine::PQL { AnalysisContext::ResolutionResult result = _context.resolve(element->getName(), false); if (!result.success) { - ExprError error("Unable to resolve identifier \"" + element->getName() + "\"", element->getName().length()); - _context.reportError(error); + throw base_error("Unable to resolve identifier \"" + element->getName() + "\""); return; } @@ -182,8 +175,7 @@ namespace PetriEngine::PQL { if(coloredContext != nullptr && coloredContext->isColored()) { std::vector names; if (!coloredContext->resolveTransition(element->getName(), names)) { - ExprError error("Unable to resolve colored identifier \"" + element->getName() + "\"", element->getName().length()); - coloredContext->reportError(error); + throw base_error("Unable to resolve colored identifier \"", element->getName(), "\""); return; } if(names.size() < 1){ @@ -262,7 +254,7 @@ namespace PetriEngine::PQL { } void AnalyzeVisitor::_accept(LogicalCondition *element) { - for (auto& cond : element->getOperands()) + for (auto& cond : element->operands()) Visitor::visit(this, cond); } @@ -368,8 +360,7 @@ namespace PetriEngine::PQL { { std::unordered_map names; if (!coloredContext->resolvePlace(p, names)) { - ExprError error("Unable to resolve colored identifier \"" + p + "\"", p.length()); - coloredContext->reportError(error); + throw base_error("Unable to resolve colored identifier \"", p, "\""); } for(auto& id : names) @@ -390,9 +381,7 @@ namespace PetriEngine::PQL { if (result.success) { p._place = result.offset; } else { - ExprError error("Unable to resolve identifier \"" + p._name + "\"", - p._name.length()); - _context.reportError(error); + throw base_error("Unable to resolve identifier \"", p._name, "\""); } } std::sort(element->_places.begin(), element->_places.end()); diff --git a/src/PetriEngine/PQL/BinaryPrinter.cpp b/src/PetriEngine/PQL/BinaryPrinter.cpp index 6473e240b..747e57efe 100644 --- a/src/PetriEngine/PQL/BinaryPrinter.cpp +++ b/src/PetriEngine/PQL/BinaryPrinter.cpp @@ -47,8 +47,12 @@ namespace PetriEngine::PQL { } void BinaryPrinter::_accept(const CommutativeExpr *element){ - auto sop = element->op(); - os.write(&sop[0], sizeof(char)); + if (PQL::type_id() == element->type()) + os.write("+", 1); + else if (PQL::type_id() == element->type()) + os.write("*", 1); + else + throw base_error("Unknown type for BinaryPrinter"); int32_t temp_constant = element->constant(); os.write(reinterpret_cast(&temp_constant), sizeof(int32_t)); uint32_t size = element->places().size(); @@ -83,7 +87,7 @@ namespace PetriEngine::PQL { auto quant = condition->getQuantifier(); os.write(reinterpret_cast(&path), sizeof(Path)); os.write(reinterpret_cast(&quant), sizeof(Quantifier)); - uint32_t size = condition->operands(); + uint32_t size = condition->size(); os.write(reinterpret_cast(&size), sizeof(uint32_t)); for(auto& c : *condition) Visitor::visit(this, c); @@ -111,8 +115,23 @@ namespace PetriEngine::PQL { auto quant = condition->getQuantifier(); os.write(reinterpret_cast(&path), sizeof(Path)); os.write(reinterpret_cast(&quant), sizeof(Quantifier)); - std::string sop = condition->op(); - os.write(sop.data(), sop.size()); + switch(condition->type()) + { + case PQL::type_id(): + os.write("<", 1); + break; + case PQL::type_id(): + os.write("<=", 2); + break; + case PQL::type_id(): + os.write("=", 1); + break; + case PQL::type_id(): + os.write("!", 1); + break; + default: + assert(false); + } os.write("\0", sizeof(char)); Visitor::visit(this, (*condition)[0]); Visitor::visit(this, (*condition)[1]); diff --git a/src/PetriEngine/PQL/CTLVisitor.cpp b/src/PetriEngine/PQL/CTLVisitor.cpp index ac51cbc40..6dc7a6b27 100644 --- a/src/PetriEngine/PQL/CTLVisitor.cpp +++ b/src/PetriEngine/PQL/CTLVisitor.cpp @@ -26,8 +26,8 @@ namespace PetriEngine::PQL { } void IsCTLVisitor::_accept(const LogicalCondition *element) { - for (size_t i = 0; i < element->operands(); i++){ - Visitor::visit(this, (*element)[i]); + for (auto& e : *element){ + Visitor::visit(this, e); if (_cur_type != CTLSyntaxType::BOOLEAN){ isCTL = false; break; diff --git a/src/PetriEngine/PQL/Evaluation.cpp b/src/PetriEngine/PQL/Evaluation.cpp index 6c18d6456..019e71750 100644 --- a/src/PetriEngine/PQL/Evaluation.cpp +++ b/src/PetriEngine/PQL/Evaluation.cpp @@ -85,7 +85,7 @@ namespace PetriEngine { namespace PQL { { Visitor::visit(this, (*element)[0]); int64_t r = _value; - for(size_t i = 1; i < element->operands(); ++i) + for(size_t i = 1; i < element->size(); ++i) { Visitor::visit(this, (*element)[i]); r -= _value; @@ -198,7 +198,7 @@ namespace PetriEngine { namespace PQL { void EvaluateVisitor::_accept(AndCondition *element) { auto res = Condition::RTRUE; - for (auto &c: element->getOperands()) { + for (auto &c: *element) { Visitor::visit(this, c); if (_return_value == Condition::RFALSE) { _return_value = {Condition::RFALSE}; @@ -211,7 +211,7 @@ namespace PetriEngine { namespace PQL { void EvaluateVisitor::_accept(OrCondition *element) { auto res = Condition::RFALSE; - for (auto &c: element->getOperands()) { + for (auto &c: *element) { Visitor::visit(this, c); if (_return_value == Condition::RTRUE) { _return_value = {Condition::RTRUE}; @@ -344,7 +344,7 @@ namespace PetriEngine { namespace PQL { void EvaluateAndSetVisitor::_accept(AndCondition *element) { Condition::Result res = Condition::RTRUE; - for (auto &c: element->getOperands()) { + for (auto &c: *element) { Visitor::visit(this, c); if (_return_value == Condition::RFALSE) { res = Condition::RFALSE; @@ -359,7 +359,7 @@ namespace PetriEngine { namespace PQL { void EvaluateAndSetVisitor::_accept(OrCondition *element) { Condition::Result res = Condition::RFALSE; - for (auto &c: element->getOperands()) { + for (auto &c: *element) { Visitor::visit(this, c); if (_return_value == Condition::RTRUE) { res = Condition::RTRUE; diff --git a/src/PetriEngine/PQL/Expressions.cpp b/src/PetriEngine/PQL/Expressions.cpp index d8e522a26..cd0d64063 100644 --- a/src/PetriEngine/PQL/Expressions.cpp +++ b/src/PetriEngine/PQL/Expressions.cpp @@ -168,40 +168,6 @@ namespace PetriEngine { } } - /******************** opTAPAAL ********************/ - - std::string EqualCondition::opTAPAAL() const { - return "="; - } - - std::string NotEqualCondition::opTAPAAL() const { - return "="; - } //Handled with hack in NotEqualCondition::toTAPAALQuery - - std::string LessThanCondition::opTAPAAL() const { - return "<"; - } - - std::string LessThanOrEqualCondition::opTAPAAL() const { - return "<="; - } - - std::string EqualCondition::sopTAPAAL() const { - return "="; - } - - std::string NotEqualCondition::sopTAPAAL() const { - return "="; - } //Handled with hack in NotEqualCondition::toTAPAALQuery - - std::string LessThanCondition::sopTAPAAL() const { - return ">="; - } - - std::string LessThanOrEqualCondition::sopTAPAAL() const { - return ">"; - } - size_t UnfoldedUpperBoundsCondition::value(const MarkVal* marking) { size_t tmp = 0; @@ -214,40 +180,6 @@ namespace PetriEngine { return tmp; } - /******************** Op (BinaryExpr subclasses) ********************/ - - std::string PlusExpr::op() const { - return "+"; - } - - std::string SubtractExpr::op() const { - return "-"; - } - - std::string MultiplyExpr::op() const { - return "*"; - } - - /******************** Op (CompareCondition subclasses) ********************/ - - std::string EqualCondition::op() const { - return "=="; - } - - std::string NotEqualCondition::op() const { - return "!="; - } - - std::string LessThanCondition::op() const { - return "<"; - } - - std::string LessThanOrEqualCondition::op() const { - return "<="; - } - - /******************** free of places ********************/ - bool NaryExpr::placeFree() const { for(auto& e : _exprs) diff --git a/src/PetriEngine/PQL/PQL.cpp b/src/PetriEngine/PQL/PQL.cpp index dfc86d0bc..fcc507141 100644 --- a/src/PetriEngine/PQL/PQL.cpp +++ b/src/PetriEngine/PQL/PQL.cpp @@ -27,20 +27,14 @@ namespace PetriEngine { Expr::~Expr()= default; - bool Condition::isTriviallyTrue() { - if (trivial == 1) { - return true; - } - - return false; + bool is_true(const Condition& c) + { + return c.type() == type_id() && static_cast(c).value; } - bool Condition::isTriviallyFalse() { - if (trivial == 2) { - return true; - } - - return false; + bool is_false(const Condition& c) + { + return c.type() == type_id() && !static_cast(c).value; } Condition::~Condition() = default; diff --git a/src/PetriEngine/PQL/PredicateCheckers.cpp b/src/PetriEngine/PQL/PredicateCheckers.cpp index eac22debf..8d2e5991c 100644 --- a/src/PetriEngine/PQL/PredicateCheckers.cpp +++ b/src/PetriEngine/PQL/PredicateCheckers.cpp @@ -37,7 +37,7 @@ namespace PetriEngine::PQL { void NestedDeadlockVisitor::_accept(const LogicalCondition *condition) { _nested_in_logical_condition = true; - for (auto& c : condition->getOperands()) + for (auto& c : *condition) Visitor::visit(this, c); _nested_in_logical_condition = false; } @@ -139,7 +139,7 @@ namespace PetriEngine::PQL { void IsNotReachabilityVisitor::_accept(const LogicalCondition *element) { if (_is_nested) { - for(auto& c : element->getOperands()) + for(auto& c : *element) { Visitor::visit(this, c); if(_condition_found) diff --git a/src/PetriEngine/PQL/PushNegation.cpp b/src/PetriEngine/PQL/PushNegation.cpp index ec555744c..37c246dbb 100644 --- a/src/PetriEngine/PQL/PushNegation.cpp +++ b/src/PetriEngine/PQL/PushNegation.cpp @@ -462,8 +462,8 @@ namespace PetriEngine::PQL { std::vector nef, other; for (auto &c: _conds) { auto n = subvisit(c, _nested, negate_children); - if (n->isTriviallyFalse()) return n; - if (n->isTriviallyTrue()) continue; + if (is_false(n)) return n; + if (is_true(n)) continue; if (auto neg = dynamic_cast(n.get())) { if (auto ef = dynamic_cast((*neg)[0].get())) { nef.push_back((*ef)[0]); @@ -495,10 +495,10 @@ namespace PetriEngine::PQL { std::vector nef, other; for (auto &c: _conds) { auto n = subvisit(c, _nested, negate_children); - if (n->isTriviallyTrue()) { + if (is_true(n)) { return n; } - if (n->isTriviallyFalse()) continue; + if (is_false(n)) continue; if (auto ef = dynamic_cast(n.get())) { nef.push_back((*ef)[0]); } else { @@ -520,8 +520,8 @@ namespace PetriEngine::PQL { void PushNegationVisitor::_accept(OrCondition *element) { auto cond = initialMarkingRW([&]() -> Condition_ptr { - return negated ? pushAnd(element->getOperands(), nested, true) : - pushOr(element->getOperands(), nested, false); + return negated ? pushAnd(element->operands(), nested, true) : + pushOr(element->operands(), nested, false); }, stats, context, nested, negated, initrw); RETURN(cond) } @@ -529,8 +529,8 @@ namespace PetriEngine::PQL { void PushNegationVisitor::_accept(AndCondition *element) { auto cond = initialMarkingRW([&]() -> Condition_ptr { - return negated ? pushOr(element->getOperands(), nested, true) : - pushAnd(element->getOperands(), nested, false); + return negated ? pushOr(element->operands(), nested, true) : + pushAnd(element->operands(), nested, false); }, stats, context, nested, negated, initrw); RETURN(cond); diff --git a/src/PetriEngine/PQL/QueryPrinter.cpp b/src/PetriEngine/PQL/QueryPrinter.cpp index 5c7e4ce6e..b7ba090fa 100644 --- a/src/PetriEngine/PQL/QueryPrinter.cpp +++ b/src/PetriEngine/PQL/QueryPrinter.cpp @@ -29,7 +29,7 @@ namespace PetriEngine { void QueryPrinter::_accept(const LogicalCondition *element, const std::string &op) { os << "("; Visitor::visit(this, (*element)[0]); - for (size_t i = 1; i < element->operands(); ++i) { + for (size_t i = 1; i < element->size(); ++i) { os << " " << op << " "; Visitor::visit(this, (*element)[i]); } @@ -264,7 +264,7 @@ namespace PetriEngine { void QueryPrinter::_accept(const NaryExpr *element, const std::string &op) { os << "("; Visitor::visit(this, (*element)[0]); - for(size_t i = 1; i < element->operands(); ++i) + for(size_t i = 1; i < element->size(); ++i) { os << " " << op << " "; Visitor::visit(this, (*element)[i]); diff --git a/src/PetriEngine/PQL/Simplifier.cpp b/src/PetriEngine/PQL/Simplifier.cpp index db01e5a5a..e25a2eeac 100644 --- a/src/PetriEngine/PQL/Simplifier.cpp +++ b/src/PetriEngine/PQL/Simplifier.cpp @@ -48,15 +48,15 @@ namespace PetriEngine::PQL { std::vector conditions; std::vector lps, neglpsv; - for (const auto &c: element->getOperands()) { + for (const auto &c: *element) { Visitor::visit(this, c); auto r = std::move(return_value); assert(r.neglps); assert(r.lps); - if (r.formula->isTriviallyTrue()) { + if (is_true(r.formula)) { return Retval(BooleanCondition::TRUE_CONSTANT); - } else if (r.formula->isTriviallyFalse()) { + } else if (is_false(r.formula)) { continue; } conditions.push_back(r.formula); @@ -95,12 +95,12 @@ namespace PetriEngine::PQL { std::vector conditions; std::vector lpsv; std::vector neglps; - for (auto &c: element->getOperands()) { + for (auto &c: *element) { Visitor::visit(this, c); auto r = std::move(return_value); - if (r.formula->isTriviallyFalse()) { + if (is_false(r.formula)) { return Retval(BooleanCondition::FALSE_CONSTANT); - } else if (r.formula->isTriviallyTrue()) { + } else if (is_true(r.formula)) { continue; } @@ -138,9 +138,9 @@ namespace PetriEngine::PQL { /************ Auxiliary functions for quantifier simplification ***********/ Retval Simplifier::simplifyAG(Retval &r) { - if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)) { + if (is_true(r.formula) || !r.neglps->satisfiable(context)) { return Retval(BooleanCondition::TRUE_CONSTANT); - } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(context)) { + } else if (is_false(r.formula) || !r.lps->satisfiable(context)) { return Retval(BooleanCondition::FALSE_CONSTANT); } else { return Retval(std::make_shared(r.formula)); @@ -148,9 +148,9 @@ namespace PetriEngine::PQL { } Retval Simplifier::simplifyAF(Retval &r) { - if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)) { + if (is_true(r.formula) || !r.neglps->satisfiable(context)) { return Retval(BooleanCondition::TRUE_CONSTANT); - } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(context)) { + } else if (is_false(r.formula) || !r.lps->satisfiable(context)) { return Retval(BooleanCondition::FALSE_CONSTANT); } else { return Retval(std::make_shared(r.formula)); @@ -158,9 +158,9 @@ namespace PetriEngine::PQL { } Retval Simplifier::simplifyAX(Retval &r) { - if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)) { + if (is_true(r.formula) || !r.neglps->satisfiable(context)) { return Retval(BooleanCondition::TRUE_CONSTANT); - } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(context)) { + } else if (is_false(r.formula) || !r.lps->satisfiable(context)) { return Retval(std::make_shared()); } else { return Retval(std::make_shared(r.formula)); @@ -168,9 +168,9 @@ namespace PetriEngine::PQL { } Retval Simplifier::simplifyEG(Retval &r) { - if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)) { + if (is_true(r.formula) || !r.neglps->satisfiable(context)) { return Retval(BooleanCondition::TRUE_CONSTANT); - } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(context)) { + } else if (is_false(r.formula) || !r.lps->satisfiable(context)) { return Retval(BooleanCondition::FALSE_CONSTANT); } else { return Retval(std::make_shared(r.formula)); @@ -178,9 +178,9 @@ namespace PetriEngine::PQL { } Retval Simplifier::simplifyEF(Retval &r) { - if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)) { + if (is_true(r.formula) || !r.neglps->satisfiable(context)) { return Retval(BooleanCondition::TRUE_CONSTANT); - } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(context)) { + } else if (is_false(r.formula) || !r.lps->satisfiable(context)) { return Retval(BooleanCondition::FALSE_CONSTANT); } else { return Retval(std::make_shared(r.formula)); @@ -188,10 +188,10 @@ namespace PetriEngine::PQL { } Retval Simplifier::simplifyEX(Retval &r) { - if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)) { + if (is_true(r.formula) || !r.neglps->satisfiable(context)) { return Retval(std::make_shared( std::make_shared())); - } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(context)) { + } else if (is_false(r.formula) || !r.lps->satisfiable(context)) { return Retval(BooleanCondition::FALSE_CONSTANT); } else { return Retval(std::make_shared(r.formula)); @@ -201,9 +201,9 @@ namespace PetriEngine::PQL { template Retval Simplifier::simplifySimpleQuant(Retval &r) { static_assert(std::is_base_of_v); - if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)) { + if (is_true(r.formula) || !r.neglps->satisfiable(context)) { return Retval(BooleanCondition::TRUE_CONSTANT); - } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(context)) { + } else if (is_false(r.formula) || !r.lps->satisfiable(context)) { return Retval(BooleanCondition::FALSE_CONSTANT); } else { return Retval(std::make_shared(r.formula)); @@ -279,9 +279,9 @@ namespace PetriEngine::PQL { void Simplifier::_accept(const AndCondition *element) { if (context.timeout()) { if (context.negated()) { - RETURN(Retval(std::make_shared(makeAnd(element->getOperands())))) + RETURN(Retval(std::make_shared(makeAnd(element->operands())))) } else { - RETURN(Retval(makeAnd(element->getOperands()))) + RETURN(Retval(makeAnd(element->operands()))) } } @@ -295,9 +295,9 @@ namespace PetriEngine::PQL { void Simplifier::_accept(const OrCondition *element) { if (context.timeout()) { if (context.negated()) { - RETURN(Retval(std::make_shared(makeOr(element->getOperands())))) + RETURN(Retval(std::make_shared(makeOr(element->operands())))) } else { - RETURN(Retval(makeOr(element->getOperands()))) + RETURN(Retval(makeOr(element->operands()))) } } if (context.negated()) { @@ -667,10 +667,10 @@ namespace PetriEngine::PQL { void Simplifier::_accept(const ControlCondition *condition) { Visitor::visit(this, condition->getCond()); - if(return_value.formula->isTriviallyTrue() || return_value.formula->isTriviallyFalse()) + if(is_true(return_value.formula) || is_false(return_value.formula)) { - bool is_true = return_value.formula->isTriviallyTrue() xor (!context.negated()); - RETURN(Retval(is_true ? + bool val = is_true(return_value.formula) xor (!context.negated()); + RETURN(Retval(val ? Retval(BooleanCondition::TRUE_CONSTANT) : Retval(BooleanCondition::FALSE_CONSTANT))) } @@ -719,12 +719,12 @@ namespace PetriEngine::PQL { context.setNegate(false); Visitor::visit(this, (*condition)[1]); Retval r2 = std::move(return_value); - if (r2.formula->isTriviallyTrue() || !r2.neglps->satisfiable(context)) { + if (is_true(r2.formula) || !r2.neglps->satisfiable(context)) { context.setNegate(neg); RETURN(neg ? Retval(BooleanCondition::FALSE_CONSTANT) : Retval(BooleanCondition::TRUE_CONSTANT)) - } else if (r2.formula->isTriviallyFalse() || !r2.lps->satisfiable(context)) { + } else if (is_false(r2.formula) || !r2.lps->satisfiable(context)) { context.setNegate(neg); RETURN(neg ? Retval(BooleanCondition::TRUE_CONSTANT) : @@ -735,19 +735,19 @@ namespace PetriEngine::PQL { context.setNegate(neg); if (context.negated()) { - if (r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(context)) { + if (is_true(r1.formula) || !r1.neglps->satisfiable(context)) { RETURN(Retval(std::make_shared( std::make_shared(r2.formula)))) - } else if (r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(context)) { + } else if (is_false(r1.formula) || !r1.lps->satisfiable(context)) { RETURN(Retval(std::make_shared(r2.formula))) } else { RETURN(Retval(std::make_shared( std::make_shared(r1.formula, r2.formula)))) } } else { - if (r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(context)) { + if (is_true(r1.formula) || !r1.neglps->satisfiable(context)) { RETURN(Retval(std::make_shared(r2.formula))) - } else if (r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(context)) { + } else if (is_false(r1.formula) || !r1.lps->satisfiable(context)) { RETURN(std::move(r2)) } else { RETURN(Retval(std::make_shared(r1.formula, r2.formula))) @@ -761,12 +761,12 @@ namespace PetriEngine::PQL { context.setNegate(false); Visitor::visit(this, condition->getCond2()); Retval r2 = std::move(return_value); - if (r2.formula->isTriviallyTrue() || !r2.neglps->satisfiable(context)) { + if (is_true(r2.formula) || !r2.neglps->satisfiable(context)) { context.setNegate(neg); RETURN(neg ? Retval(BooleanCondition::FALSE_CONSTANT) : Retval(BooleanCondition::TRUE_CONSTANT)) - } else if (r2.formula->isTriviallyFalse() || !r2.lps->satisfiable(context)) { + } else if (is_false(r2.formula) || !r2.lps->satisfiable(context)) { context.setNegate(neg); RETURN(neg ? Retval(BooleanCondition::TRUE_CONSTANT) : @@ -777,19 +777,19 @@ namespace PetriEngine::PQL { context.setNegate(neg); if (context.negated()) { - if (r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(context)) { + if (is_true(r1.formula) || !r1.neglps->satisfiable(context)) { RETURN(Retval(std::make_shared( std::make_shared(r2.formula)))) - } else if (r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(context)) { + } else if (is_false(r1.formula) || !r1.lps->satisfiable(context)) { RETURN(Retval(std::make_shared(r2.formula))) } else { RETURN(Retval(std::make_shared( std::make_shared(r1.formula, r2.formula)))) } } else { - if (r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(context)) { + if (is_true(r1.formula) || !r1.neglps->satisfiable(context)) { RETURN(Retval(std::make_shared(r2.formula))) - } else if (r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(context)) { + } else if (is_false(r1.formula) || !r1.lps->satisfiable(context)) { RETURN(std::move(r2)) } else { RETURN(Retval(std::make_shared(r1.formula, r2.formula))) @@ -803,12 +803,12 @@ namespace PetriEngine::PQL { Visitor::visit(this, condition->getCond2()); Retval r2 = std::move(return_value); - if (r2.formula->isTriviallyTrue() || !r2.neglps->satisfiable(context)) { + if (is_true(r2.formula) || !r2.neglps->satisfiable(context)) { context.setNegate(neg); RETURN(neg ? Retval(BooleanCondition::FALSE_CONSTANT) : Retval(BooleanCondition::TRUE_CONSTANT)) - } else if (r2.formula->isTriviallyFalse() || !r2.lps->satisfiable(context)) { + } else if (is_false(r2.formula) || !r2.lps->satisfiable(context)) { context.setNegate(neg); RETURN(neg ? Retval(BooleanCondition::TRUE_CONSTANT) : @@ -820,19 +820,19 @@ namespace PetriEngine::PQL { context.setNegate(neg); if (context.negated()) { - if (r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(context)) { + if (is_true(r1.formula) || !r1.neglps->satisfiable(context)) { RETURN(Retval(std::make_shared( std::make_shared(r2.formula)))) - } else if (r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(context)) { + } else if (is_false(r1.formula) || !r1.lps->satisfiable(context)) { RETURN(Retval(std::make_shared(r2.formula))) } else { RETURN(Retval(std::make_shared( std::make_shared(r1.formula, r2.formula)))) } } else { - if (r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(context)) { + if (is_true(r1.formula) || !r1.neglps->satisfiable(context)) { RETURN(Retval(std::make_shared(r2.formula))) - } else if (r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(context)) { + } else if (is_false(r1.formula) || !r1.lps->satisfiable(context)) { RETURN(std::move(r2)) } else { RETURN(Retval(std::make_shared(r1.formula, r2.formula))) diff --git a/src/PetriParse/QueryBinaryParser.cpp b/src/PetriParse/QueryBinaryParser.cpp index 49be8f614..2eddbc5dc 100644 --- a/src/PetriParse/QueryBinaryParser.cpp +++ b/src/PetriParse/QueryBinaryParser.cpp @@ -126,14 +126,10 @@ Condition_ptr QueryBinaryParser::parseQuery(std::istream& binary, const std::vec if(sop == "<") return std::make_shared(e1, e2); else if(sop == "<=") - return std::make_shared(e1, e2); - else if(sop == ">=") - return std::make_shared(e2, e1); - else if(sop == ">") return std::make_shared(e2, e1); - else if(sop == "==") + else if(sop == "=") return std::make_shared(e1, e2); - else if(sop == "!=") + else if(sop == "!") return std::make_shared(e1, e2); else { diff --git a/src/VerifyPN.cpp b/src/VerifyPN.cpp index cbf9079e1..9ce5b8989 100644 --- a/src/VerifyPN.cpp +++ b/src/VerifyPN.cpp @@ -54,18 +54,8 @@ using namespace PetriEngine::Reachability; ReturnValue contextAnalysis(ColoredPetriNetBuilder& cpnBuilder, PetriNetBuilder& builder, const PetriNet* net, std::vector >& queries) { //Context analysis ColoredAnalysisContext context(builder.getPlaceNames(), builder.getTransitionNames(), net, cpnBuilder.getUnfoldedPlaceNames(), cpnBuilder.getUnfoldedTransitionNames(), cpnBuilder.isColored()); - for (auto& q : queries) { + for (auto& q : queries) PetriEngine::PQL::analyze(q, context); - - //Print errors if any - if (context.errors().size() > 0) { - std::stringstream ss; - for (size_t i = 0; i < context.errors().size(); i++) { - ss << "Query Context Analysis Error: " << context.errors()[i].toString() << "\n"; - } - throw base_error(ss.str()); - } - } return ReturnValue::ContinueCode; } @@ -210,7 +200,7 @@ void writeQueries(const std::vector>&queries, std::ve out.open(filename, std::ios::binary | std::ios::out); uint32_t cnt = 0; for (uint32_t j = 0; j < queries.size(); j++) { - if (queries[j]->isTriviallyTrue() || queries[j]->isTriviallyFalse()) continue; + if (PQL::is_true(queries[j]) || PQL::is_false(queries[j])) continue; ++cnt; } out.write(reinterpret_cast (&cnt), sizeof (uint32_t)); @@ -228,7 +218,7 @@ void writeQueries(const std::vector>&queries, std::ve for (uint32_t j = 0; j < queries.size(); j++) { auto i = order[j]; - if (queries[i]->isTriviallyTrue() || queries[i]->isTriviallyFalse()) continue; + if (PQL::is_true(queries[i]) || PQL::is_false(queries[i])) continue; if (binary) { out.write(querynames[i].data(), querynames[i].size()); out.write("\0", sizeof (char)); @@ -330,7 +320,7 @@ Condition_ptr simplify_ltl_query(Condition_ptr query, return LTL::simplify(pushNegation(cond, stats, evalContext, false, false, true), options); }, stats, evalContext, false, false, true); - if (cond->isTriviallyTrue() || cond->isTriviallyFalse()) { + if (PQL::is_true(cond) || PQL::is_false(cond)) { // nothing } else if (wasACond) { cond = std::make_shared(cond); @@ -488,9 +478,9 @@ void simplify_queries( const MarkVal* marking, out << "Skipping linear-programming (-q 0)" << std::endl; } if (options.cpnOverApprox && wasAGCPNApprox) { - if (queries[i]->isTriviallyTrue()) + if (PQL::is_true(queries[i])) queries[i] = std::make_shared(false); - else if (queries[i]->isTriviallyFalse()) + else if (PQL::is_false(queries[i])) queries[i] = std::make_shared(true); queries[i]->setInvariant(wasAGCPNApprox); } diff --git a/src/main.cpp b/src/main.cpp index 421a0919a..2871086c5 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -203,7 +203,7 @@ int main(int argc, const char** argv) { if (!options.statespaceexploration) { for (size_t i = 0; i < queries.size(); ++i) { - if (queries[i]->isTriviallyTrue()) { + if (PQL::is_true(queries[i])) { if(initial_marking_solved.count(i) > 0 && options.trace != TraceLevel::None) { // we misuse the implementation to make sure we print the empty-trace @@ -219,7 +219,7 @@ int main(int argc, const char** argv) { } else if (options.printstatistics) { std::cout << "Query solved by Query Simplification.\n" << std::endl; } - } else if (queries[i]->isTriviallyFalse()) { + } else if (PQL::is_false(queries[i])) { if(initial_marking_solved.count(i) > 0 && options.trace != TraceLevel::None) { // we misuse the implementation to make sure we print the empty-trace