← Back to branch summary

~verifydtapn-contributers/verifydtapn/trunk

« back to all changes in this revision

Viewing changes to src/DiscreteVerification/DataStructures/CoveredMarkingVisitor.cpp

  • 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/CoveredMarkingVisitor.cpp
 
1
/* 
 
2
 * File:   CoveredMarkingVisitor.cpp
 
3
 * Author: Peter G. Jensen
 
4
 *
 
5
 * Created on 18 June 2015, 14:23
 
6
 */
 
7
 
 
8
#include "CoveredMarkingVisitor.h"
 
9
 
 
10
 
 
11
using namespace ptrie;
 
12
namespace VerifyTAPN {
 
13
namespace DiscreteVerification {
 
14
 
 
15
    CoveredMarkingVisitor::CoveredMarkingVisitor(
 
16
                            MarkingEncoder<MetaData*, NonStrictMarking>& enc)
 
17
    : encoder(enc), scratchpad(0)
 
18
    {
 
19
        
 
20
    }
 
21
    
 
22
    
 
23
    CoveredMarkingVisitor::~CoveredMarkingVisitor()
 
24
    {
 
25
        scratchpad.release();
 
26
    }
 
27
    
 
28
    void CoveredMarkingVisitor::set_target(NonStrictMarking* m, ptriepointer_t<MetaData*> me)
 
29
    {
 
30
        target = m;
 
31
        _found=false;
 
32
        _targetencoding = me;
 
33
        
 
34
        if(encoder.scratchpad.size() > scratchpad.size())
 
35
        {
 
36
            scratchpad.release();
 
37
            scratchpad = encoder.scratchpad.clone();
 
38
        }
 
39
    }
 
40
    
 
41
    bool CoveredMarkingVisitor::set(int index, bool value)
 
42
    {
 
43
        if(_found) return true;  // end
 
44
        scratchpad.set(index, value);
 
45
        // If we have enough bits to constitute a single token (with placement)
 
46
        if((index + 1) % encoder.offsetBitSize == 0 && index > 0)
 
47
        {
 
48
            size_t begin = (index / encoder.offsetBitSize) * encoder.offsetBitSize;
 
49
            unsigned long long data = 0;
 
50
            uint count = 0;
 
51
            uint cbit = index;
 
52
            
 
53
            while (cbit >= begin + encoder.countBitSize) {
 
54
                data = data << 1;
 
55
                if(scratchpad.at(cbit))
 
56
                {
 
57
                    data |= 1;
 
58
                }
 
59
                --cbit;
 
60
            }
 
61
            
 
62
            while(cbit >= begin)
 
63
            {
 
64
                count = count << 1;
 
65
                if(scratchpad.at(cbit))
 
66
                {
 
67
                    count |= 1;
 
68
                }
 
69
                if(cbit == 0) break;
 
70
                cbit--;
 
71
            }
 
72
            
 
73
            if (count) {
 
74
                return !target_contains_token(data, count);
 
75
            }
 
76
            // should not really happen
 
77
            assert(false);
 
78
            return true;    // skip if happens!
 
79
        }
 
80
        else
 
81
        {
 
82
            return false;   // not enough info
 
83
        }
 
84
    }
 
85
    
 
86
    bool CoveredMarkingVisitor::set_remainder(int index, 
 
87
                                            ptriepointer_t<MetaData*> pointer)
 
88
    {
 
89
        // special case, marking cannot cover itself
 
90
        if(pointer.index == _targetencoding.index) return false;
 
91
        if(_found) return true;  // end
 
92
 
 
93
        encoding_t remainder = pointer.remainder();
 
94
        uint offset = index - (index % 8);  // offset matches on a byte
 
95
        uint begin = (index / encoder.offsetBitSize ) * encoder.offsetBitSize;   // start from whole token
 
96
        // check inclusion 
 
97
 
 
98
        bool bit;
 
99
        
 
100
        while(true)
 
101
        {
 
102
            uint cbit = begin;
 
103
            unsigned long long data = 0;
 
104
            uint count = 0;
 
105
            cbit += encoder.offsetBitSize - 1;
 
106
            // unpack place/age/count
 
107
            while (cbit >= begin + encoder.countBitSize) {
 
108
                data = data << 1;
 
109
 
 
110
                if(cbit < offset) bit = scratchpad.at(cbit);
 
111
                else bit = remainder.at(cbit - offset);
 
112
 
 
113
                if(bit)
 
114
                {
 
115
                    data |= 1;
 
116
                }
 
117
                --cbit;
 
118
            }
 
119
 
 
120
            while(cbit >= begin)
 
121
            {
 
122
                count = count << 1;
 
123
 
 
124
                if(cbit < offset) bit = scratchpad.at(cbit);
 
125
                else bit = remainder.at(cbit - offset);
 
126
 
 
127
                if(bit)
 
128
                {
 
129
                    count |= 1;
 
130
                }
 
131
                if(cbit == 0) break;
 
132
                cbit--;                
 
133
            }
 
134
            begin += encoder.offsetBitSize;
 
135
            if (count) 
 
136
            {
 
137
                if(!target_contains_token(data, count))
 
138
                {
 
139
                    return false;
 
140
                }
 
141
            }
 
142
            else
 
143
            {
 
144
                break;
 
145
            }
 
146
        }
 
147
        
 
148
        match = pointer;
 
149
        _found = true;
 
150
        return true;
 
151
    }
 
152
    
 
153
    bool CoveredMarkingVisitor::back(int index)
 
154
    {
 
155
        return false;
 
156
    }
 
157
    
 
158
    bool CoveredMarkingVisitor::target_contains_token(unsigned long long placeage, uint count)
 
159
    {
 
160
        if(count == 0) return true;
 
161
        
 
162
        int age = floor(placeage / encoder.numberOfPlaces);
 
163
        int place = (placeage % encoder.numberOfPlaces);
 
164
        int cnt = count;
 
165
        const TokenList& tokens = target->getTokenList(place);
 
166
        
 
167
 
 
168
        for(    TokenList::const_iterator it = tokens.begin();
 
169
                it != tokens.end(); ++it)
 
170
        {
 
171
            if(it->getAge() == age)
 
172
            {
 
173
                if(it->getCount() >= cnt) return true; // continue
 
174
                else return false; // skip branch
 
175
            }
 
176
            else if(it->getAge() > age) return false;  // skip branch
 
177
        }
 
178
 
 
179
        return false; // skip branch
 
180
    }
 
181
    
 
182
    NonStrictMarking* CoveredMarkingVisitor::decode()
 
183
    {
 
184
        NonStrictMarking* m = encoder.decode(match);
 
185
        m->meta = match.get_meta();
 
186
        return m;
 
187
    }
 
188
    
 
189
}
 
190
}
 
 
b'\\ No newline at end of file'