verifypn

Merge lp:~verifypn-cpn/verifypn/partitioning into lp:~tapaal-ltl/verifypn/random-fix

  1. partitioning
  2. Merge into random-fix
Proposed by Thomas Pedersen
Status: Merged
Merged at revision: 243
Proposed branch: lp:~verifypn-cpn/verifypn/partitioning
Merge into: lp:~tapaal-ltl/verifypn/random-fix
Diff against target: 2672 lines (+1506/-351)
20 files modified
include/PetriEngine/Colored/BindingGenerator.h (+35/-0)
include/PetriEngine/Colored/ColoredPetriNetBuilder.h (+23/-4)
include/PetriEngine/Colored/Colors.h (+0/-1)
include/PetriEngine/Colored/EquivalenceClass.h (+79/-0)
include/PetriEngine/Colored/Expressions.h (+121/-33)
include/PetriEngine/Colored/GuardRestrictor.h (+64/-22)
include/PetriEngine/Colored/IntervalGenerator.h (+5/-4)
include/PetriEngine/Colored/Intervals.h (+133/-5)
include/PetriEngine/Colored/PartitionBuilder.h (+49/-0)
include/PetriEngine/options.h (+3/-1)
include/PetriParse/PNMLParser.h (+4/-3)
src/PetriEngine/Colored/BindingGenerator.cpp (+106/-2)
src/PetriEngine/Colored/CMakeLists.txt (+2/-0)
src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp (+151/-40)
src/PetriEngine/Colored/EquivalenceClass.cpp (+116/-0)
src/PetriEngine/Colored/GuardRestrictor.cpp (+255/-215)
src/PetriEngine/Colored/PartitionBuilder.cpp (+333/-0)
src/PetriEngine/PQL/Expressions.cpp (+1/-1)
src/PetriParse/PNMLParser.cpp (+7/-6)
src/VerifyPN.cpp (+19/-14)
To merge this branch: bzr merge lp:~verifypn-cpn/verifypn/partitioning
Reviewer Review Type Date Requested Status
Peter Gjøl Jensen Pending
Review via email: mp+401116@code.launchpad.net

Commit message

Merge partitioning

To post a comment you must log in.

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'include/PetriEngine/Colored/BindingGenerator.h'
2--- include/PetriEngine/Colored/BindingGenerator.h 2021-03-15 10:04:47 +0000
3+++ include/PetriEngine/Colored/BindingGenerator.h 2021-04-14 13:35:08 +0000
4@@ -21,11 +21,46 @@
5 #include <unordered_map>
6
7 #include "ColoredNetStructures.h"
8+#include "EquivalenceClass.h"
9
10 namespace PetriEngine {
11
12 typedef std::unordered_map<std::string, Colored::ColorType*> ColorTypeMap;
13
14+ class NaiveBindingGenerator {
15+ public:
16+ class Iterator {
17+ private:
18+ NaiveBindingGenerator* _generator;
19+
20+ public:
21+ Iterator(NaiveBindingGenerator* generator);
22+
23+ bool operator==(Iterator& other);
24+ bool operator!=(Iterator& other);
25+ Iterator& operator++();
26+ const Colored::ExpressionContext::BindingMap operator++(int);
27+ Colored::ExpressionContext::BindingMap& operator*();
28+ };
29+ private:
30+ Colored::GuardExpression_ptr _expr;
31+ Colored::ExpressionContext::BindingMap _bindings;
32+ ColorTypeMap& _colorTypes;
33+
34+ bool eval();
35+
36+ public:
37+ NaiveBindingGenerator(Colored::Transition& transition,
38+ ColorTypeMap& colorTypes);
39+
40+ Colored::ExpressionContext::BindingMap& nextBinding();
41+ Colored::ExpressionContext::BindingMap& currentBinding();
42+ bool isInitial() const;
43+ Iterator begin();
44+ Iterator end();
45+ };
46+
47+
48 class FixpointBindingGenerator {
49 public:
50 class Iterator {
51
52=== modified file 'include/PetriEngine/Colored/ColoredPetriNetBuilder.h'
53--- include/PetriEngine/Colored/ColoredPetriNetBuilder.h 2021-03-23 09:15:21 +0000
54+++ include/PetriEngine/Colored/ColoredPetriNetBuilder.h 2021-04-14 13:35:08 +0000
55@@ -27,6 +27,7 @@
56 #include "../PetriNetBuilder.h"
57 #include "BindingGenerator.h"
58 #include "IntervalGenerator.h"
59+#include "PartitionBuilder.h"
60 #include "ArcIntervals.h"
61
62 namespace PetriEngine {
63@@ -80,6 +81,14 @@
64 return _time;
65 }
66
67+ double getPartitionTime() const {
68+ return _partitionTimer;
69+ }
70+
71+ double getPartitionVarMapTime() const {
72+ return _partitionVarMapTimer;
73+ }
74+
75 double getFixpointTime() const {
76 return _fixPointCreationTime;
77 }
78@@ -132,13 +141,15 @@
79
80 PetriNetBuilder& unfold();
81 PetriNetBuilder& stripColors();
82- void computePlaceColorFixpoint(uint32_t maxIntervals, uint32_t maxIntervalsReduced, int32_t timeout);
83+ void computePlaceColorFixpoint(uint32_t max_intervals, uint32_t max_intervals_reduced, int32_t timeout);
84+ void computePartition();
85
86 private:
87 std::unordered_map<std::string,uint32_t> _placenames;
88 std::unordered_map<std::string,uint32_t> _transitionnames;
89 std::unordered_map<uint32_t, std::unordered_map<uint32_t, Colored::ArcIntervals>> _arcIntervals;
90 std::unordered_map<uint32_t,std::vector<uint32_t>> _placePostTransitionMap;
91+ std::unordered_map<uint32_t,std::vector<uint32_t>> _placePreTransitionMap;
92 std::unordered_map<uint32_t,FixpointBindingGenerator> _bindings;
93 PTPlaceMap _ptplacenames;
94 PTTransitionMap _pttransitionnames;
95@@ -156,18 +167,25 @@
96 PetriNetBuilder _ptBuilder;
97 bool _unfolded = false;
98 bool _stripped = false;
99+ bool _fixpointDone = false;
100+ bool _partitionComputed = false;
101
102 std::vector<uint32_t> _placeFixpointQueue;
103+ std::unordered_map<uint32_t, Colored::EquivalenceVec> _partition;
104
105 double _time;
106 double _fixPointCreationTime;
107
108- double _timer;
109+ double _partitionTimer = 0;
110+
111+ double _partitionVarMapTimer = 0;
112
113 std::string arcToString(Colored::Arc& arc) const ;
114
115 void printPlaceTable();
116
117+
118+
119 std::unordered_map<uint32_t, Colored::ArcIntervals> setupTransitionVars(Colored::Transition transition);
120
121 void addArc(const std::string& place,
122@@ -180,11 +198,12 @@
123 void processInputArcs(Colored::Transition& transition, uint32_t currentPlaceId, uint32_t transitionId, bool &transitionActivated, uint32_t max_intervals);
124 void processOutputArcs(Colored::Transition& transition);
125
126- void unfoldPlace(const Colored::Place* place, const PetriEngine::Colored::Color *color);
127+ void unfoldPlace(const Colored::Place* place, const PetriEngine::Colored::Color *color, uint32_t unfoldPlace, uint32_t id);
128 void unfoldTransition(Colored::Transition& transition);
129 void handleOrphanPlace(Colored::Place& place, std::unordered_map<std::string, uint32_t> unfoldedPlaceMap);
130+ void createPartionVarmaps();
131
132- void unfoldArc(Colored::Arc& arc, Colored::ExpressionContext::BindingMap& binding, std::string& name, bool input);
133+ void unfoldArc(Colored::Arc& arc, Colored::ExpressionContext::BindingMap& binding, std::string& name);
134 };
135
136 //Used for checking if a variable is inside either a succ or pred expression
137
138=== modified file 'include/PetriEngine/Colored/Colors.h'
139--- include/PetriEngine/Colored/Colors.h 2021-03-15 10:04:47 +0000
140+++ include/PetriEngine/Colored/Colors.h 2021-04-14 13:35:08 +0000
141@@ -357,7 +357,6 @@
142 struct ColorFixpoint {
143 Colored::intervalTuple_t constraints;
144 bool inQueue;
145- uint32_t productSize;
146
147 bool constainsColor(std::pair<const PetriEngine::Colored::Color *const, std::vector<uint32_t>> constPair) {
148 std::unordered_map<uint32_t, bool> contained;
149
150=== added file 'include/PetriEngine/Colored/EquivalenceClass.h'
151--- include/PetriEngine/Colored/EquivalenceClass.h 1970-01-01 00:00:00 +0000
152+++ include/PetriEngine/Colored/EquivalenceClass.h 2021-04-14 13:35:08 +0000
153@@ -0,0 +1,79 @@
154+#ifndef PARTITION_H
155+#define PARTITION_H
156+
157+#include "Intervals.h"
158+#include "Colors.h"
159+#include "ArcIntervals.h"
160+
161+namespace PetriEngine {
162+ namespace Colored {
163+ class EquivalenceClass {
164+ public:
165+ EquivalenceClass();
166+ EquivalenceClass(ColorType *colorType);
167+ EquivalenceClass(ColorType *colorType, intervalTuple_t colorIntervals);
168+ ~EquivalenceClass() {}
169+ std::string toString(){
170+ std::cout << "Id: " << _id << std::endl;
171+ return _colorIntervals.toString();
172+ }
173+
174+ bool isEmpty(){
175+ if(_colorIntervals.size() < 1 || _colorIntervals.getFirst().size() < 1){
176+ return true;
177+ }
178+ return false;
179+ }
180+
181+ bool containsColor(std::vector<uint32_t> ids);
182+
183+ size_t size();
184+
185+ EquivalenceClass intersect(EquivalenceClass other);
186+
187+ EquivalenceClass subtract(EquivalenceClass other, bool print);
188+
189+ static uint32_t idCounter;
190+ uint32_t _id;
191+ ColorType *_colorType;
192+ intervalTuple_t _colorIntervals;
193+
194+ private:
195+
196+
197+ };
198+
199+ struct EquivalenceVec{
200+ std::vector<EquivalenceClass> _equivalenceClasses;
201+ std::unordered_map<const Colored::Color *, EquivalenceClass *> colorEQClassMap;
202+ bool diagonal = false;
203+
204+ void applyPartition(Colored::ArcIntervals& arcInterval){
205+ if(diagonal){
206+ return;
207+ }
208+ std::vector<Colored::intervalTuple_t> newTupleVec;
209+ for(auto intervalTuple : arcInterval._intervalTupleVec){
210+ intervalTuple.combineNeighbours();
211+ intervalTuple_t newIntervalTuple;
212+ for(auto interval : intervalTuple._intervals){
213+ for(auto EQClass : _equivalenceClasses){
214+ for(auto EQinterval : EQClass._colorIntervals._intervals){
215+ auto overlap = interval.getOverlap(EQinterval);
216+ if(overlap.isSound()){
217+ newIntervalTuple.addInterval(EQinterval.getSingleColorInterval());
218+ continue;
219+ }
220+ }
221+ }
222+ }
223+ newTupleVec.push_back(std::move(newIntervalTuple));
224+ }
225+ arcInterval._intervalTupleVec = std::move(newTupleVec);
226+ }
227+ };
228+
229+ }
230+}
231+
232+#endif /* PARTITION_H */
233\ No newline at end of file
234
235=== modified file 'include/PetriEngine/Colored/Expressions.h'
236--- include/PetriEngine/Colored/Expressions.h 2021-03-31 13:49:31 +0000
237+++ include/PetriEngine/Colored/Expressions.h 2021-04-14 13:35:08 +0000
238@@ -31,6 +31,7 @@
239
240 #include "Colors.h"
241 #include "Multiset.h"
242+#include "EquivalenceClass.h"
243 #include "ArcIntervals.h"
244 #include "GuardRestrictor.h"
245 #include "../errorcodes.h"
246@@ -44,6 +45,7 @@
247
248 BindingMap& binding;
249 std::unordered_map<std::string, ColorType*>& colorTypes;
250+ Colored::EquivalenceVec& placePartition;
251
252 const Color* findColor(const std::string& color) const {
253 if (color.compare("dot") == 0)
254@@ -366,6 +368,10 @@
255 const Color* eval(ExpressionContext& context) const override {
256 return &++(*_color->eval(context));
257 }
258+
259+ bool isTuple() const override {
260+ return _color->isTuple();
261+ }
262
263 void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
264 //save index before evaluating nested expression to decrease all the correct modifiers
265@@ -390,7 +396,7 @@
266
267 auto nestedInterval = _color->getOutputIntervals(varMap, colortypes);
268 Colored::GuardRestrictor guardRestrictor = Colored::GuardRestrictor();
269- return guardRestrictor.shiftIntervals(colortypes, &nestedInterval, 1, colortypesBefore);
270+ return guardRestrictor.shiftIntervals(varMap, colortypes, &nestedInterval, 1, colortypesBefore);
271 }
272
273 void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override {
274@@ -420,6 +426,10 @@
275 const Color* eval(ExpressionContext& context) const override {
276 return &--(*_color->eval(context));
277 }
278+
279+ bool isTuple() const override {
280+ return _color->isTuple();
281+ }
282
283 void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
284 //save index before evaluating nested expression to decrease all the correct modifiers
285@@ -444,7 +454,7 @@
286
287 auto nestedInterval = _color->getOutputIntervals(varMap, colortypes);
288 Colored::GuardRestrictor guardRestrictor;
289- return guardRestrictor.shiftIntervals(colortypes, &nestedInterval, -1, colortypesBefore);
290+ return guardRestrictor.shiftIntervals(varMap, colortypes, &nestedInterval, -1, colortypesBefore);
291 }
292
293 void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override {
294@@ -583,7 +593,12 @@
295
296 virtual bool eval(ExpressionContext& context) const = 0;
297
298- virtual void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const = 0;
299+ virtual void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const = 0;
300+
301+ virtual void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const {
302+ std::set<const Colored::Variable*> diagonalVars;
303+ restrictVars(variableMap, diagonalVars);
304+ }
305 };
306
307 typedef std::shared_ptr<GuardExpression> GuardExpression_ptr;
308@@ -603,7 +618,11 @@
309 _right->getVariables(variables, varPositions, varModifierMap);
310 }
311
312- void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override {
313+ bool isTuple() const override {
314+ return _left->isTuple() || _right->isTuple();
315+ }
316+
317+ void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
318 std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapL;
319 std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapR;
320 std::unordered_map<uint32_t, const Colored::Variable *> varPositionsL;
321@@ -623,7 +642,7 @@
322 return;
323 }
324 Colored::GuardRestrictor guardRestrictor;
325- guardRestrictor.restrictDiagonal(&variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, true, true);
326+ guardRestrictor.restrictVars(variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, diagonalVars, true, true);
327 }
328
329 std::string toString() const override {
330@@ -645,13 +664,17 @@
331 bool eval(ExpressionContext& context) const override {
332 return _left->eval(context) > _right->eval(context);
333 }
334+
335+ bool isTuple() const override {
336+ return _left->isTuple() || _right->isTuple();
337+ }
338
339 void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
340 _left->getVariables(variables, varPositions, varModifierMap);
341 _right->getVariables(variables, varPositions, varModifierMap);
342 }
343
344- void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override {
345+ void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
346 std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapL;
347 std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapR;
348 std::unordered_map<uint32_t, const Colored::Variable *> varPositionsL;
349@@ -672,7 +695,7 @@
350 }
351
352 Colored::GuardRestrictor guardRestrictor;
353- guardRestrictor.restrictDiagonal(&variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, false, true);
354+ guardRestrictor.restrictVars(variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, diagonalVars, false, true);
355 }
356
357 std::string toString() const override {
358@@ -693,13 +716,17 @@
359 bool eval(ExpressionContext& context) const override {
360 return _left->eval(context) <= _right->eval(context);
361 }
362+
363+ bool isTuple() const override {
364+ return _left->isTuple() || _right->isTuple();
365+ }
366
367 void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
368 _left->getVariables(variables, varPositions, varModifierMap);
369 _right->getVariables(variables, varPositions, varModifierMap);
370 }
371
372- void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override {
373+ void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
374 std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapL;
375 std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapR;
376 std::unordered_map<uint32_t, const Colored::Variable *> varPositionsL;
377@@ -720,7 +747,7 @@
378 }
379
380 Colored::GuardRestrictor guardRestrictor;
381- guardRestrictor.restrictDiagonal(&variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, true, false);
382+ guardRestrictor.restrictVars(variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, diagonalVars, true, false);
383 }
384
385 std::string toString() const override {
386@@ -742,13 +769,17 @@
387 bool eval(ExpressionContext& context) const override {
388 return _left->eval(context) >= _right->eval(context);
389 }
390+
391+ bool isTuple() const override {
392+ return _left->isTuple() || _right->isTuple();
393+ }
394
395 void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
396 _left->getVariables(variables, varPositions, varModifierMap);
397 _right->getVariables(variables, varPositions, varModifierMap);
398 }
399
400- void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override {
401+ void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
402 std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapL;
403 std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapR;
404 std::unordered_map<uint32_t, const Colored::Variable *> varPositionsL;
405@@ -769,7 +800,7 @@
406 }
407
408 Colored::GuardRestrictor guardRestrictor;
409- guardRestrictor.restrictDiagonal(&variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, false, false);
410+ guardRestrictor.restrictVars(variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, diagonalVars, false, false);
411 }
412
413 std::string toString() const override {
414@@ -791,13 +822,17 @@
415 return _left->eval(context) == _right->eval(context);
416 }
417
418+ bool isTuple() const override {
419+ return _left->isTuple() || _right->isTuple();
420+ }
421+
422 void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
423 _left->getVariables(variables, varPositions, varModifierMap);
424 _right->getVariables(variables, varPositions, varModifierMap);
425 }
426
427
428- void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override {
429+ void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
430 std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapL;
431 std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapR;
432 std::unordered_map<uint32_t, const Colored::Variable *> varPositionsL;
433@@ -818,7 +853,7 @@
434 }
435
436 Colored::GuardRestrictor guardRestrictor;
437- guardRestrictor.restrictEquality(&variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR);
438+ guardRestrictor.restrictEquality(variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, diagonalVars);
439 }
440
441 std::string toString() const override {
442@@ -839,13 +874,17 @@
443 bool eval(ExpressionContext& context) const override {
444 return _left->eval(context) != _right->eval(context);
445 }
446+
447+ bool isTuple() const override {
448+ return _left->isTuple() || _right->isTuple();
449+ }
450
451 void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
452 _left->getVariables(variables, varPositions, varModifierMap);
453 _right->getVariables(variables, varPositions, varModifierMap);
454 }
455
456- void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override {
457+ void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
458
459 }
460
461@@ -866,6 +905,10 @@
462 bool eval(ExpressionContext& context) const override {
463 return !_expr->eval(context);
464 }
465+
466+ bool isTuple() const override {
467+ return _expr->isTuple();
468+ }
469
470 void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
471 _expr->getVariables(variables, varPositions, varModifierMap, index);
472@@ -876,7 +919,7 @@
473 return res;
474 }
475
476- void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override {
477+ void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
478 std::set<const Colored::Variable *> variables;
479 _expr->getVariables(variables);
480 //TODO: invert the var intervals here instead of using the full intervals
481@@ -903,15 +946,19 @@
482 bool eval(ExpressionContext& context) const override {
483 return _left->eval(context) && _right->eval(context);
484 }
485+
486+ bool isTuple() const override {
487+ return _left->isTuple() || _right->isTuple();
488+ }
489
490 void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
491 _left->getVariables(variables, varPositions, varModifierMap);
492 _right->getVariables(variables, varPositions, varModifierMap);
493 }
494
495- void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override {
496- _left->restrictVars(variableMap);
497- _right->restrictVars(variableMap);
498+ void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
499+ _left->restrictVars(variableMap, diagonalVars);
500+ _right->restrictVars(variableMap, diagonalVars);
501 }
502
503 std::string toString() const override {
504@@ -932,16 +979,20 @@
505 bool eval(ExpressionContext& context) const override {
506 return _left->eval(context) || _right->eval(context);
507 }
508+
509+ bool isTuple() const override {
510+ return _left->isTuple() || _right->isTuple();
511+ }
512
513 void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
514 _left->getVariables(variables, varPositions, varModifierMap);
515 _right->getVariables(variables, varPositions, varModifierMap);
516 }
517
518- void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override{
519+ void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override{
520 auto varMapCopy = variableMap;
521- _left->restrictVars(variableMap);
522- _right->restrictVars(varMapCopy);
523+ _left->restrictVars(variableMap, diagonalVars);
524+ _right->restrictVars(varMapCopy, diagonalVars);
525
526 for(size_t i = 0; i < variableMap.size(); i++){
527 for(auto& varPair : varMapCopy[i]){
528@@ -996,15 +1047,26 @@
529
530 public:
531 virtual ~AllExpression() {};
532- std::vector<const Color*> eval(ExpressionContext& context) const {
533- std::vector<const Color*> colors;
534+ std::vector<std::pair<const Color*,uint32_t>> eval(ExpressionContext& context) const {
535+ std::vector<std::pair<const Color*,uint32_t>> colors;
536 assert(_sort != nullptr);
537- for (size_t i = 0; i < _sort->size(); i++) {
538- colors.push_back(&(*_sort)[i]);
539+ if(context.placePartition.diagonal || context.placePartition._equivalenceClasses.empty()){
540+ for (size_t i = 0; i < _sort->size(); i++) {
541+ colors.push_back(std::make_pair(&(*_sort)[i], 1));
542+ }
543+ } else {
544+ for (auto EqClass : context.placePartition._equivalenceClasses){
545+ colors.push_back(std::make_pair(_sort->getColor(EqClass._colorIntervals.getLowerIds()),EqClass.size()));
546+ }
547 }
548+
549 return colors;
550 }
551
552+ bool isTuple() const override {
553+ return _sort->productSize() > 1;
554+ }
555+
556 void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const {
557 for (size_t i = 0; i < _sort->size(); i++) {
558 constantMap[index].push_back(&(*_sort)[i]);
559@@ -1068,21 +1130,30 @@
560
561 public:
562 Multiset eval(ExpressionContext& context) const override {
563- std::vector<const Color*> colors;
564+ std::vector<std::pair<const Color*,uint32_t>> col;
565 if (!_color.empty()) {
566 for (auto elem : _color) {
567- colors.push_back(elem->eval(context));
568+ col.push_back(std::make_pair(elem->eval(context), _number));
569 }
570 } else if (_all != nullptr) {
571- colors = _all->eval(context);
572- }
573- std::vector<std::pair<const Color*,uint32_t>> col;
574- for (auto elem : colors) {
575- col.push_back(std::make_pair(elem, _number));
576- }
577+ col = _all->eval(context);
578+ for(auto& pair : col){
579+ pair.second = pair.second * _number;
580+ }
581+ }
582+
583 return Multiset(col);
584 }
585
586+ bool isTuple() const override {
587+ for(auto colorExpr : _color){
588+ if(colorExpr->isTuple()){
589+ return true;
590+ }
591+ }
592+ return false;
593+ }
594+
595 void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
596 if (_all != nullptr)
597 return;
598@@ -1204,6 +1275,15 @@
599 }
600 }
601
602+ bool isTuple() const override {
603+ for(auto arcExpr : _constituents){
604+ if(arcExpr->isTuple()){
605+ return true;
606+ }
607+ }
608+ return false;
609+ }
610+
611 bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
612 for (auto elem : _constituents) {
613 uint32_t newIndex = 0;
614@@ -1284,6 +1364,10 @@
615 //_right->getVariables(variables, varPositions, varModifierMap);
616 }
617
618+ bool isTuple() const override {
619+ return _left->isTuple() || _right->isTuple();
620+ }
621+
622 bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
623 return _left->getArcIntervals(arcIntervals, cfp, index, modifier);
624 //We ignore the restrictions imposed by the subtraction for now
625@@ -1339,6 +1423,10 @@
626 _expr->getVariables(variables, varPositions,varModifierMap);
627 }
628
629+ bool isTuple() const override {
630+ return _expr->isTuple();
631+ }
632+
633 bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
634 return _expr ->getArcIntervals(arcIntervals, cfp, index, modifier);
635 }
636
637=== modified file 'include/PetriEngine/Colored/GuardRestrictor.h'
638--- include/PetriEngine/Colored/GuardRestrictor.h 2021-03-15 10:04:47 +0000
639+++ include/PetriEngine/Colored/GuardRestrictor.h 2021-04-14 13:35:08 +0000
640@@ -33,32 +33,46 @@
641
642 GuardRestrictor();
643
644- void restrictDiagonal(std::vector<std::unordered_map<const Variable *, intervalTuple_t>> *variableMap,
645- std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
646- std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
647- std::unordered_map<uint32_t, const Variable *> *varPositionsL,
648- std::unordered_map<uint32_t, const Variable *> *varPositionsR,
649- std::unordered_map<uint32_t, const Color*> *constantMapL,
650- std::unordered_map<uint32_t, const Color*> *constantMapR,
651+ void restrictDiagonal(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
652+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
653+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
654+ std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsL,
655+ std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsR,
656+ std::unordered_map<uint32_t, const Color*> *constantMapL,
657+ std::unordered_map<uint32_t, const Color*> *constantMapR,
658+ std::set<const Colored::Variable*> &diagonalVars,
659+ const Colored::Variable *var,
660+ uint32_t index, bool lessthan, bool strict);
661+
662+
663+
664+ void restrictEquality(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
665+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
666+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
667+ std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsL,
668+ std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsR,
669+ std::unordered_map<uint32_t, const Color*> *constantMapL,
670+ std::unordered_map<uint32_t, const Color*> *constantMapR,
671+ std::set<const Colored::Variable*> &diagonalVars);
672+
673+ void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
674+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
675+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
676+ std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsL,
677+ std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsR,
678+ std::unordered_map<uint32_t, const Color*> *constantMapL,
679+ std::unordered_map<uint32_t, const Color*> *constantMapR,
680+ std::set<const Colored::Variable*> &diagonalVars,
681 bool lessthan, bool strict);
682
683- void restrictEquality(std::vector<std::unordered_map<const Variable *, intervalTuple_t>> *variableMap,
684- std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
685- std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
686- std::unordered_map<uint32_t, const Variable *> *varPositionsL,
687- std::unordered_map<uint32_t, const Variable *> *varPositionsR,
688- std::unordered_map<uint32_t, const Color*> *constantMapL,
689- std::unordered_map<uint32_t, const Color*> *constantMapR);
690-
691- intervalTuple_t shiftIntervals(std::vector<const ColorType *> *colortypes,
692- intervalTuple_t *intervals,
693- int32_t modifier,
694- uint32_t ctSizeBefore) const;
695+ intervalTuple_t shiftIntervals(std::unordered_map<const Variable *, intervalTuple_t>& varMap,
696+ std::vector<const ColorType *> *colortypes, intervalTuple_t *intervals,
697+ int32_t modifier, uint32_t ctSizeBefore) const;
698
699 private:
700 int32_t getVarModifier(std::unordered_map<uint32_t, int32_t> *modPairMap, uint32_t index);
701 interval_t getIntervalFromIds(std::vector<uint32_t> *idVec, uint32_t ctSize, int32_t modifier);
702- intervalTuple_t getIntervalOverlap(std::vector<interval_t> *intervals1, std::vector<interval_t> *intervals2);
703+ intervalTuple_t getIntervalOverlap(std::vector<Colored::interval_t> *intervals1, std::vector<Colored::interval_t> *intervals2);
704
705 void expandIdVec(std::unordered_map<const Variable *, intervalTuple_t> *varMap,
706 std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *mainVarModifierMap,
707@@ -68,13 +82,41 @@
708 const Variable *otherVar,
709 std::vector<uint32_t> &idVec, size_t targetSize, uint32_t index);
710
711- void expandIntervalVec(std::unordered_map<const Variable *, intervalTuple_t> *varMap,
712+ void expandIntervalVec(std::unordered_map<const Variable *, intervalTuple_t> varMap,
713 std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *mainVarModifierMap,
714 std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *otherVarModifierMap,
715 std::unordered_map<uint32_t, const Variable *> *varPositions,
716 std::unordered_map<uint32_t, const Color*> *constantMap,
717 const Variable *otherVar,
718- std::vector<interval_t> &intervalVec, size_t targetSize, uint32_t index);
719+ std::vector<interval_t> &intervalVec, size_t targetSize, uint32_t index);
720+
721+ void restrictByConstant(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
722+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *mainVarModifierMap,
723+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *otherVarModifierMap,
724+ std::unordered_map<uint32_t, const Colored::Variable *> *varPositions,
725+ std::unordered_map<uint32_t, const Color*> *constantMap,
726+ const Colored::Variable *var,
727+ const Colored::Variable *otherVar,
728+ uint32_t index, bool lessthan, bool strict);
729+
730+ void restrictEqByConstant(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
731+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *mainVarModifierMap,
732+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *otherVarModifierMap,
733+ std::unordered_map<uint32_t, const Colored::Variable *> *varPositions,
734+ std::unordered_map<uint32_t, const Color*> *constantMap,
735+ const Colored::Variable *var,
736+ uint32_t index);
737+
738+ void restrictEqDiagonal(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
739+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
740+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
741+ std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsL,
742+ std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsR,
743+ std::unordered_map<uint32_t, const Color*> *constantMapL,
744+ std::unordered_map<uint32_t, const Color*> *constantMapR,
745+ std::set<const Colored::Variable*> &diagonalVars,
746+ const Colored::Variable *var,
747+ uint32_t index);
748 };
749 }
750 }
751
752=== modified file 'include/PetriEngine/Colored/IntervalGenerator.h'
753--- include/PetriEngine/Colored/IntervalGenerator.h 2021-03-15 10:04:47 +0000
754+++ include/PetriEngine/Colored/IntervalGenerator.h 2021-04-14 13:35:08 +0000
755@@ -83,9 +83,9 @@
756 }
757
758 void populateLocalMap(Colored::ArcIntervals *arcIntervals,
759- std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t> &varMap,
760- std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t> &localVarMap,
761- Colored::interval_t* interval, bool& allVarsAssigned, uint32_t tuplePos){
762+ std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t> &varMap,
763+ std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t> &localVarMap,
764+ Colored::interval_t* interval, bool& allVarsAssigned, uint32_t tuplePos){
765 for(auto& pair : arcIntervals->_varIndexModMap){
766 Colored::intervalTuple_t varIntervals;
767 std::vector<Colored::ColorType*> varColorTypes;
768@@ -178,7 +178,8 @@
769
770 if(allVarsAssigned){
771 newVarMapVec.push_back(std::move(localVarMap));
772- }
773+ }
774+
775 }
776 }
777 variableMaps = std::move(newVarMapVec);
778
779=== modified file 'include/PetriEngine/Colored/Intervals.h'
780--- include/PetriEngine/Colored/Intervals.h 2021-03-24 10:39:01 +0000
781+++ include/PetriEngine/Colored/Intervals.h 2021-04-14 13:35:08 +0000
782@@ -23,6 +23,11 @@
783 #include <set>
784 #include <unordered_map>
785 #include <chrono>
786+#include <string>
787+#include <string.h>
788+#include <iostream>
789+#include <fstream>
790+#include <sstream>
791
792
793 namespace PetriEngine {
794@@ -116,6 +121,14 @@
795 return ids;
796 }
797
798+ interval_t getSingleColorInterval(){
799+ interval_t newInterval;
800+ for(auto id : getLowerIds()){
801+ newInterval.addRange(id,id);
802+ }
803+ return newInterval;
804+ }
805+
806 bool equals(interval_t other){
807 if(other.size() != size()){
808 return false;
809@@ -169,11 +182,55 @@
810 return overlapInterval;
811 }
812
813+ std::vector<interval_t> getSubtracted(interval_t other, uint32_t ctSize){
814+ std::vector<interval_t> result;
815+
816+ if(size() != other.size()){
817+ return result;
818+ }
819+
820+ for(uint32_t i = 0; i < size(); i++){
821+ interval_t newInterval = *this;
822+
823+ int32_t newMinUpper = std::min(((int) other[i]._lower) -1, (int)_ranges[i]._upper);
824+ //uint32_t otherUpper = (other[i]._upper +1) >= ctSize? ctSize-1: other[i]._upper +1;
825+ uint32_t newMaxLower = std::max(other[i]._upper +1, _ranges[i]._lower);
826+
827+ if(((int32_t) _ranges[i]._lower) <= newMinUpper && newMaxLower <= _ranges[i]._upper){
828+ auto intervalCopy = *this;
829+ auto lowerRange = Reachability::range_t(_ranges[i]._lower, newMinUpper);
830+ auto upperRange = Reachability::range_t(newMaxLower, _ranges[i]._upper);
831+ newInterval._ranges[i] = lowerRange;
832+ intervalCopy._ranges[i] = upperRange;
833+ result.push_back(std::move(intervalCopy));
834+ result.push_back(std::move(newInterval));
835+
836+ } else if (((int32_t) _ranges[i]._lower) <= newMinUpper){
837+ auto lowerRange = Reachability::range_t(_ranges[i]._lower, newMinUpper);
838+ newInterval._ranges[i] = lowerRange;
839+ result.push_back(std::move(newInterval));
840+ } else if (newMaxLower <= _ranges[i]._upper) {
841+ auto upperRange = Reachability::range_t(newMaxLower, _ranges[i]._upper);
842+ newInterval._ranges[i] = upperRange;
843+ result.push_back(std::move(newInterval));
844+ }
845+ }
846+ return result;
847+ }
848+
849 void print() {
850 for(auto range : _ranges){
851 std::cout << " " << range._lower << "-" << range._upper << " ";
852 }
853 }
854+
855+ std::string toString() {
856+ std::ostringstream strs;
857+ for(auto range : _ranges){
858+ strs << " " << range._lower << "-" << range._upper << " ";
859+ }
860+ return strs.str();
861+ }
862 };
863
864 struct closestIntervals {
865@@ -299,13 +356,19 @@
866 }
867
868 for (auto& localInterval : _intervals) {
869- bool overlap = true;
870+ bool extendsInterval = true;
871 enum FoundPlace {undecided, greater, lower};
872 FoundPlace foundPlace = undecided;
873
874+ //uint32_t allowedDist = 1;
875+
876 for(uint32_t k = 0; k < interval.size(); k++){
877 if(interval[k]._lower > localInterval[k]._upper || localInterval[k]._lower > interval[k]._upper){
878- overlap = false;
879+ //if(interval[k]._lower > localInterval[k]._upper + allowedDist || localInterval[k]._lower > interval[k]._upper + allowedDist){
880+ extendsInterval = false;
881+ // } else {
882+ // allowedDist = 0;
883+ // }
884 }
885 if(interval[k]._lower < localInterval[k]._lower){
886 if(foundPlace == undecided){
887@@ -316,12 +379,12 @@
888 foundPlace = greater;
889 }
890 }
891- if(!overlap && foundPlace != undecided){
892+ if(!extendsInterval && foundPlace != undecided){
893 break;
894 }
895 }
896
897- if(overlap) {
898+ if(extendsInterval) {
899 for(uint32_t k = 0; k < interval.size(); k++){
900 localInterval[k] |= interval[k];
901 }
902@@ -383,6 +446,16 @@
903 }
904 }
905
906+ std::string toString() {
907+ std::string out;
908+ for (auto interval : _intervals){
909+ out += "[";
910+ out += interval.toString();
911+ out += "]\n";
912+ }
913+ return out;
914+ }
915+
916 std::vector<uint32_t> getLowerIds(){
917 std::vector<uint32_t> ids;
918 for(auto interval : _intervals){
919@@ -545,8 +618,8 @@
920 }
921
922 _intervals.erase(_intervals.begin() + closestInterval.intervalId2);
923-
924 }
925+ simplify();
926 }
927
928 closestIntervals getClosestIntervals(){
929@@ -560,7 +633,14 @@
930 for(uint32_t k = 0; k < interval->size(); k++) {
931 int32_t val1 = otherInterval->operator[](k)._lower - interval->operator[](k)._upper;
932 int32_t val2 = interval->operator[](k)._lower - otherInterval->operator[](k)._upper;
933+ // int32_t lowerDist = interval->operator[](k)._lower > otherInterval->operator[](k)._lower?
934+ // interval->operator[](k)._lower - otherInterval->operator[](k)._lower :
935+ // otherInterval->operator[](k)._lower - interval->operator[](k)._lower;
936+ // int32_t upperDist = interval->operator[](k)._upper > otherInterval->operator[](k)._upper?
937+ // interval->operator[](k)._upper - otherInterval->operator[](k)._upper :
938+ // otherInterval->operator[](k)._upper - interval->operator[](k)._upper;
939 dist += std::max(0, std::max(val1, val2));
940+ //dist += std::max(upperDist + lowerDist, upperDist + lowerDist + std::max(val1, val2));
941 if(dist >= currentBest.distance){
942 break;
943 }
944@@ -621,6 +701,54 @@
945 for (auto i = rangesToRemove.rbegin(); i != rangesToRemove.rend(); ++i) {
946 _intervals.erase(_intervals.begin() + *i);
947 }
948+ }
949+
950+ void combineNeighbours() {
951+ std::set<uint32_t> rangesToRemove;
952+ if(_intervals.empty()){
953+ return;
954+ }
955+
956+ for (uint32_t i = 0; i < _intervals.size(); i++) {
957+ auto interval = &_intervals[i];
958+ if(!interval->isSound()){
959+ rangesToRemove.insert(i);
960+ continue;
961+ }
962+ for(uint32_t j = i+1; j < _intervals.size(); j++){
963+ auto otherInterval = &_intervals[j];
964+
965+ if(!otherInterval->isSound()){
966+ continue;
967+ }
968+ bool overlap = true;
969+
970+ uint32_t dist = 1;
971+
972+ if(overlap){
973+ for(uint32_t k = 0; k < interval->size(); k++) {
974+ if(interval->operator[](k)._lower > otherInterval->operator[](k)._upper || otherInterval->operator[](k)._lower > interval->operator[](k)._upper) {
975+ if(interval->operator[](k)._lower > otherInterval->operator[](k)._upper + dist || otherInterval->operator[](k)._lower > interval->operator[](k)._upper + dist) {
976+ overlap = false;
977+ break;
978+ } else {
979+ dist = 0;
980+ }
981+ }
982+ }
983+ }
984+
985+ if(overlap) {
986+ for(uint32_t l = 0; l < interval->size(); l++) {
987+ interval->operator[](l) |= otherInterval->operator[](l);
988+ }
989+ rangesToRemove.insert(j);
990+ }
991+ }
992+ }
993+ for (auto i = rangesToRemove.rbegin(); i != rangesToRemove.rend(); ++i) {
994+ _intervals.erase(_intervals.begin() + *i);
995+ }
996 }
997 };
998 }
999
1000=== added file 'include/PetriEngine/Colored/PartitionBuilder.h'
1001--- include/PetriEngine/Colored/PartitionBuilder.h 1970-01-01 00:00:00 +0000
1002+++ include/PetriEngine/Colored/PartitionBuilder.h 2021-04-14 13:35:08 +0000
1003@@ -0,0 +1,49 @@
1004+#include "ColoredNetStructures.h"
1005+#include "EquivalenceClass.h"
1006+#include "IntervalGenerator.h"
1007+
1008+namespace PetriEngine {
1009+ namespace Colored {
1010+ class PartitionBuilder {
1011+ public:
1012+ 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);
1013+ ~PartitionBuilder() {}
1014+
1015+ //void initPartition();
1016+ void partitionNet();
1017+ void refinePartition();
1018+ void printPartion();
1019+ void assignColorMap(std::unordered_map<uint32_t, EquivalenceVec> &partition);
1020+
1021+ std::unordered_map<uint32_t, EquivalenceVec> getPartition(){
1022+ return _partition;
1023+ }
1024+ private:
1025+ std::vector<Transition> *_transitions;
1026+ std::unordered_map<uint32_t,std::vector<uint32_t>> *_placePostTransitionMap;
1027+ std::unordered_map<uint32_t,std::vector<uint32_t>> *_placePreTransitionMap;
1028+ std::unordered_map<uint32_t,bool> _inQueue;
1029+ std::vector<Place> *_places;
1030+ std::unordered_map<uint32_t, EquivalenceVec> _partition;
1031+ PetriEngine::IntervalGenerator intervalGenerator;
1032+ std::vector<uint32_t> _placeQueue;
1033+
1034+ bool splitPartition(EquivalenceVec equivalenceVec, uint32_t placeId);
1035+
1036+ void handleTransition(uint32_t transitionId, uint32_t postPlaceId);
1037+ void handleTransition(Transition *transitionId, uint32_t postPlaceId, Arc *postArc);
1038+
1039+ void handleLeafTransitions();
1040+
1041+ void addToQueue(uint32_t placeId);
1042+
1043+ std::vector<std::unordered_map<const Variable *, intervalTuple_t>> prepareVariables(
1044+ std::unordered_map<const Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMap,
1045+ EquivalenceClass *eqClass , Arc *postArc, uint32_t placeId);
1046+
1047+ bool findOverlap(EquivalenceVec equivalenceVec1, EquivalenceVec equivalenceVec2, uint32_t &overlap1, uint32_t &overlap2, EquivalenceClass &intersection);
1048+
1049+ uint32_t eqClassIdCounter = 0;
1050+ };
1051+ }
1052+}
1053\ No newline at end of file
1054
1055=== modified file 'include/PetriEngine/options.h'
1056--- include/PetriEngine/options.h 2021-04-07 08:50:10 +0000
1057+++ include/PetriEngine/options.h 2021-04-14 13:35:08 +0000
1058@@ -72,9 +72,11 @@
1059
1060 //CPN Specific options
1061 bool cpnOverApprox = false;
1062+ bool computeCFP = true;
1063+ bool computePartition = true;
1064 bool isCPN = false;
1065 uint32_t seed_offset = 0;
1066- int max_intervals = 250;
1067+ int max_intervals = 250; //0 disabled
1068 int max_intervals_reduced = 5;
1069
1070 size_t seed() { return ++seed_offset; }
1071
1072=== modified file 'include/PetriParse/PNMLParser.h'
1073--- include/PetriParse/PNMLParser.h 2021-02-18 12:01:45 +0000
1074+++ include/PetriParse/PNMLParser.h 2021-04-14 13:35:08 +0000
1075@@ -31,6 +31,7 @@
1076 #include "../PetriEngine/Colored/ColoredNetStructures.h"
1077 #include "../PetriEngine/Colored/Expressions.h"
1078 #include "../PetriEngine/Colored/Colors.h"
1079+#include "../PetriEngine/Colored/EquivalenceClass.h"
1080
1081 class PNMLParser {
1082
1083@@ -88,9 +89,9 @@
1084 PetriEngine::Colored::ColorExpression_ptr parseColorExpression(rapidxml::xml_node<>* element);
1085 PetriEngine::Colored::AllExpression_ptr parseAllExpression(rapidxml::xml_node<>* element);
1086 PetriEngine::Colored::ColorType* parseUserSort(rapidxml::xml_node<>* element);
1087- PetriEngine::Colored::NumberOfExpression_ptr parseNumberOfExpression(rapidxml::xml_node<>* element);
1088+ PetriEngine::Colored::ArcExpression_ptr parseNumberOfExpression(rapidxml::xml_node<>* element);
1089 void collectColorsInTuple(rapidxml::xml_node<>* element,std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>>& collectedColors);
1090- PetriEngine::Colored::ArcExpression_ptr constructAddExpressionFromTupleExpression(rapidxml::xml_node<>* element,std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> collectedColors);
1091+ PetriEngine::Colored::ArcExpression_ptr constructAddExpressionFromTupleExpression(rapidxml::xml_node<>* element,std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> collectedColors, uint32_t numberof);
1092 void parseTransportArc(rapidxml::xml_node<>* element);
1093 void parseValue(rapidxml::xml_node<>* element, std::string& text);
1094 uint32_t parseNumberConstant(rapidxml::xml_node<>* element);
1095@@ -111,4 +112,4 @@
1096 std::vector<Query> queries;
1097 };
1098
1099-#endif // PNMLPARSER_H
1100+#endif // PNMLPARSER_H
1101\ No newline at end of file
1102
1103=== modified file 'src/PetriEngine/Colored/BindingGenerator.cpp'
1104--- src/PetriEngine/Colored/BindingGenerator.cpp 2021-03-24 10:39:01 +0000
1105+++ src/PetriEngine/Colored/BindingGenerator.cpp 2021-04-14 13:35:08 +0000
1106@@ -21,7 +21,109 @@
1107
1108 namespace PetriEngine {
1109
1110- FixpointBindingGenerator::Iterator::Iterator(FixpointBindingGenerator* generator)
1111+ NaiveBindingGenerator::Iterator::Iterator(NaiveBindingGenerator* generator)
1112+ : _generator(generator)
1113+ {
1114+ }
1115+
1116+ bool NaiveBindingGenerator::Iterator::operator==(Iterator& other) {
1117+ return _generator == other._generator;
1118+ }
1119+
1120+ bool NaiveBindingGenerator::Iterator::operator!=(Iterator& other) {
1121+ return _generator != other._generator;
1122+ }
1123+
1124+ NaiveBindingGenerator::Iterator& NaiveBindingGenerator::Iterator::operator++() {
1125+ _generator->nextBinding();
1126+ if (_generator->isInitial()) _generator = nullptr;
1127+ return *this;
1128+ }
1129+
1130+ const Colored::ExpressionContext::BindingMap NaiveBindingGenerator::Iterator::operator++(int) {
1131+ auto prev = _generator->currentBinding();
1132+ ++*this;
1133+ return prev;
1134+ }
1135+
1136+ Colored::ExpressionContext::BindingMap& NaiveBindingGenerator::Iterator::operator*() {
1137+ return _generator->currentBinding();
1138+ }
1139+
1140+ NaiveBindingGenerator::NaiveBindingGenerator(Colored::Transition& transition,
1141+ ColorTypeMap& colorTypes)
1142+ : _colorTypes(colorTypes)
1143+ {
1144+ _expr = transition.guard;
1145+ std::set<const Colored::Variable*> variables;
1146+ if (_expr != nullptr) {
1147+ _expr->getVariables(variables);
1148+ }
1149+ for (auto arc : transition.input_arcs) {
1150+ assert(arc.expr != nullptr);
1151+ arc.expr->getVariables(variables);
1152+ }
1153+ for (auto arc : transition.output_arcs) {
1154+ assert(arc.expr != nullptr);
1155+ arc.expr->getVariables(variables);
1156+ }
1157+ for (auto var : variables) {
1158+ _bindings[var] = &var->colorType->operator[](0);
1159+ }
1160+
1161+ if (!eval())
1162+ nextBinding();
1163+ }
1164+
1165+ bool NaiveBindingGenerator::eval() {
1166+ if (_expr == nullptr)
1167+ return true;
1168+ Colored::EquivalenceVec placePartition;
1169+
1170+ Colored::ExpressionContext context {_bindings, _colorTypes, placePartition};
1171+ return _expr->eval(context);
1172+ }
1173+
1174+ Colored::ExpressionContext::BindingMap& NaiveBindingGenerator::nextBinding() {
1175+ bool test = false;
1176+ while (!test) {
1177+ for (auto& _binding : _bindings) {
1178+ _binding.second = &_binding.second->operator++();
1179+ if (_binding.second->getId() != 0) {
1180+ break;
1181+ }
1182+ }
1183+
1184+ if (isInitial())
1185+ break;
1186+
1187+ test = eval();
1188+ }
1189+ return _bindings;
1190+ }
1191+
1192+ Colored::ExpressionContext::BindingMap& NaiveBindingGenerator::currentBinding() {
1193+ return _bindings;
1194+ }
1195+
1196+ bool NaiveBindingGenerator::isInitial() const {
1197+ for (auto& b : _bindings) {
1198+ if (b.second->getId() != 0) return false;
1199+ }
1200+ return true;
1201+ }
1202+
1203+ NaiveBindingGenerator::Iterator NaiveBindingGenerator::begin() {
1204+ return {this};
1205+ }
1206+
1207+ NaiveBindingGenerator::Iterator NaiveBindingGenerator::end() {
1208+ return {nullptr};
1209+ }
1210+
1211+
1212+
1213+ FixpointBindingGenerator::Iterator::Iterator(FixpointBindingGenerator* generator)
1214 : _generator(generator)
1215 {
1216 }
1217@@ -78,6 +180,7 @@
1218 arc.expr->getVariables(variables);
1219 }
1220
1221+
1222 for (auto var : variables) {
1223 if(_transition.variableMaps.empty() || _transition.variableMaps[_nextIndex][var]._intervals.empty()){
1224 _noValidBindings = true;
1225@@ -96,7 +199,8 @@
1226 if (_expr == nullptr)
1227 return true;
1228
1229- Colored::ExpressionContext context {_bindings, _colorTypes};
1230+ Colored::EquivalenceVec placePartition;
1231+ Colored::ExpressionContext context {_bindings, _colorTypes, placePartition};
1232 return _expr->eval(context);
1233 }
1234
1235
1236=== modified file 'src/PetriEngine/Colored/CMakeLists.txt'
1237--- src/PetriEngine/Colored/CMakeLists.txt 2021-03-15 12:10:13 +0000
1238+++ src/PetriEngine/Colored/CMakeLists.txt 2021-04-14 13:35:08 +0000
1239@@ -4,5 +4,7 @@
1240 Colors.cpp
1241 Multiset.cpp
1242 BindingGenerator.cpp
1243+PartitionBuilder.cpp
1244+EquivalenceClass.cpp
1245 GuardRestrictor.cpp)
1246 add_dependencies(Colored rapidxml-ext ptrie-ext glpk-ext)
1247
1248=== modified file 'src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp'
1249--- src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp 2021-03-24 10:39:01 +0000
1250+++ src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp 2021-04-14 13:35:08 +0000
1251@@ -49,7 +49,7 @@
1252 }
1253
1254 Colored::intervalTuple_t placeConstraints;
1255- Colored::ColorFixpoint colorFixpoint = {placeConstraints, !tokens.empty(), (uint32_t) type->productSize()};
1256+ Colored::ColorFixpoint colorFixpoint = {placeConstraints, !tokens.empty()};
1257
1258 if(tokens.size() == type->size()){
1259 colorFixpoint.constraints.addInterval(type->getFullInterval());
1260@@ -120,7 +120,7 @@
1261 assert(t < _transitions.size());
1262 assert(p < _places.size());
1263
1264- if (input) _placePostTransitionMap[p].emplace_back(t);
1265+ input? _placePostTransitionMap[p].emplace_back(t): _placePreTransitionMap[p].emplace_back(t);
1266
1267 Colored::Arc arc;
1268 arc.place = p;
1269@@ -157,19 +157,30 @@
1270 }
1271 }
1272
1273+ void ColoredPetriNetBuilder::computePartition(){
1274+ auto partitionStart = std::chrono::high_resolution_clock::now();
1275+ Colored::PartitionBuilder pBuilder = Colored::PartitionBuilder(&_transitions, &_places, &_placePostTransitionMap, &_placePreTransitionMap);
1276+ pBuilder.partitionNet();
1277+ //pBuilder.printPartion();
1278+ _partition = pBuilder.getPartition();
1279+ pBuilder.assignColorMap(_partition);
1280+ _partitionComputed = true;
1281+ auto partitionEnd = std::chrono::high_resolution_clock::now();
1282+ _partitionTimer = (std::chrono::duration_cast<std::chrono::microseconds>(partitionEnd - partitionStart).count())*0.000001;
1283+ }
1284+
1285 void ColoredPetriNetBuilder::computePlaceColorFixpoint(uint32_t maxIntervals, uint32_t maxIntervalsReduced, int32_t timeout) {
1286 //Start timers for timing color fixpoint creation and max interval reduction steps
1287 auto start = std::chrono::high_resolution_clock::now();
1288 std::chrono::_V2::system_clock::time_point end = std::chrono::high_resolution_clock::now();
1289 auto reduceTimer = std::chrono::high_resolution_clock::now();
1290 while(!_placeFixpointQueue.empty()){
1291- uint32_t currentPlaceId = _placeFixpointQueue.back();
1292 //Reduce max interval once timeout passes
1293- if(timeout > 0 && std::chrono::duration_cast<std::chrono::seconds>(end - reduceTimer).count() >= timeout){
1294+ if(maxIntervals > maxIntervalsReduced && timeout > 0 && std::chrono::duration_cast<std::chrono::seconds>(end - reduceTimer).count() >= timeout){
1295 maxIntervals = maxIntervalsReduced;
1296- reduceTimer = std::chrono::high_resolution_clock::now();
1297 }
1298
1299+ uint32_t currentPlaceId = _placeFixpointQueue.back();
1300 _placeFixpointQueue.pop_back();
1301 _placeColorFixpoints[currentPlaceId].inQueue = false;
1302 std::vector<uint32_t> connectedTransitions = _placePostTransitionMap[currentPlaceId];
1303@@ -195,6 +206,7 @@
1304 end = std::chrono::high_resolution_clock::now();
1305 }
1306
1307+ _fixpointDone = true;
1308 _fixPointCreationTime = (std::chrono::duration_cast<std::chrono::microseconds>(end - start).count())*0.000001;
1309
1310 //printPlaceTable();
1311@@ -216,11 +228,49 @@
1312 return res;
1313 }
1314
1315+ void ColoredPetriNetBuilder::createPartionVarmaps(){
1316+ for(uint32_t transitionId = 0; transitionId < _transitions.size(); transitionId++){
1317+ Colored::Transition &transition = _transitions[transitionId];
1318+ std::set<const Colored::Variable *> variables;
1319+ _arcIntervals[transitionId] = setupTransitionVars(transition);
1320+
1321+ for(auto inArc : transition.input_arcs){
1322+ Colored::ArcIntervals& arcInterval = _arcIntervals[transitionId][inArc.place];
1323+ uint32_t index = 0;
1324+ arcInterval._intervalTupleVec.clear();
1325+ PetriEngine::Colored::ColorFixpoint cfp;
1326+
1327+ Colored::intervalTuple_t intervalTuple;
1328+ intervalTuple.addInterval(_places[inArc.place].type->getFullInterval());
1329+ cfp.constraints = intervalTuple;
1330+
1331+ inArc.expr->getArcIntervals(arcInterval, cfp, &index, 0);
1332+ _partition[inArc.place].applyPartition(arcInterval);
1333+ }
1334+
1335+ intervalGenerator.getVarIntervals(transition.variableMaps, _arcIntervals[transitionId]);
1336+ for(auto outArc : transition.output_arcs){
1337+ outArc.expr->getVariables(variables);
1338+ }
1339+ if(transition.guard != nullptr){
1340+ transition.guard->getVariables(variables);
1341+ }
1342+ for(auto var : variables){
1343+ for(auto &varmap : transition.variableMaps){
1344+ if(varmap.count(var) == 0){
1345+ Colored::intervalTuple_t intervalTuple;
1346+ intervalTuple.addInterval(var->colorType->getFullInterval());
1347+ varmap[var] = intervalTuple;
1348+ }
1349+ }
1350+ }
1351+ }
1352+ }
1353+
1354 //Retrieve color intervals for the input arcs based on their places
1355 void ColoredPetriNetBuilder::getArcIntervals(Colored::Transition& transition, bool &transitionActivated, uint32_t max_intervals, uint32_t transitionId){
1356 for (auto arc : transition.input_arcs) {
1357- PetriEngine::Colored::ColorFixpoint& curCFP = _placeColorFixpoints[arc.place];
1358-
1359+ PetriEngine::Colored::ColorFixpoint& curCFP = _placeColorFixpoints[arc.place];
1360 curCFP.constraints.restrict(max_intervals);
1361 _maxIntervals = std::max(_maxIntervals, (uint32_t) curCFP.constraints.size());
1362
1363@@ -231,7 +281,11 @@
1364 if(!arc.expr->getArcIntervals(arcInterval, curCFP, &index, 0)){
1365 transitionActivated = false;
1366 return;
1367- }
1368+ }
1369+
1370+ if(_partitionComputed){
1371+ _partition[arc.place].applyPartition(arcInterval);
1372+ }
1373 }
1374 }
1375
1376@@ -256,11 +310,8 @@
1377
1378 //Retreive interval colors from the input arcs restricted by the transition guard
1379 void ColoredPetriNetBuilder::processInputArcs(Colored::Transition& transition, uint32_t currentPlaceId, uint32_t transitionId, bool &transitionActivated, uint32_t max_intervals) {
1380-
1381-
1382 getArcIntervals(transition, transitionActivated, max_intervals, transitionId);
1383
1384-
1385 if(!transitionActivated){
1386 return;
1387 }
1388@@ -298,12 +349,29 @@
1389 transitionHasVarOutArcs = true;
1390 }
1391
1392+ //Apply partitioning to unbound outgoing variables such that
1393+ // bindings are only created for colors used in the rest of the net
1394+ if(!_partition[arc.place].diagonal){
1395+ for(auto outVar : variables){
1396+ for(auto& varMap : transition.variableMaps){
1397+ if(varMap.count(outVar) == 0){
1398+ Colored::intervalTuple_t varIntervalTuple;
1399+ for(auto EqClass : _partition[arc.place]._equivalenceClasses){
1400+ varIntervalTuple.addInterval(EqClass._colorIntervals.back().getSingleColorInterval());
1401+ }
1402+ varMap[outVar] = varIntervalTuple;
1403+ }
1404+ }
1405+ }
1406+ }
1407+
1408 auto intervals = arc.expr->getOutputIntervals(transition.variableMaps);
1409 intervals.simplify();
1410
1411 for(auto& interval : intervals._intervals){
1412 placeFixpoint.constraints.addInterval(std::move(interval));
1413 }
1414+ placeFixpoint.constraints.simplify();
1415
1416 //Check if the place should be added to the queue
1417 if (!placeFixpoint.inQueue) {
1418@@ -326,8 +394,13 @@
1419 PetriNetBuilder& ColoredPetriNetBuilder::unfold() {
1420 if (_stripped) assert(false);
1421 if (_isColored && !_unfolded) {
1422+ std::cout << "Unfolding " << _fixpointDone << _partitionComputed << std::endl;
1423 auto start = std::chrono::high_resolution_clock::now();
1424
1425+ if(!_fixpointDone && _partitionComputed){
1426+ createPartionVarmaps();
1427+ }
1428+
1429 for (auto& transition : _transitions) {
1430 unfoldTransition(transition);
1431 }
1432@@ -335,6 +408,7 @@
1433 for (auto& place : _places) {
1434 handleOrphanPlace(place, unfoldedPlaceMap);
1435 }
1436+
1437 _unfolded = true;
1438 auto end = std::chrono::high_resolution_clock::now();
1439 _time = (std::chrono::duration_cast<std::chrono::microseconds>(end - start).count())*0.000001;
1440@@ -348,16 +422,14 @@
1441 //Ideally, orphan places should just be translated to a constant in the query
1442 void ColoredPetriNetBuilder::handleOrphanPlace(Colored::Place& place, std::unordered_map<std::string, uint32_t> unfoldedPlaceMap) {
1443 if(_ptplacenames.count(place.name) <= 0){
1444-
1445 std::string name = place.name + "_orphan";
1446 _ptBuilder.addPlace(name, place.marking.size(), 0.0, 0.0);
1447 _ptplacenames[place.name][0] = std::move(name);
1448 } else {
1449 uint32_t usedTokens = 0;
1450
1451- for(std::pair<const uint32_t, std::string> unfoldedPlace : _ptplacenames[place.name]){
1452+ for(std::pair<const uint32_t, std::string> unfoldedPlace : _ptplacenames[place.name]){
1453 auto unfoldedMarking = _ptBuilder.initMarking();
1454-
1455 auto unfoldedPlaceId = unfoldedPlaceMap[unfoldedPlace.second];
1456 usedTokens += unfoldedMarking[unfoldedPlaceId];
1457 }
1458@@ -372,50 +444,89 @@
1459 //++_nptplaces;
1460 }
1461
1462- void ColoredPetriNetBuilder::unfoldPlace(const Colored::Place* place, const PetriEngine::Colored::Color *color) {
1463+ void ColoredPetriNetBuilder::unfoldPlace(const Colored::Place* place, const PetriEngine::Colored::Color *color, uint32_t placeId, uint32_t id) {
1464+ size_t tokenSize = 0;
1465+ if(!_partitionComputed || _partition[placeId].diagonal){
1466+ tokenSize = place->marking[color];
1467+ }else {
1468+ for(auto colorEqClassPair : _partition[placeId].colorEQClassMap){
1469+ if(colorEqClassPair.second->_id == _partition[placeId].colorEQClassMap[color]->_id){
1470+ tokenSize += place->marking[colorEqClassPair.first];
1471+ }
1472+ }
1473+ }
1474+
1475 std::string name = place->name + "_" + std::to_string(color->getId());
1476- _ptBuilder.addPlace(name, place->marking[color], 0.0, 0.0);
1477- _ptplacenames[place->name][color->getId()] = std::move(name);
1478- ++_nptplaces;
1479+ _ptBuilder.addPlace(name, tokenSize, 0.0, 0.0);
1480+ _ptplacenames[place->name][id] = std::move(name);
1481+ ++_nptplaces;
1482 }
1483
1484 void ColoredPetriNetBuilder::unfoldTransition(Colored::Transition& transition) {
1485- FixpointBindingGenerator gen(transition, _colors);
1486- size_t i = 0;
1487- for (auto b : gen) {
1488- std::string name = transition.name + "_" + std::to_string(i++);
1489- _ptBuilder.addTransition(name, 0.0, 0.0);
1490- _pttransitionnames[transition.name].push_back(name);
1491- ++_npttransitions;
1492- for (auto& arc : transition.input_arcs) {
1493- unfoldArc(arc, b, name, true );
1494- }
1495- for (auto& arc : transition.output_arcs) {
1496- unfoldArc(arc, b, name, false);
1497- }
1498- }
1499+ if(_fixpointDone || _partitionComputed){
1500+ FixpointBindingGenerator gen(transition, _colors);
1501+ size_t i = 0;
1502+
1503+ for (auto b : gen) {
1504+ std::string name = transition.name + "_" + std::to_string(i++);
1505+ _ptBuilder.addTransition(name, 0.0, 0.0);
1506+ _pttransitionnames[transition.name].push_back(name);
1507+ ++_npttransitions;
1508+
1509+ for (auto& arc : transition.input_arcs) {
1510+ unfoldArc(arc, b, name );
1511+ }
1512+ for (auto& arc : transition.output_arcs) {
1513+ unfoldArc(arc, b, name);
1514+ }
1515+ }
1516+ } else {
1517+ std::cout << "Entered naive" << std::endl;
1518+ NaiveBindingGenerator gen(transition, _colors);
1519+ size_t i = 0;
1520+ for (auto b : gen) {
1521+ std::string name = transition.name + "_" + std::to_string(i++);
1522+ _ptBuilder.addTransition(name, 0.0, 0.0);
1523+ _pttransitionnames[transition.name].push_back(name);
1524+ ++_npttransitions;
1525+ for (auto& arc : transition.input_arcs) {
1526+ unfoldArc(arc, b, name);
1527+ }
1528+ for (auto& arc : transition.output_arcs) {
1529+ unfoldArc(arc, b, name);
1530+ }
1531+ }
1532+ }
1533 }
1534
1535- void ColoredPetriNetBuilder::unfoldArc(Colored::Arc& arc, Colored::ExpressionContext::BindingMap& binding, std::string& tName, bool input) {
1536- Colored::ExpressionContext context {binding, _colors};
1537+ void ColoredPetriNetBuilder::unfoldArc(Colored::Arc& arc, Colored::ExpressionContext::BindingMap& binding, std::string& tName) {
1538+ Colored::ExpressionContext context {binding, _colors, _partition[arc.place]};
1539 auto ms = arc.expr->eval(context);
1540-
1541+
1542 for (const auto& color : ms) {
1543 if (color.second == 0) {
1544 continue;
1545 }
1546+
1547 const PetriEngine::Colored::Place& place = _places[arc.place];
1548- const std::string& pName = _ptplacenames[place.name][color.first->getId()];
1549- if (pName.empty()) {
1550- unfoldPlace(&place, color.first);
1551- }
1552+ uint32_t id;
1553+ if(!_partitionComputed || _partition[arc.place].diagonal){
1554+ id = color.first->getId();
1555+ } else {
1556+ id = _partition[arc.place].colorEQClassMap[color.first]->_id;
1557+ }
1558+ const std::string& pName = _ptplacenames[place.name][id];
1559+ if (pName.empty()) {
1560+ unfoldPlace(&place, color.first, arc.place, id);
1561+ }
1562+
1563 if (arc.input) {
1564 _ptBuilder.addInputArc(pName, tName, false, color.second);
1565 } else {
1566 _ptBuilder.addOutputArc(tName, pName, color.second);
1567 }
1568 ++_nptarcs;
1569- }
1570+ }
1571 }
1572
1573 //----------------------- Strip Colors -----------------------//
1574
1575=== added file 'src/PetriEngine/Colored/EquivalenceClass.cpp'
1576--- src/PetriEngine/Colored/EquivalenceClass.cpp 1970-01-01 00:00:00 +0000
1577+++ src/PetriEngine/Colored/EquivalenceClass.cpp 2021-04-14 13:35:08 +0000
1578@@ -0,0 +1,116 @@
1579+#include "PetriEngine/Colored/EquivalenceClass.h"
1580+
1581+namespace PetriEngine {
1582+ namespace Colored {
1583+
1584+ uint32_t EquivalenceClass::idCounter = 0;
1585+
1586+ EquivalenceClass::EquivalenceClass() : _id(++idCounter){
1587+ }
1588+ EquivalenceClass::EquivalenceClass(ColorType *colorType)
1589+ : _id(++idCounter), _colorType(colorType){
1590+ }
1591+ EquivalenceClass::EquivalenceClass(ColorType *colorType, intervalTuple_t colorIntervals)
1592+ : _id(++idCounter), _colorType(colorType), _colorIntervals(colorIntervals){
1593+ }
1594+
1595+ EquivalenceClass EquivalenceClass::intersect(EquivalenceClass other){
1596+ EquivalenceClass result = EquivalenceClass();
1597+
1598+ if(_colorType != other._colorType){
1599+ return result;
1600+ }
1601+ result._colorType = _colorType;
1602+
1603+ for(auto interval : _colorIntervals._intervals){
1604+ for(auto otherInterval : other._colorIntervals._intervals){
1605+ auto overlappingInterval = interval.getOverlap(otherInterval);
1606+ if(overlappingInterval.isSound()){
1607+ result._colorIntervals.addInterval(overlappingInterval);
1608+ }
1609+ }
1610+ }
1611+ return result;
1612+ }
1613+
1614+
1615+ EquivalenceClass EquivalenceClass::subtract(EquivalenceClass other, bool print){
1616+ EquivalenceClass result = EquivalenceClass();
1617+ if(_colorType != other._colorType){
1618+ return result;
1619+ }
1620+ result._colorType = _colorType;
1621+ intervalTuple_t resIntervals;
1622+ for(auto interval : _colorIntervals._intervals){
1623+ intervalTuple_t intervalSubRes;
1624+ for(auto otherInterval : other._colorIntervals._intervals){
1625+ auto subtractedIntervals = interval.getSubtracted(otherInterval, _colorType->size());
1626+ if(print){
1627+ std::cout << interval.toString() << " - " << otherInterval.toString() << " = " << std::endl;
1628+ for(auto subinter : subtractedIntervals){
1629+ std::cout << subinter.toString() << std::endl;
1630+ }
1631+ std::cout << "~~~~~~" << std::endl;
1632+ }
1633+
1634+
1635+ if(subtractedIntervals.empty() || subtractedIntervals[0].size() == 0){
1636+ intervalSubRes._intervals.clear();
1637+ break;
1638+ }
1639+
1640+ if(intervalSubRes._intervals.empty()){
1641+ intervalSubRes._intervals = subtractedIntervals;
1642+ } else {
1643+ intervalTuple_t newIntervals;
1644+ for(auto newInterval : subtractedIntervals){
1645+ for(auto interval : intervalSubRes._intervals){
1646+ auto intersection = interval.getOverlap(newInterval);
1647+ if(intersection.isSound()){
1648+ newIntervals.addInterval(intersection);
1649+ }
1650+ }
1651+ }
1652+ intervalSubRes = std::move(newIntervals);
1653+ // for(auto newInterval : subtractedIntervals){
1654+ // resIntervals.addInterval(newInterval);
1655+ // }
1656+ }
1657+ if(print){
1658+ std::cout << "intermediate res is now: " << intervalSubRes.toString() << std::endl;
1659+ }
1660+ }
1661+ if(print) std::cout << "Done looping inner" << std::endl;
1662+ for(auto interval : intervalSubRes._intervals){
1663+ resIntervals.addInterval(interval);
1664+ }
1665+ if(print){
1666+ std::cout << "Subtract res is now: " << resIntervals.toString() << std::endl;
1667+ }
1668+
1669+ }
1670+ result._colorIntervals = resIntervals;
1671+ return result;
1672+ }
1673+
1674+ bool EquivalenceClass::containsColor(std::vector<uint32_t> ids){
1675+ interval_t interval;
1676+ for(auto id : ids){
1677+ interval.addRange(id,id);
1678+ }
1679+ return _colorIntervals.contains(interval);
1680+ }
1681+
1682+ size_t EquivalenceClass::size(){
1683+ size_t result = 0;
1684+ for(auto interval : _colorIntervals._intervals){
1685+ size_t intervalSize = 1;
1686+ for(auto range : interval._ranges){
1687+ intervalSize *= range.size();
1688+ }
1689+ result += intervalSize;
1690+ }
1691+ return result;
1692+ }
1693+ }
1694+}
1695\ No newline at end of file
1696
1697=== modified file 'src/PetriEngine/Colored/GuardRestrictor.cpp'
1698--- src/PetriEngine/Colored/GuardRestrictor.cpp 2021-03-24 10:39:01 +0000
1699+++ src/PetriEngine/Colored/GuardRestrictor.cpp 2021-04-14 13:35:08 +0000
1700@@ -85,17 +85,16 @@
1701 }
1702 }
1703
1704- void GuardRestrictor::expandIntervalVec(std::unordered_map<const Variable *, intervalTuple_t> *varMap,
1705- std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *mainVarModifierMap,
1706- std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *otherVarModifierMap,
1707- std::unordered_map<uint32_t, const Variable *> *varPositions,
1708- std::unordered_map<uint32_t, const Color*> *constantMap,
1709- const Variable *otherVar,
1710- std::vector<interval_t> &intervalVec, size_t targetSize, uint32_t index){
1711-
1712+ void GuardRestrictor::expandIntervalVec(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t> varMap,
1713+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *mainVarModifierMap,
1714+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *otherVarModifierMap,
1715+ std::unordered_map<uint32_t, const Colored::Variable *> *varPositions,
1716+ std::unordered_map<uint32_t, const Color*> *constantMap,
1717+ const Colored::Variable *otherVar,
1718+ std::vector<Colored::interval_t> &intervalVec, size_t targetSize, uint32_t index){
1719 while(intervalVec.size() < targetSize){
1720 if(varPositions->count(index)){
1721- auto rightTupleInterval = varMap->operator[](varPositions->operator[](index));
1722+ auto rightTupleInterval = varMap[varPositions->operator[](index)];
1723 int32_t rightVarMod = getVarModifier(&mainVarModifierMap->operator[](varPositions->operator[](index)).back(), index);
1724 rightTupleInterval.applyModifier(-rightVarMod, varPositions->operator[](index)->colorType->getConstituentsSizes());
1725 intervalVec.insert(intervalVec.end(), rightTupleInterval._intervals.begin(), rightTupleInterval._intervals.end());
1726@@ -117,212 +116,253 @@
1727 }
1728 }
1729
1730- void GuardRestrictor::restrictDiagonal(std::vector<std::unordered_map<const Variable *, intervalTuple_t>> *variableMap,
1731- std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
1732- std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
1733- std::unordered_map<uint32_t, const Variable *> *varPositionsL,
1734- std::unordered_map<uint32_t, const Variable *> *varPositionsR,
1735- std::unordered_map<uint32_t, const Color*> *constantMapL,
1736- std::unordered_map<uint32_t, const Color*> *constantMapR,
1737- bool lessthan, bool strict) {
1738-
1739- for(auto& varMap : *variableMap){
1740- for(auto varPositionPair : *varPositionsL){
1741- uint32_t index = varPositionPair.first;
1742- if(varPositionsR->count(index)){
1743- if(varMap.count(varPositionPair.second) == 0){
1744- std::cout << "Unable to find left var " << varPositionPair.second->name << std::endl;
1745- }
1746- if(varMap.count(varPositionsR->operator[](index)) == 0){
1747- std::cout << "Unable to find right var " << varPositionsR->operator[](index)->name << std::endl;
1748- }
1749- auto leftTupleInterval = &varMap[varPositionPair.second];
1750- auto rightTupleInterval = &varMap[varPositionsR->operator[](index)];
1751- int32_t leftVarModifier = getVarModifier(&varModifierMapL->operator[](varPositionPair.second).back(), index);
1752- int32_t rightVarModifier = getVarModifier(&varModifierMapR->operator[](varPositionsR->operator[](index)).back(), index);
1753-
1754- auto leftIds = leftTupleInterval->getLowerIds(-leftVarModifier, varPositionPair.second->colorType->getConstituentsSizes());
1755- auto rightIds = rightTupleInterval->getUpperIds(-rightVarModifier, varPositionsR->operator[](index)->colorType->getConstituentsSizes());
1756-
1757- //comparing vars of same size
1758- if(varPositionPair.second->colorType->productSize() == varPositionsR->operator[](index)->colorType->productSize()){
1759- if(lessthan){
1760- leftTupleInterval->constrainUpper(rightIds, strict);
1761- rightTupleInterval->constrainLower(leftIds, strict);
1762- } else {
1763- leftTupleInterval->constrainLower(rightIds, strict);
1764- rightTupleInterval->constrainUpper(leftIds, strict);
1765- }
1766-
1767- } else if(varPositionPair.second->colorType->productSize() > varPositionsR->operator[](index)->colorType->productSize()){
1768- std::vector<uint32_t> leftLowerVec(leftIds.begin(), leftIds.begin() + rightTupleInterval->tupleSize());
1769-
1770- auto idVec = rightIds;
1771-
1772- expandIdVec(&varMap, varModifierMapR, varModifierMapL, varPositionsR, constantMapR, varPositionPair.second, idVec, leftTupleInterval->tupleSize(), index + varPositionsR->operator[](index)->colorType->productSize());
1773-
1774- if(lessthan){
1775- leftTupleInterval->constrainUpper(idVec, strict);
1776- rightTupleInterval->constrainLower(leftLowerVec, strict);
1777- } else {
1778- leftTupleInterval->constrainLower(idVec, strict);
1779- rightTupleInterval->constrainUpper(leftLowerVec, strict);
1780- }
1781-
1782- } else {
1783- std::vector<uint32_t> rightUpperVec(rightIds.begin(), rightIds.begin() + leftTupleInterval->tupleSize());
1784-
1785- auto idVec = leftIds;
1786- expandIdVec(&varMap, varModifierMapR, varModifierMapL, varPositionsL, constantMapL, varPositionsR->operator[](index), idVec, rightTupleInterval->tupleSize(), index + varPositionsL->operator[](index)->colorType->productSize());
1787-
1788- if(lessthan){
1789- leftTupleInterval->constrainUpper(rightUpperVec, strict);
1790- rightTupleInterval->constrainLower(idVec, strict);
1791- } else {
1792- leftTupleInterval->constrainLower(rightUpperVec, strict);
1793- rightTupleInterval->constrainUpper(idVec, strict);
1794- }
1795- }
1796- } else {
1797- auto rightColor = constantMapR->operator[](index);
1798- auto leftTupleInterval = &varMap[varPositionPair.second];
1799- std::vector<uint32_t> idVec;
1800- rightColor->getTupleId(&idVec);
1801-
1802- expandIdVec(&varMap, varModifierMapR, varModifierMapL, varPositionsR, constantMapR, varPositionPair.second, idVec, leftTupleInterval->tupleSize(), index + idVec.size());
1803-
1804- if(lessthan){
1805- leftTupleInterval->constrainUpper(idVec, strict);
1806- } else {
1807- leftTupleInterval->constrainLower(idVec, strict);
1808- }
1809- }
1810- }
1811-
1812- for(auto varPositionPair : *varPositionsR){
1813- uint32_t index = varPositionPair.first;
1814-
1815- if(constantMapL->count(index)){
1816- auto leftColor = constantMapL->operator[](index);
1817- auto rightTupleInterval = &varMap[varPositionPair.second];
1818- std::vector<uint32_t> idVec;
1819- leftColor->getTupleId(&idVec);
1820-
1821- expandIdVec(&varMap, varModifierMapR, varModifierMapL, varPositionsL, constantMapL, varPositionsR->operator[](index), idVec, rightTupleInterval->tupleSize(), index + idVec.size());
1822-
1823- if(lessthan){
1824- rightTupleInterval->constrainUpper(idVec, strict);
1825- } else {
1826- rightTupleInterval->constrainLower(idVec, strict);
1827- }
1828- }
1829- }
1830- }
1831- }
1832-
1833- void GuardRestrictor::restrictEquality(std::vector<std::unordered_map<const Variable *, intervalTuple_t>> *variableMap,
1834- std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
1835- std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
1836- std::unordered_map<uint32_t, const Variable *> *varPositionsL,
1837- std::unordered_map<uint32_t, const Variable *> *varPositionsR,
1838- std::unordered_map<uint32_t, const Color*> *constantMapL,
1839- std::unordered_map<uint32_t, const Color*> *constantMapR) {
1840-
1841- for(auto& varMap : *variableMap){
1842- for(auto varPositionPair : *varPositionsL){
1843- uint32_t index = varPositionPair.first;
1844- if(varPositionsR->count(index)){
1845- auto leftTupleIntervalVal = varMap[varPositionPair.second];
1846- auto rightTupleIntervalVal = varMap[varPositionsR->operator[](index)];
1847- auto leftTupleInterval = &varMap[varPositionPair.second];
1848- auto rightTupleInterval = &varMap[varPositionsR->operator[](index)];
1849- int32_t leftVarModifier = getVarModifier(&varModifierMapL->operator[](varPositionPair.second).back(), index);
1850- int32_t rightVarModifier = getVarModifier(&varModifierMapR->operator[](varPositionsR->operator[](index)).back(), index);
1851-
1852- leftTupleIntervalVal.applyModifier(-leftVarModifier, varPositionPair.second->colorType->getConstituentsSizes());
1853- rightTupleIntervalVal.applyModifier(-rightVarModifier, varPositionsR->operator[](index)->colorType->getConstituentsSizes());
1854- //comparing vars of same size
1855- if(varPositionPair.second->colorType->productSize() == varPositionsR->operator[](index)->colorType->productSize()){
1856- intervalTuple_t newIntervalTuple = getIntervalOverlap(&leftTupleIntervalVal._intervals, &rightTupleIntervalVal._intervals);
1857-
1858- *leftTupleInterval = newIntervalTuple;
1859- *rightTupleInterval = newIntervalTuple;
1860- leftTupleInterval->applyModifier(leftVarModifier, varPositionPair.second->colorType->getConstituentsSizes());
1861- rightTupleInterval->applyModifier(rightVarModifier, varPositionsR->operator[](index)->colorType->getConstituentsSizes());
1862- } else if(varPositionPair.second->colorType->productSize() > varPositionsR->operator[](index)->colorType->productSize()){
1863- std::vector<interval_t> resizedLeftIntervals = leftTupleIntervalVal.shrinkIntervals(varPositionsR->operator[](index)->colorType->productSize());
1864- auto intervalVec = rightTupleIntervalVal._intervals;
1865-
1866- expandIntervalVec(&varMap, varModifierMapR, varModifierMapL, varPositionsR, constantMapR, varPositionPair.second, intervalVec, leftTupleInterval->tupleSize(), index + varPositionsR->operator[](index)->colorType->productSize());
1867-
1868- intervalTuple_t newIntervalTupleR = getIntervalOverlap(&rightTupleIntervalVal._intervals, &resizedLeftIntervals);
1869- intervalTuple_t newIntervalTupleL = getIntervalOverlap(&leftTupleIntervalVal._intervals, &intervalVec);
1870-
1871- newIntervalTupleL.applyModifier(leftVarModifier, varPositionPair.second->colorType->getConstituentsSizes());
1872- newIntervalTupleR.applyModifier(rightVarModifier, varPositionsR->operator[](index)->colorType->getConstituentsSizes());
1873-
1874- *leftTupleInterval = newIntervalTupleL;
1875- *rightTupleInterval = newIntervalTupleR;
1876- } else {
1877- std::vector<interval_t> resizedRightIntervals = rightTupleIntervalVal.shrinkIntervals(varPositionsL->operator[](index)->colorType->productSize());
1878- auto intervalVec = leftTupleIntervalVal._intervals;
1879-
1880- expandIntervalVec(&varMap, varModifierMapR, varModifierMapL, varPositionsL, constantMapL, varPositionsR->operator[](index), intervalVec, rightTupleInterval->tupleSize(), index + varPositionsL->operator[](index)->colorType->productSize());
1881-
1882- intervalTuple_t newIntervalTupleL = getIntervalOverlap(&leftTupleIntervalVal._intervals, &resizedRightIntervals);
1883- intervalTuple_t newIntervalTupleR = getIntervalOverlap(&rightTupleIntervalVal._intervals, &intervalVec);
1884-
1885- newIntervalTupleL.applyModifier(leftVarModifier, varPositionPair.second->colorType->getConstituentsSizes());
1886- newIntervalTupleR.applyModifier(rightVarModifier, varPositionsR->operator[](index)->colorType->getConstituentsSizes());
1887-
1888- *leftTupleInterval = newIntervalTupleL;
1889- *rightTupleInterval = newIntervalTupleR;
1890- }
1891- } else {
1892- auto rightColor = constantMapR->operator[](index);
1893- auto leftTupleInterval = &varMap[varPositionPair.second];
1894- std::vector<uint32_t> idVec;
1895- rightColor->getTupleId(&idVec);
1896- int32_t leftVarModifier = getVarModifier(&varModifierMapL->operator[](varPositionPair.second).back(), index);
1897-
1898- std::vector<interval_t> intervals;
1899- intervals.push_back(getIntervalFromIds(&idVec, varPositionPair.second->colorType->size(), leftVarModifier));
1900-
1901- expandIntervalVec(&varMap, varModifierMapR, varModifierMapL, varPositionsR, constantMapR, varPositionPair.second, intervals, leftTupleInterval->tupleSize(), index + idVec.size());
1902-
1903- intervalTuple_t newIntervalTupleL = getIntervalOverlap(&leftTupleInterval->_intervals, &intervals);
1904- *leftTupleInterval = newIntervalTupleL;
1905- }
1906- }
1907-
1908- for(auto varPositionPair : *varPositionsR){
1909- uint32_t index = varPositionPair.first;
1910-
1911- if(constantMapL->count(index)){
1912- auto leftColor = constantMapL->operator[](index);
1913- auto rightTupleInterval = &varMap[varPositionPair.second];
1914- std::vector<uint32_t> idVec;
1915- leftColor->getTupleId(&idVec);
1916- int32_t rightVarModifier = getVarModifier(&varModifierMapR->operator[](varPositionPair.second).back(), index);
1917-
1918- std::vector<interval_t> intervals;
1919- intervals.push_back(getIntervalFromIds(&idVec, varPositionPair.second->colorType->size(), rightVarModifier));
1920-
1921- expandIntervalVec(&varMap, varModifierMapR, varModifierMapL, varPositionsL, constantMapL, varPositionsR->operator[](index), intervals, rightTupleInterval->tupleSize(), index + idVec.size());
1922-
1923- intervalTuple_t newIntervalTupleR = getIntervalOverlap(&rightTupleInterval->_intervals, &intervals);
1924- *rightTupleInterval = newIntervalTupleR;
1925- }
1926- }
1927- }
1928- }
1929-
1930- intervalTuple_t GuardRestrictor::shiftIntervals(std::vector<const ColorType *> *colortypes, intervalTuple_t *intervals, int32_t modifier, uint32_t ctSizeBefore) const {
1931- intervalTuple_t newIntervals;
1932-
1933+ void GuardRestrictor::restrictByConstant(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
1934+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *mainVarModifierMap,
1935+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *otherVarModifierMap,
1936+ std::unordered_map<uint32_t, const Colored::Variable *> *varPositions,
1937+ std::unordered_map<uint32_t, const Color*> *constantMap,
1938+ const Colored::Variable *var,
1939+ const Colored::Variable *otherVar,
1940+ uint32_t index, bool lessthan, bool strict){
1941+ for(auto& varMap : variableMap){
1942+ auto leftColor = constantMap->operator[](index);
1943+ auto rightTupleInterval = &varMap[var];
1944+ std::vector<uint32_t> idVec;
1945+ leftColor->getTupleId(&idVec);
1946+
1947+ expandIdVec(&varMap, mainVarModifierMap, otherVarModifierMap, varPositions, constantMap, otherVar, idVec, rightTupleInterval->tupleSize(), index + idVec.size());
1948+
1949+ if(lessthan){
1950+ rightTupleInterval->constrainUpper(idVec, strict);
1951+ } else {
1952+ rightTupleInterval->constrainLower(idVec, strict);
1953+ }
1954+ }
1955+ }
1956+
1957+ void GuardRestrictor::restrictEqByConstant(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
1958+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *mainVarModifierMap,
1959+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *otherVarModifierMap,
1960+ std::unordered_map<uint32_t, const Colored::Variable *> *varPositions,
1961+ std::unordered_map<uint32_t, const Color*> *constantMap,
1962+ const Colored::Variable *var,
1963+ uint32_t index){
1964+ for(auto& varMap : variableMap){
1965+ auto color = constantMap->operator[](index);
1966+ auto tupleInterval = &varMap[var];
1967+ std::vector<uint32_t> idVec;
1968+ color->getTupleId(&idVec);
1969+ int32_t varModifier = getVarModifier(&otherVarModifierMap->operator[](var).back(), index);
1970+
1971+ std::vector<Colored::interval_t> intervals;
1972+ intervals.push_back(getIntervalFromIds(&idVec, var->colorType->size(), varModifier));
1973+
1974+ expandIntervalVec(varMap, mainVarModifierMap, otherVarModifierMap, varPositions, constantMap, var, intervals, tupleInterval->tupleSize(), index + idVec.size());
1975+
1976+ Colored::intervalTuple_t newIntervalTupleL = getIntervalOverlap(&tupleInterval->_intervals, &intervals);
1977+ *tupleInterval = newIntervalTupleL;
1978+ }
1979+ }
1980+
1981+ void GuardRestrictor::restrictDiagonal(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
1982+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
1983+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
1984+ std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsL,
1985+ std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsR,
1986+ std::unordered_map<uint32_t, const Color*> *constantMapL,
1987+ std::unordered_map<uint32_t, const Color*> *constantMapR,
1988+ std::set<const Colored::Variable*> &diagonalVars,
1989+ const Colored::Variable *var,
1990+ uint32_t index, bool lessthan, bool strict){
1991+
1992+ diagonalVars.insert(var);
1993+ diagonalVars.insert(varPositionsR->operator[](index));
1994+
1995+ for(auto& varMap : variableMap){
1996+ if(varMap.count(var) == 0){
1997+ std::cout << "Unable to find left var " << var->name << std::endl;
1998+ }
1999+ if(varMap.count(varPositionsR->operator[](index)) == 0){
2000+ std::cout << "Unable to find right var " << varPositionsR->operator[](index)->name << std::endl;
2001+ }
2002+
2003+ auto leftTupleInterval = &varMap[var];
2004+ auto rightTupleInterval = &varMap[varPositionsR->operator[](index)];
2005+ int32_t leftVarModifier = getVarModifier(&varModifierMapL->operator[](var).back(), index);
2006+ int32_t rightVarModifier = getVarModifier(&varModifierMapR->operator[](varPositionsR->operator[](index)).back(), index);
2007+
2008+ auto leftIds = leftTupleInterval->getLowerIds(-leftVarModifier, var->colorType->getConstituentsSizes());
2009+ auto rightIds = rightTupleInterval->getUpperIds(-rightVarModifier, varPositionsR->operator[](index)->colorType->getConstituentsSizes());
2010+
2011+ //comparing vars of same size
2012+ if(var->colorType->productSize() == varPositionsR->operator[](index)->colorType->productSize()){
2013+ if(lessthan){
2014+ leftTupleInterval->constrainUpper(rightIds, strict);
2015+ rightTupleInterval->constrainLower(leftIds, strict);
2016+ } else {
2017+ leftTupleInterval->constrainLower(rightIds, strict);
2018+ rightTupleInterval->constrainUpper(leftIds, strict);
2019+ }
2020+ } else if(var->colorType->productSize() > varPositionsR->operator[](index)->colorType->productSize()){
2021+ std::vector<uint32_t> leftLowerVec(leftIds.begin(), leftIds.begin() + rightTupleInterval->tupleSize());
2022+
2023+ auto idVec = rightIds;
2024+
2025+ expandIdVec(&varMap, varModifierMapR, varModifierMapL, varPositionsR, constantMapR, var, idVec, leftTupleInterval->tupleSize(), index + varPositionsR->operator[](index)->colorType->productSize());
2026+
2027+ if(lessthan){
2028+ leftTupleInterval->constrainUpper(idVec, strict);
2029+ rightTupleInterval->constrainLower(leftLowerVec, strict);
2030+ } else {
2031+ leftTupleInterval->constrainLower(idVec, strict);
2032+ rightTupleInterval->constrainUpper(leftLowerVec, strict);
2033+ }
2034+
2035+ } else {
2036+ std::vector<uint32_t> rightUpperVec(rightIds.begin(), rightIds.begin() + leftTupleInterval->tupleSize());
2037+
2038+ auto idVec = leftIds;
2039+ expandIdVec(&varMap, varModifierMapR, varModifierMapL, varPositionsL, constantMapL, varPositionsR->operator[](index), idVec, rightTupleInterval->tupleSize(), index + varPositionsL->operator[](index)->colorType->productSize());
2040+
2041+ if(lessthan){
2042+ leftTupleInterval->constrainUpper(rightUpperVec, strict);
2043+ rightTupleInterval->constrainLower(idVec, strict);
2044+ } else {
2045+ leftTupleInterval->constrainLower(rightUpperVec, strict);
2046+ rightTupleInterval->constrainUpper(idVec, strict);
2047+ }
2048+ }
2049+ }
2050+ }
2051+
2052+ void GuardRestrictor::restrictEqDiagonal(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
2053+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
2054+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
2055+ std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsL,
2056+ std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsR,
2057+ std::unordered_map<uint32_t, const Color*> *constantMapL,
2058+ std::unordered_map<uint32_t, const Color*> *constantMapR,
2059+ std::set<const Colored::Variable*> &diagonalVars,
2060+ const Colored::Variable *var,
2061+ uint32_t index){
2062+ diagonalVars.insert(var);
2063+ diagonalVars.insert(varPositionsR->operator[](index));
2064+
2065+ for(auto& varMap : variableMap){
2066+ auto leftTupleIntervalVal = varMap[var];
2067+ auto rightTupleIntervalVal = varMap[varPositionsR->operator[](index)];
2068+ auto leftTupleInterval = &varMap[var];
2069+ auto rightTupleInterval = &varMap[varPositionsR->operator[](index)];
2070+ int32_t leftVarModifier = getVarModifier(&varModifierMapL->operator[](var).back(), index);
2071+ int32_t rightVarModifier = getVarModifier(&varModifierMapR->operator[](varPositionsR->operator[](index)).back(), index);
2072+
2073+ leftTupleIntervalVal.applyModifier(-leftVarModifier, var->colorType->getConstituentsSizes());
2074+ rightTupleIntervalVal.applyModifier(-rightVarModifier, varPositionsR->operator[](index)->colorType->getConstituentsSizes());
2075+ //comparing vars of same size
2076+ if(var->colorType->productSize() == varPositionsR->operator[](index)->colorType->productSize()){
2077+ Colored::intervalTuple_t newIntervalTuple = getIntervalOverlap(&leftTupleIntervalVal._intervals, &rightTupleIntervalVal._intervals);
2078+
2079+ *leftTupleInterval = newIntervalTuple;
2080+ *rightTupleInterval = newIntervalTuple;
2081+ leftTupleInterval->applyModifier(leftVarModifier, var->colorType->getConstituentsSizes());
2082+ rightTupleInterval->applyModifier(rightVarModifier, varPositionsR->operator[](index)->colorType->getConstituentsSizes());
2083+ } else if(var->colorType->productSize() > varPositionsR->operator[](index)->colorType->productSize()){
2084+ std::vector<Colored::interval_t> resizedLeftIntervals = leftTupleIntervalVal.shrinkIntervals(varPositionsR->operator[](index)->colorType->productSize());
2085+ auto intervalVec = rightTupleIntervalVal._intervals;
2086+
2087+ expandIntervalVec(varMap, varModifierMapR, varModifierMapL, varPositionsR, constantMapR, var, intervalVec, leftTupleInterval->tupleSize(), index + varPositionsR->operator[](index)->colorType->productSize());
2088+
2089+ Colored::intervalTuple_t newIntervalTupleR = getIntervalOverlap(&rightTupleIntervalVal._intervals, &resizedLeftIntervals);
2090+ Colored::intervalTuple_t newIntervalTupleL = getIntervalOverlap(&leftTupleIntervalVal._intervals, &intervalVec);
2091+
2092+ newIntervalTupleL.applyModifier(leftVarModifier, var->colorType->getConstituentsSizes());
2093+ newIntervalTupleR.applyModifier(rightVarModifier, varPositionsR->operator[](index)->colorType->getConstituentsSizes());
2094+
2095+ *leftTupleInterval = newIntervalTupleL;
2096+ *rightTupleInterval = newIntervalTupleR;
2097+ } else {
2098+ std::vector<Colored::interval_t> resizedRightIntervals = rightTupleIntervalVal.shrinkIntervals(varPositionsL->operator[](index)->colorType->productSize());
2099+ auto intervalVec = leftTupleIntervalVal._intervals;
2100+
2101+ expandIntervalVec(varMap, varModifierMapR, varModifierMapL, varPositionsL, constantMapL, varPositionsR->operator[](index), intervalVec, rightTupleInterval->tupleSize(), index + varPositionsL->operator[](index)->colorType->productSize());
2102+
2103+ Colored::intervalTuple_t newIntervalTupleL = getIntervalOverlap(&leftTupleIntervalVal._intervals, &resizedRightIntervals);
2104+ Colored::intervalTuple_t newIntervalTupleR = getIntervalOverlap(&rightTupleIntervalVal._intervals, &intervalVec);
2105+
2106+ newIntervalTupleL.applyModifier(leftVarModifier, var->colorType->getConstituentsSizes());
2107+ newIntervalTupleR.applyModifier(rightVarModifier, varPositionsR->operator[](index)->colorType->getConstituentsSizes());
2108+
2109+ *leftTupleInterval = newIntervalTupleL;
2110+ *rightTupleInterval = newIntervalTupleR;
2111+ }
2112+ }
2113+ }
2114+
2115+ void GuardRestrictor::restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
2116+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
2117+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
2118+ std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsL,
2119+ std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsR,
2120+ std::unordered_map<uint32_t, const Color*> *constantMapL,
2121+ std::unordered_map<uint32_t, const Color*> *constantMapR,
2122+ std::set<const Colored::Variable*> &diagonalVars,
2123+ bool lessthan, bool strict) {
2124+
2125+ for(auto varPositionPair : *varPositionsL){
2126+ uint32_t index = varPositionPair.first;
2127+ if(varPositionsR->count(index)){
2128+ restrictDiagonal(variableMap, varModifierMapL, varModifierMapR, varPositionsL, varPositionsR,
2129+ constantMapL, constantMapR, diagonalVars, varPositionPair.second, index, lessthan, strict);
2130+ } else {
2131+ restrictByConstant(variableMap, varModifierMapR, varModifierMapL, varPositionsR, constantMapR,
2132+ varPositionPair.second, varPositionPair.second, index, lessthan, strict);
2133+ }
2134+ }
2135+
2136+ for(auto varPositionPair : *varPositionsR){
2137+ uint32_t index = varPositionPair.first;
2138+
2139+ if(constantMapL->count(index)){
2140+ restrictByConstant(variableMap,varModifierMapL, varModifierMapR, varPositionsL, constantMapL,
2141+ varPositionPair.second, varPositionsR->operator[](index),index, lessthan, strict);
2142+ }
2143+ }
2144+ }
2145+
2146+ void GuardRestrictor::restrictEquality(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
2147+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
2148+ std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
2149+ std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsL,
2150+ std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsR,
2151+ std::unordered_map<uint32_t, const Color*> *constantMapL,
2152+ std::unordered_map<uint32_t, const Color*> *constantMapR,
2153+ std::set<const Colored::Variable*> &diagonalVars) {
2154+ for(auto varPositionPair : *varPositionsL){
2155+ uint32_t index = varPositionPair.first;
2156+ if(varPositionsR->count(index)){
2157+ restrictEqDiagonal(variableMap, varModifierMapL, varModifierMapR, varPositionsL, varPositionsR,
2158+ constantMapL, constantMapR, diagonalVars, varPositionPair.second, index);
2159+ } else {
2160+ restrictEqByConstant(variableMap, varModifierMapR, varModifierMapL, varPositionsR,
2161+ constantMapR, varPositionPair.second, index);
2162+ }
2163+ }
2164+
2165+ for(auto varPositionPair : *varPositionsR){
2166+ uint32_t index = varPositionPair.first;
2167+
2168+ if(constantMapL->count(index)){
2169+ restrictEqByConstant(variableMap, varModifierMapL, varModifierMapR, varPositionsL,
2170+ constantMapL, varPositionPair.second, index);
2171+ }
2172+ }
2173+ }
2174+
2175+ intervalTuple_t GuardRestrictor::shiftIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes, PetriEngine::Colored::intervalTuple_t *intervals, int32_t modifier, uint32_t ctSizeBefore) const {
2176+ Colored::intervalTuple_t newIntervals;
2177 for(uint32_t i = 0; i < intervals->size(); i++) {
2178- interval_t newInterval;
2179- std::vector<interval_t> tempIntervals;
2180+ Colored::interval_t newInterval;
2181+ std::vector<Colored::interval_t> tempIntervals;
2182 auto interval = &intervals->operator[](i);
2183 for(uint32_t j = 0; j < interval->_ranges.size(); j++) {
2184 auto& range = interval->operator[](j);
2185@@ -351,7 +391,7 @@
2186 tempIntervals.push_back(newInterval);
2187 tempIntervals.push_back(intervalCopy);
2188 } else {
2189- std::vector<interval_t> newTempIntervals;
2190+ std::vector<Colored::interval_t> newTempIntervals;
2191 for(auto tempInterval : tempIntervals){
2192 auto intervalCopy = tempInterval;
2193 tempInterval.addRange(range._lower, ctSize-1);
2194
2195=== added file 'src/PetriEngine/Colored/PartitionBuilder.cpp'
2196--- src/PetriEngine/Colored/PartitionBuilder.cpp 1970-01-01 00:00:00 +0000
2197+++ src/PetriEngine/Colored/PartitionBuilder.cpp 2021-04-14 13:35:08 +0000
2198@@ -0,0 +1,333 @@
2199+#include "PetriEngine/Colored/PartitionBuilder.h"
2200+#include <numeric>
2201+#include <chrono>
2202+
2203+
2204+
2205+namespace PetriEngine {
2206+ namespace Colored {
2207+
2208+ 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)
2209+ : _transitions(transitions), _places(places), _placePostTransitionMap(placePostTransitionMap), _placePreTransitionMap(placePreTransitionMap) {
2210+
2211+ //Instantiate partitions
2212+ for(uint32_t i = 0; i < _places->size(); i++){
2213+ auto place = _places->operator[](i);
2214+ interval_t fullInterval = place.type->getFullInterval();
2215+ EquivalenceClass fullClass = EquivalenceClass(place.type);
2216+ fullClass._colorIntervals.addInterval(fullInterval);
2217+ _partition[i]._equivalenceClasses.push_back(fullClass);
2218+ _placeQueue.push_back(i);
2219+ _inQueue[i] = true;
2220+ }
2221+ }
2222+
2223+ void PartitionBuilder::printPartion() {
2224+ for(auto equivalenceVec : _partition){
2225+ std::cout << "Partition for place " << _places->operator[](equivalenceVec.first).name << std::endl;
2226+ for (auto equivalenceClass : equivalenceVec.second._equivalenceClasses){
2227+ std::cout << equivalenceClass.toString() << std::endl;
2228+
2229+ }
2230+ std::cout << "Diagonal " << equivalenceVec.second.diagonal << std::endl << std::endl;;
2231+ }
2232+ }
2233+
2234+ void PartitionBuilder::partitionNet(){
2235+ handleLeafTransitions();
2236+
2237+ while(!_placeQueue.empty()){
2238+ auto placeId = _placeQueue.back();
2239+ _placeQueue.pop_back();
2240+ _inQueue[placeId] = false;
2241+
2242+ auto place = _places->operator[](placeId);
2243+
2244+ for(uint32_t transitionId : _placePreTransitionMap->operator[](placeId)){
2245+ //std::cout << "For transition " << _transitions->operator[](transitionId).name << " and place " << _places->operator[](placeId).name << std::endl;
2246+ //printPartion();
2247+
2248+ handleTransition(transitionId, placeId);
2249+
2250+ //std::cout << "---------------------------------------------------" << std::endl;
2251+ }
2252+ }
2253+ }
2254+
2255+ void PartitionBuilder::assignColorMap(std::unordered_map<uint32_t, EquivalenceVec> &partition){
2256+ for(auto& eqVec : partition){
2257+ if(eqVec.second.diagonal){
2258+ continue;
2259+ }
2260+ ColorType *colorType = _places->operator[](eqVec.first).type;
2261+ for(uint32_t i = 0; i < colorType->size(); i++){
2262+ const Color *color = &colorType->operator[](i);
2263+ for(auto& eqClass : eqVec.second._equivalenceClasses){
2264+ std::vector<uint32_t> colorIds;
2265+ color->getTupleId(&colorIds);
2266+ if(eqClass.containsColor(colorIds)){
2267+ eqVec.second.colorEQClassMap[color] = &eqClass;
2268+ }
2269+ }
2270+ }
2271+ }
2272+ }
2273+
2274+ void PartitionBuilder::handleTransition(uint32_t transitionId, uint32_t postPlaceId){
2275+ auto transition = _transitions->operator[](transitionId);
2276+ Arc postArc;
2277+ bool arcFound = false;
2278+ for(auto& outArc : transition.output_arcs){
2279+ if(outArc.place == postPlaceId){
2280+ postArc = outArc;
2281+ arcFound = true;
2282+ break;
2283+ }
2284+ }
2285+
2286+ if(!arcFound){
2287+ return;
2288+ }
2289+
2290+ handleTransition(&transition, postPlaceId, &postArc);
2291+ }
2292+
2293+ void PartitionBuilder::handleTransition(Transition *transition, uint32_t postPlaceId, Arc *postArc) {
2294+ std::unordered_map<const PetriEngine::Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMap;
2295+ std::unordered_map<uint32_t, const PetriEngine::Colored::Variable *> varPositionMap;
2296+ std::set<const PetriEngine::Colored::Variable *> postArcVars;
2297+ std::set<const PetriEngine::Colored::Variable *>guardVars;
2298+ std::set<const Colored::Variable*> diagonalVars;
2299+
2300+ postArc->expr->getVariables(postArcVars, varPositionMap, varModifierMap);
2301+
2302+ for(auto varModMap : varModifierMap){
2303+ if(varModMap.second.size() > 1){
2304+ uint32_t actualSize = 0;
2305+ for(auto map : varModMap.second){
2306+ if(!map.empty()){
2307+ actualSize++;
2308+ }
2309+ }
2310+ if(actualSize > 1) {
2311+ _partition[postPlaceId].diagonal = true;
2312+ }
2313+ }
2314+ }
2315+
2316+ if(transition->guard != nullptr){
2317+ transition->guard->getVariables(guardVars);
2318+ }
2319+
2320+ auto placePartition = _partition[postPlaceId]._equivalenceClasses;
2321+
2322+ for(auto eqClass : placePartition){
2323+ auto varMaps = prepareVariables(varModifierMap, &eqClass, postArc, postPlaceId);
2324+
2325+ for(auto& varMap : varMaps){
2326+ for(auto var : guardVars){
2327+ if(varMap.count(var) == 0){
2328+ varMap[var].addInterval(var->colorType->getFullInterval());
2329+ }
2330+ }
2331+ }
2332+
2333+ if(transition->guard != nullptr){
2334+ transition->guard->restrictVars(varMaps, diagonalVars);
2335+ }
2336+
2337+ std::unordered_map<uint32_t, std::set<const Colored::Variable *>> placeVariableMap;
2338+ for(auto inArc : transition->input_arcs){
2339+ //Hack to avoid considering dot places and dealing with retrieving the correct dot pointer
2340+ if(_places->operator[](inArc.place).type->getName() == "Dot" || _places->operator[](inArc.place).type->getName() == "dot"){
2341+ _partition[inArc.place].diagonal = true;
2342+ }
2343+
2344+ if(_partition[inArc.place].diagonal){
2345+ continue;
2346+ }
2347+
2348+ std::unordered_map<const PetriEngine::Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>> preVarModifierMap;
2349+ std::unordered_map<uint32_t, const PetriEngine::Colored::Variable *> preVarPositionMap;
2350+ std::set<const PetriEngine::Colored::Variable *> preArcVars;
2351+ inArc.expr->getVariables(preArcVars, preVarPositionMap, preVarModifierMap);
2352+ for(auto placeVariables : placeVariableMap){
2353+ for(auto variable : preArcVars){
2354+ if(placeVariables.second.count(variable)){
2355+ _partition[inArc.place].diagonal = true;
2356+ _partition[placeVariables.first].diagonal = true;
2357+ addToQueue(inArc.place);
2358+ addToQueue(placeVariables.first);
2359+ break;
2360+ }
2361+ }
2362+ if(_partition[inArc.place].diagonal) {
2363+ break;
2364+ }
2365+ }
2366+ placeVariableMap[inArc.place] = preArcVars;
2367+
2368+ if(_partition[inArc.place].diagonal){
2369+ continue;
2370+ }
2371+
2372+ if(_partition[postPlaceId].diagonal){
2373+ for(auto preVar : preArcVars){
2374+ if(postArcVars.count(preVar)){
2375+ //maybe something different should happen for tuples
2376+ // --(x,y)-->[]--(z,y)-->
2377+ _partition[inArc.place].diagonal = true;
2378+ break;
2379+ }
2380+ }
2381+ }
2382+
2383+ if(_partition[inArc.place].diagonal){
2384+ addToQueue(inArc.place);
2385+ continue;
2386+ }
2387+
2388+ for(auto varModMap : preVarModifierMap){
2389+ if(varModMap.second.size() > 1){
2390+ uint32_t actualSize = 0;
2391+ for(auto map : varModMap.second){
2392+ if(!map.empty()){
2393+ actualSize++;
2394+ }
2395+ }
2396+ if(actualSize > 1) {
2397+ _partition[inArc.place].diagonal = true;
2398+ }
2399+ }
2400+ }
2401+ for(auto preVar : preArcVars){
2402+ if(diagonalVars.count(preVar)){
2403+ //should only happen if the variable is not in a tuple
2404+ _partition[inArc.place].diagonal = true;
2405+ break;
2406+ }
2407+ }
2408+
2409+ auto outIntervals = inArc.expr->getOutputIntervals(varMaps);
2410+ outIntervals.simplify();
2411+ EquivalenceVec newEqVec;
2412+ EquivalenceClass newEqClass = EquivalenceClass(_partition[inArc.place]._equivalenceClasses.back()._colorType, outIntervals);
2413+ newEqVec._equivalenceClasses.push_back(newEqClass);
2414+
2415+ if((_partition[inArc.place].diagonal || splitPartition(newEqVec, inArc.place))){
2416+ addToQueue(inArc.place);
2417+ }
2418+ }
2419+ }
2420+
2421+ //is this still needed? does not seem so
2422+ // std::set<const PetriEngine::Colored::Variable *> preArcVars;
2423+ // for(auto inArc : transition->input_arcs){
2424+ // inArc.expr->getVariables(preArcVars);
2425+ // for(auto postVar : postArcVars){
2426+ // if(preArcVars.count(postVar)){
2427+ // if(diagonalVars.count(postVar)){
2428+ // _partition[inArc.place].diagonal = true;
2429+ // }
2430+ // }
2431+ // }
2432+ // }
2433+ }
2434+
2435+ void PartitionBuilder::addToQueue(uint32_t placeId){
2436+ if(!_inQueue[placeId]){
2437+ _placeQueue.push_back(placeId);
2438+ _inQueue[placeId] = true;
2439+ }
2440+ }
2441+
2442+
2443+ bool PartitionBuilder::splitPartition(PetriEngine::Colored::EquivalenceVec equivalenceVec, uint32_t placeId){
2444+ bool split = false;
2445+ if(_partition.count(placeId) == 0){
2446+ _partition[placeId] = equivalenceVec;
2447+ } else {
2448+ EquivalenceClass intersection = EquivalenceClass();
2449+ uint32_t ecPos1 = 0, ecPos2 = 0;
2450+ while(findOverlap(equivalenceVec, _partition[placeId],ecPos1, ecPos2, intersection)) {
2451+ auto ec1 = equivalenceVec._equivalenceClasses[ecPos1];
2452+ auto ec2 = _partition[placeId]._equivalenceClasses[ecPos2];
2453+ auto rightSubtractEc = ec1.subtract(ec2, false);
2454+ auto leftSubtractEc = ec2.subtract(ec1, false);
2455+ // if((_places->operator[](placeId).name == "NB_ATTENTE_A")) {
2456+ // std::cout << "comparing " << ec2.toString() << " to " << ec1.toString() << std::endl;
2457+
2458+ // std::cout << "Intersection: " << intersection.toString() << std::endl;
2459+ // std::cout << "Left: " << leftSubtractEc.toString() << std::endl;
2460+ // std::cout << "Right: " << rightSubtractEc.toString() << std::endl;
2461+ // ec2.subtract(ec1, true);
2462+ // }
2463+
2464+
2465+ equivalenceVec._equivalenceClasses.erase(equivalenceVec._equivalenceClasses.begin() + ecPos1);
2466+ _partition[placeId]._equivalenceClasses.erase(_partition[placeId]._equivalenceClasses.begin() + ecPos2);
2467+
2468+ if(!intersection.isEmpty()){
2469+ _partition[placeId]._equivalenceClasses.push_back(intersection);
2470+ intersection._colorIntervals._intervals.clear();
2471+ }
2472+ if(!leftSubtractEc.isEmpty()){
2473+ _partition[placeId]._equivalenceClasses.push_back(leftSubtractEc);
2474+ split = true;
2475+ }
2476+ if(!rightSubtractEc.isEmpty()){
2477+ equivalenceVec._equivalenceClasses.push_back(rightSubtractEc);
2478+ }
2479+ }
2480+ }
2481+ return split;
2482+ }
2483+
2484+ bool PartitionBuilder::findOverlap(EquivalenceVec equivalenceVec1, EquivalenceVec equivalenceVec2, uint32_t &overlap1, uint32_t &overlap2, EquivalenceClass &intersection){
2485+ for(uint32_t i = 0; i < equivalenceVec1._equivalenceClasses.size(); i++){
2486+ for(uint32_t j = 0; j < equivalenceVec2._equivalenceClasses.size(); j++){
2487+ auto ec = equivalenceVec1._equivalenceClasses[i];
2488+ auto ec2 = equivalenceVec2._equivalenceClasses[j];
2489+
2490+ auto intersectingEc = ec.intersect(ec2);
2491+ if(!intersectingEc.isEmpty()){
2492+ overlap1 = i;
2493+ overlap2 = j;
2494+ intersection = intersectingEc;
2495+ return true;
2496+ }
2497+ }
2498+ }
2499+ return false;
2500+ }
2501+
2502+ std::vector<std::unordered_map<const Variable *, intervalTuple_t>>
2503+ PartitionBuilder::prepareVariables(
2504+ std::unordered_map<const Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMap,
2505+ EquivalenceClass *eqClass , Arc *arc, uint32_t placeId){
2506+ std::vector<std::unordered_map<const Variable *, intervalTuple_t>> varMaps;
2507+ std::unordered_map<const Variable *, intervalTuple_t> varMap;
2508+ varMaps.push_back(varMap);
2509+ std::unordered_map<uint32_t, ArcIntervals> placeArcIntervals;
2510+ ColorFixpoint postPlaceFixpoint;
2511+ postPlaceFixpoint.constraints = eqClass->_colorIntervals;
2512+ ArcIntervals newArcInterval(&postPlaceFixpoint, varModifierMap);
2513+ uint32_t index = 0;
2514+
2515+ arc->expr->getArcIntervals(newArcInterval, postPlaceFixpoint, &index, 0);
2516+ placeArcIntervals[placeId] = newArcInterval;
2517+ intervalGenerator.getVarIntervals(varMaps, placeArcIntervals);
2518+
2519+ return varMaps;
2520+ }
2521+
2522+ void PartitionBuilder::handleLeafTransitions(){
2523+ for(uint32_t i = 0; i < _transitions->size(); i++){
2524+ auto transition = _transitions->operator[](i);
2525+ if(transition.output_arcs.empty() && !transition.input_arcs.empty()){
2526+ handleTransition(&transition, transition.input_arcs.back().place, &transition.input_arcs.back());
2527+ }
2528+ }
2529+ }
2530+ }
2531+}
2532\ No newline at end of file
2533
2534=== modified file 'src/PetriEngine/PQL/Expressions.cpp'
2535--- src/PetriEngine/PQL/Expressions.cpp 2021-03-31 11:31:54 +0000
2536+++ src/PetriEngine/PQL/Expressions.cpp 2021-04-14 13:35:08 +0000
2537@@ -377,7 +377,7 @@
2538 }
2539
2540 if (names.size() == 1) {
2541- _compiled = generateUnfoldedIdentifierExpr(*coloredContext, names, 0);
2542+ _compiled = generateUnfoldedIdentifierExpr(*coloredContext, names, names.begin()->first);
2543 } else {
2544 std::vector<Expr_ptr> identifiers;
2545 for (auto& unfoldedName : names) {
2546
2547=== modified file 'src/PetriParse/PNMLParser.cpp'
2548--- src/PetriParse/PNMLParser.cpp 2021-03-18 09:54:59 +0000
2549+++ src/PetriParse/PNMLParser.cpp 2021-04-14 13:35:08 +0000
2550@@ -231,7 +231,7 @@
2551 } else if (strcmp(element->name(), "tuple") == 0) {
2552 std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> collectedColors;
2553 collectColorsInTuple(element, collectedColors);
2554- auto expr = constructAddExpressionFromTupleExpression(element, collectedColors);
2555+ auto expr = constructAddExpressionFromTupleExpression(element, collectedColors, 1);
2556 std::cout << expr->toString() << std::endl;
2557 return expr;
2558 }
2559@@ -240,7 +240,7 @@
2560 return nullptr;
2561 }
2562
2563-PetriEngine::Colored::ArcExpression_ptr PNMLParser::constructAddExpressionFromTupleExpression(rapidxml::xml_node<>* element,std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> collectedColors){
2564+PetriEngine::Colored::ArcExpression_ptr PNMLParser::constructAddExpressionFromTupleExpression(rapidxml::xml_node<>* element,std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> collectedColors, uint32_t numberof){
2565 auto initCartesianSet = cartesianProduct(collectedColors[0], collectedColors[1]);
2566 for(uint32_t i = 2; i < collectedColors.size(); i++){
2567 initCartesianSet = cartesianProduct(initCartesianSet, collectedColors[i]);
2568@@ -255,7 +255,7 @@
2569 tupleExpr->setColorType(tupleExpr->getColorType(colorTypes));
2570 std::vector<PetriEngine::Colored::ColorExpression_ptr> placeholderVector;
2571 placeholderVector.push_back(tupleExpr);
2572- numberOfExpressions.push_back(std::make_shared<PetriEngine::Colored::NumberOfExpression>(std::move(placeholderVector),1));
2573+ numberOfExpressions.push_back(std::make_shared<PetriEngine::Colored::NumberOfExpression>(std::move(placeholderVector),numberof));
2574 }
2575 std::vector<PetriEngine::Colored::ArcExpression_ptr> constituents;
2576 for (auto expr : numberOfExpressions) {
2577@@ -471,7 +471,7 @@
2578 return nullptr;
2579 }
2580
2581-PetriEngine::Colored::NumberOfExpression_ptr PNMLParser::parseNumberOfExpression(rapidxml::xml_node<>* element) {
2582+PetriEngine::Colored::ArcExpression_ptr PNMLParser::parseNumberOfExpression(rapidxml::xml_node<>* element) {
2583 auto num = element->first_node();
2584 uint32_t number = parseNumberConstant(num);
2585 rapidxml::xml_node<>* first;
2586@@ -561,7 +561,8 @@
2587 initialMarking = atoll(text.c_str());
2588 } else if (strcmp(it->name(),"hlinitialMarking") == 0) {
2589 std::unordered_map<const PetriEngine::Colored::Variable*, const PetriEngine::Colored::Color*> binding;
2590- PetriEngine::Colored::ExpressionContext context {binding, colorTypes};
2591+ PetriEngine::Colored::EquivalenceVec placePartition;
2592+ PetriEngine::Colored::ExpressionContext context {binding, colorTypes, placePartition};
2593 hlinitialMarking = parseArcExpression(it->first_node("structure"))->eval(context);
2594 } else if (strcmp(it->name(), "type") == 0) {
2595 type = parseUserSort(it);
2596@@ -778,4 +779,4 @@
2597 }
2598 printf("Could not find color: %s\nCANNOT_COMPUTE\n", value);
2599 exit(ErrorCode);
2600-}
2601\ No newline at end of file
2602+}
2603
2604=== modified file 'src/VerifyPN.cpp'
2605--- src/VerifyPN.cpp 2021-04-12 15:27:26 +0000
2606+++ src/VerifyPN.cpp 2021-04-14 13:35:08 +0000
2607@@ -408,6 +408,10 @@
2608 options.gamemode = true;
2609 } else if (strcmp(argv[i], "-c") == 0 || strcmp(argv[i], "--cpn-overapproximation") == 0) {
2610 options.cpnOverApprox = true;
2611+ } else if (strcmp(argv[i], "--disable-cfp") == 0) {
2612+ options.computeCFP = false;
2613+ } else if (strcmp(argv[i], "--disable-partitioning") == 0) {
2614+ options.computePartition = false;
2615 } else if (strcmp(argv[i], "-h") == 0 || strcmp(argv[i], "--help") == 0) {
2616 printf("Usage: verifypn [options] model-file query-file\n"
2617 "A tool for answering CTL and reachability queries of place cardinality\n"
2618@@ -455,6 +459,8 @@
2619 " -noreach Force use of CTL/LTL engine, even when queries are reachability.\n"
2620 " Not recommended since the reachability engine is faster.\n"
2621 " -c, --cpn-overapproximation Over approximate query on Colored Petri Nets (CPN only)\n"
2622+ " --disable-cfp Disable the computation of possible colors in the Petri Net (CPN only)\n"
2623+ " --disable-partitioning Disable the partitioning of colors in the Petri Net (CPN only)\n"
2624 //" -g Enable game mode (CTL Only)" // Feature not yet implemented
2625 #ifdef VERIFYPN_MC_Simplification
2626 " -z <number of cores> Number of cores to use (currently only query simplification)\n"
2627@@ -775,24 +781,16 @@
2628 builder.getUnfoldedTransitionCount() << " transitions, and " <<
2629 builder.getUnfoldedArcCount() << " arcs" << std::endl;
2630 std::cout << "Unfolded in " << builder.getUnfoldTime() << " seconds" << std::endl;
2631+ std::cout << "Partitioned in " << builder.getPartitionTime() << " seconds" << std::endl;
2632
2633
2634 if(!options.output_stats.empty()){
2635 std::ofstream log(generated_filename, std::ios_base::app | std::ios_base::out);
2636 std::ostringstream strs;
2637- strs << filename << "," << builder.getPlaceCount() << "," << builder.getTransitionCount() << "," << builder.getArcCount() << "," << builder.getUnfoldedPlaceCount() << "," << builder.getUnfoldedTransitionCount() << "," << builder.getUnfoldedArcCount() << "," << builder.getUnfoldTime() << "," << builder.getFixpointTime() << "\n";
2638- std::string str = strs.str();
2639- log << str;
2640- }
2641-
2642- if(!options.output_stats.empty()){
2643- std::ofstream log(generated_filename, std::ios_base::app | std::ios_base::out);
2644- std::ostringstream strs;
2645- strs << filename << "," << builder.getPlaceCount() << "," << builder.getTransitionCount() << "," << builder.getArcCount() << "," << builder.getUnfoldedPlaceCount() << "," << builder.getUnfoldedTransitionCount() << "," << builder.getUnfoldedArcCount() << "," << builder.getUnfoldTime() << "," << builder.getFixpointTime() << "\n";
2646- std::string str = strs.str();
2647- log << str;
2648- }
2649-
2650+ strs << filename << "," << builder.getPlaceCount() << "," << builder.getTransitionCount() << "," << builder.getArcCount() << "," << builder.getUnfoldedPlaceCount() << "," << builder.getUnfoldedTransitionCount() << "," << builder.getUnfoldedArcCount() << "," << builder.getUnfoldTime() << "," << builder.getFixpointTime() << "," << builder.getPartitionTime() << "\n";
2651+ std::string str = strs.str();
2652+ log << str;
2653+ }
2654 //}
2655 }
2656
2657@@ -1049,7 +1047,14 @@
2658 }
2659 }
2660
2661- cpnBuilder.computePlaceColorFixpoint(options.max_intervals, options.max_intervals_reduced, options.intervalTimeout);
2662+ if(options.computePartition){
2663+ cpnBuilder.computePartition();
2664+ }
2665+ if(options.computeCFP){
2666+ cpnBuilder.computePlaceColorFixpoint(options.max_intervals, options.max_intervals_reduced, options.intervalTimeout);
2667+ }
2668+
2669+
2670
2671 auto builder = options.cpnOverApprox ? cpnBuilder.stripColors() : cpnBuilder.unfold();
2672 printUnfoldingStats(cpnBuilder, options);

Subscribers

People subscribed via source and target branches

to all changes: