← Back to branch summary

~tapaal-ltl/verifypn/rule-D-fix

« back to all changes in this revision

Viewing changes to PetriEngine/Structures/LimitedStateAllocator.h

  • Committer: Jonas Finnemann Jensen
  • Date: 2011-09-15 13:30:00 UTC
  • Revision ID: jopsen@gmail.com-20110915133000-wnywm1odf82emiuw
Import of sources from github

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriEngine/Structures/LimitedStateAllocator.h
 
1
/* PeTe - Petri Engine exTremE
 
2
 * Copyright (C) 2011  Jonas Finnemann Jensen <jopsen@gmail.com>,
 
3
 *                     Thomas Søndersø Nielsen <primogens@gmail.com>,
 
4
 *                     Lars Kærlund Østergaard <larsko@gmail.com>,
 
5
 * 
 
6
 * This program is free software: you can redistribute it and/or modify
 
7
 * it under the terms of the GNU General Public License as published by
 
8
 * the Free Software Foundation, either version 3 of the License, or
 
9
 * (at your option) any later version.
 
10
 * 
 
11
 * This program is distributed in the hope that it will be useful,
 
12
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 
13
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
14
 * GNU General Public License for more details.
 
15
 * 
 
16
 * You should have received a copy of the GNU General Public License
 
17
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
18
 */
 
19
#ifndef LIMITEDSTATEALLOCATOR_H
 
20
#define LIMITEDSTATEALLOCATOR_H
 
21
 
 
22
#include "../PetriNet.h"
 
23
#include "State.h"
 
24
 
 
25
#include <stdlib.h>
 
26
#include <string.h>
 
27
#include <stdio.h>
 
28
#include <math.h>
 
29
 
 
30
namespace PetriEngine {
 
31
namespace Structures {
 
32
 
 
33
/** State allocator that is limited on memory */
 
34
template<size_t blocksize = 100000>
 
35
class LimitedStateAllocator{
 
36
        struct Block{
 
37
                Block* parent;
 
38
                char* m;
 
39
        } __attribute__((__packed__));
 
40
public:
 
41
        LimitedStateAllocator(const PetriNet& net, int memorylimit = 0){
 
42
                _nPlaces = net.numberOfPlaces();
 
43
                _nVars = net.numberOfVariables();
 
44
                if(memorylimit != 0)
 
45
                        _blocklimit = ceil(memorylimit / (stateSize() * blocksize));
 
46
                else
 
47
                        _blocklimit = -1;
 
48
                _b = NULL;
 
49
                createNewBlock();
 
50
        }
 
51
        ~LimitedStateAllocator(){
 
52
                while(_b){
 
53
                        Block* nb = _b->parent;
 
54
                        delete[] (char*)_b;
 
55
                        _b = nb;
 
56
                }
 
57
        }
 
58
        /** Create new state */
 
59
        State* createState(){
 
60
                if(_offset == blocksize - 1){
 
61
                        if(_blocklimit == 0)
 
62
                                return NULL;
 
63
                        createNewBlock();
 
64
                }
 
65
                char* d = (_b->m + sizeof(Block) + stateSize() * _offset);
 
66
                State* s = (State*)d;
 
67
                s->_parent = NULL;
 
68
                s->_parentTransition = 0;
 
69
                s->_transitionMultiplicity = 0;
 
70
                s->_marking = (MarkVal*)(d + sizeof(State));
 
71
                s->_valuation = (VarVal*)(d + sizeof(State) + sizeof(MarkVal) * _nPlaces);
 
72
                _offset++;
 
73
                return s;
 
74
        }
 
75
private:
 
76
        size_t stateSize(){
 
77
                return sizeof(State) + sizeof(MarkVal) * _nPlaces + sizeof(VarVal) * _nVars;
 
78
        }
 
79
        void createNewBlock(){
 
80
                if(_blocklimit > 0)
 
81
                        _blocklimit--;
 
82
                size_t s = sizeof(Block) + stateSize() * blocksize;
 
83
                char* m = new char[s];
 
84
                memset(m, 0, s);
 
85
                Block* b = (Block*)m;
 
86
                b->parent = _b;
 
87
                b->m = m + sizeof(Block);
 
88
                _b = b;
 
89
                _offset = 0;
 
90
        }
 
91
        size_t _offset;
 
92
        Block* _b;
 
93
        int _nPlaces;
 
94
        int _nVars;
 
95
        int _blocklimit;
 
96
};
 
97
 
 
98
} // Structures
 
99
} // PetriEngine
 
100
 
 
101
#endif // LIMITEDSTATEALLOCATOR_H