← Back to branch summary

~verifypn-maintainers/verifypn/u4.2

« back to all changes in this revision

Viewing changes to include/PetriEngine/Colored/PartitionBuilder.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/PartitionBuilder.h
1
1
#include "ColoredNetStructures.h"
2
 
#include "EquivalenceClass.h"
 
2
#include "EquivalenceVec.h"
3
3
#include "IntervalGenerator.h"
4
4
 
5
5
namespace PetriEngine {
6
6
    namespace Colored {
7
7
        class PartitionBuilder {
 
8
 
 
9
            
8
10
            public:
9
 
                PartitionBuilder(std::vector<Transition> *transitions, 
10
 
                                std::vector<Place> *places, 
11
 
                                std::unordered_map<uint32_t,std::vector<uint32_t>> *placePostTransitionMap, 
12
 
                                std::unordered_map<uint32_t,std::vector<uint32_t>> *placePreTransitionMap);
 
11
                PartitionBuilder(const std::vector<Transition> &transitions, 
 
12
                                const std::vector<Place> &places, 
 
13
                                const std::unordered_map<uint32_t,std::vector<uint32_t>> &placePostTransitionMap, 
 
14
                                const std::unordered_map<uint32_t,std::vector<uint32_t>> &placePreTransitionMap);
13
15
 
14
 
                PartitionBuilder(std::vector<Transition> *transitions, 
15
 
                                std::vector<Place> *places, 
16
 
                                std::unordered_map<uint32_t,std::vector<uint32_t>> *placePostTransitionMap, 
17
 
                                std::unordered_map<uint32_t,std::vector<uint32_t>> *placePreTransitionMap,
18
 
                                std::vector<Colored::ColorFixpoint> *placeColorFixpoints);
 
16
                PartitionBuilder(const std::vector<Transition> &transitions, 
 
17
                                const std::vector<Place> &places, 
 
18
                                const std::unordered_map<uint32_t,std::vector<uint32_t>> &placePostTransitionMap, 
 
19
                                const std::unordered_map<uint32_t,std::vector<uint32_t>> &placePreTransitionMap,
 
20
                                const std::vector<Colored::ColorFixpoint> *placeColorFixpoints);
19
21
                
20
22
                ~PartitionBuilder() {}
21
23
 
22
24
                //void initPartition();
23
 
                void partitionNet();
24
 
                void refinePartition();
25
 
                void printPartion();
26
 
                void assignColorMap(std::unordered_map<uint32_t, EquivalenceVec> &partition);
 
25
                bool partitionNet(int32_t timeout);
 
26
                void printPartion() const;
 
27
                void assignColorMap(std::unordered_map<uint32_t, EquivalenceVec> &partition) const;
27
28
 
28
 
                std::unordered_map<uint32_t, EquivalenceVec> getPartition(){
 
29
                std::unordered_map<uint32_t, EquivalenceVec> getPartition() const{
29
30
                    return _partition;
30
31
                }
 
32
 
31
33
            private:
32
 
                std::vector<Transition> *_transitions;
33
 
                std::unordered_map<uint32_t,std::vector<uint32_t>> *_placePostTransitionMap;
34
 
                std::unordered_map<uint32_t,std::vector<uint32_t>> *_placePreTransitionMap;
 
34
                const std::vector<Transition> &_transitions;
 
35
                const std::vector<Place> &_places;
 
36
                const std::unordered_map<uint32_t,std::vector<uint32_t>> &_placePostTransitionMap;
 
37
                const std::unordered_map<uint32_t,std::vector<uint32_t>> &_placePreTransitionMap;
35
38
                std::unordered_map<uint32_t,bool> _inQueue;
36
 
                std::vector<Place> *_places;
37
39
                std::unordered_map<uint32_t, EquivalenceVec> _partition;
38
 
                PetriEngine::IntervalGenerator intervalGenerator;
 
40
                const PetriEngine::Colored::IntervalGenerator _interval_generator = IntervalGenerator();
39
41
                std::vector<uint32_t> _placeQueue;
40
42
 
41
43
                bool splitPartition(EquivalenceVec equivalenceVec, uint32_t placeId);
42
44
 
43
45
                void handleTransition(uint32_t transitionId, uint32_t postPlaceId);
44
 
                void handleTransition(Transition *transitionId, uint32_t postPlaceId, Arc *postArc);
 
46
                void handleTransition(const Transition &transitionId, const uint32_t postPlaceId, const Arc *postArc);
45
47
 
46
48
                void handleLeafTransitions();
47
49
                
48
50
                void addToQueue(uint32_t placeId);
49
51
 
50
 
                std::vector<std::unordered_map<const Variable *, intervalTuple_t>> prepareVariables(
51
 
                            std::unordered_map<const Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMap, 
52
 
                            EquivalenceClass *eqClass , Arc *postArc, uint32_t placeId);
53
 
 
54
 
                bool findOverlap(EquivalenceVec equivalenceVec1, EquivalenceVec equivalenceVec2, uint32_t &overlap1, uint32_t &overlap2, EquivalenceClass &intersection);
55
 
 
56
 
                uint32_t eqClassIdCounter = 0;
 
52
                bool checkTupleDiagonal(uint32_t placeId);
 
53
                bool checkDiagonal(uint32_t placeId);
 
54
 
 
55
                void handleInArcs(const Transition &transition, std::set<const Colored::Variable*> &diagonalVars, const PositionVariableMap &varPositionMap, const std::vector<PetriEngine::Colored::VariableIntervalMap> &varMaps, uint32_t postPlaceId);
 
56
 
 
57
                void applyNewIntervals(const Arc &inArc, const std::vector<PetriEngine::Colored::VariableIntervalMap> &varMaps);
 
58
 
 
59
                void checkVarOnArc(const VariableModifierMap &varModifierMap, std::set<const Colored::Variable*> &diagonalVars, uint32_t placeId, bool inputArc);
 
60
 
 
61
                void checkVarOnInputArcs(const std::unordered_map<uint32_t,PositionVariableMap> &placeVariableMap, const PositionVariableMap &preVarPositionMap, std::set<const Colored::Variable*> &diagonalVars, uint32_t placeId);
 
62
 
 
63
                void markSharedVars(const PositionVariableMap &preVarPositionMap, const PositionVariableMap &varPositionMap, uint32_t postPlaceId, uint32_t prePlaceId);
 
64
                void checkVarInGuard(const PositionVariableMap &preVarPositionMap, const std::set<const Colored::Variable*> &diagonalVars, uint32_t placeId);
 
65
 
 
66
                std::vector<VariableIntervalMap> prepareVariables(
 
67
                            const VariableModifierMap &varModifierMap, 
 
68
                            const EquivalenceClass& eqClass , const Arc *postArc, uint32_t placeId);
 
69
 
 
70
                bool findOverlap(const EquivalenceVec &equivalenceVec1,const EquivalenceVec &equivalenceVec2, uint32_t &overlap1, uint32_t &overlap2, EquivalenceClass &intersection);
 
71
 
 
72
                uint32_t _eq_id_counter = 0;
 
73
 
57
74
        };
58
75
    }
59
 
}
 
 
b'\\ No newline at end of file'
 
76
}