Merge lp:~yrke/tapaal/cleanup-PNO-namingAndInterface into lp:tapaal
- cleanup-PNO-namingAndInterface
- Merge into trunk
Status: | Merged | ||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Approved by: | Jiri Srba | ||||||||||||
Approved revision: | 1211 | ||||||||||||
Merged at revision: | 1067 | ||||||||||||
Proposed branch: | lp:~yrke/tapaal/cleanup-PNO-namingAndInterface | ||||||||||||
Merge into: | lp:tapaal | ||||||||||||
Diff against target: |
11415 lines (+4524/-4480) 68 files modified
src/dk/aau/cs/gui/SharedPlacesAndTransitionsPanel.java (+14/-16) src/dk/aau/cs/gui/TabContent.java (+1097/-180) src/dk/aau/cs/gui/TemplateExplorer.java (+56/-58) src/dk/aau/cs/gui/components/EnabledTransitionsList.java (+9/-83) src/dk/aau/cs/gui/components/NonsearchableJList.java (+1/-1) src/dk/aau/cs/gui/components/TransitionFireingComponent.java (+12/-6) src/dk/aau/cs/gui/smartDraw/SmartDrawWorker.java (+9/-13) src/dk/aau/cs/gui/undo/TimedPlaceMarkingEdit.java (+5/-5) src/dk/aau/cs/io/TapnXmlLoader.java (+2/-3) src/dk/aau/cs/model/tapn/LocalTimedPlace.java (+1/-118) src/dk/aau/cs/model/tapn/NetworkMarking.java (+5/-4) src/dk/aau/cs/model/tapn/SharedPlace.java (+6/-122) src/dk/aau/cs/model/tapn/TimedArcPetriNet.java (+8/-13) src/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java (+7/-8) src/dk/aau/cs/model/tapn/TimedInhibitorArc.java (+6/-2) src/dk/aau/cs/model/tapn/TimedPlace.java (+114/-31) src/dk/aau/cs/model/tapn/TimedToken.java (+2/-8) src/dk/aau/cs/model/tapn/TimedTransition.java (+5/-5) src/dk/aau/cs/model/tapn/TransportArc.java (+6/-2) src/net/tapaal/gui/DrawingSurfaceManager/AbstractDrawingSurfaceManager.java (+14/-4) src/net/tapaal/swinghelpers/DispatchEventsToParentHandler.java (+58/-0) src/pipe/dataLayer/DataLayer.java (+158/-197) src/pipe/dataLayer/Template.java (+3/-8) src/pipe/gui/AnimationHistoryList.java (+1/-1) src/pipe/gui/Animator.java (+610/-622) src/pipe/gui/CreateGui.java (+7/-8) src/pipe/gui/DelayEnabledTransitionControl.java (+7/-8) src/pipe/gui/GuiFrame.java (+1554/-1575) src/pipe/gui/GuiFrameController.java (+1/-1) src/pipe/gui/SelectionManager.java (+43/-27) src/pipe/gui/SimulationControl.java (+11/-21) src/pipe/gui/action/SplitArcAction.java (+6/-2) src/pipe/gui/canvas/Canvas.java (+3/-2) src/pipe/gui/canvas/DrawingSurfaceImpl.java (+49/-222) src/pipe/gui/canvas/PrototypeCanvas.java (+3/-2) src/pipe/gui/graphicElements/AnnotationNote.java (+5/-4) src/pipe/gui/graphicElements/Arc.java (+34/-34) src/pipe/gui/graphicElements/ArcPath.java (+34/-32) src/pipe/gui/graphicElements/ArcPathPoint.java (+35/-32) src/pipe/gui/graphicElements/Drawable.java (+7/-0) src/pipe/gui/graphicElements/GraphicalElement.java (+162/-0) src/pipe/gui/graphicElements/Note.java (+1/-4) src/pipe/gui/graphicElements/PetriNetObject.java (+15/-62) src/pipe/gui/graphicElements/PetriNetObjectWithLabel.java (+6/-33) src/pipe/gui/graphicElements/Place.java (+2/-5) src/pipe/gui/graphicElements/PlaceTransitionObject.java (+26/-48) src/pipe/gui/graphicElements/Transition.java (+53/-122) src/pipe/gui/graphicElements/tapn/TimedInhibitorArcComponent.java (+9/-1) src/pipe/gui/graphicElements/tapn/TimedInputArcComponent.java (+9/-0) src/pipe/gui/graphicElements/tapn/TimedOutputArcComponent.java (+11/-3) src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java (+13/-31) src/pipe/gui/graphicElements/tapn/TimedTransitionComponent.java (+21/-11) src/pipe/gui/graphicElements/tapn/TimedTransportArcComponent.java (+22/-0) src/pipe/gui/handler/AnnotationNoteHandler.java (+0/-15) src/pipe/gui/handler/ArcHandler.java (+42/-36) src/pipe/gui/handler/ArcPathPointHandler.java (+0/-1) src/pipe/gui/handler/LabelHandler.java (+10/-10) src/pipe/gui/handler/NoteHandler.java (+0/-1) src/pipe/gui/handler/PetriNetObjectHandler.java (+11/-10) src/pipe/gui/handler/PlaceHandler.java (+12/-69) src/pipe/gui/handler/PlaceTransitionObjectHandler.java (+34/-480) src/pipe/gui/handler/TimedArcHandler.java (+0/-5) src/pipe/gui/handler/TransitionHandler.java (+0/-28) src/pipe/gui/handler/TransportArcHandler.java (+1/-1) src/pipe/gui/undo/TranslatePetriNetObjectEdit.java (+7/-8) src/pipe/gui/undo/UndoManager.java (+3/-14) src/pipe/gui/widgets/ArcTokenSelector.java (+1/-1) tests/dk/aau/cs/io/TapnXmlLoaderTest.kt (+45/-1) |
||||||||||||
To merge this branch: | bzr merge lp:~yrke/tapaal/cleanup-PNO-namingAndInterface | ||||||||||||
Related bugs: |
|
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
Jiri Srba | Approve | ||
Peter Haahr Taankvist (community) | Approve | ||
Lena Ernstsen (community) | Approve | ||
Kenneth Yrke Jørgensen | Needs Resubmitting | ||
Review via email: mp+386803@code.launchpad.net |
Commit message
Description of the change
Kenneth Yrke Jørgensen (yrke) wrote : | # |
- 1206. By Kenneth Yrke Jørgensen
-
Merged changes from other computer
- 1207. By Kenneth Yrke Jørgensen
-
Removed color
- 1208. By Kenneth Yrke Jørgensen
-
Corrected spelling
Peter Haahr Taankvist (ptaank) wrote : | # |
Open alternating-
Peter Haahr Taankvist (ptaank) wrote : | # |
The problem with pressing shift+U many times still persists:
Open alternating-
press shift+U 23 times
now press ctrl+U some times
The spacing will not increase, rather the places will all stay on top of each other and arcpathpoints will fly everywhere.
Peter Haahr Taankvist (ptaank) wrote : | # |
> The problem with pressing shift+U many times still persists:
>
> Open alternating-
>
> press shift+U 23 times
>
> now press ctrl+U some times
>
> The spacing will not increase, rather the places will all stay on top of each
> other and arcpathpoints will fly everywhere.
What's worse is that the same happens with ctrl+z
Peter Haahr Taankvist (ptaank) wrote : | # |
It is not possible to undo resizing of annotation notes
Lena Ernstsen (lsaid) wrote : | # |
1)
When I select ‘place’ and want to add it to the the component I sometimes have to click several times before it registers and adds the ‘place’. Same goes for transitions, tokens, and the different arcs.
2)
The positions of the different arcs are shown as ‘X:0 Y:0’. But I'm not sure if this is relevant or not.
3)
There is a weird behaviour when moving an arc with extra inserted points. When moving such and arc a little to the right, then it moves very fast by itself to the far right and goes off screen. When undoing, the arc does not return to how it was setup before moving it, but rather it stays to the far right and removes the extra points.
The same thing happens if you move the end point of an arc with an extra point a little down.
Peter Haahr Taankvist (ptaank) wrote : | # |
> 1)
> When I select ‘place’ and want to add it to the the component I sometimes have
> to click several times before it registers and adds the ‘place’. Same goes for
> transitions, tokens, and the different arcs.
>
> 2)
> The positions of the different arcs are shown as ‘X:0 Y:0’. But I'm not sure
> if this is relevant or not.
>
> 3)
> There is a weird behaviour when moving an arc with extra inserted points. When
> moving such and arc a little to the right, then it moves very fast by itself
> to the far right and goes off screen. When undoing, the arc does not return to
> how it was setup before moving it, but rather it stays to the far right and
> removes the extra points.
> The same thing happens if you move the end point of an arc with an extra point
> a little down.
How to reproduce #3
Place a place and a transition and draw an arc between them. Now drag at one of the endpoints and the arcs will fly all over.
Peter Haahr Taankvist (ptaank) wrote : | # |
> 1)
> When I select ‘place’ and want to add it to the the component I sometimes have
> to click several times before it registers and adds the ‘place’. Same goes for
> transitions, tokens, and the different arcs.
>
> 2)
> The positions of the different arcs are shown as ‘X:0 Y:0’. But I'm not sure
> if this is relevant or not.
>
> 3)
> There is a weird behaviour when moving an arc with extra inserted points. When
> moving such and arc a little to the right, then it moves very fast by itself
> to the far right and goes off screen. When undoing, the arc does not return to
> how it was setup before moving it, but rather it stays to the far right and
> removes the extra points.
> The same thing happens if you move the end point of an arc with an extra point
> a little down.
4)
#1 To add to this it also seems that it has a hard time registering a click on an enabled transition in animation mode.
Peter Haahr Taankvist (ptaank) wrote : | # |
5)
Adding text to an annotation note and then undoing does not undo the size of the annotation note.
- 1209. By Kenneth Yrke Jørgensen
-
Changed mouse clicked events to mouse down
- 1210. By Kenneth Yrke Jørgensen
-
Disabled dragging arcs
Current implementation does not support this
- 1211. By Kenneth Yrke Jørgensen
-
Moved adding of arcpath point with doubleclick to new controller
Kenneth Yrke Jørgensen (yrke) wrote : | # |
Changed draw from click to mouse down, addresses #1,4. #2 is as expected, #3 is also in trunk but added a fix so you can't draw on an arc.
Lena Ernstsen (lsaid) : | # |
Peter Haahr Taankvist (ptaank) : | # |
Jiri Srba (srba) : | # |
Preview Diff
1 | === modified file 'src/dk/aau/cs/gui/SharedPlacesAndTransitionsPanel.java' |
2 | --- src/dk/aau/cs/gui/SharedPlacesAndTransitionsPanel.java 2020-05-27 13:15:44 +0000 |
3 | +++ src/dk/aau/cs/gui/SharedPlacesAndTransitionsPanel.java 2020-07-09 12:55:48 +0000 |
4 | @@ -45,17 +45,17 @@ |
5 | private static final String TRANSITIONS = "Transitions"; |
6 | private static final String PLACES = "Places"; |
7 | |
8 | - private JList list; |
9 | - private SharedPlacesListModel sharedPlacesListModel; |
10 | - private SharedTransitionsListModel sharedTransitionsListModel; |
11 | - private JComboBox placesTransitionsComboBox; |
12 | - private UndoManager undoManager; |
13 | - private NameGenerator nameGenerator; |
14 | - private TabContent tab; |
15 | + private final JList list = new NonsearchableJList(); |
16 | + private final SharedPlacesListModel sharedPlacesListModel; |
17 | + private final SharedTransitionsListModel sharedTransitionsListModel; |
18 | + private final JComboBox placesTransitionsComboBox = new JComboBox(new String[]{ PLACES, TRANSITIONS }); |
19 | + private final UndoManager undoManager; |
20 | + private final NameGenerator nameGenerator; |
21 | + private final TabContent tab; |
22 | |
23 | - private JButton renameButton = new JButton("Rename"); |
24 | - private JButton removeButton = new JButton("Remove"); |
25 | - private JButton addButton = new JButton("New"); |
26 | + private final JButton renameButton = new JButton("Rename"); |
27 | + private final JButton removeButton = new JButton("Remove"); |
28 | + private final JButton addButton = new JButton("New"); |
29 | private JButton moveUpButton; |
30 | private JButton moveDownButton; |
31 | private JButton sortButton; |
32 | @@ -128,9 +128,8 @@ |
33 | |
34 | private void initComponents() { |
35 | JPanel listPanel = new JPanel(new GridBagLayout()); |
36 | - |
37 | - list = new NonsearchableJList(); |
38 | - list.addListSelectionListener(new ListSelectionListener() { |
39 | + |
40 | + list.addListSelectionListener(new ListSelectionListener() { |
41 | public void valueChanged(ListSelectionEvent e) { |
42 | if(!e.getValueIsAdjusting()){ |
43 | JList source = (JList)e.getSource(); |
44 | @@ -262,9 +261,8 @@ |
45 | gbc.fill = GridBagConstraints.HORIZONTAL; |
46 | gbc.anchor = GridBagConstraints.NORTH; |
47 | listPanel.add(sortButton,gbc); |
48 | - |
49 | - placesTransitionsComboBox = new JComboBox(new String[]{ PLACES, TRANSITIONS }); |
50 | - placesTransitionsComboBox.setToolTipText(toolTipChangeBetweenPlacesAndTransitions); |
51 | + |
52 | + placesTransitionsComboBox.setToolTipText(toolTipChangeBetweenPlacesAndTransitions); |
53 | placesTransitionsComboBox.addActionListener(e -> { |
54 | JComboBox source = (JComboBox)e.getSource(); |
55 | String selectedItem = (String)source.getSelectedItem(); |
56 | |
57 | === modified file 'src/dk/aau/cs/gui/TabContent.java' |
58 | --- src/dk/aau/cs/gui/TabContent.java 2020-06-22 07:41:12 +0000 |
59 | +++ src/dk/aau/cs/gui/TabContent.java 2020-07-09 12:55:48 +0000 |
60 | @@ -3,6 +3,7 @@ |
61 | import java.awt.*; |
62 | import java.awt.event.MouseAdapter; |
63 | import java.awt.event.MouseEvent; |
64 | +import java.awt.geom.Point2D; |
65 | import java.io.*; |
66 | import java.math.BigDecimal; |
67 | import java.util.*; |
68 | @@ -11,12 +12,11 @@ |
69 | import javax.swing.*; |
70 | import javax.swing.border.BevelBorder; |
71 | |
72 | -import dk.aau.cs.approximation.OverApproximation; |
73 | -import dk.aau.cs.approximation.UnderApproximation; |
74 | import dk.aau.cs.debug.Logger; |
75 | import dk.aau.cs.gui.components.StatisticsPanel; |
76 | import dk.aau.cs.gui.undo.Command; |
77 | import dk.aau.cs.gui.undo.DeleteQueriesCommand; |
78 | +import dk.aau.cs.gui.undo.TimedPlaceMarkingEdit; |
79 | import dk.aau.cs.io.*; |
80 | import dk.aau.cs.io.queries.SUMOQueryLoader; |
81 | import dk.aau.cs.io.queries.XMLQueryLoader; |
82 | @@ -35,12 +35,13 @@ |
83 | import pipe.gui.*; |
84 | import pipe.gui.canvas.DrawingSurfaceImpl; |
85 | import pipe.gui.graphicElements.*; |
86 | -import pipe.gui.graphicElements.tapn.TimedPlaceComponent; |
87 | -import pipe.gui.graphicElements.tapn.TimedTransitionComponent; |
88 | -import pipe.gui.handler.PlaceTransitionObjectHandler; |
89 | +import pipe.gui.graphicElements.tapn.*; |
90 | +import pipe.gui.undo.*; |
91 | +import pipe.gui.widgets.ConstantsPane; |
92 | import pipe.gui.undo.ChangeSpacingEdit; |
93 | import pipe.gui.undo.UndoManager; |
94 | import pipe.gui.widgets.*; |
95 | + |
96 | import net.tapaal.swinghelpers.JSplitPaneFix; |
97 | import dk.aau.cs.gui.components.BugHandledJXMultisplitPane; |
98 | import dk.aau.cs.gui.components.TransitionFireingComponent; |
99 | @@ -49,37 +50,443 @@ |
100 | |
101 | public class TabContent extends JSplitPane implements TabContentActions{ |
102 | |
103 | + static class TAPNLens { |
104 | + public boolean isTimed() { |
105 | + return timed; |
106 | + } |
107 | + |
108 | + public boolean isGame() { |
109 | + return game; |
110 | + } |
111 | + |
112 | + private final boolean timed; |
113 | + private final boolean game; |
114 | + |
115 | + TAPNLens(boolean timed, boolean game) { |
116 | + this.timed = timed; |
117 | + this.game = game; |
118 | + } |
119 | + } |
120 | + private final TAPNLens lens; |
121 | + |
122 | //Model and state |
123 | - private TimedArcPetriNetNetwork tapnNetwork = new TimedArcPetriNetNetwork(); |
124 | - private HashMap<TimedArcPetriNet, DataLayer> guiModels = new HashMap<TimedArcPetriNet, DataLayer>(); |
125 | - private HashMap<TimedArcPetriNet, Zoomer> zoomLevels = new HashMap<TimedArcPetriNet, Zoomer>(); |
126 | - |
127 | - |
128 | - private UndoManager undoManager = new UndoManager(); |
129 | + private final TimedArcPetriNetNetwork tapnNetwork; |
130 | + |
131 | + //XXX: Replace with bi-map |
132 | + private final HashMap<TimedArcPetriNet, DataLayer> guiModels = new HashMap<TimedArcPetriNet, DataLayer>(); |
133 | + private final HashMap<DataLayer, TimedArcPetriNet> guiModelToModel = new HashMap<>(); |
134 | + |
135 | + private final HashMap<TimedArcPetriNet, Zoomer> zoomLevels = new HashMap<TimedArcPetriNet, Zoomer>(); |
136 | + |
137 | + |
138 | + private final UndoManager undoManager = new UndoManager(); |
139 | + |
140 | + public final GuiModelManager guiModelManager = new GuiModelManager(); |
141 | + public class GuiModelManager { |
142 | + public GuiModelManager(){ |
143 | + |
144 | + } |
145 | + |
146 | + public void addNewTimedPlace(DataLayer c, Point p){ |
147 | + Require.notNull(c, "datalyer can't be null"); |
148 | + Require.notNull(p, "Point can't be null"); |
149 | + |
150 | + dk.aau.cs.model.tapn.LocalTimedPlace tp = new dk.aau.cs.model.tapn.LocalTimedPlace(drawingSurface.getNameGenerator().getNewPlaceName(guiModelToModel.get(c))); |
151 | + TimedPlaceComponent pnObject = new TimedPlaceComponent(p.x, p.y, tp); |
152 | + guiModelToModel.get(c).add(tp); |
153 | + c.addPetriNetObject(pnObject); |
154 | + |
155 | + getUndoManager().addNewEdit(new AddTimedPlaceCommand(pnObject, guiModelToModel.get(c), c)); |
156 | + |
157 | + } |
158 | + |
159 | + public void addNewTimedTransitions(DataLayer c, Point p) { |
160 | + dk.aau.cs.model.tapn.TimedTransition transition = new dk.aau.cs.model.tapn.TimedTransition(drawingSurface.getNameGenerator().getNewTransitionName(guiModelToModel.get(c))); |
161 | + |
162 | + TimedTransitionComponent pnObject = new TimedTransitionComponent(p.x, p.y, transition); |
163 | + |
164 | + guiModelToModel.get(c).add(transition); |
165 | + c.addPetriNetObject(pnObject); |
166 | + |
167 | + getUndoManager().addNewEdit(new AddTimedTransitionCommand(pnObject, guiModelToModel.get(c), c)); |
168 | + } |
169 | + |
170 | + public void addAnnotationNote(DataLayer c, Point p) { |
171 | + AnnotationNote pnObject = new AnnotationNote(p.x, p.y); |
172 | + |
173 | + //enableEditMode open editor, retuns true of text added, else false |
174 | + //If no text is added,dont add it to model |
175 | + if (pnObject.enableEditMode(true)) { |
176 | + c.addPetriNetObject(pnObject); |
177 | + getUndoManager().addEdit(new AddAnnotationNoteCommand(pnObject, c)); |
178 | + } |
179 | + } |
180 | + |
181 | + public void addTimedInputArc(DataLayer c, TimedPlaceComponent p, TimedTransitionComponent t, ArcPath path) { |
182 | + Require.notNull(c, "DataLayer can't be null"); |
183 | + Require.notNull(p, "Place can't be null"); |
184 | + Require.notNull(t, "Transitions can't be null"); |
185 | + |
186 | + TimedArcPetriNet modelNet = guiModelToModel.get(c); |
187 | + |
188 | + if (!modelNet.hasArcFromPlaceToTransition(p.underlyingPlace(), t.underlyingTransition())) { |
189 | + |
190 | + TimedInputArc tia = new TimedInputArc( |
191 | + p.underlyingPlace(), |
192 | + t.underlyingTransition(), |
193 | + TimeInterval.ZERO_INF |
194 | + ); |
195 | + |
196 | + TimedInputArcComponent tiac = new TimedInputArcComponent(p,t,tia); |
197 | + |
198 | + if (path != null) { |
199 | + tiac.setArcPath(new ArcPath(tiac, path)); |
200 | + } |
201 | + |
202 | + Command edit = new AddTimedInputArcCommand( |
203 | + tiac, |
204 | + modelNet, |
205 | + c |
206 | + ); |
207 | + edit.redo(); |
208 | + |
209 | + undoManager.addNewEdit(edit); |
210 | + |
211 | + } else { |
212 | + //TODO: can't have two arcs between place and transition |
213 | + JOptionPane.showMessageDialog( |
214 | + CreateGui.getApp(), |
215 | + "There was an error drawing the arc. Possible problems:\n" |
216 | + + " - There is already an arc between the selected place and transition\n" |
217 | + + " - You are attempting to draw an arc between a shared transition and a shared place", |
218 | + "Error", JOptionPane.ERROR_MESSAGE |
219 | + ); |
220 | + } |
221 | + } |
222 | + |
223 | + public void addTimedOutputArc(DataLayer c, TimedTransitionComponent t, TimedPlaceComponent p, ArcPath path) { |
224 | + Require.notNull(c, "DataLayer can't be null"); |
225 | + Require.notNull(p, "Place can't be null"); |
226 | + Require.notNull(t, "Transitions can't be null"); |
227 | + |
228 | + TimedArcPetriNet modelNet = guiModelToModel.get(c); |
229 | + |
230 | + if (!modelNet.hasArcFromTransitionToPlace(t.underlyingTransition(), p.underlyingPlace())) { |
231 | + |
232 | + TimedOutputArc toa = new TimedOutputArc( |
233 | + t.underlyingTransition(), |
234 | + p.underlyingPlace() |
235 | + ); |
236 | + |
237 | + TimedOutputArcComponent toac = new TimedOutputArcComponent(t, p, toa); |
238 | + |
239 | + if (path != null) { |
240 | + toac.setArcPath(new ArcPath(toac, path)); |
241 | + } |
242 | + |
243 | + Command edit = new AddTimedOutputArcCommand( |
244 | + toac, |
245 | + modelNet, |
246 | + c |
247 | + ); |
248 | + edit.redo(); |
249 | + undoManager.addNewEdit(edit); |
250 | + |
251 | + } else { |
252 | + |
253 | + JOptionPane.showMessageDialog( |
254 | + CreateGui.getApp(), |
255 | + "There was an error drawing the arc. Possible problems:\n" |
256 | + + " - There is already an arc between the selected place and transition\n" |
257 | + + " - You are attempting to draw an arc between a shared transition and a shared place", |
258 | + "Error", JOptionPane.ERROR_MESSAGE |
259 | + ); |
260 | + |
261 | + } |
262 | + |
263 | + |
264 | + } |
265 | + |
266 | + public void addInhibitorArc(DataLayer c, TimedPlaceComponent p, TimedTransitionComponent t, ArcPath path) { |
267 | + Require.notNull(c, "DataLayer can't be null"); |
268 | + Require.notNull(p, "Place can't be null"); |
269 | + Require.notNull(t, "Transitions can't be null"); |
270 | + |
271 | + TimedArcPetriNet modelNet = guiModelToModel.get(c); |
272 | + |
273 | + if (!modelNet.hasArcFromPlaceToTransition(p.underlyingPlace(), t.underlyingTransition())) { |
274 | + |
275 | + TimedInhibitorArc tiha = new TimedInhibitorArc( |
276 | + p.underlyingPlace(), |
277 | + t.underlyingTransition() |
278 | + ); |
279 | + |
280 | + TimedInhibitorArcComponent tihac = new TimedInhibitorArcComponent(p, t, tiha); |
281 | + |
282 | + if (path != null) { |
283 | + tihac.setArcPath(new ArcPath(tihac, path)); |
284 | + } |
285 | + |
286 | + Command edit = new AddTimedInhibitorArcCommand( |
287 | + tihac, |
288 | + modelNet, |
289 | + c |
290 | + ); |
291 | + edit.redo(); |
292 | + undoManager.addNewEdit(edit); |
293 | + |
294 | + } else { |
295 | + |
296 | + JOptionPane.showMessageDialog( |
297 | + CreateGui.getApp(), |
298 | + "There was an error drawing the arc. Possible problems:\n" |
299 | + + " - There is already an arc between the selected place and transition\n" |
300 | + + " - You are attempting to draw an arc between a shared transition and a shared place", |
301 | + "Error", JOptionPane.ERROR_MESSAGE |
302 | + ); |
303 | + |
304 | + } |
305 | + |
306 | + } |
307 | + |
308 | + public void addTimedTransportArc(DataLayer c, TimedPlaceComponent p1, TimedTransitionComponent t, TimedPlaceComponent p2, ArcPath path1, ArcPath path2) { |
309 | + Require.notNull(c, "DataLayer can't be null"); |
310 | + Require.notNull(p1, "Place1 can't be null"); |
311 | + Require.notNull(t, "Transitions can't be null"); |
312 | + Require.notNull(p2, "Place2 can't be null"); |
313 | + |
314 | + TimedArcPetriNet modelNet = guiModelToModel.get(c); |
315 | + |
316 | + if ( |
317 | + !modelNet.hasArcFromPlaceToTransition(p1.underlyingPlace(), t.underlyingTransition()) && |
318 | + !modelNet.hasArcFromTransitionToPlace(t.underlyingTransition(), p2.underlyingPlace()) |
319 | + ) { |
320 | + |
321 | + int groupNr = getNextTransportArcMaxGroupNumber(p1, t); |
322 | + |
323 | + TransportArc tta = new TransportArc(p1.underlyingPlace(), t.underlyingTransition(), p2.underlyingPlace()); |
324 | + |
325 | + TimedTransportArcComponent ttac1 = new TimedTransportArcComponent(p1, t, tta, groupNr); |
326 | + TimedTransportArcComponent ttac2 = new TimedTransportArcComponent(t, p2, tta, groupNr); |
327 | + |
328 | + ttac1.setConnectedTo(ttac2); |
329 | + ttac2.setConnectedTo(ttac1); |
330 | + |
331 | + if (path1 != null) { |
332 | + ttac1.setArcPath(new ArcPath(ttac1, path1)); |
333 | + } |
334 | + if (path2 != null) { |
335 | + ttac2.setArcPath(new ArcPath(ttac2, path2)); |
336 | + } |
337 | + |
338 | + //XXX: the Command should take both arcs |
339 | + Command edit = new AddTransportArcCommand( |
340 | + ttac2, |
341 | + tta, |
342 | + modelNet, |
343 | + c |
344 | + ); |
345 | + edit.redo(); |
346 | + undoManager.addNewEdit(edit); |
347 | + |
348 | + } else { |
349 | + JOptionPane.showMessageDialog( |
350 | + CreateGui.getApp(), |
351 | + "There was an error drawing the arc. Possible problems:\n" |
352 | + + " - There is already an arc between the source place and transition\n" |
353 | + + " - There is already an arc between the transtion and the target place\n" |
354 | + + " - You are attempting to draw an arc between a shared transition and a shared place", |
355 | + "Error", JOptionPane.ERROR_MESSAGE |
356 | + ); |
357 | + } |
358 | + |
359 | + } |
360 | + |
361 | + private int getNextTransportArcMaxGroupNumber(TimedPlaceComponent p, TimedTransitionComponent t) { |
362 | + int groupMaxCounter = 0; |
363 | + |
364 | + for (Arc a : t.getPreset()) { |
365 | + if (a instanceof TimedTransportArcComponent && a.getTarget().equals(t)) { |
366 | + if (((TimedTransportArcComponent) a).getGroupNr() > groupMaxCounter) { |
367 | + groupMaxCounter = ((TimedTransportArcComponent) a).getGroupNr(); |
368 | + } |
369 | + } |
370 | + } |
371 | + |
372 | + return groupMaxCounter+1; |
373 | + } |
374 | + |
375 | + |
376 | + public void deleteSelection() { |
377 | + // check if queries need to be removed |
378 | + ArrayList<PetriNetObject> selection = drawingSurface().getSelectionObject().getSelection(); |
379 | + Iterable<TAPNQuery> queries = queries(); |
380 | + HashSet<TAPNQuery> queriesToDelete = new HashSet<TAPNQuery>(); |
381 | + |
382 | + boolean queriesAffected = false; |
383 | + for (PetriNetObject pn : selection) { |
384 | + if (pn instanceof TimedPlaceComponent) { |
385 | + TimedPlaceComponent place = (TimedPlaceComponent)pn; |
386 | + if(!place.underlyingPlace().isShared()){ |
387 | + for (TAPNQuery q : queries) { |
388 | + if (q.getProperty().containsAtomicPropositionWithSpecificPlaceInTemplate(((LocalTimedPlace)place.underlyingPlace()).model().name(),place.underlyingPlace().name())) { |
389 | + queriesAffected = true; |
390 | + queriesToDelete.add(q); |
391 | + } |
392 | + } |
393 | + } |
394 | + } else if (pn instanceof TimedTransitionComponent){ |
395 | + TimedTransitionComponent transition = (TimedTransitionComponent)pn; |
396 | + if(!transition.underlyingTransition().isShared()){ |
397 | + for (TAPNQuery q : queries) { |
398 | + if (q.getProperty().containsAtomicPropositionWithSpecificTransitionInTemplate((transition.underlyingTransition()).model().name(),transition.underlyingTransition().name())) { |
399 | + queriesAffected = true; |
400 | + queriesToDelete.add(q); |
401 | + } |
402 | + } |
403 | + } |
404 | + } |
405 | + } |
406 | + StringBuilder s = new StringBuilder(); |
407 | + s.append("The following queries are associated with the currently selected objects:\n\n"); |
408 | + for (TAPNQuery q : queriesToDelete) { |
409 | + s.append(q.getName()); |
410 | + s.append('\n'); |
411 | + } |
412 | + s.append("\nAre you sure you want to remove the current selection and all associated queries?"); |
413 | + |
414 | + int choice = queriesAffected ? JOptionPane.showConfirmDialog( |
415 | + CreateGui.getApp(), s.toString(), "Warning", |
416 | + JOptionPane.YES_NO_OPTION, JOptionPane.QUESTION_MESSAGE) |
417 | + : JOptionPane.YES_OPTION; |
418 | + |
419 | + if (choice == JOptionPane.YES_OPTION) { |
420 | + getUndoManager().newEdit(); // new "transaction"" |
421 | + if (queriesAffected) { |
422 | + TabContent currentTab = TabContent.this; |
423 | + for (TAPNQuery q : queriesToDelete) { |
424 | + Command cmd = new DeleteQueriesCommand(currentTab, Arrays.asList(q)); |
425 | + cmd.redo(); |
426 | + getUndoManager().addEdit(cmd); |
427 | + } |
428 | + } |
429 | + |
430 | + deleteSelection(selection); |
431 | + network().buildConstraints(); |
432 | + } |
433 | + } |
434 | + |
435 | + //XXX: function moved from undoManager --kyrke - 2019-07-06 |
436 | + private void deleteObject(PetriNetObject pnObject) { |
437 | + if (pnObject instanceof ArcPathPoint) { |
438 | + |
439 | + ArcPathPoint arcPathPoint = (ArcPathPoint)pnObject; |
440 | + |
441 | + //If the arc is marked for deletion, skip deleting individual arcpathpoint |
442 | + if (!(arcPathPoint.getArcPath().getArc().isSelected())) { |
443 | + |
444 | + //Don't delete the two last arc path points |
445 | + if (arcPathPoint.isDeleteable()) { |
446 | + Command cmd = new DeleteArcPathPointEdit( |
447 | + arcPathPoint.getArcPath().getArc(), |
448 | + arcPathPoint, |
449 | + arcPathPoint.getIndex(), |
450 | + getModel() |
451 | + ); |
452 | + cmd.redo(); |
453 | + getUndoManager().addEdit(cmd); |
454 | + } |
455 | + } |
456 | + }else{ |
457 | + //The list of selected objects is not updated when a element is deleted |
458 | + //We might delete the same object twice, which will give an error |
459 | + //Eg. a place with output arc is deleted (deleted also arc) while arc is also selected. |
460 | + //There is properly a better way to track this (check model?) but while refactoring we will keeps it close |
461 | + //to the orginal code -- kyrke 2019-06-27 |
462 | + if (!pnObject.isDeleted()) { |
463 | + Command cmd = null; |
464 | + if(pnObject instanceof TimedPlaceComponent){ |
465 | + TimedPlaceComponent tp = (TimedPlaceComponent)pnObject; |
466 | + cmd = new DeleteTimedPlaceCommand(tp, guiModelToModel.get(getModel()), getModel()); |
467 | + }else if(pnObject instanceof TimedTransitionComponent){ |
468 | + TimedTransitionComponent transition = (TimedTransitionComponent)pnObject; |
469 | + cmd = new DeleteTimedTransitionCommand(transition, transition.underlyingTransition().model(), getModel()); |
470 | + }else if(pnObject instanceof TimedTransportArcComponent){ |
471 | + TimedTransportArcComponent transportArc = (TimedTransportArcComponent)pnObject; |
472 | + cmd = new DeleteTransportArcCommand(transportArc, transportArc.underlyingTransportArc(), transportArc.underlyingTransportArc().model(), getModel()); |
473 | + }else if(pnObject instanceof TimedInhibitorArcComponent){ |
474 | + TimedInhibitorArcComponent tia = (TimedInhibitorArcComponent)pnObject; |
475 | + cmd = new DeleteTimedInhibitorArcCommand(tia, tia.underlyingTimedInhibitorArc().model(), getModel()); |
476 | + }else if(pnObject instanceof TimedInputArcComponent){ |
477 | + TimedInputArcComponent tia = (TimedInputArcComponent)pnObject; |
478 | + cmd = new DeleteTimedInputArcCommand(tia, tia.underlyingTimedInputArc().model(), getModel()); |
479 | + }else if(pnObject instanceof TimedOutputArcComponent){ |
480 | + TimedOutputArcComponent toa = (TimedOutputArcComponent)pnObject; |
481 | + cmd = new DeleteTimedOutputArcCommand(toa, toa.underlyingArc().model(), getModel()); |
482 | + }else if(pnObject instanceof AnnotationNote){ |
483 | + cmd = new DeleteAnnotationNoteCommand((AnnotationNote)pnObject, getModel()); |
484 | + }else{ |
485 | + throw new RuntimeException("This should not be possible"); |
486 | + } |
487 | + cmd.redo(); |
488 | + getUndoManager().addEdit(cmd); |
489 | + } |
490 | + } |
491 | + } |
492 | + |
493 | + |
494 | + private void deleteSelection(PetriNetObject pnObject) { |
495 | + if(pnObject instanceof PlaceTransitionObject){ |
496 | + PlaceTransitionObject pto = (PlaceTransitionObject)pnObject; |
497 | + |
498 | + ArrayList<Arc> arcsToDelete = new ArrayList<>(); |
499 | + |
500 | + //Notice since we delte elements from the collection we can't do this while iterating, we need to |
501 | + // capture the arcs and delete them later. |
502 | + for(Arc arc : pto.getPreset()){ |
503 | + arcsToDelete.add(arc); |
504 | + } |
505 | + |
506 | + for(Arc arc : pto.getPostset()){ |
507 | + arcsToDelete.add(arc); |
508 | + } |
509 | + |
510 | + arcsToDelete.forEach(this::deleteObject); |
511 | + } |
512 | + |
513 | + deleteObject(pnObject); |
514 | + } |
515 | + |
516 | + public void deleteSelection(ArrayList<PetriNetObject> selection) { |
517 | + for (PetriNetObject pnObject : selection) { |
518 | + deleteSelection(pnObject); |
519 | + } |
520 | + } |
521 | + |
522 | + |
523 | + } |
524 | + |
525 | |
526 | /** |
527 | * Creates a new tab with the selected file, or a new file if filename==null |
528 | */ |
529 | public static TabContent createNewTabFromInputStream(InputStream file, String name) throws Exception { |
530 | - TabContent tab = new TabContent(); |
531 | - tab.setInitialName(name); |
532 | |
533 | - try { |
534 | + try { |
535 | ModelLoader loader = new ModelLoader(); |
536 | LoadedModel loadedModel = loader.load(file); |
537 | |
538 | - tab.setNetwork(loadedModel.network(), loadedModel.templates()); |
539 | - tab.setQueries(loadedModel.queries()); |
540 | - tab.setConstants(loadedModel.network().constants()); |
541 | + TabContent tab = new TabContent(loadedModel.network(), loadedModel.templates(), loadedModel.queries()); |
542 | + tab.setInitialName(name); |
543 | |
544 | tab.selectFirstElements(); |
545 | |
546 | tab.setFile(null); |
547 | + return tab; |
548 | } catch (Exception e) { |
549 | throw new Exception("TAPAAL encountered an error while loading the file: " + name + "\n\nPossible explanations:\n - " + e.toString()); |
550 | } |
551 | |
552 | - return tab; |
553 | } |
554 | |
555 | public static TabContent createNewEmptyTab(String name){ |
556 | @@ -89,7 +496,7 @@ |
557 | //Set Default Template |
558 | String templateName = tab.drawingSurface().getNameGenerator().getNewTemplateName(); |
559 | Template template = new Template(new TimedArcPetriNet(templateName), new DataLayer(), new Zoomer()); |
560 | - tab.addTemplate(template, false); |
561 | + tab.addTemplate(template); |
562 | |
563 | return tab; |
564 | } |
565 | @@ -99,14 +506,6 @@ |
566 | */ |
567 | |
568 | public static TabContent createNewTabFromPNMLFile(File file) throws Exception { |
569 | - TabContent tab = new TabContent(); |
570 | - |
571 | - String name = null; |
572 | - |
573 | - if (file != null) { |
574 | - name = file.getName().replaceAll(".pnml", ".tapn"); |
575 | - } |
576 | - tab.setInitialName(name); |
577 | |
578 | if (file != null) { |
579 | try { |
580 | @@ -116,24 +515,28 @@ |
581 | PNMLoader loader = new PNMLoader(); |
582 | loadedModel = loader.load(file); |
583 | |
584 | - |
585 | - tab.setNetwork(loadedModel.network(), loadedModel.templates()); |
586 | - tab.setQueries(loadedModel.queries()); |
587 | - tab.setConstants(loadedModel.network().constants()); |
588 | + TabContent tab = new TabContent(loadedModel.network(), loadedModel.templates(), loadedModel.queries()); |
589 | + |
590 | + String name = null; |
591 | + |
592 | + if (file != null) { |
593 | + name = file.getName().replaceAll(".pnml", ".tapn"); |
594 | + } |
595 | + tab.setInitialName(name); |
596 | |
597 | tab.selectFirstElements(); |
598 | |
599 | tab.setMode(Pipe.ElementType.SELECT); |
600 | |
601 | + //appView.updatePreferredSize(); //XXX 2018-05-23 kyrke seems not to be needed |
602 | + name = name.replace(".pnml",".tapn"); // rename .pnml input file to .tapn |
603 | + return tab; |
604 | |
605 | } catch (Exception e) { |
606 | throw new Exception("TAPAAL encountered an error while loading the file: " + file.getName() + "\n\nPossible explanations:\n - " + e.toString()); |
607 | } |
608 | } |
609 | - |
610 | - //appView.updatePreferredSize(); //XXX 2018-05-23 kyrke seems not to be needed |
611 | - name = name.replace(".pnml",".tapn"); // rename .pnml input file to .tapn |
612 | - return tab; |
613 | + return null; |
614 | } |
615 | |
616 | /** |
617 | @@ -227,49 +630,72 @@ |
618 | |
619 | private WorkflowDialog workflowDialog = null; |
620 | |
621 | - public TabContent() { |
622 | - for (TimedArcPetriNet net : tapnNetwork.allTemplates()) { |
623 | - guiModels.put(net, new DataLayer()); |
624 | - zoomLevels.put(net, new Zoomer()); |
625 | - hasPositionalInfos.put(net, Boolean.FALSE); |
626 | - } |
627 | - |
628 | - drawingSurface = new DrawingSurfaceImpl(new DataLayer(), this, managerRef); |
629 | - drawingSurfaceScroller = new JScrollPane(drawingSurface); |
630 | - // make it less bad on XP |
631 | - drawingSurfaceScroller.setBorder(new BevelBorder(BevelBorder.LOWERED)); |
632 | - drawingSurfaceScroller.setWheelScrollingEnabled(true); |
633 | - drawingSurfaceScroller.getVerticalScrollBar().setUnitIncrement(10); |
634 | - drawingSurfaceScroller.getHorizontalScrollBar().setUnitIncrement(10); |
635 | - |
636 | - // Make clicking the drawing area move focus to GuiFrame |
637 | - drawingSurface.addMouseListener(new MouseAdapter() { |
638 | - @Override |
639 | - public void mouseClicked(MouseEvent e) { |
640 | - CreateGui.getApp().requestFocus(); |
641 | - } |
642 | - }); |
643 | - |
644 | - drawingSurfaceDummy = new JPanel(new GridBagLayout()); |
645 | - GridBagConstraints gc=new GridBagConstraints(); |
646 | - gc.fill=GridBagConstraints.HORIZONTAL; |
647 | - gc.gridx=0; |
648 | - gc.gridy=0; |
649 | - drawingSurfaceDummy.add(new JLabel("The net is too big to be drawn"), gc); |
650 | - |
651 | - createEditorLeftPane(); |
652 | - createAnimatorSplitPane(); |
653 | - |
654 | - this.setOrientation(HORIZONTAL_SPLIT); |
655 | - this.setLeftComponent(editorSplitPaneScroller); |
656 | - this.setRightComponent(drawingSurfaceScroller); |
657 | - |
658 | - this.setContinuousLayout(true); |
659 | - this.setOneTouchExpandable(true); |
660 | - this.setBorder(null); // avoid multiple borders |
661 | - this.setDividerSize(8); |
662 | - //XXX must be after the animationcontroller is created |
663 | - animationModeController = new CanvasAnimationController(getAnimator()); |
664 | + |
665 | + private TabContent() { |
666 | + this(new TimedArcPetriNetNetwork(), new ArrayList<>(), new TAPNLens(true,false)); |
667 | + } |
668 | + |
669 | + private TabContent(TimedArcPetriNetNetwork network, Collection<Template> templates, TAPNLens lens) { |
670 | + |
671 | + Require.that(network != null, "network cannot be null"); |
672 | + Require.notNull(lens, "Lens can't be null"); |
673 | + this.lens = lens; |
674 | + tapnNetwork = network; |
675 | + |
676 | + guiModels.clear(); |
677 | + for (Template template : templates) { |
678 | + addGuiModel(template.model(), template.guiModel()); |
679 | + zoomLevels.put(template.model(), template.zoomer()); |
680 | + hasPositionalInfos.put(template.model(), template.getHasPositionalInfo()); |
681 | + } |
682 | + |
683 | + drawingSurface = new DrawingSurfaceImpl(new DataLayer(), this, managerRef); |
684 | + drawingSurfaceScroller = new JScrollPane(drawingSurface); |
685 | + // make it less bad on XP |
686 | + drawingSurfaceScroller.setBorder(new BevelBorder(BevelBorder.LOWERED)); |
687 | + drawingSurfaceScroller.setWheelScrollingEnabled(true); |
688 | + drawingSurfaceScroller.getVerticalScrollBar().setUnitIncrement(10); |
689 | + drawingSurfaceScroller.getHorizontalScrollBar().setUnitIncrement(10); |
690 | + |
691 | + // Make clicking the drawing area move focus to GuiFrame |
692 | + drawingSurface.addMouseListener(new MouseAdapter() { |
693 | + @Override |
694 | + public void mouseClicked(MouseEvent e) { |
695 | + CreateGui.getApp().requestFocus(); |
696 | + } |
697 | + }); |
698 | + |
699 | + drawingSurfaceDummy = new JPanel(new GridBagLayout()); |
700 | + GridBagConstraints gc=new GridBagConstraints(); |
701 | + gc.fill=GridBagConstraints.HORIZONTAL; |
702 | + gc.gridx=0; |
703 | + gc.gridy=0; |
704 | + drawingSurfaceDummy.add(new JLabel("The net is too big to be drawn"), gc); |
705 | + |
706 | + createEditorLeftPane(); |
707 | + createAnimatorSplitPane(); |
708 | + |
709 | + this.setOrientation(HORIZONTAL_SPLIT); |
710 | + this.setLeftComponent(editorSplitPaneScroller); |
711 | + this.setRightComponent(drawingSurfaceScroller); |
712 | + |
713 | + this.setContinuousLayout(true); |
714 | + this.setOneTouchExpandable(true); |
715 | + this.setBorder(null); // avoid multiple borders |
716 | + this.setDividerSize(8); |
717 | + //XXX must be after the animationcontroller is created |
718 | + animationModeController = new CanvasAnimationController(getAnimator()); |
719 | + } |
720 | + |
721 | + private TabContent(TimedArcPetriNetNetwork network, Collection<Template> templates, Iterable<TAPNQuery> tapnqueries) { |
722 | + this(network, templates, tapnqueries, new TAPNLens(true, false)); |
723 | + } |
724 | + private TabContent(TimedArcPetriNetNetwork network, Collection<Template> templates, Iterable<TAPNQuery> tapnqueries, TAPNLens lens) { |
725 | + this(network, templates, lens); |
726 | + |
727 | + setNetwork(network, templates); |
728 | + setQueries(tapnqueries); |
729 | + setConstants(network().constants()); |
730 | } |
731 | |
732 | public SharedPlacesAndTransitionsPanel getSharedPlacesAndTransitionsPanel(){ |
733 | @@ -706,34 +1132,24 @@ |
734 | return count; |
735 | } |
736 | |
737 | - /* |
738 | - XXX: 2018-05-07 kyrke, added a version of addTemplate that does not call templatExplorer.updatTemplateList |
739 | - used in createNewTab (as updateTamplateList expects the current tab to be selected) |
740 | - this needs to be refactored asap. but the is the only way I could get it to work for now. |
741 | - The code is very unclean on what is a template, TimeArcPetriNetNetwork, seems to mix concerns about |
742 | - gui/controller/model. Further refactoring is needed to clean up this mess. |
743 | - */ |
744 | - public void addTemplate(Template template, boolean updateTemplateExplorer) { |
745 | + public void addTemplate(Template template) { |
746 | tapnNetwork.add(template.model()); |
747 | guiModels.put(template.model(), template.guiModel()); |
748 | + guiModelToModel.put(template.guiModel(), template.model()); |
749 | zoomLevels.put(template.model(), template.zoomer()); |
750 | hasPositionalInfos.put(template.model(), template.getHasPositionalInfo()); |
751 | - if (updateTemplateExplorer) { |
752 | - templateExplorer.updateTemplateList(); |
753 | - } |
754 | - } |
755 | - |
756 | - public void addTemplate(Template template) { |
757 | - addTemplate(template, true); |
758 | + templateExplorer.updateTemplateList(); |
759 | } |
760 | |
761 | public void addGuiModel(TimedArcPetriNet net, DataLayer guiModel) { |
762 | guiModels.put(net, guiModel); |
763 | + guiModelToModel.put(guiModel, net); |
764 | } |
765 | |
766 | public void removeTemplate(Template template) { |
767 | tapnNetwork.remove(template.model()); |
768 | guiModels.remove(template.model()); |
769 | + guiModelToModel.remove(template.guiModel()); |
770 | zoomLevels.remove(template.model()); |
771 | hasPositionalInfos.remove(template.model()); |
772 | templateExplorer.updateTemplateList(); |
773 | @@ -747,7 +1163,7 @@ |
774 | return queries.getQueries(); |
775 | } |
776 | |
777 | - public void setQueries(Iterable<TAPNQuery> queries) { |
778 | + private void setQueries(Iterable<TAPNQuery> queries) { |
779 | this.queries.setQueries(queries); |
780 | } |
781 | |
782 | @@ -759,20 +1175,12 @@ |
783 | queries.addQuery(query); |
784 | } |
785 | |
786 | - public void setConstants(Iterable<Constant> constants) { |
787 | + private void setConstants(Iterable<Constant> constants) { |
788 | tapnNetwork.setConstants(constants); |
789 | } |
790 | |
791 | - public void setNetwork(TimedArcPetriNetNetwork network, Collection<Template> templates) { |
792 | - Require.that(network != null, "network cannot be null"); |
793 | - tapnNetwork = network; |
794 | + private void setNetwork(TimedArcPetriNetNetwork network, Collection<Template> templates) { |
795 | |
796 | - guiModels.clear(); |
797 | - for (Template template : templates) { |
798 | - addGuiModel(template.model(), template.guiModel()); |
799 | - zoomLevels.put(template.model(), template.zoomer()); |
800 | - hasPositionalInfos.put(template.model(), template.getHasPositionalInfo()); |
801 | - } |
802 | |
803 | sharedPTPanel.setNetwork(network); |
804 | templateExplorer.updateTemplateList(); |
805 | @@ -1060,6 +1468,8 @@ |
806 | animator.updateAnimationButtonsEnabled(); //Update stepBack/Forward |
807 | } |
808 | |
809 | + private Pipe.ElementType editorMode = Pipe.ElementType.SELECT; |
810 | + |
811 | //XXX temp while refactoring, kyrke - 2019-07-25 |
812 | @Override |
813 | public void setMode(Pipe.ElementType mode) { |
814 | @@ -1068,11 +1478,67 @@ |
815 | |
816 | //Disable selection and deselect current selection |
817 | drawingSurface().getSelectionObject().clearSelection(); |
818 | - |
819 | - //If pending arc draw, remove it |
820 | - if (drawingSurface().createArc != null) { |
821 | - PlaceTransitionObjectHandler.cleanupArc(drawingSurface().createArc, drawingSurface()); |
822 | - } |
823 | + editorMode = mode; |
824 | + switch (mode) { |
825 | + case ADDTOKEN: |
826 | + setManager(new AbstractDrawingSurfaceManager() { |
827 | + @Override |
828 | + public void registerEvents() { |
829 | + registerEvent( |
830 | + e -> e.pno instanceof TimedPlaceComponent && e.a == MouseAction.pressed, |
831 | + e -> placeClicked((TimedPlaceComponent) e.pno) |
832 | + ); |
833 | + } |
834 | + |
835 | + public void placeClicked(TimedPlaceComponent pno) { |
836 | + Command command = new TimedPlaceMarkingEdit(pno, 1); |
837 | + command.redo(); |
838 | + undoManager.addNewEdit(command); |
839 | + } |
840 | + }); |
841 | + break; |
842 | + case DELTOKEN: |
843 | + setManager(new AbstractDrawingSurfaceManager() { |
844 | + @Override |
845 | + public void registerEvents() { |
846 | + registerEvent( |
847 | + e -> e.pno instanceof TimedPlaceComponent && e.a == MouseAction.pressed, |
848 | + e -> placeClicked((TimedPlaceComponent) e.pno) |
849 | + ); |
850 | + } |
851 | + |
852 | + public void placeClicked(TimedPlaceComponent pno) { |
853 | + Command command = new TimedPlaceMarkingEdit(pno, -1); |
854 | + command.redo(); |
855 | + undoManager.addNewEdit(command); |
856 | + } |
857 | + }); |
858 | + break; |
859 | + case TAPNPLACE: |
860 | + setManager(new CanvasPlaceDrawController()); |
861 | + break; |
862 | + case TAPNTRANS: |
863 | + setManager(new CanvasTransitionDrawController()); |
864 | + break; |
865 | + case ANNOTATION: |
866 | + setManager(new CanvasAnnotationNoteDrawController()); |
867 | + break; |
868 | + case TAPNARC: |
869 | + setManager(new CanvasArcDrawController()); |
870 | + break; |
871 | + case TAPNINHIBITOR_ARC: |
872 | + setManager(new CanvasInhibitorarcDrawController()); |
873 | + break; |
874 | + case TRANSPORTARC: |
875 | + setManager(new CanvasTransportarcDrawController()); |
876 | + break; |
877 | + case SELECT: |
878 | + setManager(new CanvasGeneralDrawController()); |
879 | + break; |
880 | + default: |
881 | + setManager(notingManager); |
882 | + break; |
883 | + } |
884 | |
885 | if (mode == Pipe.ElementType.SELECT) { |
886 | drawingSurface().setCursor(Cursor.getPredefinedCursor(Cursor.DEFAULT_CURSOR)); |
887 | @@ -1221,63 +1687,7 @@ |
888 | |
889 | @Override |
890 | public void deleteSelection() { |
891 | - // check if queries need to be removed |
892 | - ArrayList<PetriNetObject> selection = drawingSurface().getSelectionObject().getSelection(); |
893 | - Iterable<TAPNQuery> queries = queries(); |
894 | - HashSet<TAPNQuery> queriesToDelete = new HashSet<TAPNQuery>(); |
895 | - |
896 | - boolean queriesAffected = false; |
897 | - for (PetriNetObject pn : selection) { |
898 | - if (pn instanceof TimedPlaceComponent) { |
899 | - TimedPlaceComponent place = (TimedPlaceComponent)pn; |
900 | - if(!place.underlyingPlace().isShared()){ |
901 | - for (TAPNQuery q : queries) { |
902 | - if (q.getProperty().containsAtomicPropositionWithSpecificPlaceInTemplate(((LocalTimedPlace)place.underlyingPlace()).model().name(),place.underlyingPlace().name())) { |
903 | - queriesAffected = true; |
904 | - queriesToDelete.add(q); |
905 | - } |
906 | - } |
907 | - } |
908 | - } else if (pn instanceof TimedTransitionComponent){ |
909 | - TimedTransitionComponent transition = (TimedTransitionComponent)pn; |
910 | - if(!transition.underlyingTransition().isShared()){ |
911 | - for (TAPNQuery q : queries) { |
912 | - if (q.getProperty().containsAtomicPropositionWithSpecificTransitionInTemplate((transition.underlyingTransition()).model().name(),transition.underlyingTransition().name())) { |
913 | - queriesAffected = true; |
914 | - queriesToDelete.add(q); |
915 | - } |
916 | - } |
917 | - } |
918 | - } |
919 | - } |
920 | - StringBuilder s = new StringBuilder(); |
921 | - s.append("The following queries are associated with the currently selected objects:\n\n"); |
922 | - for (TAPNQuery q : queriesToDelete) { |
923 | - s.append(q.getName()); |
924 | - s.append('\n'); |
925 | - } |
926 | - s.append("\nAre you sure you want to remove the current selection and all associated queries?"); |
927 | - |
928 | - int choice = queriesAffected ? JOptionPane.showConfirmDialog( |
929 | - CreateGui.getApp(), s.toString(), "Warning", |
930 | - JOptionPane.YES_NO_OPTION, JOptionPane.QUESTION_MESSAGE) |
931 | - : JOptionPane.YES_OPTION; |
932 | - |
933 | - if (choice == JOptionPane.YES_OPTION) { |
934 | - getUndoManager().newEdit(); // new "transaction"" |
935 | - if (queriesAffected) { |
936 | - TabContent currentTab = this; |
937 | - for (TAPNQuery q : queriesToDelete) { |
938 | - Command cmd = new DeleteQueriesCommand(currentTab, Arrays.asList(q)); |
939 | - cmd.redo(); |
940 | - getUndoManager().addEdit(cmd); |
941 | - } |
942 | - } |
943 | - |
944 | - drawingSurface().deleteSelection(drawingSurface().getSelectionObject().getSelection()); |
945 | - //getCurrentTab().drawingSurface().repaint(); |
946 | - network().buildConstraints(); |
947 | - } |
948 | + guiModelManager.deleteSelection(); |
949 | |
950 | |
951 | } |
952 | @@ -1309,13 +1719,13 @@ |
953 | |
954 | //If arc is being drawn delete it |
955 | |
956 | - if (drawingSurface().createArc == null) { |
957 | + if (editorMode == Pipe.ElementType.SELECT) { |
958 | getUndoManager().undo(); |
959 | network().buildConstraints(); |
960 | |
961 | } else { |
962 | |
963 | - PlaceTransitionObjectHandler.cleanupArc(drawingSurface().createArc, drawingSurface()); |
964 | + setMode(Pipe.ElementType.SELECT); |
965 | |
966 | } |
967 | } |
968 | @@ -1330,13 +1740,13 @@ |
969 | |
970 | //If arc is being drawn delete it |
971 | |
972 | - if (drawingSurface().createArc == null) { |
973 | + if (editorMode == Pipe.ElementType.SELECT) { |
974 | getUndoManager().redo(); |
975 | network().buildConstraints(); |
976 | |
977 | } else { |
978 | |
979 | - PlaceTransitionObjectHandler.cleanupArc(drawingSurface().createArc, drawingSurface()); |
980 | + setMode(Pipe.ElementType.SELECT); |
981 | |
982 | } |
983 | } |
984 | @@ -1462,6 +1872,321 @@ |
985 | return null; |
986 | } |
987 | |
988 | + class CanvasPlaceDrawController extends AbstractDrawingSurfaceManager { |
989 | + |
990 | + @Override |
991 | + public void drawingSurfaceMousePressed(MouseEvent e) { |
992 | + Point p = canvas.adjustPointToGridAndZoom(e.getPoint(), canvas.getZoom()); |
993 | + |
994 | + guiModelManager.addNewTimedPlace(canvas.getGuiModel(), p); |
995 | + } |
996 | + |
997 | + @Override |
998 | + public void registerEvents() { |
999 | + |
1000 | + } |
1001 | + } |
1002 | + |
1003 | + class CanvasTransitionDrawController extends AbstractDrawingSurfaceManager { |
1004 | + |
1005 | + @Override |
1006 | + public void drawingSurfaceMousePressed(MouseEvent e) { |
1007 | + Point p = canvas.adjustPointToGridAndZoom(e.getPoint(), canvas.getZoom()); |
1008 | + |
1009 | + guiModelManager.addNewTimedTransitions(drawingSurface.getGuiModel(), p); |
1010 | + } |
1011 | + |
1012 | + @Override |
1013 | + public void registerEvents() { |
1014 | + |
1015 | + } |
1016 | + } |
1017 | + |
1018 | + class CanvasAnnotationNoteDrawController extends AbstractDrawingSurfaceManager { |
1019 | + |
1020 | + @Override |
1021 | + public void drawingSurfaceMousePressed(MouseEvent e) { |
1022 | + Point p = canvas.adjustPointToGridAndZoom(e.getPoint(), canvas.getZoom()); |
1023 | + |
1024 | + guiModelManager.addAnnotationNote(drawingSurface.getGuiModel(), p); |
1025 | + } |
1026 | + |
1027 | + @Override |
1028 | + public void registerEvents() { |
1029 | + |
1030 | + } |
1031 | + } |
1032 | + |
1033 | + class CanvasInhibitorarcDrawController extends AbstractDrawingSurfaceManager { |
1034 | + |
1035 | + private TimedTransitionComponent transition; |
1036 | + private TimedPlaceComponent place; |
1037 | + private Arc arc; |
1038 | + |
1039 | + @Override |
1040 | + public void registerEvents() { |
1041 | + registerEvent( |
1042 | + e->e.pno instanceof TimedPlaceComponent && e.a == MouseAction.pressed, |
1043 | + e->placeClicked(((TimedPlaceComponent) e.pno)) |
1044 | + ); |
1045 | + registerEvent( |
1046 | + e->e.pno instanceof TimedTransitionComponent && e.a == MouseAction.pressed, |
1047 | + e->transitionClicked(((TimedTransitionComponent) e.pno)) |
1048 | + ); |
1049 | + registerEvent( |
1050 | + e->e.pno instanceof PlaceTransitionObject && e.a == MouseAction.entered, |
1051 | + e->placetranstionMouseOver(((PlaceTransitionObject) e.pno)) |
1052 | + ); |
1053 | + registerEvent( |
1054 | + e->e.pno instanceof PlaceTransitionObject && e.a == MouseAction.exited, |
1055 | + e->placetranstionMouseExited(((PlaceTransitionObject) e.pno)) |
1056 | + ); |
1057 | + registerEvent( |
1058 | + e->e.pno instanceof PlaceTransitionObject && e.a == MouseAction.moved, |
1059 | + e->placetransitionMouseMoved(((PlaceTransitionObject) e.pno), e.e) |
1060 | + ); |
1061 | + } |
1062 | + |
1063 | + private void placetransitionMouseMoved(PlaceTransitionObject pno, MouseEvent e) { |
1064 | + if (arc != null) { |
1065 | + if (arc.getSource() == pno || !arc.getSource().areNotSameType(pno)) { |
1066 | + //Dispatch event to parent (drawing surface) |
1067 | + e.translatePoint(pno.getX(),pno.getY()); |
1068 | + pno.getParent().dispatchEvent(e); |
1069 | + } |
1070 | + } |
1071 | + } |
1072 | + |
1073 | + private void placetranstionMouseExited(PlaceTransitionObject pto) { |
1074 | + if (arc != null) { |
1075 | + arc.setTarget(null); |
1076 | + //XXX this is bad, we have to clean up internal state manually, should be refactored //kyrke - 2019-11-14 |
1077 | + // Relates to bug #1849786 |
1078 | + if (pto instanceof Transition) { |
1079 | + ((Transition)pto).removeArcCompareObject(arc); |
1080 | + } |
1081 | + arc.updateArcPosition(); |
1082 | + } |
1083 | + } |
1084 | + |
1085 | + private void placetranstionMouseOver(PlaceTransitionObject pno) { |
1086 | + if (arc != null) { |
1087 | + if (arc.getSource() != pno && arc.getSource().areNotSameType(pno)) { |
1088 | + arc.setTarget(pno); |
1089 | + arc.updateArcPosition(); |
1090 | + } |
1091 | + } |
1092 | + } |
1093 | + |
1094 | + private void transitionClicked(TimedTransitionComponent pno) { |
1095 | + if (place != null && transition == null) { |
1096 | + transition = pno; |
1097 | + CreateGui.getDrawingSurface().clearAllPrototype(); |
1098 | + guiModelManager.addInhibitorArc(getModel(), place, transition, arc.getArcPath()); |
1099 | + clearPendingArc(); |
1100 | + } |
1101 | + } |
1102 | + |
1103 | + private void placeClicked(TimedPlaceComponent pno) { |
1104 | + if (place == null && transition == null) { |
1105 | + place = pno; |
1106 | + arc = new TimedInhibitorArcComponent(pno); |
1107 | + //XXX calling zoomUpdate will set the endpoint to 0,0, drawing the arc from source to 0,0 |
1108 | + //to avoid this we change the endpoint to set the end point to the same as the end point |
1109 | + //needs further refactorings //kyrke 2019-09-05 |
1110 | + arc.setEndPoint(pno.getPositionX(), pno.getPositionY(), false); |
1111 | + CreateGui.getDrawingSurface().addPrototype(arc); |
1112 | + arc.requestFocusInWindow(); |
1113 | + arc.setSelectable(false); |
1114 | + arc.enableDrawingKeyBindings(this::clearPendingArc); |
1115 | + } else if (transition != null && place == null) { |
1116 | + place = pno; |
1117 | + CreateGui.getDrawingSurface().clearAllPrototype(); |
1118 | + guiModelManager.addTimedOutputArc(getModel(), transition, place, arc.getArcPath()); |
1119 | + clearPendingArc(); |
1120 | + } |
1121 | + } |
1122 | + |
1123 | + private void clearPendingArc() { |
1124 | + CreateGui.getDrawingSurface().clearAllPrototype(); |
1125 | + place = null; |
1126 | + transition = null; |
1127 | + arc = null; |
1128 | + } |
1129 | + |
1130 | + @Override |
1131 | + public void drawingSurfaceMouseMoved(MouseEvent e) { |
1132 | + if(arc!=null) { |
1133 | + arc.setEndPoint(e.getX(), e.getY(), e.isShiftDown()); |
1134 | + } |
1135 | + } |
1136 | + |
1137 | + @Override |
1138 | + public void drawingSurfaceMousePressed(MouseEvent e) { |
1139 | + if (arc!=null) {; |
1140 | + Point p = e.getPoint(); |
1141 | + int x = Zoomer.getUnzoomedValue(p.x, CreateGui.getDrawingSurface().getZoom()); |
1142 | + int y = Zoomer.getUnzoomedValue(p.y, CreateGui.getDrawingSurface().getZoom()); |
1143 | + |
1144 | + boolean shiftDown = e.isShiftDown(); |
1145 | + //XXX: x,y is ignored is overwritten when mouse is moved, this just add a new point to the end of list |
1146 | + arc.getArcPath().addPoint(arc.getArcPath().getEndIndex(), x,y, shiftDown); |
1147 | + } |
1148 | + } |
1149 | + |
1150 | + @Override |
1151 | + public void registerManager(DrawingSurfaceImpl canvas) { |
1152 | + CreateGui.useExtendedBounds = true; |
1153 | + } |
1154 | + |
1155 | + @Override |
1156 | + public void deregisterManager() { |
1157 | + clearPendingArc(); |
1158 | + CreateGui.useExtendedBounds = false; |
1159 | + } |
1160 | + |
1161 | + |
1162 | + } |
1163 | + class CanvasArcDrawController extends AbstractDrawingSurfaceManager { |
1164 | + private TimedTransitionComponent transition; |
1165 | + private TimedPlaceComponent place; |
1166 | + private Arc arc; |
1167 | + |
1168 | + @Override |
1169 | + public void registerEvents() { |
1170 | + registerEvent( |
1171 | + e->e.pno instanceof TimedPlaceComponent && e.a == MouseAction.pressed, |
1172 | + e->placeClicked(((TimedPlaceComponent) e.pno)) |
1173 | + ); |
1174 | + registerEvent( |
1175 | + e->e.pno instanceof TimedTransitionComponent && e.a == MouseAction.pressed, |
1176 | + e->transitionClicked(((TimedTransitionComponent) e.pno)) |
1177 | + ); |
1178 | + registerEvent( |
1179 | + e->e.pno instanceof PlaceTransitionObject && e.a == MouseAction.entered, |
1180 | + e->placetranstionMouseOver(((PlaceTransitionObject) e.pno)) |
1181 | + ); |
1182 | + registerEvent( |
1183 | + e->e.pno instanceof PlaceTransitionObject && e.a == MouseAction.exited, |
1184 | + e->placetranstionMouseExited(((PlaceTransitionObject) e.pno)) |
1185 | + ); |
1186 | + registerEvent( |
1187 | + e->e.pno instanceof PlaceTransitionObject && e.a == MouseAction.moved, |
1188 | + e->placetransitionMouseMoved(((PlaceTransitionObject) e.pno), e.e) |
1189 | + ); |
1190 | + } |
1191 | + |
1192 | + private void placetransitionMouseMoved(PlaceTransitionObject pno, MouseEvent e) { |
1193 | + if (arc != null) { |
1194 | + if (arc.getSource() == pno || !arc.getSource().areNotSameType(pno)) { |
1195 | + //Dispatch event to parent (drawing surface) |
1196 | + e.translatePoint(pno.getX(),pno.getY()); |
1197 | + pno.getParent().dispatchEvent(e); |
1198 | + } |
1199 | + } |
1200 | + } |
1201 | + |
1202 | + private void placetranstionMouseExited(PlaceTransitionObject pto) { |
1203 | + if (arc != null) { |
1204 | + arc.setTarget(null); |
1205 | + //XXX this is bad, we have to clean up internal state manually, should be refactored //kyrke - 2019-11-14 |
1206 | + // Relates to bug #1849786 |
1207 | + if (pto instanceof Transition) { |
1208 | + ((Transition)pto).removeArcCompareObject(arc); |
1209 | + } |
1210 | + arc.updateArcPosition(); |
1211 | + } |
1212 | + } |
1213 | + |
1214 | + private void placetranstionMouseOver(PlaceTransitionObject pno) { |
1215 | + if (arc != null) { |
1216 | + if (arc.getSource() != pno && arc.getSource().areNotSameType(pno)) { |
1217 | + arc.setTarget(pno); |
1218 | + arc.updateArcPosition(); |
1219 | + } |
1220 | + } |
1221 | + } |
1222 | + |
1223 | + private void transitionClicked(TimedTransitionComponent pno) { |
1224 | + if (place == null && transition == null) { |
1225 | + transition = pno; |
1226 | + arc = new TimedOutputArcComponent(pno); |
1227 | + |
1228 | + //XXX calling zoomUpdate will set the endpoint to 0,0, drawing the arc from source to 0,0 |
1229 | + //to avoid this we change the endpoint to set the end point to the same as the end point |
1230 | + //needs further refactorings //kyrke 2019-09-05 |
1231 | + arc.setEndPoint(pno.getPositionX(), pno.getPositionY(), false); |
1232 | + CreateGui.getDrawingSurface().addPrototype(arc); |
1233 | + arc.requestFocusInWindow(); |
1234 | + arc.setSelectable(false); |
1235 | + arc.enableDrawingKeyBindings(this::clearPendingArc); |
1236 | + } else if (place != null && transition == null) { |
1237 | + transition = pno; |
1238 | + CreateGui.getDrawingSurface().clearAllPrototype(); |
1239 | + guiModelManager.addTimedInputArc(getModel(), place, transition, arc.getArcPath()); |
1240 | + clearPendingArc(); |
1241 | + } |
1242 | + } |
1243 | + |
1244 | + private void placeClicked(TimedPlaceComponent pno) { |
1245 | + if (place == null && transition == null) { |
1246 | + place = pno; |
1247 | + arc = new TimedInputArcComponent(pno); |
1248 | + //XXX calling zoomUpdate will set the endpoint to 0,0, drawing the arc from source to 0,0 |
1249 | + //to avoid this we change the endpoint to set the end point to the same as the end point |
1250 | + //needs further refactorings //kyrke 2019-09-05 |
1251 | + arc.setEndPoint(pno.getPositionX(), pno.getPositionY(), false); |
1252 | + CreateGui.getDrawingSurface().addPrototype(arc); |
1253 | + arc.requestFocusInWindow(); |
1254 | + arc.setSelectable(false); |
1255 | + arc.enableDrawingKeyBindings(this::clearPendingArc); |
1256 | + } else if (transition != null && place == null) { |
1257 | + place = pno; |
1258 | + CreateGui.getDrawingSurface().clearAllPrototype(); |
1259 | + guiModelManager.addTimedOutputArc(getModel(), transition, place, arc.getArcPath()); |
1260 | + clearPendingArc(); |
1261 | + } |
1262 | + } |
1263 | + |
1264 | + private void clearPendingArc() { |
1265 | + CreateGui.getDrawingSurface().clearAllPrototype(); |
1266 | + place = null; |
1267 | + transition = null; |
1268 | + arc = null; |
1269 | + } |
1270 | + |
1271 | + @Override |
1272 | + public void drawingSurfaceMouseMoved(MouseEvent e) { |
1273 | + if(arc!=null) { |
1274 | + arc.setEndPoint(e.getX(), e.getY(), e.isShiftDown()); |
1275 | + } |
1276 | + } |
1277 | + |
1278 | + @Override |
1279 | + public void drawingSurfaceMousePressed(MouseEvent e) { |
1280 | + if (arc!=null) {; |
1281 | + Point p = e.getPoint(); |
1282 | + int x = Zoomer.getUnzoomedValue(p.x, CreateGui.getDrawingSurface().getZoom()); |
1283 | + int y = Zoomer.getUnzoomedValue(p.y, CreateGui.getDrawingSurface().getZoom()); |
1284 | + |
1285 | + boolean shiftDown = e.isShiftDown(); |
1286 | + //XXX: x,y is ignored is overwritten when mouse is moved, this just add a new point to the end of list |
1287 | + arc.getArcPath().addPoint(arc.getArcPath().getEndIndex(), x,y, shiftDown); |
1288 | + } |
1289 | + } |
1290 | + |
1291 | + @Override |
1292 | + public void registerManager(DrawingSurfaceImpl canvas) { |
1293 | + CreateGui.useExtendedBounds = true; |
1294 | + } |
1295 | + |
1296 | + @Override |
1297 | + public void deregisterManager() { |
1298 | + clearPendingArc(); |
1299 | + CreateGui.useExtendedBounds = false; |
1300 | + } |
1301 | + } |
1302 | + |
1303 | static class CanvasAnimationController extends AbstractDrawingSurfaceManager { |
1304 | |
1305 | private final Animator animator; |
1306 | @@ -1473,7 +2198,7 @@ |
1307 | @Override |
1308 | public void registerEvents() { |
1309 | registerEvent( |
1310 | - e -> e.a == MouseAction.clicked && e.pno instanceof TimedTransitionComponent && SwingUtilities.isLeftMouseButton(e.e), |
1311 | + e -> e.a == MouseAction.pressed && e.pno instanceof TimedTransitionComponent && SwingUtilities.isLeftMouseButton(e.e), |
1312 | e -> transitionLeftClicked((TimedTransitionComponent)e.pno) |
1313 | ); |
1314 | registerEvent( |
1315 | @@ -1516,13 +2241,205 @@ |
1316 | //De-register old manager |
1317 | managerRef.get().deregisterManager(); |
1318 | managerRef.setReference(newManager); |
1319 | - managerRef.get().registerManager(); |
1320 | - } |
1321 | - |
1322 | - //XXX: A quick function made while refactoring to test if the tab is currently |
1323 | - // the tab selected, and is allowed to change gui the gui. Should be controlled an other way |
1324 | - // /kyrke 2019-11-10 |
1325 | - public boolean isTabInFocus(){ |
1326 | - return app.isPresent(); |
1327 | - } |
1328 | + managerRef.get().registerManager(drawingSurface); |
1329 | + } |
1330 | + |
1331 | + private final class CanvasTransportarcDrawController extends AbstractDrawingSurfaceManager { |
1332 | + |
1333 | + private TimedTransitionComponent transition; |
1334 | + private TimedPlaceComponent place1; |
1335 | + private TimedPlaceComponent place2; |
1336 | + private Arc arc; |
1337 | + private Arc arc1; |
1338 | + private Arc arc2; |
1339 | + |
1340 | + |
1341 | + @Override |
1342 | + public void registerEvents() { |
1343 | + registerEvent( |
1344 | + e->e.pno instanceof TimedPlaceComponent && e.a == MouseAction.pressed, |
1345 | + e->placeClicked(((TimedPlaceComponent) e.pno)) |
1346 | + ); |
1347 | + registerEvent( |
1348 | + e->e.pno instanceof TimedTransitionComponent && e.a == MouseAction.pressed, |
1349 | + e->transitionClicked(((TimedTransitionComponent) e.pno)) |
1350 | + ); |
1351 | + registerEvent( |
1352 | + e->e.pno instanceof PlaceTransitionObject && e.a == MouseAction.entered, |
1353 | + e->placetranstionMouseOver(((PlaceTransitionObject) e.pno)) |
1354 | + ); |
1355 | + registerEvent( |
1356 | + e->e.pno instanceof PlaceTransitionObject && e.a == MouseAction.exited, |
1357 | + e->placetranstionMouseExited(((PlaceTransitionObject) e.pno)) |
1358 | + ); |
1359 | + registerEvent( |
1360 | + e->e.pno instanceof PlaceTransitionObject && e.a == MouseAction.moved, |
1361 | + e->placetransitionMouseMoved(((PlaceTransitionObject) e.pno), e.e) |
1362 | + ); |
1363 | + } |
1364 | + |
1365 | + private void placetransitionMouseMoved(PlaceTransitionObject pno, MouseEvent e) { |
1366 | + if (arc != null) { |
1367 | + if (arc.getSource() == pno || !arc.getSource().areNotSameType(pno)) { |
1368 | + //Dispatch event to parent (drawing surface) |
1369 | + e.translatePoint(pno.getX(),pno.getY()); |
1370 | + pno.getParent().dispatchEvent(e); |
1371 | + } |
1372 | + } |
1373 | + } |
1374 | + |
1375 | + private void placetranstionMouseExited(PlaceTransitionObject pto) { |
1376 | + if (arc != null) { |
1377 | + arc.setTarget(null); |
1378 | + //XXX this is bad, we have to clean up internal state manually, should be refactored //kyrke - 2019-11-14 |
1379 | + // Relates to bug #1849786 |
1380 | + if (pto instanceof Transition) { |
1381 | + ((Transition)pto).removeArcCompareObject(arc); |
1382 | + } |
1383 | + arc.updateArcPosition(); |
1384 | + } |
1385 | + } |
1386 | + |
1387 | + private void placetranstionMouseOver(PlaceTransitionObject pno) { |
1388 | + if (arc != null) { |
1389 | + if (arc.getSource() != pno && arc.getSource().areNotSameType(pno)) { |
1390 | + arc.setTarget(pno); |
1391 | + arc.updateArcPosition(); |
1392 | + } |
1393 | + } |
1394 | + } |
1395 | + |
1396 | + private void transitionClicked(TimedTransitionComponent pno) { |
1397 | + if (place1 != null && transition == null) { |
1398 | + transition = pno; |
1399 | + arc2 = arc = new TimedTransportArcComponent(pno, -1, false); |
1400 | + |
1401 | + //XXX calling zoomUpdate will set the endpoint to 0,0, drawing the arc from source to 0,0 |
1402 | + //to avoid this we change the endpoint to set the end point to the same as the end point |
1403 | + //needs further refactorings //kyrke 2019-09-05 |
1404 | + arc.setEndPoint(pno.getPositionX(), pno.getPositionY(), false); |
1405 | + CreateGui.getDrawingSurface().addPrototype(arc); |
1406 | + arc.requestFocusInWindow(); |
1407 | + arc.setSelectable(false); |
1408 | + arc.enableDrawingKeyBindings(this::clearPendingArc); |
1409 | + } |
1410 | + } |
1411 | + |
1412 | + private void placeClicked(TimedPlaceComponent pno) { |
1413 | + if (place1 == null && transition == null) { |
1414 | + place1 = pno; |
1415 | + arc1 = arc = new TimedTransportArcComponent(pno, -1, true); |
1416 | + //XXX calling zoomUpdate will set the endpoint to 0,0, drawing the arc from source to 0,0 |
1417 | + //to avoid this we change the endpoint to set the end point to the same as the end point |
1418 | + //needs further refactorings //kyrke 2019-09-05 |
1419 | + arc.setEndPoint(pno.getPositionX(), pno.getPositionY(), false); |
1420 | + CreateGui.getDrawingSurface().addPrototype(arc); |
1421 | + arc.requestFocusInWindow(); |
1422 | + arc.setSelectable(false); |
1423 | + arc.enableDrawingKeyBindings(this::clearPendingArc); |
1424 | + } else if (transition != null && place2 == null) { |
1425 | + place2 = pno; |
1426 | + CreateGui.getDrawingSurface().clearAllPrototype(); |
1427 | + guiModelManager.addTimedTransportArc(getModel(), place1, transition, place2, arc1.getArcPath(), arc2.getArcPath()); |
1428 | + clearPendingArc(); |
1429 | + } |
1430 | + } |
1431 | + |
1432 | + private void clearPendingArc() { |
1433 | + CreateGui.getDrawingSurface().clearAllPrototype(); |
1434 | + place1 = place2 = null; |
1435 | + transition = null; |
1436 | + arc = arc1 = arc2 = null; |
1437 | + } |
1438 | + |
1439 | + @Override |
1440 | + public void drawingSurfaceMouseMoved(MouseEvent e) { |
1441 | + if(arc!=null) { |
1442 | + arc.setEndPoint(e.getX(), e.getY(), e.isShiftDown()); |
1443 | + } |
1444 | + } |
1445 | + |
1446 | + @Override |
1447 | + public void drawingSurfaceMousePressed(MouseEvent e) { |
1448 | + if (arc!=null) { |
1449 | + Point p = e.getPoint(); |
1450 | + int x = Zoomer.getUnzoomedValue(p.x, CreateGui.getDrawingSurface().getZoom()); |
1451 | + int y = Zoomer.getUnzoomedValue(p.y, CreateGui.getDrawingSurface().getZoom()); |
1452 | + |
1453 | + boolean shiftDown = e.isShiftDown(); |
1454 | + //XXX: x,y is ignored is overwritten when mouse is moved, this just add a new point to the end of list |
1455 | + arc.getArcPath().addPoint(arc.getArcPath().getEndIndex(), x,y, shiftDown); |
1456 | + } |
1457 | + } |
1458 | + |
1459 | + @Override |
1460 | + public void registerManager(DrawingSurfaceImpl canvas) { |
1461 | + CreateGui.useExtendedBounds = true; |
1462 | + } |
1463 | + |
1464 | + @Override |
1465 | + public void deregisterManager() { |
1466 | + clearPendingArc(); |
1467 | + CreateGui.useExtendedBounds = false; |
1468 | + } |
1469 | + } |
1470 | + |
1471 | + private class CanvasGeneralDrawController extends AbstractDrawingSurfaceManager { |
1472 | + @Override |
1473 | + public void registerEvents() { |
1474 | + registerEvent( |
1475 | + e->e.pno instanceof TimedTransitionComponent && e.a == MouseAction.doubleClicked, |
1476 | + e-> ((TimedTransitionComponent) e.pno).showEditor() |
1477 | + ); |
1478 | + registerEvent( |
1479 | + e->e.pno instanceof TimedPlaceComponent && e.a == MouseAction.doubleClicked, |
1480 | + e-> ((TimedPlaceComponent) e.pno).showEditor() |
1481 | + ); |
1482 | + registerEvent( |
1483 | + e->e.pno instanceof TimedTransitionComponent && e.a == MouseAction.rightClicked, |
1484 | + e-> ((TimedTransitionComponent) e.pno).getMouseHandler().getPopup(e.e).show(e.pno, e.e.getX(), e.e.getY()) |
1485 | + ); |
1486 | + registerEvent( |
1487 | + e->e.pno instanceof TimedPlaceComponent && e.a == MouseAction.rightClicked, |
1488 | + e-> ((TimedPlaceComponent) e.pno).getMouseHandler().getPopup(e.e).show(e.pno, e.e.getX(), e.e.getY()) |
1489 | + ); |
1490 | + registerEvent( |
1491 | + e->e.pno instanceof Arc && e.a == MouseAction.rightClicked, |
1492 | + e-> ((Arc) e.pno).getMouseHandler().getPopup(e.e).show(e.pno, e.e.getX(), e.e.getY()) |
1493 | + ); |
1494 | + registerEvent( |
1495 | + e->e.pno instanceof AnnotationNote && e.a == MouseAction.doubleClicked, |
1496 | + e-> ((AnnotationNote) e.pno).enableEditMode() |
1497 | + ); |
1498 | + registerEvent( |
1499 | + e->e.pno instanceof AnnotationNote && e.a == MouseAction.rightClicked, |
1500 | + e-> ((AnnotationNote) e.pno).getMouseHandler().getPopup(e.e).show(e.pno, e.e.getX(), e.e.getY()) |
1501 | + ); |
1502 | + registerEvent( |
1503 | + e->e.pno instanceof Arc && e.a == MouseAction.entered, |
1504 | + e -> ((Arc)e.pno).getArcPath().showPoints() |
1505 | + ); |
1506 | + registerEvent( |
1507 | + e->e.pno instanceof Arc && e.a == MouseAction.exited, |
1508 | + e -> ((Arc)e.pno).getArcPath().hidePoints() |
1509 | + ); |
1510 | + registerEvent( |
1511 | + e->e.pno instanceof Arc && e.a == MouseAction.doubleClicked && e.e.isControlDown(), |
1512 | + e->arcDoubleClickedWithContrl(((Arc) e.pno), e.e) |
1513 | + ); |
1514 | + |
1515 | + } |
1516 | + |
1517 | + private void arcDoubleClickedWithContrl(Arc arc, MouseEvent e) { |
1518 | + CreateGui.getCurrentTab().getUndoManager().addNewEdit( |
1519 | + arc.getArcPath().insertPoint( |
1520 | + new Point2D.Double( |
1521 | + Zoomer.getUnzoomedValue(arc.getX() + e.getX(), arc.getZoom()), |
1522 | + Zoomer.getUnzoomedValue(arc.getY() + e.getY(), arc.getZoom()) |
1523 | + ), |
1524 | + e.isAltDown() |
1525 | + ) |
1526 | + ); |
1527 | + } |
1528 | + } |
1529 | } |
1530 | |
1531 | === modified file 'src/dk/aau/cs/gui/TemplateExplorer.java' |
1532 | --- src/dk/aau/cs/gui/TemplateExplorer.java 2020-05-27 13:15:44 +0000 |
1533 | +++ src/dk/aau/cs/gui/TemplateExplorer.java 2020-07-09 12:55:48 +0000 |
1534 | @@ -81,12 +81,12 @@ |
1535 | private JButton renameButton; |
1536 | private JButton copyButton; |
1537 | |
1538 | - private TabContent parent; |
1539 | - private UndoManager undoManager; |
1540 | + private final TabContent parent; |
1541 | + private final UndoManager undoManager; |
1542 | private boolean isInAnimationMode; |
1543 | |
1544 | - public JButton moveUpButton; |
1545 | - public JButton moveDownButton; |
1546 | + private JButton moveUpButton; |
1547 | + private JButton moveDownButton; |
1548 | private JButton sortButton; |
1549 | |
1550 | private static final String toolTipNewComponent ="Create a new component"; |
1551 | @@ -188,7 +188,7 @@ |
1552 | |
1553 | private void initExplorerPanel() { |
1554 | templatePanel = new JPanel(new GridBagLayout()); |
1555 | - listModel = new DefaultListModel(); |
1556 | + listModel = new DefaultListModel<>(); |
1557 | for (Template net : parent.allTemplates()) { |
1558 | listModel.addElement(net); |
1559 | } |
1560 | @@ -214,7 +214,7 @@ |
1561 | } |
1562 | }); |
1563 | |
1564 | - templateList = new NonsearchableJList(listModel); |
1565 | + templateList = new NonsearchableJList<>(listModel); |
1566 | |
1567 | templateList.setSelectionMode(ListSelectionModel.SINGLE_SELECTION); |
1568 | templateList.setSelectedIndex(0); |
1569 | @@ -476,7 +476,7 @@ |
1570 | private void onOKRenameTemplate() { |
1571 | Template template = selectedModel(); |
1572 | String newName = nameTextField.getText().trim(); |
1573 | - if (newName == null || template.model().name().equals(newName)) { |
1574 | + if (template.model().name().equals(newName)) { |
1575 | exit(); |
1576 | return; |
1577 | } |
1578 | @@ -508,37 +508,34 @@ |
1579 | } |
1580 | |
1581 | private void onOK() { |
1582 | - Template template = null; |
1583 | - String templateName = nameTextField.getText().trim(); |
1584 | - if (templateName != null) { |
1585 | - if(!isNameAllowed(templateName)) { |
1586 | - JOptionPane.showMessageDialog(parent.drawingSurface(), |
1587 | - "Acceptable names for components are defined by the regular expression:\n[a-zA-Z][_a-zA-Z0-9]*\n\nThe new component could not be created.", |
1588 | - "Error Creating Component", |
1589 | - JOptionPane.ERROR_MESSAGE); |
1590 | - exit(); |
1591 | - ShowNewTemplateDialog(templateName); |
1592 | - return; |
1593 | - } |
1594 | - else if (parent.network().hasTAPNCalled(templateName)) { |
1595 | - JOptionPane.showMessageDialog(parent.drawingSurface(), |
1596 | - "A component named \"" + templateName + "\" already exists.\n\nThe new component could not be created.", |
1597 | - "Error Creating Component", |
1598 | - JOptionPane.ERROR_MESSAGE); |
1599 | - exit(); |
1600 | - ShowNewTemplateDialog(templateName); |
1601 | - return; |
1602 | - } |
1603 | - else { |
1604 | - template = createNewTemplate(templateName); |
1605 | - |
1606 | - int index = listModel.size(); |
1607 | - undoManager.addNewEdit(new AddTemplateCommand(TemplateExplorer.this, template, index)); |
1608 | - parent.addTemplate(template); |
1609 | - } |
1610 | - } |
1611 | - |
1612 | - exit(); |
1613 | + String templateName = nameTextField.getText().trim(); |
1614 | + if(!isNameAllowed(templateName)) { |
1615 | + JOptionPane.showMessageDialog(parent.drawingSurface(), |
1616 | + "Acceptable names for components are defined by the regular expression:\n[a-zA-Z][_a-zA-Z0-9]*\n\nThe new component could not be created.", |
1617 | + "Error Creating Component", |
1618 | + JOptionPane.ERROR_MESSAGE); |
1619 | + exit(); |
1620 | + ShowNewTemplateDialog(templateName); |
1621 | + return; |
1622 | + } |
1623 | + else if (parent.network().hasTAPNCalled(templateName)) { |
1624 | + JOptionPane.showMessageDialog(parent.drawingSurface(), |
1625 | + "A component named \"" + templateName + "\" already exists.\n\nThe new component could not be created.", |
1626 | + "Error Creating Component", |
1627 | + JOptionPane.ERROR_MESSAGE); |
1628 | + exit(); |
1629 | + ShowNewTemplateDialog(templateName); |
1630 | + return; |
1631 | + } |
1632 | + else { |
1633 | + Template template = createNewTemplate(templateName); |
1634 | + |
1635 | + int index = listModel.size(); |
1636 | + undoManager.addNewEdit(new AddTemplateCommand(TemplateExplorer.this, template, index)); |
1637 | + parent.addTemplate(template); |
1638 | + } |
1639 | + |
1640 | + exit(); |
1641 | } |
1642 | |
1643 | private void exit() { |
1644 | @@ -639,8 +636,7 @@ |
1645 | } |
1646 | |
1647 | private void ShowNewTemplateDialog(String nameToShow) { |
1648 | - dialog = new EscapableDialog(CreateGui.getApp(), |
1649 | - "Enter Component Name", true); |
1650 | + dialog = new EscapableDialog(CreateGui.getApp(), "Enter Component Name", true); |
1651 | initComponentsOfNewTemplateDialog(nameToShow); |
1652 | dialog.add(container); |
1653 | dialog.setResizable(false); |
1654 | @@ -742,8 +738,7 @@ |
1655 | } |
1656 | |
1657 | private void showRenameTemplateDialog(String nameToShow) { |
1658 | - dialog = new EscapableDialog(CreateGui.getApp(), |
1659 | - "Enter Component Name", true); |
1660 | + dialog = new EscapableDialog(CreateGui.getApp(), "Enter Component Name", true); |
1661 | Template template = selectedModel(); |
1662 | if (nameToShow.equals("")){ |
1663 | initComponentsOfRenameTemplateDialog(template.model().name()); |
1664 | @@ -777,7 +772,7 @@ |
1665 | |
1666 | public void openSelectedTemplate() { |
1667 | Template tapn = selectedModel(); |
1668 | - if (tapn != null && parent.isTabInFocus()) { |
1669 | + if (tapn != null) { |
1670 | parent.changeToTemplate(tapn); |
1671 | } |
1672 | //parent.drawingSurface().repaintAll(); |
1673 | @@ -789,7 +784,7 @@ |
1674 | |
1675 | public void updateTemplateList() { |
1676 | int selectedIndex = templateList.getSelectedIndex(); |
1677 | - DefaultListModel newList = new DefaultListModel(); |
1678 | + DefaultListModel<Template> newList = new DefaultListModel<>(); |
1679 | |
1680 | if(isInAnimationMode) { |
1681 | for (Template net : parent.activeTemplates()) { |
1682 | @@ -852,7 +847,7 @@ |
1683 | listModel.setElementAt(o, index+1); |
1684 | } |
1685 | @Override |
1686 | - public JList getJList(){ |
1687 | + public JList<Template> getJList(){ |
1688 | return templateList; |
1689 | } |
1690 | |
1691 | @@ -995,21 +990,24 @@ |
1692 | } |
1693 | renameButton.setEnabled(true); |
1694 | copyButton.setEnabled(true); |
1695 | - if(templateList.getModel().getSize() >= 2) |
1696 | - sortButton.setEnabled(true); |
1697 | - else |
1698 | - sortButton.setEnabled(false); |
1699 | - |
1700 | - if(index > 0) |
1701 | - moveUpButton.setEnabled(true); |
1702 | - else |
1703 | - moveUpButton.setEnabled(false); |
1704 | + if(templateList.getModel().getSize() >= 2) { |
1705 | + sortButton.setEnabled(true); |
1706 | + } else { |
1707 | + sortButton.setEnabled(false); |
1708 | + } |
1709 | + |
1710 | + if(index > 0) { |
1711 | + moveUpButton.setEnabled(true); |
1712 | + } else { |
1713 | + moveUpButton.setEnabled(false); |
1714 | + } |
1715 | |
1716 | |
1717 | - if(index < parent.network().allTemplates().size() - 1) |
1718 | - moveDownButton.setEnabled(true); |
1719 | - else |
1720 | - moveDownButton.setEnabled(false); |
1721 | + if(index < parent.network().allTemplates().size() - 1) { |
1722 | + moveDownButton.setEnabled(true); |
1723 | + } else { |
1724 | + moveDownButton.setEnabled(false); |
1725 | + } |
1726 | } |
1727 | templateList.ensureIndexIsVisible(index); |
1728 | openSelectedTemplate(); |
1729 | |
1730 | === modified file 'src/dk/aau/cs/gui/components/EnabledTransitionsList.java' |
1731 | --- src/dk/aau/cs/gui/components/EnabledTransitionsList.java 2020-05-18 08:14:37 +0000 |
1732 | +++ src/dk/aau/cs/gui/components/EnabledTransitionsList.java 2020-07-09 12:55:48 +0000 |
1733 | @@ -38,17 +38,14 @@ |
1734 | initPanel(); |
1735 | } |
1736 | |
1737 | - DefaultListModel<TransitionListItem> transitions; |
1738 | - JList<TransitionListItem> transitionsList; |
1739 | - JScrollPane scrollPane; |
1740 | + final DefaultListModel<TransitionListItem> transitions = new DefaultListModel<>(); |
1741 | + final JList<TransitionListItem> transitionsList = new JList<>(transitions); |
1742 | + final JScrollPane scrollPane = new JScrollPane(transitionsList); |
1743 | TransitionListItem lastSelected; |
1744 | |
1745 | public void initPanel(){ |
1746 | - transitions = new DefaultListModel<>(); |
1747 | - transitionsList = new JList<>(transitions); |
1748 | - transitionsList.setCellRenderer(new EnabledTransitionListCellRenderer()); |
1749 | |
1750 | - transitionsList.addMouseListener(new MouseAdapter() { |
1751 | + transitionsList.addMouseListener(new MouseAdapter() { |
1752 | @Override |
1753 | public void mouseClicked(MouseEvent e) { |
1754 | if(e.getClickCount() == 2){ |
1755 | @@ -64,9 +61,7 @@ |
1756 | } |
1757 | }); |
1758 | |
1759 | - scrollPane = new JScrollPane(transitionsList); |
1760 | - |
1761 | - this.add(scrollPane, BorderLayout.CENTER); |
1762 | + this.add(scrollPane, BorderLayout.CENTER); |
1763 | } |
1764 | |
1765 | public void startReInit(){ |
1766 | @@ -110,18 +105,12 @@ |
1767 | public void addTransition(Template template, Transition transition){ |
1768 | TransitionListItem item = new TransitionListItem(transition, template); |
1769 | |
1770 | - transition.isDelayEnabled(); |
1771 | if(!transitions.contains(item)){ |
1772 | transitions.addElement(item); |
1773 | } |
1774 | } |
1775 | |
1776 | - public void removeTransition(Template template, Transition transition){ |
1777 | - TransitionListItem item = new TransitionListItem(transition, template); |
1778 | - transitions.removeElement(item); |
1779 | - } |
1780 | - |
1781 | - public void fireSelectedTransition(){ |
1782 | + public void fireSelectedTransition(){ |
1783 | TransitionListItem item = transitionsList.getSelectedValue(); |
1784 | |
1785 | if(item != null) { |
1786 | @@ -131,27 +120,10 @@ |
1787 | |
1788 | interface ListItem extends Comparable<ListItem>{} |
1789 | |
1790 | - class SplitterListItem implements ListItem{ |
1791 | - |
1792 | - @Override |
1793 | - public int compareTo(ListItem o) { |
1794 | - if(o instanceof TransitionListItem){ |
1795 | - return o.compareTo(this); |
1796 | - } else { |
1797 | - return 0; |
1798 | - } |
1799 | - } |
1800 | - |
1801 | - @Override |
1802 | - public String toString() { |
1803 | - return "_"; |
1804 | - } |
1805 | - |
1806 | - } |
1807 | |
1808 | static class TransitionListItem implements ListItem{ |
1809 | - private Transition transition; |
1810 | - private Template template; |
1811 | + private final Transition transition; |
1812 | + private final Template template; |
1813 | |
1814 | public TransitionListItem(Transition transition, Template template){ |
1815 | this.transition = transition; |
1816 | @@ -160,8 +132,7 @@ |
1817 | |
1818 | public String toString(boolean showIntervals) { |
1819 | |
1820 | - String interval = transition.getDInterval() == null || !showIntervals ? |
1821 | - "" : transition.getDInterval().toString() + " "; |
1822 | + String interval = transition.getDInterval() == null || !showIntervals ? "" : transition.getDInterval().toString() + " "; |
1823 | |
1824 | String transitionName = getTransition().getName(); |
1825 | if(isShared()){ |
1826 | @@ -237,51 +208,6 @@ |
1827 | } |
1828 | } |
1829 | |
1830 | - //This class creates the stippled line shown between the enabled transitions and the delay-enabled transitions |
1831 | - class EnabledTransitionListCellRenderer extends DefaultListCellRenderer{ |
1832 | - |
1833 | - @Override |
1834 | - public Component getListCellRendererComponent(JList list, Object value, |
1835 | - int index, boolean isSelected, boolean cellHasFocus) { |
1836 | - if(value instanceof SplitterListItem){ |
1837 | - JLabel separator = new JLabel(); |
1838 | - separator.setBorder(new DashBorder()); |
1839 | - separator.setPreferredSize(new Dimension(1, 1)); |
1840 | - return separator; |
1841 | - } else { |
1842 | - return super.getListCellRendererComponent(list, value, index, isSelected, cellHasFocus); |
1843 | - } |
1844 | - } |
1845 | - |
1846 | - class DashBorder implements Border { |
1847 | - private final Insets insets = new Insets(1, 1, 1, 1); |
1848 | - private final int length = 5; |
1849 | - private final int space = 3; |
1850 | - public boolean isBorderOpaque() { |
1851 | - return false; |
1852 | - } |
1853 | - public void paintBorder(Component c, Graphics g, int x, int y, |
1854 | - int width, int height) { |
1855 | - g.setColor(Color.BLACK); |
1856 | - // --- draw horizontal --- |
1857 | - for (int i = 0; i < width; i += length) { |
1858 | - g.drawLine(i, y, i + length, y); |
1859 | - g.drawLine(i, height - 1, i + length, height - 1); |
1860 | - i += space; |
1861 | - } |
1862 | - // --- draw vertical --- |
1863 | - for (int i = 0; i < height; i += length) { |
1864 | - g.drawLine(0, i, 0, i + length); |
1865 | - g.drawLine(width - 1, i, width - 1, i + length); |
1866 | - i += space; |
1867 | - } |
1868 | - } |
1869 | - public Insets getBorderInsets(Component c) { |
1870 | - return insets; |
1871 | - } |
1872 | - } |
1873 | - } |
1874 | - |
1875 | public int getNumberOfTransitions() { |
1876 | return transitions.size(); |
1877 | } |
1878 | |
1879 | === modified file 'src/dk/aau/cs/gui/components/NonsearchableJList.java' |
1880 | --- src/dk/aau/cs/gui/components/NonsearchableJList.java 2020-04-18 12:27:02 +0000 |
1881 | +++ src/dk/aau/cs/gui/components/NonsearchableJList.java 2020-07-09 12:55:48 +0000 |
1882 | @@ -19,7 +19,7 @@ |
1883 | removeKeyListener(); |
1884 | } |
1885 | |
1886 | - public NonsearchableJList(ListModel dataModel){ |
1887 | + public NonsearchableJList(ListModel<E> dataModel){ |
1888 | super (dataModel); |
1889 | removeKeyListener(); |
1890 | } |
1891 | |
1892 | === modified file 'src/dk/aau/cs/gui/components/TransitionFireingComponent.java' |
1893 | --- src/dk/aau/cs/gui/components/TransitionFireingComponent.java 2020-05-18 14:10:47 +0000 |
1894 | +++ src/dk/aau/cs/gui/components/TransitionFireingComponent.java 2020-07-09 12:55:48 +0000 |
1895 | @@ -28,14 +28,19 @@ |
1896 | |
1897 | enabledTransitionsList = new EnabledTransitionsList(); |
1898 | |
1899 | - this.setBorder(BorderFactory.createCompoundBorder( |
1900 | + this.setBorder( |
1901 | + BorderFactory.createCompoundBorder( |
1902 | BorderFactory.createTitledBorder("Enabled Transitions"), |
1903 | - BorderFactory.createEmptyBorder(3, 3, 3, 3))); |
1904 | - this |
1905 | - .setToolTipText("List of currently enabled transitions (double click a transition to fire it)"); |
1906 | - enabledTransitionsList.setPreferredSize(new Dimension( |
1907 | + BorderFactory.createEmptyBorder(3, 3, 3, 3) |
1908 | + ) |
1909 | + ); |
1910 | + this.setToolTipText("List of currently enabled transitions (double click a transition to fire it)"); |
1911 | + enabledTransitionsList.setPreferredSize( |
1912 | + new Dimension( |
1913 | enabledTransitionsList.getPreferredSize().width, |
1914 | - enabledTransitionsList.getMinimumSize().height)); |
1915 | + enabledTransitionsList.getMinimumSize().height |
1916 | + ) |
1917 | + ); |
1918 | |
1919 | settingsButton = new JButton("Settings"); |
1920 | settingsButton.setPreferredSize(new Dimension(0, settingsButton.getPreferredSize().height)); //Make the two buttons equal in size |
1921 | @@ -50,6 +55,7 @@ |
1922 | fireSelectedTransition(); |
1923 | } |
1924 | }); |
1925 | + |
1926 | fireButton.addKeyListener(new KeyAdapter() { |
1927 | @Override |
1928 | public void keyPressed(KeyEvent e) { |
1929 | |
1930 | === modified file 'src/dk/aau/cs/gui/smartDraw/SmartDrawWorker.java' |
1931 | --- src/dk/aau/cs/gui/smartDraw/SmartDrawWorker.java 2020-05-23 12:57:37 +0000 |
1932 | +++ src/dk/aau/cs/gui/smartDraw/SmartDrawWorker.java 2020-07-09 12:55:48 +0000 |
1933 | @@ -2,7 +2,6 @@ |
1934 | |
1935 | import java.awt.Point; |
1936 | import java.util.ArrayList; |
1937 | -import java.util.Iterator; |
1938 | import java.util.List; |
1939 | import java.util.Random; |
1940 | |
1941 | @@ -199,19 +198,16 @@ |
1942 | } |
1943 | } |
1944 | |
1945 | - private ArrayList<Arc> getAllArcsFromObject(PlaceTransitionObject object) { |
1946 | + private ArrayList<Arc> getAllArcsFromObject(PlaceTransitionObject pno) { |
1947 | ArrayList<Arc> arcsForObject = new ArrayList<Arc>(); |
1948 | - Iterator<Arc> fromIterator = object.getConnectFromIterator(); |
1949 | - Iterator<Arc> toIterator = object.getConnectToIterator(); |
1950 | - Arc arc; |
1951 | - while(fromIterator.hasNext()) { |
1952 | - arc = fromIterator.next(); |
1953 | - arcsForObject.add(arc); |
1954 | - } |
1955 | - while(toIterator.hasNext()) { |
1956 | - arc = toIterator.next(); |
1957 | - arcsForObject.add(arc); |
1958 | - } |
1959 | + |
1960 | + for (Arc a : pno.getPreset()) { |
1961 | + arcsForObject.add(a); |
1962 | + } |
1963 | + for (Arc a : pno.getPostset()) { |
1964 | + arcsForObject.add(a); |
1965 | + } |
1966 | + |
1967 | return arcsForObject; |
1968 | } |
1969 | private void moveObject(PlaceTransitionObject object, Point point) { |
1970 | |
1971 | === modified file 'src/dk/aau/cs/gui/undo/TimedPlaceMarkingEdit.java' |
1972 | --- src/dk/aau/cs/gui/undo/TimedPlaceMarkingEdit.java 2011-09-23 21:23:31 +0000 |
1973 | +++ src/dk/aau/cs/gui/undo/TimedPlaceMarkingEdit.java 2020-07-09 12:55:48 +0000 |
1974 | @@ -4,7 +4,7 @@ |
1975 | |
1976 | // TODO: Fix this to work on the model class instead of the GUI class |
1977 | public class TimedPlaceMarkingEdit extends Command { |
1978 | - private int numberOfTokens; |
1979 | + private final int numberOfTokens; |
1980 | private final TimedPlaceComponent timedPlaceComponent; |
1981 | |
1982 | public TimedPlaceMarkingEdit(TimedPlaceComponent tpc, int numberOfTokens) { |
1983 | @@ -15,9 +15,9 @@ |
1984 | @Override |
1985 | public void redo() { |
1986 | if (numberOfTokens > 0) { |
1987 | - timedPlaceComponent.addTokens(Math.abs(numberOfTokens)); |
1988 | + timedPlaceComponent.underlyingPlace().addTokens(Math.abs(numberOfTokens)); |
1989 | } else { |
1990 | - timedPlaceComponent.removeTokens(Math.abs(numberOfTokens)); |
1991 | + timedPlaceComponent.underlyingPlace().removeTokens(Math.abs(numberOfTokens)); |
1992 | } |
1993 | timedPlaceComponent.repaint(); |
1994 | } |
1995 | @@ -25,9 +25,9 @@ |
1996 | @Override |
1997 | public void undo() { |
1998 | if (numberOfTokens > 0) { |
1999 | - timedPlaceComponent.removeTokens(Math.abs(numberOfTokens)); |
2000 | + timedPlaceComponent.underlyingPlace().removeTokens(Math.abs(numberOfTokens)); |
2001 | } else { |
2002 | - timedPlaceComponent.addTokens(Math.abs(numberOfTokens)); |
2003 | + timedPlaceComponent.underlyingPlace().addTokens(Math.abs(numberOfTokens)); |
2004 | } |
2005 | timedPlaceComponent.repaint(); |
2006 | } |
2007 | |
2008 | === modified file 'src/dk/aau/cs/io/TapnXmlLoader.java' |
2009 | --- src/dk/aau/cs/io/TapnXmlLoader.java 2020-05-06 15:19:14 +0000 |
2010 | +++ src/dk/aau/cs/io/TapnXmlLoader.java 2020-07-09 12:55:48 +0000 |
2011 | @@ -162,10 +162,9 @@ |
2012 | } |
2013 | |
2014 | SharedPlace place = new SharedPlace(name, invariant); |
2015 | + place.addTokens(numberOfTokens); |
2016 | place.setCurrentMarking(marking); |
2017 | - for(int j = 0; j < numberOfTokens; j++){ |
2018 | - marking.add(new TimedToken(place)); |
2019 | - } |
2020 | + |
2021 | return place; |
2022 | } |
2023 | |
2024 | |
2025 | === modified file 'src/dk/aau/cs/model/tapn/LocalTimedPlace.java' |
2026 | --- src/dk/aau/cs/model/tapn/LocalTimedPlace.java 2019-11-26 13:59:12 +0000 |
2027 | +++ src/dk/aau/cs/model/tapn/LocalTimedPlace.java 2020-07-09 12:55:48 +0000 |
2028 | @@ -1,28 +1,12 @@ |
2029 | package dk.aau.cs.model.tapn; |
2030 | |
2031 | -import java.util.ArrayList; |
2032 | -import java.util.List; |
2033 | -import java.util.regex.Pattern; |
2034 | - |
2035 | -import dk.aau.cs.model.tapn.TimedPlace.PlaceType; |
2036 | -import dk.aau.cs.model.tapn.event.TimedPlaceEvent; |
2037 | -import dk.aau.cs.model.tapn.event.TimedPlaceListener; |
2038 | -import dk.aau.cs.util.Require; |
2039 | import dk.aau.cs.util.Tuple; |
2040 | |
2041 | public class LocalTimedPlace extends TimedPlace { |
2042 | - private static final Pattern namePattern = Pattern.compile("^[a-zA-Z_][a-zA-Z0-9_]*$"); |
2043 | - |
2044 | - private String name; |
2045 | - private TimeInvariant invariant; |
2046 | |
2047 | private TimedArcPetriNet model; |
2048 | - private TimedMarking currentMarking; |
2049 | - private List<TimedPlaceListener> listeners = new ArrayList<TimedPlaceListener>(); |
2050 | - |
2051 | - private Tuple<PlaceType, Integer> extrapolation = new Tuple<TimedPlace.PlaceType, Integer>(PlaceType.Dead, -2); |
2052 | |
2053 | - public LocalTimedPlace(String name) { |
2054 | + public LocalTimedPlace(String name) { |
2055 | this(name, TimeInvariant.LESS_THAN_INFINITY); |
2056 | } |
2057 | |
2058 | @@ -39,111 +23,10 @@ |
2059 | this.model = model; |
2060 | } |
2061 | |
2062 | - public void addTimedPlaceListener(TimedPlaceListener listener){ |
2063 | - Require.that(listener != null, "Listener cannot be null"); |
2064 | - listeners.add(listener); |
2065 | - } |
2066 | - |
2067 | - public void removeTimedPlaceListener(TimedPlaceListener listener){ |
2068 | - Require.that(listener != null, "Listener cannot be null"); |
2069 | - listeners.remove(listener); |
2070 | - } |
2071 | - |
2072 | public boolean isShared() { |
2073 | return false; |
2074 | } |
2075 | |
2076 | - public void setCurrentMarking(TimedMarking marking) { |
2077 | - Require.that(marking != null, "marking cannot be null"); |
2078 | - currentMarking = marking; |
2079 | - fireMarkingChanged(); |
2080 | - } |
2081 | - |
2082 | - public String name() { |
2083 | - return name; |
2084 | - } |
2085 | - |
2086 | - public void setName(String newName) { |
2087 | - Require.that(newName != null && !newName.isEmpty(), "A timed place must have a name"); |
2088 | - Require.that(isValid(newName) && !newName.toLowerCase().equals("true") && !newName.toLowerCase().equals("false"), "The specified name must conform to the pattern [a-zA-Z_][a-zA-Z0-9_]*"); |
2089 | - this.name = newName; |
2090 | - fireNameChanged(); |
2091 | - } |
2092 | - |
2093 | - private void fireNameChanged() { |
2094 | - for(TimedPlaceListener listener : listeners){ |
2095 | - listener.nameChanged(new TimedPlaceEvent(this)); |
2096 | - } |
2097 | - } |
2098 | - |
2099 | - private void fireInvariantChanged(){ |
2100 | - for(TimedPlaceListener listener : listeners){ |
2101 | - listener.invariantChanged(new TimedPlaceEvent(this)); |
2102 | - } |
2103 | - } |
2104 | - |
2105 | - private void fireMarkingChanged(){ |
2106 | - for(TimedPlaceListener listener : listeners){ |
2107 | - listener.markingChanged(new TimedPlaceEvent(this)); |
2108 | - } |
2109 | - } |
2110 | - |
2111 | - private boolean isValid(String newName) { |
2112 | - return namePattern.matcher(newName).matches(); |
2113 | - } |
2114 | - |
2115 | - public TimeInvariant invariant() { |
2116 | - return invariant; |
2117 | - } |
2118 | - |
2119 | - public void setInvariant(TimeInvariant invariant) { |
2120 | - Require.that(invariant != null, "A timed place must have a non-null invariant"); |
2121 | - this.invariant = invariant; |
2122 | - fireInvariantChanged(); |
2123 | - } |
2124 | - |
2125 | - public List<TimedToken> tokens() { |
2126 | - return currentMarking.getTokensFor(this); |
2127 | - } |
2128 | - |
2129 | - public int numberOfTokens() { |
2130 | - return tokens().size(); |
2131 | - } |
2132 | - |
2133 | - @Override |
2134 | - public void addToken(TimedToken timedToken) { |
2135 | - Require.that(timedToken != null, "timedToken cannot be null"); |
2136 | - Require.that(timedToken.place().equals(this), "token is located in a different place"); |
2137 | - |
2138 | - currentMarking.add(timedToken); |
2139 | - fireMarkingChanged(); |
2140 | - } |
2141 | - |
2142 | - @Override |
2143 | - public void addTokens(Iterable<TimedToken> tokens) { |
2144 | - Require.that(tokens != null, "tokens cannot be null"); |
2145 | - |
2146 | - for(TimedToken token : tokens){ |
2147 | - currentMarking.add(token); // avoid firing marking changed on every add |
2148 | - } |
2149 | - fireMarkingChanged(); |
2150 | - } |
2151 | - |
2152 | - @Override |
2153 | - public void removeToken(TimedToken timedToken) { |
2154 | - Require.that(timedToken != null, "timedToken cannot be null"); |
2155 | - currentMarking.remove(timedToken); |
2156 | - fireMarkingChanged(); |
2157 | - } |
2158 | - |
2159 | - @Override |
2160 | - public void removeToken() { |
2161 | - if (numberOfTokens() > 0) { |
2162 | - currentMarking.remove(tokens().get(0)); |
2163 | - fireMarkingChanged(); |
2164 | - } |
2165 | - } |
2166 | - |
2167 | public LocalTimedPlace copy() { |
2168 | LocalTimedPlace p = new LocalTimedPlace(name); |
2169 | |
2170 | |
2171 | === modified file 'src/dk/aau/cs/model/tapn/NetworkMarking.java' |
2172 | --- src/dk/aau/cs/model/tapn/NetworkMarking.java 2020-05-23 13:29:16 +0000 |
2173 | +++ src/dk/aau/cs/model/tapn/NetworkMarking.java 2020-07-09 12:55:48 +0000 |
2174 | @@ -14,8 +14,8 @@ |
2175 | import dk.aau.cs.util.Tuple; |
2176 | |
2177 | public class NetworkMarking implements TimedMarking { |
2178 | - private HashMap<TimedArcPetriNet, LocalTimedMarking> markings = new HashMap<TimedArcPetriNet, LocalTimedMarking>(); |
2179 | - private HashMap<TimedPlace, List<TimedToken>> sharedPlacesTokens = new HashMap<TimedPlace, List<TimedToken>>(); |
2180 | + private final HashMap<TimedArcPetriNet, LocalTimedMarking> markings = new HashMap<TimedArcPetriNet, LocalTimedMarking>(); |
2181 | + private final HashMap<TimedPlace, List<TimedToken>> sharedPlacesTokens = new HashMap<TimedPlace, List<TimedToken>>(); |
2182 | |
2183 | public NetworkMarking() { |
2184 | } |
2185 | @@ -130,8 +130,9 @@ |
2186 | private Tuple<NetworkMarking, List<TimedToken>> fireSharedTransition(SharedTransition sharedTransition, FiringMode firingMode) { |
2187 | // validity of arguments already checked above |
2188 | NetworkMarking clone = clone(); |
2189 | - Tuple<LocalTimedMarking, List<TimedToken>> ltm; |
2190 | - List<TimedToken> consumedTokens = new ArrayList<TimedToken>(); |
2191 | + Tuple<LocalTimedMarking, List<TimedToken>> ltm; |
2192 | + List<TimedToken> consumedTokens = new ArrayList<TimedToken>(); |
2193 | + |
2194 | for(TimedTransition transition : sharedTransition.transitions()){ |
2195 | if(transition.model().isActive()) { |
2196 | ltm = clone.getMarkingFor(transition.model()).fireTransition(transition, firingMode); |
2197 | |
2198 | === modified file 'src/dk/aau/cs/model/tapn/SharedPlace.java' |
2199 | --- src/dk/aau/cs/model/tapn/SharedPlace.java 2020-06-03 18:20:30 +0000 |
2200 | +++ src/dk/aau/cs/model/tapn/SharedPlace.java 2020-07-09 12:55:48 +0000 |
2201 | @@ -1,30 +1,16 @@ |
2202 | package dk.aau.cs.model.tapn; |
2203 | |
2204 | import java.util.ArrayList; |
2205 | -import java.util.List; |
2206 | -import java.util.regex.Pattern; |
2207 | |
2208 | import pipe.dataLayer.Template; |
2209 | import pipe.gui.CreateGui; |
2210 | -import dk.aau.cs.model.tapn.event.TimedPlaceEvent; |
2211 | -import dk.aau.cs.model.tapn.event.TimedPlaceListener; |
2212 | -import dk.aau.cs.util.Require; |
2213 | import dk.aau.cs.util.Tuple; |
2214 | |
2215 | public class SharedPlace extends TimedPlace{ |
2216 | - private static final Pattern namePattern = Pattern.compile("^[a-zA-Z_][a-zA-Z0-9_]*$"); |
2217 | - |
2218 | - private String name; |
2219 | - private List<TimedPlace> places = new ArrayList<TimedPlace>(); |
2220 | - private TimeInvariant invariant; |
2221 | - |
2222 | - private TimedArcPetriNetNetwork network; |
2223 | - private TimedMarking currentMarking; |
2224 | - private Tuple<PlaceType, Integer> extrapolation = new Tuple<TimedPlace.PlaceType, Integer>(PlaceType.Dead, -2); |
2225 | - |
2226 | - private List<TimedPlaceListener> listeners = new ArrayList<TimedPlaceListener>(); |
2227 | - |
2228 | - public SharedPlace(String name){ |
2229 | + |
2230 | + private TimedArcPetriNetNetwork network; |
2231 | + |
2232 | + public SharedPlace(String name){ |
2233 | this(name, TimeInvariant.LESS_THAN_INFINITY); |
2234 | } |
2235 | |
2236 | @@ -32,33 +18,8 @@ |
2237 | setName(name); |
2238 | setInvariant(invariant); |
2239 | } |
2240 | - |
2241 | - public String name() { |
2242 | - return name; |
2243 | - } |
2244 | - |
2245 | - public void setName(String newName) { |
2246 | - Require.that(newName != null && !newName.isEmpty(), "A timed transition must have a name"); |
2247 | - Require.that(isValid(newName) && !newName.toLowerCase().equals("true") && !newName.toLowerCase().equals("false"), "The specified name must conform to the pattern [a-zA-Z_][a-zA-Z0-9_]*"); |
2248 | - name = newName; |
2249 | - fireNameChanged(); |
2250 | - } |
2251 | - |
2252 | - private boolean isValid(String newName) { |
2253 | - return namePattern.matcher(newName).matches(); |
2254 | - } |
2255 | - |
2256 | - public TimeInvariant invariant(){ |
2257 | - return invariant; |
2258 | - } |
2259 | - |
2260 | - public void setInvariant(TimeInvariant invariant) { |
2261 | - Require.that(invariant != null, "invariant must not be null"); |
2262 | - this.invariant = invariant; |
2263 | - fireInvariantChanged(); |
2264 | - } |
2265 | - |
2266 | - public void setNetwork(TimedArcPetriNetNetwork network) { |
2267 | + |
2268 | + public void setNetwork(TimedArcPetriNetNetwork network) { |
2269 | this.network = network; |
2270 | } |
2271 | |
2272 | @@ -66,15 +27,7 @@ |
2273 | return network; |
2274 | } |
2275 | |
2276 | - public void addTimedPlaceListener(TimedPlaceListener listener) { |
2277 | - Require.that(listener != null, "Listener cannot be null"); |
2278 | - listeners.add(listener); |
2279 | - } |
2280 | |
2281 | - public void removeTimedPlaceListener(TimedPlaceListener listener) { |
2282 | - Require.that(listener != null, "Listener cannot be null"); |
2283 | - listeners.remove(listener); |
2284 | - } |
2285 | |
2286 | public TimedPlace copy() { |
2287 | return new SharedPlace(this.name(), this.invariant().copy()); |
2288 | @@ -84,71 +37,6 @@ |
2289 | return true; |
2290 | } |
2291 | |
2292 | - public void setCurrentMarking(TimedMarking marking) { |
2293 | - Require.that(marking != null, "marking cannot be null"); |
2294 | - currentMarking = marking; |
2295 | - fireMarkingChanged(); |
2296 | - } |
2297 | - |
2298 | - @Override |
2299 | - public void addToken(TimedToken timedToken) { |
2300 | - Require.that(timedToken != null, "timedToken cannot be null"); |
2301 | - Require.that(timedToken.place().equals(this), "token is located in a different place"); |
2302 | - |
2303 | - currentMarking.add(timedToken); |
2304 | - fireMarkingChanged(); |
2305 | - } |
2306 | - |
2307 | - @Override |
2308 | - public void addTokens(Iterable<TimedToken> tokens) { |
2309 | - Require.that(tokens != null, "tokens cannot be null"); // TODO: maybe check that tokens are in this place? |
2310 | - |
2311 | - for(TimedToken token : tokens){ |
2312 | - currentMarking.add(token); // avoid firing marking changed on every add |
2313 | - } |
2314 | - fireMarkingChanged(); |
2315 | - } |
2316 | - |
2317 | - @Override |
2318 | - public void removeToken(TimedToken timedToken) { |
2319 | - Require.that(timedToken != null, "timedToken cannot be null"); |
2320 | - currentMarking.remove(timedToken); |
2321 | - fireMarkingChanged(); |
2322 | - } |
2323 | - |
2324 | - @Override |
2325 | - public void removeToken() { |
2326 | - if (numberOfTokens() > 0) { |
2327 | - currentMarking.remove(tokens().get(0)); |
2328 | - fireMarkingChanged(); |
2329 | - } |
2330 | - } |
2331 | - |
2332 | - public List<TimedToken> tokens() { |
2333 | - return currentMarking.getTokensFor(this); |
2334 | - } |
2335 | - |
2336 | - public int numberOfTokens() { |
2337 | - return tokens().size(); |
2338 | - } |
2339 | - |
2340 | - private void fireMarkingChanged() { |
2341 | - for(TimedPlaceListener listener : listeners){ |
2342 | - listener.markingChanged(new TimedPlaceEvent(this)); |
2343 | - } |
2344 | - } |
2345 | - |
2346 | - private void fireNameChanged() { |
2347 | - for(TimedPlaceListener listener : listeners){ |
2348 | - listener.nameChanged(new TimedPlaceEvent(this)); |
2349 | - } |
2350 | - } |
2351 | - |
2352 | - private void fireInvariantChanged() { |
2353 | - for(TimedPlaceListener listener : listeners){ |
2354 | - listener.invariantChanged(new TimedPlaceEvent(this)); |
2355 | - } |
2356 | - } |
2357 | |
2358 | public ArrayList<String> getComponentsUsingThisPlace(){ |
2359 | ArrayList<String> components = new ArrayList<String>(); |
2360 | @@ -214,8 +102,4 @@ |
2361 | |
2362 | return new Tuple<TimedPlace.PlaceType, Integer>(type, cmax); |
2363 | } |
2364 | - |
2365 | - public List<TimedPlace> getPlaces() { |
2366 | - return places; |
2367 | - } |
2368 | } |
2369 | |
2370 | === modified file 'src/dk/aau/cs/model/tapn/TimedArcPetriNet.java' |
2371 | --- src/dk/aau/cs/model/tapn/TimedArcPetriNet.java 2020-06-03 12:16:19 +0000 |
2372 | +++ src/dk/aau/cs/model/tapn/TimedArcPetriNet.java 2020-07-09 12:55:48 +0000 |
2373 | @@ -18,18 +18,17 @@ |
2374 | //This is used when loading big nets as the checking of names is slow. |
2375 | private boolean checkNames = true; |
2376 | |
2377 | - private List<TimedPlace> places = new ArrayList<TimedPlace>(); |
2378 | - private List<TimedTransition> transitions = new ArrayList<TimedTransition>(); |
2379 | - private List<TimedInputArc> inputArcs = new ArrayList<TimedInputArc>(); |
2380 | - private List<TimedOutputArc> outputArcs = new ArrayList<TimedOutputArc>(); |
2381 | - private List<TimedInhibitorArc> inhibitorArcs = new ArrayList<TimedInhibitorArc>(); |
2382 | - private List<TransportArc> transportArcs = new ArrayList<TransportArc>(); |
2383 | + private final List<TimedPlace> places = new ArrayList<TimedPlace>(); |
2384 | + private final List<TimedTransition> transitions = new ArrayList<TimedTransition>(); |
2385 | + private final List<TimedInputArc> inputArcs = new ArrayList<TimedInputArc>(); |
2386 | + private final List<TimedOutputArc> outputArcs = new ArrayList<TimedOutputArc>(); |
2387 | + private final List<TimedInhibitorArc> inhibitorArcs = new ArrayList<TimedInhibitorArc>(); |
2388 | + private final List<TransportArc> transportArcs = new ArrayList<TransportArc>(); |
2389 | |
2390 | - private TimedMarking currentMarking; |
2391 | + private TimedMarking currentMarking = new LocalTimedMarking(); |
2392 | |
2393 | public TimedArcPetriNet(String name) { |
2394 | setName(name); |
2395 | - setMarking(new LocalTimedMarking()); |
2396 | isActive = true; |
2397 | } |
2398 | |
2399 | @@ -127,11 +126,7 @@ |
2400 | currentMarking.add(token); |
2401 | } |
2402 | |
2403 | - public void removeToken(TimedToken token) { |
2404 | - currentMarking.remove(token); |
2405 | - } |
2406 | - |
2407 | - public void remove(TimedPlace place) { |
2408 | + public void remove(TimedPlace place) { |
2409 | boolean removed = places.remove(place); |
2410 | if (removed && !place.isShared()){ |
2411 | currentMarking.removePlaceFromMarking(place); |
2412 | |
2413 | === modified file 'src/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java' |
2414 | --- src/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java 2019-03-22 13:57:03 +0000 |
2415 | +++ src/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java 2020-07-09 12:55:48 +0000 |
2416 | @@ -15,16 +15,16 @@ |
2417 | import dk.aau.cs.verification.TAPNComposer; |
2418 | |
2419 | public class TimedArcPetriNetNetwork { |
2420 | - private List<TimedArcPetriNet> tapns = new ArrayList<TimedArcPetriNet>(); |
2421 | - private List<SharedPlace> sharedPlaces = new ArrayList<SharedPlace>(); |
2422 | - private List<SharedTransition> sharedTransitions = new ArrayList<SharedTransition>(); |
2423 | + private final List<TimedArcPetriNet> tapns = new ArrayList<TimedArcPetriNet>(); |
2424 | + private final List<SharedPlace> sharedPlaces = new ArrayList<SharedPlace>(); |
2425 | + private final List<SharedTransition> sharedTransitions = new ArrayList<SharedTransition>(); |
2426 | |
2427 | - private NetworkMarking currentMarking; |
2428 | - private ConstantStore constants; |
2429 | + private NetworkMarking currentMarking = new NetworkMarking(); |
2430 | + private final ConstantStore constants; |
2431 | |
2432 | private int defaultBound = 3; |
2433 | |
2434 | - private List<ConstantsListener> constantsListeners = new ArrayList<ConstantsListener>(); |
2435 | + private final List<ConstantsListener> constantsListeners = new ArrayList<ConstantsListener>(); |
2436 | |
2437 | private boolean paintNet = true; |
2438 | |
2439 | @@ -34,8 +34,7 @@ |
2440 | |
2441 | public TimedArcPetriNetNetwork(ConstantStore constants){ |
2442 | this.constants = constants; |
2443 | - currentMarking = new NetworkMarking(); |
2444 | - buildConstraints(); |
2445 | + buildConstraints(); |
2446 | } |
2447 | |
2448 | public void addConstantsListener(ConstantsListener listener){ |
2449 | |
2450 | === modified file 'src/dk/aau/cs/model/tapn/TimedInhibitorArc.java' |
2451 | --- src/dk/aau/cs/model/tapn/TimedInhibitorArc.java 2012-09-19 18:15:59 +0000 |
2452 | +++ src/dk/aau/cs/model/tapn/TimedInhibitorArc.java 2020-07-09 12:55:48 +0000 |
2453 | @@ -14,8 +14,12 @@ |
2454 | public TimedInhibitorArc(TimedPlace source, TimedTransition destination, TimeInterval interval, Weight weight) { |
2455 | super(source, destination, TimeInterval.ZERO_INF, weight); |
2456 | } |
2457 | - |
2458 | - public List<TimeInterval> getDEnabledInterval(){ |
2459 | + |
2460 | + public TimedInhibitorArc(TimedPlace source, TimedTransition destination) { |
2461 | + this(source, destination, TimeInterval.ZERO_INF, new IntWeight(1)); |
2462 | + } |
2463 | + |
2464 | + public List<TimeInterval> getDEnabledInterval(){ |
2465 | if(source().tokens().size() < getWeight().value()){ |
2466 | return Arrays.asList(new TimeInterval(true, new RatBound(BigDecimal.ZERO), Bound.Infinity, false)); |
2467 | } else { |
2468 | |
2469 | === modified file 'src/dk/aau/cs/model/tapn/TimedPlace.java' |
2470 | --- src/dk/aau/cs/model/tapn/TimedPlace.java 2020-06-03 12:16:19 +0000 |
2471 | +++ src/dk/aau/cs/model/tapn/TimedPlace.java 2020-07-09 12:55:48 +0000 |
2472 | @@ -1,13 +1,24 @@ |
2473 | package dk.aau.cs.model.tapn; |
2474 | |
2475 | +import java.math.BigDecimal; |
2476 | import java.util.ArrayList; |
2477 | import java.util.List; |
2478 | +import java.util.regex.Pattern; |
2479 | |
2480 | +import dk.aau.cs.model.tapn.event.TimedPlaceEvent; |
2481 | import dk.aau.cs.model.tapn.event.TimedPlaceListener; |
2482 | import dk.aau.cs.util.Require; |
2483 | import dk.aau.cs.util.Tuple; |
2484 | |
2485 | public abstract class TimedPlace { |
2486 | + |
2487 | + protected static final Pattern namePattern = Pattern.compile("^[a-zA-Z_][a-zA-Z0-9_]*$"); |
2488 | + protected final List<TimedPlaceListener> listeners = new ArrayList<TimedPlaceListener>(); |
2489 | + protected Tuple<PlaceType, Integer> extrapolation = new Tuple<PlaceType, Integer>(PlaceType.Dead, -2); |
2490 | + protected String name; |
2491 | + protected TimeInvariant invariant; |
2492 | + protected TimedMarking currentMarking; |
2493 | + |
2494 | private SharedPlace sharedPlace; |
2495 | private List<TimedOutputArc> postset = new ArrayList<TimedOutputArc>(); |
2496 | private List<TimedInputArc> preset = new ArrayList<TimedInputArc>(); |
2497 | @@ -17,28 +28,67 @@ |
2498 | public enum PlaceType{ |
2499 | Standard, Invariant, Dead |
2500 | } |
2501 | - |
2502 | - public abstract void addTimedPlaceListener(TimedPlaceListener listener); |
2503 | - public abstract void removeTimedPlaceListener(TimedPlaceListener listener); |
2504 | |
2505 | public abstract boolean isShared(); |
2506 | |
2507 | - public abstract String name(); |
2508 | - public abstract void setName(String newName); |
2509 | - |
2510 | - public abstract TimeInvariant invariant(); |
2511 | - public abstract void setInvariant(TimeInvariant invariant); |
2512 | - |
2513 | - public abstract List<TimedToken> tokens(); |
2514 | - public abstract int numberOfTokens(); |
2515 | - |
2516 | - public abstract void setCurrentMarking(TimedMarking marking); |
2517 | - |
2518 | - public abstract void addToken(TimedToken timedToken); |
2519 | - public abstract void addTokens(Iterable<TimedToken> tokens); |
2520 | - |
2521 | - public abstract void removeToken(TimedToken timedToken); |
2522 | - public abstract void removeToken(); |
2523 | + public String name() { |
2524 | + return name; |
2525 | + } |
2526 | + |
2527 | + public void setName(String newName) { |
2528 | + Require.that(newName != null && !newName.isEmpty(), "A timed place must have a name"); |
2529 | + Require.that(isValid(newName) && !newName.toLowerCase().equals("true") && !newName.toLowerCase().equals("false"), "The specified name must conform to the pattern [a-zA-Z_][a-zA-Z0-9_]*"); |
2530 | + this.name = newName; |
2531 | + fireNameChanged(); |
2532 | + } |
2533 | + |
2534 | + public TimeInvariant invariant(){ |
2535 | + return invariant; |
2536 | + } |
2537 | + |
2538 | + public List<TimedToken> tokens() { |
2539 | + return currentMarking.getTokensFor(this); |
2540 | + } |
2541 | + |
2542 | + public int numberOfTokens() { |
2543 | + return tokens().size(); |
2544 | + } |
2545 | + |
2546 | + public void addToken(TimedToken timedToken) { |
2547 | + Require.that(timedToken != null, "timedToken cannot be null"); |
2548 | + Require.that(timedToken.place().equals(this), "token is located in a different place"); |
2549 | + |
2550 | + currentMarking.add(timedToken); |
2551 | + fireMarkingChanged(); |
2552 | + } |
2553 | + |
2554 | + public void addTokens(Iterable<TimedToken> tokens) { |
2555 | + Require.that(tokens != null, "tokens cannot be null"); |
2556 | + |
2557 | + for(TimedToken token : tokens){ |
2558 | + currentMarking.add(token); // avoid firing marking changed on every add |
2559 | + } |
2560 | + fireMarkingChanged(); |
2561 | + } |
2562 | + |
2563 | + public void addTokens(int numberOfTokensToAdd) { |
2564 | + for (int i = 0; i < numberOfTokensToAdd; i++) { |
2565 | + addToken(new TimedToken(this, BigDecimal.ZERO)); |
2566 | + } |
2567 | + } |
2568 | + |
2569 | + public void removeTokens(int numberOfTokensToRemove) { |
2570 | + for (int i = 0; i < numberOfTokensToRemove; i++) { |
2571 | + removeToken(); |
2572 | + } |
2573 | + } |
2574 | + |
2575 | + public void removeToken() { |
2576 | + if (numberOfTokens() > 0) { |
2577 | + currentMarking.remove(tokens().get(0)); |
2578 | + fireMarkingChanged(); |
2579 | + } |
2580 | + } |
2581 | |
2582 | public abstract Tuple<PlaceType, Integer> extrapolate(); |
2583 | |
2584 | @@ -65,6 +115,51 @@ |
2585 | return name() == other.name(); |
2586 | } |
2587 | |
2588 | + |
2589 | + protected void fireMarkingChanged() { |
2590 | + for(TimedPlaceListener listener : listeners){ |
2591 | + listener.markingChanged(new TimedPlaceEvent(this)); |
2592 | + } |
2593 | + } |
2594 | + |
2595 | + protected void fireNameChanged() { |
2596 | + for(TimedPlaceListener listener : listeners){ |
2597 | + listener.nameChanged(new TimedPlaceEvent(this)); |
2598 | + } |
2599 | + } |
2600 | + |
2601 | + protected void fireInvariantChanged() { |
2602 | + for(TimedPlaceListener listener : listeners){ |
2603 | + listener.invariantChanged(new TimedPlaceEvent(this)); |
2604 | + } |
2605 | + } |
2606 | + |
2607 | + protected boolean isValid(String newName) { |
2608 | + return namePattern.matcher(newName).matches(); |
2609 | + } |
2610 | + |
2611 | + public void setInvariant(TimeInvariant invariant) { |
2612 | + Require.that(invariant != null, "invariant must not be null"); |
2613 | + this.invariant = invariant; |
2614 | + fireInvariantChanged(); |
2615 | + } |
2616 | + |
2617 | + public void addTimedPlaceListener(TimedPlaceListener listener) { |
2618 | + Require.that(listener != null, "Listener cannot be null"); |
2619 | + listeners.add(listener); |
2620 | + } |
2621 | + |
2622 | + public void removeTimedPlaceListener(TimedPlaceListener listener) { |
2623 | + Require.that(listener != null, "Listener cannot be null"); |
2624 | + listeners.remove(listener); |
2625 | + } |
2626 | + |
2627 | + public void setCurrentMarking(TimedMarking marking) { |
2628 | + Require.that(marking != null, "marking cannot be null"); |
2629 | + currentMarking = marking; |
2630 | + fireMarkingChanged(); |
2631 | + } |
2632 | + |
2633 | public boolean isOrphan() { |
2634 | return presetSize() == 0 && postsetSize() == 0; |
2635 | } |
2636 | @@ -112,16 +207,4 @@ |
2637 | return postset.size() + transportArcs.size() + inhibitorArcs.size(); |
2638 | } |
2639 | |
2640 | -// public abstract void addInhibitorArc(TimedInhibitorArc arc); |
2641 | -// public abstract void addToPreset(TransportArc arc); |
2642 | -// public abstract void addToPreset(TimedOutputArc arc); |
2643 | -// public abstract void addToPostset(TransportArc arc); |
2644 | -// public abstract void addToPostset(TimedInputArc arc); |
2645 | -// |
2646 | -// public abstract void removeFromPostset(TimedInputArc arc); |
2647 | -// public abstract void removeFromPostset(TransportArc arc); |
2648 | -// public abstract void removeFromPreset(TransportArc arc); |
2649 | -// public abstract void removeFromPreset(TimedOutputArc arc); |
2650 | -// public abstract void removeInhibitorArc(TimedInhibitorArc arc); |
2651 | - |
2652 | } |
2653 | \ No newline at end of file |
2654 | |
2655 | === modified file 'src/dk/aau/cs/model/tapn/TimedToken.java' |
2656 | --- src/dk/aau/cs/model/tapn/TimedToken.java 2019-03-23 07:51:29 +0000 |
2657 | +++ src/dk/aau/cs/model/tapn/TimedToken.java 2020-07-09 12:55:48 +0000 |
2658 | @@ -31,8 +31,7 @@ |
2659 | } |
2660 | |
2661 | public TimedToken clone() { |
2662 | - return new TimedToken(place, age); // age is immutable so ok to pass it |
2663 | - // to constructor |
2664 | + return new TimedToken(place, age); // age is immutable so ok to pass it to constructor |
2665 | } |
2666 | |
2667 | public TimedToken delay(BigDecimal delay) { |
2668 | @@ -44,12 +43,7 @@ |
2669 | DecimalFormat df = new DecimalFormat(); |
2670 | df.setMaximumFractionDigits(Pipe.AGE_DECIMAL_PRECISION); |
2671 | |
2672 | - StringBuilder buffer = new StringBuilder("("); |
2673 | - buffer.append(place.toString()); |
2674 | - buffer.append(", "); |
2675 | - buffer.append(df.format(age)); |
2676 | - buffer.append(')'); |
2677 | - return buffer.toString(); |
2678 | + return String.format("(%s, %s)", place.toString(), df.format(age)); |
2679 | } |
2680 | |
2681 | @Override |
2682 | |
2683 | === modified file 'src/dk/aau/cs/model/tapn/TimedTransition.java' |
2684 | --- src/dk/aau/cs/model/tapn/TimedTransition.java 2020-06-18 20:57:07 +0000 |
2685 | +++ src/dk/aau/cs/model/tapn/TimedTransition.java 2020-07-09 12:55:48 +0000 |
2686 | @@ -17,16 +17,16 @@ |
2687 | private static final Pattern namePattern = Pattern.compile("^[a-zA-Z_][a-zA-Z0-9_]*$"); |
2688 | |
2689 | private String name; |
2690 | - private List<TimedOutputArc> postset = new ArrayList<TimedOutputArc>(); |
2691 | - private List<TimedInputArc> preset = new ArrayList<TimedInputArc>(); |
2692 | - private List<TransportArc> transportArcsGoingThrough = new ArrayList<TransportArc>(); |
2693 | - private List<TimedInhibitorArc> inhibitorArcs = new ArrayList<TimedInhibitorArc>(); |
2694 | + private final List<TimedOutputArc> postset = new ArrayList<TimedOutputArc>(); |
2695 | + private final List<TimedInputArc> preset = new ArrayList<TimedInputArc>(); |
2696 | + private final List<TransportArc> transportArcsGoingThrough = new ArrayList<TransportArc>(); |
2697 | + private final List<TimedInhibitorArc> inhibitorArcs = new ArrayList<TimedInhibitorArc>(); |
2698 | private TimeInterval dInterval = null; |
2699 | private boolean isUrgent = false; |
2700 | |
2701 | private SharedTransition sharedTransition; |
2702 | |
2703 | - private List<TimedTransitionListener> listeners = new ArrayList<TimedTransitionListener>(); |
2704 | + private final List<TimedTransitionListener> listeners = new ArrayList<TimedTransitionListener>(); |
2705 | |
2706 | public TimedTransition(String name) { |
2707 | this(name, false); |
2708 | |
2709 | === modified file 'src/dk/aau/cs/model/tapn/TransportArc.java' |
2710 | --- src/dk/aau/cs/model/tapn/TransportArc.java 2018-05-13 19:54:55 +0000 |
2711 | +++ src/dk/aau/cs/model/tapn/TransportArc.java 2020-07-09 12:55:48 +0000 |
2712 | @@ -36,8 +36,12 @@ |
2713 | setTimeInterval(interval); |
2714 | this.weight = weight; |
2715 | } |
2716 | - |
2717 | - public Weight getWeight(){ |
2718 | + |
2719 | + public TransportArc(TimedPlace source, TimedTransition transitions, TimedPlace destination) { |
2720 | + this(source, transitions, destination, TimeInterval.ZERO_INF); |
2721 | + } |
2722 | + |
2723 | + public Weight getWeight(){ |
2724 | return weight; |
2725 | } |
2726 | |
2727 | |
2728 | === modified file 'src/net/tapaal/gui/DrawingSurfaceManager/AbstractDrawingSurfaceManager.java' |
2729 | --- src/net/tapaal/gui/DrawingSurfaceManager/AbstractDrawingSurfaceManager.java 2020-04-18 14:41:05 +0000 |
2730 | +++ src/net/tapaal/gui/DrawingSurfaceManager/AbstractDrawingSurfaceManager.java 2020-07-09 12:55:48 +0000 |
2731 | @@ -1,5 +1,7 @@ |
2732 | package net.tapaal.gui.DrawingSurfaceManager; |
2733 | |
2734 | +import pipe.gui.canvas.DrawingSurfaceImpl; |
2735 | +import pipe.gui.graphicElements.GraphicalElement; |
2736 | import pipe.gui.graphicElements.PetriNetObject; |
2737 | |
2738 | import java.awt.event.MouseEvent; |
2739 | @@ -11,6 +13,8 @@ |
2740 | |
2741 | public abstract class AbstractDrawingSurfaceManager { |
2742 | |
2743 | + protected DrawingSurfaceImpl canvas; |
2744 | + |
2745 | public void drawingSurfaceMouseClicked(MouseEvent e) {} |
2746 | public void drawingSurfaceMousePressed(MouseEvent e) {} |
2747 | public void drawingSurfaceMouseReleased(MouseEvent e){} |
2748 | @@ -20,6 +24,8 @@ |
2749 | |
2750 | public enum MouseAction { |
2751 | clicked, |
2752 | + doubleClicked, |
2753 | + rightClicked, |
2754 | pressed, |
2755 | released, |
2756 | dragged, |
2757 | @@ -31,12 +37,12 @@ |
2758 | public static class DrawingSurfaceEvent { |
2759 | |
2760 | |
2761 | - public final PetriNetObject pno; |
2762 | + public final GraphicalElement pno; |
2763 | public final MouseEvent e; |
2764 | public final MouseAction a; |
2765 | //Mouse Event type eg click mouse over etc |
2766 | |
2767 | - public DrawingSurfaceEvent(PetriNetObject pno, MouseEvent e, MouseAction a) { |
2768 | + public DrawingSurfaceEvent(GraphicalElement pno, MouseEvent e, MouseAction a) { |
2769 | this.pno = pno; |
2770 | this.e = e; |
2771 | this.a = a; |
2772 | @@ -47,8 +53,12 @@ |
2773 | private final Map<Predicate<DrawingSurfaceEvent>, Consumer<DrawingSurfaceEvent>> filter = new LinkedHashMap<>(); |
2774 | private final AbstractDrawingSurfaceManager next = null; |
2775 | |
2776 | - public void registerManager(){} |
2777 | - public void deregisterManager(){} |
2778 | + public void registerManager(DrawingSurfaceImpl canvas){ |
2779 | + this.canvas = canvas; |
2780 | + } |
2781 | + public void deregisterManager(){ |
2782 | + this.canvas = null; |
2783 | + } |
2784 | |
2785 | public AbstractDrawingSurfaceManager() { |
2786 | registerEvents(); |
2787 | |
2788 | === added file 'src/net/tapaal/swinghelpers/DispatchEventsToParentHandler.java' |
2789 | --- src/net/tapaal/swinghelpers/DispatchEventsToParentHandler.java 1970-01-01 00:00:00 +0000 |
2790 | +++ src/net/tapaal/swinghelpers/DispatchEventsToParentHandler.java 2020-07-09 12:55:48 +0000 |
2791 | @@ -0,0 +1,58 @@ |
2792 | +package net.tapaal.swinghelpers; |
2793 | + |
2794 | +import javax.swing.*; |
2795 | +import java.awt.*; |
2796 | +import java.awt.event.*; |
2797 | + |
2798 | +public final class DispatchEventsToParentHandler implements MouseListener, MouseWheelListener, MouseMotionListener { |
2799 | + |
2800 | + private static void dispatchEventToParent(MouseEvent e) { |
2801 | + if(e.getSource() instanceof Component) { |
2802 | + Component c = ((Component) e.getSource()); |
2803 | + if (c.getParent() != null) { |
2804 | + SwingUtilities.convertPoint(c, e.getPoint(), c.getParent()); |
2805 | + c.getParent().dispatchEvent(e); |
2806 | + } |
2807 | + } |
2808 | + } |
2809 | + |
2810 | + @Override |
2811 | + public final void mouseClicked(MouseEvent e) { |
2812 | + dispatchEventToParent(e); |
2813 | + } |
2814 | + |
2815 | + @Override |
2816 | + public final void mousePressed(MouseEvent e) { |
2817 | + dispatchEventToParent(e); |
2818 | + } |
2819 | + |
2820 | + @Override |
2821 | + public final void mouseReleased(MouseEvent e) { |
2822 | + dispatchEventToParent(e); |
2823 | + } |
2824 | + |
2825 | + @Override |
2826 | + public final void mouseEntered(MouseEvent e) { |
2827 | + dispatchEventToParent(e); |
2828 | + } |
2829 | + |
2830 | + @Override |
2831 | + public final void mouseExited(MouseEvent e) { |
2832 | + dispatchEventToParent(e); |
2833 | + } |
2834 | + |
2835 | + @Override |
2836 | + public final void mouseDragged(MouseEvent e) { |
2837 | + dispatchEventToParent(e); |
2838 | + } |
2839 | + |
2840 | + @Override |
2841 | + public final void mouseMoved(MouseEvent e) { |
2842 | + dispatchEventToParent(e); |
2843 | + } |
2844 | + |
2845 | + @Override |
2846 | + public final void mouseWheelMoved(MouseWheelEvent e) { |
2847 | + dispatchEventToParent(e); |
2848 | + } |
2849 | +} |
2850 | |
2851 | === modified file 'src/pipe/dataLayer/DataLayer.java' |
2852 | --- src/pipe/dataLayer/DataLayer.java 2020-05-18 10:06:28 +0000 |
2853 | +++ src/pipe/dataLayer/DataLayer.java 2020-07-09 12:55:48 +0000 |
2854 | @@ -29,36 +29,36 @@ |
2855 | //migth not be best solution long term. |
2856 | private void removeFromViewIfConnected(PetriNetObject pno) { |
2857 | if (view != null) { |
2858 | - view.removePetriNetObject(pno); |
2859 | + view.removePetriNetObject(pno.getGraphicalElement()); |
2860 | } |
2861 | } |
2862 | |
2863 | private void addToViewIfConnected(PetriNetObject pno) { |
2864 | if (view != null) { |
2865 | - view.addNewPetriNetObject(pno); |
2866 | + view.addNewPetriNetObject(pno.getGraphicalElement()); |
2867 | } |
2868 | } |
2869 | |
2870 | /** PNML File Name */ |
2871 | public String pnmlName = null; |
2872 | /** List containing all the Place objects in the Petri-Net */ |
2873 | - private ArrayList<Place> placesArray = null; |
2874 | + private final ArrayList<Place> placesArray = new ArrayList<Place>(); |
2875 | /** ArrayList containing all the Transition objects in the Petri-Net */ |
2876 | - private ArrayList<Transition> transitionsArray = null; |
2877 | + private final ArrayList<Transition> transitionsArray = new ArrayList<Transition>(); |
2878 | /** ArrayList containing all the Arc objects in the Petri-Net */ |
2879 | - private ArrayList<Arc> arcsArray = null; |
2880 | + private final ArrayList<Arc> arcsArray = new ArrayList<Arc>(); |
2881 | |
2882 | /** Set holding all ArcPathPoints |
2883 | * Uses the reference as lookup key (not hash code) |
2884 | * Collections.newSetFromMap(new IdentityHashMap<E, Boolean>()); |
2885 | * */ |
2886 | - private Set<ArcPathPoint> arcPathSet = Collections.newSetFromMap(new IdentityHashMap<>()); |
2887 | + private final Set<ArcPathPoint> arcPathSet = Collections.newSetFromMap(new IdentityHashMap<>()); |
2888 | |
2889 | /** |
2890 | * ArrayList for net-level label objects (as opposed to element-level |
2891 | * labels). |
2892 | */ |
2893 | - private ArrayList<AnnotationNote> labelsArray = null; |
2894 | + private final ArrayList<AnnotationNote> labelsArray = new ArrayList<AnnotationNote>(); |
2895 | |
2896 | /** |
2897 | * An ArrayList used to point to either the Arc, Place or Transition |
2898 | @@ -66,22 +66,23 @@ |
2899 | */ |
2900 | private ArrayList<? extends PetriNetObject> changeArrayList = null; |
2901 | |
2902 | - /** |
2903 | + // may as well do the hashtable here as well |
2904 | + /** |
2905 | * Hashtable which maps PlaceTransitionObjects to their list of connected |
2906 | * arcs |
2907 | */ |
2908 | - private Hashtable<PlaceTransitionObject, ArrayList<TimedOutputArcComponent>> arcsMap = null; |
2909 | + private final Hashtable<PlaceTransitionObject, ArrayList<TimedOutputArcComponent>> arcsMap = new Hashtable<PlaceTransitionObject, ArrayList<TimedOutputArcComponent>>(); |
2910 | |
2911 | /** |
2912 | * Hashtable which maps PlaceTransitionObjects to their list of connected |
2913 | * arcs |
2914 | */ |
2915 | - private Hashtable<PlaceTransitionObject, ArrayList<TimedInhibitorArcComponent>> tapnInhibitorsMap = null; |
2916 | + private final Hashtable<PlaceTransitionObject, ArrayList<TimedInhibitorArcComponent>> tapnInhibitorsMap = new Hashtable<PlaceTransitionObject, ArrayList<TimedInhibitorArcComponent>>(); |
2917 | |
2918 | |
2919 | //XXX: Added from drawingsurface to have a way to acces all elements added, |
2920 | //Should be refactored later to combine the existing list, however this is the quick fix during refactoring |
2921 | - private ArrayList<PetriNetObject> petriNetObjects = new ArrayList<PetriNetObject>(); |
2922 | + private final ArrayList<PetriNetObject> petriNetObjects = new ArrayList<PetriNetObject>(); |
2923 | |
2924 | public ArrayList<PetriNetObject> getPNObjects() { |
2925 | return petriNetObjects; |
2926 | @@ -101,16 +102,8 @@ |
2927 | * Create empty Petri-Net object |
2928 | */ |
2929 | public DataLayer() { |
2930 | - placesArray = new ArrayList<Place>(); |
2931 | - transitionsArray = new ArrayList<Transition>(); |
2932 | - arcsArray = new ArrayList<Arc>(); |
2933 | - |
2934 | - labelsArray = new ArrayList<AnnotationNote>(); |
2935 | - |
2936 | - // may as well do the hashtable here as well |
2937 | - arcsMap = new Hashtable<PlaceTransitionObject, ArrayList<TimedOutputArcComponent>>(); |
2938 | - tapnInhibitorsMap = new Hashtable<PlaceTransitionObject, ArrayList<TimedInhibitorArcComponent>>(); |
2939 | - } |
2940 | + super(); |
2941 | + } |
2942 | |
2943 | |
2944 | /** |
2945 | @@ -162,105 +155,94 @@ |
2946 | |
2947 | // Check if the arcs have a valid source and target |
2948 | if (arcInput.getSource() == null || arcInput.getTarget() == null) { |
2949 | - System.err.println(("Cant add arc" + arcInput + " where source: " |
2950 | + System.err.println( |
2951 | + "Cant add arc" + arcInput + " where source: " |
2952 | + arcInput.getSource() + " or target: " |
2953 | - + arcInput.getTarget() + " is null")); |
2954 | + + arcInput.getTarget() + " is null" |
2955 | + ); |
2956 | return; |
2957 | } |
2958 | |
2959 | - if (arcInput != null) { |
2960 | - if (arcInput.getId() != null && arcInput.getId().length() > 0) { |
2961 | - for (int i = 0; i < arcsArray.size(); i++) { |
2962 | - if (arcInput.getId().equals((arcsArray.get(i)).getId())) { |
2963 | - unique = false; |
2964 | - } |
2965 | - } |
2966 | - } else { |
2967 | - String id = null; |
2968 | - if (arcsArray != null && arcsArray.size() > 0) { |
2969 | - int no = arcsArray.size(); |
2970 | - do { |
2971 | - for (int i = 0; i < arcsArray.size(); i++) { |
2972 | - id = "A" + no; |
2973 | - if (arcsArray.get(i) != null) { |
2974 | - if (id.equals((arcsArray.get(i)).getId())) { |
2975 | - unique = false; |
2976 | - no++; |
2977 | - } else { |
2978 | - unique = true; |
2979 | - } |
2980 | - } |
2981 | - } |
2982 | - } while (!unique); |
2983 | - } else { |
2984 | - id = "A0"; |
2985 | - } |
2986 | - if (id != null) { |
2987 | - arcInput.setId(id); |
2988 | - } else { |
2989 | - arcInput.setId("error"); |
2990 | - } |
2991 | - } |
2992 | - |
2993 | - //XXX: this is still nedede as nets loaded from file (XML/tapn) does not set connectedTo correctly //2019-09-18 |
2994 | - // Transportarc fix boddy |
2995 | - if (arcInput instanceof TimedTransportArcComponent) { |
2996 | - TimedTransportArcComponent tmp = (TimedTransportArcComponent) arcInput; |
2997 | - PlaceTransitionObject first = tmp.getSource(); |
2998 | - |
2999 | - if (tmp.getConnectedTo() == null) { |
3000 | - if (first instanceof TimedPlaceComponent) { |
3001 | - |
3002 | - for (Object o : tmp.getTarget().getPostset()) { |
3003 | - |
3004 | - if (o instanceof TimedTransportArcComponent) { |
3005 | - if (tmp.getGroupNr() == ((TimedTransportArcComponent) o) |
3006 | - .getGroupNr()) { |
3007 | - // Found partner |
3008 | - |
3009 | - tmp |
3010 | - .setConnectedTo(((TimedTransportArcComponent) o)); |
3011 | - ((TimedTransportArcComponent) o) |
3012 | - .setConnectedTo(tmp); |
3013 | - |
3014 | - break; |
3015 | - } |
3016 | - } |
3017 | - |
3018 | - } |
3019 | - |
3020 | - } else { |
3021 | - // First is TimedTransition |
3022 | - tmp = (TimedTransportArcComponent) arcInput; |
3023 | - |
3024 | - for (Object o : tmp.getSource().getPreset()) { |
3025 | - |
3026 | - if (o instanceof TimedTransportArcComponent) { |
3027 | - if (tmp.getGroupNr() == ((TimedTransportArcComponent) o) |
3028 | - .getGroupNr()) { |
3029 | - // Found partner |
3030 | - |
3031 | - tmp |
3032 | - .setConnectedTo(((TimedTransportArcComponent) o)); |
3033 | - ((TimedTransportArcComponent) o) |
3034 | - .setConnectedTo(tmp); |
3035 | - |
3036 | - break; |
3037 | - } |
3038 | - } |
3039 | - |
3040 | - } |
3041 | - |
3042 | - } |
3043 | - } |
3044 | - |
3045 | - } |
3046 | - |
3047 | - arcsArray.add(arcInput); |
3048 | - addArcToArcsMap(arcInput); |
3049 | - |
3050 | - } |
3051 | - } |
3052 | + if (arcInput.getId() != null && arcInput.getId().length() > 0) { |
3053 | + for (Arc arc : arcsArray) { |
3054 | + if (arcInput.getId().equals(arc.getId())) { |
3055 | + unique = false; |
3056 | + } |
3057 | + } |
3058 | + } else { |
3059 | + String id = null; |
3060 | + if (arcsArray.size() > 0) { |
3061 | + int no = arcsArray.size(); |
3062 | + do { |
3063 | + for (Arc arc : arcsArray) { |
3064 | + id = "A" + no; |
3065 | + if (arc != null) { |
3066 | + if (id.equals(arc.getId())) { |
3067 | + unique = false; |
3068 | + no++; |
3069 | + } else { |
3070 | + unique = true; |
3071 | + } |
3072 | + } |
3073 | + } |
3074 | + } while (!unique); |
3075 | + } else { |
3076 | + id = "A0"; |
3077 | + } |
3078 | + arcInput.setId(id); |
3079 | + } |
3080 | + |
3081 | + //XXX: this is still nedede as nets loaded from file (XML/tapn) does not set connectedTo correctly //2019-09-18 |
3082 | + // Transportarc fix boddy |
3083 | + if (arcInput instanceof TimedTransportArcComponent) { |
3084 | + TimedTransportArcComponent tmp = (TimedTransportArcComponent) arcInput; |
3085 | + PlaceTransitionObject first = tmp.getSource(); |
3086 | + |
3087 | + if (tmp.getConnectedTo() == null) { |
3088 | + if (first instanceof TimedPlaceComponent) { |
3089 | + |
3090 | + for (Object o : tmp.getTarget().getPostset()) { |
3091 | + |
3092 | + if (o instanceof TimedTransportArcComponent) { |
3093 | + if (tmp.getGroupNr() == ((TimedTransportArcComponent) o).getGroupNr()) { |
3094 | + // Found partner |
3095 | + |
3096 | + tmp.setConnectedTo(((TimedTransportArcComponent) o)); |
3097 | + ((TimedTransportArcComponent) o).setConnectedTo(tmp); |
3098 | + |
3099 | + break; |
3100 | + } |
3101 | + } |
3102 | + |
3103 | + } |
3104 | + |
3105 | + } else { |
3106 | + // First is TimedTransition |
3107 | + |
3108 | + for (Object o : tmp.getSource().getPreset()) { |
3109 | + |
3110 | + if (o instanceof TimedTransportArcComponent) { |
3111 | + if (tmp.getGroupNr() == ((TimedTransportArcComponent) o).getGroupNr()) { |
3112 | + // Found partner |
3113 | + |
3114 | + tmp.setConnectedTo(((TimedTransportArcComponent) o)); |
3115 | + ((TimedTransportArcComponent) o).setConnectedTo(tmp); |
3116 | + |
3117 | + break; |
3118 | + } |
3119 | + } |
3120 | + |
3121 | + } |
3122 | + |
3123 | + } |
3124 | + } |
3125 | + |
3126 | + } |
3127 | + |
3128 | + arcsArray.add(arcInput); |
3129 | + addArcToArcsMap(arcInput); |
3130 | + |
3131 | + } |
3132 | |
3133 | private void addTransportArc(TimedTransportArcComponent transportArc) { |
3134 | arcsArray.add(transportArc); |
3135 | @@ -271,40 +253,34 @@ |
3136 | boolean unique = true; |
3137 | |
3138 | if (inhibitorArcInput != null) { |
3139 | - if (inhibitorArcInput.getId() != null |
3140 | - && inhibitorArcInput.getId().length() > 0) { |
3141 | - for (int i = 0; i < arcsArray.size(); i++) { |
3142 | - if (inhibitorArcInput.getId().equals( |
3143 | - (arcsArray.get(i)).getId())) { |
3144 | - unique = false; |
3145 | - } |
3146 | - } |
3147 | + if (inhibitorArcInput.getId() != null && inhibitorArcInput.getId().length() > 0) { |
3148 | + for (Arc arc : arcsArray) { |
3149 | + if (inhibitorArcInput.getId().equals(arc.getId())) { |
3150 | + unique = false; |
3151 | + } |
3152 | + } |
3153 | } else { |
3154 | String id = null; |
3155 | - if (arcsArray != null && arcsArray.size() > 0) { |
3156 | + if (arcsArray.size() > 0) { |
3157 | int no = arcsArray.size(); |
3158 | do { |
3159 | - for (int i = 0; i < arcsArray.size(); i++) { |
3160 | - id = "I" + no; |
3161 | - if (arcsArray.get(i) != null) { |
3162 | - if (id.equals((arcsArray.get(i)).getId())) { |
3163 | - unique = false; |
3164 | - no++; |
3165 | - } else { |
3166 | - unique = true; |
3167 | - } |
3168 | - } |
3169 | - } |
3170 | + for (Arc arc : arcsArray) { |
3171 | + id = "I" + no; |
3172 | + if (arc != null) { |
3173 | + if (id.equals(arc.getId())) { |
3174 | + unique = false; |
3175 | + no++; |
3176 | + } else { |
3177 | + unique = true; |
3178 | + } |
3179 | + } |
3180 | + } |
3181 | } while (!unique); |
3182 | } else { |
3183 | id = "I0"; |
3184 | } |
3185 | - if (id != null) { |
3186 | - inhibitorArcInput.setId(id); |
3187 | - } else { |
3188 | - inhibitorArcInput.setId("error"); |
3189 | - } |
3190 | - } |
3191 | + inhibitorArcInput.setId(id); |
3192 | + } |
3193 | |
3194 | arcsArray.add(inhibitorArcInput); |
3195 | addInhibitorArcToInhibitorsMap(inhibitorArcInput); |
3196 | @@ -529,18 +505,13 @@ |
3197 | attached = ((Arc) pnObject).getTarget(); |
3198 | |
3199 | if (attached != null) { |
3200 | - if (tapnInhibitorsMap.get(attached) != null) { // causing |
3201 | - // null |
3202 | - // pointer |
3203 | - // exceptions |
3204 | - // (!) |
3205 | + if (tapnInhibitorsMap.get(attached) != null) { // causing null pointer exceptions (!) |
3206 | tapnInhibitorsMap.get(attached).remove(pnObject); |
3207 | } |
3208 | |
3209 | attached.removeToArc((Arc) pnObject); |
3210 | if (attached instanceof Transition) { |
3211 | - ((Transition) attached) |
3212 | - .removeArcCompareObject((Arc) pnObject); |
3213 | + ((Transition) attached).removeArcCompareObject((Arc) pnObject); |
3214 | } |
3215 | // attached.updateConnected(); //causing null pointer |
3216 | // exceptions (?) |
3217 | @@ -567,10 +538,7 @@ |
3218 | |
3219 | attached = ((Arc) pnObject).getTarget(); |
3220 | if (attached != null) { |
3221 | - if (arcsMap.get(attached) != null) { // causing null |
3222 | - // pointer |
3223 | - // exceptions |
3224 | - // (!) |
3225 | + if (arcsMap.get(attached) != null) { // causing null pointer exceptions (!) |
3226 | arcsMap.get(attached).remove(pnObject); |
3227 | } |
3228 | |
3229 | @@ -586,8 +554,7 @@ |
3230 | |
3231 | } |
3232 | } catch (NullPointerException npe) { |
3233 | - System.out.println("NullPointerException [debug]\n" |
3234 | - + npe.getMessage()); |
3235 | + System.out.println("NullPointerException [debug]\n" + npe.getMessage()); |
3236 | throw npe; |
3237 | } |
3238 | // we reset to null so that the wrong ArrayList can't get added to |
3239 | @@ -599,8 +566,10 @@ |
3240 | * set all enabled transitions to highlighted |
3241 | */ |
3242 | public Iterable<Transition> transitions() { |
3243 | - return transitionsArray; |
3244 | - } |
3245 | + |
3246 | + return transitionsArray; |
3247 | + } |
3248 | + |
3249 | |
3250 | /** |
3251 | * Sets an internal ArrayList according to the class of the object passed |
3252 | @@ -735,16 +704,14 @@ |
3253 | public Transition getTransitionById(String transitionID) { |
3254 | Transition returnTransition = null; |
3255 | |
3256 | - if (transitionsArray != null) { |
3257 | - if (transitionID != null) { |
3258 | - for (Transition transition : transitionsArray) { |
3259 | - if (transitionID.equalsIgnoreCase(transition.getId())) { |
3260 | - returnTransition = transition; |
3261 | - } |
3262 | - } |
3263 | - } |
3264 | - } |
3265 | - return returnTransition; |
3266 | + if (transitionID != null) { |
3267 | + for (Transition transition : transitionsArray) { |
3268 | + if (transitionID.equalsIgnoreCase(transition.getId())) { |
3269 | + returnTransition = transition; |
3270 | + } |
3271 | + } |
3272 | + } |
3273 | + return returnTransition; |
3274 | } |
3275 | |
3276 | /** |
3277 | @@ -758,16 +725,14 @@ |
3278 | public Transition getTransitionByName(String transitionName) { |
3279 | Transition returnTransition = null; |
3280 | |
3281 | - if (transitionsArray != null) { |
3282 | - if (transitionName != null) { |
3283 | - for (Transition transition : transitionsArray) { |
3284 | - if (transitionName.equalsIgnoreCase(transition.getName())) { |
3285 | - returnTransition = transition; |
3286 | - } |
3287 | - } |
3288 | - } |
3289 | - } |
3290 | - return returnTransition; |
3291 | + if (transitionName != null) { |
3292 | + for (Transition transition : transitionsArray) { |
3293 | + if (transitionName.equalsIgnoreCase(transition.getName())) { |
3294 | + returnTransition = transition; |
3295 | + } |
3296 | + } |
3297 | + } |
3298 | + return returnTransition; |
3299 | } |
3300 | |
3301 | /** |
3302 | @@ -780,16 +745,14 @@ |
3303 | public Place getPlaceById(String placeID) { |
3304 | Place returnPlace = null; |
3305 | |
3306 | - if (placesArray != null) { |
3307 | - if (placeID != null) { |
3308 | - for (Place place : placesArray) { |
3309 | - if (placeID.equalsIgnoreCase(place.getId())) { |
3310 | - returnPlace = place; |
3311 | - } |
3312 | - } |
3313 | - } |
3314 | - } |
3315 | - return returnPlace; |
3316 | + if (placeID != null) { |
3317 | + for (Place place : placesArray) { |
3318 | + if (placeID.equalsIgnoreCase(place.getId())) { |
3319 | + returnPlace = place; |
3320 | + } |
3321 | + } |
3322 | + } |
3323 | + return returnPlace; |
3324 | } |
3325 | |
3326 | /** |
3327 | @@ -802,16 +765,14 @@ |
3328 | public Place getPlaceByName(String placeName) { |
3329 | Place returnPlace = null; |
3330 | |
3331 | - if (placesArray != null) { |
3332 | - if (placeName != null) { |
3333 | - for (Place place : placesArray) { |
3334 | - if (placeName.equalsIgnoreCase(place.getName())) { |
3335 | - returnPlace = place; |
3336 | - } |
3337 | - } |
3338 | - } |
3339 | - } |
3340 | - return returnPlace; |
3341 | + if (placeName != null) { |
3342 | + for (Place place : placesArray) { |
3343 | + if (placeName.equalsIgnoreCase(place.getName())) { |
3344 | + returnPlace = place; |
3345 | + } |
3346 | + } |
3347 | + } |
3348 | + return returnPlace; |
3349 | } |
3350 | |
3351 | /** |
3352 | |
3353 | === modified file 'src/pipe/dataLayer/Template.java' |
3354 | --- src/pipe/dataLayer/Template.java 2020-01-12 10:11:08 +0000 |
3355 | +++ src/pipe/dataLayer/Template.java 2020-07-09 12:55:48 +0000 |
3356 | @@ -5,9 +5,9 @@ |
3357 | import dk.aau.cs.util.Require; |
3358 | |
3359 | public class Template { |
3360 | - private TimedArcPetriNet net; |
3361 | - private DataLayer guiModel; |
3362 | - private Zoomer zoomer; |
3363 | + private final TimedArcPetriNet net; |
3364 | + private final DataLayer guiModel; |
3365 | + private final Zoomer zoomer; |
3366 | private boolean hasPositionalInfo = false; |
3367 | |
3368 | public Template(TimedArcPetriNet net, DataLayer guiModel, Zoomer zoomer) { |
3369 | @@ -37,11 +37,6 @@ |
3370 | net.setActive(isActive); |
3371 | } |
3372 | |
3373 | - public void setGuiModel(DataLayer guiModel) { |
3374 | - Require.notNull(guiModel, "GuiModel cannot be null"); |
3375 | - this.guiModel = guiModel; |
3376 | - } |
3377 | - |
3378 | public Template copy() { |
3379 | TimedArcPetriNet tapn = net.copy(); |
3380 | tapn.setName(tapn.name() + "Copy"); |
3381 | |
3382 | === modified file 'src/pipe/gui/AnimationHistoryList.java' |
3383 | --- src/pipe/gui/AnimationHistoryList.java 2020-05-18 11:23:28 +0000 |
3384 | +++ src/pipe/gui/AnimationHistoryList.java 2020-07-09 12:55:48 +0000 |
3385 | @@ -152,7 +152,7 @@ |
3386 | } |
3387 | for (Template t : CreateGui.getCurrentTab().activeTemplates()){ |
3388 | for(Transition trans : t.guiModel().getTransitions()){ |
3389 | - if(trans.isEnabled(true) || trans.isDelayEnabledTransition(true)){ |
3390 | + if(trans.isTransitionEnabled() || trans.isDelayEnabled()){ |
3391 | return; |
3392 | } |
3393 | } |
3394 | |
3395 | === modified file 'src/pipe/gui/Animator.java' |
3396 | --- src/pipe/gui/Animator.java 2020-05-25 07:16:04 +0000 |
3397 | +++ src/pipe/gui/Animator.java 2020-07-09 12:55:48 +0000 |
3398 | @@ -39,659 +39,648 @@ |
3399 | import dk.aau.cs.verification.VerifyTAPN.TraceType; |
3400 | |
3401 | public class Animator { |
3402 | - private final ArrayList<TAPNNetworkTraceStep> actionHistory = new ArrayList<TAPNNetworkTraceStep>(); |
3403 | - private int currentAction; |
3404 | - private final ArrayList<NetworkMarking> markings = new ArrayList<NetworkMarking>(); |
3405 | - private int currentMarkingIndex = 0; |
3406 | - private TAPNNetworkTrace trace = null; |
3407 | - |
3408 | - public FiringMode firingmode = new RandomFiringMode(); |
3409 | - private TabContent tab; |
3410 | - private NetworkMarking initialMarking; |
3411 | - |
3412 | - private boolean isDisplayingUntimedTrace = false; |
3413 | - private static boolean isUrgentTransitionEnabled = false; |
3414 | - |
3415 | - public static boolean isUrgentTransitionEnabled(){ |
3416 | - return isUrgentTransitionEnabled; |
3417 | - } |
3418 | - |
3419 | - public Animator(TabContent tab) { |
3420 | - currentAction = -1; |
3421 | - setTabContent(tab); |
3422 | - } |
3423 | - |
3424 | - private void setTabContent(TabContent tab) { |
3425 | - this.tab = tab; |
3426 | - } |
3427 | - |
3428 | - private NetworkMarking currentMarking() { |
3429 | - return markings.get(currentMarkingIndex); |
3430 | - } |
3431 | - |
3432 | - public void setTrace(TAPNNetworkTrace trace) { |
3433 | + private final ArrayList<TAPNNetworkTraceStep> actionHistory = new ArrayList<TAPNNetworkTraceStep>(); |
3434 | + private int currentAction = -1; |
3435 | + private final ArrayList<NetworkMarking> markings = new ArrayList<NetworkMarking>(); |
3436 | + private int currentMarkingIndex = 0; |
3437 | + private TAPNNetworkTrace trace = null; |
3438 | + |
3439 | + public FiringMode firingmode = new RandomFiringMode(); |
3440 | + private final TabContent tab; |
3441 | + private NetworkMarking initialMarking; |
3442 | + |
3443 | + private boolean isDisplayingUntimedTrace = false; |
3444 | + private static boolean isUrgentTransitionEnabled = false; |
3445 | + |
3446 | + public static boolean isUrgentTransitionEnabled(){ |
3447 | + return isUrgentTransitionEnabled; |
3448 | + } |
3449 | + |
3450 | + public Animator(TabContent tab) { |
3451 | + super(); |
3452 | + |
3453 | + this.tab = tab; |
3454 | + } |
3455 | + |
3456 | + private NetworkMarking currentMarking() { |
3457 | + return markings.get(currentMarkingIndex); |
3458 | + } |
3459 | + |
3460 | + public void setTrace(TAPNNetworkTrace trace) { |
3461 | CreateGui.getCurrentTab().setAnimationMode(true); |
3462 | |
3463 | - if (trace.isConcreteTrace()) { |
3464 | - this.trace = trace; |
3465 | - setTimedTrace(trace); |
3466 | - } else { |
3467 | - setUntimedTrace(trace); |
3468 | - isDisplayingUntimedTrace = true; |
3469 | - } |
3470 | - currentAction = -1; |
3471 | - currentMarkingIndex = 0; |
3472 | - tab.network().setMarking(markings.get(currentMarkingIndex)); |
3473 | - tab.getAnimationHistorySidePanel().setSelectedIndex(0); |
3474 | - updateAnimationButtonsEnabled(); |
3475 | - updateFireableTransitions(); |
3476 | - } |
3477 | - |
3478 | - private void setUntimedTrace(TAPNNetworkTrace trace) { |
3479 | - tab.addAbstractAnimationPane(); |
3480 | - AnimationHistoryList untimedAnimationHistory = tab.getUntimedAnimationHistory(); |
3481 | - |
3482 | - for(TAPNNetworkTraceStep step : trace){ |
3483 | - untimedAnimationHistory.addHistoryItem(step.toString()); |
3484 | - } |
3485 | - |
3486 | - tab.getUntimedAnimationHistory().setSelectedIndex(0); |
3487 | - setFiringmode("Random"); |
3488 | - |
3489 | - JOptionPane.showMessageDialog(CreateGui.getApp(), |
3490 | - "The verification process returned an untimed trace.\n\n" |
3491 | - + "This means that with appropriate time delays the displayed\n" |
3492 | - + "sequence of discrete transitions can become a concrete trace.\n" |
3493 | - + "In case of liveness properties (EG, AF) the untimed trace\n" |
3494 | - + "either ends in a deadlock, a time divergent computation without\n" |
3495 | - + "any discrete transitions, or it loops back to some earlier configuration.\n" |
3496 | - + "The user may experiment in the simulator with different time delays\n" |
3497 | - + "in order to realize the suggested untimed trace in the model.", |
3498 | - "Verification Information", JOptionPane.INFORMATION_MESSAGE); |
3499 | - } |
3500 | - |
3501 | - private void setTimedTrace(TAPNNetworkTrace trace) { |
3502 | - for (TAPNNetworkTraceStep step : trace) { |
3503 | - addMarking(step, step.performStepFrom(currentMarking())); |
3504 | - } |
3505 | - if(getTrace().getTraceType() != TraceType.NOT_EG){ //If the trace was not explicitly set, maybe we have calculated it is deadlock. |
3506 | - tab.getAnimationHistorySidePanel().setLastShown(getTrace().getTraceType()); |
3507 | - } |
3508 | - } |
3509 | - |
3510 | - private void addToTimedTrace(List<TAPNNetworkTraceStep> stepList){ |
3511 | - for (TAPNNetworkTraceStep step : stepList) { |
3512 | - addMarking(step, step.performStepFrom(currentMarking())); |
3513 | - } |
3514 | - } |
3515 | - |
3516 | - public NetworkMarking getInitialMarking(){ |
3517 | - return initialMarking; |
3518 | - } |
3519 | - |
3520 | - /** |
3521 | - * Highlights enabled transitions |
3522 | - */ |
3523 | - public void highlightEnabledTransitions() { |
3524 | - updateFireableTransitions(); |
3525 | - DataLayer current = activeGuiModel(); |
3526 | - |
3527 | - for (Transition tempTransition : current.transitions()) { |
3528 | - if (tempTransition.isEnabled(true) || (tempTransition.isDelayEnabledTransition(true) && !isUrgentTransitionEnabled)) { |
3529 | - tempTransition.repaint(); |
3530 | - } |
3531 | - } |
3532 | - } |
3533 | - |
3534 | - /** |
3535 | - * Called during animation to unhighlight previously highlighted transitions |
3536 | - */ |
3537 | - private void unhighlightDisabledTransitions() { |
3538 | - DataLayer current = activeGuiModel(); |
3539 | - |
3540 | - for (Transition t : current.transitions()) { |
3541 | - if (!(t.isEnabled(true)) || !t.isDelayEnabledTransition(true) || (t.isDelayEnabledTransition(true) && isUrgentTransitionEnabled)) { |
3542 | - t.repaint(); |
3543 | - } |
3544 | - } |
3545 | - } |
3546 | - |
3547 | - public void updateFireableTransitions(){ |
3548 | - TransitionFireingComponent transFireComponent = tab.getTransitionFireingComponent(); |
3549 | - transFireComponent.startReInit(); |
3550 | - isUrgentTransitionEnabled = false; |
3551 | - |
3552 | - outer: for( Template temp : tab.activeTemplates()){ |
3553 | - for (Transition tempTransition : temp.guiModel().transitions()) { |
3554 | - if (tempTransition.isEnabled(true) && temp.model().getTransitionByName(tempTransition.getName()).isUrgent()) { |
3555 | + if (trace.isConcreteTrace()) { |
3556 | + this.trace = trace; |
3557 | + setTimedTrace(trace); |
3558 | + } else { |
3559 | + setUntimedTrace(trace); |
3560 | + isDisplayingUntimedTrace = true; |
3561 | + } |
3562 | + currentAction = -1; |
3563 | + currentMarkingIndex = 0; |
3564 | + tab.network().setMarking(markings.get(currentMarkingIndex)); |
3565 | + tab.getAnimationHistorySidePanel().setSelectedIndex(0); |
3566 | + updateAnimationButtonsEnabled(); |
3567 | + updateFireableTransitions(); |
3568 | + } |
3569 | + |
3570 | + private void setUntimedTrace(TAPNNetworkTrace trace) { |
3571 | + tab.addAbstractAnimationPane(); |
3572 | + AnimationHistoryList untimedAnimationHistory = tab.getUntimedAnimationHistory(); |
3573 | + |
3574 | + for(TAPNNetworkTraceStep step : trace){ |
3575 | + untimedAnimationHistory.addHistoryItem(step.toString()); |
3576 | + } |
3577 | + |
3578 | + tab.getUntimedAnimationHistory().setSelectedIndex(0); |
3579 | + setFiringmode("Random"); |
3580 | + |
3581 | + JOptionPane.showMessageDialog(CreateGui.getApp(), |
3582 | + "The verification process returned an untimed trace.\n\n" |
3583 | + + "This means that with appropriate time delays the displayed\n" |
3584 | + + "sequence of discrete transitions can become a concrete trace.\n" |
3585 | + + "In case of liveness properties (EG, AF) the untimed trace\n" |
3586 | + + "either ends in a deadlock, a time divergent computation without\n" |
3587 | + + "any discrete transitions, or it loops back to some earlier configuration.\n" |
3588 | + + "The user may experiment in the simulator with different time delays\n" |
3589 | + + "in order to realize the suggested untimed trace in the model.", |
3590 | + "Verification Information", JOptionPane.INFORMATION_MESSAGE); |
3591 | + } |
3592 | + |
3593 | + private void setTimedTrace(TAPNNetworkTrace trace) { |
3594 | + for (TAPNNetworkTraceStep step : trace) { |
3595 | + addMarking(step, step.performStepFrom(currentMarking())); |
3596 | + } |
3597 | + if(getTrace().getTraceType() != TraceType.NOT_EG){ //If the trace was not explicitly set, maybe we have calculated it is deadlock. |
3598 | + tab.getAnimationHistorySidePanel().setLastShown(getTrace().getTraceType()); |
3599 | + } |
3600 | + } |
3601 | + |
3602 | + private void addToTimedTrace(List<TAPNNetworkTraceStep> stepList){ |
3603 | + for (TAPNNetworkTraceStep step : stepList) { |
3604 | + addMarking(step, step.performStepFrom(currentMarking())); |
3605 | + } |
3606 | + } |
3607 | + |
3608 | + public NetworkMarking getInitialMarking(){ |
3609 | + return initialMarking; |
3610 | + } |
3611 | + |
3612 | + /** |
3613 | + * Highlights enabled transitions |
3614 | + */ |
3615 | + public void highlightEnabledTransitions() { |
3616 | + updateFireableTransitions(); |
3617 | + } |
3618 | + |
3619 | + /** |
3620 | + * Called during animation to unhighlight previously highlighted transitions |
3621 | + */ |
3622 | + private void unhighlightDisabledTransitions() { |
3623 | + disableTransitions(); |
3624 | + } |
3625 | + |
3626 | + public void updateFireableTransitions(){ |
3627 | + TransitionFireingComponent transFireComponent = tab.getTransitionFireingComponent(); |
3628 | + transFireComponent.startReInit(); |
3629 | + isUrgentTransitionEnabled = false; |
3630 | + |
3631 | + outer: for( Template template : tab.activeTemplates()){ |
3632 | + for (TimedTransition t : template.model().transitions()) { |
3633 | + if (t.isUrgent() && t.isEnabled()) { |
3634 | isUrgentTransitionEnabled = true; |
3635 | break outer; |
3636 | } |
3637 | } |
3638 | - } |
3639 | - |
3640 | - for( Template temp : tab.activeTemplates()){ |
3641 | - for (Transition tempTransition : temp.guiModel().transitions()) { |
3642 | - if (tempTransition.isEnabled(true) || (tempTransition.isDelayEnabledTransition(true) && CreateGui.getApp().isShowingDelayEnabledTransitions() && !isUrgentTransitionEnabled)) { |
3643 | - transFireComponent.addTransition(temp, tempTransition); |
3644 | + } |
3645 | + |
3646 | + for( Template template : tab.activeTemplates()){ |
3647 | + for (Transition t : template.guiModel().transitions()) { |
3648 | + if (t.isTransitionEnabled()) { |
3649 | + t.markTransitionEnabled(true); |
3650 | + transFireComponent.addTransition(template, t); |
3651 | + } else if (CreateGui.getApp().isShowingDelayEnabledTransitions() && |
3652 | + t.isDelayEnabled() && !isUrgentTransitionEnabled |
3653 | + ) { |
3654 | + t.markTransitionDelayEnabled(true); |
3655 | + transFireComponent.addTransition(template, t); |
3656 | } |
3657 | + |
3658 | } |
3659 | - } |
3660 | - |
3661 | - transFireComponent.reInitDone(); |
3662 | - } |
3663 | - |
3664 | - /** |
3665 | - * Called at end of animation and resets all Transitions to false and |
3666 | - * unhighlighted |
3667 | - */ |
3668 | - private void disableTransitions() { |
3669 | - for(Template template : tab.allTemplates()) |
3670 | - { |
3671 | + } |
3672 | + |
3673 | + transFireComponent.reInitDone(); |
3674 | + } |
3675 | + |
3676 | + /** |
3677 | + * Called at end of animation and resets all Transitions to false and |
3678 | + * unhighlighted |
3679 | + */ |
3680 | + private void disableTransitions() { |
3681 | + for(Template template : tab.allTemplates()) |
3682 | + { |
3683 | for (Transition tempTransition : template.guiModel().transitions()) { |
3684 | - tempTransition.setEnabledFalse(); |
3685 | - tempTransition.setDelayEnabledTransitionFalse(); |
3686 | + tempTransition.disableHightligh(); |
3687 | + |
3688 | tempTransition.repaint(); |
3689 | } |
3690 | - } |
3691 | - } |
3692 | - |
3693 | - /** |
3694 | - * Stores model at start of animation |
3695 | - */ |
3696 | - public void storeModel() { |
3697 | - initialMarking = tab.network().marking(); |
3698 | - resethistory(); |
3699 | - markings.add(initialMarking); |
3700 | - } |
3701 | - |
3702 | - /** |
3703 | - * Restores model at end of animation and sets all transitions to false and |
3704 | - * unhighlighted |
3705 | - */ |
3706 | - public void restoreModel() { |
3707 | - if (tab != null) { |
3708 | - disableTransitions(); |
3709 | - if (initialMarking != null) { |
3710 | - tab.network().setMarking(initialMarking); |
3711 | - } |
3712 | - currentAction = -1; |
3713 | - } |
3714 | - } |
3715 | - |
3716 | - /** |
3717 | - * Steps back through previously fired transitions |
3718 | - * |
3719 | - * @author jokke refactored and added backwards firing for TAPNTransitions |
3720 | - */ |
3721 | - |
3722 | - public void stepBack() { |
3723 | + } |
3724 | + } |
3725 | + |
3726 | + /** |
3727 | + * Stores model at start of animation |
3728 | + */ |
3729 | + public void storeModel() { |
3730 | + initialMarking = tab.network().marking(); |
3731 | + resethistory(); |
3732 | + markings.add(initialMarking); |
3733 | + } |
3734 | + |
3735 | + /** |
3736 | + * Restores model at end of animation and sets all transitions to false and |
3737 | + * unhighlighted |
3738 | + */ |
3739 | + public void restoreModel() { |
3740 | + if (tab != null) { |
3741 | + disableTransitions(); |
3742 | + tab.network().setMarking(initialMarking); |
3743 | + currentAction = -1; |
3744 | + } |
3745 | + } |
3746 | + |
3747 | + /** |
3748 | + * Steps back through previously fired transitions |
3749 | + * |
3750 | + * @author jokke refactored and added backwards firing for TAPNTransitions |
3751 | + */ |
3752 | + |
3753 | + public void stepBack() { |
3754 | tab.getAnimationHistorySidePanel().stepBackwards(); |
3755 | - if (!actionHistory.isEmpty()){ |
3756 | - TAPNNetworkTraceStep lastStep = actionHistory.get(currentAction); |
3757 | - if(isDisplayingUntimedTrace && lastStep instanceof TAPNNetworkTimedTransitionStep){ |
3758 | - AnimationHistoryList untimedAnimationHistory = tab.getUntimedAnimationHistory(); |
3759 | - String previousInUntimedTrace = untimedAnimationHistory.getElement(untimedAnimationHistory.getSelectedIndex()); |
3760 | - if(previousInUntimedTrace.equals(lastStep.toString())){ |
3761 | - untimedAnimationHistory.stepBackwards(); |
3762 | - } |
3763 | - } |
3764 | - tab.network().setMarking(markings.get(currentMarkingIndex - 1)); |
3765 | + if (!actionHistory.isEmpty()){ |
3766 | + TAPNNetworkTraceStep lastStep = actionHistory.get(currentAction); |
3767 | + if(isDisplayingUntimedTrace && lastStep instanceof TAPNNetworkTimedTransitionStep){ |
3768 | + AnimationHistoryList untimedAnimationHistory = tab.getUntimedAnimationHistory(); |
3769 | + String previousInUntimedTrace = untimedAnimationHistory.getElement(untimedAnimationHistory.getSelectedIndex()); |
3770 | + if(previousInUntimedTrace.equals(lastStep.toString())){ |
3771 | + untimedAnimationHistory.stepBackwards(); |
3772 | + } |
3773 | + } |
3774 | + tab.network().setMarking(markings.get(currentMarkingIndex - 1)); |
3775 | |
3776 | - activeGuiModel().repaintPlaces(); |
3777 | - unhighlightDisabledTransitions(); |
3778 | - highlightEnabledTransitions(); |
3779 | - currentAction--; |
3780 | - currentMarkingIndex--; |
3781 | + activeGuiModel().repaintPlaces(); |
3782 | + unhighlightDisabledTransitions(); |
3783 | + highlightEnabledTransitions(); |
3784 | + currentAction--; |
3785 | + currentMarkingIndex--; |
3786 | |
3787 | updateAnimationButtonsEnabled(); |
3788 | updateMouseOverInformation(); |
3789 | - reportBlockingPlaces(); |
3790 | - } |
3791 | - } |
3792 | - |
3793 | - /** |
3794 | - * Steps forward through previously fired transitions |
3795 | - */ |
3796 | - |
3797 | - public void stepForward() { |
3798 | + reportBlockingPlaces(); |
3799 | + } |
3800 | + } |
3801 | + |
3802 | + /** |
3803 | + * Steps forward through previously fired transitions |
3804 | + */ |
3805 | + |
3806 | + public void stepForward() { |
3807 | tab.getAnimationHistorySidePanel().stepForward(); |
3808 | - if(currentAction == actionHistory.size()-1 && trace != null){ |
3809 | - int selectedIndex = tab.getAnimationHistorySidePanel().getSelectedIndex(); |
3810 | - int action = currentAction; |
3811 | - int markingIndex = currentMarkingIndex; |
3812 | - |
3813 | - if(getTrace().getTraceType() == TraceType.EG_DELAY_FOREVER){ |
3814 | - addMarking(new TAPNNetworkTimeDelayStep(BigDecimal.ONE), currentMarking().delay(BigDecimal.ONE)); |
3815 | - } |
3816 | - if(getTrace().getLoopToIndex() != -1){ |
3817 | - addToTimedTrace(getTrace().getLoopSteps()); |
3818 | - } |
3819 | - |
3820 | - tab.getAnimationHistorySidePanel().setSelectedIndex(selectedIndex); |
3821 | - currentAction = action; |
3822 | - currentMarkingIndex = markingIndex; |
3823 | - } |
3824 | - |
3825 | - if (currentAction < actionHistory.size() - 1) { |
3826 | - TAPNNetworkTraceStep nextStep = actionHistory.get(currentAction+1); |
3827 | - if(isDisplayingUntimedTrace && nextStep instanceof TAPNNetworkTimedTransitionStep){ |
3828 | - AnimationHistoryList untimedAnimationHistory = tab.getUntimedAnimationHistory(); |
3829 | - String nextInUntimedTrace = untimedAnimationHistory.getElement(untimedAnimationHistory.getSelectedIndex()+1); |
3830 | - if(nextInUntimedTrace.equals(nextStep.toString())){ |
3831 | - untimedAnimationHistory.stepForward(); |
3832 | - } |
3833 | - } |
3834 | - tab.network().setMarking(markings.get(currentMarkingIndex + 1)); |
3835 | - |
3836 | - activeGuiModel().repaintPlaces(); |
3837 | - unhighlightDisabledTransitions(); |
3838 | - highlightEnabledTransitions(); |
3839 | - currentAction++; |
3840 | - currentMarkingIndex++; |
3841 | - activeGuiModel().redrawVisibleTokenLists(); |
3842 | + if(currentAction == actionHistory.size()-1 && trace != null){ |
3843 | + int selectedIndex = tab.getAnimationHistorySidePanel().getSelectedIndex(); |
3844 | + int action = currentAction; |
3845 | + int markingIndex = currentMarkingIndex; |
3846 | + |
3847 | + if(getTrace().getTraceType() == TraceType.EG_DELAY_FOREVER){ |
3848 | + addMarking(new TAPNNetworkTimeDelayStep(BigDecimal.ONE), currentMarking().delay(BigDecimal.ONE)); |
3849 | + } |
3850 | + if(getTrace().getLoopToIndex() != -1){ |
3851 | + addToTimedTrace(getTrace().getLoopSteps()); |
3852 | + } |
3853 | + |
3854 | + tab.getAnimationHistorySidePanel().setSelectedIndex(selectedIndex); |
3855 | + currentAction = action; |
3856 | + currentMarkingIndex = markingIndex; |
3857 | + } |
3858 | + |
3859 | + if (currentAction < actionHistory.size() - 1) { |
3860 | + TAPNNetworkTraceStep nextStep = actionHistory.get(currentAction+1); |
3861 | + if(isDisplayingUntimedTrace && nextStep instanceof TAPNNetworkTimedTransitionStep){ |
3862 | + AnimationHistoryList untimedAnimationHistory = tab.getUntimedAnimationHistory(); |
3863 | + String nextInUntimedTrace = untimedAnimationHistory.getElement(untimedAnimationHistory.getSelectedIndex()+1); |
3864 | + if(nextInUntimedTrace.equals(nextStep.toString())){ |
3865 | + untimedAnimationHistory.stepForward(); |
3866 | + } |
3867 | + } |
3868 | + tab.network().setMarking(markings.get(currentMarkingIndex + 1)); |
3869 | + |
3870 | + activeGuiModel().repaintPlaces(); |
3871 | + unhighlightDisabledTransitions(); |
3872 | + highlightEnabledTransitions(); |
3873 | + currentAction++; |
3874 | + currentMarkingIndex++; |
3875 | + activeGuiModel().redrawVisibleTokenLists(); |
3876 | |
3877 | updateAnimationButtonsEnabled(); |
3878 | updateMouseOverInformation(); |
3879 | - reportBlockingPlaces(); |
3880 | - |
3881 | - } |
3882 | - } |
3883 | - |
3884 | - /** |
3885 | - * Make the selected transition in the animation box blink, based on the |
3886 | - * list element label |
3887 | - */ |
3888 | - |
3889 | - public void blinkSelected(String label){ |
3890 | - if(label.contains(".")){ |
3891 | - label = label.split("\\.")[1]; |
3892 | - } |
3893 | - |
3894 | - Transition t = activeGuiModel().getTransitionByName(label); |
3895 | - if(t != null){ |
3896 | - t.blink(); |
3897 | - } |
3898 | - } |
3899 | - |
3900 | - public void dFireTransition(TimedTransition transition){ |
3901 | - if(!CreateGui.getApp().isShowingDelayEnabledTransitions() || isUrgentTransitionEnabled()){ |
3902 | - fireTransition(transition); |
3903 | - return; |
3904 | - } |
3905 | - |
3906 | - TimeInterval dInterval = transition.getdInterval(); |
3907 | - |
3908 | - BigDecimal delayGranularity = tab.getDelayEnabledTransitionControl().getValue(); |
3909 | - //Make sure the granularity is small enough |
3910 | - BigDecimal lowerBound = IntervalOperations.getRatBound(dInterval.lowerBound()).getBound(); |
3911 | - if(!dInterval.IsLowerBoundNonStrict() && !dInterval.isIncluded(lowerBound.add(delayGranularity))){ |
3912 | - do{ |
3913 | - delayGranularity = delayGranularity.divide(BigDecimal.TEN); |
3914 | - } while (delayGranularity.compareTo(new BigDecimal("0.00001")) >= 0 && !dInterval.isIncluded(lowerBound.add(delayGranularity))); |
3915 | - } |
3916 | - |
3917 | - if(delayGranularity.compareTo(new BigDecimal("0.00001")) < 0){ |
3918 | - JOptionPane.showMessageDialog(CreateGui.getApp(), "<html>Due to the limit of only five decimal points in the simulator</br> its not possible to fire the transition</html>"); |
3919 | - } else { |
3920 | - BigDecimal delay = tab.getDelayEnabledTransitionControl().getDelayMode().GetDelay(transition, dInterval, delayGranularity); |
3921 | - if(delay != null){ |
3922 | - if(delay.compareTo(BigDecimal.ZERO) != 0){ //Don't delay if the chosen delay is 0 |
3923 | - if(!letTimePass(delay)){ |
3924 | - return; |
3925 | - } |
3926 | - } |
3927 | - |
3928 | - fireTransition(transition); |
3929 | - |
3930 | - } |
3931 | - } |
3932 | - } |
3933 | - |
3934 | - // TODO: Clean up this method |
3935 | - private void fireTransition(TimedTransition transition) { |
3936 | - |
3937 | - if(!clearStepsForward()){ |
3938 | - return; |
3939 | - } |
3940 | - |
3941 | - Tuple<NetworkMarking, List<TimedToken>> next = null; |
3942 | - List<TimedToken> tokensToConsume = null; |
3943 | - |
3944 | - try{ |
3945 | - if (getFiringmode() != null) { |
3946 | - next = currentMarking().fireTransition(transition, getFiringmode()); |
3947 | - } else { |
3948 | - tokensToConsume = getTokensToConsume(transition); |
3949 | - if(tokensToConsume == null) return; // Cancelled |
3950 | - next = new Tuple<NetworkMarking, List<TimedToken>> (currentMarking().fireTransition(transition, tokensToConsume), tokensToConsume); |
3951 | - } |
3952 | - }catch(RequireException e){ |
3953 | - JOptionPane.showMessageDialog(CreateGui.getApp(), "There was an error firing the transition. Reason: " + e.getMessage(), "Error", JOptionPane.ERROR_MESSAGE); |
3954 | - return; |
3955 | - } |
3956 | - |
3957 | - // It is important that this comes after the above, since |
3958 | - // cancelling the token selection dialogue above should not result in changes |
3959 | - // to the untimed animation history |
3960 | - if (isDisplayingUntimedTrace){ |
3961 | - AnimationHistoryList untimedAnimationHistory = tab.getUntimedAnimationHistory(); |
3962 | - if(untimedAnimationHistory.isStepForwardAllowed()){ |
3963 | - String nextFromUntimedTrace = untimedAnimationHistory.getElement(untimedAnimationHistory.getSelectedIndex()+1); |
3964 | - |
3965 | - if(nextFromUntimedTrace.equals(transition.model().name() + "." + transition.name()) || transition.isShared() && nextFromUntimedTrace.equals(transition.name())){ |
3966 | - untimedAnimationHistory.stepForward(); |
3967 | - }else{ |
3968 | - int fireTransition = JOptionPane.showConfirmDialog(CreateGui.getApp(), |
3969 | - "Are you sure you want to fire a transition which does not follow the untimed trace?\n" |
3970 | - + "Firing this transition will discard the untimed trace and revert to standard simulation.", |
3971 | - "Discrading Untimed Trace", JOptionPane.YES_NO_OPTION ); |
3972 | - |
3973 | - if (fireTransition == JOptionPane.NO_OPTION){ |
3974 | - return; |
3975 | - }else{ |
3976 | - removeSetTrace(false); |
3977 | - } |
3978 | - } |
3979 | - } |
3980 | - } |
3981 | - |
3982 | - tab.network().setMarking(next.value1()); |
3983 | - |
3984 | - activeGuiModel().repaintPlaces(); |
3985 | - highlightEnabledTransitions(); |
3986 | - unhighlightDisabledTransitions(); |
3987 | - addMarking(new TAPNNetworkTimedTransitionStep(transition, next.value2()), next.value1()); |
3988 | - |
3989 | - updateAnimationButtonsEnabled(); |
3990 | - updateMouseOverInformation(); |
3991 | - reportBlockingPlaces(); |
3992 | - |
3993 | - } |
3994 | - |
3995 | - public boolean letTimePass(BigDecimal delay) { |
3996 | - |
3997 | - if(!clearStepsForward()){ |
3998 | - return false; |
3999 | - } |
4000 | - |
4001 | - boolean result = false; |
4002 | - if (delay.compareTo(new BigDecimal(0))==0 || (currentMarking().isDelayPossible(delay) && !isUrgentTransitionEnabled)) { |
4003 | - NetworkMarking delayedMarking = currentMarking().delay(delay); |
4004 | - tab.network().setMarking(delayedMarking); |
4005 | - addMarking(new TAPNNetworkTimeDelayStep(delay), delayedMarking); |
4006 | - result = true; |
4007 | - } |
4008 | - |
4009 | - activeGuiModel().repaintPlaces(); |
4010 | - highlightEnabledTransitions(); |
4011 | - unhighlightDisabledTransitions(); |
4012 | - |
4013 | - updateAnimationButtonsEnabled(); |
4014 | - updateMouseOverInformation(); |
4015 | - reportBlockingPlaces(); |
4016 | - |
4017 | - return result; |
4018 | - } |
4019 | - |
4020 | - public void reportBlockingPlaces(){ |
4021 | - |
4022 | - try{ |
4023 | - BigDecimal delay = tab.getAnimationController().getCurrentDelay(); |
4024 | - if(isUrgentTransitionEnabled && delay.compareTo(new BigDecimal(0))>0){ |
4025 | - tab.getAnimationController().getOkButton().setEnabled(false); |
4026 | - StringBuilder sb = new StringBuilder(); |
4027 | - sb.append("<html>Time delay is disabled due to the<br /> following enabled urgent transitions:<br /><br />"); |
4028 | - for( Template temp : tab.activeTemplates()){ |
4029 | - for (Transition tempTransition : temp.guiModel().transitions()) { |
4030 | - if (tempTransition.isEnabled(true) && temp.model().getTransitionByName(tempTransition.getName()).isUrgent()) { |
4031 | - sb.append(temp.toString() + "." + tempTransition.getName() + "<br />"); |
4032 | - } |
4033 | - } |
4034 | - } |
4035 | - sb.append("</html>"); |
4036 | - tab.getAnimationController().getOkButton().setToolTipText(sb.toString()); |
4037 | - return; |
4038 | - } |
4039 | - if(delay.compareTo(new BigDecimal(0))<0){ |
4040 | - tab.getAnimationController().getOkButton().setEnabled(false); |
4041 | - tab.getAnimationController().getOkButton().setToolTipText("Time delay is possible only for nonnegative rational numbers"); |
4042 | - } else { |
4043 | - List<TimedPlace> blockingPlaces = currentMarking().getBlockingPlaces(delay); |
4044 | - if(blockingPlaces.size() == 0){ |
4045 | - tab.getAnimationController().getOkButton().setEnabled(true); |
4046 | - tab.getAnimationController().getOkButton().setToolTipText("Press to add the delay"); |
4047 | - } else { |
4048 | - StringBuilder sb = new StringBuilder(); |
4049 | - sb.append("<html>Time delay of " + delay + " time unit(s) is disabled due to <br /> age invariants in the following places:<br /><br />"); |
4050 | - for (TimedPlace t :blockingPlaces){ |
4051 | - sb.append(t.toString() + "<br />"); |
4052 | - } |
4053 | - //JOptionPane.showMessageDialog(null, sb.toString()); |
4054 | - sb.append("</html>"); |
4055 | - tab.getAnimationController().getOkButton().setEnabled(false); |
4056 | - tab.getAnimationController().getOkButton().setToolTipText(sb.toString()); |
4057 | - } |
4058 | - } |
4059 | - } catch (NumberFormatException e) { |
4060 | - // Do nothing, invalud number |
4061 | - } catch (ParseException e) { |
4062 | - tab.getAnimationController().getOkButton().setEnabled(false); |
4063 | - tab.getAnimationController().getOkButton().setToolTipText("The text in the input field is not a number"); |
4064 | - } |
4065 | - } |
4066 | - |
4067 | - private DataLayer activeGuiModel() { |
4068 | - return tab.currentTemplate().guiModel(); |
4069 | - } |
4070 | - |
4071 | - private void resethistory() { |
4072 | - actionHistory.clear(); |
4073 | - markings.clear(); |
4074 | - currentAction = -1; |
4075 | - currentMarkingIndex = 0; |
4076 | - tab.getAnimationHistorySidePanel().reset(); |
4077 | - if(tab.getUntimedAnimationHistory() != null){ |
4078 | - tab.getUntimedAnimationHistory().reset(); |
4079 | - } |
4080 | - } |
4081 | - |
4082 | - public FiringMode getFiringmode() { |
4083 | - return firingmode; |
4084 | - } |
4085 | - |
4086 | - // removes stored markings and actions from index "startWith" (included) |
4087 | - private void removeStoredActions(int startWith) { |
4088 | - int lastIndex = actionHistory.size() - 1; |
4089 | - for (int i = startWith; i <= lastIndex; i++) { |
4090 | - removeLastHistoryStep(); |
4091 | - } |
4092 | - } |
4093 | - |
4094 | - private void addMarking(TAPNNetworkTraceStep action, NetworkMarking marking) { |
4095 | - if (currentAction < actionHistory.size() - 1) { |
4096 | + reportBlockingPlaces(); |
4097 | + |
4098 | + } |
4099 | + } |
4100 | + |
4101 | + /** |
4102 | + * Make the selected transition in the animation box blink, based on the |
4103 | + * list element label |
4104 | + */ |
4105 | + |
4106 | + public void blinkSelected(String label){ |
4107 | + if(label.contains(".")){ |
4108 | + label = label.split("\\.")[1]; |
4109 | + } |
4110 | + |
4111 | + Transition t = activeGuiModel().getTransitionByName(label); |
4112 | + if(t != null){ |
4113 | + t.blink(); |
4114 | + } |
4115 | + } |
4116 | + |
4117 | + public void dFireTransition(TimedTransition transition){ |
4118 | + if(!CreateGui.getApp().isShowingDelayEnabledTransitions() || isUrgentTransitionEnabled()){ |
4119 | + fireTransition(transition); |
4120 | + return; |
4121 | + } |
4122 | + |
4123 | + TimeInterval dInterval = transition.getdInterval(); |
4124 | + |
4125 | + BigDecimal delayGranularity = tab.getDelayEnabledTransitionControl().getValue(); |
4126 | + //Make sure the granularity is small enough |
4127 | + BigDecimal lowerBound = IntervalOperations.getRatBound(dInterval.lowerBound()).getBound(); |
4128 | + if(!dInterval.IsLowerBoundNonStrict() && !dInterval.isIncluded(lowerBound.add(delayGranularity))){ |
4129 | + do{ |
4130 | + delayGranularity = delayGranularity.divide(BigDecimal.TEN); |
4131 | + } while (delayGranularity.compareTo(new BigDecimal("0.00001")) >= 0 && !dInterval.isIncluded(lowerBound.add(delayGranularity))); |
4132 | + } |
4133 | + |
4134 | + if(delayGranularity.compareTo(new BigDecimal("0.00001")) < 0){ |
4135 | + JOptionPane.showMessageDialog(CreateGui.getApp(), "<html>Due to the limit of only five decimal points in the simulator</br> its not possible to fire the transition</html>"); |
4136 | + } else { |
4137 | + BigDecimal delay = tab.getDelayEnabledTransitionControl().getDelayMode().GetDelay(transition, dInterval, delayGranularity); |
4138 | + if(delay != null){ |
4139 | + if(delay.compareTo(BigDecimal.ZERO) != 0){ //Don't delay if the chosen delay is 0 |
4140 | + if(!letTimePass(delay)){ |
4141 | + return; |
4142 | + } |
4143 | + } |
4144 | + |
4145 | + fireTransition(transition); |
4146 | + } |
4147 | + } |
4148 | + } |
4149 | + |
4150 | + // TODO: Clean up this method |
4151 | + private void fireTransition(TimedTransition transition) { |
4152 | + |
4153 | + if(!clearStepsForward()){ |
4154 | + return; |
4155 | + } |
4156 | + |
4157 | + Tuple<NetworkMarking, List<TimedToken>> next = null; |
4158 | + List<TimedToken> tokensToConsume = null; |
4159 | + try{ |
4160 | + if (getFiringmode() != null) { |
4161 | + next = currentMarking().fireTransition(transition, getFiringmode()); |
4162 | + } else { |
4163 | + tokensToConsume = getTokensToConsume(transition); |
4164 | + if(tokensToConsume == null) return; // Cancelled |
4165 | + next = new Tuple<NetworkMarking, List<TimedToken>> (currentMarking().fireTransition(transition, tokensToConsume), tokensToConsume); |
4166 | + } |
4167 | + }catch(RequireException e){ |
4168 | + JOptionPane.showMessageDialog(CreateGui.getApp(), "There was an error firing the transition. Reason: " + e.getMessage(), "Error", JOptionPane.ERROR_MESSAGE); |
4169 | + return; |
4170 | + } |
4171 | + |
4172 | + // It is important that this comes after the above, since |
4173 | + // cancelling the token selection dialogue above should not result in changes |
4174 | + // to the untimed animation history |
4175 | + if (isDisplayingUntimedTrace){ |
4176 | + AnimationHistoryList untimedAnimationHistory = tab.getUntimedAnimationHistory(); |
4177 | + if(untimedAnimationHistory.isStepForwardAllowed()){ |
4178 | + String nextFromUntimedTrace = untimedAnimationHistory.getElement(untimedAnimationHistory.getSelectedIndex()+1); |
4179 | + |
4180 | + if(nextFromUntimedTrace.equals(transition.model().name() + "." + transition.name()) || transition.isShared() && nextFromUntimedTrace.equals(transition.name())){ |
4181 | + untimedAnimationHistory.stepForward(); |
4182 | + }else{ |
4183 | + int fireTransition = JOptionPane.showConfirmDialog(CreateGui.getApp(), |
4184 | + "Are you sure you want to fire a transition which does not follow the untimed trace?\n" |
4185 | + + "Firing this transition will discard the untimed trace and revert to standard simulation.", |
4186 | + "Discrading Untimed Trace", JOptionPane.YES_NO_OPTION ); |
4187 | + |
4188 | + if (fireTransition == JOptionPane.NO_OPTION){ |
4189 | + return; |
4190 | + }else{ |
4191 | + removeSetTrace(false); |
4192 | + } |
4193 | + } |
4194 | + } |
4195 | + } |
4196 | + |
4197 | + tab.network().setMarking(next.value1()); |
4198 | + |
4199 | + activeGuiModel().repaintPlaces(); |
4200 | + unhighlightDisabledTransitions(); |
4201 | + highlightEnabledTransitions(); |
4202 | + |
4203 | + addMarking(new TAPNNetworkTimedTransitionStep(transition, next.value2()), next.value1()); |
4204 | + |
4205 | + updateAnimationButtonsEnabled(); |
4206 | + updateMouseOverInformation(); |
4207 | + reportBlockingPlaces(); |
4208 | + |
4209 | + } |
4210 | + |
4211 | + public boolean letTimePass(BigDecimal delay) { |
4212 | + |
4213 | + if(!clearStepsForward()){ |
4214 | + return false; |
4215 | + } |
4216 | + |
4217 | + boolean result = false; |
4218 | + if (delay.compareTo(new BigDecimal(0))==0 || (currentMarking().isDelayPossible(delay) && !isUrgentTransitionEnabled)) { |
4219 | + NetworkMarking delayedMarking = currentMarking().delay(delay); |
4220 | + tab.network().setMarking(delayedMarking); |
4221 | + addMarking(new TAPNNetworkTimeDelayStep(delay), delayedMarking); |
4222 | + result = true; |
4223 | + } |
4224 | + |
4225 | + activeGuiModel().repaintPlaces(); |
4226 | + unhighlightDisabledTransitions(); |
4227 | + highlightEnabledTransitions(); |
4228 | + |
4229 | + updateAnimationButtonsEnabled(); |
4230 | + updateMouseOverInformation(); |
4231 | + reportBlockingPlaces(); |
4232 | + return result; |
4233 | + } |
4234 | + |
4235 | + public void reportBlockingPlaces() { |
4236 | + |
4237 | + try { |
4238 | + BigDecimal delay = tab.getAnimationController().getCurrentDelay(); |
4239 | + |
4240 | + if (isUrgentTransitionEnabled && !delay.equals(BigDecimal.ZERO) ) { |
4241 | + tab.getAnimationController().getOkButton().setEnabled(false); |
4242 | + |
4243 | + StringBuilder sb = new StringBuilder(); |
4244 | + sb.append("<html>Time delay is disabled due to the<br /> following enabled urgent transitions:<br /><br />"); |
4245 | + for (Template template : tab.activeTemplates()) { |
4246 | + for (Transition t : template.guiModel().transitions()) { |
4247 | + if (t.isTransitionEnabled() && template.model().getTransitionByName(t.getName()).isUrgent()) { |
4248 | + sb.append(template.toString() + "." + t.getName() + "<br />"); |
4249 | + } |
4250 | + } |
4251 | + } |
4252 | + sb.append("</html>"); |
4253 | + |
4254 | + tab.getAnimationController().getOkButton().setToolTipText(sb.toString()); |
4255 | + |
4256 | + return; |
4257 | + } |
4258 | + |
4259 | + if (delay.compareTo(new BigDecimal(0)) < 0) { |
4260 | + tab.getAnimationController().getOkButton().setEnabled(false); |
4261 | + tab.getAnimationController().getOkButton().setToolTipText("Time delay is possible only for nonnegative rational numbers"); |
4262 | + } else { |
4263 | + List<TimedPlace> blockingPlaces = currentMarking().getBlockingPlaces(delay); |
4264 | + if (blockingPlaces.size() == 0) { |
4265 | + tab.getAnimationController().getOkButton().setEnabled(true); |
4266 | + tab.getAnimationController().getOkButton().setToolTipText("Press to add the delay"); |
4267 | + } else { |
4268 | + StringBuilder sb = new StringBuilder(); |
4269 | + sb.append("<html>Time delay of " + delay + " time unit(s) is disabled due to <br /> age invariants in the following places:<br /><br />"); |
4270 | + for (TimedPlace t : blockingPlaces) { |
4271 | + sb.append(t.toString() + "<br />"); |
4272 | + } |
4273 | + //JOptionPane.showMessageDialog(null, sb.toString()); |
4274 | + sb.append("</html>"); |
4275 | + tab.getAnimationController().getOkButton().setEnabled(false); |
4276 | + tab.getAnimationController().getOkButton().setToolTipText(sb.toString()); |
4277 | + } |
4278 | + } |
4279 | + } catch (ParseException | NumberFormatException e) { |
4280 | + tab.getAnimationController().getOkButton().setEnabled(false); |
4281 | + tab.getAnimationController().getOkButton().setToolTipText("The text in the input field is not a number"); |
4282 | + } |
4283 | + } |
4284 | + |
4285 | + private DataLayer activeGuiModel() { |
4286 | + return tab.currentTemplate().guiModel(); |
4287 | + } |
4288 | + |
4289 | + private void resethistory() { |
4290 | + actionHistory.clear(); |
4291 | + markings.clear(); |
4292 | + currentAction = -1; |
4293 | + currentMarkingIndex = 0; |
4294 | + tab.getAnimationHistorySidePanel().reset(); |
4295 | + if(tab.getUntimedAnimationHistory() != null){ |
4296 | + tab.getUntimedAnimationHistory().reset(); |
4297 | + } |
4298 | + } |
4299 | + |
4300 | + public FiringMode getFiringmode() { |
4301 | + return firingmode; |
4302 | + } |
4303 | + |
4304 | + // removes stored markings and actions from index "startWith" (included) |
4305 | + private void removeStoredActions(int startWith) { |
4306 | + int lastIndex = actionHistory.size() - 1; |
4307 | + for (int i = startWith; i <= lastIndex; i++) { |
4308 | + removeLastHistoryStep(); |
4309 | + } |
4310 | + } |
4311 | + |
4312 | + private void addMarking(TAPNNetworkTraceStep action, NetworkMarking marking) { |
4313 | + if (currentAction < actionHistory.size() - 1) { |
4314 | removeStoredActions(currentAction + 1); |
4315 | } |
4316 | |
4317 | - tab.network().setMarking(marking); |
4318 | - tab.getAnimationHistorySidePanel().addHistoryItem(action.toString()); |
4319 | - actionHistory.add(action); |
4320 | - markings.add(marking); |
4321 | - currentAction++; |
4322 | - currentMarkingIndex++; |
4323 | - } |
4324 | - |
4325 | - private void removeLastHistoryStep() { |
4326 | - actionHistory.remove(actionHistory.size() - 1); |
4327 | - markings.remove(markings.size() - 1); |
4328 | - } |
4329 | - |
4330 | - //XXX: should be enum? |
4331 | + tab.network().setMarking(marking); |
4332 | + tab.getAnimationHistorySidePanel().addHistoryItem(action.toString()); |
4333 | + actionHistory.add(action); |
4334 | + markings.add(marking); |
4335 | + currentAction++; |
4336 | + currentMarkingIndex++; |
4337 | + } |
4338 | + |
4339 | + private void removeLastHistoryStep() { |
4340 | + actionHistory.remove(actionHistory.size() - 1); |
4341 | + markings.remove(markings.size() - 1); |
4342 | + } |
4343 | + |
4344 | + //XXX: should be enum? |
4345 | public static final String[] FIRINGMODES = { "Random", "Oldest", "Youngest", "Manual" }; |
4346 | - public void setFiringmode(String t) { |
4347 | - switch (t) { |
4348 | - case "Random": |
4349 | - firingmode = new RandomFiringMode(); |
4350 | - break; |
4351 | - case "Youngest": |
4352 | - firingmode = new YoungestFiringMode(); |
4353 | - break; |
4354 | - case "Oldest": |
4355 | - firingmode = new OldestFiringMode(); |
4356 | - break; |
4357 | - case "Manual": |
4358 | - firingmode = null; |
4359 | - break; |
4360 | - default: |
4361 | - System.err |
4362 | - .println("Illegal firing mode mode: " + t + " not found."); |
4363 | - break; |
4364 | - } |
4365 | - |
4366 | - tab.getAnimationController().updateFiringModeComboBox(); |
4367 | - tab.getAnimationController().setToolTipText("Select a method for choosing tokens during transition firing"); |
4368 | - } |
4369 | - |
4370 | - enum FillListStatus{ |
4371 | - lessThanWeight, |
4372 | - weight, |
4373 | - moreThanWeight |
4374 | - } |
4375 | - |
4376 | - //Creates a list of tokens if there is only weight tokens in each of the places |
4377 | - //Used by getTokensToConsume |
4378 | - private FillListStatus fillList(TimedTransition transition, List<TimedToken> listToFill){ |
4379 | - for(TimedInputArc in: transition.getInputArcs()){ |
4380 | - List<TimedToken> elligibleTokens = in.getElligibleTokens(); |
4381 | - if(elligibleTokens.size() < in.getWeight().value()){ |
4382 | - return FillListStatus.lessThanWeight; |
4383 | - } else if(elligibleTokens.size() == in.getWeight().value()){ |
4384 | - listToFill.addAll(elligibleTokens); |
4385 | - } else { |
4386 | - return FillListStatus.moreThanWeight; |
4387 | - } |
4388 | - } |
4389 | - for(TransportArc in: transition.getTransportArcsGoingThrough()){ |
4390 | - List<TimedToken> elligibleTokens = in.getElligibleTokens(); |
4391 | - if(elligibleTokens.size() < in.getWeight().value()){ |
4392 | - return FillListStatus.lessThanWeight; |
4393 | - } else if(elligibleTokens.size() == in.getWeight().value()){ |
4394 | - listToFill.addAll(elligibleTokens); |
4395 | - } else { |
4396 | - return FillListStatus.moreThanWeight; |
4397 | - } |
4398 | - } |
4399 | - return FillListStatus.weight; |
4400 | - } |
4401 | - |
4402 | - private List<TimedToken> getTokensToConsume(TimedTransition transition){ |
4403 | - //If there are only "weight tokens in each place |
4404 | - List<TimedToken> result = new ArrayList<TimedToken>(); |
4405 | - boolean userShouldChoose = false; |
4406 | - if(transition.isShared()){ |
4407 | - for(TimedTransition t : transition.sharedTransition().transitions()){ |
4408 | - FillListStatus status = fillList(t, result); |
4409 | - if(status == FillListStatus.lessThanWeight){ |
4410 | - return null; |
4411 | - } else if(status == FillListStatus.moreThanWeight){ |
4412 | - userShouldChoose = true; |
4413 | - break; |
4414 | - } |
4415 | - } |
4416 | - } else { |
4417 | - FillListStatus status = fillList(transition, result); |
4418 | - if(status == FillListStatus.lessThanWeight){ |
4419 | - return null; |
4420 | - } else if(status == FillListStatus.moreThanWeight){ |
4421 | - userShouldChoose = true; |
4422 | - } |
4423 | - } |
4424 | - |
4425 | - if (userShouldChoose){ |
4426 | - return showSelectSimulatorDialogue(transition); |
4427 | - } else { |
4428 | - return result; |
4429 | - } |
4430 | - } |
4431 | - |
4432 | - private List<TimedToken> showSelectSimulatorDialogue(TimedTransition transition) { |
4433 | - EscapableDialog guiDialog = new EscapableDialog(CreateGui.getApp(), "Select Tokens", true); |
4434 | - |
4435 | - Container contentPane = guiDialog.getContentPane(); |
4436 | - contentPane.setLayout(new BoxLayout(contentPane, BoxLayout.PAGE_AXIS)); |
4437 | - AnimationTokenSelectDialog animationTokenSelectDialog = new AnimationTokenSelectDialog(transition); |
4438 | - contentPane.add(animationTokenSelectDialog); |
4439 | - guiDialog.setResizable(true); |
4440 | - |
4441 | - // Make window fit contents' preferred size |
4442 | - guiDialog.pack(); |
4443 | - |
4444 | - // Move window to the middle of the screen |
4445 | - guiDialog.setLocationRelativeTo(null); |
4446 | - guiDialog.setVisible(true); |
4447 | - |
4448 | - return animationTokenSelectDialog.getTokens(); |
4449 | - } |
4450 | - |
4451 | - public void reset(boolean keepInitial){ |
4452 | - resethistory(); |
4453 | - removeSetTrace(false); |
4454 | - if(keepInitial && initialMarking != null){ |
4455 | - markings.add(initialMarking); |
4456 | - tab.network().setMarking(initialMarking); |
4457 | - currentAction = -1; |
4458 | - updateFireableTransitions(); |
4459 | - } |
4460 | - } |
4461 | - |
4462 | - private boolean removeSetTrace(boolean askUser){ |
4463 | - if(askUser && isShowingTrace()){ //Warn about deleting trace |
4464 | - int answer = JOptionPane.showConfirmDialog(CreateGui.getApp(), |
4465 | - "You are about to remove the current trace.", |
4466 | - "Removing Trace", JOptionPane.OK_CANCEL_OPTION, JOptionPane.WARNING_MESSAGE); |
4467 | - if(answer != JOptionPane.OK_OPTION) return false; |
4468 | - } |
4469 | - if(isDisplayingUntimedTrace){ |
4470 | - tab.removeAbstractAnimationPane(); |
4471 | - } |
4472 | - isDisplayingUntimedTrace = false; |
4473 | - trace = null; |
4474 | - return true; |
4475 | - } |
4476 | - |
4477 | - public TimedTAPNNetworkTrace getTrace(){ |
4478 | - return (TimedTAPNNetworkTrace)trace; |
4479 | - } |
4480 | - |
4481 | - private boolean clearStepsForward(){ |
4482 | - boolean answer = true; |
4483 | - if(!isDisplayingUntimedTrace){ |
4484 | - answer = removeSetTrace(true); |
4485 | - } |
4486 | - if(answer){ |
4487 | - tab.getAnimationHistorySidePanel().clearStepsForward(); |
4488 | - } |
4489 | - return answer; |
4490 | - } |
4491 | - |
4492 | - private boolean isShowingTrace(){ |
4493 | - return isDisplayingUntimedTrace || trace != null; |
4494 | - } |
4495 | - |
4496 | - public ArrayList<TAPNNetworkTraceStep> getActionHistory() { |
4497 | - return actionHistory; |
4498 | - } |
4499 | + public void setFiringmode(String t) { |
4500 | + switch (t) { |
4501 | + case "Random": |
4502 | + firingmode = new RandomFiringMode(); |
4503 | + break; |
4504 | + case "Youngest": |
4505 | + firingmode = new YoungestFiringMode(); |
4506 | + break; |
4507 | + case "Oldest": |
4508 | + firingmode = new OldestFiringMode(); |
4509 | + break; |
4510 | + case "Manual": |
4511 | + firingmode = null; |
4512 | + break; |
4513 | + default: |
4514 | + System.err |
4515 | + .println("Illegal firing mode mode: " + t + " not found."); |
4516 | + break; |
4517 | + } |
4518 | + |
4519 | + tab.getAnimationController().updateFiringModeComboBox(); |
4520 | + tab.getAnimationController().setToolTipText("Select a method for choosing tokens during transition firing"); |
4521 | + } |
4522 | + |
4523 | + enum FillListStatus{ |
4524 | + lessThanWeight, |
4525 | + weight, |
4526 | + moreThanWeight |
4527 | + } |
4528 | + |
4529 | + //Creates a list of tokens if there is only weight tokens in each of the places |
4530 | + //Used by getTokensToConsume |
4531 | + private FillListStatus fillList(TimedTransition transition, List<TimedToken> listToFill){ |
4532 | + for(TimedInputArc in: transition.getInputArcs()){ |
4533 | + List<TimedToken> elligibleTokens = in.getElligibleTokens(); |
4534 | + if(elligibleTokens.size() < in.getWeight().value()){ |
4535 | + return FillListStatus.lessThanWeight; |
4536 | + } else if(elligibleTokens.size() == in.getWeight().value()){ |
4537 | + listToFill.addAll(elligibleTokens); |
4538 | + } else { |
4539 | + return FillListStatus.moreThanWeight; |
4540 | + } |
4541 | + } |
4542 | + for(TransportArc in: transition.getTransportArcsGoingThrough()){ |
4543 | + List<TimedToken> elligibleTokens = in.getElligibleTokens(); |
4544 | + if(elligibleTokens.size() < in.getWeight().value()){ |
4545 | + return FillListStatus.lessThanWeight; |
4546 | + } else if(elligibleTokens.size() == in.getWeight().value()){ |
4547 | + listToFill.addAll(elligibleTokens); |
4548 | + } else { |
4549 | + return FillListStatus.moreThanWeight; |
4550 | + } |
4551 | + } |
4552 | + return FillListStatus.weight; |
4553 | + } |
4554 | + |
4555 | + private List<TimedToken> getTokensToConsume(TimedTransition transition){ |
4556 | + //If there are only "weight tokens in each place |
4557 | + List<TimedToken> result = new ArrayList<TimedToken>(); |
4558 | + boolean userShouldChoose = false; |
4559 | + if(transition.isShared()){ |
4560 | + for(TimedTransition t : transition.sharedTransition().transitions()){ |
4561 | + FillListStatus status = fillList(t, result); |
4562 | + if(status == FillListStatus.lessThanWeight){ |
4563 | + return null; |
4564 | + } else if(status == FillListStatus.moreThanWeight){ |
4565 | + userShouldChoose = true; |
4566 | + break; |
4567 | + } |
4568 | + } |
4569 | + } else { |
4570 | + FillListStatus status = fillList(transition, result); |
4571 | + if(status == FillListStatus.lessThanWeight){ |
4572 | + return null; |
4573 | + } else if(status == FillListStatus.moreThanWeight){ |
4574 | + userShouldChoose = true; |
4575 | + } |
4576 | + } |
4577 | + |
4578 | + if (userShouldChoose){ |
4579 | + return showSelectSimulatorDialogue(transition); |
4580 | + } else { |
4581 | + return result; |
4582 | + } |
4583 | + } |
4584 | + |
4585 | + private List<TimedToken> showSelectSimulatorDialogue(TimedTransition transition) { |
4586 | + EscapableDialog guiDialog = new EscapableDialog(CreateGui.getApp(), "Select Tokens", true); |
4587 | + |
4588 | + Container contentPane = guiDialog.getContentPane(); |
4589 | + contentPane.setLayout(new BoxLayout(contentPane, BoxLayout.PAGE_AXIS)); |
4590 | + AnimationTokenSelectDialog animationSelectmodeDialog = new AnimationTokenSelectDialog(transition); |
4591 | + contentPane.add(animationSelectmodeDialog); |
4592 | + guiDialog.setResizable(true); |
4593 | + |
4594 | + // Make window fit contents' preferred size |
4595 | + guiDialog.pack(); |
4596 | + |
4597 | + // Move window to the middle of the screen |
4598 | + guiDialog.setLocationRelativeTo(null); |
4599 | + guiDialog.setVisible(true); |
4600 | + |
4601 | + return animationSelectmodeDialog.getTokens(); |
4602 | + } |
4603 | + |
4604 | + public void reset(boolean keepInitial){ |
4605 | + resethistory(); |
4606 | + removeSetTrace(false); |
4607 | + if(keepInitial && initialMarking != null){ |
4608 | + markings.add(initialMarking); |
4609 | + tab.network().setMarking(initialMarking); |
4610 | + currentAction = -1; |
4611 | + updateFireableTransitions(); |
4612 | + } |
4613 | + } |
4614 | + |
4615 | + private boolean removeSetTrace(boolean askUser){ |
4616 | + if(askUser && isShowingTrace()){ //Warn about deleting trace |
4617 | + int answer = JOptionPane.showConfirmDialog(CreateGui.getApp(), |
4618 | + "You are about to remove the current trace.", |
4619 | + "Removing Trace", JOptionPane.OK_CANCEL_OPTION, JOptionPane.WARNING_MESSAGE); |
4620 | + if(answer != JOptionPane.OK_OPTION) return false; |
4621 | + } |
4622 | + if(isDisplayingUntimedTrace){ |
4623 | + tab.removeAbstractAnimationPane(); |
4624 | + } |
4625 | + isDisplayingUntimedTrace = false; |
4626 | + trace = null; |
4627 | + return true; |
4628 | + } |
4629 | + |
4630 | + public TimedTAPNNetworkTrace getTrace(){ |
4631 | + return (TimedTAPNNetworkTrace)trace; |
4632 | + } |
4633 | + |
4634 | + private boolean clearStepsForward(){ |
4635 | + boolean answer = true; |
4636 | + if(!isDisplayingUntimedTrace){ |
4637 | + answer = removeSetTrace(true); |
4638 | + } |
4639 | + if(answer){ |
4640 | + tab.getAnimationHistorySidePanel().clearStepsForward(); |
4641 | + } |
4642 | + return answer; |
4643 | + } |
4644 | + |
4645 | + private boolean isShowingTrace(){ |
4646 | + return isDisplayingUntimedTrace || trace != null; |
4647 | + } |
4648 | + |
4649 | + public ArrayList<TAPNNetworkTraceStep> getActionHistory() { |
4650 | + return actionHistory; |
4651 | + } |
4652 | |
4653 | |
4654 | private void setEnabledStepbackwardAction(boolean b) { |
4655 | stepbackwardAction.setEnabled(b); |
4656 | - |
4657 | } |
4658 | |
4659 | private void setEnabledStepforwardAction(boolean b) { |
4660 | stepforwardAction.setEnabled(b); |
4661 | + } |
4662 | |
4663 | - } |
4664 | public final GuiAction stepforwardAction = CreateGui.getAppGui().stepforwardAction; |
4665 | public final GuiAction stepbackwardAction = CreateGui.getAppGui().stepbackwardAction; |
4666 | |
4667 | @@ -703,8 +692,6 @@ |
4668 | |
4669 | } |
4670 | |
4671 | - /* GUI Model / Actions helpers */ |
4672 | - //XXX: Should be moved to animationController or similar |
4673 | /** |
4674 | * Updates the mouseOver label showing token ages in animationmode |
4675 | * when a "animation" action is happening. "live updates" any mouseOver label |
4676 | @@ -717,4 +704,5 @@ |
4677 | } |
4678 | } |
4679 | } |
4680 | + |
4681 | } |
4682 | |
4683 | === modified file 'src/pipe/gui/CreateGui.java' |
4684 | --- src/pipe/gui/CreateGui.java 2020-05-27 13:07:27 +0000 |
4685 | +++ src/pipe/gui/CreateGui.java 2020-07-09 12:55:48 +0000 |
4686 | @@ -14,16 +14,14 @@ |
4687 | |
4688 | public class CreateGui { |
4689 | |
4690 | - private static GuiFrame appGui; |
4691 | - private static GuiFrameController appGuiController; |
4692 | + private final static GuiFrame appGui = new GuiFrame(TAPAAL.getProgramName()); |
4693 | + private final static GuiFrameController appGuiController = new GuiFrameController(appGui); |
4694 | |
4695 | - private static ArrayList<TabContent> tabs = new ArrayList<TabContent>(); |
4696 | + private static final ArrayList<TabContent> tabs = new ArrayList<TabContent>(); |
4697 | |
4698 | public static void init() { |
4699 | - appGui = new GuiFrame(TAPAAL.getProgramName()); |
4700 | - appGuiController = new GuiFrameController(appGui); |
4701 | |
4702 | - if (Platform.isMac()){ |
4703 | + if (Platform.isMac()){ |
4704 | try { |
4705 | SpecialMacHandler.postprocess(); |
4706 | } catch (NoClassDefFoundError e) { |
4707 | @@ -37,8 +35,7 @@ |
4708 | |
4709 | @Deprecated |
4710 | public static DataLayer getModel() { |
4711 | - if (appGui==null) return null; |
4712 | - return getModel(appGui.getSelectedTabIndex()); |
4713 | + return getModel(appGui.getSelectedTabIndex()); |
4714 | } |
4715 | |
4716 | @Deprecated |
4717 | @@ -140,4 +137,6 @@ |
4718 | } |
4719 | |
4720 | |
4721 | + public static boolean useExtendedBounds = false; |
4722 | + |
4723 | } |
4724 | |
4725 | === modified file 'src/pipe/gui/DelayEnabledTransitionControl.java' |
4726 | --- src/pipe/gui/DelayEnabledTransitionControl.java 2020-05-18 14:33:45 +0000 |
4727 | +++ src/pipe/gui/DelayEnabledTransitionControl.java 2020-07-09 12:55:48 +0000 |
4728 | @@ -30,11 +30,11 @@ |
4729 | private static BigDecimal defaultGranularity = new BigDecimal("0.1"); |
4730 | private static boolean defaultIsRandomTrasition; |
4731 | |
4732 | - private JLabel precitionLabel; |
4733 | - private JSlider delayEnabledPrecision; |
4734 | - private JLabel delayModeLabel; |
4735 | - private JComboBox<DelayMode> delayMode; |
4736 | - JCheckBox randomMode; |
4737 | + private final JLabel precitionLabel; |
4738 | + private final JSlider delayEnabledPrecision; |
4739 | + private final JLabel delayModeLabel; |
4740 | + private final JComboBox<DelayMode> delayMode; |
4741 | + final JCheckBox randomMode = new JCheckBox("Choose next transition randomly"); |
4742 | |
4743 | private DelayEnabledTransitionControl() { |
4744 | super(new GridBagLayout()); |
4745 | @@ -61,9 +61,8 @@ |
4746 | DelayMode[] items = {ShortestDelayMode.getInstance(), RandomDelayMode.getInstance(), ManualDelayMode.getInstance()}; |
4747 | delayMode = new JComboBox(items); |
4748 | setDelayMode(defaultDelayMode); |
4749 | - |
4750 | - randomMode = new JCheckBox("Choose next transition randomly"); |
4751 | - setRandomTransitionMode(defaultIsRandomTrasition); |
4752 | + |
4753 | + setRandomTransitionMode(defaultIsRandomTrasition); |
4754 | |
4755 | GridBagConstraints gbc = new GridBagConstraints(); |
4756 | gbc.gridwidth = 2; |
4757 | |
4758 | === modified file 'src/pipe/gui/GuiFrame.java' |
4759 | --- src/pipe/gui/GuiFrame.java 2020-06-22 08:06:22 +0000 |
4760 | +++ src/pipe/gui/GuiFrame.java 2020-07-09 12:55:48 +0000 |
4761 | @@ -40,1103 +40,1175 @@ |
4762 | import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNDiscreteVerification; |
4763 | |
4764 | |
4765 | -public class GuiFrame extends JFrame implements GuiFrameActions, SafeGuiFrameActions { |
4766 | - |
4767 | - // for zoom combobox and dropdown |
4768 | - private final int[] zoomLevels = { 40, 60, 80, 100, 120, 140, 160, 180, 200, 300 }; |
4769 | - |
4770 | - private String frameTitle; |
4771 | - |
4772 | - private Pipe.ElementType mode; |
4773 | - |
4774 | - private int newNameCounter = 1; |
4775 | - |
4776 | - final MutableReference<GuiFrameControllerActions> guiFrameController = new MutableReference<>(); |
4777 | - |
4778 | - private ExtendedJTabbedPane<TabContent> appTab; |
4779 | - |
4780 | - private StatusBar statusBar; |
4781 | - private JMenuBar menuBar; |
4782 | - private JToolBar drawingToolBar; |
4783 | - private JComboBox<String> zoomComboBox; |
4784 | - |
4785 | - private GuiAction createAction; |
4786 | - private GuiAction openAction; |
4787 | - private GuiAction closeAction; |
4788 | - private GuiAction saveAction; |
4789 | - private GuiAction saveAsAction; |
4790 | - private GuiAction exitAction; |
4791 | - private GuiAction printAction; |
4792 | - private GuiAction importPNMLAction; |
4793 | - private GuiAction importSUMOAction; |
4794 | - private GuiAction importXMLAction; |
4795 | - private GuiAction exportPNGAction; |
4796 | - private GuiAction exportPSAction; |
4797 | - private GuiAction exportToTikZAction; |
4798 | - private GuiAction exportToPNMLAction; |
4799 | - private GuiAction exportToXMLAction; |
4800 | - private GuiAction exportTraceAction; |
4801 | - private GuiAction importTraceAction; |
4802 | - private GuiAction exportBatchAction; |
4803 | - |
4804 | - private GuiAction /* copyAction, cutAction, pasteAction, */undoAction, redoAction; |
4805 | - private GuiAction toggleGrid; |
4806 | - private GuiAction alignToGrid; |
4807 | - private GuiAction netStatisticsAction; |
4808 | - private GuiAction batchProcessingAction; |
4809 | - private GuiAction engineSelectionAction; |
4810 | - private GuiAction clearPreferencesAction; |
4811 | - |
4812 | - private GuiAction verifyAction; |
4813 | - private GuiAction workflowDialogAction; |
4814 | - private GuiAction smartDrawAction; |
4815 | - private GuiAction mergeComponentsDialogAction; |
4816 | - private GuiAction stripTimeDialogAction; |
4817 | - |
4818 | - private GuiAction zoomOutAction; |
4819 | - private GuiAction zoomInAction; |
4820 | - private GuiAction zoomToAction; |
4821 | - |
4822 | - private GuiAction incSpacingAction; |
4823 | - private GuiAction decSpacingAction; |
4824 | - public GuiAction deleteAction; |
4825 | - |
4826 | - private GuiAction annotationAction; |
4827 | - private GuiAction inhibarcAction; |
4828 | - private GuiAction transAction; |
4829 | - private GuiAction tokenAction; |
4830 | - private GuiAction selectAction; |
4831 | - private GuiAction deleteTokenAction; |
4832 | - private GuiAction timedPlaceAction; |
4833 | - |
4834 | - private GuiAction timedArcAction; |
4835 | - private GuiAction transportArcAction; |
4836 | - |
4837 | - private GuiAction showTokenAgeAction; |
4838 | - private GuiAction showComponentsAction; |
4839 | - private GuiAction showSharedPTAction; |
4840 | - private GuiAction showQueriesAction; |
4841 | - private GuiAction showConstantsAction; |
4842 | - private GuiAction showZeroToInfinityIntervalsAction; |
4843 | - private GuiAction showEnabledTransitionsAction; |
4844 | - private GuiAction showDelayEnabledTransitionsAction; |
4845 | - private GuiAction showToolTipsAction; |
4846 | - private GuiAction showAdvancedWorkspaceAction; |
4847 | - private GuiAction showSimpleWorkspaceAction; |
4848 | - private GuiAction saveWorkSpaceAction; |
4849 | - private GuiAction showAboutAction; |
4850 | - private GuiAction showHomepage; |
4851 | - private GuiAction showAskQuestionAction; |
4852 | - private GuiAction showReportBugAction; |
4853 | - private GuiAction showFAQAction; |
4854 | - private GuiAction checkUpdate; |
4855 | - |
4856 | - |
4857 | - private GuiAction selectAllAction; |
4858 | - |
4859 | - private GuiAction startAction; |
4860 | - public GuiAction stepforwardAction; |
4861 | - public GuiAction stepbackwardAction; |
4862 | - private GuiAction timeAction; |
4863 | - private GuiAction delayFireAction; |
4864 | - private GuiAction prevcomponentAction; |
4865 | - private GuiAction nextcomponentAction; |
4866 | - |
4867 | - public enum GUIMode { |
4868 | - draw, animation, noNet |
4869 | - } |
4870 | - |
4871 | - private JCheckBoxMenuItem showZeroToInfinityIntervalsCheckBox; |
4872 | - private JCheckBoxMenuItem showTokenAgeCheckBox; |
4873 | - |
4874 | - private JMenu zoomMenu; |
4875 | - |
4876 | - public GuiFrame(String title) { |
4877 | - // HAK-arrange for frameTitle to be initialized and the default file |
4878 | - // name to be appended to basic window title |
4879 | - |
4880 | - frameTitle = title; |
4881 | - setTitle(null); |
4882 | - trySetLookAndFeel(); |
4883 | - |
4884 | - Dimension screenSize = Toolkit.getDefaultToolkit().getScreenSize(); |
4885 | - this.setSize(screenSize.width * 80 / 100, screenSize.height * 80 / 100); |
4886 | - this.setLocationRelativeTo(null); |
4887 | - this.setMinimumSize(new Dimension(825, 480)); |
4888 | - |
4889 | - setDefaultCloseOperation(DO_NOTHING_ON_CLOSE); |
4890 | - |
4891 | - //XXX: Moved appTab from creategui needs further refacotring |
4892 | - //kyrke 2018-05-20 |
4893 | - appTab = new ExtendedJTabbedPane<TabContent>() { |
4894 | - @Override |
4895 | - public Component generator() { |
4896 | - return new TabComponent(this) { |
4897 | +public class GuiFrame extends JFrame implements GuiFrameActions, SafeGuiFrameActions { |
4898 | + |
4899 | + // for zoom combobox and dropdown |
4900 | + private final int[] zoomLevels = {40, 60, 80, 100, 120, 140, 160, 180, 200, 300}; |
4901 | + |
4902 | + private String frameTitle; |
4903 | + |
4904 | + private Pipe.ElementType mode; |
4905 | + |
4906 | + private int newNameCounter = 1; |
4907 | + |
4908 | + final MutableReference<GuiFrameControllerActions> guiFrameController = new MutableReference<>(); |
4909 | + |
4910 | + private ExtendedJTabbedPane<TabContent> appTab; |
4911 | + |
4912 | + private StatusBar statusBar; |
4913 | + private JMenuBar menuBar; |
4914 | + private JToolBar drawingToolBar; |
4915 | + private JComboBox<String> zoomComboBox; |
4916 | + |
4917 | + private static final int shortcutkey = Toolkit.getDefaultToolkit().getMenuShortcutKeyMask(); |
4918 | + |
4919 | + private final GuiAction createAction = new GuiAction("New", "Create a new Petri net", KeyStroke.getKeyStroke('N', shortcutkey)) { |
4920 | + public void actionPerformed(ActionEvent arg0) { |
4921 | + guiFrameController.ifPresent(GuiFrameControllerActions::showNewPNDialog); |
4922 | + } |
4923 | + }; |
4924 | + private final GuiAction openAction = new GuiAction("Open", "Open", KeyStroke.getKeyStroke('O', shortcutkey)) { |
4925 | + public void actionPerformed(ActionEvent arg0) { |
4926 | + guiFrameController.ifPresent(GuiFrameControllerActions::openTAPNFile); |
4927 | + } |
4928 | + }; |
4929 | + private final GuiAction closeAction = new GuiAction("Close", "Close the current tab", KeyStroke.getKeyStroke('W', shortcutkey)) { |
4930 | + public void actionPerformed(ActionEvent arg0) { |
4931 | + TabContent index = (TabContent) appTab.getSelectedComponent(); |
4932 | + guiFrameController.ifPresent(o -> o.closeTab(index)); |
4933 | + } |
4934 | + }; |
4935 | + private final GuiAction saveAction = new GuiAction("Save", "Save", KeyStroke.getKeyStroke('S', shortcutkey)) { |
4936 | + public void actionPerformed(ActionEvent arg0) { |
4937 | + if (canNetBeSavedAndShowMessage()) { |
4938 | + guiFrameController.ifPresent(GuiFrameControllerActions::save); |
4939 | + } |
4940 | + } |
4941 | + }; |
4942 | + private final GuiAction saveAsAction = new GuiAction("Save as", "Save as...", KeyStroke.getKeyStroke('S', (shortcutkey + InputEvent.SHIFT_MASK))) { |
4943 | + public void actionPerformed(ActionEvent arg0) { |
4944 | + if (canNetBeSavedAndShowMessage()) { |
4945 | + guiFrameController.ifPresent(GuiFrameControllerActions::saveAs); |
4946 | + } |
4947 | + } |
4948 | + }; |
4949 | + private final GuiAction exitAction = new GuiAction("Exit", "Close the program", KeyStroke.getKeyStroke('Q', shortcutkey)) { |
4950 | + public void actionPerformed(ActionEvent arg0) { |
4951 | + guiFrameController.ifPresent(GuiFrameControllerActions::exit); |
4952 | + } |
4953 | + }; |
4954 | + private final GuiAction printAction = new GuiAction("Print", "Print", KeyStroke.getKeyStroke('P', shortcutkey)) { |
4955 | + public void actionPerformed(ActionEvent arg0) { |
4956 | + Export.exportGuiView(getCurrentTab().drawingSurface(), Export.PRINTER, null); |
4957 | + } |
4958 | + }; |
4959 | + private final GuiAction importPNMLAction = new GuiAction("PNML untimed net", "Import an untimed net in the PNML format", KeyStroke.getKeyStroke('X', shortcutkey)) { |
4960 | + public void actionPerformed(ActionEvent arg0) { |
4961 | + guiFrameController.ifPresent(GuiFrameControllerActions::importPNMLFile); |
4962 | + } |
4963 | + }; |
4964 | + private final GuiAction importSUMOAction = new GuiAction("SUMO queries (.txt)", "Import SUMO queries in a plain text format") { |
4965 | + public void actionPerformed(ActionEvent arg0) { |
4966 | + currentTab.ifPresent(TabContentActions::importSUMOQueries); |
4967 | + } |
4968 | + }; |
4969 | + private final GuiAction importXMLAction = new GuiAction("XML queries (.xml)", "Import MCC queries in XML format", KeyStroke.getKeyStroke('R', shortcutkey)) { |
4970 | + public void actionPerformed(ActionEvent arg0) { |
4971 | + currentTab.ifPresent(TabContentActions::importXMLQueries); |
4972 | + } |
4973 | + }; |
4974 | + private final GuiAction exportPNGAction = new GuiAction("PNG", "Export the net to PNG format", KeyStroke.getKeyStroke('G', shortcutkey)) { |
4975 | + public void actionPerformed(ActionEvent arg0) { |
4976 | + if (canNetBeSavedAndShowMessage()) { |
4977 | + Export.exportGuiView(getCurrentTab().drawingSurface(), Export.PNG, null); |
4978 | + } |
4979 | + } |
4980 | + }; |
4981 | + private final GuiAction exportPSAction = new GuiAction("PostScript", "Export the net to PostScript format", KeyStroke.getKeyStroke('T', shortcutkey)) { |
4982 | + public void actionPerformed(ActionEvent arg0) { |
4983 | + if (canNetBeSavedAndShowMessage()) { |
4984 | + Export.exportGuiView(getCurrentTab().drawingSurface(), Export.POSTSCRIPT, null); |
4985 | + } |
4986 | + } |
4987 | + }; |
4988 | + private final GuiAction exportToTikZAction = new GuiAction("TikZ", "Export the net to LaTex (TikZ) format", KeyStroke.getKeyStroke('L', shortcutkey)) { |
4989 | + public void actionPerformed(ActionEvent arg0) { |
4990 | + if (canNetBeSavedAndShowMessage()) { |
4991 | + Export.exportGuiView(getCurrentTab().drawingSurface(), Export.TIKZ, getCurrentTab().drawingSurface().getGuiModel()); |
4992 | + } |
4993 | + } |
4994 | + }; |
4995 | + private final GuiAction exportToPNMLAction = new GuiAction("PNML", "Export the net to PNML format", KeyStroke.getKeyStroke('D', shortcutkey)) { |
4996 | + public void actionPerformed(ActionEvent arg0) { |
4997 | + if (canNetBeSavedAndShowMessage()) { |
4998 | + if (Preferences.getInstance().getShowPNMLWarning()) { |
4999 | + JCheckBox showAgain = new JCheckBox("Do not show this warning."); |
5000 | + String message = "In the saved PNML all timing information will be lost\n" + |
This branch fixes stuff related to drawing and animation; we should test nothing unexpected is broken.
Bugfixes:
- Clearify text in manual select token menu #1883974
- Fixed undo/redo of objects moved at differnt zoom than current
- Fixed adding arcpah point (menu or double click) at zoom differnt than 100
- Fixed an issue archpath endpoint could be moved.
Changes:
Animation:
- Updated now enabled transitions are calculated, now have one function that calculates and update components.
- Enabledness i no longer saved in TranstionComponents (dispatches to model)
- Moved code needed to setup animation from TabContent to the animation controller
- Renamed animation components to clarify behavior
-
Drawing:
- Moved drawing of place/transitions arcs and notes to new controller (CanvasController)
- Updated calulation of arc angles (between objecs) from using tan to use atan2, this also fixes an exception thrown when two objecs are very close.
- Made a number of members final
- Pushed members in Local/Shared Time Places up (to share code)
- Added a new function a add X tokens to a place (insted of having to create a new token and add them in a loop)
- Added tests for loading tokens
- Added new type GraphicalElement that is added to Canvas, for now PetriNetObject exstendes GraphicalElmenet, but then can later be split
- setNetwork in a tab is now removed an a network set via constructor
- labels Offset is not saved in unzoom coords
- arcpath poins are not created uning unzoomed coords