← Back to branch summary

~tapaal-dist-ctl/verifypn/warning_fix

« back to all changes in this revision

Viewing changes to PetriEngine/PQL/Contexts.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/Contexts.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 CONTEXTS_H
 
20
#define CONTEXTS_H
 
21
 
 
22
#include "../PetriNet.h"
 
23
#include "PQL.h"
 
24
#include "../Structures/DistanceMatrix.h"
 
25
#include "../Structures/StateConstraints.h"
 
26
 
 
27
#include <string>
 
28
#include <vector>
 
29
#include <list>
 
30
 
 
31
namespace PetriEngine {
 
32
namespace PQL{
 
33
 
 
34
/** Context provided for context analysis */
 
35
class AnalysisContext{
 
36
private:
 
37
        std::vector<std::string> _places;
 
38
        std::vector<std::string> _variables;
 
39
        std::vector<ExprError> _errors;
 
40
public:
 
41
        /** A resolution result */
 
42
        struct ResolutionResult {
 
43
                /** Offset in relevant vector */
 
44
                int offset;
 
45
                /** True, if the resolution was successful */
 
46
                bool success;
 
47
                /** True if the identifer was resolved to a place */
 
48
                bool isPlace;
 
49
        };
 
50
        AnalysisContext(const PetriNet& net)
 
51
         : _places(net.placeNames()), _variables(net.variableNames()) {}
 
52
        AnalysisContext(const std::vector<std::string>& places,
 
53
                                        const std::vector<std::string>& variables)
 
54
         : _places(places), _variables(variables) {}
 
55
 
 
56
        /** Resolve an identifier */
 
57
        ResolutionResult resolve(std::string identifier) const{
 
58
                ResolutionResult result;
 
59
                result.offset = -1;
 
60
                result.success = false;
 
61
                for(size_t i = 0; i < _places.size(); i++){
 
62
                        if(_places[i] == identifier){
 
63
                                result.offset = i;
 
64
                                result.isPlace = true;
 
65
                                result.success = true;
 
66
                                return result;
 
67
                        }
 
68
                }
 
69
                for(size_t i = 0; i < _variables.size(); i++){
 
70
                        if(_variables[i] == identifier){
 
71
                                result.offset = i;
 
72
                                result.isPlace = false;
 
73
                                result.success = true;
 
74
                                return result;
 
75
                        }
 
76
                }
 
77
                return result;
 
78
        }
 
79
 
 
80
        /** Report error */
 
81
        void reportError(const ExprError& error){
 
82
                _errors.push_back(error);
 
83
        }
 
84
        /** Get list of errors */
 
85
        const std::vector<ExprError>& errors() const{
 
86
                return _errors;
 
87
        }
 
88
};
 
89
 
 
90
/** Context provided for evalation */
 
91
class EvaluationContext{
 
92
public:
 
93
        /** Create evaluation context, this doesn't take ownershop */
 
94
        EvaluationContext(const MarkVal* marking, const VarVal* assignment){
 
95
                _marking = marking;
 
96
                _assignment = assignment;
 
97
        }
 
98
        const MarkVal* marking() const {return _marking;}
 
99
        const VarVal* assignment() const {return _assignment;}
 
100
private:
 
101
        const MarkVal* _marking;
 
102
        const VarVal* _assignment;
 
103
};
 
104
 
 
105
/** Context for distance computation */
 
106
class DistanceContext : public EvaluationContext{
 
107
public:
 
108
        /** Strategy flags for distance computation */
 
109
        enum DistanceStrategy{
 
110
                AndExtreme      = 1<<0,
 
111
                AndAverage      = 1<<1,
 
112
                AndSum          = 1<<2,
 
113
                OrExtreme       = 1<<3,
 
114
                OrAverage       = 1<<4,
 
115
                ArcCount        = 1<<5,
 
116
                TokenCost       = 1<<6
 
117
        };
 
118
 
 
119
        DistanceContext(const PetriNet& net,
 
120
                                        DistanceStrategy strategy,
 
121
                                        const MarkVal* marking,
 
122
                                        const VarVal* valuation,
 
123
                                        Structures::DistanceMatrix* dm)
 
124
                : EvaluationContext(marking, valuation), _net(net) {
 
125
                _strategy = strategy;
 
126
                _negated = false;
 
127
                _dm = dm;
 
128
        }
 
129
        DistanceStrategy strategy() const { return _strategy; }
 
130
        const PetriNet& net() const { return _net; }
 
131
        void negate() { _negated = !_negated; }
 
132
        bool negated() const { return _negated; }
 
133
        const Structures::DistanceMatrix* distanceMatrix() const { return _dm; }
 
134
private:
 
135
        const PetriNet& _net;
 
136
        DistanceStrategy _strategy;
 
137
        bool _negated;
 
138
        Structures::DistanceMatrix* _dm;
 
139
};
 
140
 
 
141
/** Constraint Analysis Context used for over-approximation */
 
142
class ConstraintAnalysisContext{
 
143
public:
 
144
        typedef std::vector<Structures::StateConstraints*> ConstraintSet;
 
145
 
 
146
        ConstraintAnalysisContext(const PetriNet& net) : _net(net) {
 
147
                canAnalyze = true;
 
148
                negated = false;
 
149
        }
 
150
        const PetriNet& net() const { return _net; }
 
151
        bool canAnalyze;
 
152
        bool negated;
 
153
        ConstraintSet retval;
 
154
private:
 
155
        const PetriNet& _net;
 
156
};
 
157
 
 
158
/** Context for condition to TAPAAL export */
 
159
class TAPAALConditionExportContext{
 
160
public:
 
161
        bool failed;
 
162
        std::string netName;
 
163
};
 
164
 
 
165
/** Just-In-Time compilation context */
 
166
class CodeGenerationContext{
 
167
public:
 
168
        CodeGenerationContext(llvm::Value* marking,
 
169
                                                  llvm::Value* valuation,
 
170
                                                  llvm::BasicBlock* label,
 
171
                                                  llvm::LLVMContext& context)
 
172
                : _context(context) {
 
173
                _marking = marking;
 
174
                _valuation = valuation;
 
175
                _label = label;
 
176
        }
 
177
        /** Marking */
 
178
        llvm::Value* marking() { return _marking; }
 
179
        /** Variable valuation */
 
180
        llvm::Value* valuation() { return _valuation; }
 
181
        /** Label for the current code block */
 
182
        llvm::BasicBlock* label() { return _label; }
 
183
        /** LLVM Context that is currently generating */
 
184
        llvm::LLVMContext& context() { return _context; }
 
185
private:
 
186
        llvm::Value* _marking;
 
187
        llvm::Value* _valuation;
 
188
        llvm::BasicBlock* _label;
 
189
        llvm::LLVMContext& _context;
 
190
};
 
191
 
 
192
} // PQL
 
193
} // PetriEngine
 
194
 
 
195
#endif // CONTEXTS_H