Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 15 additions & 25 deletions include/PetriEngine/PQL/Contexts.h
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@
* Thomas Søndersø Nielsen <primogens@gmail.com>,
* Lars Kærlund Østergaard <larsko@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/>.
*/
Expand Down Expand Up @@ -41,7 +41,6 @@ namespace PetriEngine {
const std::unordered_map<std::string, uint32_t>& _placeNames;
const std::unordered_map<std::string, uint32_t>& _transitionNames;
const PetriNet* _net;
std::vector<ExprError> _errors;
public:

/** A resolution result */
Expand All @@ -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<ExprError>& errors() const {
return _errors;
}
auto& allPlaceNames() const { return _placeNames; }
auto& allTransitionNames() const { return _transitionNames; }

Expand Down Expand Up @@ -122,13 +112,13 @@ namespace PetriEngine {
_marking = marking;
_net = net;
}

EvaluationContext() {};

const MarkVal* marking() const {
return _marking;
}

void setMarking(MarkVal* marking) {
_marking = marking;
}
Expand Down Expand Up @@ -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);
Expand All @@ -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<std::chrono::seconds>(end - _start);
return (diff.count() >= _queryTimeout);
}

uint32_t getLpTimeout() const;

Simplification::LPCache* cache() const
{
return _cache;
}


glp_prob* makeBaseLP() const;

private:
Expand Down
42 changes: 2 additions & 40 deletions include/PetriEngine/PQL/Expressions.h
Original file line number Diff line number Diff line change
Expand Up @@ -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<Expr_ptr> _exprs;
Expand Down Expand Up @@ -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 */
Expand All @@ -276,8 +273,6 @@ namespace PetriEngine {
Member constraint(SimplificationContext& context) const override;

protected:
//int binaryOp() const;
std::string op() const override;
};

/** Binary multiplication expression **/
Expand All @@ -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*/
Expand Down Expand Up @@ -677,10 +671,7 @@ namespace PetriEngine {
{
return _conds[i];
};
size_t operands() const {
return _conds.size();
}
const std::vector<Condition_ptr>& getOperands() const { return _conds; }
const std::vector<Condition_ptr>& operands() const { return _conds; }
CTLType getQueryType() const override { return CTLType::LOPERATOR; }
Path getPath() const override { return Path::pError; }

Expand Down Expand Up @@ -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<uint32_t(uint32_t, uint32_t, bool)> d) const;
Expand All @@ -856,10 +839,6 @@ namespace PetriEngine {

uint32_t distance(DistanceContext& context) const override;
virtual type_id_t type() const { return PQL::type_id<decltype(this)>(); };
private:
std::string op() const override;
std::string opTAPAAL() const override;
std::string sopTAPAAL() const override;
};

/* None equality conditon */
Expand All @@ -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<decltype(this)>(); };
private:
std::string op() const override;
std::string opTAPAAL() const override;
std::string sopTAPAAL() const override;
};

/* Less-than conditon */
Expand All @@ -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<decltype(this)>(); };
private:
std::string op() const override;
std::string opTAPAAL() const override;
std::string sopTAPAAL() const override;
};

/* Less-than-or-equal conditon */
Expand All @@ -896,22 +867,13 @@ namespace PetriEngine {

uint32_t distance(DistanceContext& context) const override;
virtual type_id_t type() const { return PQL::type_id<decltype(this)>(); };
private:
std::string op() const override;
std::string opTAPAAL() const override;
std::string sopTAPAAL() const override;
};

/* Bool condition */
class BooleanCondition : public Condition {
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;
Expand Down
60 changes: 14 additions & 46 deletions include/PetriEngine/PQL/PQL.h
Original file line number Diff line number Diff line change
Expand Up @@ -59,52 +59,29 @@ namespace PetriEngine {
}
}

bool is_true(const Condition& c);
bool is_false(const Condition& c);
template<typename C>
bool is_true(const C* c) { return is_true(*c); }
template<typename C>
bool is_false(const C* c) { return is_false(*c); }
template<typename C>
bool is_true(const std::shared_ptr<C>& c) { return is_true(c.get()); }
template<typename C>
bool is_false(const std::shared_ptr<C>& 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();
Expand All @@ -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;
}
};
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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> Condition_ptr;
using Condition_constptr = std::shared_ptr<const Condition>;
Expand Down
Loading