← Back to branch summary

~verifydtapn-contributers/verifydtapn/trunk

« back to all changes in this revision

Viewing changes to src/DiscreteVerification/DataStructures/MarkingEncoder.h

  • Committer: Jiri Srba
  • Date: 2015-08-31 12:39:10 UTC
  • mfrom: (324.3.24 PTrieWorkflow)
  • Revision ID: srba@cs.aau.dk-20150831123910-qwr9g6pq7zntajhe
merged in a big branch implementing PTrie for workflow analysis

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/DiscreteVerification/DataStructures/MarkingEncoder.h
20
20
namespace VerifyTAPN {
21
21
    namespace DiscreteVerification {
22
22
 
 
23
        class CoveredMarkingVisitor;
 
24
        
23
25
        template<typename T, typename M = NonStrictMarkingBase>
24
26
        class MarkingEncoder
25
27
        {
 
28
        friend class CoveredMarkingVisitor;
26
29
        typedef binarywrapper_t<T> encoding_t;
27
30
 
28
31
        private:
32
35
            const uint countBitSize;
33
36
            const uint placeAgeBitSize;
34
37
            const uint offsetBitSize; 
35
 
            uint markingBitSize;
 
38
            const uint markingBitSize;
36
39
            TAPN::TimedArcPetriNet& tapn;
37
40
            encoding_t scratchpad;
38
 
            void* raw;
39
41
        public:
40
42
            MarkingEncoder(TAPN::TimedArcPetriNet& tapn, int knumber,
41
43
                                                        int nplaces, int mage);
58
60
            markingBitSize(offsetBitSize * (knumber ? knumber : 1)),
59
61
            tapn(tapn)
60
62
        {
61
 
                scratchpad = encoding_t(markingBitSize);
62
 
                raw = (void*)scratchpad.raw();
 
63
                scratchpad = encoding_t(0);
63
64
        }
64
65
        
65
66
        template<typename T, typename M>
71
72
        template<typename T, typename M>
72
73
        M* MarkingEncoder<T, M>::decode(const ptriepointer_t<T>& pointer)
73
74
        {
74
 
            assert(scratchpad.raw() == raw);
 
75
            // we allready know here that the scratchpad is large enough,
 
76
            // it is monotonically increased when we encode, ie; no marking
 
77
            // taking up more bits are currently in the ptrie.
 
78
            
75
79
            M* m = new M();
76
80
            assert(pointer.container->consistent());
77
81
            const encoding_t remainder = pointer.remainder();
81
85
            
82
86
            uint cbit = 0;
83
87
            // foreach token
84
 
            uint data = 0;
85
 
            uint count = 0;
 
88
      
86
89
            bool bit;
87
90
            for (uint i = 0; i < maxNumberOfTokens; i++) {
88
91
                uint offset = offsetBitSize * i;
89
92
                cbit = offset + offsetBitSize - 1;
 
93
                unsigned long long data = 0;
 
94
                uint count = 0;
90
95
                
91
96
                while (cbit >= offset + countBitSize) {
92
97
                    data = data << 1;
137
142
                    uint place = (data % this->numberOfPlaces);
138
143
                    Token t = Token(age, count);
139
144
                    m->addTokenInPlace(tapn.getPlace(place), t);
140
 
                    data = 0;
141
 
                    count = 0;
142
145
                }
143
146
                else
144
147
                {
157
160
        template<typename T, typename M>
158
161
        binarywrapper_t<T> MarkingEncoder<T, M>::encode(M* marking)
159
162
        {
 
163
            // make sure we have space to encode marking
 
164
            size_t count = 0;
 
165
            for (vector<Place>::const_iterator pi = marking->getPlaceList().begin();
 
166
                    pi != marking->getPlaceList().end();
 
167
                    pi++) {
 
168
                count += pi->tokens.size();
 
169
            }
 
170
            count *= offsetBitSize;
 
171
            count /= 8;
 
172
            count += 1;
 
173
            
 
174
            if(scratchpad.size() < count)
 
175
            {
 
176
                scratchpad.release();
 
177
                scratchpad = encoding_t(count * 8);
 
178
            }
 
179
            
 
180
 
 
181
 
160
182
            scratchpad.zero();
161
183
            int tc = 0;
162
184
            uint bitcount = 0;