← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to PetriEngine/Structures/AlignedEncoder.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/Structures/AlignedEncoder.h
1
 
/* 
2
 
 * File:   Encoder.h
3
 
 * Author: Peter G. Jensen
4
 
 *
5
 
 * Created on 11 March 2016, 14:15
6
 
 */
7
 
 
8
 
 
9
 
#ifndef ALIGNEDENCODER_H
10
 
#define ALIGNEDENCODER_H
11
 
 
12
 
#include <cmath>
13
 
#include "binarywrapper.h"
14
 
 
15
 
using namespace ptrie;
16
 
 
17
 
 
18
 
class AlignedEncoder
19
 
{
20
 
    typedef binarywrapper_t scratchpad_t;
21
 
    public:
22
 
        AlignedEncoder(uint32_t places, uint32_t k);
23
 
 
24
 
        ~AlignedEncoder();
25
 
 
26
 
        size_t encode(const uint32_t* data, unsigned char type);
27
 
 
28
 
        void decode(uint32_t* destination, const unsigned char* source);
29
 
     
30
 
        binarywrapper_t& scratchpad()
31
 
        {
32
 
            return _scratchpad;
33
 
        }
34
 
        
35
 
        unsigned char getType(uint32_t sum, uint32_t pwt, bool same, uint32_t val) const;
36
 
        
37
 
        size_t size(const uchar* data) const;
38
 
private:
39
 
        uint32_t tokenBytes(uint32_t ntokens) const;
40
 
    
41
 
        uint32_t writeBitVector(size_t offset, const uint32_t* data);
42
 
        
43
 
        uint32_t writeTwoBitVector(size_t offset, const uint32_t* data);
44
 
        
45
 
        template<typename T>
46
 
        uint32_t writeTokens(size_t offset, const uint32_t* data);
47
 
        
48
 
        template<typename T>
49
 
        uint32_t writeTokenCounts(size_t offset, const uint32_t* data);
50
 
        
51
 
        uint32_t writePlaces(size_t offset, const uint32_t* data);
52
 
                
53
 
        uint32_t readBitVector(uint32_t* destination, const unsigned char* source, uint32_t offset, uint32_t value);
54
 
 
55
 
        uint32_t readTwoBitVector(uint32_t* destination, const unsigned char* source, uint32_t offset);
56
 
        
57
 
        uint32_t readPlaces(uint32_t* destination, const unsigned char* source, uint32_t offset, uint32_t value);
58
 
                
59
 
        template<typename T>
60
 
        uint32_t readTokens(uint32_t* destination, const unsigned char* source, uint32_t offset);
61
 
        
62
 
        template<typename T>
63
 
        uint32_t readPlaceTokenCounts(uint32_t* destination, const unsigned char* source, uint32_t offset) const;
64
 
 
65
 
        template<typename T>        
66
 
        size_t placeTokenCountsSize(const unsigned char* source, uint32_t offset) const;
67
 
        
68
 
        template<typename T>
69
 
        uint32_t readBitTokenCounts(uint32_t* destination, const unsigned char* source, uint32_t offset) const;
70
 
 
71
 
        template<typename T>        
72
 
        size_t bitTokenCountsSize(const unsigned char* source, uint32_t offset) const;
73
 
        
74
 
        uint32_t _places;
75
 
        
76
 
        uint32_t _psize;
77
 
     
78
 
        // dummy value for template
79
 
        scratchpad_t _scratchpad;
80
 
 
81
 
};
82
 
 
83
 
 
84
 
#endif  /* ALIGNEDENCODER_H */