← Back to branch summary

~verifypn-cpn/verifypn/colored

« back to all changes in this revision

Viewing changes to PetriEngine/DTAPN/DTAPNTranslator.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/DTAPN/DTAPNTranslator.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 "DTAPNTranslator.h"
 
20
 
 
21
#define MAX(a,b)        (a < b ? b : a)
 
22
#include <sstream>
 
23
#include <assert.h>
 
24
 
 
25
using namespace std;
 
26
 
 
27
/** Auxiliary function for converting from int to string */
 
28
std::string i2s(int i){
 
29
        stringstream ss;
 
30
        ss<<i;
 
31
        return ss.str();
 
32
}
 
33
 
 
34
namespace PetriEngine{
 
35
namespace DTAPN {
 
36
 
 
37
void DTAPNTranslator::addPlace(const std::string& name, int tokens, int maxInvariantAge, double, double){
 
38
        assert(!name.empty());
 
39
        Place p;
 
40
        p.name = name;
 
41
        p.tokens = tokens;
 
42
        if(maxInvariantAge != -1)
 
43
                p.maxAge = maxInvariantAge;
 
44
        else
 
45
                p.maxAge = 0;
 
46
        p.maxInvariantAge = maxInvariantAge;
 
47
        places.push_back(p);
 
48
}
 
49
 
 
50
void DTAPNTranslator::addTransition(const std::string& name, double, double){
 
51
        assert(!name.empty());
 
52
        Transition t;
 
53
        t.name = name;
 
54
        transitions.push_back(t);
 
55
}
 
56
 
 
57
bool DTAPNTranslator::hasIdentifier(const std::string& id){
 
58
        for(PlaceIter p = places.begin(); p != places.end(); p++)
 
59
                if(p->name == id)
 
60
                        return true;
 
61
        for(TransitionIter t = transitions.begin(); t != transitions.end(); t++)
 
62
                if(t->name == id)
 
63
                        return true;
 
64
        return false;
 
65
}
 
66
 
 
67
void DTAPNTranslator::addInputArc(const std::string& place, const std::string& transition, int startInterval, int endInterval){
 
68
        InArc a;
 
69
        a.start = place;
 
70
        a.end = transition;
 
71
        a.startInterval = startInterval;
 
72
        a.endInterval = endInterval;
 
73
        inArcs.push_back(a);
 
74
}
 
75
 
 
76
void DTAPNTranslator::addOutputArc(const std::string& transition, const std::string& place){
 
77
        OutArc a;
 
78
        a.start = transition;
 
79
        a.end = place;
 
80
        outArcs.push_back(a);
 
81
}
 
82
 
 
83
DTAPNTranslator::Place& DTAPNTranslator::findPlace(const string& name){
 
84
        for(PlaceIter p = places.begin(); p != places.end(); p++)
 
85
                if(p->name == name)
 
86
                        return *p;
 
87
        // We should always find something
 
88
        assert(false);
 
89
        return places.front();
 
90
}
 
91
 
 
92
/** Make sure it can't collide with stuff we have */
 
93
std::string DTAPNTranslator::escapeIdentifier(std::string identifier){
 
94
        while(hasIdentifier(identifier))
 
95
                identifier += "_";
 
96
        return identifier;
 
97
}
 
98
 
 
99
/** Gets the input arcs of a transition */
 
100
DTAPNTranslator::InArcList DTAPNTranslator::preset(const std::string& transition){
 
101
        InArcList preset;
 
102
        for(InArcIter ai = inArcs.begin(); ai != inArcs.end(); ai++){
 
103
                if(ai->end == transition)
 
104
                        preset.push_back(*ai);
 
105
        }
 
106
        return preset;
 
107
}
 
108
 
 
109
/** Gets the output arcs of a transition */
 
110
DTAPNTranslator::OutArcList DTAPNTranslator::postset(const std::string& transition){
 
111
        OutArcList postset;
 
112
        for(OutArcIter ai = outArcs.begin(); ai != outArcs.end(); ai++){
 
113
                if(ai->start == transition)
 
114
                        postset.push_back(*ai);
 
115
        }
 
116
        return postset;
 
117
}
 
118
 
 
119
/** True, if place is the target of any output arcs */
 
120
bool DTAPNTranslator::isEndPlace(const std::string& place){
 
121
        for(OutArcIter ai = outArcs.begin(); ai != outArcs.end(); ai++){
 
122
                if(ai->end == place)
 
123
                        return true;
 
124
        }
 
125
        return false;
 
126
}
 
127
 
 
128
/** Translates a bounded DTAPN into a PNDV */
 
129
void DTAPNTranslator::makePNDV(AbstractPetriNetBuilder* builder){
 
130
        // Find max age for all places
 
131
        for(InArcIter ai = inArcs.begin(); ai != inArcs.end(); ai++){
 
132
                Place& p = findPlace(ai->start);
 
133
                if(p.maxInvariantAge == -1)
 
134
                        p.maxAge = MAX(p.maxAge, MAX(ai->startInterval, ai->endInterval + 1));
 
135
        }
 
136
 
 
137
        // Replace infinity with max age
 
138
        for(InArcIter ai = inArcs.begin(); ai != inArcs.end(); ai++){
 
139
                Place& p = findPlace(ai->start);
 
140
                if(ai->endInterval == -1)
 
141
                        ai->endInterval = p.maxAge;
 
142
        }
 
143
 
 
144
        // Build control variables (Transition Lock and Release Lock)
 
145
        lockStateIdle = 0;
 
146
        lockStateAgeing = transitions.size()+1;
 
147
        builder->addVariable("L", 0, transitions.size() + 1); //one for each transition + idle and ageing
 
148
 
 
149
        // For each place
 
150
        for(PlaceIter p = places.begin(); p != places.end(); p++){
 
151
                // Build original place
 
152
                builder->addPlace(p->name, p->tokens); // Ignore coordinates
 
153
 
 
154
                // Build variables for token ages
 
155
                for(int i = 0; i < bound; i++)
 
156
                        builder->addVariable(tokenAgeVariable(p->name, i), 0, p->maxAge);
 
157
        }
 
158
 
 
159
        // For each transition
 
160
        for(TransitionIter t = transitions.begin(); t != transitions.end(); t++){
 
161
                // Find pre and post sets
 
162
                InArcList  pre  = preset(t->name);
 
163
                OutArcList post = postset(t->name);
 
164
 
 
165
                // Build original transition, remember to set release lock
 
166
                string assign = "L := " + i2s(lockStateIdle) + "; \n";
 
167
                // Create result assign
 
168
                for(OutArcIter ai = post.begin(); ai != post.end(); ai++){
 
169
                        assign += tokenAgeVariable(ai->end, 0) + " := 0 ; \n";
 
170
                        for(int i = 1; i < bound-1; i++)
 
171
                                assign += tokenAgeVariable(ai->end, i) + " := "  + tokenAgeVariable(ai->end, i-1) + " ; \n";
 
172
                }
 
173
 
 
174
                builder->addTransition(t->name, "", assign);
 
175
 
 
176
                // For each in-arc
 
177
                int inArcNr = 0;
 
178
                for(InArcIter ai = pre.begin(); ai != pre.end(); ai++){
 
179
                        // Build pre-place
 
180
                        string preplace = prePlace(t->name, inArcNr);
 
181
                        builder->addPlace(preplace, 0);
 
182
                        // Build k new pre-place-transitions
 
183
                        for(int i = 0; i < bound; i++){
 
184
                                string pretrans = prePlaceTransition(t->name, inArcNr, i);
 
185
 
 
186
                                // Create pre-condition
 
187
                                string conds;
 
188
                                // preplace == 0
 
189
                                conds += preplace + " == 0 and \n";
 
190
                                // ai->start >= i
 
191
                                conds += ai->start + " >= " + i2s(i+1) + " and \n";
 
192
                                // ai->startInterval <= <ai->start>_<i>
 
193
                                conds += i2s(ai->startInterval) + " <= " + tokenAgeVariable(ai->start, i) + " and \n";
 
194
                                // <ai->start>_<i> <= ai->endInterval
 
195
                                conds += tokenAgeVariable(ai->start, i) + " <= " + i2s(ai->endInterval) + " and \n";
 
196
                                // L == LockStateIdle or L == lockState(t->name)
 
197
                                conds += "( L == " + i2s(lockStateIdle) + " or L == " + lockState(t->name) + " )";
 
198
 
 
199
                                // Create post-assignments
 
200
                                string assigns;
 
201
                                // L := lockState(t->name)
 
202
                                assigns += "L := " + lockState(t->name) + " ; \n";
 
203
                                // Shift the values of variables with higher index
 
204
                                for(int j = i; j < bound - 1; j++){
 
205
                                        // <place>_<j>   := <place>_<j+1>
 
206
                                        assigns += tokenAgeVariable(ai->start,j);
 
207
                                        assigns += " := " + tokenAgeVariable(ai->start,j + 1) + " ; \n";
 
208
                                }
 
209
                                builder->addTransition(pretrans, conds, assigns);
 
210
 
 
211
                                // Add arc from original place to new transition
 
212
                                builder->addInputArc(ai->start, pretrans);
 
213
                                // Add arc from transition to pre-place.
 
214
                                builder->addOutputArc(pretrans, preplace);
 
215
                        }
 
216
                        // Connect pre-place to original transition
 
217
                        builder->addInputArc(preplace, t->name);
 
218
                        inArcNr++;
 
219
                }
 
220
 
 
221
                // Create arcs to post-places
 
222
                for(OutArcIter ai = post.begin(); ai != post.end(); ai++)
 
223
                        builder->addOutputArc(t->name, ai->end);
 
224
        }
 
225
 
 
226
        // Create control net (for ageing)
 
227
        int marking = 1;
 
228
        for(PlaceIter p = places.begin(); p != places.end(); p++){
 
229
                for(int i = 0; i < bound; i++){
 
230
                        // Build intermediate places
 
231
                        builder->addPlace(intermediateAgeingPlace(p->name, i), marking);
 
232
                        marking = 0;
 
233
                }
 
234
        }
 
235
        bool isFirst = true;
 
236
        for(PlaceIter p = places.begin(); p != places.end(); p++){
 
237
                for(int i = 0; i < bound; i++){
 
238
                        // Determine if we're last
 
239
                        bool isLast = false;
 
240
                        int ni = i + 1;
 
241
                        PlaceIter np = p;
 
242
                        if(i == bound-1){
 
243
                                np++;
 
244
                                ni = 0;
 
245
                                if(np == places.end()){
 
246
                                        np = places.begin();
 
247
                                        isLast = true;
 
248
                                }
 
249
                        }
 
250
                        string iplace = intermediateAgeingPlace(p->name, i);
 
251
                        string niplace = intermediateAgeingPlace(np->name, ni);
 
252
 
 
253
                        string tokenAge = tokenAgeVariable(p->name, i);
 
254
                        string maxCond, ageCond, maxAssign, ageAssign;
 
255
                        // If we are the first place, require that the lock is idle, and set it ageing
 
256
                        if(isFirst){
 
257
                                isFirst = false;
 
258
                                maxCond += "L == " + i2s(lockStateIdle) + " and ";
 
259
                                ageCond += "L == " + i2s(lockStateIdle) + " and ";
 
260
                                maxAssign += "L := " + i2s(lockStateAgeing) + " ; ";
 
261
                                ageAssign += "L := " + i2s(lockStateAgeing) + " ; ";
 
262
                        }else if(isLast){
 
263
                                // If we're last, set lock state idle
 
264
                                maxAssign += "L := " + i2s(lockStateIdle) + " ; ";
 
265
                                ageAssign += "L := " + i2s(lockStateIdle) + " ; ";
 
266
                        }
 
267
                        // Increment token age if not max
 
268
                        maxCond += tokenAge + " == " + i2s(p->maxAge);
 
269
                        ageCond += tokenAge + " < " + i2s(p->maxAge);
 
270
                        // Prevent aging if it violates the invariant
 
271
                        if(p->maxInvariantAge != -1)
 
272
                                ageCond += " and " + tokenAge + " < " + i2s(p->maxInvariantAge);
 
273
                        ageAssign += tokenAge + " := " + tokenAge + " + 1 ;";
 
274
                        // Create intermediate ageing transitions
 
275
                        string maxT = maxTransition(p->name, i);
 
276
                        string ageT = ageTransition(p->name, i);
 
277
                        // Create and connect age transition
 
278
                        builder->addTransition(ageT, ageCond, ageAssign);
 
279
                        builder->addInputArc(iplace, ageT);
 
280
                        builder->addOutputArc(ageT, niplace);
 
281
                        //Create max transition if there's no invariant
 
282
                        if(p->maxInvariantAge != -1){
 
283
                                builder->addTransition(maxT, maxCond, maxAssign);
 
284
                                builder->addInputArc(iplace, maxT);
 
285
                                builder->addOutputArc(maxT, niplace);
 
286
                        }
 
287
                }
 
288
        }
 
289
}
 
290
 
 
291
/** Lock state for a transition */
 
292
string DTAPNTranslator::lockState(const string& transition){
 
293
        int next = lockStateIdle + 1;
 
294
        for(TransitionIter t = transitions.begin(); t != transitions.end(); t++){
 
295
                if(t->name == transition)
 
296
                        return i2s(next);
 
297
                next++;
 
298
        }
 
299
        assert(false);
 
300
        return "";
 
301
}
 
302
 
 
303
/** Max transition between two intermediate ageing places */
 
304
string DTAPNTranslator::maxTransition(const string& place, int tokenIndex){
 
305
        return escapeIdentifier(place + "_max_t_" + i2s(tokenIndex));
 
306
}
 
307
 
 
308
/** Age transition between two intermediate ageing places */
 
309
string DTAPNTranslator::ageTransition(const string& place, int tokenIndex){
 
310
        return escapeIdentifier(place + "_age_t_" + i2s(tokenIndex));
 
311
}
 
312
 
 
313
/** An intermediate ageing place*/
 
314
string DTAPNTranslator::intermediateAgeingPlace(const string& place, int tokenIndex){
 
315
        return escapeIdentifier(place + "_age_" + i2s(tokenIndex));
 
316
}
 
317
 
 
318
/** Pre place to a transition */
 
319
string DTAPNTranslator::prePlace(const string& transition, int inArcNr){
 
320
        return escapeIdentifier(transition + "_pre_" + i2s(inArcNr));
 
321
}
 
322
 
 
323
/** Transition from place to pre-place */
 
324
string DTAPNTranslator::prePlaceTransition(const string& transition, int inArcNr, int tokenIndex){
 
325
        return escapeIdentifier(transition + "_pre_t_" + i2s(inArcNr) + "_" + i2s(tokenIndex));
 
326
}
 
327
 
 
328
/** Variable representing the age of a specific token at a place */
 
329
string DTAPNTranslator::tokenAgeVariable(const string& place, int tokenIndex){
 
330
        return escapeIdentifier(place + "_" + i2s(tokenIndex));
 
331
}
 
332
 
 
333
/** Translates a DTAPN query into a PNDV query */
 
334
string DTAPNTranslator::translateQuery(const std::string &query){
 
335
        return "L == 0 and ( "+ query + " ) ";
 
336
}
 
337
 
 
338
} // DTAPN
 
339
} // PetriEngine
 
340