← Back to branch summary

~tapaal-ltl/verifypn/fireable-empty-preset-fix

« back to all changes in this revision

Viewing changes to src/PetriEngine/Colored/EquivalenceClass.cpp

  • Committer: srba.jiri at gmail
  • Date: 2021-07-07 12:02:50 UTC
  • mfrom: (233.1.63 update-parser)
  • Revision ID: srba.jiri@gmail.com-20210707120250-f86fv0m9ycbge3qs
merged in lp:~tapaal-contributor/verifypn/update-parser improving CPN unfodling and refactoring the code, fixing parser

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/PetriEngine/Colored/EquivalenceClass.cpp
3
3
namespace PetriEngine {
4
4
    namespace Colored {
5
5
 
6
 
        uint32_t EquivalenceClass::idCounter = 0;
7
 
 
8
 
        EquivalenceClass::EquivalenceClass() : _id(++idCounter){
9
 
        }
10
 
        EquivalenceClass::EquivalenceClass(ColorType *colorType) 
11
 
        : _id(++idCounter), _colorType(colorType){
12
 
        }
13
 
        EquivalenceClass::EquivalenceClass(ColorType *colorType, intervalTuple_t colorIntervals) 
14
 
        : _id(++idCounter), _colorType(colorType), _colorIntervals(colorIntervals){
15
 
        }
16
 
 
17
 
        EquivalenceClass EquivalenceClass::intersect(EquivalenceClass other){
18
 
            EquivalenceClass result = EquivalenceClass();
 
6
 
 
7
        EquivalenceClass::EquivalenceClass(uint32_t id) : _id(id){
 
8
        }
 
9
        EquivalenceClass::EquivalenceClass(uint32_t id, const ColorType *colorType)
 
10
        : _id(id), _colorType(colorType){
 
11
        }
 
12
        EquivalenceClass::EquivalenceClass(uint32_t id, const ColorType *colorType, interval_vector_t&& colorIntervals)
 
13
        : _id(id), _colorType(colorType), _colorIntervals(std::move(colorIntervals)){
 
14
        }
 
15
 
 
16
        EquivalenceClass EquivalenceClass::intersect(uint32_t id, const EquivalenceClass &other) const{
 
17
            EquivalenceClass result = EquivalenceClass(id);
19
18
 
20
19
            if(_colorType != other._colorType){
21
20
                return result;
22
21
            }
23
22
            result._colorType = _colorType;
24
23
 
25
 
            for(auto interval : _colorIntervals._intervals){
26
 
                for(auto otherInterval : other._colorIntervals._intervals){
 
24
            for(const auto& interval : _colorIntervals){
 
25
                for(const auto& otherInterval : other._colorIntervals){
27
26
                    auto overlappingInterval = interval.getOverlap(otherInterval);
28
27
                    if(overlappingInterval.isSound()){
29
28
                        result._colorIntervals.addInterval(overlappingInterval);
34
33
        }
35
34
 
36
35
 
37
 
        EquivalenceClass EquivalenceClass::subtract(EquivalenceClass other, bool print){
38
 
            EquivalenceClass result = EquivalenceClass();
 
36
        EquivalenceClass EquivalenceClass::subtract(uint32_t id, const EquivalenceClass &other, const std::vector<bool> &diagonalPositions) const{
 
37
            EquivalenceClass result = EquivalenceClass(id);
39
38
            if(_colorType != other._colorType){
40
39
                return result;
41
40
            }
42
41
            result._colorType = _colorType;
43
 
            intervalTuple_t resIntervals;
44
 
            for(auto interval : _colorIntervals._intervals){ 
45
 
                intervalTuple_t intervalSubRes;                   
46
 
                for(auto otherInterval : other._colorIntervals._intervals){
47
 
                    auto subtractedIntervals = interval.getSubtracted(otherInterval, _colorType->size());
48
 
                    if(print){
49
 
                        std::cout << interval.toString() << " - " << otherInterval.toString() << " = " << std::endl;
50
 
                        for(auto subinter : subtractedIntervals){
51
 
                            std::cout << subinter.toString() << std::endl;
52
 
                        }
53
 
                        std::cout << "~~~~~~" << std::endl;
54
 
                    }
 
42
            interval_vector_t resIntervals;
 
43
            for(const auto& interval : _colorIntervals){
 
44
                interval_vector_t intervalSubRes;
 
45
                for(const auto& otherInterval : other._colorIntervals){
 
46
                    auto subtractedIntervals = interval.getSubtracted(otherInterval, diagonalPositions);
55
47
                    
56
48
 
57
49
                    if(subtractedIntervals.empty() || subtractedIntervals[0].size() == 0){
58
 
                        intervalSubRes._intervals.clear();
 
50
                        intervalSubRes.clear();
59
51
                        break;                           
60
52
                    }
61
53
 
62
 
                    if(intervalSubRes._intervals.empty()){
63
 
                        intervalSubRes._intervals = subtractedIntervals;
 
54
                    if(intervalSubRes.empty()){
 
55
                        intervalSubRes = subtractedIntervals;
64
56
                    } else {
65
 
                        intervalTuple_t newIntervals;
66
 
                        for(auto newInterval : subtractedIntervals){
67
 
                            for(auto interval : intervalSubRes._intervals){
 
57
                        interval_vector_t newIntervals;
 
58
                        for(const auto& newInterval : subtractedIntervals){
 
59
                            for(const auto& interval : intervalSubRes){
68
60
                                auto intersection = interval.getOverlap(newInterval);
69
61
                                if(intersection.isSound()){
70
62
                                    newIntervals.addInterval(intersection);
71
63
                                }
72
64
                            }
73
65
                        }
74
 
                        intervalSubRes = std::move(newIntervals);   
75
 
                        // for(auto newInterval : subtractedIntervals){
76
 
                        //     resIntervals.addInterval(newInterval);
77
 
                        // }                            
78
 
                    }
79
 
                    if(print){
80
 
                        std::cout << "intermediate res is now: " << intervalSubRes.toString() << std::endl;
 
66
                        intervalSubRes = std::move(newIntervals);                              
81
67
                    }
82
68
                }
83
 
                if(print) std::cout << "Done looping inner" << std::endl;
84
 
                for(auto interval : intervalSubRes._intervals){
 
69
                for(const auto& interval : intervalSubRes){
85
70
                    resIntervals.addInterval(interval);
86
 
                }
87
 
                if(print){
88
 
                    std::cout << "Subtract res is now: " << resIntervals.toString() << std::endl;
89
 
                }
90
 
                
 
71
                }                
91
72
            }
92
73
            result._colorIntervals = resIntervals;                  
93
74
            return result;
94
75
        }
95
76
 
96
 
        bool EquivalenceClass::containsColor(std::vector<uint32_t> ids){
97
 
            interval_t interval;
98
 
            for(auto id : ids){
99
 
                interval.addRange(id,id);
100
 
            }
101
 
            return _colorIntervals.contains(interval);
 
77
        bool EquivalenceClass::containsColor(const std::vector<uint32_t> &ids, const std::vector<bool> &diagonalPositions) const {
 
78
            if(ids.size() != _colorIntervals.front().size()){
 
79
                return false;
 
80
            }
 
81
            for(const auto &interval : _colorIntervals){
 
82
                bool contained = true;
 
83
                for(uint32_t i = 0; i < ids.size(); i++){
 
84
                    if(!diagonalPositions[i] && !interval[i].contains(ids[i])){
 
85
                        contained = false;
 
86
                        break;
 
87
                    }
 
88
                }
 
89
                if(contained){
 
90
                    return true;
 
91
                }
 
92
            }
 
93
            return false;
102
94
        }
103
95
 
104
 
        size_t EquivalenceClass::size(){
 
96
        size_t EquivalenceClass::size() const{
105
97
            size_t result = 0;
106
 
            for(auto interval : _colorIntervals._intervals){
 
98
            for(const auto& interval : _colorIntervals){
107
99
                size_t intervalSize = 1;
108
 
                for(auto range : interval._ranges){
 
100
                for(const auto& range : interval._ranges){
109
101
                    intervalSize *= range.size();
110
102
                }
111
103
                result += intervalSize;