~tapaal-ltl/verifypn/fireable-empty-preset-fix
» Revision
243
: src/PetriEngine/Colored/PartitionBuilder.cpp
« back to all changes in this revision
Viewing changes to src/PetriEngine/Colored/PartitionBuilder.cpp
- browse files at revision 243
- compare with another revision
- download diff
- download tarball
- view history from revision 243
- Committer: srba.jiri at gmail
- Date: 2021-07-07 12:02:50 UTC
- mfrom: (233.1.63 update-parser)
- Revision ID: srba.jiri@gmail.com-20210707120250-f86fv0m9ycbge3qs
merged in lp:~tapaal-contributor/verifypn/update-parser improving CPN unfodling and refactoring the code, fixing parser
- files added:
- include/PetriEngine/Colored/EquivalenceVec.h
- files modified:
- include/PetriEngine/AbstractPetriNetBuilder.h
added
removed
src/PetriEngine/Colored/PartitionBuilder.cpp
7
7
namespace PetriEngine {
8
8
namespace Colored {
9
9
10
PartitionBuilder::PartitionBuilder(std::vector<Transition> *transitions, std::vector<Place> *places, std::unordered_map<uint32_t,std::vector<uint32_t>> *placePostTransitionMap, std::unordered_map<uint32_t,std::vector<uint32_t>> *placePreTransitionMap)
11
: _transitions(transitions), _places(places), _placePostTransitionMap(placePostTransitionMap), _placePreTransitionMap(placePreTransitionMap) {
12
13
//Instantiate partitions
14
for(uint32_t i = 0; i < _places->size(); i++){
15
auto place = _places->operator[](i);
16
interval_t fullInterval = place.type->getFullInterval();
17
EquivalenceClass fullClass = EquivalenceClass(place.type);
18
fullClass._colorIntervals.addInterval(fullInterval);
19
_partition[i]._equivalenceClasses.push_back(fullClass);
20
_placeQueue.push_back(i);
21
_inQueue[i] = true;
22
}
23
}
24
25
PartitionBuilder::PartitionBuilder(std::vector<Transition> *transitions, std::vector<Place> *places, std::unordered_map<uint32_t,std::vector<uint32_t>> *placePostTransitionMap, std::unordered_map<uint32_t,std::vector<uint32_t>> *placePreTransitionMap, std::vector<Colored::ColorFixpoint> *placeColorFixpoints)
26
: _transitions(transitions), _places(places), _placePostTransitionMap(placePostTransitionMap), _placePreTransitionMap(placePreTransitionMap) {
27
28
//Instantiate partitions
29
for(uint32_t i = 0; i < _places->size(); i++){
30
auto place = _places->operator[](i);
31
EquivalenceClass fullClass = EquivalenceClass(place.type);
32
fullClass._colorIntervals = placeColorFixpoints->operator[](i).constraints;
33
_partition[i]._equivalenceClasses.push_back(fullClass);
34
_placeQueue.push_back(i);
35
_inQueue[i] = true;
36
}
37
}
38
39
void PartitionBuilder::printPartion() {
40
for(auto equivalenceVec : _partition){
41
std::cout << "Partition for place " << _places->operator[](equivalenceVec.first).name << std::endl;
42
for (auto equivalenceClass : equivalenceVec.second._equivalenceClasses){
10
PartitionBuilder::PartitionBuilder(const std::vector<Transition> &transitions, const std::vector<Place> &places, const std::unordered_map<uint32_t,std::vector<uint32_t>> &placePostTransitionMap, const std::unordered_map<uint32_t,std::vector<uint32_t>> &placePreTransitionMap)
11
: PartitionBuilder(transitions, places, placePostTransitionMap, placePreTransitionMap, nullptr){
12
}
13
14
PartitionBuilder::PartitionBuilder(const std::vector<Transition> &transitions, const std::vector<Place> &places, const std::unordered_map<uint32_t,std::vector<uint32_t>> &placePostTransitionMap, const std::unordered_map<uint32_t,std::vector<uint32_t>> &placePreTransitionMap, const std::vector<Colored::ColorFixpoint> *placeColorFixpoints)
15
: _transitions(transitions), _places(places), _placePostTransitionMap(placePostTransitionMap), _placePreTransitionMap(placePreTransitionMap) {
16
17
//Instantiate partitions
18
for(uint32_t i = 0; i < _places.size(); i++){
19
const PetriEngine::Colored::Place& place = _places[i];
20
EquivalenceClass fullClass = EquivalenceClass(++_eq_id_counter, place.type);
21
if(placeColorFixpoints != nullptr){
22
fullClass.setIntervalVector(placeColorFixpoints->operator[](i).constraints);
23
} else {
24
fullClass.addInterval(place.type->getFullInterval());
25
}
26
_partition[i].push_back_Eqclass(fullClass);
27
for(uint32_t j = 0; j < place.type->productSize(); j++){
28
_partition[i].push_back_diagonalTuplePos(false);
29
}
30
_placeQueue.push_back(i);
31
_inQueue[i] = true;
32
}
33
}
34
35
void PartitionBuilder::printPartion() const {
36
for(const auto &equivalenceVec : _partition){
37
std::cout << "Partition for place " << _places[equivalenceVec.first].name << std::endl;
38
std::cout << "Diag variables: (";
39
for(auto daigPos : equivalenceVec.second.getDiagonalTuplePositions()){
40
std::cout << daigPos << ",";
41
}
42
std::cout << ")" << std::endl;
43
for (const auto &equivalenceClass : equivalenceVec.second.getEquivalenceClasses()){
43
44
std::cout << equivalenceClass.toString() << std::endl;
44
45
45
46
}
46
std::cout << "Diagonal " << equivalenceVec.second.diagonal << std::endl << std::endl;;
47
std::cout << "Diagonal " << equivalenceVec.second.isDiagonal() << std::endl << std::endl;;
47
48
}
48
49
}
49
50
50
void PartitionBuilder::partitionNet(){
51
bool PartitionBuilder::partitionNet(int32_t timeout) {
52
const auto start = std::chrono::high_resolution_clock::now();
51
53
handleLeafTransitions();
54
auto end = std::chrono::high_resolution_clock::now();
52
55
53
while(!_placeQueue.empty()){
56
while(!_placeQueue.empty() && timeout > 0 && std::chrono::duration_cast<std::chrono::seconds>(end - start).count() < timeout){
54
57
auto placeId = _placeQueue.back();
55
58
_placeQueue.pop_back();
56
59
_inQueue[placeId] = false;
57
60
58
auto place = _places->operator[](placeId);
61
bool allPositionsDiagonal = true;
62
for(auto diag : _partition[placeId].getDiagonalTuplePositions()){
63
if(!diag){
64
allPositionsDiagonal = false;
65
break;
66
}
67
}
59
68
60
for(uint32_t transitionId : _placePreTransitionMap->operator[](placeId)){
61
//std::cout << "For transition " << _transitions->operator[](transitionId).name << " and place " << _places->operator[](placeId).name << std::endl;
62
//printPartion();
63
64
handleTransition(transitionId, placeId);
65
66
//std::cout << "---------------------------------------------------" << std::endl;
67
}
68
}
69
if(allPositionsDiagonal || _partition[placeId].getEquivalenceClasses().size() >=
70
_partition[placeId].getEquivalenceClasses().back().type()->size(_partition[placeId].getDiagonalTuplePositions())){
71
_partition[placeId].setDiagonal(true);
72
}
73
if(_placePreTransitionMap.find(placeId) != _placePreTransitionMap.end()){
74
for(uint32_t transitionId : _placePreTransitionMap.find(placeId)->second){
75
handleTransition(transitionId, placeId);
76
}
77
}
78
end = std::chrono::high_resolution_clock::now();
79
}
80
return _placeQueue.empty();
69
81
}
70
82
71
void PartitionBuilder::assignColorMap(std::unordered_map<uint32_t, EquivalenceVec> &partition){
83
void PartitionBuilder::assignColorMap(std::unordered_map<uint32_t, EquivalenceVec> &partition) const{
72
84
for(auto& eqVec : partition){
73
if(eqVec.second.diagonal){
85
if(eqVec.second.isDiagonal()){
74
86
continue;
75
87
}
76
ColorType *colorType = _places->operator[](eqVec.first).type;
88
const ColorType *colorType = _places[eqVec.first].type;
77
89
for(uint32_t i = 0; i < colorType->size(); i++){
78
const Color *color = &colorType->operator[](i);
79
for(auto& eqClass : eqVec.second._equivalenceClasses){
80
std::vector<uint32_t> colorIds;
81
color->getTupleId(&colorIds);
82
if(eqClass.containsColor(colorIds)){
83
eqVec.second.colorEQClassMap[color] = &eqClass;
84
}
85
}
90
const Color *color = &(*colorType)[i];
91
eqVec.second.addColorToEqClassMap(color);
86
92
}
87
93
}
88
94
}
89
95
90
96
void PartitionBuilder::handleTransition(uint32_t transitionId, uint32_t postPlaceId){
91
auto transition = _transitions->operator[](transitionId);
97
const PetriEngine::Colored::Transition &transition = _transitions[transitionId];
92
98
Arc postArc;
93
99
bool arcFound = false;
94
for(auto& outArc : transition.output_arcs){
100
for(const auto& outArc : transition.output_arcs){
95
101
if(outArc.place == postPlaceId){
96
102
postArc = outArc;
97
103
arcFound = true;
103
109
return;
104
110
}
105
111
106
handleTransition(&transition, postPlaceId, &postArc);
112
handleTransition(transition, postPlaceId, &postArc);
107
113
}
108
114
109
void PartitionBuilder::handleTransition(Transition *transition, uint32_t postPlaceId, Arc *postArc) {
110
std::unordered_map<const PetriEngine::Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMap;
111
std::unordered_map<uint32_t, const PetriEngine::Colored::Variable *> varPositionMap;
112
std::set<const PetriEngine::Colored::Variable *> postArcVars;
113
std::set<const PetriEngine::Colored::Variable *>guardVars;
114
std::set<const Colored::Variable*> diagonalVars;
115
116
postArc->expr->getVariables(postArcVars, varPositionMap, varModifierMap);
117
118
for(auto varModMap : varModifierMap){
115
//Check if a variable appears more than once on the output arc
116
//If the place is does not have a product colortype mark the whole place as diagonal, otherwise only the positions
117
void PartitionBuilder::checkVarOnArc(const VariableModifierMap &varModifierMap, std::set<const Colored::Variable*> &diagonalVars, uint32_t placeId, bool inputArc){
118
for(const auto &varModMap : varModifierMap){
119
119
if(varModMap.second.size() > 1){
120
120
uint32_t actualSize = 0;
121
for(auto map : varModMap.second){
121
std::vector<uint32_t> positions;
122
for(const auto &map : varModMap.second){
122
123
if(!map.empty()){
124
for(auto position : map){
125
positions.push_back(position.first);
126
}
123
127
actualSize++;
124
128
}
125
129
}
126
130
if(actualSize > 1) {
127
_partition[postPlaceId].diagonal = true;
131
diagonalVars.insert(varModMap.first);
132
if(_partition[placeId].getEquivalenceClasses().back().type()->productSize() == 1){
133
_partition[placeId].setDiagonal(true);
134
} else {
135
for(auto pos : positions){
136
if(!_partition[placeId].getDiagonalTuplePositions()[pos]){
137
if(inputArc) addToQueue(placeId);
138
_partition[placeId].setDiagonalTuplePosition(pos,true);
139
}
140
}
141
}
128
142
}
129
143
}
130
144
}
131
132
if(transition->guard != nullptr){
133
transition->guard->getVariables(guardVars);
134
}
135
136
auto placePartition = _partition[postPlaceId]._equivalenceClasses;
137
138
for(auto eqClass : placePartition){
139
auto varMaps = prepareVariables(varModifierMap, &eqClass, postArc, postPlaceId);
140
145
}
146
//Check if the variales on this preArc also appear on other preArcs for the transition
147
//and mark them as diagonal if they do
148
void PartitionBuilder::checkVarOnInputArcs(const std::unordered_map<uint32_t,PositionVariableMap> &placeVariableMap, const PositionVariableMap &preVarPositionMap, std::set<const Colored::Variable*> &diagonalVars, uint32_t placeId){
149
for(const auto &placeVariables : placeVariableMap){
150
for(const auto &variable : preVarPositionMap){
151
for(const auto &varPosition : placeVariables.second){
152
if(varPosition.second == variable.second){
153
diagonalVars.insert(variable.second);
154
if(_partition[placeId].getEquivalenceClasses().back().type()->productSize() == 1){
155
_partition[placeId].setDiagonal(true);
156
} else if(!_partition[placeId].getDiagonalTuplePositions()[variable.first]) {
157
addToQueue(placeId);
158
_partition[placeId].setDiagonalTuplePosition(variable.first, true);
159
}
160
161
if(_partition[placeVariables.first].getEquivalenceClasses().back().type()->productSize() == 1){
162
_partition[placeVariables.first].setDiagonal(true);
163
addToQueue(placeVariables.first);
164
} else if(!_partition[placeVariables.first].getDiagonalTuplePositions()[varPosition.first]) {
165
addToQueue(placeVariables.first);
166
_partition[placeVariables.first].setDiagonalTuplePosition(varPosition.first, true);
167
}
168
break;
169
}
170
}
171
if(_partition[placeId].isDiagonal()){
172
break;
173
}
174
}
175
if(_partition[placeId].isDiagonal()){
176
break;
177
}
178
}
179
}
180
//Check if the preArc share variables with the postArc and mark diagonal if the
181
//variable positions are diagonal in the post place
182
void PartitionBuilder::markSharedVars(const PositionVariableMap &preVarPositionMap, const PositionVariableMap &varPositionMap, uint32_t postPlaceId, uint32_t prePlaceId){
183
for(const auto &preVar : preVarPositionMap){
184
for(const auto &postVar : varPositionMap){
185
if(preVar.second == postVar.second){
186
if(_partition[postPlaceId].isDiagonal() || _partition[postPlaceId].getDiagonalTuplePositions()[postVar.first]){
187
if(_partition[prePlaceId].getEquivalenceClasses().back().type()->productSize() == 1){
188
_partition[prePlaceId].setDiagonal(true);
189
} else if(!_partition[prePlaceId].getDiagonalTuplePositions()[preVar.first]) {
190
addToQueue(prePlaceId);
191
_partition[prePlaceId].setDiagonalTuplePosition(preVar.first, true);
192
}
193
}
194
}
195
}
196
}
197
}
198
//Check if any of the variables on the preArc was part of a diagonal constraint in the gaurd
199
void PartitionBuilder::checkVarInGuard(const PositionVariableMap &preVarPositionMap, const std::set<const Colored::Variable*> &diagonalVars, uint32_t placeId){
200
for(const auto &preVar : preVarPositionMap){
201
if(diagonalVars.count(preVar.second)){
202
if(_partition[placeId].getEquivalenceClasses().back().type()->productSize() == 1){
203
_partition[placeId].setDiagonal(true);
204
break;
205
} else if(!_partition[placeId].getDiagonalTuplePositions()[preVar.first]) {
206
addToQueue(placeId);
207
_partition[placeId].setDiagonalTuplePosition(preVar.first, true);
208
}
209
}
210
}
211
}
212
213
//Check if we have marked all positions in the product type of the place as diagonal
214
//and mark the whole place as diagonal if it is the case
215
bool PartitionBuilder::checkTupleDiagonal(uint32_t placeId){
216
bool allPositionsDiagonal = true;
217
for(auto diag : _partition[placeId].getDiagonalTuplePositions()){
218
if(!diag){
219
allPositionsDiagonal = false;
220
break;
221
}
222
}
223
224
if(allPositionsDiagonal){
225
_partition[placeId].setDiagonal(true);
226
addToQueue(placeId);
227
return true;
228
}
229
return false;
230
}
231
232
bool PartitionBuilder::checkDiagonal(uint32_t placeId){
233
if(_partition[placeId].isDiagonal()){
234
addToQueue(placeId);
235
return true;
236
}
237
return false;
238
}
239
240
void PartitionBuilder::applyNewIntervals(const Arc &inArc, const std::vector<PetriEngine::Colored::VariableIntervalMap> &varMaps){
241
//Retrieve the intervals for the current place,
242
//based on the intervals from the postPlace, the postArc, preArc and guard
243
auto outIntervals = inArc.expr->getOutputIntervals(varMaps);
244
EquivalenceVec newEqVec;
245
for(auto& intervalTuple : outIntervals){
246
intervalTuple.simplify();
247
EquivalenceClass newEqClass(++_eq_id_counter, _partition[inArc.place].getEquivalenceClasses().back().type(), std::move(intervalTuple));
248
newEqVec.push_back_Eqclass(std::move(newEqClass));
249
}
250
newEqVec.setDiagonalTuplePositions(_partition[inArc.place].getDiagonalTuplePositions());
251
252
//If the prePlace has not been marked as diagonal, then split the current partitions based on the new intervals
253
if(splitPartition(std::move(newEqVec), inArc.place)){
254
addToQueue(inArc.place);
255
}
256
_partition[inArc.place].mergeEqClasses();
257
}
258
259
void PartitionBuilder::handleTransition(const Transition &transition, const uint32_t postPlaceId, const Arc *postArc) {
260
VariableModifierMap varModifierMap;
261
PositionVariableMap varPositionMap;
262
std::set<const PetriEngine::Colored::Variable *> postArcVars;
263
std::set<const PetriEngine::Colored::Variable *> guardVars;
264
std::set<const Colored::Variable*> diagonalVars;
265
266
postArc->expr->getVariables(postArcVars, varPositionMap, varModifierMap, true);
267
268
checkVarOnArc(varModifierMap, diagonalVars, postPlaceId, false);
269
270
if(transition.guard != nullptr){
271
transition.guard->getVariables(guardVars);
272
}
273
// we have to copy here, the following loop has the *potential* to modify _partition[postPlaceId]
274
const std::vector<Colored::EquivalenceClass> placePartition = _partition[postPlaceId].getEquivalenceClasses();
275
276
//Partition each of the equivalence classes
277
for(const auto &eqClass : placePartition){
278
auto varMaps = prepareVariables(varModifierMap, eqClass, postArc, postPlaceId);
279
280
//If there are variables in the guard, that doesn't come from the postPlace
281
//we give them the full interval
141
282
for(auto& varMap : varMaps){
142
for(auto var : guardVars){
283
for(auto* var : guardVars){
143
284
if(varMap.count(var) == 0){
144
285
varMap[var].addInterval(var->colorType->getFullInterval());
145
286
}
146
287
}
147
288
}
148
149
if(transition->guard != nullptr){
150
transition->guard->restrictVars(varMaps, diagonalVars);
151
}
152
153
std::unordered_map<uint32_t, std::set<const Colored::Variable *>> placeVariableMap;
154
for(auto inArc : transition->input_arcs){
155
//Hack to avoid considering dot places and dealing with retrieving the correct dot pointer
156
if(_places->operator[](inArc.place).type->getName() == "Dot" || _places->operator[](inArc.place).type->getName() == "dot"){
157
_partition[inArc.place].diagonal = true;
158
}
159
160
if(_partition[inArc.place].diagonal){
161
continue;
162
}
163
164
std::unordered_map<const PetriEngine::Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>> preVarModifierMap;
165
std::unordered_map<uint32_t, const PetriEngine::Colored::Variable *> preVarPositionMap;
166
std::set<const PetriEngine::Colored::Variable *> preArcVars;
167
inArc.expr->getVariables(preArcVars, preVarPositionMap, preVarModifierMap);
168
for(auto placeVariables : placeVariableMap){
169
for(auto variable : preArcVars){
170
if(placeVariables.second.count(variable)){
171
_partition[inArc.place].diagonal = true;
172
_partition[placeVariables.first].diagonal = true;
173
addToQueue(inArc.place);
174
addToQueue(placeVariables.first);
175
break;
176
}
177
}
178
if(_partition[inArc.place].diagonal) {
179
break;
180
}
181
}
182
placeVariableMap[inArc.place] = preArcVars;
183
184
if(_partition[inArc.place].diagonal){
185
continue;
186
}
187
188
if(_partition[postPlaceId].diagonal){
189
for(auto preVar : preArcVars){
190
if(postArcVars.count(preVar)){
191
//maybe something different should happen for tuples
192
// --(x,y)-->[]--(z,y)-->
193
_partition[inArc.place].diagonal = true;
194
break;
195
}
196
}
197
}
198
199
if(_partition[inArc.place].diagonal){
200
addToQueue(inArc.place);
201
continue;
202
}
203
204
for(auto varModMap : preVarModifierMap){
205
if(varModMap.second.size() > 1){
206
uint32_t actualSize = 0;
207
for(auto map : varModMap.second){
208
if(!map.empty()){
209
actualSize++;
210
}
211
}
212
if(actualSize > 1) {
213
_partition[inArc.place].diagonal = true;
214
}
215
}
216
}
217
for(auto preVar : preArcVars){
218
if(diagonalVars.count(preVar)){
219
//should only happen if the variable is not in a tuple
220
_partition[inArc.place].diagonal = true;
221
break;
222
}
223
}
224
225
auto outIntervals = inArc.expr->getOutputIntervals(varMaps);
226
outIntervals.simplify();
227
EquivalenceVec newEqVec;
228
EquivalenceClass newEqClass = EquivalenceClass(_partition[inArc.place]._equivalenceClasses.back()._colorType, outIntervals);
229
newEqVec._equivalenceClasses.push_back(newEqClass);
230
231
if((_partition[inArc.place].diagonal || splitPartition(newEqVec, inArc.place))){
232
addToQueue(inArc.place);
233
}
234
}
235
}
236
237
//is this still needed? does not seem so
238
// std::set<const PetriEngine::Colored::Variable *> preArcVars;
239
// for(auto inArc : transition->input_arcs){
240
// inArc.expr->getVariables(preArcVars);
241
// for(auto postVar : postArcVars){
242
// if(preArcVars.count(postVar)){
243
// if(diagonalVars.count(postVar)){
244
// _partition[inArc.place].diagonal = true;
245
// }
246
// }
247
// }
248
// }
289
if(transition.guard != nullptr){
290
transition.guard->restrictVars(varMaps, diagonalVars);
291
}
292
293
handleInArcs(transition, diagonalVars, varPositionMap, varMaps, postPlaceId);
294
}
295
}
296
297
void PartitionBuilder::handleInArcs(const Transition &transition, std::set<const Colored::Variable*> &diagonalVars, const PositionVariableMap &varPositionMap, const std::vector<PetriEngine::Colored::VariableIntervalMap> &varMaps, uint32_t postPlaceId){
298
std::unordered_map<uint32_t,PositionVariableMap> placeVariableMap;
299
for(const auto &inArc : transition.input_arcs){
300
//Hack to avoid considering dot places
301
if(_places[inArc.place].type == ColorType::dotInstance()){
302
_partition[inArc.place].setDiagonal(true);
303
}
304
305
if(_partition[inArc.place].isDiagonal()){
306
continue;
307
}
308
VariableModifierMap preVarModifierMap;
309
PositionVariableMap preVarPositionMap;
310
std::set<const PetriEngine::Colored::Variable *> preArcVars;
311
inArc.expr->getVariables(preArcVars, preVarPositionMap, preVarModifierMap, true);
312
checkVarOnInputArcs(placeVariableMap, preVarPositionMap, diagonalVars, inArc.place);
313
placeVariableMap[inArc.place] = preVarPositionMap;
314
if(checkDiagonal(inArc.place)) continue;
315
316
markSharedVars(preVarPositionMap, varPositionMap, postPlaceId, inArc.place);
317
if(checkDiagonal(inArc.place)) continue;
318
checkVarOnArc(preVarModifierMap, diagonalVars, inArc.place, true);
319
if(checkDiagonal(inArc.place)) continue;
320
321
checkVarInGuard(preVarPositionMap, diagonalVars, inArc.place);
322
if(checkDiagonal(inArc.place)) continue;
323
324
_partition[inArc.place].mergeEqClasses();
325
if(_partition[inArc.place].getEquivalenceClasses().size() >=
326
_partition[inArc.place].getEquivalenceClasses().back().type()->size(_partition[inArc.place].getDiagonalTuplePositions())){
327
_partition[inArc.place].setDiagonal(true);
328
continue;
329
}
330
331
if(checkTupleDiagonal(inArc.place)){
332
continue;
333
}
334
335
applyNewIntervals(inArc, varMaps);
336
}
249
337
}
250
338
251
339
void PartitionBuilder::addToQueue(uint32_t placeId){
261
349
if(_partition.count(placeId) == 0){
262
350
_partition[placeId] = equivalenceVec;
263
351
} else {
264
EquivalenceClass intersection = EquivalenceClass();
352
EquivalenceClass intersection(++_eq_id_counter);
265
353
uint32_t ecPos1 = 0, ecPos2 = 0;
266
354
while(findOverlap(equivalenceVec, _partition[placeId],ecPos1, ecPos2, intersection)) {
267
auto ec1 = equivalenceVec._equivalenceClasses[ecPos1];
268
auto ec2 = _partition[placeId]._equivalenceClasses[ecPos2];
269
auto rightSubtractEc = ec1.subtract(ec2, false);
270
auto leftSubtractEc = ec2.subtract(ec1, false);
271
// if((_places->operator[](placeId).name == "NB_ATTENTE_A")) {
272
// std::cout << "comparing " << ec2.toString() << " to " << ec1.toString() << std::endl;
273
274
// std::cout << "Intersection: " << intersection.toString() << std::endl;
275
// std::cout << "Left: " << leftSubtractEc.toString() << std::endl;
276
// std::cout << "Right: " << rightSubtractEc.toString() << std::endl;
277
// ec2.subtract(ec1, true);
278
// }
279
280
281
equivalenceVec._equivalenceClasses.erase(equivalenceVec._equivalenceClasses.begin() + ecPos1);
282
_partition[placeId]._equivalenceClasses.erase(_partition[placeId]._equivalenceClasses.begin() + ecPos2);
355
const auto &ec1 = equivalenceVec.getEquivalenceClasses()[ecPos1];
356
const auto &ec2 = _partition[placeId].getEquivalenceClasses()[ecPos2];
357
const auto rightSubtractEc = ec1.subtract(++_eq_id_counter, ec2, equivalenceVec.getDiagonalTuplePositions());
358
const auto leftSubtractEc = ec2.subtract(++_eq_id_counter, ec1, _partition[placeId].getDiagonalTuplePositions());
359
360
equivalenceVec.erase_Eqclass(ecPos1);
361
_partition[placeId].erase_Eqclass(ecPos2);
283
362
284
363
if(!intersection.isEmpty()){
285
_partition[placeId]._equivalenceClasses.push_back(intersection);
286
intersection._colorIntervals._intervals.clear();
364
_partition[placeId].push_back_Eqclass(intersection);
365
intersection.clear();
287
366
}
288
367
if(!leftSubtractEc.isEmpty()){
289
_partition[placeId]._equivalenceClasses.push_back(leftSubtractEc);
368
_partition[placeId].push_back_Eqclass(leftSubtractEc);
290
369
split = true;
291
370
}
292
371
if(!rightSubtractEc.isEmpty()){
293
equivalenceVec._equivalenceClasses.push_back(rightSubtractEc);
294
}
372
equivalenceVec.push_back_Eqclass(rightSubtractEc);
373
}
295
374
}
296
375
}
297
376
return split;
298
377
}
299
378
300
bool PartitionBuilder::findOverlap(EquivalenceVec equivalenceVec1, EquivalenceVec equivalenceVec2, uint32_t &overlap1, uint32_t &overlap2, EquivalenceClass &intersection){
301
for(uint32_t i = 0; i < equivalenceVec1._equivalenceClasses.size(); i++){
302
for(uint32_t j = 0; j < equivalenceVec2._equivalenceClasses.size(); j++){
303
auto ec = equivalenceVec1._equivalenceClasses[i];
304
auto ec2 = equivalenceVec2._equivalenceClasses[j];
379
bool PartitionBuilder::findOverlap(const EquivalenceVec &equivalenceVec1, const EquivalenceVec &equivalenceVec2, uint32_t &overlap1, uint32_t &overlap2, EquivalenceClass &intersection) {
380
for(uint32_t i = 0; i < equivalenceVec1.getEquivalenceClasses().size(); i++){
381
for(uint32_t j = 0; j < equivalenceVec2.getEquivalenceClasses().size(); j++){
382
const auto &ec = equivalenceVec1.getEquivalenceClasses()[i];
383
const auto &ec2 = equivalenceVec2.getEquivalenceClasses()[j];
305
384
306
auto intersectingEc = ec.intersect(ec2);
385
auto intersectingEc = ec.intersect(++_eq_id_counter, ec2);
307
386
if(!intersectingEc.isEmpty()){
308
387
overlap1 = i;
309
388
overlap2 = j;
315
394
return false;
316
395
}
317
396
318
std::vector<std::unordered_map<const Variable *, intervalTuple_t>>
397
std::vector<VariableIntervalMap>
319
398
PartitionBuilder::prepareVariables(
320
std::unordered_map<const Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMap,
321
EquivalenceClass *eqClass , Arc *arc, uint32_t placeId){
322
std::vector<std::unordered_map<const Variable *, intervalTuple_t>> varMaps;
323
std::unordered_map<const Variable *, intervalTuple_t> varMap;
399
const VariableModifierMap &varModifierMap,
400
const EquivalenceClass& eqClass , const Arc *arc, uint32_t placeId){
401
std::vector<VariableIntervalMap> varMaps;
402
VariableIntervalMap varMap;
324
403
varMaps.push_back(varMap);
325
404
std::unordered_map<uint32_t, ArcIntervals> placeArcIntervals;
326
405
ColorFixpoint postPlaceFixpoint;
327
postPlaceFixpoint.constraints = eqClass->_colorIntervals;
406
postPlaceFixpoint.constraints = eqClass.intervals();
328
407
ArcIntervals newArcInterval(&postPlaceFixpoint, varModifierMap);
329
408
uint32_t index = 0;
330
409
331
arc->expr->getArcIntervals(newArcInterval, postPlaceFixpoint, &index, 0);
332
placeArcIntervals[placeId] = newArcInterval;
333
intervalGenerator.getVarIntervals(varMaps, placeArcIntervals);
410
arc->expr->getArcIntervals(newArcInterval, postPlaceFixpoint, index, 0);
411
placeArcIntervals[placeId] = std::move(newArcInterval);
412
_interval_generator.getVarIntervals(varMaps, placeArcIntervals);
334
413
335
414
return varMaps;
336
415
}
337
416
338
417
void PartitionBuilder::handleLeafTransitions(){
339
for(uint32_t i = 0; i < _transitions->size(); i++){
340
auto transition = _transitions->operator[](i);
418
for(uint32_t i = 0; i < _transitions.size(); i++){
419
const Transition &transition = _transitions[i];
341
420
if(transition.output_arcs.empty() && !transition.input_arcs.empty()){
342
handleTransition(&transition, transition.input_arcs.back().place, &transition.input_arcs.back());
421
handleTransition(transition, transition.input_arcs.back().place, &transition.input_arcs.back());
343
422
}
344
423
}
345
424
}
346
425
}
347
}
b'\\ No newline at end of file'
426
}
Loggerhead is a web-based interface for Breezy
Version: 2.0.1