Merge lp:~tapaal-approx/tapaal/TAPNComposerWithGUI into lp:tapaal

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
Reviewer Review Type Date Requested Status
Jakob Taankvist (community) Approve
Jiri Srba Approve
Mathias Grund Sørensen (community) code Approve
Review via email: mp+222407@code.launchpad.net

Commit message

Removes TAPNComposer and replaces it with TAPNComposerWithGUI.
Also fixes some issues with reporting verification time for approximations.

Description of the change

Removes TAPNComposer and replaces it with TAPNComposerWithGUI.
Also fixes some issues with reporting verification time for approximations.

To post a comment you must log in.
866. By Jiri Srba

merged with trunk

Revision history for this message
Jiri Srba (srba) wrote :

Why is the code at lines 73-107 removed?

review: Needs Information
Revision history for this message
Thomas Stig Jacobsen (tsja10) wrote :

The code was unused in the class

Revision history for this message
Mathias Grund Sørensen (mathias.grund) wrote :

Looks as expected

review: Approve (code)
Revision history for this message
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
867. By Jiri Srba

refactoring: TAPNComposerWithGui renamed to TAPNComposer

Revision history for this message
Jiri Srba (srba) wrote :

Refactoring done. I will merge it to trunk now.

review: Approve
Revision history for this message
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();

Subscribers

People subscribed via source and target branches