← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to PetriEngine/Reducer.h

  • Committer: srba.jiri at gmail
  • Date: 2020-09-11 14:23:39 UTC
  • mfrom: (213.1.151 interval_tar)
  • Revision ID: srba.jiri@gmail.com-20200911142339-bq9328s1gppw24uj
merged in lp:~verifypn-maintainers/verifypn/interval_tar doing 
- Implements TAR w/o z3, but using a simple integer inference engine for Hoare logic.
 - Replaces LP-Solve with GLPK, reduces computation-time and memory overhead
 - Implements new global properties, translated into CTL formulae.

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriEngine/Reducer.h
1
 
/* 
2
 
 * File:   Reducer.h
3
 
 * Author: srba
4
 
 *
5
 
 * Created on 15 February 2014, 10:50
6
 
 */
7
 
 
8
 
#ifndef REDUCER_H
9
 
#define REDUCER_H
10
 
 
11
 
#include "PetriNet.h"
12
 
#include "PQL/Contexts.h"
13
 
#include "PetriParse/PNMLParser.h"
14
 
#include "NetStructures.h"
15
 
 
16
 
namespace PetriEngine {
17
 
 
18
 
    using ArcIter = std::vector<Arc>::iterator;
19
 
    
20
 
    class PetriNetBuilder;
21
 
        
22
 
    class QueryPlaceAnalysisContext : public PQL::AnalysisContext {
23
 
        std::vector<uint32_t> _placeInQuery;
24
 
        bool _deadlock;
25
 
    public:
26
 
 
27
 
        QueryPlaceAnalysisContext(const std::unordered_map<std::string, uint32_t>& pnames, const std::unordered_map<std::string, uint32_t>& tnames, const PetriNet* net) 
28
 
        : PQL::AnalysisContext(pnames, tnames, net) {
29
 
            _placeInQuery.resize(_placeNames.size(), 0);
30
 
            _deadlock = false;
31
 
        };
32
 
        
33
 
        virtual ~QueryPlaceAnalysisContext()
34
 
        {
35
 
        }
36
 
        
37
 
        uint32_t*  getQueryPlaceCount(){
38
 
            return _placeInQuery.data();
39
 
        }
40
 
 
41
 
        bool hasDeadlock() { return _deadlock; }
42
 
        
43
 
        virtual void setHasDeadlock() override {
44
 
            _deadlock = true;
45
 
        };
46
 
        
47
 
        ResolutionResult resolve(const std::string& identifier, bool place) override {
48
 
            if(!place) return PQL::AnalysisContext::resolve(identifier, false);
49
 
            ResolutionResult result;
50
 
            result.offset = -1;
51
 
            result.success = false;
52
 
            auto it = _placeNames.find(identifier);
53
 
            if(it != _placeNames.end())
54
 
            {
55
 
                uint32_t i = it->second;
56
 
                result.offset = (int)i;
57
 
                result.success = true;
58
 
                _placeInQuery[i]++;
59
 
                return result;
60
 
            }
61
 
            
62
 
            return result;
63
 
        }
64
 
 
65
 
    };
66
 
 
67
 
   struct ExpandedArc
68
 
   {
69
 
       ExpandedArc(std::string place, size_t weight) : place(place), weight(weight) {}
70
 
       
71
 
        friend std::ostream& operator<<(std::ostream& os, ExpandedArc const & ea) {
72
 
            for(size_t i = 0; i < ea.weight; ++i)
73
 
            {
74
 
                os << "\t\t<token place=\"" << ea.place << "\" age=\"0\"/>\n";
75
 
            }
76
 
            return os;
77
 
        }
78
 
       
79
 
        std::string place;        
80
 
        size_t weight;
81
 
   };
82
 
    
83
 
    class Reducer {
84
 
    public:
85
 
        Reducer(PetriNetBuilder*);
86
 
        ~Reducer();
87
 
        void Print(QueryPlaceAnalysisContext& context); // prints the net, just for debugging
88
 
        void Reduce(QueryPlaceAnalysisContext& context, int enablereduction, bool reconstructTrace, int timeout, bool remove_loops, bool remove_consumers, bool next_safe);
89
 
        
90
 
        size_t RemovedTransitions() const {
91
 
            return _removedTransitions;
92
 
        }
93
 
 
94
 
        size_t RemovedPlaces() const {
95
 
            return _removedPlaces;
96
 
        }
97
 
 
98
 
        void printStats(std::ostream& out)
99
 
        {
100
 
            out << "Removed transitions: " << _removedTransitions << "\n"
101
 
                << "Removed places: " << _removedPlaces << "\n"
102
 
                << "Applications of rule A: " << _ruleA << "\n"
103
 
                << "Applications of rule B: " << _ruleB << "\n"
104
 
                << "Applications of rule C: " << _ruleC << "\n"
105
 
                << "Applications of rule D: " << _ruleD << "\n"
106
 
                << "Applications of rule E: " << _ruleE << "\n"
107
 
                << "Applications of rule F: " << _ruleF << "\n"
108
 
                << "Applications of rule G: " << _ruleG << "\n"
109
 
                << "Applications of rule H: " << _ruleH << "\n"
110
 
                << "Applications of rule I: " << _ruleI << std::endl;
111
 
        }
112
 
 
113
 
        void postFire(std::ostream&, const std::string& transition);
114
 
        void extraConsume(std::ostream&, const std::string& transition);
115
 
        void initFire(std::ostream&);
116
 
 
117
 
    private:
118
 
        size_t _removedTransitions = 0;
119
 
        size_t _removedPlaces= 0;
120
 
        size_t _ruleA = 0, _ruleB = 0, _ruleC = 0, _ruleD = 0, _ruleE = 0, _ruleF = 0, _ruleG = 0, _ruleH = 0, _ruleI = 0;
121
 
        PetriNetBuilder* parent = nullptr;
122
 
        bool reconstructTrace = false;
123
 
        std::chrono::high_resolution_clock::time_point _timer;
124
 
        int _timeout = 0;
125
 
 
126
 
        // The reduction methods return true if they reduced something and reductions should continue with other rules
127
 
        bool ReducebyRuleA(uint32_t* placeInQuery);
128
 
        bool ReducebyRuleB(uint32_t* placeInQuery);
129
 
        bool ReducebyRuleC(uint32_t* placeInQuery);
130
 
        bool ReducebyRuleD(uint32_t* placeInQuery);
131
 
        bool ReducebyRuleE(uint32_t* placeInQuery);
132
 
        bool ReducebyRuleI(uint32_t* placeInQuery, bool remove_loops, bool remove_consumers);
133
 
        bool ReducebyRuleF(uint32_t* placeInQuery);
134
 
        bool ReducebyRuleG(uint32_t* placeInQuery, bool remove_loops, bool remove_consumers);
135
 
        bool ReducebyRuleH(uint32_t* placeInQuery);
136
 
        
137
 
        std::string getTransitionName(uint32_t transition);
138
 
        std::string getPlaceName(uint32_t place);
139
 
        
140
 
        Transition& getTransition(uint32_t transition);
141
 
        ArcIter getOutArc(Transition&, uint32_t place);
142
 
        ArcIter getInArc(uint32_t place, Transition&);
143
 
        void eraseTransition(std::vector<uint32_t>&, uint32_t);
144
 
        void skipTransition(uint32_t);
145
 
        void skipPlace(uint32_t);
146
 
        
147
 
        bool consistent();
148
 
        bool hasTimedout() const {
149
 
            auto end = std::chrono::high_resolution_clock::now();
150
 
            auto diff = std::chrono::duration_cast<std::chrono::seconds>(end - _timer);
151
 
            return (diff.count() >= _timeout);
152
 
        }
153
 
        
154
 
        std::vector<std::string> _initfire;
155
 
        std::unordered_map<std::string, std::vector<std::string>> _postfire;
156
 
        std::unordered_map<std::string, std::vector<ExpandedArc>> _extraconsume;
157
 
    };
158
 
 
159
 
    
160
 
 
161
 
 
162
 
}
163
 
 
164
 
 
165
 
#endif /* REDUCER_H */
166