← Back to branch summary

~tapaal-ltl/verifypn/rule-D-fix

« back to all changes in this revision

Viewing changes to PetriEngine/ValidationBuilder.cpp

  • 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/ValidationBuilder.cpp
 
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
#include "ValidationBuilder.h"
 
20
 
 
21
#include "PQL/PQLParser.h"
 
22
#include "PQL/Contexts.h"
 
23
 
 
24
#include <assert.h>
 
25
#include <sstream>
 
26
#include <set>
 
27
 
 
28
using namespace std;
 
29
 
 
30
namespace PetriEngine{
 
31
 
 
32
 
 
33
/** Auxiliary function for converting into to string */
 
34
inline string int2string(int i){
 
35
        stringstream ss;
 
36
        ss<<i;
 
37
        return ss.str();
 
38
}
 
39
 
 
40
ValidationBuilder::ValidationBuilder() : AbstractPetriNetBuilder() {}
 
41
 
 
42
void ValidationBuilder::addVariable(const std::string& name,
 
43
                                                                        int initialValue,
 
44
                                                                        int range){
 
45
        _varNames.push_back(name);
 
46
        if(initialValue > range){       //TODO: Figure out if this is > or >=
 
47
                string msg = "Initial value " + int2string(initialValue)
 
48
                                         + " is larger than range " + int2string(range);
 
49
                _errors.push_back(ValidationError(name, msg));
 
50
        }
 
51
}
 
52
 
 
53
void ValidationBuilder::addPlace(const std::string& name,
 
54
                                                                 int tokens,
 
55
                                                                 double,
 
56
                                                                 double){
 
57
        _placeNames.push_back(name);
 
58
        if(tokens < 0){
 
59
                string msg = "Initial marking " + int2string(tokens)
 
60
                                         + " is less than zero";
 
61
                _errors.push_back(ValidationError(name, msg));
 
62
        }
 
63
}
 
64
 
 
65
void ValidationBuilder::addTransition(const std::string& name,
 
66
                                                                          const std::string& conditions,
 
67
                                                                          const std::string& assignments,
 
68
                                                                          double,
 
69
                                                                          double){
 
70
        _transitionNames.push_back(name);
 
71
        _conditions.push_back(conditions);
 
72
        _assignments.push_back(assignments);
 
73
}
 
74
 
 
75
void ValidationBuilder::addInputArc(const std::string& place,
 
76
                                                                        const std::string& transition,
 
77
                                                                        int weight){
 
78
        _inputArcs.push_back(Arc(place, transition));
 
79
        if(weight < 0){
 
80
                string msg = "Weight is " + int2string(weight)
 
81
                                         + " is less than zero";
 
82
                _errors.push_back(ValidationError(place, transition, msg));
 
83
        }
 
84
}
 
85
 
 
86
void ValidationBuilder::addOutputArc(const std::string& transition,
 
87
                                                                         const std::string& place,
 
88
                                                                         int weight){
 
89
        _outputArcs.push_back(Arc(transition, place));
 
90
        if(weight < 0){
 
91
                string msg = "Weight is " + int2string(weight)
 
92
                                         + " is less than zero";
 
93
                _errors.push_back(ValidationError(transition, place, msg));
 
94
        }
 
95
}
 
96
 
 
97
/** Get the number of matching identifiers */
 
98
int ValidationBuilder::countMatchingIds(const std::string& id){
 
99
        int count = 0;
 
100
        for(size_t i = 0; i < _varNames.size(); i++)
 
101
                if(_varNames[i] == id) count++;
 
102
        for(size_t i = 0; i < _placeNames.size(); i++)
 
103
                if(_placeNames[i] == id) count++;
 
104
        for(size_t i = 0; i < _transitionNames.size(); i++)
 
105
                if(_transitionNames[i] == id) count++;
 
106
        return count;
 
107
}
 
108
 
 
109
bool ValidationBuilder::validate(){
 
110
        //Check for duplicate identifiers
 
111
        set<string> reportedDuplicates; //Use a set to avoid reporting them more than once
 
112
        //Check variable names
 
113
        for(size_t i = 0; i < _varNames.size(); i++){
 
114
                const string& id = _varNames[i];
 
115
                int count = countMatchingIds(id);
 
116
                assert(count >= 1);
 
117
                if(count > 1 && reportedDuplicates.count(id) == 0){
 
118
                        reportedDuplicates.insert(id);
 
119
                        _errors.push_back(ValidationError(id,
 
120
                                                                                          "The identifiers must be unique, \""
 
121
                                                                                          + id + "\" is shared by "
 
122
                                                                                          + int2string(count) + " entities"));
 
123
                }
 
124
        }
 
125
        //Check place names
 
126
        for(size_t i = 0; i < _placeNames.size(); i++){
 
127
                const string& id = _placeNames[i];
 
128
                int count = countMatchingIds(id);
 
129
                assert(count >= 1);
 
130
                if(count > 1 && reportedDuplicates.count(id) == 0){
 
131
                        reportedDuplicates.insert(id);
 
132
                        _errors.push_back(ValidationError(id,
 
133
                                                                                          "The identifiers must be unique, \""
 
134
                                                                                          + id + "\" is shared by "
 
135
                                                                                          + int2string(count) + " entities"));
 
136
                }
 
137
        }
 
138
        //Check transition names
 
139
        for(size_t i = 0; i < _transitionNames.size(); i++){
 
140
                const string& id = _transitionNames[i];
 
141
                int count = countMatchingIds(id);
 
142
                assert(count >= 1);
 
143
                if(count > 1 && reportedDuplicates.count(id) == 0){
 
144
                        reportedDuplicates.insert(id);
 
145
                        _errors.push_back(ValidationError(id,
 
146
                                                                                          "The identifiers must be unique, \""
 
147
                                                                                          + id + "\" is shared by "
 
148
                                                                                          + int2string(count) + " entities"));
 
149
                }
 
150
        }
 
151
 
 
152
        //Check all input arcs
 
153
        for(size_t i = 0; i < _inputArcs.size(); i++){
 
154
                const Arc& arc = _inputArcs[i];
 
155
                bool foundPlace = false;
 
156
                bool foundTransition = false;
 
157
                //Look for place
 
158
                for(size_t j = 0; j < _placeNames.size(); j++){
 
159
                        foundPlace |= _placeNames[j] == arc.start;
 
160
                        if(foundPlace) break;
 
161
                }
 
162
                //Look for transition
 
163
                for(size_t j = 0; j < _transitionNames.size(); j++){
 
164
                        foundTransition |= _transitionNames[j] == arc.end;
 
165
                        if(foundTransition) break;
 
166
                }
 
167
                //Report error
 
168
                if(!foundPlace || !foundTransition){
 
169
                        string msg;
 
170
                        if(!foundPlace && !foundTransition)
 
171
                                msg = "Neigther end-points found";
 
172
                        else if(!foundPlace)
 
173
                                msg = "Start-place \"" + arc.start + "\" not found";
 
174
                        else
 
175
                                msg = "End-transition \"" + arc.end + "\" not found";
 
176
                        _errors.push_back(ValidationError(arc.start,
 
177
                                                                                          arc.end,
 
178
                                                                                          msg));
 
179
                }
 
180
        }
 
181
        //Check all output arcs
 
182
        for(size_t i = 0; i < _outputArcs.size(); i++){
 
183
                const Arc& arc = _outputArcs[i];
 
184
                bool foundPlace = false;
 
185
                bool foundTransition = false;
 
186
                //Look for transition
 
187
                for(size_t j = 0; j < _transitionNames.size(); j++){
 
188
                        foundTransition |= _transitionNames[j] == arc.start;
 
189
                        if(foundTransition) break;
 
190
                }
 
191
                //Look for place
 
192
                for(size_t j = 0; j < _placeNames.size(); j++){
 
193
                        foundPlace |= _placeNames[j] == arc.end;
 
194
                        if(foundPlace) break;
 
195
                }
 
196
                //Report error
 
197
                if(!foundPlace || !foundTransition){
 
198
                        string msg;
 
199
                        if(!foundPlace && !foundTransition)
 
200
                                msg = "Neither end-points found";
 
201
                        else if(!foundPlace)
 
202
                                msg = "End-place \"" + arc.end + "\" not found";
 
203
                        else
 
204
                                msg = "Start-transition \"" + arc.start + "\" not found";
 
205
                        _errors.push_back(ValidationError(arc.start,
 
206
                                                                                          arc.end,
 
207
                                                                                          msg));
 
208
                }
 
209
        }
 
210
 
 
211
        //Attempt to parse all non-empty conditions
 
212
        for(size_t i = 0; i < _conditions.size(); i++){
 
213
                if(_conditions[i].empty()) continue;
 
214
                PQL::Condition* cond = PQL::ParseQuery(_conditions[i]);
 
215
                if(cond){
 
216
                        PQL::AnalysisContext context(_placeNames, _varNames);
 
217
                        cond->analyze(context);
 
218
                        for(size_t j = 0; j < context.errors().size(); j++){
 
219
                                _errors.push_back(ValidationError(_transitionNames[i],
 
220
                                                                                                  context.errors()[j],
 
221
                                                                                                  true));
 
222
                        }
 
223
                        delete cond;
 
224
                        cond = NULL;
 
225
                }else
 
226
                        _errors.push_back(ValidationError(_transitionNames[i],
 
227
                                                                                          "Unable to parse non-empty condition"));
 
228
        }
 
229
        //Attempt to parse all non-empty assignments
 
230
        for(size_t i = 0; i < _assignments.size(); i++){
 
231
                if(_assignments[i].empty()) continue;
 
232
                PQL::AssignmentExpression* a = PQL::ParseAssignment(_assignments[i]);
 
233
                if(a){
 
234
                        PQL::AnalysisContext context(_placeNames, _varNames);
 
235
                        a->analyze(context);
 
236
                        for(size_t j = 0; j < context.errors().size(); j++){
 
237
                                _errors.push_back(ValidationError(_transitionNames[i],
 
238
                                                                                                  context.errors()[j],
 
239
                                                                                                  false));
 
240
                        }
 
241
                        delete a;
 
242
                        a = NULL;
 
243
                }else
 
244
                        _errors.push_back(ValidationError(_transitionNames[i],
 
245
                                                                                          "Unable to parse non-empty assignment"));
 
246
        }
 
247
 
 
248
        return _errors.empty();
 
249
}
 
250
 
 
251
 
 
252
 
 
253
} // PetriEngine