← Back to branch summary

~tapaal-contributor/tapaal/disappearing-tokens-1940098

« back to all changes in this revision

Viewing changes to src/dk/aau/cs/verification/TAPNComposer.java

  • Committer: Kenneth Yrke Jørgensen
  • Date: 2011-04-12 09:50:16 UTC
  • mfrom: (329.1.188 tapaal-1.5)
  • Revision ID: mail@yrke.dk-20110412095016-e4hqdgab5596ja09
Merged with branch addning support for new 1.5 features

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/dk/aau/cs/verification/TAPNComposer.java
 
1
package dk.aau.cs.verification;
 
2
 
 
3
import java.util.HashSet;
 
4
 
 
5
import dk.aau.cs.model.tapn.SharedPlace;
 
6
import dk.aau.cs.model.tapn.TimedArcPetriNet;
 
7
import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
 
8
import dk.aau.cs.model.tapn.TimedInhibitorArc;
 
9
import dk.aau.cs.model.tapn.TimedInputArc;
 
10
import dk.aau.cs.model.tapn.TimedOutputArc;
 
11
import dk.aau.cs.model.tapn.LocalTimedPlace;
 
12
import dk.aau.cs.model.tapn.TimedPlace;
 
13
import dk.aau.cs.model.tapn.TimedToken;
 
14
import dk.aau.cs.model.tapn.TimedTransition;
 
15
import dk.aau.cs.model.tapn.TransportArc;
 
16
import dk.aau.cs.util.Tuple;
 
17
 
 
18
public class TAPNComposer {
 
19
        private static final String PLACE_FORMAT = "P%1$d";
 
20
        private static final String TRANSITION_FORMAT = "T%1$d";
 
21
 
 
22
        private int nextPlaceIndex;
 
23
        private int nextTransitionIndex;
 
24
 
 
25
        private HashSet<String> processedSharedObjects;
 
26
 
 
27
        public Tuple<TimedArcPetriNet, NameMapping> transformModel(TimedArcPetriNetNetwork model) {
 
28
                nextPlaceIndex = -1;
 
29
                nextTransitionIndex = -1;
 
30
                processedSharedObjects = new HashSet<String>();
 
31
                TimedArcPetriNet tapn = new TimedArcPetriNet("ComposedModel");
 
32
                NameMapping mapping = new NameMapping();
 
33
 
 
34
                createSharedPlaces(model, tapn, mapping);
 
35
                createPlaces(model, tapn, mapping);
 
36
                createTransitions(model, tapn, mapping);
 
37
                createInputArcs(model, tapn, mapping);
 
38
                createOutputArcs(model, tapn, mapping);
 
39
                createTransportArcs(model, tapn, mapping);
 
40
                createInhibitorArcs(model, tapn, mapping);
 
41
 
 
42
                //dumpToConsole(tapn, mapping);
 
43
 
 
44
                return new Tuple<TimedArcPetriNet, NameMapping>(tapn, mapping);
 
45
        }
 
46
 
 
47
        @SuppressWarnings("unused")
 
48
        private void dumpToConsole(TimedArcPetriNet tapn, NameMapping mapping) {
 
49
                System.out.println("Composed Model:");
 
50
                System.out.println("PLACES:");
 
51
                for(TimedPlace place : tapn.places()){
 
52
                        System.out.print("\t");
 
53
                        System.out.print(place.name());
 
54
                        System.out.print(", invariant: ");
 
55
                        System.out.print(place.invariant().toString());
 
56
                        System.out.print(" (Original: ");
 
57
                        System.out.print(mapping.map(place.name()));
 
58
                        System.out.println(")");
 
59
                }
 
60
 
 
61
                System.out.println();
 
62
                System.out.println("TRANSITIONS:");
 
63
                for(TimedTransition transition : tapn.transitions()){
 
64
                        System.out.print("\t");
 
65
                        System.out.print(transition.name());
 
66
                        System.out.print(" (Original: ");
 
67
                        System.out.print(mapping.map(transition.name()).toString());
 
68
                        System.out.println(")");
 
69
                }
 
70
 
 
71
                System.out.println();
 
72
                System.out.println("INPUT ARCS:");
 
73
                for(TimedInputArc arc : tapn.inputArcs()){
 
74
                        System.out.print("\tSource: ");
 
75
                        System.out.print(arc.source().name());
 
76
                        System.out.print(", Target: ");
 
77
                        System.out.print(arc.destination().name());
 
78
                        System.out.print(", Interval: ");
 
79
                        System.out.println(arc.interval().toString());
 
80
                }
 
81
 
 
82
                System.out.println();
 
83
                System.out.println("OUTPUT ARCS:");
 
84
                for(TimedOutputArc arc : tapn.outputArcs()){
 
85
                        System.out.print("\tSource: ");
 
86
                        System.out.print(arc.source().name());
 
87
                        System.out.print(", Target: ");
 
88
                        System.out.println(arc.destination().name());
 
89
                }
 
90
 
 
91
                System.out.println();
 
92
                System.out.println("TRANSPORT ARCS:");
 
93
                for(TransportArc arc : tapn.transportArcs()){
 
94
                        System.out.print("\tSource: ");
 
95
                        System.out.print(arc.source().name());
 
96
                        System.out.print(", Transition: ");
 
97
                        System.out.print(arc.transition().name());
 
98
                        System.out.print(", Target: ");
 
99
                        System.out.print(arc.destination().name());
 
100
                        System.out.print(", Interval: ");
 
101
                        System.out.println(arc.interval().toString());
 
102
                }
 
103
 
 
104
                System.out.println();
 
105
                System.out.println("INHIBITOR ARCS:");
 
106
                for(TimedInhibitorArc arc : tapn.inhibitorArcs()){
 
107
                        System.out.print("\tSource: ");
 
108
                        System.out.print(arc.source().name());
 
109
                        System.out.print(", Target: ");
 
110
                        System.out.print(arc.destination().name());
 
111
                        System.out.print(", Interval: ");
 
112
                        System.out.println(arc.interval().toString());
 
113
                }
 
114
 
 
115
                System.out.println();
 
116
                System.out.println("MARKING:");
 
117
                for(TimedPlace place : tapn.places()){
 
118
                        for(TimedToken token : place.tokens()){
 
119
                                System.out.print(token.toString());
 
120
                                System.out.print(", ");
 
121
                        }
 
122
                }
 
123
                System.out.println();
 
124
                System.out.println();
 
125
        }
 
126
        
 
127
        private void createSharedPlaces(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping) {
 
128
                for(SharedPlace place : model.sharedPlaces()){
 
129
                        String uniquePlaceName = getUniquePlaceName();
 
130
                        
 
131
                        LocalTimedPlace constructedPlace = new LocalTimedPlace(uniquePlaceName, place.invariant());
 
132
                        constructedModel.add(constructedPlace);
 
133
                        mapping.addMappingForShared(place.name(), uniquePlaceName);
 
134
 
 
135
                        if(isSharedPlaceUsedInTemplates(model, place)){
 
136
                                for (TimedToken token : place.tokens()) {
 
137
                                        constructedPlace.addToken(new TimedToken(constructedPlace, token.age()));
 
138
                                }
 
139
                        }
 
140
                }
 
141
        }
 
142
 
 
143
        private boolean isSharedPlaceUsedInTemplates(TimedArcPetriNetNetwork model, SharedPlace place) {
 
144
                for(TimedArcPetriNet tapn : model.templates()){
 
145
                        for(TimedPlace timedPlace : tapn.places()){
 
146
                                if(timedPlace.equals(place)) return true;
 
147
                        }
 
148
                }
 
149
                return false;
 
150
        }
 
151
 
 
152
        private void createPlaces(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping) {
 
153
                for (TimedArcPetriNet tapn : model.templates()) {
 
154
                        for (TimedPlace timedPlace : tapn.places()) {
 
155
                                if(!timedPlace.isShared()){
 
156
                                        String uniquePlaceName = getUniquePlaceName();
 
157
 
 
158
                                        LocalTimedPlace place = new LocalTimedPlace(uniquePlaceName, timedPlace.invariant());
 
159
                                        constructedModel.add(place);
 
160
                                        mapping.addMapping(tapn.name(), timedPlace.name(), uniquePlaceName);
 
161
 
 
162
                                        for (TimedToken token : timedPlace.tokens()) {
 
163
                                                place.addToken(new TimedToken(place, token.age()));
 
164
                                        }
 
165
                                }
 
166
                        }
 
167
                }
 
168
        }
 
169
 
 
170
        private String getUniquePlaceName() {
 
171
                nextPlaceIndex++;
 
172
                return String.format(PLACE_FORMAT, nextPlaceIndex);
 
173
        }
 
174
 
 
175
        private void createTransitions(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping) {
 
176
                for (TimedArcPetriNet tapn : model.templates()) {
 
177
                        for (TimedTransition timedTransition : tapn.transitions()) {
 
178
                                if(!processedSharedObjects.contains(timedTransition.name())){
 
179
                                        String uniqueTransitionName = getUniqueTransitionName();
 
180
 
 
181
                                        constructedModel.add(new TimedTransition(uniqueTransitionName));
 
182
                                        if(timedTransition.isShared()){
 
183
                                                String name = timedTransition.sharedTransition().name();
 
184
                                                processedSharedObjects.add(name);
 
185
                                                mapping.addMappingForShared(name, uniqueTransitionName);
 
186
                                        }else{
 
187
                                                mapping.addMapping(tapn.name(), timedTransition.name(), uniqueTransitionName);
 
188
                                        }
 
189
                                }
 
190
                        }
 
191
                }
 
192
        }
 
193
 
 
194
        private String getUniqueTransitionName() {
 
195
                nextTransitionIndex++;
 
196
                return String.format(TRANSITION_FORMAT, nextTransitionIndex);
 
197
        }
 
198
 
 
199
        private void createInputArcs(TimedArcPetriNetNetwork model,
 
200
                        TimedArcPetriNet constructedModel, NameMapping mapping) {
 
201
                for (TimedArcPetriNet tapn : model.templates()) {
 
202
                        for (TimedInputArc arc : tapn.inputArcs()) {
 
203
                                String template = arc.source().isShared() ? "" : tapn.name();
 
204
                                TimedPlace source = constructedModel.getPlaceByName(mapping.map(template, arc.source().name()));
 
205
                                
 
206
                                template = arc.destination().isShared() ? "" : tapn.name();
 
207
                                TimedTransition target = constructedModel.getTransitionByName(mapping.map(template, arc.destination().name()));
 
208
 
 
209
                                constructedModel.add(new TimedInputArc(source, target, arc.interval()));
 
210
                        }
 
211
                }
 
212
        }
 
213
 
 
214
        private void createOutputArcs(TimedArcPetriNetNetwork model,
 
215
                        TimedArcPetriNet constructedModel, NameMapping mapping) {
 
216
                for (TimedArcPetriNet tapn : model.templates()) {
 
217
                        for (TimedOutputArc arc : tapn.outputArcs()) {
 
218
                                String template = arc.source().isShared() ? "" : tapn.name();
 
219
                                TimedTransition source = constructedModel.getTransitionByName(mapping.map(template, arc.source().name()));
 
220
 
 
221
                                template = arc.destination().isShared() ? "" : tapn.name();
 
222
                                TimedPlace target = constructedModel.getPlaceByName(mapping.map(template, arc.destination().name()));
 
223
 
 
224
                                constructedModel.add(new TimedOutputArc(source, target));
 
225
                        }
 
226
                }
 
227
        }
 
228
 
 
229
        private void createTransportArcs(TimedArcPetriNetNetwork model,
 
230
                        TimedArcPetriNet constructedModel, NameMapping mapping) {
 
231
                for (TimedArcPetriNet tapn : model.templates()) {
 
232
                        for (TransportArc arc : tapn.transportArcs()) {
 
233
                                String template = arc.source().isShared() ? "" : tapn.name();
 
234
                                TimedPlace source = constructedModel.getPlaceByName(mapping.map(template, arc.source().name()));
 
235
                                
 
236
                                template = arc.transition().isShared() ? "" : tapn.name();
 
237
                                TimedTransition transition = constructedModel.getTransitionByName(mapping.map(template, arc.transition().name()));
 
238
                                
 
239
                                template = arc.destination().isShared() ? "" : tapn.name();
 
240
                                TimedPlace target = constructedModel.getPlaceByName(mapping.map(template, arc.destination().name()));
 
241
 
 
242
                                constructedModel.add(new TransportArc(source, transition,target, arc.interval()));
 
243
                        }
 
244
                }
 
245
        }
 
246
 
 
247
        private void createInhibitorArcs(TimedArcPetriNetNetwork model,
 
248
                        TimedArcPetriNet constructedModel, NameMapping mapping) {
 
249
                for (TimedArcPetriNet tapn : model.templates()) {
 
250
                        for (TimedInhibitorArc arc : tapn.inhibitorArcs()) {
 
251
                                String template = arc.source().isShared() ? "" : tapn.name();
 
252
                                TimedPlace source = constructedModel.getPlaceByName(mapping.map(template, arc.source().name()));
 
253
 
 
254
                                template = arc.destination().isShared() ? "" : tapn.name();
 
255
                                TimedTransition target = constructedModel.getTransitionByName(mapping.map(template, arc.destination().name()));
 
256
 
 
257
                                constructedModel.add(new TimedInhibitorArc(source, target, arc.interval()));
 
258
                        }
 
259
                }
 
260
        }
 
261
}