Merge lp:~tapaal-approx/tapaal/TAPNComposerWithGUI into lp:tapaal
- TAPNComposerWithGUI
- Merge into trunk
Proposed by
Jiri Srba
Status: | Merged | ||||
---|---|---|---|---|---|
Approved by: | Jiri Srba | ||||
Approved revision: | 867 | ||||
Merged at revision: | 864 | ||||
Proposed branch: | lp:~tapaal-approx/tapaal/TAPNComposerWithGUI | ||||
Merge into: | lp:tapaal | ||||
Diff against target: |
1652 lines (+7/-859) 8 files modified
src/dk/aau/cs/approximation/ApproximationWorker.java (+2/-47) src/dk/aau/cs/approximation/ITAPNApproximation.java (+0/-1) src/dk/aau/cs/approximation/OverApproximation.java (+0/-4) src/dk/aau/cs/approximation/UnderApproximation.java (+0/-7) src/dk/aau/cs/io/PNMLWriter.java (+2/-2) src/dk/aau/cs/verification/TAPNComposer.java (+0/-195) src/dk/aau/cs/verification/TAPNComposerWithGUI.java (+0/-599) src/pipe/gui/widgets/QueryDialog.java (+3/-4) |
||||
To merge this branch: | bzr merge lp:~tapaal-approx/tapaal/TAPNComposerWithGUI | ||||
Related bugs: |
|
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
Jakob Taankvist (community) | Approve | ||
Jiri Srba | Approve | ||
Mathias Grund Sørensen (community) | code | Approve | |
Review via email:
|
Commit message
Removes TAPNComposer and replaces it with TAPNComposerWit
Also fixes some issues with reporting verification time for approximations.
Description of the change
Removes TAPNComposer and replaces it with TAPNComposerWit
Also fixes some issues with reporting verification time for approximations.
To post a comment you must log in.
Revision history for this message
![](/+icing/build/overlay/assets/skins/sam/images/close.gif)
Thomas Stig Jacobsen (tsja10) wrote : | # |
The code was unused in the class
Revision history for this message
![](/+icing/build/overlay/assets/skins/sam/images/close.gif)
Mathias Grund Sørensen (mathias.grund) wrote : | # |
Looks as expected
review:
Approve
(code)
Revision history for this message
![](/+icing/build/overlay/assets/skins/sam/images/close.gif)
Jakob Taankvist (jakob-taankvist) wrote : | # |
It looks great!
I think we should rename TAPNComposerWithGUI to TAPNComposer - now that we are back to only having one.
review:
Needs Fixing
Revision history for this message
![](/+icing/build/overlay/assets/skins/sam/images/close.gif)
Jiri Srba (srba) wrote : | # |
Refactoring done. I will merge it to trunk now.
review:
Approve
Revision history for this message
![](/+icing/build/overlay/assets/skins/sam/images/close.gif)
Jakob Taankvist (jakob-taankvist) : | # |
review:
Approve
Preview Diff
[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1 | === modified file 'src/dk/aau/cs/approximation/ApproximationWorker.java' |
2 | --- src/dk/aau/cs/approximation/ApproximationWorker.java 2014-05-25 13:08:27 +0000 |
3 | +++ src/dk/aau/cs/approximation/ApproximationWorker.java 2014-06-07 16:33:21 +0000 |
4 | @@ -4,10 +4,7 @@ |
5 | |
6 | import javax.swing.SwingWorker.StateValue; |
7 | |
8 | -import pipe.dataLayer.TAPNQuery.SearchOption; |
9 | import pipe.dataLayer.TAPNQuery.TraceOption; |
10 | -import pipe.gui.FileFinderImpl; |
11 | -import pipe.gui.MessengerImpl; |
12 | import pipe.gui.RunVerificationBase; |
13 | import pipe.gui.widgets.InclusionPlaces; |
14 | import dk.aau.cs.Messenger; |
15 | @@ -21,7 +18,6 @@ |
16 | import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetStep; |
17 | import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetTrace; |
18 | import dk.aau.cs.model.tapn.simulation.TimedTransitionStep; |
19 | -import dk.aau.cs.translations.ReductionOption; |
20 | import dk.aau.cs.util.MemoryMonitor; |
21 | import dk.aau.cs.util.Tuple; |
22 | import dk.aau.cs.verification.ITAPNComposer; |
23 | @@ -33,13 +29,7 @@ |
24 | import dk.aau.cs.verification.TAPNTraceDecomposer; |
25 | import dk.aau.cs.verification.VerificationOptions; |
26 | import dk.aau.cs.verification.VerificationResult; |
27 | -import dk.aau.cs.verification.UPPAAL.Verifyta; |
28 | import dk.aau.cs.verification.UPPAAL.VerifytaOptions; |
29 | -import dk.aau.cs.verification.VerifyTAPN.ModelReduction; |
30 | -import dk.aau.cs.verification.VerifyTAPN.VerifyPN; |
31 | -import dk.aau.cs.verification.VerifyTAPN.VerifyPNOptions; |
32 | -import dk.aau.cs.verification.VerifyTAPN.VerifyTAPN; |
33 | -import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNDiscreteVerification; |
34 | import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNOptions; |
35 | import dk.aau.cs.verification.batchProcessing.BatchProcessingWorker; |
36 | |
37 | @@ -122,7 +112,7 @@ |
38 | value.setTrace(null); |
39 | value.setSecondaryTrace(null); |
40 | } |
41 | - return new VerificationResult<TAPNNetworkTrace>(result.errorMessage(), result.verificationTime()); |
42 | + return new VerificationResult<TAPNNetworkTrace>(result.errorMessage(), approxResult.verificationTime() + result.verificationTime()); |
43 | } |
44 | //Create the result from trace TAPN |
45 | renameTraceTransitions(result.getTrace()); |
46 | @@ -268,7 +258,7 @@ |
47 | value.setTrace(null); |
48 | value.setSecondaryTrace(null); |
49 | } |
50 | - return new VerificationResult<TAPNNetworkTrace>(result.errorMessage(), result.verificationTime()); |
51 | + return new VerificationResult<TAPNNetworkTrace>(result.errorMessage(), result.verificationTime() + approxResult.verificationTime()); |
52 | } |
53 | //Create the result from trace TAPN |
54 | renameTraceTransitions(result.getTrace()); |
55 | @@ -633,39 +623,4 @@ |
56 | Tuple<TimedArcPetriNet, NameMapping> composedModel = composer.transformModel(model.network()); |
57 | return composedModel; |
58 | } |
59 | - |
60 | - private ModelChecker getModelChecker(pipe.dataLayer.TAPNQuery query) { |
61 | - if(query.getReductionOption() == ReductionOption.VerifyTAPN) |
62 | - return getVerifyTAPN(); |
63 | - else if(query.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification) |
64 | - return getVerifyTAPNDiscreteVerification(); |
65 | - else if(query.getReductionOption() == ReductionOption.VerifyPN || query.getReductionOption() == ReductionOption.VerifyPNApprox || query.getReductionOption() == ReductionOption.VerifyPNReduce) |
66 | - return getVerifyPN(); |
67 | - else |
68 | - return getVerifyta(); |
69 | - } |
70 | - |
71 | - private Verifyta getVerifyta() { |
72 | - Verifyta verifyta = new Verifyta(new FileFinderImpl(), new MessengerImpl()); |
73 | - verifyta.setup(); |
74 | - return verifyta; |
75 | - } |
76 | - |
77 | - private static VerifyTAPN getVerifyTAPN() { |
78 | - VerifyTAPN verifytapn = new VerifyTAPN(new FileFinderImpl(), new MessengerImpl()); |
79 | - verifytapn.setup(); |
80 | - return verifytapn; |
81 | - } |
82 | - |
83 | - private static VerifyPN getVerifyPN() { |
84 | - VerifyPN verifypn = new VerifyPN(new FileFinderImpl(), new MessengerImpl()); |
85 | - verifypn.setup(); |
86 | - return verifypn; |
87 | - } |
88 | - |
89 | - private static VerifyTAPNDiscreteVerification getVerifyTAPNDiscreteVerification() { |
90 | - VerifyTAPNDiscreteVerification verifytapnDiscreteVerification = new VerifyTAPNDiscreteVerification(new FileFinderImpl(), new MessengerImpl()); |
91 | - verifytapnDiscreteVerification.setup(); |
92 | - return verifytapnDiscreteVerification; |
93 | - } |
94 | } |
95 | |
96 | === modified file 'src/dk/aau/cs/approximation/ITAPNApproximation.java' |
97 | --- src/dk/aau/cs/approximation/ITAPNApproximation.java 2014-03-24 12:12:30 +0000 |
98 | +++ src/dk/aau/cs/approximation/ITAPNApproximation.java 2014-06-07 16:33:21 +0000 |
99 | @@ -1,7 +1,6 @@ |
100 | package dk.aau.cs.approximation; |
101 | |
102 | import dk.aau.cs.model.tapn.TimedArcPetriNet; |
103 | -import dk.aau.cs.verification.VerificationOptions; |
104 | |
105 | public interface ITAPNApproximation { |
106 | //Returns a copy of a network which is the approximated network |
107 | |
108 | === modified file 'src/dk/aau/cs/approximation/OverApproximation.java' |
109 | --- src/dk/aau/cs/approximation/OverApproximation.java 2014-05-28 19:07:25 +0000 |
110 | +++ src/dk/aau/cs/approximation/OverApproximation.java 2014-06-07 16:33:21 +0000 |
111 | @@ -2,8 +2,6 @@ |
112 | |
113 | import java.util.ArrayList; |
114 | import java.util.HashMap; |
115 | -import java.util.Map.Entry; |
116 | - |
117 | import dk.aau.cs.TCTL.TCTLAFNode; |
118 | import dk.aau.cs.TCTL.TCTLAGNode; |
119 | import dk.aau.cs.TCTL.TCTLAbstractProperty; |
120 | @@ -19,9 +17,7 @@ |
121 | import dk.aau.cs.model.tapn.simulation.*; |
122 | import dk.aau.cs.util.Tuple; |
123 | import dk.aau.cs.verification.NameMapping; |
124 | -import dk.aau.cs.verification.VerificationOptions; |
125 | import dk.aau.cs.verification.VerificationResult; |
126 | -import pipe.dataLayer.TAPNQuery; |
127 | |
128 | public class OverApproximation implements ITAPNApproximation { |
129 | @Override |
130 | |
131 | === modified file 'src/dk/aau/cs/approximation/UnderApproximation.java' |
132 | --- src/dk/aau/cs/approximation/UnderApproximation.java 2014-05-27 18:43:59 +0000 |
133 | +++ src/dk/aau/cs/approximation/UnderApproximation.java 2014-06-07 16:33:21 +0000 |
134 | @@ -1,11 +1,9 @@ |
135 | package dk.aau.cs.approximation; |
136 | |
137 | -import java.lang.reflect.Array; |
138 | import java.util.ArrayList; |
139 | |
140 | import dk.aau.cs.model.tapn.Bound; |
141 | import dk.aau.cs.model.tapn.IntBound; |
142 | -import dk.aau.cs.model.tapn.TAPNElement; |
143 | import dk.aau.cs.model.tapn.TimeInterval; |
144 | import dk.aau.cs.model.tapn.TimeInvariant; |
145 | import dk.aau.cs.model.tapn.TimedArcPetriNet; |
146 | @@ -15,15 +13,10 @@ |
147 | import dk.aau.cs.model.tapn.TimedPlace; |
148 | import dk.aau.cs.model.tapn.TimedTransition; |
149 | import dk.aau.cs.model.tapn.TransportArc; |
150 | -import dk.aau.cs.verification.VerificationOptions; |
151 | import pipe.dataLayer.DataLayer; |
152 | -import pipe.dataLayer.TAPNQuery; |
153 | import pipe.gui.graphicElements.Arc; |
154 | import pipe.gui.graphicElements.Place; |
155 | import pipe.gui.graphicElements.Transition; |
156 | -import pipe.gui.graphicElements.tapn.TimedInhibitorArcComponent; |
157 | -import pipe.gui.graphicElements.tapn.TimedInputArcComponent; |
158 | -import pipe.gui.graphicElements.tapn.TimedTransportArcComponent; |
159 | |
160 | public class UnderApproximation implements ITAPNApproximation { |
161 | @Override |
162 | |
163 | === modified file 'src/dk/aau/cs/io/PNMLWriter.java' |
164 | --- src/dk/aau/cs/io/PNMLWriter.java 2014-06-04 22:29:05 +0000 |
165 | +++ src/dk/aau/cs/io/PNMLWriter.java 2014-06-07 16:33:21 +0000 |
166 | @@ -34,7 +34,7 @@ |
167 | import dk.aau.cs.model.tapn.TimedArcPetriNet; |
168 | import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; |
169 | import dk.aau.cs.util.Require; |
170 | -import dk.aau.cs.verification.TAPNComposerWithGUI; |
171 | +import dk.aau.cs.verification.TAPNComposer; |
172 | |
173 | public class PNMLWriter implements NetWriter { |
174 | |
175 | @@ -53,7 +53,7 @@ |
176 | Document document = null; |
177 | Transformer transformer = null; |
178 | ByteArrayOutputStream os = new ByteArrayOutputStream(); |
179 | - TAPNComposerWithGUI composer = new TAPNComposerWithGUI(new MessengerImpl(), guiModels); |
180 | + TAPNComposer composer = new TAPNComposer(new MessengerImpl(), guiModels); |
181 | composedNetwork = composer.transformModel(network).value1(); |
182 | |
183 | // Build a Petri Net XML Document |
184 | |
185 | === added file 'src/dk/aau/cs/verification/TAPNComposer.java' |
186 | --- src/dk/aau/cs/verification/TAPNComposer.java 1970-01-01 00:00:00 +0000 |
187 | +++ src/dk/aau/cs/verification/TAPNComposer.java 2014-06-07 16:33:21 +0000 |
188 | @@ -0,0 +1,627 @@ |
189 | +package dk.aau.cs.verification; |
190 | + |
191 | +import java.util.HashMap; |
192 | +import java.util.HashSet; |
193 | +import java.util.Map.Entry; |
194 | + |
195 | +import pipe.dataLayer.DataLayer; |
196 | +import pipe.gui.graphicElements.Arc; |
197 | +import pipe.gui.graphicElements.ArcPath; |
198 | +import pipe.gui.graphicElements.ArcPathPoint; |
199 | +import pipe.gui.graphicElements.Place; |
200 | +import pipe.gui.graphicElements.PlaceTransitionObject; |
201 | +import pipe.gui.graphicElements.Transition; |
202 | +import pipe.gui.graphicElements.tapn.TimedInhibitorArcComponent; |
203 | +import pipe.gui.graphicElements.tapn.TimedInputArcComponent; |
204 | +import pipe.gui.graphicElements.tapn.TimedOutputArcComponent; |
205 | +import pipe.gui.graphicElements.tapn.TimedPlaceComponent; |
206 | +import pipe.gui.graphicElements.tapn.TimedTransitionComponent; |
207 | +import pipe.gui.graphicElements.tapn.TimedTransportArcComponent; |
208 | +import dk.aau.cs.Messenger; |
209 | +import dk.aau.cs.model.tapn.Bound; |
210 | +import dk.aau.cs.model.tapn.IntBound; |
211 | +import dk.aau.cs.model.tapn.LocalTimedPlace; |
212 | +import dk.aau.cs.model.tapn.SharedPlace; |
213 | +import dk.aau.cs.model.tapn.TimeInterval; |
214 | +import dk.aau.cs.model.tapn.TimeInvariant; |
215 | +import dk.aau.cs.model.tapn.TimedArcPetriNet; |
216 | +import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; |
217 | +import dk.aau.cs.model.tapn.TimedInhibitorArc; |
218 | +import dk.aau.cs.model.tapn.TimedInputArc; |
219 | +import dk.aau.cs.model.tapn.TimedOutputArc; |
220 | +import dk.aau.cs.model.tapn.TimedPlace; |
221 | +import dk.aau.cs.model.tapn.TimedToken; |
222 | +import dk.aau.cs.model.tapn.TimedTransition; |
223 | +import dk.aau.cs.model.tapn.TransportArc; |
224 | +import dk.aau.cs.util.Tuple; |
225 | + |
226 | +public class TAPNComposer implements ITAPNComposer { |
227 | + private Messenger messenger; |
228 | + private boolean hasShownMessage = false; |
229 | + |
230 | + private HashSet<String> processedSharedObjects; |
231 | + private HashMap<TimedArcPetriNet, DataLayer> guiModels; |
232 | + private DataLayer composedGuiModel; |
233 | + |
234 | + public TAPNComposer(Messenger messenger, HashMap<TimedArcPetriNet, DataLayer> guiModels){ |
235 | + this.messenger = messenger; |
236 | + |
237 | + HashMap<TimedArcPetriNet, DataLayer> newGuiModels = new HashMap<TimedArcPetriNet, DataLayer>(); |
238 | + for(Entry<TimedArcPetriNet, DataLayer> entry : guiModels.entrySet()) { |
239 | + newGuiModels.put(entry.getKey(), entry.getValue().copy(entry.getKey())); |
240 | + } |
241 | + |
242 | + this.guiModels = newGuiModels; |
243 | + } |
244 | + |
245 | + public TAPNComposer(Messenger messenger) { |
246 | + this.messenger = messenger; |
247 | + } |
248 | + |
249 | + public Tuple<TimedArcPetriNet, NameMapping> transformModel(TimedArcPetriNetNetwork model) { |
250 | + processedSharedObjects = new HashSet<String>(); |
251 | + TimedArcPetriNet tapn = new TimedArcPetriNet("ComposedModel"); |
252 | + DataLayer guiModel = new DataLayer(); |
253 | + NameMapping mapping = new NameMapping(); |
254 | + hasShownMessage = false; |
255 | + |
256 | + |
257 | + double greatestWidth = 0, |
258 | + greatestHeight = 0; |
259 | + if (this.guiModels != null) { |
260 | + for (TimedArcPetriNet tapn1 : model.activeTemplates()) { |
261 | + greatestWidth = greatestWidth >= getRightmostObject(guiModels.get(tapn1)).getPositionX() ? greatestWidth : getRightmostObject(guiModels.get(tapn1)).getPositionX(); |
262 | + greatestHeight = greatestHeight >= getLowestObject(guiModels.get(tapn1)).getPositionY() ? greatestHeight : getLowestObject(guiModels.get(tapn1)).getPositionY(); |
263 | + } |
264 | + } |
265 | + |
266 | + createSharedPlaces(model, tapn, mapping, guiModel); |
267 | + createPlaces(model, tapn, mapping, guiModel, greatestWidth, greatestHeight); |
268 | + createTransitions(model, tapn, mapping, guiModel, greatestWidth, greatestHeight); |
269 | + createInputArcs(model, tapn, mapping, guiModel, greatestWidth, greatestHeight); |
270 | + createOutputArcs(model, tapn, mapping, guiModel, greatestWidth, greatestHeight); |
271 | + createTransportArcs(model, tapn, mapping, guiModel, greatestWidth, greatestHeight); |
272 | + createInhibitorArcs(model, tapn, mapping, guiModel, greatestWidth, greatestHeight); |
273 | + |
274 | + // Set composed guiModel in the instance variable |
275 | + this.composedGuiModel = guiModel; |
276 | + |
277 | + return new Tuple<TimedArcPetriNet, NameMapping>(tapn, mapping); |
278 | + } |
279 | + |
280 | + public DataLayer getGuiModel() { |
281 | + return this.composedGuiModel; |
282 | + } |
283 | + |
284 | + private Tuple<Integer, Integer> calculateComponentPosition(int netNumber) { |
285 | + Integer x = netNumber % 2; |
286 | + Integer y = (int) Math.floor(netNumber / 2d); |
287 | + |
288 | + return new Tuple<Integer, Integer>(x, y); |
289 | + } |
290 | + |
291 | + private PlaceTransitionObject getRightmostObject(DataLayer guiModel) { |
292 | + PlaceTransitionObject returnObject = null; |
293 | + |
294 | + for (PlaceTransitionObject currentObject : guiModel.getPlaces()) { |
295 | + if (returnObject == null || returnObject.getPositionX() < currentObject.getPositionX()) { |
296 | + returnObject = currentObject; |
297 | + } |
298 | + } |
299 | + |
300 | + for (PlaceTransitionObject currentObject : guiModel.getTransitions()) { |
301 | + if (returnObject == null || returnObject.getPositionX() < currentObject.getPositionX()) { |
302 | + returnObject = currentObject; |
303 | + } |
304 | + } |
305 | + |
306 | + return returnObject; |
307 | + } |
308 | + |
309 | + private PlaceTransitionObject getLowestObject(DataLayer guiModel) { |
310 | + PlaceTransitionObject returnObject = null; |
311 | + |
312 | + for (PlaceTransitionObject currentObject : guiModel.getPlaces()) { |
313 | + if (returnObject == null || returnObject.getPositionY() < currentObject.getPositionY()) { |
314 | + returnObject = currentObject; |
315 | + } |
316 | + } |
317 | + |
318 | + for (PlaceTransitionObject currentObject : guiModel.getTransitions()) { |
319 | + if (returnObject == null || returnObject.getPositionY() < currentObject.getPositionY()) { |
320 | + returnObject = currentObject; |
321 | + } |
322 | + } |
323 | + |
324 | + return returnObject; |
325 | + } |
326 | + |
327 | + private Place getSharedPlace(String name) { |
328 | + for(Entry<TimedArcPetriNet, DataLayer> hashmapEntry : guiModels.entrySet()) { |
329 | + Place findPlace = hashmapEntry.getValue().getPlaceByName(name); |
330 | + if (findPlace != null) |
331 | + return findPlace; |
332 | + } |
333 | + return null; |
334 | + } |
335 | + |
336 | + private void createSharedPlaces(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping, DataLayer guiModel) { |
337 | + for(SharedPlace place : model.sharedPlaces()){ |
338 | + String uniquePlaceName = (model.activeTemplates().size() > 1) ? "Shared_" + place.name() : place.name(); |
339 | + |
340 | + LocalTimedPlace constructedPlace = null; |
341 | + if (place.invariant().upperBound() instanceof Bound.InfBound) { |
342 | + constructedPlace = new LocalTimedPlace(uniquePlaceName, place.invariant()); |
343 | + } else { |
344 | + constructedPlace = new LocalTimedPlace(uniquePlaceName, new TimeInvariant(place.invariant().isUpperNonstrict(), new IntBound(place.invariant().upperBound().value()))); |
345 | + } |
346 | + constructedModel.add(constructedPlace); |
347 | + mapping.addMappingForShared(place.name(), uniquePlaceName); |
348 | + |
349 | + if(model.isSharedPlaceUsedInTemplates(place)){ |
350 | + for (TimedToken token : place.tokens()) { |
351 | + constructedPlace.addToken(new TimedToken(constructedPlace, token.age())); |
352 | + } |
353 | + } |
354 | + |
355 | + // Gui work |
356 | + if (this.guiModels != null) { |
357 | + Place oldPlace = getSharedPlace(place.name()); |
358 | + TimedPlaceComponent newPlace = new TimedPlaceComponent( |
359 | + oldPlace.getPositionX(), |
360 | + oldPlace.getPositionY(), |
361 | + oldPlace.getId(), |
362 | + uniquePlaceName, |
363 | + oldPlace.getNameOffsetX(), |
364 | + oldPlace.getNameOffsetY(), |
365 | + 0, |
366 | + oldPlace.getMarkingOffsetXObject().doubleValue(), |
367 | + oldPlace.getMarkingOffsetYObject().doubleValue(), |
368 | + 0 |
369 | + ); |
370 | + newPlace.setGuiModel(guiModel); |
371 | + newPlace.setUnderlyingPlace(constructedPlace); |
372 | + newPlace.setName(uniquePlaceName); |
373 | + guiModel.addPlace(newPlace); |
374 | + } |
375 | + } |
376 | + } |
377 | + |
378 | + private void createPlaces(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping, DataLayer guiModel, double greatestWidth, double greatestHeight) { |
379 | + int i = 0; |
380 | + for (TimedArcPetriNet tapn : model.activeTemplates()) { |
381 | + DataLayer currentGuiModel = null; |
382 | + if (this.guiModels != null) { |
383 | + currentGuiModel = this.guiModels.get(tapn); |
384 | + } |
385 | + Tuple<Integer, Integer> offset = this.calculateComponentPosition(i); |
386 | + |
387 | + for (TimedPlace timedPlace : tapn.places()) { |
388 | + if(!timedPlace.isShared()){ |
389 | + String uniquePlaceName = (model.activeTemplates().size() > 1) ? ((LocalTimedPlace)timedPlace).model().name() + "_" + timedPlace.name() : timedPlace.name(); |
390 | + |
391 | + LocalTimedPlace place = null; |
392 | + if (timedPlace.invariant().upperBound() instanceof Bound.InfBound) { |
393 | + place = new LocalTimedPlace(uniquePlaceName, timedPlace.invariant()); |
394 | + } else { |
395 | + place = new LocalTimedPlace(uniquePlaceName, new TimeInvariant(timedPlace.invariant().isUpperNonstrict(), new IntBound(timedPlace.invariant().upperBound().value()))); |
396 | + } |
397 | + constructedModel.add(place); |
398 | + mapping.addMapping(tapn.name(), timedPlace.name(), uniquePlaceName); |
399 | + |
400 | + for (TimedToken token : timedPlace.tokens()) { |
401 | + place.addToken(new TimedToken(place, token.age())); |
402 | + } |
403 | + |
404 | + // Gui work |
405 | + if (this.guiModels != null) { |
406 | + Place oldPlace = currentGuiModel.getPlaceByName(timedPlace.name()); |
407 | + TimedPlaceComponent newPlace = new TimedPlaceComponent( |
408 | + oldPlace.getPositionX() + offset.value1() * greatestWidth, |
409 | + oldPlace.getPositionY() + offset.value2() * greatestHeight, |
410 | + oldPlace.getId(), |
411 | + uniquePlaceName, |
412 | + oldPlace.getNameOffsetX(), |
413 | + oldPlace.getNameOffsetY(), |
414 | + 0, |
415 | + oldPlace.getMarkingOffsetXObject().doubleValue(), |
416 | + oldPlace.getMarkingOffsetYObject().doubleValue(), |
417 | + 0 |
418 | + ); |
419 | + newPlace.setGuiModel(guiModel); |
420 | + newPlace.setUnderlyingPlace(place); |
421 | + newPlace.setName(uniquePlaceName); |
422 | + guiModel.addPlace(newPlace); |
423 | + } |
424 | + } |
425 | + } |
426 | + i++; |
427 | + } |
428 | + } |
429 | + |
430 | + private void createTransitions(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping, DataLayer guiModel, double greatestWidth, double greatestHeight) { |
431 | + int i = 0; |
432 | + for (TimedArcPetriNet tapn : model.activeTemplates()) { |
433 | + DataLayer currentGuiModel = null; |
434 | + if (this.guiModels != null) { |
435 | + currentGuiModel = this.guiModels.get(tapn); |
436 | + } |
437 | + Tuple<Integer, Integer> offset = this.calculateComponentPosition(i); |
438 | + |
439 | + for (TimedTransition timedTransition : tapn.transitions()) { |
440 | + if(!processedSharedObjects.contains(timedTransition.name())){ |
441 | + |
442 | + // CAUTION: This if statement removes orphan transitions. |
443 | + // This changes answers for e.g. DEADLOCK queries if |
444 | + // support for such queries are added later. |
445 | + // ONLY THE IF SENTENCE SHOULD BE REMOVED. REST OF CODE SHOULD BE LEFT INTACT |
446 | + if(!timedTransition.isOrphan()){ |
447 | + String uniqueTransitionName = ""; |
448 | + if (model.activeTemplates().size() > 1) { |
449 | + uniqueTransitionName = ( ! timedTransition.isShared()) ? timedTransition.model().name() + "_" + timedTransition.name() : "Shared_" + timedTransition.name(); |
450 | + } else { |
451 | + uniqueTransitionName = timedTransition.name(); |
452 | + } |
453 | + |
454 | + TimedTransition transition = new TimedTransition(uniqueTransitionName, timedTransition.isUrgent()); |
455 | + constructedModel.add(transition); |
456 | + |
457 | + // Gui work |
458 | + if (this.guiModels != null) { |
459 | + Transition oldTransition = currentGuiModel.getTransitionByName(timedTransition.name()); |
460 | + TimedTransitionComponent newTransition = new TimedTransitionComponent( |
461 | + oldTransition.getPositionX() + offset.value1() * greatestWidth, |
462 | + oldTransition.getPositionY() + offset.value2() * greatestHeight, |
463 | + oldTransition.getId(), |
464 | + uniqueTransitionName, |
465 | + oldTransition.getNameOffsetX(), |
466 | + oldTransition.getNameOffsetY(), |
467 | + true, |
468 | + false, |
469 | + oldTransition.getAngle(), |
470 | + 0); |
471 | + newTransition.setGuiModel(guiModel); |
472 | + newTransition.setUnderlyingTransition(transition); |
473 | + newTransition.setName(uniqueTransitionName); |
474 | + guiModel.addTransition(newTransition); |
475 | + } |
476 | + |
477 | + if(timedTransition.isShared()){ |
478 | + String name = timedTransition.sharedTransition().name(); |
479 | + processedSharedObjects.add(name); |
480 | + mapping.addMappingForShared(name, uniqueTransitionName); |
481 | + }else{ |
482 | + mapping.addMapping(tapn.name(), timedTransition.name(), uniqueTransitionName); |
483 | + } |
484 | + }else{ |
485 | + if(!hasShownMessage){ |
486 | + messenger.displayInfoMessage("There are orphan transitions (no incoming and no outgoing arcs) in the model." |
487 | + + System.getProperty("line.separator") + "They will be removed before the verification."); |
488 | + hasShownMessage = true; |
489 | + } |
490 | + } |
491 | + } |
492 | + } |
493 | + i++; |
494 | + } |
495 | + } |
496 | + |
497 | + private ArcPath createArcPath(DataLayer currentGuiModel, PlaceTransitionObject source, PlaceTransitionObject target, Arc arc, double offsetX, double offsetY) { |
498 | + Arc guiArc = currentGuiModel.getArcByEndpoints(source, target); |
499 | + ArcPath arcPath = guiArc.getArcPath(); |
500 | + int arcPathPointsNum = arcPath.getNumPoints(); |
501 | + |
502 | + // Build ArcPath |
503 | + ArcPath newArcPath = new ArcPath(arc); |
504 | + for(int k = 0; k < arcPathPointsNum; k++) { |
505 | + ArcPathPoint point = arcPath.getArcPathPoint(k); |
506 | + newArcPath.addPoint( |
507 | + point.getPoint().x + offsetX, |
508 | + point.getPoint().y + offsetY, |
509 | + point.getPointType() |
510 | + ); |
511 | + } |
512 | + |
513 | + return newArcPath; |
514 | + } |
515 | + |
516 | + private void createInputArcs(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping, DataLayer guiModel, double greatestWidth, double greatestHeight) { |
517 | + int i = 0; |
518 | + for (TimedArcPetriNet tapn : model.activeTemplates()) { |
519 | + DataLayer currentGuiModel = null; |
520 | + if (this.guiModels != null) { |
521 | + currentGuiModel = this.guiModels.get(tapn); |
522 | + } |
523 | + Tuple<Integer, Integer> offset = this.calculateComponentPosition(i); |
524 | + |
525 | + for (TimedInputArc arc : tapn.inputArcs()) { |
526 | + String sourceTemplate = arc.source().isShared() ? "" : tapn.name(); |
527 | + TimedPlace source = constructedModel.getPlaceByName(mapping.map(sourceTemplate, arc.source().name())); |
528 | + |
529 | + String targetTemplate = arc.destination().isShared() ? "" : tapn.name(); |
530 | + TimedTransition target = constructedModel.getTransitionByName(mapping.map(targetTemplate, arc.destination().name())); |
531 | + |
532 | + TimeInterval newInterval = new TimeInterval(arc.interval()); |
533 | + newInterval.setLowerBound(new IntBound(newInterval.lowerBound().value())); |
534 | + if (newInterval.upperBound() instanceof Bound.InfBound) { |
535 | + newInterval.setUpperBound(newInterval.upperBound()); |
536 | + } else { |
537 | + newInterval.setUpperBound(new IntBound(newInterval.upperBound().value())); |
538 | + } |
539 | + TimedInputArc addedArc = new TimedInputArc(source, target, newInterval, arc.getWeight()); |
540 | + constructedModel.add(addedArc); |
541 | + |
542 | + // Gui work |
543 | + if (this.guiModels != null) { |
544 | + Place guiSource = guiModel.getPlaceByName(mapping.map(sourceTemplate, arc.source().name())); |
545 | + Transition guiTarget = guiModel.getTransitionByName(mapping.map(targetTemplate, arc.destination().name())); |
546 | + |
547 | + Arc newArc = new TimedInputArcComponent(new TimedOutputArcComponent( |
548 | + 0d, |
549 | + 0d, |
550 | + 0d, |
551 | + 0d, |
552 | + guiSource, |
553 | + guiTarget, |
554 | + arc.getWeight().value(), |
555 | + mapping.map(sourceTemplate, arc.source().name()) + "_to_" + mapping.map(targetTemplate, arc.destination().name()), |
556 | + false |
557 | + )); |
558 | + |
559 | + // Build ArcPath |
560 | + Place oldGuiSource = currentGuiModel.getPlaceByName(arc.source().name()); |
561 | + Transition oldGuiTarget = currentGuiModel.getTransitionByName(arc.destination().name()); |
562 | + ArcPath newArcPath = createArcPath(currentGuiModel, oldGuiSource, oldGuiTarget, newArc, offset.value1() * greatestWidth, offset.value2() * greatestHeight); |
563 | + |
564 | + // Set arcPath, guiModel and connectors |
565 | + ((TimedInputArcComponent) newArc).setUnderlyingArc(addedArc); |
566 | + newArc.setArcPath(newArcPath); |
567 | + newArc.setGuiModel(guiModel); |
568 | + newArc.updateArcPosition(); |
569 | + guiModel.addPetriNetObject(newArc); |
570 | + guiSource.addConnectFrom(newArc); |
571 | + guiTarget.addConnectTo(newArc); |
572 | + } |
573 | + } |
574 | + i++; |
575 | + } |
576 | + } |
577 | + |
578 | + private void createOutputArcs(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping, DataLayer guiModel, double greatestWidth, double greatestHeight) { |
579 | + int i = 0; |
580 | + for (TimedArcPetriNet tapn : model.activeTemplates()) { |
581 | + DataLayer currentGuiModel = null; |
582 | + if (this.guiModels != null) { |
583 | + currentGuiModel = this.guiModels.get(tapn); |
584 | + } |
585 | + Tuple<Integer, Integer> offset = this.calculateComponentPosition(i); |
586 | + |
587 | + for (TimedOutputArc arc : tapn.outputArcs()) { |
588 | + String sourceTemplate = arc.source().isShared() ? "" : tapn.name(); |
589 | + TimedTransition source = constructedModel.getTransitionByName(mapping.map(sourceTemplate, arc.source().name())); |
590 | + |
591 | + String destinationTemplate = arc.destination().isShared() ? "" : tapn.name(); |
592 | + TimedPlace target = constructedModel.getPlaceByName(mapping.map(destinationTemplate, arc.destination().name())); |
593 | + |
594 | + TimedOutputArc addedArc = new TimedOutputArc(source, target, arc.getWeight()); |
595 | + constructedModel.add(addedArc); |
596 | + |
597 | + // Gui work |
598 | + if (this.guiModels != null) { |
599 | + Transition guiSource = guiModel.getTransitionByName(mapping.map(sourceTemplate, arc.source().name())); |
600 | + Place guiTarget = guiModel.getPlaceByName(mapping.map(destinationTemplate, arc.destination().name())); |
601 | + |
602 | + TimedOutputArcComponent newArc = new TimedOutputArcComponent( |
603 | + 0d, |
604 | + 0d, |
605 | + 0d, |
606 | + 0d, |
607 | + guiModel.getTransitionByName(mapping.map(sourceTemplate, arc.source().name())), |
608 | + guiModel.getPlaceByName(mapping.map(destinationTemplate, arc.destination().name())), |
609 | + arc.getWeight().value(), |
610 | + mapping.map(sourceTemplate, arc.source().name()) + "_to_" + mapping.map(destinationTemplate, arc.destination().name()), |
611 | + false |
612 | + ); |
613 | + |
614 | + // Build ArcPath |
615 | + Transition oldGuiSource = currentGuiModel.getTransitionByName(arc.source().name()); |
616 | + Place oldGuiTarget = currentGuiModel.getPlaceByName(arc.destination().name()); |
617 | + ArcPath newArcPath = createArcPath(currentGuiModel, oldGuiSource, oldGuiTarget, newArc, offset.value1() * greatestWidth, offset.value2() * greatestHeight); |
618 | + |
619 | + // Set arcPath, guiModel and connectors |
620 | + newArc.setUnderlyingArc(addedArc); |
621 | + newArc.setArcPath(newArcPath); |
622 | + newArc.setGuiModel(guiModel); |
623 | + newArc.updateArcPosition(); |
624 | + guiModel.addArc(newArc); |
625 | + guiSource.addConnectTo(newArc); |
626 | + guiTarget.addConnectFrom(newArc); |
627 | + } |
628 | + } |
629 | + i++; |
630 | + } |
631 | + } |
632 | + |
633 | + private void createTransportArcs(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping, DataLayer guiModel, double greatestWidth, double greatestHeight) { |
634 | + int i = 0; |
635 | + int nextGroupNr = 0; |
636 | + for (TimedArcPetriNet tapn : model.activeTemplates()) { |
637 | + DataLayer currentGuiModel = null; |
638 | + if (this.guiModels != null) { |
639 | + currentGuiModel = this.guiModels.get(tapn); |
640 | + } |
641 | + Tuple<Integer, Integer> offset = this.calculateComponentPosition(i); |
642 | + |
643 | + for (TransportArc arc : tapn.transportArcs()) { |
644 | + String sourceTemplate = arc.source().isShared() ? "" : tapn.name(); |
645 | + String transitionTemplate = arc.transition().isShared() ? "" : tapn.name(); |
646 | + String destinationTemplate = arc.destination().isShared() ? "" : tapn.name(); |
647 | + |
648 | + TimedPlace source = constructedModel.getPlaceByName(mapping.map(sourceTemplate, arc.source().name())); |
649 | + TimedTransition transition = constructedModel.getTransitionByName(mapping.map(transitionTemplate, arc.transition().name())); |
650 | + TimedPlace destination = constructedModel.getPlaceByName(mapping.map(destinationTemplate, arc.destination().name())); |
651 | + |
652 | + TimeInterval newInterval = new TimeInterval(arc.interval()); |
653 | + newInterval.setLowerBound(new IntBound(newInterval.lowerBound().value())); |
654 | + if (newInterval.upperBound() instanceof Bound.InfBound) { |
655 | + newInterval.setUpperBound(newInterval.upperBound()); |
656 | + } else { |
657 | + newInterval.setUpperBound(new IntBound(newInterval.upperBound().value())); |
658 | + } |
659 | + TransportArc addedArc = new TransportArc(source, transition, destination, newInterval, arc.getWeight()); |
660 | + constructedModel.add(addedArc); |
661 | + |
662 | + //Create input transport arc |
663 | + // Gui work |
664 | + if (this.guiModels != null) { |
665 | + Place guiSourceIn = guiModel.getPlaceByName(mapping.map(sourceTemplate, arc.source().name())); |
666 | + Transition guiTargetIn = guiModel.getTransitionByName(mapping.map(transitionTemplate, arc.transition().name())); |
667 | + |
668 | + TimedTransportArcComponent newInArc = new TimedTransportArcComponent( |
669 | + new TimedInputArcComponent(new TimedOutputArcComponent( |
670 | + 0d, |
671 | + 0d, |
672 | + 0d, |
673 | + 0d, |
674 | + guiSourceIn, |
675 | + guiTargetIn, |
676 | + arc.getWeight().value(), |
677 | + mapping.map(sourceTemplate, arc.source().name()) + "_to_" + mapping.map(transitionTemplate, arc.transition().name()), |
678 | + false |
679 | + )), |
680 | + nextGroupNr, |
681 | + true |
682 | + ); |
683 | + |
684 | + // Build ArcPath |
685 | + Place oldGuiSourceIn = currentGuiModel.getPlaceByName(arc.source().name()); |
686 | + Transition oldGuiTargetIn = currentGuiModel.getTransitionByName(arc.transition().name()); |
687 | + ArcPath newArcPathIn = createArcPath(currentGuiModel, oldGuiSourceIn, oldGuiTargetIn, newInArc, offset.value1() * greatestWidth, offset.value2() * greatestHeight); |
688 | + |
689 | + newInArc.setUnderlyingArc(addedArc); |
690 | + newInArc.setArcPath(newArcPathIn); |
691 | + newInArc.setGuiModel(guiModel); |
692 | + newInArc.updateArcPosition(); |
693 | + guiModel.addArc(newInArc); |
694 | + |
695 | + guiSourceIn.addConnectTo(newInArc); |
696 | + guiTargetIn.addConnectFrom(newInArc); |
697 | + |
698 | + // Calculate the next group number for this transport arc |
699 | + // By looking at the target of the newInArc -> a transition |
700 | + // Then finding the largest existing group number of outgoing transport arcs from this transition |
701 | + for (Object pt : newInArc.getTarget().getPostset()) { |
702 | + if (pt instanceof TimedTransportArcComponent) { |
703 | + if (((TimedTransportArcComponent) pt).getGroupNr() > nextGroupNr) { |
704 | + nextGroupNr = ((TimedTransportArcComponent) pt).getGroupNr(); |
705 | + } |
706 | + } |
707 | + } |
708 | + |
709 | + ((TimedTransportArcComponent) newInArc).setGroupNr(nextGroupNr + 1); |
710 | + |
711 | + //Create output transport arc |
712 | + Transition guiSourceOut = guiModel.getTransitionByName(mapping.map(transitionTemplate, arc.transition().name())); |
713 | + Place guiTargetOut = guiModel.getPlaceByName(mapping.map(destinationTemplate, arc.destination().name())); |
714 | + |
715 | + TimedTransportArcComponent newOutArc = new TimedTransportArcComponent( |
716 | + new TimedInputArcComponent(new TimedOutputArcComponent( |
717 | + 0d, |
718 | + 0d, |
719 | + 0d, |
720 | + 0d, |
721 | + guiSourceOut, |
722 | + guiTargetOut, |
723 | + 1, |
724 | + mapping.map(transitionTemplate, arc.transition().name()) + "_to_" + mapping.map(destinationTemplate, arc.destination().name()), |
725 | + false |
726 | + )), |
727 | + nextGroupNr + 1, |
728 | + false |
729 | + ); |
730 | + |
731 | + // Build ArcPath |
732 | + Transition oldGuiSourceOut = currentGuiModel.getTransitionByName(arc.transition().name()); |
733 | + Place oldGuiTargetOut = currentGuiModel.getPlaceByName(arc.destination().name()); |
734 | + ArcPath newArcPathOut = createArcPath(currentGuiModel, oldGuiSourceOut, oldGuiTargetOut, newOutArc, offset.value1() * greatestWidth, offset.value2() * greatestHeight); |
735 | + |
736 | + newOutArc.setUnderlyingArc(addedArc); |
737 | + newOutArc.setArcPath(newArcPathOut); |
738 | + newOutArc.setGuiModel(guiModel); |
739 | + newOutArc.updateArcPosition(); |
740 | + guiModel.addArc(newOutArc); |
741 | + |
742 | + // Add connection references to the two transport arcs |
743 | + newInArc.setConnectedTo(newOutArc); |
744 | + newOutArc.setConnectedTo(newInArc); |
745 | + |
746 | + guiSourceOut.addConnectTo(newOutArc); |
747 | + guiTargetOut.addConnectFrom(newOutArc); |
748 | + } |
749 | + } |
750 | + i++; |
751 | + } |
752 | + } |
753 | + |
754 | + |
755 | + |
756 | + private void createInhibitorArcs(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping, DataLayer guiModel, double greatestWidth, double greatestHeight) { |
757 | + int i = 0; |
758 | + for (TimedArcPetriNet tapn : model.activeTemplates()) { |
759 | + DataLayer currentGuiModel = null; |
760 | + if (this.guiModels != null) { |
761 | + currentGuiModel = this.guiModels.get(tapn); |
762 | + } |
763 | + Tuple<Integer, Integer> offset = this.calculateComponentPosition(i); |
764 | + |
765 | + for (TimedInhibitorArc arc : tapn.inhibitorArcs()) { |
766 | + String sourceTemplate = arc.source().isShared() ? "" : tapn.name(); |
767 | + String destinationTemplate = arc.destination().isShared() ? "" : tapn.name(); |
768 | + |
769 | + TimedPlace source = constructedModel.getPlaceByName(mapping.map(sourceTemplate, arc.source().name())); |
770 | + TimedTransition target = constructedModel.getTransitionByName(mapping.map(destinationTemplate, arc.destination().name())); |
771 | + |
772 | + TimeInterval newInterval = new TimeInterval(arc.interval()); |
773 | + newInterval.setLowerBound(new IntBound(newInterval.lowerBound().value())); |
774 | + if (newInterval.upperBound() instanceof Bound.InfBound) { |
775 | + newInterval.setUpperBound(newInterval.upperBound()); |
776 | + } else { |
777 | + newInterval.setUpperBound(new IntBound(newInterval.upperBound().value())); |
778 | + } |
779 | + TimedInhibitorArc addedArc = new TimedInhibitorArc(source, target, newInterval, arc.getWeight()); |
780 | + constructedModel.add(addedArc); |
781 | + |
782 | + // Gui work |
783 | + if (this.guiModels != null) { |
784 | + Place guiSource = guiModel.getPlaceByName(mapping.map(sourceTemplate, arc.source().name())); |
785 | + Transition guiTarget = guiModel.getTransitionByName(mapping.map(destinationTemplate, arc.destination().name())); |
786 | + Arc newArc = new TimedInhibitorArcComponent(new TimedOutputArcComponent( |
787 | + 0d, |
788 | + 0d, |
789 | + 0d, |
790 | + 0d, |
791 | + guiSource, |
792 | + guiTarget, |
793 | + arc.getWeight().value(), |
794 | + mapping.map(sourceTemplate, arc.source().name()) + "_to_" + mapping.map(destinationTemplate, arc.destination().name()), |
795 | + false |
796 | + ), ""); |
797 | + |
798 | + // Build ArcPath |
799 | + Place oldGuiSource = currentGuiModel.getPlaceByName(arc.source().name()); |
800 | + Transition oldGuiTarget = currentGuiModel.getTransitionByName(arc.destination().name()); |
801 | + ArcPath newArcPath = createArcPath(currentGuiModel, oldGuiSource, oldGuiTarget, newArc, offset.value1() * greatestWidth, offset.value2() * greatestHeight); |
802 | + |
803 | + ((TimedInhibitorArcComponent) newArc).setUnderlyingArc(addedArc); |
804 | + newArc.setArcPath(newArcPath); |
805 | + newArc.setGuiModel(guiModel); |
806 | + newArc.updateArcPosition(); |
807 | + guiModel.addPetriNetObject(newArc); |
808 | + guiSource.addConnectTo(newArc); |
809 | + guiTarget.addConnectFrom(newArc); |
810 | + } |
811 | + } |
812 | + i++; |
813 | + } |
814 | + } |
815 | +} |
816 | |
817 | === removed file 'src/dk/aau/cs/verification/TAPNComposer.java' |
818 | --- src/dk/aau/cs/verification/TAPNComposer.java 2014-05-09 11:17:58 +0000 |
819 | +++ src/dk/aau/cs/verification/TAPNComposer.java 1970-01-01 00:00:00 +0000 |
820 | @@ -1,195 +0,0 @@ |
821 | -package dk.aau.cs.verification; |
822 | - |
823 | -import java.util.HashSet; |
824 | - |
825 | -import dk.aau.cs.Messenger; |
826 | -import dk.aau.cs.model.tapn.LocalTimedPlace; |
827 | -import dk.aau.cs.model.tapn.SharedPlace; |
828 | -import dk.aau.cs.model.tapn.TimedArcPetriNet; |
829 | -import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; |
830 | -import dk.aau.cs.model.tapn.TimedInhibitorArc; |
831 | -import dk.aau.cs.model.tapn.TimedInputArc; |
832 | -import dk.aau.cs.model.tapn.TimedOutputArc; |
833 | -import dk.aau.cs.model.tapn.TimedPlace; |
834 | -import dk.aau.cs.model.tapn.TimedToken; |
835 | -import dk.aau.cs.model.tapn.TimedTransition; |
836 | -import dk.aau.cs.model.tapn.TransportArc; |
837 | -import dk.aau.cs.util.Tuple; |
838 | - |
839 | -public class TAPNComposer implements ITAPNComposer { |
840 | - private static final String PLACE_FORMAT = "P%1$d"; |
841 | - private static final String TRANSITION_FORMAT = "T%1$d"; |
842 | - |
843 | - private Messenger messenger; |
844 | - private boolean hasShownMessage = false; |
845 | - |
846 | - private int nextPlaceIndex; |
847 | - private int nextTransitionIndex; |
848 | - |
849 | - private HashSet<String> processedSharedObjects; |
850 | - |
851 | - public TAPNComposer(Messenger messenger){ |
852 | - this.messenger = messenger; |
853 | - } |
854 | - |
855 | - @Override |
856 | - public Tuple<TimedArcPetriNet, NameMapping> transformModel(TimedArcPetriNetNetwork model) { |
857 | - nextPlaceIndex = -1; |
858 | - nextTransitionIndex = -1; |
859 | - processedSharedObjects = new HashSet<String>(); |
860 | - TimedArcPetriNet tapn = new TimedArcPetriNet("ComposedModel"); |
861 | - NameMapping mapping = new NameMapping(); |
862 | - hasShownMessage = false; |
863 | - |
864 | - createSharedPlaces(model, tapn, mapping); |
865 | - createPlaces(model, tapn, mapping); |
866 | - createTransitions(model, tapn, mapping); |
867 | - createInputArcs(model, tapn, mapping); |
868 | - createOutputArcs(model, tapn, mapping); |
869 | - createTransportArcs(model, tapn, mapping); |
870 | - createInhibitorArcs(model, tapn, mapping); |
871 | - |
872 | - return new Tuple<TimedArcPetriNet, NameMapping>(tapn, mapping); |
873 | - } |
874 | - |
875 | - private void createSharedPlaces(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping) { |
876 | - for(SharedPlace place : model.sharedPlaces()){ |
877 | - String uniquePlaceName = getUniquePlaceName(); |
878 | - |
879 | - LocalTimedPlace constructedPlace = new LocalTimedPlace(uniquePlaceName, place.invariant()); |
880 | - constructedModel.add(constructedPlace); |
881 | - mapping.addMappingForShared(place.name(), uniquePlaceName); |
882 | - |
883 | - if(model.isSharedPlaceUsedInTemplates(place)){ |
884 | - for (TimedToken token : place.tokens()) { |
885 | - constructedPlace.addToken(new TimedToken(constructedPlace, token.age())); |
886 | - } |
887 | - } |
888 | - } |
889 | - } |
890 | - |
891 | - private void createPlaces(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping) { |
892 | - for (TimedArcPetriNet tapn : model.activeTemplates()) { |
893 | - for (TimedPlace timedPlace : tapn.places()) { |
894 | - if(!timedPlace.isShared()){ |
895 | - String uniquePlaceName = getUniquePlaceName(); |
896 | - |
897 | - LocalTimedPlace place = new LocalTimedPlace(uniquePlaceName, timedPlace.invariant()); |
898 | - constructedModel.add(place); |
899 | - mapping.addMapping(tapn.name(), timedPlace.name(), uniquePlaceName); |
900 | - |
901 | - for (TimedToken token : timedPlace.tokens()) { |
902 | - place.addToken(new TimedToken(place, token.age())); |
903 | - } |
904 | - } |
905 | - } |
906 | - } |
907 | - } |
908 | - |
909 | - private String getUniquePlaceName() { |
910 | - nextPlaceIndex++; |
911 | - return String.format(PLACE_FORMAT, nextPlaceIndex); |
912 | - } |
913 | - |
914 | - private void createTransitions(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping) { |
915 | - for (TimedArcPetriNet tapn : model.activeTemplates()) { |
916 | - for (TimedTransition timedTransition : tapn.transitions()) { |
917 | - if(!processedSharedObjects.contains(timedTransition.name())){ |
918 | - |
919 | - // CAUTION: This if statement removes orphan transitions. |
920 | - // This changes answers for e.g. DEADLOCK queries if |
921 | - // support for such queries are added later. |
922 | - // ONLY THE IF SENTENCE SHOULD BE REMOVED. REST OF CODE SHOULD BE LEFT INTACT |
923 | - if(!timedTransition.isOrphan()){ |
924 | - String uniqueTransitionName = getUniqueTransitionName(); |
925 | - |
926 | - constructedModel.add(new TimedTransition(uniqueTransitionName, timedTransition.isUrgent())); |
927 | - if(timedTransition.isShared()){ |
928 | - String name = timedTransition.sharedTransition().name(); |
929 | - processedSharedObjects.add(name); |
930 | - mapping.addMappingForShared(name, uniqueTransitionName); |
931 | - }else{ |
932 | - mapping.addMapping(tapn.name(), timedTransition.name(), uniqueTransitionName); |
933 | - } |
934 | - }else{ |
935 | - if(!hasShownMessage){ |
936 | - messenger.displayInfoMessage("There are orphan transitions (no incoming and no outgoing arcs) in the model." |
937 | - + System.getProperty("line.separator") + "They will be removed (together with any connected inhibitor arcs) before the verification."); |
938 | - hasShownMessage = true; |
939 | - } |
940 | - } |
941 | - } |
942 | - } |
943 | - } |
944 | - } |
945 | - |
946 | - private String getUniqueTransitionName() { |
947 | - nextTransitionIndex++; |
948 | - return String.format(TRANSITION_FORMAT, nextTransitionIndex); |
949 | - } |
950 | - |
951 | - private void createInputArcs(TimedArcPetriNetNetwork model, |
952 | - TimedArcPetriNet constructedModel, NameMapping mapping) { |
953 | - for (TimedArcPetriNet tapn : model.activeTemplates()) { |
954 | - for (TimedInputArc arc : tapn.inputArcs()) { |
955 | - String template = arc.source().isShared() ? "" : tapn.name(); |
956 | - TimedPlace source = constructedModel.getPlaceByName(mapping.map(template, arc.source().name())); |
957 | - |
958 | - template = arc.destination().isShared() ? "" : tapn.name(); |
959 | - TimedTransition target = constructedModel.getTransitionByName(mapping.map(template, arc.destination().name())); |
960 | - |
961 | - constructedModel.add(new TimedInputArc(source, target, arc.interval(), arc.getWeight())); |
962 | - } |
963 | - } |
964 | - } |
965 | - |
966 | - private void createOutputArcs(TimedArcPetriNetNetwork model, |
967 | - TimedArcPetriNet constructedModel, NameMapping mapping) { |
968 | - for (TimedArcPetriNet tapn : model.activeTemplates()) { |
969 | - for (TimedOutputArc arc : tapn.outputArcs()) { |
970 | - String template = arc.source().isShared() ? "" : tapn.name(); |
971 | - TimedTransition source = constructedModel.getTransitionByName(mapping.map(template, arc.source().name())); |
972 | - |
973 | - template = arc.destination().isShared() ? "" : tapn.name(); |
974 | - TimedPlace target = constructedModel.getPlaceByName(mapping.map(template, arc.destination().name())); |
975 | - |
976 | - constructedModel.add(new TimedOutputArc(source, target, arc.getWeight())); |
977 | - } |
978 | - } |
979 | - } |
980 | - |
981 | - private void createTransportArcs(TimedArcPetriNetNetwork model, |
982 | - TimedArcPetriNet constructedModel, NameMapping mapping) { |
983 | - for (TimedArcPetriNet tapn : model.activeTemplates()) { |
984 | - for (TransportArc arc : tapn.transportArcs()) { |
985 | - String template = arc.source().isShared() ? "" : tapn.name(); |
986 | - TimedPlace source = constructedModel.getPlaceByName(mapping.map(template, arc.source().name())); |
987 | - |
988 | - template = arc.transition().isShared() ? "" : tapn.name(); |
989 | - TimedTransition transition = constructedModel.getTransitionByName(mapping.map(template, arc.transition().name())); |
990 | - |
991 | - template = arc.destination().isShared() ? "" : tapn.name(); |
992 | - TimedPlace target = constructedModel.getPlaceByName(mapping.map(template, arc.destination().name())); |
993 | - |
994 | - constructedModel.add(new TransportArc(source, transition,target, arc.interval(), arc.getWeight())); |
995 | - } |
996 | - } |
997 | - } |
998 | - |
999 | - private void createInhibitorArcs(TimedArcPetriNetNetwork model, |
1000 | - TimedArcPetriNet constructedModel, NameMapping mapping) { |
1001 | - for (TimedArcPetriNet tapn : model.activeTemplates()) { |
1002 | - for (TimedInhibitorArc arc : tapn.inhibitorArcs()) { |
1003 | - if(arc.destination().isOrphan()) continue; |
1004 | - |
1005 | - String template = arc.source().isShared() ? "" : tapn.name(); |
1006 | - TimedPlace source = constructedModel.getPlaceByName(mapping.map(template, arc.source().name())); |
1007 | - |
1008 | - template = arc.destination().isShared() ? "" : tapn.name(); |
1009 | - TimedTransition target = constructedModel.getTransitionByName(mapping.map(template, arc.destination().name())); |
1010 | - |
1011 | - constructedModel.add(new TimedInhibitorArc(source, target, arc.interval(), arc.getWeight())); |
1012 | - } |
1013 | - } |
1014 | - } |
1015 | -} |
1016 | |
1017 | === removed file 'src/dk/aau/cs/verification/TAPNComposerWithGUI.java' |
1018 | --- src/dk/aau/cs/verification/TAPNComposerWithGUI.java 2014-05-28 18:51:52 +0000 |
1019 | +++ src/dk/aau/cs/verification/TAPNComposerWithGUI.java 1970-01-01 00:00:00 +0000 |
1020 | @@ -1,599 +0,0 @@ |
1021 | -package dk.aau.cs.verification; |
1022 | - |
1023 | -import java.util.HashMap; |
1024 | -import java.util.HashSet; |
1025 | -import java.util.Map.Entry; |
1026 | - |
1027 | -import pipe.dataLayer.DataLayer; |
1028 | -import pipe.gui.graphicElements.Arc; |
1029 | -import pipe.gui.graphicElements.ArcPath; |
1030 | -import pipe.gui.graphicElements.ArcPathPoint; |
1031 | -import pipe.gui.graphicElements.Place; |
1032 | -import pipe.gui.graphicElements.PlaceTransitionObject; |
1033 | -import pipe.gui.graphicElements.Transition; |
1034 | -import pipe.gui.graphicElements.tapn.TimedInhibitorArcComponent; |
1035 | -import pipe.gui.graphicElements.tapn.TimedInputArcComponent; |
1036 | -import pipe.gui.graphicElements.tapn.TimedOutputArcComponent; |
1037 | -import pipe.gui.graphicElements.tapn.TimedPlaceComponent; |
1038 | -import pipe.gui.graphicElements.tapn.TimedTransitionComponent; |
1039 | -import pipe.gui.graphicElements.tapn.TimedTransportArcComponent; |
1040 | -import dk.aau.cs.Messenger; |
1041 | -import dk.aau.cs.model.tapn.Bound; |
1042 | -import dk.aau.cs.model.tapn.IntBound; |
1043 | -import dk.aau.cs.model.tapn.LocalTimedPlace; |
1044 | -import dk.aau.cs.model.tapn.SharedPlace; |
1045 | -import dk.aau.cs.model.tapn.TimeInterval; |
1046 | -import dk.aau.cs.model.tapn.TimeInvariant; |
1047 | -import dk.aau.cs.model.tapn.TimedArcPetriNet; |
1048 | -import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; |
1049 | -import dk.aau.cs.model.tapn.TimedInhibitorArc; |
1050 | -import dk.aau.cs.model.tapn.TimedInputArc; |
1051 | -import dk.aau.cs.model.tapn.TimedOutputArc; |
1052 | -import dk.aau.cs.model.tapn.TimedPlace; |
1053 | -import dk.aau.cs.model.tapn.TimedToken; |
1054 | -import dk.aau.cs.model.tapn.TimedTransition; |
1055 | -import dk.aau.cs.model.tapn.TransportArc; |
1056 | -import dk.aau.cs.util.Tuple; |
1057 | - |
1058 | -public class TAPNComposerWithGUI implements ITAPNComposer { |
1059 | - private static final String PLACE_FORMAT = "P%1$d"; |
1060 | - private static final String TRANSITION_FORMAT = "T%1$d"; |
1061 | - |
1062 | - private Messenger messenger; |
1063 | - private boolean hasShownMessage = false; |
1064 | - |
1065 | - private int nextPlaceIndex; |
1066 | - private int nextTransitionIndex; |
1067 | - |
1068 | - private HashSet<String> processedSharedObjects; |
1069 | - private HashMap<TimedArcPetriNet, DataLayer> guiModels; |
1070 | - private DataLayer composedGuiModel; |
1071 | - |
1072 | - public TAPNComposerWithGUI(Messenger messenger, HashMap<TimedArcPetriNet, DataLayer> guiModels){ |
1073 | - this.messenger = messenger; |
1074 | - |
1075 | - HashMap<TimedArcPetriNet, DataLayer> newGuiModels = new HashMap<TimedArcPetriNet, DataLayer>(); |
1076 | - for(Entry<TimedArcPetriNet, DataLayer> entry : guiModels.entrySet()) { |
1077 | - newGuiModels.put(entry.getKey(), entry.getValue().copy(entry.getKey())); |
1078 | - } |
1079 | - |
1080 | - this.guiModels = newGuiModels; |
1081 | - } |
1082 | - |
1083 | - public Tuple<TimedArcPetriNet, NameMapping> transformModel(TimedArcPetriNetNetwork model) { |
1084 | - nextPlaceIndex = -1; |
1085 | - nextTransitionIndex = -1; |
1086 | - processedSharedObjects = new HashSet<String>(); |
1087 | - TimedArcPetriNet tapn = new TimedArcPetriNet("ComposedModel"); |
1088 | - DataLayer guiModel = new DataLayer(); |
1089 | - NameMapping mapping = new NameMapping(); |
1090 | - hasShownMessage = false; |
1091 | - |
1092 | - |
1093 | - double greatestWidth = 0, |
1094 | - greatestHeight = 0; |
1095 | - for (TimedArcPetriNet tapn1 : model.activeTemplates()) { |
1096 | - greatestWidth = greatestWidth >= getRightmostObject(guiModels.get(tapn1)).getPositionX() ? greatestWidth : getRightmostObject(guiModels.get(tapn1)).getPositionX(); |
1097 | - greatestHeight = greatestHeight >= getLowestObject(guiModels.get(tapn1)).getPositionY() ? greatestHeight : getLowestObject(guiModels.get(tapn1)).getPositionY(); |
1098 | - } |
1099 | - |
1100 | - createSharedPlaces(model, tapn, mapping, guiModel); |
1101 | - createPlaces(model, tapn, mapping, guiModel, greatestWidth, greatestHeight); |
1102 | - createTransitions(model, tapn, mapping, guiModel, greatestWidth, greatestHeight); |
1103 | - createInputArcs(model, tapn, mapping, guiModel, greatestWidth, greatestHeight); |
1104 | - createOutputArcs(model, tapn, mapping, guiModel, greatestWidth, greatestHeight); |
1105 | - createTransportArcs(model, tapn, mapping, guiModel, greatestWidth, greatestHeight); |
1106 | - createInhibitorArcs(model, tapn, mapping, guiModel, greatestWidth, greatestHeight); |
1107 | - |
1108 | - // Set composed guiModel in the instance variable |
1109 | - this.composedGuiModel = guiModel; |
1110 | - |
1111 | - return new Tuple<TimedArcPetriNet, NameMapping>(tapn, mapping); |
1112 | - } |
1113 | - |
1114 | - public DataLayer getGuiModel() { |
1115 | - return this.composedGuiModel; |
1116 | - } |
1117 | - |
1118 | - private Tuple<Integer, Integer> calculateComponentPosition(int netNumber) { |
1119 | - Integer x = netNumber % 2; |
1120 | - Integer y = (int) Math.floor(netNumber / 2d); |
1121 | - |
1122 | - return new Tuple<Integer, Integer>(x, y); |
1123 | - } |
1124 | - |
1125 | - private PlaceTransitionObject getRightmostObject(DataLayer guiModel) { |
1126 | - PlaceTransitionObject returnObject = null; |
1127 | - |
1128 | - for (PlaceTransitionObject currentObject : guiModel.getPlaces()) { |
1129 | - if (returnObject == null || returnObject.getPositionX() < currentObject.getPositionX()) { |
1130 | - returnObject = currentObject; |
1131 | - } |
1132 | - } |
1133 | - |
1134 | - for (PlaceTransitionObject currentObject : guiModel.getTransitions()) { |
1135 | - if (returnObject == null || returnObject.getPositionX() < currentObject.getPositionX()) { |
1136 | - returnObject = currentObject; |
1137 | - } |
1138 | - } |
1139 | - |
1140 | - return returnObject; |
1141 | - } |
1142 | - |
1143 | - private PlaceTransitionObject getLowestObject(DataLayer guiModel) { |
1144 | - PlaceTransitionObject returnObject = null; |
1145 | - |
1146 | - for (PlaceTransitionObject currentObject : guiModel.getPlaces()) { |
1147 | - if (returnObject == null || returnObject.getPositionY() < currentObject.getPositionY()) { |
1148 | - returnObject = currentObject; |
1149 | - } |
1150 | - } |
1151 | - |
1152 | - for (PlaceTransitionObject currentObject : guiModel.getTransitions()) { |
1153 | - if (returnObject == null || returnObject.getPositionY() < currentObject.getPositionY()) { |
1154 | - returnObject = currentObject; |
1155 | - } |
1156 | - } |
1157 | - |
1158 | - return returnObject; |
1159 | - } |
1160 | - |
1161 | - private Place getSharedPlace(String name) { |
1162 | - for(Entry<TimedArcPetriNet, DataLayer> hashmapEntry : guiModels.entrySet()) { |
1163 | - Place findPlace = hashmapEntry.getValue().getPlaceByName(name); |
1164 | - if (findPlace != null) |
1165 | - return findPlace; |
1166 | - } |
1167 | - return null; |
1168 | - } |
1169 | - |
1170 | - private void createSharedPlaces(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping, DataLayer guiModel) { |
1171 | - for(SharedPlace place : model.sharedPlaces()){ |
1172 | - String uniquePlaceName = (model.activeTemplates().size() > 1) ? "Shared_" + place.name() : place.name(); |
1173 | - |
1174 | - LocalTimedPlace constructedPlace = null; |
1175 | - if (place.invariant().upperBound() instanceof Bound.InfBound) { |
1176 | - constructedPlace = new LocalTimedPlace(uniquePlaceName, place.invariant()); |
1177 | - } else { |
1178 | - constructedPlace = new LocalTimedPlace(uniquePlaceName, new TimeInvariant(place.invariant().isUpperNonstrict(), new IntBound(place.invariant().upperBound().value()))); |
1179 | - } |
1180 | - constructedModel.add(constructedPlace); |
1181 | - mapping.addMappingForShared(place.name(), uniquePlaceName); |
1182 | - |
1183 | - if(model.isSharedPlaceUsedInTemplates(place)){ |
1184 | - for (TimedToken token : place.tokens()) { |
1185 | - constructedPlace.addToken(new TimedToken(constructedPlace, token.age())); |
1186 | - } |
1187 | - } |
1188 | - |
1189 | - Place oldPlace = getSharedPlace(place.name()); |
1190 | - TimedPlaceComponent newPlace = new TimedPlaceComponent( |
1191 | - oldPlace.getPositionX(), |
1192 | - oldPlace.getPositionY(), |
1193 | - oldPlace.getId(), |
1194 | - uniquePlaceName, |
1195 | - oldPlace.getNameOffsetX(), |
1196 | - oldPlace.getNameOffsetY(), |
1197 | - 0, |
1198 | - oldPlace.getMarkingOffsetXObject().doubleValue(), |
1199 | - oldPlace.getMarkingOffsetYObject().doubleValue(), |
1200 | - 0 |
1201 | - ); |
1202 | - newPlace.setGuiModel(guiModel); |
1203 | - newPlace.setUnderlyingPlace(constructedPlace); |
1204 | - newPlace.setName(uniquePlaceName); |
1205 | - guiModel.addPlace(newPlace); |
1206 | - } |
1207 | - } |
1208 | - |
1209 | - private void createPlaces(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping, DataLayer guiModel, double greatestWidth, double greatestHeight) { |
1210 | - int i = 0; |
1211 | - for (TimedArcPetriNet tapn : model.activeTemplates()) { |
1212 | - Tuple<Integer, Integer> offset = this.calculateComponentPosition(i); |
1213 | - DataLayer currentGuiModel = this.guiModels.get(tapn); |
1214 | - |
1215 | - for (TimedPlace timedPlace : tapn.places()) { |
1216 | - if(!timedPlace.isShared()){ |
1217 | - String uniquePlaceName = (model.activeTemplates().size() > 1) ? ((LocalTimedPlace)timedPlace).model().name() + "_" + timedPlace.name() : timedPlace.name(); |
1218 | - |
1219 | - LocalTimedPlace place = null; |
1220 | - if (timedPlace.invariant().upperBound() instanceof Bound.InfBound) { |
1221 | - place = new LocalTimedPlace(uniquePlaceName, timedPlace.invariant()); |
1222 | - } else { |
1223 | - place = new LocalTimedPlace(uniquePlaceName, new TimeInvariant(timedPlace.invariant().isUpperNonstrict(), new IntBound(timedPlace.invariant().upperBound().value()))); |
1224 | - } |
1225 | - constructedModel.add(place); |
1226 | - mapping.addMapping(tapn.name(), timedPlace.name(), uniquePlaceName); |
1227 | - |
1228 | - for (TimedToken token : timedPlace.tokens()) { |
1229 | - place.addToken(new TimedToken(place, token.age())); |
1230 | - } |
1231 | - |
1232 | - Place oldPlace = currentGuiModel.getPlaceByName(timedPlace.name()); |
1233 | - TimedPlaceComponent newPlace = new TimedPlaceComponent( |
1234 | - oldPlace.getPositionX() + offset.value1() * greatestWidth, |
1235 | - oldPlace.getPositionY() + offset.value2() * greatestHeight, |
1236 | - oldPlace.getId(), |
1237 | - uniquePlaceName, |
1238 | - oldPlace.getNameOffsetX(), |
1239 | - oldPlace.getNameOffsetY(), |
1240 | - 0, |
1241 | - oldPlace.getMarkingOffsetXObject().doubleValue(), |
1242 | - oldPlace.getMarkingOffsetYObject().doubleValue(), |
1243 | - 0 |
1244 | - ); |
1245 | - newPlace.setGuiModel(guiModel); |
1246 | - newPlace.setUnderlyingPlace(place); |
1247 | - newPlace.setName(uniquePlaceName); |
1248 | - guiModel.addPlace(newPlace); |
1249 | - } |
1250 | - } |
1251 | - i++; |
1252 | - } |
1253 | - } |
1254 | - |
1255 | - private String getUniquePlaceName() { |
1256 | - nextPlaceIndex++; |
1257 | - return String.format(PLACE_FORMAT, nextPlaceIndex); |
1258 | - } |
1259 | - |
1260 | - private void createTransitions(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping, DataLayer guiModel, double greatestWidth, double greatestHeight) { |
1261 | - int i = 0; |
1262 | - for (TimedArcPetriNet tapn : model.activeTemplates()) { |
1263 | - Tuple<Integer, Integer> offset = this.calculateComponentPosition(i); |
1264 | - DataLayer currentGuiModel = this.guiModels.get(tapn); |
1265 | - |
1266 | - for (TimedTransition timedTransition : tapn.transitions()) { |
1267 | - if(!processedSharedObjects.contains(timedTransition.name())){ |
1268 | - |
1269 | - // CAUTION: This if statement removes orphan transitions. |
1270 | - // This changes answers for e.g. DEADLOCK queries if |
1271 | - // support for such queries are added later. |
1272 | - // ONLY THE IF SENTENCE SHOULD BE REMOVED. REST OF CODE SHOULD BE LEFT INTACT |
1273 | - if(!timedTransition.isOrphan()){ |
1274 | - String uniqueTransitionName = ""; |
1275 | - if (model.activeTemplates().size() > 1) { |
1276 | - uniqueTransitionName = ( ! timedTransition.isShared()) ? timedTransition.model().name() + "_" + timedTransition.name() : "Shared_" + timedTransition.name(); |
1277 | - } else { |
1278 | - uniqueTransitionName = timedTransition.name(); |
1279 | - } |
1280 | - |
1281 | - TimedTransition transition = new TimedTransition(uniqueTransitionName, timedTransition.isUrgent()); |
1282 | - constructedModel.add(transition); |
1283 | - Transition oldTransition = currentGuiModel.getTransitionByName(timedTransition.name()); |
1284 | - TimedTransitionComponent newTransition = new TimedTransitionComponent( |
1285 | - oldTransition.getPositionX() + offset.value1() * greatestWidth, |
1286 | - oldTransition.getPositionY() + offset.value2() * greatestHeight, |
1287 | - oldTransition.getId(), |
1288 | - uniqueTransitionName, |
1289 | - oldTransition.getNameOffsetX(), |
1290 | - oldTransition.getNameOffsetY(), |
1291 | - true, |
1292 | - false, |
1293 | - oldTransition.getAngle(), |
1294 | - 0); |
1295 | - newTransition.setGuiModel(guiModel); |
1296 | - newTransition.setUnderlyingTransition(transition); |
1297 | - newTransition.setName(uniqueTransitionName); |
1298 | - guiModel.addTransition(newTransition); |
1299 | - |
1300 | - if(timedTransition.isShared()){ |
1301 | - String name = timedTransition.sharedTransition().name(); |
1302 | - processedSharedObjects.add(name); |
1303 | - mapping.addMappingForShared(name, uniqueTransitionName); |
1304 | - }else{ |
1305 | - mapping.addMapping(tapn.name(), timedTransition.name(), uniqueTransitionName); |
1306 | - } |
1307 | - }else{ |
1308 | - if(!hasShownMessage){ |
1309 | - messenger.displayInfoMessage("There are orphan transitions (no incoming and no outgoing arcs) in the model." |
1310 | - + System.getProperty("line.separator") + "They will be removed before the verification."); |
1311 | - hasShownMessage = true; |
1312 | - } |
1313 | - } |
1314 | - } |
1315 | - } |
1316 | - i++; |
1317 | - } |
1318 | - } |
1319 | - |
1320 | - private String getUniqueTransitionName() { |
1321 | - nextTransitionIndex++; |
1322 | - return String.format(TRANSITION_FORMAT, nextTransitionIndex); |
1323 | - } |
1324 | - |
1325 | - private ArcPath createArcPath(DataLayer currentGuiModel, PlaceTransitionObject source, PlaceTransitionObject target, Arc arc, double offsetX, double offsetY) { |
1326 | - Arc guiArc = currentGuiModel.getArcByEndpoints(source, target); |
1327 | - ArcPath arcPath = guiArc.getArcPath(); |
1328 | - int arcPathPointsNum = arcPath.getNumPoints(); |
1329 | - |
1330 | - // Build ArcPath |
1331 | - ArcPath newArcPath = new ArcPath(arc); |
1332 | - for(int k = 0; k < arcPathPointsNum; k++) { |
1333 | - ArcPathPoint point = arcPath.getArcPathPoint(k); |
1334 | - newArcPath.addPoint( |
1335 | - point.getPoint().x + offsetX, |
1336 | - point.getPoint().y + offsetY, |
1337 | - point.getPointType() |
1338 | - ); |
1339 | - } |
1340 | - |
1341 | - return newArcPath; |
1342 | - } |
1343 | - |
1344 | - private void createInputArcs(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping, DataLayer guiModel, double greatestWidth, double greatestHeight) { |
1345 | - int i = 0; |
1346 | - for (TimedArcPetriNet tapn : model.activeTemplates()) { |
1347 | - DataLayer currentGuiModel = this.guiModels.get(tapn); |
1348 | - Tuple<Integer, Integer> offset = this.calculateComponentPosition(i); |
1349 | - |
1350 | - for (TimedInputArc arc : tapn.inputArcs()) { |
1351 | - String sourceTemplate = arc.source().isShared() ? "" : tapn.name(); |
1352 | - TimedPlace source = constructedModel.getPlaceByName(mapping.map(sourceTemplate, arc.source().name())); |
1353 | - |
1354 | - String targetTemplate = arc.destination().isShared() ? "" : tapn.name(); |
1355 | - TimedTransition target = constructedModel.getTransitionByName(mapping.map(targetTemplate, arc.destination().name())); |
1356 | - |
1357 | - TimeInterval newInterval = new TimeInterval(arc.interval()); |
1358 | - newInterval.setLowerBound(new IntBound(newInterval.lowerBound().value())); |
1359 | - if (newInterval.upperBound() instanceof Bound.InfBound) { |
1360 | - newInterval.setUpperBound(newInterval.upperBound()); |
1361 | - } else { |
1362 | - newInterval.setUpperBound(new IntBound(newInterval.upperBound().value())); |
1363 | - } |
1364 | - TimedInputArc addedArc = new TimedInputArc(source, target, newInterval, arc.getWeight()); |
1365 | - constructedModel.add(addedArc); |
1366 | - |
1367 | - Place guiSource = guiModel.getPlaceByName(mapping.map(sourceTemplate, arc.source().name())); |
1368 | - Transition guiTarget = guiModel.getTransitionByName(mapping.map(targetTemplate, arc.destination().name())); |
1369 | - |
1370 | - Arc newArc = new TimedInputArcComponent(new TimedOutputArcComponent( |
1371 | - 0d, |
1372 | - 0d, |
1373 | - 0d, |
1374 | - 0d, |
1375 | - guiSource, |
1376 | - guiTarget, |
1377 | - arc.getWeight().value(), |
1378 | - mapping.map(sourceTemplate, arc.source().name()) + "_to_" + mapping.map(targetTemplate, arc.destination().name()), |
1379 | - false |
1380 | - )); |
1381 | - |
1382 | - // Build ArcPath |
1383 | - Place oldGuiSource = currentGuiModel.getPlaceByName(arc.source().name()); |
1384 | - Transition oldGuiTarget = currentGuiModel.getTransitionByName(arc.destination().name()); |
1385 | - ArcPath newArcPath = createArcPath(currentGuiModel, oldGuiSource, oldGuiTarget, newArc, offset.value1() * greatestWidth, offset.value2() * greatestHeight); |
1386 | - |
1387 | - // Set arcPath, guiModel and connectors |
1388 | - ((TimedInputArcComponent) newArc).setUnderlyingArc(addedArc); |
1389 | - newArc.setArcPath(newArcPath); |
1390 | - newArc.setGuiModel(guiModel); |
1391 | - newArc.updateArcPosition(); |
1392 | - guiModel.addPetriNetObject(newArc); |
1393 | - guiSource.addConnectFrom(newArc); |
1394 | - guiTarget.addConnectTo(newArc); |
1395 | - } |
1396 | - i++; |
1397 | - } |
1398 | - } |
1399 | - |
1400 | - private void createOutputArcs(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping, DataLayer guiModel, double greatestWidth, double greatestHeight) { |
1401 | - int i = 0; |
1402 | - for (TimedArcPetriNet tapn : model.activeTemplates()) { |
1403 | - DataLayer currentGuiModel = this.guiModels.get(tapn); |
1404 | - Tuple<Integer, Integer> offset = this.calculateComponentPosition(i); |
1405 | - |
1406 | - for (TimedOutputArc arc : tapn.outputArcs()) { |
1407 | - String sourceTemplate = arc.source().isShared() ? "" : tapn.name(); |
1408 | - TimedTransition source = constructedModel.getTransitionByName(mapping.map(sourceTemplate, arc.source().name())); |
1409 | - |
1410 | - String destinationTemplate = arc.destination().isShared() ? "" : tapn.name(); |
1411 | - TimedPlace target = constructedModel.getPlaceByName(mapping.map(destinationTemplate, arc.destination().name())); |
1412 | - |
1413 | - TimedOutputArc addedArc = new TimedOutputArc(source, target, arc.getWeight()); |
1414 | - constructedModel.add(addedArc); |
1415 | - |
1416 | - Transition guiSource = guiModel.getTransitionByName(mapping.map(sourceTemplate, arc.source().name())); |
1417 | - Place guiTarget = guiModel.getPlaceByName(mapping.map(destinationTemplate, arc.destination().name())); |
1418 | - |
1419 | - TimedOutputArcComponent newArc = new TimedOutputArcComponent( |
1420 | - 0d, |
1421 | - 0d, |
1422 | - 0d, |
1423 | - 0d, |
1424 | - guiModel.getTransitionByName(mapping.map(sourceTemplate, arc.source().name())), |
1425 | - guiModel.getPlaceByName(mapping.map(destinationTemplate, arc.destination().name())), |
1426 | - arc.getWeight().value(), |
1427 | - mapping.map(sourceTemplate, arc.source().name()) + "_to_" + mapping.map(destinationTemplate, arc.destination().name()), |
1428 | - false |
1429 | - ); |
1430 | - |
1431 | - // Build ArcPath |
1432 | - Transition oldGuiSource = currentGuiModel.getTransitionByName(arc.source().name()); |
1433 | - Place oldGuiTarget = currentGuiModel.getPlaceByName(arc.destination().name()); |
1434 | - ArcPath newArcPath = createArcPath(currentGuiModel, oldGuiSource, oldGuiTarget, newArc, offset.value1() * greatestWidth, offset.value2() * greatestHeight); |
1435 | - |
1436 | - // Set arcPath, guiModel and connectors |
1437 | - newArc.setUnderlyingArc(addedArc); |
1438 | - newArc.setArcPath(newArcPath); |
1439 | - newArc.setGuiModel(guiModel); |
1440 | - newArc.updateArcPosition(); |
1441 | - guiModel.addArc(newArc); |
1442 | - guiSource.addConnectTo(newArc); |
1443 | - guiTarget.addConnectFrom(newArc); |
1444 | - } |
1445 | - i++; |
1446 | - } |
1447 | - } |
1448 | - |
1449 | - private void createTransportArcs(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping, DataLayer guiModel, double greatestWidth, double greatestHeight) { |
1450 | - int i = 0; |
1451 | - int nextGroupNr = 0; |
1452 | - for (TimedArcPetriNet tapn : model.activeTemplates()) { |
1453 | - DataLayer currentGuiModel = this.guiModels.get(tapn); |
1454 | - Tuple<Integer, Integer> offset = this.calculateComponentPosition(i); |
1455 | - |
1456 | - for (TransportArc arc : tapn.transportArcs()) { |
1457 | - String sourceTemplate = arc.source().isShared() ? "" : tapn.name(); |
1458 | - String transitionTemplate = arc.transition().isShared() ? "" : tapn.name(); |
1459 | - String destinationTemplate = arc.destination().isShared() ? "" : tapn.name(); |
1460 | - |
1461 | - TimedPlace source = constructedModel.getPlaceByName(mapping.map(sourceTemplate, arc.source().name())); |
1462 | - TimedTransition transition = constructedModel.getTransitionByName(mapping.map(transitionTemplate, arc.transition().name())); |
1463 | - TimedPlace destination = constructedModel.getPlaceByName(mapping.map(destinationTemplate, arc.destination().name())); |
1464 | - |
1465 | - TimeInterval newInterval = new TimeInterval(arc.interval()); |
1466 | - newInterval.setLowerBound(new IntBound(newInterval.lowerBound().value())); |
1467 | - if (newInterval.upperBound() instanceof Bound.InfBound) { |
1468 | - newInterval.setUpperBound(newInterval.upperBound()); |
1469 | - } else { |
1470 | - newInterval.setUpperBound(new IntBound(newInterval.upperBound().value())); |
1471 | - } |
1472 | - TransportArc addedArc = new TransportArc(source, transition, destination, newInterval, arc.getWeight()); |
1473 | - constructedModel.add(addedArc); |
1474 | - |
1475 | - //Create input transport arc |
1476 | - Place guiSourceIn = guiModel.getPlaceByName(mapping.map(sourceTemplate, arc.source().name())); |
1477 | - Transition guiTargetIn = guiModel.getTransitionByName(mapping.map(transitionTemplate, arc.transition().name())); |
1478 | - |
1479 | - TimedTransportArcComponent newInArc = new TimedTransportArcComponent( |
1480 | - new TimedInputArcComponent(new TimedOutputArcComponent( |
1481 | - 0d, |
1482 | - 0d, |
1483 | - 0d, |
1484 | - 0d, |
1485 | - guiSourceIn, |
1486 | - guiTargetIn, |
1487 | - arc.getWeight().value(), |
1488 | - mapping.map(sourceTemplate, arc.source().name()) + "_to_" + mapping.map(transitionTemplate, arc.transition().name()), |
1489 | - false |
1490 | - )), |
1491 | - nextGroupNr, |
1492 | - true |
1493 | - ); |
1494 | - |
1495 | - // Build ArcPath |
1496 | - Place oldGuiSourceIn = currentGuiModel.getPlaceByName(arc.source().name()); |
1497 | - Transition oldGuiTargetIn = currentGuiModel.getTransitionByName(arc.transition().name()); |
1498 | - ArcPath newArcPathIn = createArcPath(currentGuiModel, oldGuiSourceIn, oldGuiTargetIn, newInArc, offset.value1() * greatestWidth, offset.value2() * greatestHeight); |
1499 | - |
1500 | - newInArc.setUnderlyingArc(addedArc); |
1501 | - newInArc.setArcPath(newArcPathIn); |
1502 | - newInArc.setGuiModel(guiModel); |
1503 | - newInArc.updateArcPosition(); |
1504 | - guiModel.addArc(newInArc); |
1505 | - |
1506 | - guiSourceIn.addConnectTo(newInArc); |
1507 | - guiTargetIn.addConnectFrom(newInArc); |
1508 | - |
1509 | - // Calculate the next group number for this transport arc |
1510 | - // By looking at the target of the newInArc -> a transition |
1511 | - // Then finding the largest existing group number of outgoing transport arcs from this transition |
1512 | - for (Object pt : newInArc.getTarget().getPostset()) { |
1513 | - if (pt instanceof TimedTransportArcComponent) { |
1514 | - if (((TimedTransportArcComponent) pt).getGroupNr() > nextGroupNr) { |
1515 | - nextGroupNr = ((TimedTransportArcComponent) pt).getGroupNr(); |
1516 | - } |
1517 | - } |
1518 | - } |
1519 | - |
1520 | - ((TimedTransportArcComponent) newInArc).setGroupNr(nextGroupNr + 1); |
1521 | - |
1522 | - //Create output transport arc |
1523 | - Transition guiSourceOut = guiModel.getTransitionByName(mapping.map(transitionTemplate, arc.transition().name())); |
1524 | - Place guiTargetOut = guiModel.getPlaceByName(mapping.map(destinationTemplate, arc.destination().name())); |
1525 | - |
1526 | - TimedTransportArcComponent newOutArc = new TimedTransportArcComponent( |
1527 | - new TimedInputArcComponent(new TimedOutputArcComponent( |
1528 | - 0d, |
1529 | - 0d, |
1530 | - 0d, |
1531 | - 0d, |
1532 | - guiSourceOut, |
1533 | - guiTargetOut, |
1534 | - 1, |
1535 | - mapping.map(transitionTemplate, arc.transition().name()) + "_to_" + mapping.map(destinationTemplate, arc.destination().name()), |
1536 | - false |
1537 | - )), |
1538 | - nextGroupNr + 1, |
1539 | - false |
1540 | - ); |
1541 | - |
1542 | - // Build ArcPath |
1543 | - Transition oldGuiSourceOut = currentGuiModel.getTransitionByName(arc.transition().name()); |
1544 | - Place oldGuiTargetOut = currentGuiModel.getPlaceByName(arc.destination().name()); |
1545 | - ArcPath newArcPathOut = createArcPath(currentGuiModel, oldGuiSourceOut, oldGuiTargetOut, newOutArc, offset.value1() * greatestWidth, offset.value2() * greatestHeight); |
1546 | - |
1547 | - newOutArc.setUnderlyingArc(addedArc); |
1548 | - newOutArc.setArcPath(newArcPathOut); |
1549 | - newOutArc.setGuiModel(guiModel); |
1550 | - newOutArc.updateArcPosition(); |
1551 | - guiModel.addArc(newOutArc); |
1552 | - |
1553 | - // Add connection references to the two transport arcs |
1554 | - newInArc.setConnectedTo(newOutArc); |
1555 | - newOutArc.setConnectedTo(newInArc); |
1556 | - |
1557 | - guiSourceOut.addConnectTo(newOutArc); |
1558 | - guiTargetOut.addConnectFrom(newOutArc); |
1559 | - } |
1560 | - i++; |
1561 | - } |
1562 | - } |
1563 | - |
1564 | - |
1565 | - |
1566 | - private void createInhibitorArcs(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping, DataLayer guiModel, double greatestWidth, double greatestHeight) { |
1567 | - int i = 0; |
1568 | - for (TimedArcPetriNet tapn : model.activeTemplates()) { |
1569 | - DataLayer currentGuiModel = this.guiModels.get(tapn); |
1570 | - Tuple<Integer, Integer> offset = this.calculateComponentPosition(i); |
1571 | - |
1572 | - for (TimedInhibitorArc arc : tapn.inhibitorArcs()) { |
1573 | - String sourceTemplate = arc.source().isShared() ? "" : tapn.name(); |
1574 | - String destinationTemplate = arc.destination().isShared() ? "" : tapn.name(); |
1575 | - |
1576 | - TimedPlace source = constructedModel.getPlaceByName(mapping.map(sourceTemplate, arc.source().name())); |
1577 | - TimedTransition target = constructedModel.getTransitionByName(mapping.map(destinationTemplate, arc.destination().name())); |
1578 | - |
1579 | - TimeInterval newInterval = new TimeInterval(arc.interval()); |
1580 | - newInterval.setLowerBound(new IntBound(newInterval.lowerBound().value())); |
1581 | - if (newInterval.upperBound() instanceof Bound.InfBound) { |
1582 | - newInterval.setUpperBound(newInterval.upperBound()); |
1583 | - } else { |
1584 | - newInterval.setUpperBound(new IntBound(newInterval.upperBound().value())); |
1585 | - } |
1586 | - TimedInhibitorArc addedArc = new TimedInhibitorArc(source, target, newInterval, arc.getWeight()); |
1587 | - constructedModel.add(addedArc); |
1588 | - |
1589 | - Place guiSource = guiModel.getPlaceByName(mapping.map(sourceTemplate, arc.source().name())); |
1590 | - Transition guiTarget = guiModel.getTransitionByName(mapping.map(destinationTemplate, arc.destination().name())); |
1591 | - Arc newArc = new TimedInhibitorArcComponent(new TimedOutputArcComponent( |
1592 | - 0d, |
1593 | - 0d, |
1594 | - 0d, |
1595 | - 0d, |
1596 | - guiSource, |
1597 | - guiTarget, |
1598 | - arc.getWeight().value(), |
1599 | - mapping.map(sourceTemplate, arc.source().name()) + "_to_" + mapping.map(destinationTemplate, arc.destination().name()), |
1600 | - false |
1601 | - ), ""); |
1602 | - |
1603 | - // Build ArcPath |
1604 | - Place oldGuiSource = currentGuiModel.getPlaceByName(arc.source().name()); |
1605 | - Transition oldGuiTarget = currentGuiModel.getTransitionByName(arc.destination().name()); |
1606 | - ArcPath newArcPath = createArcPath(currentGuiModel, oldGuiSource, oldGuiTarget, newArc, offset.value1() * greatestWidth, offset.value2() * greatestHeight); |
1607 | - |
1608 | - ((TimedInhibitorArcComponent) newArc).setUnderlyingArc(addedArc); |
1609 | - newArc.setArcPath(newArcPath); |
1610 | - newArc.setGuiModel(guiModel); |
1611 | - newArc.updateArcPosition(); |
1612 | - guiModel.addPetriNetObject(newArc); |
1613 | - guiSource.addConnectTo(newArc); |
1614 | - guiTarget.addConnectFrom(newArc); |
1615 | - } |
1616 | - i++; |
1617 | - } |
1618 | - } |
1619 | -} |
1620 | |
1621 | === modified file 'src/pipe/gui/widgets/QueryDialog.java' |
1622 | --- src/pipe/gui/widgets/QueryDialog.java 2014-05-28 19:07:25 +0000 |
1623 | +++ src/pipe/gui/widgets/QueryDialog.java 2014-06-07 16:33:21 +0000 |
1624 | @@ -119,7 +119,6 @@ |
1625 | import dk.aau.cs.verification.ITAPNComposer; |
1626 | import dk.aau.cs.verification.NameMapping; |
1627 | import dk.aau.cs.verification.TAPNComposer; |
1628 | -import dk.aau.cs.verification.TAPNComposerWithGUI; |
1629 | import dk.aau.cs.verification.UPPAAL.UppaalExporter; |
1630 | import dk.aau.cs.verification.VerifyTAPN.ModelReduction; |
1631 | import dk.aau.cs.verification.VerifyTAPN.VerifyPNExporter; |
1632 | @@ -2604,7 +2603,7 @@ |
1633 | |
1634 | openComposedNetButton.addActionListener(new ActionListener() { |
1635 | public void actionPerformed(ActionEvent e) { |
1636 | - TAPNComposerWithGUI composer = new TAPNComposerWithGUI(new MessengerImpl(), guiModels); |
1637 | + TAPNComposer composer = new TAPNComposer(new MessengerImpl(), guiModels); |
1638 | Tuple<TimedArcPetriNet, NameMapping> transformedModel = composer.transformModel(tapnNetwork); |
1639 | |
1640 | ArrayList<Template> templates = new ArrayList<Template>(1); |
1641 | @@ -2617,9 +2616,9 @@ |
1642 | else if (underApproximationEnable.isSelected()) |
1643 | { |
1644 | UnderApproximation underaprx = new UnderApproximation(); |
1645 | - underaprx.modifyTAPN(transformedModel.value1(), getQuery().approximationDenominator(), ((TAPNComposerWithGUI) composer).getGuiModel()); |
1646 | + underaprx.modifyTAPN(transformedModel.value1(), getQuery().approximationDenominator(), ((TAPNComposer) composer).getGuiModel()); |
1647 | } |
1648 | - templates.add(new Template(transformedModel.value1(), ((TAPNComposerWithGUI) composer).getGuiModel(), new Zoomer())); |
1649 | + templates.add(new Template(transformedModel.value1(), ((TAPNComposer) composer).getGuiModel(), new Zoomer())); |
1650 | |
1651 | // Create a constant store |
1652 | ConstantStore newConstantStore = new ConstantStore(); |
Why is the code at lines 73-107 removed?