Merge lp:~yrke/tapaal/cleanup-PNO-namingAndInterface into lp:tapaal

Proposed by Kenneth Yrke Jørgensen
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
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
To post a comment you must log in.
Revision history for this message
Kenneth Yrke Jørgensen (yrke) wrote :

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

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

Revision history for this message
Peter Haahr Taankvist (ptaank) wrote :

Open alternating-bit-protocol-components. Zoom in full -> Press Ctrl+U 3 times -> zoom out to 100%. Now the Annotation Note is placed weirdly. Additionally, press ctrl+z 3 times, and it is still placed weirdly, until we zoom again.

Revision history for this message
Peter Haahr Taankvist (ptaank) wrote :

The problem with pressing shift+U many times still persists:

Open alternating-bit-protocol-components

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.

Revision history for this message
Peter Haahr Taankvist (ptaank) wrote :

> The problem with pressing shift+U many times still persists:
>
> Open alternating-bit-protocol-components
>
> 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

Revision history for this message
Peter Haahr Taankvist (ptaank) wrote :

It is not possible to undo resizing of annotation notes

Revision history for this message
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.

review: Needs Fixing
Revision history for this message
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.

Revision history for this message
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.

Revision history for this message
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

Revision history for this message
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.

review: Needs Resubmitting
Revision history for this message
Lena Ernstsen (lsaid) :
review: Approve
Revision history for this message
Peter Haahr Taankvist (ptaank) :
review: Approve
Revision history for this message
Jiri Srba (srba) :
review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/dk/aau/cs/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" +
The diff has been truncated for viewing.

Subscribers

People subscribed via source and target branches