← Back to branch summary

~verifypn-cpn/verifypn/colored

« back to all changes in this revision

Viewing changes to PetriEngine/PetriNet.cpp

  • 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/PetriNet.cpp
 
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
#include "PetriNet.h"
 
20
#include "PQL/PQL.h"
 
21
#include "PQL/Contexts.h"
 
22
#include "Structures/State.h"
 
23
 
 
24
#include <stdio.h>
 
25
#include <stdlib.h>
 
26
#include <string.h>
 
27
using namespace std;
 
28
 
 
29
namespace PetriEngine{
 
30
 
 
31
PetriNet::PetriNet(int places, int transitions, int variables)
 
32
        : _places(places), _transitions(transitions), _variables(variables) {
 
33
        //Store size for later
 
34
        _nPlaces = places;
 
35
        _nTransitions = transitions;
 
36
        _nVariables = variables;
 
37
 
 
38
        //Allocate space for ranges
 
39
        _ranges = new VarVal[variables];
 
40
 
 
41
        //Allocate space for conditions and assignments
 
42
        size_t s = (sizeof(PQL::Condition*) + sizeof(PQL::AssignmentExpression*)) * transitions;
 
43
        char* d = new char[s];
 
44
        memset(d, 0, s);
 
45
        _conditions = (PQL::Condition**)d;
 
46
        _assignments = (PQL::AssignmentExpression**)(d + sizeof(PQL::Condition*)*transitions);
 
47
 
 
48
        //Allocate transition matrix
 
49
        _tm = new MarkVal[places * transitions * 2];
 
50
        for(int i = 0; i < places * transitions * 2; i++)
 
51
                _tm[i] = 0;
 
52
}
 
53
 
 
54
PetriNet::~PetriNet(){
 
55
        if(_ranges)
 
56
                delete[] _ranges;
 
57
        _ranges = NULL;
 
58
        if(_tm)
 
59
                delete[] _tm;
 
60
        _tm = NULL;
 
61
        //Conditions and assignments is allocated in the same block
 
62
        if(_conditions)
 
63
                delete[] (char*)_conditions;
 
64
        _conditions = NULL;
 
65
        _assignments = NULL;
 
66
}
 
67
 
 
68
bool PetriNet::fire(unsigned int t,
 
69
                                        const MarkVal* m,
 
70
                                        const VarVal* a,
 
71
                                        MarkVal* result_m,
 
72
                                        VarVal* result_a) const{
 
73
        //Check the condition
 
74
        if(_conditions[t] &&
 
75
           !_conditions[t]->evaluate(PQL::EvaluationContext(m, a)))
 
76
                return false;
 
77
 
 
78
        const MarkVal* tv = _tv(t);
 
79
        //Check that we can take from the marking
 
80
        for(size_t i = 0; i < _nPlaces; i++){
 
81
                result_m[i] = m[i] - tv[i];
 
82
                if(result_m[i] < 0)
 
83
                        return false;
 
84
        }
 
85
        //Add stuff that the marking gives us
 
86
        for(size_t i = 0; i < _nPlaces; i++)
 
87
                result_m[i] += tv[i+_nPlaces];
 
88
 
 
89
 
 
90
        if(_assignments[t])
 
91
                _assignments[t]->evaluate(m, a, result_a, _ranges, _nVariables);
 
92
        else
 
93
                memcpy(result_a, a, sizeof(VarVal) * _nVariables);
 
94
 
 
95
        return true;
 
96
}
 
97
 
 
98
bool PetriNet::fire(unsigned int t,
 
99
                                        const Structures::State* s,
 
100
                                        Structures::State* ns,
 
101
                                        int multiplicity,
 
102
                                        int kbound) const{
 
103
        //Check the condition
 
104
        if(_conditions[t] &&
 
105
           !_conditions[t]->evaluate(PQL::EvaluationContext(s->marking(), s->valuation())))
 
106
                return false;
 
107
 
 
108
        // We can handle multiplicity if there's conditions or assignments on the transition
 
109
        if((_conditions[t] && multiplicity != 1) || (_assignments[t] && multiplicity != 1))
 
110
                return false;
 
111
 
 
112
        const MarkVal* tv = _tv(t);
 
113
        //Check that we can take from the marking
 
114
        MarkVal sum = 0;
 
115
        for(size_t i = 0; i < _nPlaces; i++){
 
116
                ns->marking()[i] = s->marking()[i] - tv[i] * multiplicity;
 
117
                sum += ns->marking()[i];
 
118
                if(ns->marking()[i] < 0)
 
119
                        return false;
 
120
        }
 
121
        //Check that we're within k-bound
 
122
        if(kbound != 0 && sum > kbound)
 
123
                return false;
 
124
 
 
125
        //Add stuff that the marking gives us
 
126
        for(size_t i = 0; i < _nPlaces; i++)
 
127
                ns->marking()[i] += tv[i+_nPlaces] * multiplicity;
 
128
 
 
129
 
 
130
        if(_assignments[t])
 
131
                _assignments[t]->evaluate(s->marking(), s->valuation(), ns->valuation(), _ranges, _nVariables);
 
132
        else
 
133
                memcpy(ns->valuation(), s->valuation(), sizeof(VarVal) * _nVariables);
 
134
 
 
135
        return true;
 
136
}
 
137
 
 
138
void PetriNet::fireWithoutCheck(unsigned int t,
 
139
                                                                const MarkVal *m0,
 
140
                                                                const VarVal *a0,
 
141
                                                                MarkVal *m2,
 
142
                                                                VarVal *a2,
 
143
                                                                int multiplicity) const {
 
144
        //Don't check conditions
 
145
 
 
146
        // Do assignment first, so that we can allow m0 == m2 and a0 == a2
 
147
        // e.g. reuse of memory...
 
148
        //Assume that multiplicity is zero if there's an assignment
 
149
        if(_assignments[t])
 
150
                _assignments[t]->evaluate(m0, a0, a2, _ranges, _nVariables);
 
151
        else
 
152
                memcpy(a2, a0, sizeof(VarVal) * _nVariables);
 
153
 
 
154
        const MarkVal* tv = _tv(t);
 
155
        //Check that we can take from the marking
 
156
        for(size_t i = 0; i < _nPlaces; i++)
 
157
                m2[i] = m0[i] - tv[i] * multiplicity + tv[i+_nPlaces] * multiplicity;
 
158
}
 
159
 
 
160
bool PetriNet::fireWithMarkInf(unsigned int t,
 
161
                                                           const MarkVal* m,
 
162
                                                           const VarVal* a,
 
163
                                                           MarkVal* result_m,
 
164
                                                           VarVal* result_a) const{
 
165
        //Check the condition
 
166
        if(_conditions[t] && //TODO: Use evaluate that respects MarkInf
 
167
           !_conditions[t]->evaluate(PQL::EvaluationContext(m, a)))
 
168
                return false;
 
169
 
 
170
        const MarkVal* tv = _tv(t);
 
171
        //Check that we can take from the marking
 
172
        for(size_t i = 0; i < _nPlaces; i++){
 
173
                if(m[i] == MARK_INF)
 
174
                        continue;
 
175
                result_m[i] = m[i] - tv[i];
 
176
                if(result_m[i] < 0)
 
177
                        return false;
 
178
        }
 
179
        //Add stuff that the marking gives us
 
180
        for(size_t i = 0; i < _nPlaces; i++){
 
181
                if(m[i] == MARK_INF)
 
182
                        continue;
 
183
                result_m[i] += tv[i+_nPlaces];
 
184
        }
 
185
 
 
186
 
 
187
        if(_assignments[t]) //TODO: Use evaluate that respects MarkInf
 
188
                _assignments[t]->evaluate(m, a, result_a, _ranges, _nVariables);
 
189
        else
 
190
                memcpy(result_a, a, sizeof(VarVal) * _nVariables);
 
191
 
 
192
        return true;
 
193
}
 
194
 
 
195
int PetriNet::inArc(unsigned int place, unsigned int transition) const{
 
196
        return _tv(transition)[place];
 
197
}
 
198
 
 
199
int PetriNet::outArc(unsigned int transition, unsigned int place) const{
 
200
        return _tv(transition)[place + _nPlaces];
 
201
}
 
202
 
 
203
} // PetriEngine