← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to PetriEngine/Structures/AlignedEncoder.cpp

  • 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/Structures/AlignedEncoder.cpp
1
 
/* 
2
 
 * File:   Encoder.cpp
3
 
 * Author: Peter G. Jensen
4
 
 * 
5
 
 * Created on 11 March 2016, 14:15
6
 
 */
7
 
 
8
 
#include <limits>
9
 
 
10
 
#include "AlignedEncoder.h"
11
 
 
12
 
#define SAMEBOUND 120
13
 
#define DBOUND (SAMEBOUND*2)
14
 
 
15
 
AlignedEncoder::AlignedEncoder(uint32_t places, uint32_t k)
16
 
: _places(places)
17
 
{
18
 
 
19
 
    size_t bytes = 2*sizeof(uint32_t) + (places*sizeof(uint32_t));
20
 
    _scratchpad = scratchpad_t(bytes*8);
21
 
    assert(_scratchpad.size() == (2*sizeof(uint32_t) + (_places*sizeof(uint32_t))));
22
 
    if(_places < 256) _psize = 1;
23
 
    else if(_places < 65536) _psize = 2;
24
 
    else _psize = 4;
25
 
 
26
 
    assert(_psize != 0);
27
 
}
28
 
 
29
 
AlignedEncoder::~AlignedEncoder()
30
 
{
31
 
    _scratchpad.release();
32
 
}
33
 
 
34
 
uint32_t AlignedEncoder::tokenBytes(uint32_t ntokens) const
35
 
{
36
 
    uint32_t size = 0;
37
 
    if(ntokens < 256) size = 1;
38
 
    else if(ntokens < 65536) size = 2;
39
 
    else size = 4;
40
 
    return size;
41
 
}
42
 
 
43
 
uint32_t AlignedEncoder::writeBitVector(size_t offset, const uint32_t* data)
44
 
{
45
 
    for(size_t i = 0; i < _places; ++i)
46
 
    {
47
 
        _scratchpad.set(i+(offset*8), data[i] > 0);
48
 
    }
49
 
    return offset + scratchpad_t::bytes(_places);
50
 
}
51
 
 
52
 
uint32_t AlignedEncoder::writeTwoBitVector(size_t offset, const uint32_t* data)
53
 
{
54
 
    for(size_t i = 0; i < _places; ++i)
55
 
    {
56
 
        switch(data[i])
57
 
        {
58
 
            case 1:
59
 
                _scratchpad.set((i*2)+(offset*8), true);
60
 
                break;
61
 
            case 3:
62
 
                _scratchpad.set((i*2)+(offset*8), true);                
63
 
            case 2:
64
 
                _scratchpad.set((i*2)+(offset*8)+1, true);                                
65
 
                break;
66
 
            default:                
67
 
                break;
68
 
            
69
 
        }
70
 
    }
71
 
 
72
 
    return offset + scratchpad_t::bytes(_places*2);
73
 
}
74
 
 
75
 
uint32_t AlignedEncoder::readTwoBitVector(uint32_t* destination, const unsigned char* source, uint32_t offset)
76
 
{
77
 
    scratchpad_t b = scratchpad_t((unsigned char*)&source[offset], _places*2);
78
 
    for(size_t i = 0; i < _places; ++i)
79
 
    {
80
 
        destination[i] = 0;
81
 
        if(b.at((i*2)))
82
 
        {
83
 
            destination[i] = 1;
84
 
        }
85
 
        
86
 
        if(b.at((i*2)+1))
87
 
        {
88
 
            destination[i] += 2;
89
 
        }
90
 
    }
91
 
    return offset + scratchpad_t::bytes(_places*2);
92
 
}
93
 
 
94
 
template<typename T>
95
 
uint32_t AlignedEncoder::writeTokens(size_t offset, const uint32_t* data)
96
 
{
97
 
    if(sizeof(T) == sizeof(uint32_t))
98
 
    {
99
 
        memcpy(&(_scratchpad.raw()[offset]), data, _places*sizeof(T));        
100
 
    } 
101
 
    else
102
 
    {
103
 
        for(size_t i = 0; i < _places; ++i)
104
 
        {
105
 
            T* dest = (T*)(&_scratchpad.raw()[offset + (i*sizeof(T))]);
106
 
            *dest = data[i];
107
 
        }
108
 
    }
109
 
    return offset + _places*sizeof(T);
110
 
}
111
 
 
112
 
template<typename T>
113
 
uint32_t AlignedEncoder::readTokens(uint32_t* destination, const unsigned char* source, uint32_t offset)
114
 
{
115
 
    for(size_t i = 0; i < _places; ++i)
116
 
    {
117
 
        T* src = (T*)(&source[offset + (i*sizeof(T))]);
118
 
        destination[i] = *src;
119
 
    }
120
 
    return offset + _places*sizeof(T);
121
 
}
122
 
 
123
 
template<typename T>
124
 
uint32_t AlignedEncoder::writeTokenCounts(size_t offset, const uint32_t* data)
125
 
{
126
 
    size_t cnt = 0;
127
 
 
128
 
    for(size_t i = 0; i < _places; ++i)
129
 
    {
130
 
        if(data[i] > 0)
131
 
        {
132
 
            T* dest = (T*)(&_scratchpad.raw()[offset + (cnt*sizeof(T))]);
133
 
            *dest = data[i];
134
 
            ++cnt;
135
 
        }
136
 
    }
137
 
    return offset + cnt*sizeof(T);
138
 
}
139
 
 
140
 
template<typename T>
141
 
size_t AlignedEncoder::bitTokenCountsSize(const unsigned char* source, uint32_t offset) const
142
 
{
143
 
    scratchpad_t b = scratchpad_t((unsigned char*)&source[offset], _places);
144
 
 
145
 
    size_t cnt = 0;
146
 
    for(uint32_t i = 0; i < _places; ++i)
147
 
    {
148
 
        if(b.at(i))
149
 
        {
150
 
            cnt += sizeof(T);
151
 
        }
152
 
    }
153
 
    return offset + b.size() + cnt;
154
 
}
155
 
 
156
 
template<typename T>
157
 
uint32_t AlignedEncoder::readBitTokenCounts(uint32_t* destination, const unsigned char* source, uint32_t offset) const
158
 
{
159
 
    const unsigned char* ts = &source[offset + scratchpad_t::bytes(_places)];
160
 
    scratchpad_t b = scratchpad_t((unsigned char*)&source[offset], _places);
161
 
 
162
 
    size_t cnt = 0;
163
 
    for(uint32_t i = 0; i < _places; ++i)
164
 
    {
165
 
        if(b.at(i))
166
 
        {
167
 
            destination[i] = *((T*)&ts[cnt]);
168
 
            cnt += sizeof(T);
169
 
        }
170
 
    }
171
 
    return 0;
172
 
}
173
 
 
174
 
template<typename T>
175
 
size_t AlignedEncoder::placeTokenCountsSize(const unsigned char* source, uint32_t offset) const
176
 
{
177
 
    size_t size;
178
 
    switch(_psize)
179
 
    {
180
 
        case 1:
181
 
            size = source[offset];
182
 
            break;
183
 
        case 2:
184
 
            size = *(uint16_t*)(&source[offset]);
185
 
            break;                           
186
 
        case 4:
187
 
            size = *(uint32_t*)(&source[offset]);
188
 
            break;   
189
 
        default:
190
 
            size = std::numeric_limits<size_t>::max(); // should provoke an error
191
 
            assert(false);
192
 
    }
193
 
    offset += _psize;
194
 
    return offset + (_psize * size) + (size*sizeof(T));
195
 
}
196
 
 
197
 
template<typename T>
198
 
uint32_t AlignedEncoder::readPlaceTokenCounts(uint32_t* destination, const unsigned char* source, uint32_t offset) const
199
 
{
200
 
    size_t size;
201
 
    switch(_psize)
202
 
    {
203
 
        case 1:
204
 
            size = source[offset];
205
 
            break;
206
 
        case 2:
207
 
            size = *(uint16_t*)(&source[offset]);
208
 
            break;                           
209
 
        case 4:
210
 
            size = *(uint32_t*)(&source[offset]);
211
 
            break;   
212
 
        default:
213
 
            size = std::numeric_limits<size_t>::max(); // should provoke an error
214
 
            assert(false);
215
 
    }
216
 
    
217
 
    offset += _psize;
218
 
    const unsigned char* ts = &source[offset + (_psize*size)];
219
 
    for(size_t i = 0; i < size; ++i)
220
 
    {
221
 
        size_t pos = 0;
222
 
        switch(_psize)
223
 
        {
224
 
            case 1:
225
 
                pos = source[offset + i];
226
 
                break;                
227
 
            case 2:
228
 
                pos = *((uint16_t*)&source[offset + i*2]);
229
 
                break;                
230
 
            case 4:
231
 
                pos = *((uint32_t*)&source[offset + i*4]);
232
 
                break;
233
 
            default:
234
 
                assert(false);
235
 
                break;
236
 
        }
237
 
        
238
 
        destination[pos] = *((T*)&ts[i*sizeof(T)]);     
239
 
    }
240
 
    return offset + size;
241
 
}
242
 
 
243
 
uint32_t AlignedEncoder::writePlaces(size_t offset, const uint32_t* data)
244
 
{
245
 
    size_t cnt = 0;
246
 
    uint16_t* dest16 = (uint16_t*)(&_scratchpad.raw()[offset]);
247
 
    uint32_t* dest32 = (uint32_t*)(&_scratchpad.raw()[offset]);
248
 
    for(size_t i = 0; i < _places; ++i)
249
 
    {
250
 
        if(data[i] > 0)
251
 
        {
252
 
            switch(_psize)
253
 
            {
254
 
                case 1:
255
 
                    _scratchpad.raw()[offset + cnt + 1] = (unsigned char)i;
256
 
                    break;
257
 
                case 2:
258
 
                    dest16[cnt+1] = (uint16_t)i;
259
 
                    break;  
260
 
                case 4:
261
 
                    dest32[cnt+1] = i;
262
 
                    break;                   
263
 
                default:
264
 
                    assert(false);
265
 
            }
266
 
            ++cnt;
267
 
        }
268
 
        
269
 
    }
270
 
    
271
 
    switch(_psize)
272
 
    {
273
 
        case 1:
274
 
            _scratchpad.raw()[offset] = (unsigned char)cnt;
275
 
            break;
276
 
        case 2:
277
 
            dest16[0] = cnt;
278
 
            break;            
279
 
        case 4:
280
 
            dest32[0] = cnt;
281
 
            break;
282
 
        default:
283
 
            assert(false);
284
 
    }
285
 
    return offset + _psize + cnt*_psize; 
286
 
}
287
 
 
288
 
uint32_t AlignedEncoder::readPlaces(uint32_t* destination, const unsigned char* source, uint32_t offset, uint32_t value)
289
 
{
290
 
    size_t size;
291
 
    switch(_psize)
292
 
    {
293
 
        case 1:
294
 
            size = source[offset];
295
 
            break;
296
 
        case 2:
297
 
            size = *(uint16_t*)(&source[offset]);
298
 
            break;                           
299
 
        case 4:
300
 
            size = *(uint32_t*)(&source[offset]);
301
 
            break;   
302
 
        default:
303
 
            size = std::numeric_limits<size_t>::max(); // should provoke an error
304
 
            assert(false);
305
 
    }
306
 
    
307
 
    offset += _psize;
308
 
    
309
 
    uint16_t* raw16 = (uint16_t*) &source[offset];
310
 
    uint32_t* raw32 = (uint32_t*) &source[offset];
311
 
    for(size_t i = 0; i < size; ++i)
312
 
    {
313
 
        switch(_psize)
314
 
        {
315
 
            case 1:
316
 
                destination[source[i+offset]] = value;
317
 
                break;
318
 
            case 2:
319
 
                 destination[raw16[i]] = value;
320
 
                break;
321
 
            case 4:
322
 
                destination[raw32[i]] = value;
323
 
                break;                
324
 
            default:
325
 
                assert(false);
326
 
        }
327
 
    }
328
 
    return offset + _psize*size;
329
 
}
330
 
 
331
 
uint32_t AlignedEncoder::readBitVector(uint32_t* destination, const unsigned char* source, uint32_t offset, uint32_t value)
332
 
{
333
 
    scratchpad_t b = scratchpad_t((unsigned char*)&source[offset], _places);
334
 
    for(uint32_t i = 0; i < _places; ++i)
335
 
    {
336
 
        if(b.at(i))
337
 
        {
338
 
            destination[i] = value;
339
 
        }
340
 
        else
341
 
        {
342
 
            destination[i] = 0;
343
 
        }
344
 
    }
345
 
    return offset + b.size();
346
 
}
347
 
 
348
 
unsigned char AlignedEncoder::getType(uint32_t sum, uint32_t pwt, bool same, uint32_t val) const
349
 
{
350
 
    if(pwt == 0) return 0;
351
 
    if(same && val <= SAMEBOUND)
352
 
    {
353
 
        size_t bvsize = scratchpad_t::bytes(_places);
354
 
        size_t indirect = _psize+pwt*_psize;
355
 
        
356
 
        if(bvsize <= indirect)
357
 
        {
358
 
            return val;
359
 
        }
360
 
        else
361
 
        {
362
 
            return SAMEBOUND+val;            
363
 
        }
364
 
    }
365
 
    else
366
 
    {
367
 
        size_t tsize = tokenBytes(val);
368
 
        size_t bvsize = scratchpad_t::bytes(_places*2);
369
 
        size_t indirect = _psize+pwt*(_psize+tsize);   
370
 
        size_t bvindirect = scratchpad_t::bytes(_places)+pwt*tsize;
371
 
        size_t direct = _places*tsize;
372
 
        
373
 
        if(val < 4 && bvsize <= indirect && bvsize <= bvindirect)
374
 
        {
375
 
            return DBOUND+1;
376
 
        }
377
 
        else if(direct <= indirect && direct <= bvindirect)
378
 
        {
379
 
            switch(tsize)
380
 
            {
381
 
                case 1:
382
 
                    return DBOUND+2;       
383
 
                case 2:
384
 
                    return DBOUND+3;                 
385
 
                case 4:
386
 
                    return DBOUND+4;                
387
 
                default:
388
 
                    assert(false);
389
 
            }
390
 
        }
391
 
        else if(indirect <= bvindirect)
392
 
        {
393
 
            switch(tsize)
394
 
            {
395
 
                case 1:
396
 
                    return DBOUND+5;     
397
 
                case 2:
398
 
                    return DBOUND+6;                
399
 
                case 4:
400
 
                    return DBOUND+7;
401
 
                default:
402
 
                    assert(false);
403
 
            }
404
 
        } 
405
 
        else
406
 
        {
407
 
            switch(tsize)
408
 
            {
409
 
                case 1:
410
 
                    return DBOUND+8;                
411
 
                case 2:
412
 
                    return DBOUND+9;
413
 
                case 4:
414
 
                    return DBOUND+10;
415
 
                default:
416
 
                    assert(false);
417
 
            }
418
 
        }
419
 
    }
420
 
    assert(false);
421
 
    return 0;
422
 
}
423
 
 
424
 
size_t AlignedEncoder::size(const uchar* s) const
425
 
{
426
 
    unsigned char type = s[0];
427
 
    if(type <= SAMEBOUND)
428
 
    {
429
 
        if((_places % 8) == 0) return 1 + (_places / 8);
430
 
        else return 2 + (_places / 8);
431
 
    }
432
 
    
433
 
    if(type <= DBOUND)
434
 
    {
435
 
        size_t size;
436
 
        switch(_psize)
437
 
        {
438
 
            case 1:
439
 
                size = 1 + s[1];
440
 
                break;
441
 
            case 2:
442
 
                size = 1 + *(uint16_t*)(&s[1]);
443
 
                size *= sizeof(uint16_t);
444
 
                break;                           
445
 
            case 4:
446
 
                size = 1 + *(uint32_t*)(&s[1]);
447
 
                size *= sizeof(uint32_t);
448
 
                break;   
449
 
            default:
450
 
                size = std::numeric_limits<size_t>::max(); // should provoke an error
451
 
                assert(false);
452
 
        }
453
 
        return size + 1;
454
 
    }
455
 
    
456
 
    switch(type)
457
 
    {
458
 
        case DBOUND+1:
459
 
            if((_places % 4) == 0) return 1 + (_places / 4);
460
 
            else return 2 + (_places / 4);
461
 
        case DBOUND+2:
462
 
            return 1 + (sizeof(unsigned char)*_places);
463
 
        case DBOUND+3:
464
 
            return 1 + (sizeof(uint16_t)*_places);
465
 
        case DBOUND+4:
466
 
            return 1 + (sizeof(uint32_t)*_places);
467
 
        case DBOUND+5:
468
 
            return placeTokenCountsSize<unsigned char>((unsigned char*)s, 1); 
469
 
        case DBOUND+6:
470
 
            return placeTokenCountsSize<uint16_t>((unsigned char*)s, 1); 
471
 
        case DBOUND+7:
472
 
            return placeTokenCountsSize<uint32_t>((unsigned char*)s, 1); 
473
 
        case DBOUND+8:
474
 
            return bitTokenCountsSize<unsigned char>((unsigned char*)s, 1);
475
 
        case DBOUND+9:
476
 
            return bitTokenCountsSize<uint16_t>((unsigned char*)s, 1);
477
 
        case DBOUND+10:
478
 
            return bitTokenCountsSize<uint32_t>((unsigned char*)s, 1);
479
 
        default:
480
 
            assert(false);
481
 
            return std::numeric_limits<size_t>::infinity();
482
 
    }
483
 
}
484
 
 
485
 
size_t AlignedEncoder::encode(const uint32_t* d, unsigned char type)
486
 
{
487
 
    _scratchpad.zero();
488
 
    _scratchpad.raw()[0] = type;
489
 
    if(type <= SAMEBOUND)
490
 
    {
491
 
        return writeBitVector(1, d);
492
 
    }
493
 
    if(type <= DBOUND)
494
 
    {
495
 
        return writePlaces(1, d);
496
 
    }
497
 
    
498
 
    switch(type)
499
 
    {
500
 
        case DBOUND+1:
501
 
            return writeTwoBitVector(1,d);
502
 
        case DBOUND+2:
503
 
            return writeTokens<unsigned char>(1, d);           
504
 
        case DBOUND+3:
505
 
            return writeTokens<uint16_t>(1, d);
506
 
        case DBOUND+4:
507
 
            return writeTokens<uint32_t>(1, d); 
508
 
        case DBOUND+5:
509
 
            {
510
 
                size_t size = writePlaces(1, d);
511
 
                return writeTokenCounts<unsigned char>(size, d);
512
 
            }
513
 
        case DBOUND+6:
514
 
            {
515
 
                size_t size = writePlaces(1, d);
516
 
                return writeTokenCounts<uint16_t>(size, d);
517
 
            }
518
 
        case DBOUND+7:
519
 
            {
520
 
                size_t size = writePlaces(1, d);
521
 
                return writeTokenCounts<uint32_t>(size, d);
522
 
            }           
523
 
        case DBOUND+8:
524
 
            {
525
 
                size_t size = writeBitVector(1, d);
526
 
                return writeTokenCounts<unsigned char>(size, d);
527
 
            }
528
 
        case DBOUND+9:
529
 
            {
530
 
                size_t size = writeBitVector(1, d);
531
 
                return writeTokenCounts<uint16_t>(size, d);
532
 
            }
533
 
        case DBOUND+10:
534
 
            {
535
 
                size_t size = writeBitVector(1, d);
536
 
                return writeTokenCounts<uint32_t>(size, d);
537
 
            }
538
 
        default:
539
 
            assert(false);
540
 
    }
541
 
    assert(false);
542
 
    return 0;
543
 
}
544
 
 
545
 
void AlignedEncoder::decode(uint32_t* d, const unsigned char* s)
546
 
{
547
 
    memset(d, 0, sizeof(uint32_t)*_places);
548
 
    unsigned char type = s[0];
549
 
    if(type <= SAMEBOUND)
550
 
    {
551
 
        readBitVector(d, s, 1, type);
552
 
        return;
553
 
    }
554
 
    if(type <= DBOUND)
555
 
    {
556
 
        readPlaces(d, s, 1, type - SAMEBOUND);
557
 
        return;
558
 
    }
559
 
    
560
 
    switch(type)
561
 
    {
562
 
        case DBOUND+1:
563
 
            readTwoBitVector(d,s,1);
564
 
            return;
565
 
        case DBOUND+2:
566
 
            readTokens<unsigned char>(d,s,1);
567
 
            return;
568
 
        case DBOUND+3:
569
 
            readTokens<uint16_t>(d,s,1);
570
 
            return;
571
 
        case DBOUND+4:
572
 
            readTokens<uint32_t>(d,s,1);
573
 
            return;
574
 
        case DBOUND+5:
575
 
            readPlaceTokenCounts<unsigned char>(d, s, 1); 
576
 
            return;
577
 
        case DBOUND+6:
578
 
            readPlaceTokenCounts<uint16_t>(d, s, 1); 
579
 
            return;
580
 
        case DBOUND+7:
581
 
            readPlaceTokenCounts<uint32_t>(d, s, 1); 
582
 
            return;
583
 
        case DBOUND+8:
584
 
            readBitTokenCounts<unsigned char>(d, s, 1);
585
 
            return;
586
 
        case DBOUND+9:
587
 
            readBitTokenCounts<uint16_t>(d, s, 1);
588
 
            return;
589
 
        case DBOUND+10:
590
 
            readBitTokenCounts<uint32_t>(d, s, 1);
591
 
            return;
592
 
        default:
593
 
            assert(false);
594
 
    }
595
 
}