← Back to branch summary

~verifypn-maintainers/verifypn/u4.2

« back to all changes in this revision

Viewing changes to include/PetriEngine/Colored/GuardRestrictor.h

  • 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:
include/PetriEngine/Colored/GuardRestrictor.h
33
33
 
34
34
                GuardRestrictor();
35
35
 
36
 
                void restrictDiagonal(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
37
 
                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
38
 
                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
39
 
                            std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsL,
40
 
                            std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsR,
41
 
                            std::unordered_map<uint32_t, const Color*> *constantMapL,
42
 
                            std::unordered_map<uint32_t, const Color*> *constantMapR,
 
36
                void restrictDiagonal(std::vector<VariableIntervalMap>& variableMap,
 
37
                            const VariableModifierMap &varModifierMapL,
 
38
                            const VariableModifierMap &varModifierMapR,
 
39
                            const PositionVariableMap &varPositionsL,
 
40
                            const PositionVariableMap &varPositionsR,
 
41
                            const std::unordered_map<uint32_t, const Color*> &constantMapL,
 
42
                            const std::unordered_map<uint32_t, const Color*> &constantMapR,
43
43
                            std::set<const Colored::Variable*> &diagonalVars,
44
44
                            const Colored::Variable *var, 
45
 
                            uint32_t index, bool lessthan, bool strict);
 
45
                            uint32_t index, bool lessthan, bool strict) const;
46
46
 
47
47
                
48
48
 
49
 
                void restrictEquality(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
50
 
                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
51
 
                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
52
 
                            std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsL,
53
 
                            std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsR,
54
 
                            std::unordered_map<uint32_t, const Color*> *constantMapL,
55
 
                            std::unordered_map<uint32_t, const Color*> *constantMapR,
56
 
                            std::set<const Colored::Variable*> &diagonalVars);
57
 
 
58
 
                void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
59
 
                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
60
 
                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
61
 
                            std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsL,
62
 
                            std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsR,
63
 
                            std::unordered_map<uint32_t, const Color*> *constantMapL,
64
 
                            std::unordered_map<uint32_t, const Color*> *constantMapR,
 
49
                void restrictEquality(std::vector<VariableIntervalMap>& variableMap,
 
50
                            const VariableModifierMap &varModifierMapL,
 
51
                            const VariableModifierMap &varModifierMapR,
 
52
                            const PositionVariableMap &varPositionsL,
 
53
                            const PositionVariableMap &varPositionsR,
 
54
                            const std::unordered_map<uint32_t, const Color*> &constantMapL,
 
55
                            const std::unordered_map<uint32_t, const Color*> &constantMapR,
 
56
                            std::set<const Colored::Variable*> &diagonalVars) const;
 
57
 
 
58
                void restrictInEquality(std::vector<VariableIntervalMap>& variableMap,
 
59
                            const VariableModifierMap &varModifierMapL,
 
60
                            const VariableModifierMap &varModifierMapR,
 
61
                            const PositionVariableMap &varPositionsL,
 
62
                            const PositionVariableMap &varPositionsR,
 
63
                            const std::unordered_map<uint32_t, const Color*> &constantMapL,
 
64
                            const std::unordered_map<uint32_t, const Color*> &constantMapR,
 
65
                            std::set<const Colored::Variable*> &diagonalVars) const;
 
66
 
 
67
                void restrictVars(std::vector<VariableIntervalMap>& variableMap,
 
68
                            const VariableModifierMap &varModifierMapL,
 
69
                            const VariableModifierMap &varModifierMapR,
 
70
                            const PositionVariableMap &varPositionsL,
 
71
                            const PositionVariableMap &varPositionsR,
 
72
                            const std::unordered_map<uint32_t, const Color*> &constantMapL,
 
73
                            const std::unordered_map<uint32_t, const Color*> &constantMapR,
65
74
                            std::set<const Colored::Variable*> &diagonalVars, 
66
 
                            bool lessthan, bool strict);
 
75
                            bool lessthan, bool strict) const;
67
76
 
68
 
                intervalTuple_t shiftIntervals(std::unordered_map<const Variable *, intervalTuple_t>& varMap, 
69
 
                            std::vector<const ColorType *> *colortypes, intervalTuple_t *intervals, 
 
77
                interval_vector_t shiftIntervals(const VariableIntervalMap& varMap, 
 
78
                            const std::vector<const ColorType *> &colortypes, interval_vector_t &intervals, 
70
79
                            int32_t modifier, uint32_t ctSizeBefore) const; 
71
80
 
72
81
            private:
73
 
                int32_t getVarModifier(std::unordered_map<uint32_t, int32_t> *modPairMap, uint32_t index);
74
 
                interval_t getIntervalFromIds(std::vector<uint32_t> *idVec, uint32_t ctSize, int32_t modifier);
75
 
                intervalTuple_t getIntervalOverlap(std::vector<Colored::interval_t> *intervals1, std::vector<Colored::interval_t> *intervals2);
76
 
 
77
 
                void expandIdVec(std::unordered_map<const Variable *, intervalTuple_t> *varMap,
78
 
                            std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *mainVarModifierMap,
79
 
                            std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *otherVarModifierMap,
80
 
                            std::unordered_map<uint32_t, const Variable *> *varPositions,
81
 
                            std::unordered_map<uint32_t, const Color*> *constantMap,
82
 
                            const Variable *otherVar, 
83
 
                            std::vector<uint32_t> &idVec, size_t targetSize, uint32_t index);
84
 
 
85
 
                void expandIntervalVec(std::unordered_map<const Variable *, intervalTuple_t> varMap,
86
 
                            std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *mainVarModifierMap,
87
 
                            std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *otherVarModifierMap,
88
 
                            std::unordered_map<uint32_t, const Variable *> *varPositions,
89
 
                            std::unordered_map<uint32_t, const Color*> *constantMap,
90
 
                            const Variable *otherVar, 
91
 
                            std::vector<interval_t> &intervalVec, size_t targetSize, uint32_t index);
92
 
 
93
 
                void restrictByConstant(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
94
 
                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *mainVarModifierMap,
95
 
                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *otherVarModifierMap,
96
 
                            std::unordered_map<uint32_t, const Colored::Variable *> *varPositions,
97
 
                            std::unordered_map<uint32_t, const Color*> *constantMap,
 
82
                int32_t getVarModifier(const std::unordered_map<uint32_t, int32_t> &modPairMap, uint32_t index) const;
 
83
                interval_t getIntervalFromIds(const std::vector<uint32_t> &idVec, uint32_t ctSize, int32_t modifier) const;
 
84
                interval_vector_t getIntervalOverlap(const Colored::interval_vector_t &intervals1, const Colored::interval_vector_t &intervals2) const;
 
85
                void invertIntervals(interval_vector_t &intervals, const interval_vector_t &oldIntervals, const ColorType *colorType) const;
 
86
 
 
87
 
 
88
                void handleInequalityConstants(const std::vector<VariableIntervalMap> &variableMapCopy, 
 
89
                                        std::vector<VariableIntervalMap> &variableMap, 
 
90
                                        const Variable *var, uint32_t varMapIndex) const;
 
91
 
 
92
                void handleInequalityVars(const std::vector<VariableIntervalMap> &variableMapCopy, 
 
93
                                        std::vector<VariableIntervalMap> &variableMap, 
 
94
                                        const Variable *var1, const Variable *var2, uint32_t varMapIndex) const;
 
95
 
 
96
                void expandIdVec(const VariableIntervalMap &varMap,
 
97
                            const VariableModifierMap &mainVarModifierMap,
 
98
                            const VariableModifierMap &otherVarModifierMap,
 
99
                            const std::unordered_map<uint32_t, const Variable *> &varPositions,
 
100
                            const std::unordered_map<uint32_t, const Color*> &constantMap,
 
101
                            const Variable *otherVar, 
 
102
                            std::vector<uint32_t> &idVec, size_t targetSize, uint32_t index) const;
 
103
 
 
104
                void expandIntervalVec(const VariableIntervalMap &varMap,
 
105
                            const VariableModifierMap &mainVarModifierMap,
 
106
                            const VariableModifierMap &otherVarModifierMap,
 
107
                            const std::unordered_map<uint32_t, const Variable *> &varPositions,
 
108
                            const std::unordered_map<uint32_t, const Color*> &constantMap,
 
109
                            const Variable *otherVar, 
 
110
                            interval_vector_t &intervalVec, size_t targetSize, uint32_t index) const;
 
111
 
 
112
                void restrictByConstant(std::vector<VariableIntervalMap>& variableMap,
 
113
                            const VariableModifierMap &mainVarModifierMap,
 
114
                            const VariableModifierMap &otherVarModifierMap,
 
115
                            const PositionVariableMap &varPositions,
 
116
                            const std::unordered_map<uint32_t, const Color*> &constantMap,
98
117
                            const Colored::Variable *var,
99
118
                            const Colored::Variable *otherVar, 
100
 
                            uint32_t index, bool lessthan, bool strict);
 
119
                            uint32_t index, bool lessthan, bool strict) const;
101
120
 
102
 
                void restrictEqByConstant(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
103
 
                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *mainVarModifierMap,
104
 
                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *otherVarModifierMap,
105
 
                            std::unordered_map<uint32_t, const Colored::Variable *> *varPositions,
106
 
                            std::unordered_map<uint32_t, const Color*> *constantMap,
 
121
                void restrictEqByConstant(std::vector<VariableIntervalMap>& variableMap,
 
122
                            const VariableModifierMap &mainVarModifierMap,
 
123
                            const VariableModifierMap &otherVarModifierMap,
 
124
                            const PositionVariableMap &varPositions,
 
125
                            const std::unordered_map<uint32_t, const Color*> &constantMap,
107
126
                            const Colored::Variable *var,
108
 
                            uint32_t index);
 
127
                            uint32_t index) const;
109
128
 
110
 
                void restrictEqDiagonal(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
111
 
                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
112
 
                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
113
 
                            std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsL,
114
 
                            std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsR,
115
 
                            std::unordered_map<uint32_t, const Color*> *constantMapL,
116
 
                            std::unordered_map<uint32_t, const Color*> *constantMapR,
 
129
                void restrictEqDiagonal(std::vector<VariableIntervalMap>& variableMap,
 
130
                            const VariableModifierMap &varModifierMapL,
 
131
                            const VariableModifierMap &varModifierMapR,
 
132
                            const PositionVariableMap &varPositionsL,
 
133
                            const PositionVariableMap &varPositionsR,
 
134
                            const std::unordered_map<uint32_t, const Color*> &constantMapL,
 
135
                            const std::unordered_map<uint32_t, const Color*> &constantMapR,
117
136
                            std::set<const Colored::Variable*> &diagonalVars,
118
137
                            const Colored::Variable *var, 
119
 
                            uint32_t index);    
 
138
                            uint32_t index) const;    
120
139
        };
121
140
    }
122
141
}