← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to include/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:
include/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 */