← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to src/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:
src/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 "PetriEngine/Structures/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
}