← Back to branch summary

~verifypn-cpn/verifypn/colored

« back to all changes in this revision

Viewing changes to PetriEngine/PQL/PQL.h

  • Committer: Jonas Finnemann Jensen
  • Date: 2011-09-15 13:30:00 UTC
  • Revision ID: jopsen@gmail.com-20110915133000-wnywm1odf82emiuw
Import of sources from github

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriEngine/PQL/PQL.h
 
1
/* PeTe - Petri Engine exTremE
 
2
 * Copyright (C) 2011  Jonas Finnemann Jensen <jopsen@gmail.com>,
 
3
 *                     Thomas Søndersø Nielsen <primogens@gmail.com>,
 
4
 *                     Lars Kærlund Østergaard <larsko@gmail.com>,
 
5
 * 
 
6
 * This program is free software: you can redistribute it and/or modify
 
7
 * it under the terms of the GNU General Public License as published by
 
8
 * the Free Software Foundation, either version 3 of the License, or
 
9
 * (at your option) any later version.
 
10
 * 
 
11
 * This program is distributed in the hope that it will be useful,
 
12
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 
13
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
14
 * GNU General Public License for more details.
 
15
 * 
 
16
 * You should have received a copy of the GNU General Public License
 
17
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
18
 */
 
19
#ifndef PQL_H
 
20
#define PQL_H
 
21
#include "../PetriNet.h"
 
22
#include "../Structures/State.h"
 
23
#include <string>
 
24
#include <list>
 
25
#include <vector>
 
26
 
 
27
namespace llvm{
 
28
        class Value;
 
29
        class BasicBlock;
 
30
        class LLVMContext;
 
31
}
 
32
 
 
33
namespace PetriEngine{
 
34
namespace PQL{
 
35
 
 
36
class AnalysisContext;
 
37
class EvaluationContext;
 
38
class DistanceContext;
 
39
class ConstraintAnalysisContext;
 
40
class CodeGenerationContext;
 
41
class TAPAALConditionExportContext;
 
42
 
 
43
/** Representation of a PQL error */
 
44
class ExprError{
 
45
        std::string _text;
 
46
        int _offset;
 
47
        int _length;
 
48
public:
 
49
        ExprError(std::string text = "", int offset = -1, int length = 0){
 
50
                _text = text;
 
51
                _offset = offset;
 
52
                _length = length;
 
53
        }
 
54
        /** Human readable explaination of the error */
 
55
        const std::string& text() const {return _text;}
 
56
        /** Offset in the source, -1 if undefined */
 
57
        int offset() const {return _offset;}
 
58
        /** length in the source, 0 if not applicable */
 
59
        int length() const {return _length;}
 
60
 
 
61
        /** Convert error to string */
 
62
        std::string toString() const {
 
63
                return "Parsing error \"" + text() + "\"";
 
64
        }
 
65
        /** True, if this is a default created ExprError without any information */
 
66
        bool isEmpty() const {
 
67
                return _text.empty() && _offset == -1 && _length == 0;
 
68
        }
 
69
};
 
70
 
 
71
 
 
72
 
 
73
/** Representation of an expression */
 
74
class Expr{
 
75
public:
 
76
        /** Types of expressions */
 
77
        enum Types{
 
78
                /** Binary addition expression */
 
79
                PlusExpr,
 
80
                /** Binary subtraction expression */
 
81
                SubtractExpr,
 
82
                /** Binary multiplication expression */
 
83
                MultiplyExpr,
 
84
                /** Unary minus expression */
 
85
                MinusExpr,
 
86
                /** Literal integer expression */
 
87
                LiteralExpr,
 
88
                /** Identifier expression */
 
89
                IdentifierExpr
 
90
        };
 
91
public:
 
92
        /** Virtual destructor, an expression should know it subexpressions */
 
93
        virtual ~Expr();
 
94
        /** Perform context analysis */
 
95
        virtual void analyze(AnalysisContext& context) = 0;
 
96
        /** True, if the expression is p-free */
 
97
        virtual bool pfree() const = 0;
 
98
        /** Evaluate the expression given marking and assignment */
 
99
        virtual int evaluate(const EvaluationContext& context) const = 0;
 
100
        /** Generate LLVM intermediate code for this expr  */
 
101
        //virtual llvm::Value* codegen(CodeGenerationContext& context) const = 0;
 
102
        /** Convert expression to string */
 
103
        virtual std::string toString() const = 0;
 
104
        /** Expression type */
 
105
        virtual Types type() const = 0;
 
106
        /** Scale all nested literals by factor */
 
107
        virtual void scale(int factor) = 0;
 
108
};
 
109
 
 
110
/** Base condition */
 
111
class Condition{
 
112
public:
 
113
        /** Virtual destructor */
 
114
        virtual ~Condition();
 
115
        /** Evaluate condition */
 
116
        bool evaluate(Structures::State& state) const;
 
117
        /** Perform context analysis  */
 
118
        virtual void analyze(AnalysisContext& context) = 0;
 
119
        /** Evaluate condition */
 
120
        virtual bool evaluate(const EvaluationContext& context) const = 0;
 
121
        /** Analyze constraints for over-approximation */
 
122
        virtual void findConstraints(ConstraintAnalysisContext& context) const = 0;
 
123
        /** Generate LLVM intermediate code for this condition  */
 
124
        //virtual llvm::Value* codegen(CodeGenerationContext& context) const = 0;
 
125
        /** Convert condition to string */
 
126
        virtual std::string toString() const = 0;
 
127
        /** Export condition to TAPAAL query (add EF manually!) */
 
128
        virtual std::string toTAPAALQuery(TAPAALConditionExportContext& context) const = 0;
 
129
        /** Get distance to query */
 
130
        virtual double distance(DistanceContext& context) const = 0;
 
131
        /** Scale all nested literals by factor */
 
132
        virtual void scale(int factor) = 0;
 
133
};
 
134
 
 
135
/** Assignment expression */
 
136
class AssignmentExpression{
 
137
private:
 
138
        struct VariableAssignment{
 
139
                std::string identifier;
 
140
                int offset;
 
141
                Expr* expr;
 
142
        };
 
143
        typedef std::list<VariableAssignment>::iterator iter;
 
144
        typedef std::list<VariableAssignment>::const_iterator const_iter;
 
145
public:
 
146
        void prepend(const std::string& identifier, Expr* expr){
 
147
                VariableAssignment va;
 
148
                va.offset = -1;
 
149
                va.identifier = identifier;
 
150
                va.expr = expr;
 
151
                assignments.push_front(va);
 
152
        }
 
153
        void analyze(AnalysisContext& context);
 
154
        /** Evaluate the assignment expression */
 
155
        void evaluate(const MarkVal* m,
 
156
                                  const VarVal* a,
 
157
                                  VarVal* result_a,
 
158
                                  VarVal* ranges,
 
159
                                  size_t nvars) const;
 
160
        std::string toString(){
 
161
                std::string t;
 
162
                for(iter it = assignments.begin(); it != assignments.end(); it++){
 
163
                        t = t + it->identifier + " := " + it->expr->toString() + "; ";
 
164
                }
 
165
                return t;
 
166
        }
 
167
private:
 
168
        std::list<VariableAssignment> assignments;
 
169
};
 
170
 
 
171
} // PQL
 
172
} // PetriEngine
 
173
 
 
174
#endif // PQL_H