← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to src/PetriEngine/Structures/binarywrapper.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/binarywrapper.cpp
 
1
/* VerifyPN - TAPAAL Petri Net Engine
 
2
 * Copyright (C) 2016  Peter Gjøl Jensen <root@petergjoel.dk>
 
3
 * 
 
4
 * This program is free software: you can redistribute it and/or modify
 
5
 * it under the terms of the GNU General Public License as published by
 
6
 * the Free Software Foundation, either version 3 of the License, or
 
7
 * (at your option) any later version.
 
8
 * 
 
9
 * This program is distributed in the hope that it will be useful,
 
10
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 
11
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
12
 * GNU General Public License for more details.
 
13
 * 
 
14
 * You should have received a copy of the GNU General Public License
 
15
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
16
 */
 
17
 
 
18
/* 
 
19
 * File:   binarywrapper.cpp
 
20
 * Author: Peter G. Jensen
 
21
 *
 
22
 * Created on 10 June 2015, 19:20
 
23
 */
 
24
 
 
25
#include "PetriEngine/Structures/binarywrapper.h"
 
26
namespace ptrie
 
27
{
 
28
    
 
29
    const uchar binarywrapper_t::_masks[8] = {
 
30
        static_cast <uchar>(0x80),
 
31
        static_cast <uchar>(0x40),
 
32
        static_cast <uchar>(0x20),
 
33
        static_cast <uchar>(0x10),
 
34
        static_cast <uchar>(0x08),
 
35
        static_cast <uchar>(0x04),
 
36
        static_cast <uchar>(0x02),
 
37
        static_cast <uchar>(0x01)
 
38
    };
 
39
            
 
40
    size_t binarywrapper_t::overhead(uint size)
 
41
    {
 
42
        size = size % 8;
 
43
        if (size == 0)
 
44
            return 0;
 
45
        else
 
46
            return 8 - size; 
 
47
    }
 
48
    
 
49
    
 
50
    size_t binarywrapper_t::bytes(uint size)
 
51
    {
 
52
        return (size + overhead(size))/8;
 
53
    }
 
54
    
 
55
    
 
56
    binarywrapper_t::binarywrapper_t(uint size)
 
57
    {
 
58
        _nbytes = (size + overhead(size)) / 8;
 
59
        _blob = zallocate(_nbytes);
 
60
    }
 
61
    
 
62
    
 
63
    binarywrapper_t::binarywrapper_t(const binarywrapper_t& other, uint offset)
 
64
    {
 
65
         offset = offset / 8;
 
66
 
 
67
        _nbytes = other._nbytes/*.load()*/;
 
68
        if (_nbytes > offset)
 
69
            _nbytes -= offset;
 
70
        else {
 
71
            _nbytes = 0;
 
72
        }
 
73
 
 
74
        _blob = allocate(_nbytes);
 
75
        memcpy(raw(), &(other.const_raw()[offset]), _nbytes);
 
76
        assert(raw()[0] == other.const_raw()[offset]);
 
77
    }
 
78
    
 
79
    binarywrapper_t::binarywrapper_t
 
80
        (uchar* org, uint size, uint offset, uint encodingsize)
 
81
    {
 
82
        if(size == 0 || offset >= encodingsize)
 
83
        {
 
84
            _nbytes = 0;
 
85
            _blob = nullptr;            
 
86
            return;
 
87
        }
 
88
        
 
89
        uint so = size + offset;
 
90
        offset = ((so - 1) / 8) - ((size - 1) / 8);
 
91
 
 
92
        _nbytes = ((encodingsize + this->overhead(encodingsize)) / 8);
 
93
        if (_nbytes > offset)
 
94
            _nbytes -= offset;
 
95
        else {
 
96
            _nbytes = 0;
 
97
            _blob = nullptr;
 
98
            return;
 
99
        }
 
100
 
 
101
        uchar* tmp = &(org[offset]);
 
102
        if(_nbytes <= __BW_BSIZE__)
 
103
        {
 
104
            memcpy(raw(), tmp, _nbytes);            
 
105
        }
 
106
        else
 
107
        {
 
108
            _blob = tmp;
 
109
        }
 
110
        assert(org[offset] == raw()[0]);
 
111
 
 
112
    }
 
113
    
 
114
    
 
115
    binarywrapper_t::binarywrapper_t(uchar* org, uint size)
 
116
    {
 
117
        _nbytes = size / 8 + (size % 8 ? 1 : 0);     
 
118
        _blob = org;
 
119
        
 
120
        if(_nbytes <= __BW_BSIZE__)
 
121
            memcpy(raw(), org, _nbytes);
 
122
        
 
123
//        assert(raw[0] == const_raw()[0]);
 
124
    }
 
125
    
 
126
    
 
127
    void binarywrapper_t::copy(const binarywrapper_t& other, uint offset)
 
128
    {
 
129
        memcpy(&(raw()[offset / 8]), other.const_raw(), other._nbytes);
 
130
        assert(other.const_raw()[0] == raw()[0]);
 
131
    }
 
132
    
 
133
    
 
134
    void binarywrapper_t::copy(const uchar* data, uint size)
 
135
    {
 
136
        if(size > 0)
 
137
        {
 
138
            _blob = allocate(size);
 
139
            _nbytes = size;
 
140
            memcpy(raw(), data, size);
 
141
            assert(data[0] == raw()[0]);
 
142
        }
 
143
        else
 
144
        {
 
145
            _nbytes = 0;
 
146
            release();
 
147
        }
 
148
    }
 
149
        
 
150
    // accessors
 
151
    
 
152
    void binarywrapper_t::print(std::ostream& stream, size_t length) const
 
153
    {
 
154
        stream << _nbytes << " bytes : ";
 
155
        for (size_t i = 0; i < _nbytes * 8 && i < length; i++) {
 
156
            if (i % 8 == 0 && i != 0) stream << "-";
 
157
            stream << this->at(i);
 
158
        }
 
159
    }
 
160
}
 
161
 
 
162
namespace std {
 
163
    std::ostream &operator<<(std::ostream &os, const ptrie::binarywrapper_t &b) {
 
164
        b.print(os);
 
165
        return os;
 
166
    }
 
167
}