← Back to branch summary

~tapaal-ltl/verifypn/answer-for-gui

« back to all changes in this revision

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

  • Committer: srba.jiri at gmail
  • Date: 2021-04-02 18:13:50 UTC
  • mfrom: (230.1.28 mcc2021)
  • Revision ID: srba.jiri@gmail.com-20210402181350-k71xtjut3r48l1o5
merged in lp:~tapaal-ltl/verifypn/mcc2021 adding LTL, colored fixed-point unfolding for CPN and other performance improvements

Show diffs side-by-side

added added

removed removed

Lines of Context:
include/PetriEngine/Colored/ColoredPetriNetBuilder.h
1
 
/*
2
 
 * File:   ColoredPetriNetBuilder.h
3
 
 * Author: Klostergaard
4
 
 *
5
 
 * Created on 17. februar 2018, 16:25
 
1
/* Copyright (C) 2020  Alexander Bilgram <alexander@bilgram.dk>,
 
2
 *                     Peter Haar Taankvist <ptaankvist@gmail.com>,
 
3
 *                     Thomas Pedersen <thomas.pedersen@stofanet.dk>
 
4
 *                     Andreas H. Klostergaard
 
5
 *
 
6
 * This program is free software: you can redistribute it and/or modify
 
7
 * it under the terms of the GNU General Public License as published by
 
8
 * the Free Software Foundation, either version 3 of the License, or
 
9
 * (at your option) any later version.
 
10
 *
 
11
 * This program is distributed in the hope that it will be useful,
 
12
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 
13
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
14
 * GNU General Public License for more details.
 
15
 *
 
16
 * You should have received a copy of the GNU General Public License
 
17
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
6
18
 */
7
19
 
8
20
#ifndef COLOREDPETRINETBUILDER_H
11
23
#include <vector>
12
24
#include <unordered_map>
13
25
 
14
 
#include "ColoredNetStructures.h"
15
26
#include "../AbstractPetriNetBuilder.h"
16
27
#include "../PetriNetBuilder.h"
 
28
#include "BindingGenerator.h"
 
29
#include "IntervalGenerator.h"
 
30
#include "ArcIntervals.h"
17
31
 
18
32
namespace PetriEngine {
 
33
 
19
34
    class ColoredPetriNetBuilder : public AbstractPetriNetBuilder {
20
35
    public:
21
 
        typedef std::unordered_map<std::string, Colored::ColorType*> ColorTypeMap;
22
36
        typedef std::unordered_map<std::string, std::unordered_map<uint32_t , std::string>> PTPlaceMap;
23
37
        typedef std::unordered_map<std::string, std::vector<std::string>> PTTransitionMap;
24
38
        
66
80
            return _time;
67
81
        }
68
82
 
 
83
        double getFixpointTime() const {
 
84
            return _fixPointCreationTime;
 
85
        }
 
86
 
69
87
        uint32_t getPlaceCount() const {
70
88
            return _places.size();
71
89
        }
72
90
 
 
91
        uint32_t getMaxIntervals() const {
 
92
            return _maxIntervals;
 
93
        }
 
94
 
73
95
        uint32_t getTransitionCount() const {
74
96
            return _transitions.size();
75
97
        }
77
99
        uint32_t getArcCount() const {
78
100
            uint32_t sum = 0;
79
101
            for (auto& t : _transitions) {
80
 
                sum += t.arcs.size();
 
102
                sum += t.input_arcs.size();
 
103
                sum += t.output_arcs.size();
81
104
            }
82
105
            return sum;
83
106
        }
109
132
        
110
133
        PetriNetBuilder& unfold();
111
134
        PetriNetBuilder& stripColors();
 
135
        void computePlaceColorFixpoint(uint32_t maxIntervals, uint32_t maxIntervalsReduced, int32_t timeout);
 
136
        
112
137
    private:
113
138
        std::unordered_map<std::string,uint32_t> _placenames;
114
139
        std::unordered_map<std::string,uint32_t> _transitionnames;
 
140
        std::unordered_map<uint32_t, std::unordered_map<uint32_t, Colored::ArcIntervals>> _arcIntervals;
 
141
        std::unordered_map<uint32_t,std::vector<uint32_t>> _placePostTransitionMap;
 
142
        std::unordered_map<uint32_t,FixpointBindingGenerator> _bindings;
115
143
        PTPlaceMap _ptplacenames;
116
144
        PTTransitionMap _pttransitionnames;
117
145
        uint32_t _nptplaces = 0;
118
146
        uint32_t _npttransitions = 0;
119
147
        uint32_t _nptarcs = 0;
 
148
        uint32_t _maxIntervals = 0;
 
149
        PetriEngine::IntervalGenerator intervalGenerator;
120
150
        
121
151
        std::vector<Colored::Place> _places;
122
152
        std::vector<Colored::Transition> _transitions;
123
153
        std::vector<Colored::Arc> _arcs;
 
154
        std::vector<Colored::ColorFixpoint> _placeColorFixpoints;
124
155
        ColorTypeMap _colors;
125
156
        PetriNetBuilder _ptBuilder;
126
157
        bool _unfolded = false;
127
158
        bool _stripped = false;
128
159
 
 
160
        std::vector<uint32_t> _placeFixpointQueue;
 
161
 
129
162
        double _time;
 
163
        double _fixPointCreationTime;
 
164
 
 
165
        double _timer;
130
166
 
131
167
        std::string arcToString(Colored::Arc& arc) const ;
 
168
 
 
169
        void printPlaceTable();
 
170
 
 
171
        std::unordered_map<uint32_t, Colored::ArcIntervals> setupTransitionVars(Colored::Transition transition);
132
172
        
133
173
        void addArc(const std::string& place,
134
174
                const std::string& transition,
135
175
                const Colored::ArcExpression_ptr& expr,
136
176
                bool input);
 
177
 
 
178
 
 
179
        void getArcIntervals(Colored::Transition& transition, bool &transitionActivated, uint32_t max_intervals, uint32_t transitionId);      
 
180
        void processInputArcs(Colored::Transition& transition, uint32_t currentPlaceId, uint32_t transitionId, bool &transitionActivated, uint32_t max_intervals);
 
181
        void processOutputArcs(Colored::Transition& transition);
137
182
        
138
 
        void unfoldPlace(Colored::Place& place);
 
183
        void unfoldPlace(const Colored::Place* place, const PetriEngine::Colored::Color *color);
139
184
        void unfoldTransition(Colored::Transition& transition);
140
 
        void unfoldArc(Colored::Arc& arc, Colored::ExpressionContext::BindingMap& binding, std::string& name);
 
185
        void handleOrphanPlace(Colored::Place& place, std::unordered_map<std::string, uint32_t> unfoldedPlaceMap);
 
186
 
 
187
        void unfoldArc(Colored::Arc& arc, Colored::ExpressionContext::BindingMap& binding, std::string& name, bool input);
141
188
    };
142
189
    
143
 
    class BindingGenerator {
144
 
    public:
145
 
        class Iterator {
146
 
        private:
147
 
            BindingGenerator* _generator;
148
 
            
149
 
        public:
150
 
            Iterator(BindingGenerator* generator);
151
 
            
152
 
            bool operator==(Iterator& other);
153
 
            bool operator!=(Iterator& other);
154
 
            Iterator& operator++();
155
 
            const Colored::ExpressionContext::BindingMap operator++(int);
156
 
            Colored::ExpressionContext::BindingMap& operator*();
157
 
        };
158
 
    private:
159
 
        Colored::GuardExpression_ptr _expr;
160
 
        Colored::ExpressionContext::BindingMap _bindings;
161
 
        ColoredPetriNetBuilder::ColorTypeMap& _colorTypes;
162
 
        
163
 
        bool eval();
164
 
        
165
 
    public:
166
 
        BindingGenerator(Colored::Transition& transition,
167
 
                const std::vector<Colored::Arc>& arcs,
168
 
                ColoredPetriNetBuilder::ColorTypeMap& colorTypes);
 
190
    //Used for checking if a variable is inside either a succ or pred expression
 
191
    enum ExpressionType {
 
192
        None,
 
193
        Pred,
 
194
        Succ
 
195
    };
 
196
 
169
197
 
170
 
        Colored::ExpressionContext::BindingMap& nextBinding();
171
 
        Colored::ExpressionContext::BindingMap& currentBinding();
172
 
        bool isInitial() const;
173
 
        Iterator begin();
174
 
        Iterator end();
175
 
    };
176
198
}
177
199
 
178
200
#endif /* COLOREDPETRINETBUILDER_H */
179