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
=== modified file 'src/dk/aau/cs/gui/SharedPlacesAndTransitionsPanel.java'
--- src/dk/aau/cs/gui/SharedPlacesAndTransitionsPanel.java 2020-05-27 13:15:44 +0000
+++ src/dk/aau/cs/gui/SharedPlacesAndTransitionsPanel.java 2020-07-09 12:55:48 +0000
@@ -45,17 +45,17 @@
45 private static final String TRANSITIONS = "Transitions";45 private static final String TRANSITIONS = "Transitions";
46 private static final String PLACES = "Places";46 private static final String PLACES = "Places";
4747
48 private JList list;48 private final JList list = new NonsearchableJList();
49 private SharedPlacesListModel sharedPlacesListModel;49 private final SharedPlacesListModel sharedPlacesListModel;
50 private SharedTransitionsListModel sharedTransitionsListModel;50 private final SharedTransitionsListModel sharedTransitionsListModel;
51 private JComboBox placesTransitionsComboBox;51 private final JComboBox placesTransitionsComboBox = new JComboBox(new String[]{ PLACES, TRANSITIONS });
52 private UndoManager undoManager;52 private final UndoManager undoManager;
53 private NameGenerator nameGenerator;53 private final NameGenerator nameGenerator;
54 private TabContent tab;54 private final TabContent tab;
5555
56 private JButton renameButton = new JButton("Rename");56 private final JButton renameButton = new JButton("Rename");
57 private JButton removeButton = new JButton("Remove");57 private final JButton removeButton = new JButton("Remove");
58 private JButton addButton = new JButton("New");58 private final JButton addButton = new JButton("New");
59 private JButton moveUpButton;59 private JButton moveUpButton;
60 private JButton moveDownButton;60 private JButton moveDownButton;
61 private JButton sortButton;61 private JButton sortButton;
@@ -128,9 +128,8 @@
128128
129 private void initComponents() {129 private void initComponents() {
130 JPanel listPanel = new JPanel(new GridBagLayout());130 JPanel listPanel = new JPanel(new GridBagLayout());
131 131
132 list = new NonsearchableJList();132 list.addListSelectionListener(new ListSelectionListener() {
133 list.addListSelectionListener(new ListSelectionListener() {
134 public void valueChanged(ListSelectionEvent e) {133 public void valueChanged(ListSelectionEvent e) {
135 if(!e.getValueIsAdjusting()){134 if(!e.getValueIsAdjusting()){
136 JList source = (JList)e.getSource();135 JList source = (JList)e.getSource();
@@ -262,9 +261,8 @@
262 gbc.fill = GridBagConstraints.HORIZONTAL;261 gbc.fill = GridBagConstraints.HORIZONTAL;
263 gbc.anchor = GridBagConstraints.NORTH;262 gbc.anchor = GridBagConstraints.NORTH;
264 listPanel.add(sortButton,gbc);263 listPanel.add(sortButton,gbc);
265 264
266 placesTransitionsComboBox = new JComboBox(new String[]{ PLACES, TRANSITIONS });265 placesTransitionsComboBox.setToolTipText(toolTipChangeBetweenPlacesAndTransitions);
267 placesTransitionsComboBox.setToolTipText(toolTipChangeBetweenPlacesAndTransitions);
268 placesTransitionsComboBox.addActionListener(e -> {266 placesTransitionsComboBox.addActionListener(e -> {
269 JComboBox source = (JComboBox)e.getSource();267 JComboBox source = (JComboBox)e.getSource();
270 String selectedItem = (String)source.getSelectedItem();268 String selectedItem = (String)source.getSelectedItem();
271269
=== modified file 'src/dk/aau/cs/gui/TabContent.java'
--- src/dk/aau/cs/gui/TabContent.java 2020-06-22 07:41:12 +0000
+++ src/dk/aau/cs/gui/TabContent.java 2020-07-09 12:55:48 +0000
@@ -3,6 +3,7 @@
3import java.awt.*;3import java.awt.*;
4import java.awt.event.MouseAdapter;4import java.awt.event.MouseAdapter;
5import java.awt.event.MouseEvent;5import java.awt.event.MouseEvent;
6import java.awt.geom.Point2D;
6import java.io.*;7import java.io.*;
7import java.math.BigDecimal;8import java.math.BigDecimal;
8import java.util.*;9import java.util.*;
@@ -11,12 +12,11 @@
11import javax.swing.*;12import javax.swing.*;
12import javax.swing.border.BevelBorder;13import javax.swing.border.BevelBorder;
1314
14import dk.aau.cs.approximation.OverApproximation;
15import dk.aau.cs.approximation.UnderApproximation;
16import dk.aau.cs.debug.Logger;15import dk.aau.cs.debug.Logger;
17import dk.aau.cs.gui.components.StatisticsPanel;16import dk.aau.cs.gui.components.StatisticsPanel;
18import dk.aau.cs.gui.undo.Command;17import dk.aau.cs.gui.undo.Command;
19import dk.aau.cs.gui.undo.DeleteQueriesCommand;18import dk.aau.cs.gui.undo.DeleteQueriesCommand;
19import dk.aau.cs.gui.undo.TimedPlaceMarkingEdit;
20import dk.aau.cs.io.*;20import dk.aau.cs.io.*;
21import dk.aau.cs.io.queries.SUMOQueryLoader;21import dk.aau.cs.io.queries.SUMOQueryLoader;
22import dk.aau.cs.io.queries.XMLQueryLoader;22import dk.aau.cs.io.queries.XMLQueryLoader;
@@ -35,12 +35,13 @@
35import pipe.gui.*;35import pipe.gui.*;
36import pipe.gui.canvas.DrawingSurfaceImpl;36import pipe.gui.canvas.DrawingSurfaceImpl;
37import pipe.gui.graphicElements.*;37import pipe.gui.graphicElements.*;
38import pipe.gui.graphicElements.tapn.TimedPlaceComponent;38import pipe.gui.graphicElements.tapn.*;
39import pipe.gui.graphicElements.tapn.TimedTransitionComponent;39import pipe.gui.undo.*;
40import pipe.gui.handler.PlaceTransitionObjectHandler;40import pipe.gui.widgets.ConstantsPane;
41import pipe.gui.undo.ChangeSpacingEdit;41import pipe.gui.undo.ChangeSpacingEdit;
42import pipe.gui.undo.UndoManager;42import pipe.gui.undo.UndoManager;
43import pipe.gui.widgets.*;43import pipe.gui.widgets.*;
44
44import net.tapaal.swinghelpers.JSplitPaneFix;45import net.tapaal.swinghelpers.JSplitPaneFix;
45import dk.aau.cs.gui.components.BugHandledJXMultisplitPane;46import dk.aau.cs.gui.components.BugHandledJXMultisplitPane;
46import dk.aau.cs.gui.components.TransitionFireingComponent;47import dk.aau.cs.gui.components.TransitionFireingComponent;
@@ -49,37 +50,443 @@
4950
50public class TabContent extends JSplitPane implements TabContentActions{51public class TabContent extends JSplitPane implements TabContentActions{
5152
53 static class TAPNLens {
54 public boolean isTimed() {
55 return timed;
56 }
57
58 public boolean isGame() {
59 return game;
60 }
61
62 private final boolean timed;
63 private final boolean game;
64
65 TAPNLens(boolean timed, boolean game) {
66 this.timed = timed;
67 this.game = game;
68 }
69 }
70 private final TAPNLens lens;
71
52 //Model and state72 //Model and state
53 private TimedArcPetriNetNetwork tapnNetwork = new TimedArcPetriNetNetwork();73 private final TimedArcPetriNetNetwork tapnNetwork;
54 private HashMap<TimedArcPetriNet, DataLayer> guiModels = new HashMap<TimedArcPetriNet, DataLayer>();74
55 private HashMap<TimedArcPetriNet, Zoomer> zoomLevels = new HashMap<TimedArcPetriNet, Zoomer>();75 //XXX: Replace with bi-map
5676 private final HashMap<TimedArcPetriNet, DataLayer> guiModels = new HashMap<TimedArcPetriNet, DataLayer>();
5777 private final HashMap<DataLayer, TimedArcPetriNet> guiModelToModel = new HashMap<>();
58 private UndoManager undoManager = new UndoManager();78
79 private final HashMap<TimedArcPetriNet, Zoomer> zoomLevels = new HashMap<TimedArcPetriNet, Zoomer>();
80
81
82 private final UndoManager undoManager = new UndoManager();
83
84 public final GuiModelManager guiModelManager = new GuiModelManager();
85 public class GuiModelManager {
86 public GuiModelManager(){
87
88 }
89
90 public void addNewTimedPlace(DataLayer c, Point p){
91 Require.notNull(c, "datalyer can't be null");
92 Require.notNull(p, "Point can't be null");
93
94 dk.aau.cs.model.tapn.LocalTimedPlace tp = new dk.aau.cs.model.tapn.LocalTimedPlace(drawingSurface.getNameGenerator().getNewPlaceName(guiModelToModel.get(c)));
95 TimedPlaceComponent pnObject = new TimedPlaceComponent(p.x, p.y, tp);
96 guiModelToModel.get(c).add(tp);
97 c.addPetriNetObject(pnObject);
98
99 getUndoManager().addNewEdit(new AddTimedPlaceCommand(pnObject, guiModelToModel.get(c), c));
100
101 }
102
103 public void addNewTimedTransitions(DataLayer c, Point p) {
104 dk.aau.cs.model.tapn.TimedTransition transition = new dk.aau.cs.model.tapn.TimedTransition(drawingSurface.getNameGenerator().getNewTransitionName(guiModelToModel.get(c)));
105
106 TimedTransitionComponent pnObject = new TimedTransitionComponent(p.x, p.y, transition);
107
108 guiModelToModel.get(c).add(transition);
109 c.addPetriNetObject(pnObject);
110
111 getUndoManager().addNewEdit(new AddTimedTransitionCommand(pnObject, guiModelToModel.get(c), c));
112 }
113
114 public void addAnnotationNote(DataLayer c, Point p) {
115 AnnotationNote pnObject = new AnnotationNote(p.x, p.y);
116
117 //enableEditMode open editor, retuns true of text added, else false
118 //If no text is added,dont add it to model
119 if (pnObject.enableEditMode(true)) {
120 c.addPetriNetObject(pnObject);
121 getUndoManager().addEdit(new AddAnnotationNoteCommand(pnObject, c));
122 }
123 }
124
125 public void addTimedInputArc(DataLayer c, TimedPlaceComponent p, TimedTransitionComponent t, ArcPath path) {
126 Require.notNull(c, "DataLayer can't be null");
127 Require.notNull(p, "Place can't be null");
128 Require.notNull(t, "Transitions can't be null");
129
130 TimedArcPetriNet modelNet = guiModelToModel.get(c);
131
132 if (!modelNet.hasArcFromPlaceToTransition(p.underlyingPlace(), t.underlyingTransition())) {
133
134 TimedInputArc tia = new TimedInputArc(
135 p.underlyingPlace(),
136 t.underlyingTransition(),
137 TimeInterval.ZERO_INF
138 );
139
140 TimedInputArcComponent tiac = new TimedInputArcComponent(p,t,tia);
141
142 if (path != null) {
143 tiac.setArcPath(new ArcPath(tiac, path));
144 }
145
146 Command edit = new AddTimedInputArcCommand(
147 tiac,
148 modelNet,
149 c
150 );
151 edit.redo();
152
153 undoManager.addNewEdit(edit);
154
155 } else {
156 //TODO: can't have two arcs between place and transition
157 JOptionPane.showMessageDialog(
158 CreateGui.getApp(),
159 "There was an error drawing the arc. Possible problems:\n"
160 + " - There is already an arc between the selected place and transition\n"
161 + " - You are attempting to draw an arc between a shared transition and a shared place",
162 "Error", JOptionPane.ERROR_MESSAGE
163 );
164 }
165 }
166
167 public void addTimedOutputArc(DataLayer c, TimedTransitionComponent t, TimedPlaceComponent p, ArcPath path) {
168 Require.notNull(c, "DataLayer can't be null");
169 Require.notNull(p, "Place can't be null");
170 Require.notNull(t, "Transitions can't be null");
171
172 TimedArcPetriNet modelNet = guiModelToModel.get(c);
173
174 if (!modelNet.hasArcFromTransitionToPlace(t.underlyingTransition(), p.underlyingPlace())) {
175
176 TimedOutputArc toa = new TimedOutputArc(
177 t.underlyingTransition(),
178 p.underlyingPlace()
179 );
180
181 TimedOutputArcComponent toac = new TimedOutputArcComponent(t, p, toa);
182
183 if (path != null) {
184 toac.setArcPath(new ArcPath(toac, path));
185 }
186
187 Command edit = new AddTimedOutputArcCommand(
188 toac,
189 modelNet,
190 c
191 );
192 edit.redo();
193 undoManager.addNewEdit(edit);
194
195 } else {
196
197 JOptionPane.showMessageDialog(
198 CreateGui.getApp(),
199 "There was an error drawing the arc. Possible problems:\n"
200 + " - There is already an arc between the selected place and transition\n"
201 + " - You are attempting to draw an arc between a shared transition and a shared place",
202 "Error", JOptionPane.ERROR_MESSAGE
203 );
204
205 }
206
207
208 }
209
210 public void addInhibitorArc(DataLayer c, TimedPlaceComponent p, TimedTransitionComponent t, ArcPath path) {
211 Require.notNull(c, "DataLayer can't be null");
212 Require.notNull(p, "Place can't be null");
213 Require.notNull(t, "Transitions can't be null");
214
215 TimedArcPetriNet modelNet = guiModelToModel.get(c);
216
217 if (!modelNet.hasArcFromPlaceToTransition(p.underlyingPlace(), t.underlyingTransition())) {
218
219 TimedInhibitorArc tiha = new TimedInhibitorArc(
220 p.underlyingPlace(),
221 t.underlyingTransition()
222 );
223
224 TimedInhibitorArcComponent tihac = new TimedInhibitorArcComponent(p, t, tiha);
225
226 if (path != null) {
227 tihac.setArcPath(new ArcPath(tihac, path));
228 }
229
230 Command edit = new AddTimedInhibitorArcCommand(
231 tihac,
232 modelNet,
233 c
234 );
235 edit.redo();
236 undoManager.addNewEdit(edit);
237
238 } else {
239
240 JOptionPane.showMessageDialog(
241 CreateGui.getApp(),
242 "There was an error drawing the arc. Possible problems:\n"
243 + " - There is already an arc between the selected place and transition\n"
244 + " - You are attempting to draw an arc between a shared transition and a shared place",
245 "Error", JOptionPane.ERROR_MESSAGE
246 );
247
248 }
249
250 }
251
252 public void addTimedTransportArc(DataLayer c, TimedPlaceComponent p1, TimedTransitionComponent t, TimedPlaceComponent p2, ArcPath path1, ArcPath path2) {
253 Require.notNull(c, "DataLayer can't be null");
254 Require.notNull(p1, "Place1 can't be null");
255 Require.notNull(t, "Transitions can't be null");
256 Require.notNull(p2, "Place2 can't be null");
257
258 TimedArcPetriNet modelNet = guiModelToModel.get(c);
259
260 if (
261 !modelNet.hasArcFromPlaceToTransition(p1.underlyingPlace(), t.underlyingTransition()) &&
262 !modelNet.hasArcFromTransitionToPlace(t.underlyingTransition(), p2.underlyingPlace())
263 ) {
264
265 int groupNr = getNextTransportArcMaxGroupNumber(p1, t);
266
267 TransportArc tta = new TransportArc(p1.underlyingPlace(), t.underlyingTransition(), p2.underlyingPlace());
268
269 TimedTransportArcComponent ttac1 = new TimedTransportArcComponent(p1, t, tta, groupNr);
270 TimedTransportArcComponent ttac2 = new TimedTransportArcComponent(t, p2, tta, groupNr);
271
272 ttac1.setConnectedTo(ttac2);
273 ttac2.setConnectedTo(ttac1);
274
275 if (path1 != null) {
276 ttac1.setArcPath(new ArcPath(ttac1, path1));
277 }
278 if (path2 != null) {
279 ttac2.setArcPath(new ArcPath(ttac2, path2));
280 }
281
282 //XXX: the Command should take both arcs
283 Command edit = new AddTransportArcCommand(
284 ttac2,
285 tta,
286 modelNet,
287 c
288 );
289 edit.redo();
290 undoManager.addNewEdit(edit);
291
292 } else {
293 JOptionPane.showMessageDialog(
294 CreateGui.getApp(),
295 "There was an error drawing the arc. Possible problems:\n"
296 + " - There is already an arc between the source place and transition\n"
297 + " - There is already an arc between the transtion and the target place\n"
298 + " - You are attempting to draw an arc between a shared transition and a shared place",
299 "Error", JOptionPane.ERROR_MESSAGE
300 );
301 }
302
303 }
304
305 private int getNextTransportArcMaxGroupNumber(TimedPlaceComponent p, TimedTransitionComponent t) {
306 int groupMaxCounter = 0;
307
308 for (Arc a : t.getPreset()) {
309 if (a instanceof TimedTransportArcComponent && a.getTarget().equals(t)) {
310 if (((TimedTransportArcComponent) a).getGroupNr() > groupMaxCounter) {
311 groupMaxCounter = ((TimedTransportArcComponent) a).getGroupNr();
312 }
313 }
314 }
315
316 return groupMaxCounter+1;
317 }
318
319
320 public void deleteSelection() {
321 // check if queries need to be removed
322 ArrayList<PetriNetObject> selection = drawingSurface().getSelectionObject().getSelection();
323 Iterable<TAPNQuery> queries = queries();
324 HashSet<TAPNQuery> queriesToDelete = new HashSet<TAPNQuery>();
325
326 boolean queriesAffected = false;
327 for (PetriNetObject pn : selection) {
328 if (pn instanceof TimedPlaceComponent) {
329 TimedPlaceComponent place = (TimedPlaceComponent)pn;
330 if(!place.underlyingPlace().isShared()){
331 for (TAPNQuery q : queries) {
332 if (q.getProperty().containsAtomicPropositionWithSpecificPlaceInTemplate(((LocalTimedPlace)place.underlyingPlace()).model().name(),place.underlyingPlace().name())) {
333 queriesAffected = true;
334 queriesToDelete.add(q);
335 }
336 }
337 }
338 } else if (pn instanceof TimedTransitionComponent){
339 TimedTransitionComponent transition = (TimedTransitionComponent)pn;
340 if(!transition.underlyingTransition().isShared()){
341 for (TAPNQuery q : queries) {
342 if (q.getProperty().containsAtomicPropositionWithSpecificTransitionInTemplate((transition.underlyingTransition()).model().name(),transition.underlyingTransition().name())) {
343 queriesAffected = true;
344 queriesToDelete.add(q);
345 }
346 }
347 }
348 }
349 }
350 StringBuilder s = new StringBuilder();
351 s.append("The following queries are associated with the currently selected objects:\n\n");
352 for (TAPNQuery q : queriesToDelete) {
353 s.append(q.getName());
354 s.append('\n');
355 }
356 s.append("\nAre you sure you want to remove the current selection and all associated queries?");
357
358 int choice = queriesAffected ? JOptionPane.showConfirmDialog(
359 CreateGui.getApp(), s.toString(), "Warning",
360 JOptionPane.YES_NO_OPTION, JOptionPane.QUESTION_MESSAGE)
361 : JOptionPane.YES_OPTION;
362
363 if (choice == JOptionPane.YES_OPTION) {
364 getUndoManager().newEdit(); // new "transaction""
365 if (queriesAffected) {
366 TabContent currentTab = TabContent.this;
367 for (TAPNQuery q : queriesToDelete) {
368 Command cmd = new DeleteQueriesCommand(currentTab, Arrays.asList(q));
369 cmd.redo();
370 getUndoManager().addEdit(cmd);
371 }
372 }
373
374 deleteSelection(selection);
375 network().buildConstraints();
376 }
377 }
378
379 //XXX: function moved from undoManager --kyrke - 2019-07-06
380 private void deleteObject(PetriNetObject pnObject) {
381 if (pnObject instanceof ArcPathPoint) {
382
383 ArcPathPoint arcPathPoint = (ArcPathPoint)pnObject;
384
385 //If the arc is marked for deletion, skip deleting individual arcpathpoint
386 if (!(arcPathPoint.getArcPath().getArc().isSelected())) {
387
388 //Don't delete the two last arc path points
389 if (arcPathPoint.isDeleteable()) {
390 Command cmd = new DeleteArcPathPointEdit(
391 arcPathPoint.getArcPath().getArc(),
392 arcPathPoint,
393 arcPathPoint.getIndex(),
394 getModel()
395 );
396 cmd.redo();
397 getUndoManager().addEdit(cmd);
398 }
399 }
400 }else{
401 //The list of selected objects is not updated when a element is deleted
402 //We might delete the same object twice, which will give an error
403 //Eg. a place with output arc is deleted (deleted also arc) while arc is also selected.
404 //There is properly a better way to track this (check model?) but while refactoring we will keeps it close
405 //to the orginal code -- kyrke 2019-06-27
406 if (!pnObject.isDeleted()) {
407 Command cmd = null;
408 if(pnObject instanceof TimedPlaceComponent){
409 TimedPlaceComponent tp = (TimedPlaceComponent)pnObject;
410 cmd = new DeleteTimedPlaceCommand(tp, guiModelToModel.get(getModel()), getModel());
411 }else if(pnObject instanceof TimedTransitionComponent){
412 TimedTransitionComponent transition = (TimedTransitionComponent)pnObject;
413 cmd = new DeleteTimedTransitionCommand(transition, transition.underlyingTransition().model(), getModel());
414 }else if(pnObject instanceof TimedTransportArcComponent){
415 TimedTransportArcComponent transportArc = (TimedTransportArcComponent)pnObject;
416 cmd = new DeleteTransportArcCommand(transportArc, transportArc.underlyingTransportArc(), transportArc.underlyingTransportArc().model(), getModel());
417 }else if(pnObject instanceof TimedInhibitorArcComponent){
418 TimedInhibitorArcComponent tia = (TimedInhibitorArcComponent)pnObject;
419 cmd = new DeleteTimedInhibitorArcCommand(tia, tia.underlyingTimedInhibitorArc().model(), getModel());
420 }else if(pnObject instanceof TimedInputArcComponent){
421 TimedInputArcComponent tia = (TimedInputArcComponent)pnObject;
422 cmd = new DeleteTimedInputArcCommand(tia, tia.underlyingTimedInputArc().model(), getModel());
423 }else if(pnObject instanceof TimedOutputArcComponent){
424 TimedOutputArcComponent toa = (TimedOutputArcComponent)pnObject;
425 cmd = new DeleteTimedOutputArcCommand(toa, toa.underlyingArc().model(), getModel());
426 }else if(pnObject instanceof AnnotationNote){
427 cmd = new DeleteAnnotationNoteCommand((AnnotationNote)pnObject, getModel());
428 }else{
429 throw new RuntimeException("This should not be possible");
430 }
431 cmd.redo();
432 getUndoManager().addEdit(cmd);
433 }
434 }
435 }
436
437
438 private void deleteSelection(PetriNetObject pnObject) {
439 if(pnObject instanceof PlaceTransitionObject){
440 PlaceTransitionObject pto = (PlaceTransitionObject)pnObject;
441
442 ArrayList<Arc> arcsToDelete = new ArrayList<>();
443
444 //Notice since we delte elements from the collection we can't do this while iterating, we need to
445 // capture the arcs and delete them later.
446 for(Arc arc : pto.getPreset()){
447 arcsToDelete.add(arc);
448 }
449
450 for(Arc arc : pto.getPostset()){
451 arcsToDelete.add(arc);
452 }
453
454 arcsToDelete.forEach(this::deleteObject);
455 }
456
457 deleteObject(pnObject);
458 }
459
460 public void deleteSelection(ArrayList<PetriNetObject> selection) {
461 for (PetriNetObject pnObject : selection) {
462 deleteSelection(pnObject);
463 }
464 }
465
466
467 }
468
59469
60 /**470 /**
61 * Creates a new tab with the selected file, or a new file if filename==null471 * Creates a new tab with the selected file, or a new file if filename==null
62 */472 */
63 public static TabContent createNewTabFromInputStream(InputStream file, String name) throws Exception {473 public static TabContent createNewTabFromInputStream(InputStream file, String name) throws Exception {
64 TabContent tab = new TabContent();
65 tab.setInitialName(name);
66474
67 try {475 try {
68 ModelLoader loader = new ModelLoader();476 ModelLoader loader = new ModelLoader();
69 LoadedModel loadedModel = loader.load(file);477 LoadedModel loadedModel = loader.load(file);
70478
71 tab.setNetwork(loadedModel.network(), loadedModel.templates());479 TabContent tab = new TabContent(loadedModel.network(), loadedModel.templates(), loadedModel.queries());
72 tab.setQueries(loadedModel.queries());480 tab.setInitialName(name);
73 tab.setConstants(loadedModel.network().constants());
74481
75 tab.selectFirstElements();482 tab.selectFirstElements();
76483
77 tab.setFile(null);484 tab.setFile(null);
485 return tab;
78 } catch (Exception e) {486 } catch (Exception e) {
79 throw new Exception("TAPAAL encountered an error while loading the file: " + name + "\n\nPossible explanations:\n - " + e.toString());487 throw new Exception("TAPAAL encountered an error while loading the file: " + name + "\n\nPossible explanations:\n - " + e.toString());
80 }488 }
81489
82 return tab;
83 }490 }
84491
85 public static TabContent createNewEmptyTab(String name){492 public static TabContent createNewEmptyTab(String name){
@@ -89,7 +496,7 @@
89 //Set Default Template496 //Set Default Template
90 String templateName = tab.drawingSurface().getNameGenerator().getNewTemplateName();497 String templateName = tab.drawingSurface().getNameGenerator().getNewTemplateName();
91 Template template = new Template(new TimedArcPetriNet(templateName), new DataLayer(), new Zoomer());498 Template template = new Template(new TimedArcPetriNet(templateName), new DataLayer(), new Zoomer());
92 tab.addTemplate(template, false);499 tab.addTemplate(template);
93500
94 return tab;501 return tab;
95 }502 }
@@ -99,14 +506,6 @@
99 */506 */
100507
101 public static TabContent createNewTabFromPNMLFile(File file) throws Exception {508 public static TabContent createNewTabFromPNMLFile(File file) throws Exception {
102 TabContent tab = new TabContent();
103
104 String name = null;
105
106 if (file != null) {
107 name = file.getName().replaceAll(".pnml", ".tapn");
108 }
109 tab.setInitialName(name);
110509
111 if (file != null) {510 if (file != null) {
112 try {511 try {
@@ -116,24 +515,28 @@
116 PNMLoader loader = new PNMLoader();515 PNMLoader loader = new PNMLoader();
117 loadedModel = loader.load(file);516 loadedModel = loader.load(file);
118517
119518 TabContent tab = new TabContent(loadedModel.network(), loadedModel.templates(), loadedModel.queries());
120 tab.setNetwork(loadedModel.network(), loadedModel.templates());519
121 tab.setQueries(loadedModel.queries());520 String name = null;
122 tab.setConstants(loadedModel.network().constants());521
522 if (file != null) {
523 name = file.getName().replaceAll(".pnml", ".tapn");
524 }
525 tab.setInitialName(name);
123526
124 tab.selectFirstElements();527 tab.selectFirstElements();
125528
126 tab.setMode(Pipe.ElementType.SELECT);529 tab.setMode(Pipe.ElementType.SELECT);
127530
531 //appView.updatePreferredSize(); //XXX 2018-05-23 kyrke seems not to be needed
532 name = name.replace(".pnml",".tapn"); // rename .pnml input file to .tapn
533 return tab;
128534
129 } catch (Exception e) {535 } catch (Exception e) {
130 throw new Exception("TAPAAL encountered an error while loading the file: " + file.getName() + "\n\nPossible explanations:\n - " + e.toString());536 throw new Exception("TAPAAL encountered an error while loading the file: " + file.getName() + "\n\nPossible explanations:\n - " + e.toString());
131 }537 }
132 }538 }
133539 return null;
134 //appView.updatePreferredSize(); //XXX 2018-05-23 kyrke seems not to be needed
135 name = name.replace(".pnml",".tapn"); // rename .pnml input file to .tapn
136 return tab;
137 }540 }
138541
139 /**542 /**
@@ -227,49 +630,72 @@
227 630
228 private WorkflowDialog workflowDialog = null;631 private WorkflowDialog workflowDialog = null;
229632
230 public TabContent() {633
231 for (TimedArcPetriNet net : tapnNetwork.allTemplates()) {634 private TabContent() {
232 guiModels.put(net, new DataLayer());635 this(new TimedArcPetriNetNetwork(), new ArrayList<>(), new TAPNLens(true,false));
233 zoomLevels.put(net, new Zoomer());636 }
234 hasPositionalInfos.put(net, Boolean.FALSE);637
235 }638 private TabContent(TimedArcPetriNetNetwork network, Collection<Template> templates, TAPNLens lens) {
236 639
237 drawingSurface = new DrawingSurfaceImpl(new DataLayer(), this, managerRef);640 Require.that(network != null, "network cannot be null");
238 drawingSurfaceScroller = new JScrollPane(drawingSurface);641 Require.notNull(lens, "Lens can't be null");
239 // make it less bad on XP642 this.lens = lens;
240 drawingSurfaceScroller.setBorder(new BevelBorder(BevelBorder.LOWERED));643 tapnNetwork = network;
241 drawingSurfaceScroller.setWheelScrollingEnabled(true);644
242 drawingSurfaceScroller.getVerticalScrollBar().setUnitIncrement(10);645 guiModels.clear();
243 drawingSurfaceScroller.getHorizontalScrollBar().setUnitIncrement(10);646 for (Template template : templates) {
244647 addGuiModel(template.model(), template.guiModel());
245 // Make clicking the drawing area move focus to GuiFrame648 zoomLevels.put(template.model(), template.zoomer());
246 drawingSurface.addMouseListener(new MouseAdapter() { 649 hasPositionalInfos.put(template.model(), template.getHasPositionalInfo());
247 @Override650 }
248 public void mouseClicked(MouseEvent e) {651
249 CreateGui.getApp().requestFocus();652 drawingSurface = new DrawingSurfaceImpl(new DataLayer(), this, managerRef);
250 }653 drawingSurfaceScroller = new JScrollPane(drawingSurface);
251 });654 // make it less bad on XP
252 655 drawingSurfaceScroller.setBorder(new BevelBorder(BevelBorder.LOWERED));
253 drawingSurfaceDummy = new JPanel(new GridBagLayout());656 drawingSurfaceScroller.setWheelScrollingEnabled(true);
254 GridBagConstraints gc=new GridBagConstraints();657 drawingSurfaceScroller.getVerticalScrollBar().setUnitIncrement(10);
255 gc.fill=GridBagConstraints.HORIZONTAL;658 drawingSurfaceScroller.getHorizontalScrollBar().setUnitIncrement(10);
256 gc.gridx=0;659
257 gc.gridy=0;660 // Make clicking the drawing area move focus to GuiFrame
258 drawingSurfaceDummy.add(new JLabel("The net is too big to be drawn"), gc);661 drawingSurface.addMouseListener(new MouseAdapter() {
259 662 @Override
260 createEditorLeftPane();663 public void mouseClicked(MouseEvent e) {
261 createAnimatorSplitPane();664 CreateGui.getApp().requestFocus();
262665 }
263 this.setOrientation(HORIZONTAL_SPLIT);666 });
264 this.setLeftComponent(editorSplitPaneScroller);667
265 this.setRightComponent(drawingSurfaceScroller);668 drawingSurfaceDummy = new JPanel(new GridBagLayout());
266669 GridBagConstraints gc=new GridBagConstraints();
267 this.setContinuousLayout(true);670 gc.fill=GridBagConstraints.HORIZONTAL;
268 this.setOneTouchExpandable(true);671 gc.gridx=0;
269 this.setBorder(null); // avoid multiple borders672 gc.gridy=0;
270 this.setDividerSize(8);673 drawingSurfaceDummy.add(new JLabel("The net is too big to be drawn"), gc);
271 //XXX must be after the animationcontroller is created674
272 animationModeController = new CanvasAnimationController(getAnimator());675 createEditorLeftPane();
676 createAnimatorSplitPane();
677
678 this.setOrientation(HORIZONTAL_SPLIT);
679 this.setLeftComponent(editorSplitPaneScroller);
680 this.setRightComponent(drawingSurfaceScroller);
681
682 this.setContinuousLayout(true);
683 this.setOneTouchExpandable(true);
684 this.setBorder(null); // avoid multiple borders
685 this.setDividerSize(8);
686 //XXX must be after the animationcontroller is created
687 animationModeController = new CanvasAnimationController(getAnimator());
688 }
689
690 private TabContent(TimedArcPetriNetNetwork network, Collection<Template> templates, Iterable<TAPNQuery> tapnqueries) {
691 this(network, templates, tapnqueries, new TAPNLens(true, false));
692 }
693 private TabContent(TimedArcPetriNetNetwork network, Collection<Template> templates, Iterable<TAPNQuery> tapnqueries, TAPNLens lens) {
694 this(network, templates, lens);
695
696 setNetwork(network, templates);
697 setQueries(tapnqueries);
698 setConstants(network().constants());
273 }699 }
274 700
275 public SharedPlacesAndTransitionsPanel getSharedPlacesAndTransitionsPanel(){701 public SharedPlacesAndTransitionsPanel getSharedPlacesAndTransitionsPanel(){
@@ -706,34 +1132,24 @@
706 return count;1132 return count;
707 }1133 }
7081134
709 /*1135 public void addTemplate(Template template) {
710 XXX: 2018-05-07 kyrke, added a version of addTemplate that does not call templatExplorer.updatTemplateList
711 used in createNewTab (as updateTamplateList expects the current tab to be selected)
712 this needs to be refactored asap. but the is the only way I could get it to work for now.
713 The code is very unclean on what is a template, TimeArcPetriNetNetwork, seems to mix concerns about
714 gui/controller/model. Further refactoring is needed to clean up this mess.
715 */
716 public void addTemplate(Template template, boolean updateTemplateExplorer) {
717 tapnNetwork.add(template.model());1136 tapnNetwork.add(template.model());
718 guiModels.put(template.model(), template.guiModel());1137 guiModels.put(template.model(), template.guiModel());
1138 guiModelToModel.put(template.guiModel(), template.model());
719 zoomLevels.put(template.model(), template.zoomer());1139 zoomLevels.put(template.model(), template.zoomer());
720 hasPositionalInfos.put(template.model(), template.getHasPositionalInfo());1140 hasPositionalInfos.put(template.model(), template.getHasPositionalInfo());
721 if (updateTemplateExplorer) {1141 templateExplorer.updateTemplateList();
722 templateExplorer.updateTemplateList();
723 }
724 }
725
726 public void addTemplate(Template template) {
727 addTemplate(template, true);
728 }1142 }
7291143
730 public void addGuiModel(TimedArcPetriNet net, DataLayer guiModel) {1144 public void addGuiModel(TimedArcPetriNet net, DataLayer guiModel) {
731 guiModels.put(net, guiModel);1145 guiModels.put(net, guiModel);
1146 guiModelToModel.put(guiModel, net);
732 }1147 }
7331148
734 public void removeTemplate(Template template) {1149 public void removeTemplate(Template template) {
735 tapnNetwork.remove(template.model());1150 tapnNetwork.remove(template.model());
736 guiModels.remove(template.model());1151 guiModels.remove(template.model());
1152 guiModelToModel.remove(template.guiModel());
737 zoomLevels.remove(template.model());1153 zoomLevels.remove(template.model());
738 hasPositionalInfos.remove(template.model());1154 hasPositionalInfos.remove(template.model());
739 templateExplorer.updateTemplateList();1155 templateExplorer.updateTemplateList();
@@ -747,7 +1163,7 @@
747 return queries.getQueries();1163 return queries.getQueries();
748 }1164 }
7491165
750 public void setQueries(Iterable<TAPNQuery> queries) {1166 private void setQueries(Iterable<TAPNQuery> queries) {
751 this.queries.setQueries(queries);1167 this.queries.setQueries(queries);
752 }1168 }
7531169
@@ -759,20 +1175,12 @@
759 queries.addQuery(query);1175 queries.addQuery(query);
760 }1176 }
7611177
762 public void setConstants(Iterable<Constant> constants) {1178 private void setConstants(Iterable<Constant> constants) {
763 tapnNetwork.setConstants(constants);1179 tapnNetwork.setConstants(constants);
764 }1180 }
7651181
766 public void setNetwork(TimedArcPetriNetNetwork network, Collection<Template> templates) {1182 private void setNetwork(TimedArcPetriNetNetwork network, Collection<Template> templates) {
767 Require.that(network != null, "network cannot be null");
768 tapnNetwork = network;
7691183
770 guiModels.clear();
771 for (Template template : templates) {
772 addGuiModel(template.model(), template.guiModel());
773 zoomLevels.put(template.model(), template.zoomer());
774 hasPositionalInfos.put(template.model(), template.getHasPositionalInfo());
775 }
7761184
777 sharedPTPanel.setNetwork(network);1185 sharedPTPanel.setNetwork(network);
778 templateExplorer.updateTemplateList();1186 templateExplorer.updateTemplateList();
@@ -1060,6 +1468,8 @@
1060 animator.updateAnimationButtonsEnabled(); //Update stepBack/Forward1468 animator.updateAnimationButtonsEnabled(); //Update stepBack/Forward
1061 }1469 }
10621470
1471 private Pipe.ElementType editorMode = Pipe.ElementType.SELECT;
1472
1063 //XXX temp while refactoring, kyrke - 2019-07-251473 //XXX temp while refactoring, kyrke - 2019-07-25
1064 @Override1474 @Override
1065 public void setMode(Pipe.ElementType mode) {1475 public void setMode(Pipe.ElementType mode) {
@@ -1068,11 +1478,67 @@
10681478
1069 //Disable selection and deselect current selection1479 //Disable selection and deselect current selection
1070 drawingSurface().getSelectionObject().clearSelection();1480 drawingSurface().getSelectionObject().clearSelection();
10711481 editorMode = mode;
1072 //If pending arc draw, remove it1482 switch (mode) {
1073 if (drawingSurface().createArc != null) {1483 case ADDTOKEN:
1074 PlaceTransitionObjectHandler.cleanupArc(drawingSurface().createArc, drawingSurface());1484 setManager(new AbstractDrawingSurfaceManager() {
1075 }1485 @Override
1486 public void registerEvents() {
1487 registerEvent(
1488 e -> e.pno instanceof TimedPlaceComponent && e.a == MouseAction.pressed,
1489 e -> placeClicked((TimedPlaceComponent) e.pno)
1490 );
1491 }
1492
1493 public void placeClicked(TimedPlaceComponent pno) {
1494 Command command = new TimedPlaceMarkingEdit(pno, 1);
1495 command.redo();
1496 undoManager.addNewEdit(command);
1497 }
1498 });
1499 break;
1500 case DELTOKEN:
1501 setManager(new AbstractDrawingSurfaceManager() {
1502 @Override
1503 public void registerEvents() {
1504 registerEvent(
1505 e -> e.pno instanceof TimedPlaceComponent && e.a == MouseAction.pressed,
1506 e -> placeClicked((TimedPlaceComponent) e.pno)
1507 );
1508 }
1509
1510 public void placeClicked(TimedPlaceComponent pno) {
1511 Command command = new TimedPlaceMarkingEdit(pno, -1);
1512 command.redo();
1513 undoManager.addNewEdit(command);
1514 }
1515 });
1516 break;
1517 case TAPNPLACE:
1518 setManager(new CanvasPlaceDrawController());
1519 break;
1520 case TAPNTRANS:
1521 setManager(new CanvasTransitionDrawController());
1522 break;
1523 case ANNOTATION:
1524 setManager(new CanvasAnnotationNoteDrawController());
1525 break;
1526 case TAPNARC:
1527 setManager(new CanvasArcDrawController());
1528 break;
1529 case TAPNINHIBITOR_ARC:
1530 setManager(new CanvasInhibitorarcDrawController());
1531 break;
1532 case TRANSPORTARC:
1533 setManager(new CanvasTransportarcDrawController());
1534 break;
1535 case SELECT:
1536 setManager(new CanvasGeneralDrawController());
1537 break;
1538 default:
1539 setManager(notingManager);
1540 break;
1541 }
10761542
1077 if (mode == Pipe.ElementType.SELECT) {1543 if (mode == Pipe.ElementType.SELECT) {
1078 drawingSurface().setCursor(Cursor.getPredefinedCursor(Cursor.DEFAULT_CURSOR));1544 drawingSurface().setCursor(Cursor.getPredefinedCursor(Cursor.DEFAULT_CURSOR));
@@ -1221,63 +1687,7 @@
12211687
1222 @Override1688 @Override
1223 public void deleteSelection() {1689 public void deleteSelection() {
1224 // check if queries need to be removed1690 guiModelManager.deleteSelection();
1225 ArrayList<PetriNetObject> selection = drawingSurface().getSelectionObject().getSelection();
1226 Iterable<TAPNQuery> queries = queries();
1227 HashSet<TAPNQuery> queriesToDelete = new HashSet<TAPNQuery>();
1228
1229 boolean queriesAffected = false;
1230 for (PetriNetObject pn : selection) {
1231 if (pn instanceof TimedPlaceComponent) {
1232 TimedPlaceComponent place = (TimedPlaceComponent)pn;
1233 if(!place.underlyingPlace().isShared()){
1234 for (TAPNQuery q : queries) {
1235 if (q.getProperty().containsAtomicPropositionWithSpecificPlaceInTemplate(((LocalTimedPlace)place.underlyingPlace()).model().name(),place.underlyingPlace().name())) {
1236 queriesAffected = true;
1237 queriesToDelete.add(q);
1238 }
1239 }
1240 }
1241 } else if (pn instanceof TimedTransitionComponent){
1242 TimedTransitionComponent transition = (TimedTransitionComponent)pn;
1243 if(!transition.underlyingTransition().isShared()){
1244 for (TAPNQuery q : queries) {
1245 if (q.getProperty().containsAtomicPropositionWithSpecificTransitionInTemplate((transition.underlyingTransition()).model().name(),transition.underlyingTransition().name())) {
1246 queriesAffected = true;
1247 queriesToDelete.add(q);
1248 }
1249 }
1250 }
1251 }
1252 }
1253 StringBuilder s = new StringBuilder();
1254 s.append("The following queries are associated with the currently selected objects:\n\n");
1255 for (TAPNQuery q : queriesToDelete) {
1256 s.append(q.getName());
1257 s.append('\n');
1258 }
1259 s.append("\nAre you sure you want to remove the current selection and all associated queries?");
1260
1261 int choice = queriesAffected ? JOptionPane.showConfirmDialog(
1262 CreateGui.getApp(), s.toString(), "Warning",
1263 JOptionPane.YES_NO_OPTION, JOptionPane.QUESTION_MESSAGE)
1264 : JOptionPane.YES_OPTION;
1265
1266 if (choice == JOptionPane.YES_OPTION) {
1267 getUndoManager().newEdit(); // new "transaction""
1268 if (queriesAffected) {
1269 TabContent currentTab = this;
1270 for (TAPNQuery q : queriesToDelete) {
1271 Command cmd = new DeleteQueriesCommand(currentTab, Arrays.asList(q));
1272 cmd.redo();
1273 getUndoManager().addEdit(cmd);
1274 }
1275 }
1276
1277 drawingSurface().deleteSelection(drawingSurface().getSelectionObject().getSelection());
1278 //getCurrentTab().drawingSurface().repaint();
1279 network().buildConstraints();
1280 }
12811691
12821692
1283 }1693 }
@@ -1309,13 +1719,13 @@
13091719
1310 //If arc is being drawn delete it1720 //If arc is being drawn delete it
13111721
1312 if (drawingSurface().createArc == null) {1722 if (editorMode == Pipe.ElementType.SELECT) {
1313 getUndoManager().undo();1723 getUndoManager().undo();
1314 network().buildConstraints();1724 network().buildConstraints();
13151725
1316 } else {1726 } else {
13171727
1318 PlaceTransitionObjectHandler.cleanupArc(drawingSurface().createArc, drawingSurface());1728 setMode(Pipe.ElementType.SELECT);
13191729
1320 }1730 }
1321 }1731 }
@@ -1330,13 +1740,13 @@
13301740
1331 //If arc is being drawn delete it1741 //If arc is being drawn delete it
13321742
1333 if (drawingSurface().createArc == null) {1743 if (editorMode == Pipe.ElementType.SELECT) {
1334 getUndoManager().redo();1744 getUndoManager().redo();
1335 network().buildConstraints();1745 network().buildConstraints();
13361746
1337 } else {1747 } else {
13381748
1339 PlaceTransitionObjectHandler.cleanupArc(drawingSurface().createArc, drawingSurface());1749 setMode(Pipe.ElementType.SELECT);
13401750
1341 }1751 }
1342 }1752 }
@@ -1462,6 +1872,321 @@
1462 return null;1872 return null;
1463 }1873 }
14641874
1875 class CanvasPlaceDrawController extends AbstractDrawingSurfaceManager {
1876
1877 @Override
1878 public void drawingSurfaceMousePressed(MouseEvent e) {
1879 Point p = canvas.adjustPointToGridAndZoom(e.getPoint(), canvas.getZoom());
1880
1881 guiModelManager.addNewTimedPlace(canvas.getGuiModel(), p);
1882 }
1883
1884 @Override
1885 public void registerEvents() {
1886
1887 }
1888 }
1889
1890 class CanvasTransitionDrawController extends AbstractDrawingSurfaceManager {
1891
1892 @Override
1893 public void drawingSurfaceMousePressed(MouseEvent e) {
1894 Point p = canvas.adjustPointToGridAndZoom(e.getPoint(), canvas.getZoom());
1895
1896 guiModelManager.addNewTimedTransitions(drawingSurface.getGuiModel(), p);
1897 }
1898
1899 @Override
1900 public void registerEvents() {
1901
1902 }
1903 }
1904
1905 class CanvasAnnotationNoteDrawController extends AbstractDrawingSurfaceManager {
1906
1907 @Override
1908 public void drawingSurfaceMousePressed(MouseEvent e) {
1909 Point p = canvas.adjustPointToGridAndZoom(e.getPoint(), canvas.getZoom());
1910
1911 guiModelManager.addAnnotationNote(drawingSurface.getGuiModel(), p);
1912 }
1913
1914 @Override
1915 public void registerEvents() {
1916
1917 }
1918 }
1919
1920 class CanvasInhibitorarcDrawController extends AbstractDrawingSurfaceManager {
1921
1922 private TimedTransitionComponent transition;
1923 private TimedPlaceComponent place;
1924 private Arc arc;
1925
1926 @Override
1927 public void registerEvents() {
1928 registerEvent(
1929 e->e.pno instanceof TimedPlaceComponent && e.a == MouseAction.pressed,
1930 e->placeClicked(((TimedPlaceComponent) e.pno))
1931 );
1932 registerEvent(
1933 e->e.pno instanceof TimedTransitionComponent && e.a == MouseAction.pressed,
1934 e->transitionClicked(((TimedTransitionComponent) e.pno))
1935 );
1936 registerEvent(
1937 e->e.pno instanceof PlaceTransitionObject && e.a == MouseAction.entered,
1938 e->placetranstionMouseOver(((PlaceTransitionObject) e.pno))
1939 );
1940 registerEvent(
1941 e->e.pno instanceof PlaceTransitionObject && e.a == MouseAction.exited,
1942 e->placetranstionMouseExited(((PlaceTransitionObject) e.pno))
1943 );
1944 registerEvent(
1945 e->e.pno instanceof PlaceTransitionObject && e.a == MouseAction.moved,
1946 e->placetransitionMouseMoved(((PlaceTransitionObject) e.pno), e.e)
1947 );
1948 }
1949
1950 private void placetransitionMouseMoved(PlaceTransitionObject pno, MouseEvent e) {
1951 if (arc != null) {
1952 if (arc.getSource() == pno || !arc.getSource().areNotSameType(pno)) {
1953 //Dispatch event to parent (drawing surface)
1954 e.translatePoint(pno.getX(),pno.getY());
1955 pno.getParent().dispatchEvent(e);
1956 }
1957 }
1958 }
1959
1960 private void placetranstionMouseExited(PlaceTransitionObject pto) {
1961 if (arc != null) {
1962 arc.setTarget(null);
1963 //XXX this is bad, we have to clean up internal state manually, should be refactored //kyrke - 2019-11-14
1964 // Relates to bug #1849786
1965 if (pto instanceof Transition) {
1966 ((Transition)pto).removeArcCompareObject(arc);
1967 }
1968 arc.updateArcPosition();
1969 }
1970 }
1971
1972 private void placetranstionMouseOver(PlaceTransitionObject pno) {
1973 if (arc != null) {
1974 if (arc.getSource() != pno && arc.getSource().areNotSameType(pno)) {
1975 arc.setTarget(pno);
1976 arc.updateArcPosition();
1977 }
1978 }
1979 }
1980
1981 private void transitionClicked(TimedTransitionComponent pno) {
1982 if (place != null && transition == null) {
1983 transition = pno;
1984 CreateGui.getDrawingSurface().clearAllPrototype();
1985 guiModelManager.addInhibitorArc(getModel(), place, transition, arc.getArcPath());
1986 clearPendingArc();
1987 }
1988 }
1989
1990 private void placeClicked(TimedPlaceComponent pno) {
1991 if (place == null && transition == null) {
1992 place = pno;
1993 arc = new TimedInhibitorArcComponent(pno);
1994 //XXX calling zoomUpdate will set the endpoint to 0,0, drawing the arc from source to 0,0
1995 //to avoid this we change the endpoint to set the end point to the same as the end point
1996 //needs further refactorings //kyrke 2019-09-05
1997 arc.setEndPoint(pno.getPositionX(), pno.getPositionY(), false);
1998 CreateGui.getDrawingSurface().addPrototype(arc);
1999 arc.requestFocusInWindow();
2000 arc.setSelectable(false);
2001 arc.enableDrawingKeyBindings(this::clearPendingArc);
2002 } else if (transition != null && place == null) {
2003 place = pno;
2004 CreateGui.getDrawingSurface().clearAllPrototype();
2005 guiModelManager.addTimedOutputArc(getModel(), transition, place, arc.getArcPath());
2006 clearPendingArc();
2007 }
2008 }
2009
2010 private void clearPendingArc() {
2011 CreateGui.getDrawingSurface().clearAllPrototype();
2012 place = null;
2013 transition = null;
2014 arc = null;
2015 }
2016
2017 @Override
2018 public void drawingSurfaceMouseMoved(MouseEvent e) {
2019 if(arc!=null) {
2020 arc.setEndPoint(e.getX(), e.getY(), e.isShiftDown());
2021 }
2022 }
2023
2024 @Override
2025 public void drawingSurfaceMousePressed(MouseEvent e) {
2026 if (arc!=null) {;
2027 Point p = e.getPoint();
2028 int x = Zoomer.getUnzoomedValue(p.x, CreateGui.getDrawingSurface().getZoom());
2029 int y = Zoomer.getUnzoomedValue(p.y, CreateGui.getDrawingSurface().getZoom());
2030
2031 boolean shiftDown = e.isShiftDown();
2032 //XXX: x,y is ignored is overwritten when mouse is moved, this just add a new point to the end of list
2033 arc.getArcPath().addPoint(arc.getArcPath().getEndIndex(), x,y, shiftDown);
2034 }
2035 }
2036
2037 @Override
2038 public void registerManager(DrawingSurfaceImpl canvas) {
2039 CreateGui.useExtendedBounds = true;
2040 }
2041
2042 @Override
2043 public void deregisterManager() {
2044 clearPendingArc();
2045 CreateGui.useExtendedBounds = false;
2046 }
2047
2048
2049 }
2050 class CanvasArcDrawController extends AbstractDrawingSurfaceManager {
2051 private TimedTransitionComponent transition;
2052 private TimedPlaceComponent place;
2053 private Arc arc;
2054
2055 @Override
2056 public void registerEvents() {
2057 registerEvent(
2058 e->e.pno instanceof TimedPlaceComponent && e.a == MouseAction.pressed,
2059 e->placeClicked(((TimedPlaceComponent) e.pno))
2060 );
2061 registerEvent(
2062 e->e.pno instanceof TimedTransitionComponent && e.a == MouseAction.pressed,
2063 e->transitionClicked(((TimedTransitionComponent) e.pno))
2064 );
2065 registerEvent(
2066 e->e.pno instanceof PlaceTransitionObject && e.a == MouseAction.entered,
2067 e->placetranstionMouseOver(((PlaceTransitionObject) e.pno))
2068 );
2069 registerEvent(
2070 e->e.pno instanceof PlaceTransitionObject && e.a == MouseAction.exited,
2071 e->placetranstionMouseExited(((PlaceTransitionObject) e.pno))
2072 );
2073 registerEvent(
2074 e->e.pno instanceof PlaceTransitionObject && e.a == MouseAction.moved,
2075 e->placetransitionMouseMoved(((PlaceTransitionObject) e.pno), e.e)
2076 );
2077 }
2078
2079 private void placetransitionMouseMoved(PlaceTransitionObject pno, MouseEvent e) {
2080 if (arc != null) {
2081 if (arc.getSource() == pno || !arc.getSource().areNotSameType(pno)) {
2082 //Dispatch event to parent (drawing surface)
2083 e.translatePoint(pno.getX(),pno.getY());
2084 pno.getParent().dispatchEvent(e);
2085 }
2086 }
2087 }
2088
2089 private void placetranstionMouseExited(PlaceTransitionObject pto) {
2090 if (arc != null) {
2091 arc.setTarget(null);
2092 //XXX this is bad, we have to clean up internal state manually, should be refactored //kyrke - 2019-11-14
2093 // Relates to bug #1849786
2094 if (pto instanceof Transition) {
2095 ((Transition)pto).removeArcCompareObject(arc);
2096 }
2097 arc.updateArcPosition();
2098 }
2099 }
2100
2101 private void placetranstionMouseOver(PlaceTransitionObject pno) {
2102 if (arc != null) {
2103 if (arc.getSource() != pno && arc.getSource().areNotSameType(pno)) {
2104 arc.setTarget(pno);
2105 arc.updateArcPosition();
2106 }
2107 }
2108 }
2109
2110 private void transitionClicked(TimedTransitionComponent pno) {
2111 if (place == null && transition == null) {
2112 transition = pno;
2113 arc = new TimedOutputArcComponent(pno);
2114
2115 //XXX calling zoomUpdate will set the endpoint to 0,0, drawing the arc from source to 0,0
2116 //to avoid this we change the endpoint to set the end point to the same as the end point
2117 //needs further refactorings //kyrke 2019-09-05
2118 arc.setEndPoint(pno.getPositionX(), pno.getPositionY(), false);
2119 CreateGui.getDrawingSurface().addPrototype(arc);
2120 arc.requestFocusInWindow();
2121 arc.setSelectable(false);
2122 arc.enableDrawingKeyBindings(this::clearPendingArc);
2123 } else if (place != null && transition == null) {
2124 transition = pno;
2125 CreateGui.getDrawingSurface().clearAllPrototype();
2126 guiModelManager.addTimedInputArc(getModel(), place, transition, arc.getArcPath());
2127 clearPendingArc();
2128 }
2129 }
2130
2131 private void placeClicked(TimedPlaceComponent pno) {
2132 if (place == null && transition == null) {
2133 place = pno;
2134 arc = new TimedInputArcComponent(pno);
2135 //XXX calling zoomUpdate will set the endpoint to 0,0, drawing the arc from source to 0,0
2136 //to avoid this we change the endpoint to set the end point to the same as the end point
2137 //needs further refactorings //kyrke 2019-09-05
2138 arc.setEndPoint(pno.getPositionX(), pno.getPositionY(), false);
2139 CreateGui.getDrawingSurface().addPrototype(arc);
2140 arc.requestFocusInWindow();
2141 arc.setSelectable(false);
2142 arc.enableDrawingKeyBindings(this::clearPendingArc);
2143 } else if (transition != null && place == null) {
2144 place = pno;
2145 CreateGui.getDrawingSurface().clearAllPrototype();
2146 guiModelManager.addTimedOutputArc(getModel(), transition, place, arc.getArcPath());
2147 clearPendingArc();
2148 }
2149 }
2150
2151 private void clearPendingArc() {
2152 CreateGui.getDrawingSurface().clearAllPrototype();
2153 place = null;
2154 transition = null;
2155 arc = null;
2156 }
2157
2158 @Override
2159 public void drawingSurfaceMouseMoved(MouseEvent e) {
2160 if(arc!=null) {
2161 arc.setEndPoint(e.getX(), e.getY(), e.isShiftDown());
2162 }
2163 }
2164
2165 @Override
2166 public void drawingSurfaceMousePressed(MouseEvent e) {
2167 if (arc!=null) {;
2168 Point p = e.getPoint();
2169 int x = Zoomer.getUnzoomedValue(p.x, CreateGui.getDrawingSurface().getZoom());
2170 int y = Zoomer.getUnzoomedValue(p.y, CreateGui.getDrawingSurface().getZoom());
2171
2172 boolean shiftDown = e.isShiftDown();
2173 //XXX: x,y is ignored is overwritten when mouse is moved, this just add a new point to the end of list
2174 arc.getArcPath().addPoint(arc.getArcPath().getEndIndex(), x,y, shiftDown);
2175 }
2176 }
2177
2178 @Override
2179 public void registerManager(DrawingSurfaceImpl canvas) {
2180 CreateGui.useExtendedBounds = true;
2181 }
2182
2183 @Override
2184 public void deregisterManager() {
2185 clearPendingArc();
2186 CreateGui.useExtendedBounds = false;
2187 }
2188 }
2189
1465 static class CanvasAnimationController extends AbstractDrawingSurfaceManager {2190 static class CanvasAnimationController extends AbstractDrawingSurfaceManager {
14662191
1467 private final Animator animator;2192 private final Animator animator;
@@ -1473,7 +2198,7 @@
1473 @Override2198 @Override
1474 public void registerEvents() {2199 public void registerEvents() {
1475 registerEvent(2200 registerEvent(
1476 e -> e.a == MouseAction.clicked && e.pno instanceof TimedTransitionComponent && SwingUtilities.isLeftMouseButton(e.e),2201 e -> e.a == MouseAction.pressed && e.pno instanceof TimedTransitionComponent && SwingUtilities.isLeftMouseButton(e.e),
1477 e -> transitionLeftClicked((TimedTransitionComponent)e.pno)2202 e -> transitionLeftClicked((TimedTransitionComponent)e.pno)
1478 );2203 );
1479 registerEvent(2204 registerEvent(
@@ -1516,13 +2241,205 @@
1516 //De-register old manager2241 //De-register old manager
1517 managerRef.get().deregisterManager();2242 managerRef.get().deregisterManager();
1518 managerRef.setReference(newManager);2243 managerRef.setReference(newManager);
1519 managerRef.get().registerManager();2244 managerRef.get().registerManager(drawingSurface);
1520 }2245 }
15212246
1522 //XXX: A quick function made while refactoring to test if the tab is currently2247 private final class CanvasTransportarcDrawController extends AbstractDrawingSurfaceManager {
1523 // the tab selected, and is allowed to change gui the gui. Should be controlled an other way2248
1524 // /kyrke 2019-11-102249 private TimedTransitionComponent transition;
1525 public boolean isTabInFocus(){2250 private TimedPlaceComponent place1;
1526 return app.isPresent();2251 private TimedPlaceComponent place2;
1527 }2252 private Arc arc;
2253 private Arc arc1;
2254 private Arc arc2;
2255
2256
2257 @Override
2258 public void registerEvents() {
2259 registerEvent(
2260 e->e.pno instanceof TimedPlaceComponent && e.a == MouseAction.pressed,
2261 e->placeClicked(((TimedPlaceComponent) e.pno))
2262 );
2263 registerEvent(
2264 e->e.pno instanceof TimedTransitionComponent && e.a == MouseAction.pressed,
2265 e->transitionClicked(((TimedTransitionComponent) e.pno))
2266 );
2267 registerEvent(
2268 e->e.pno instanceof PlaceTransitionObject && e.a == MouseAction.entered,
2269 e->placetranstionMouseOver(((PlaceTransitionObject) e.pno))
2270 );
2271 registerEvent(
2272 e->e.pno instanceof PlaceTransitionObject && e.a == MouseAction.exited,
2273 e->placetranstionMouseExited(((PlaceTransitionObject) e.pno))
2274 );
2275 registerEvent(
2276 e->e.pno instanceof PlaceTransitionObject && e.a == MouseAction.moved,
2277 e->placetransitionMouseMoved(((PlaceTransitionObject) e.pno), e.e)
2278 );
2279 }
2280
2281 private void placetransitionMouseMoved(PlaceTransitionObject pno, MouseEvent e) {
2282 if (arc != null) {
2283 if (arc.getSource() == pno || !arc.getSource().areNotSameType(pno)) {
2284 //Dispatch event to parent (drawing surface)
2285 e.translatePoint(pno.getX(),pno.getY());
2286 pno.getParent().dispatchEvent(e);
2287 }
2288 }
2289 }
2290
2291 private void placetranstionMouseExited(PlaceTransitionObject pto) {
2292 if (arc != null) {
2293 arc.setTarget(null);
2294 //XXX this is bad, we have to clean up internal state manually, should be refactored //kyrke - 2019-11-14
2295 // Relates to bug #1849786
2296 if (pto instanceof Transition) {
2297 ((Transition)pto).removeArcCompareObject(arc);
2298 }
2299 arc.updateArcPosition();
2300 }
2301 }
2302
2303 private void placetranstionMouseOver(PlaceTransitionObject pno) {
2304 if (arc != null) {
2305 if (arc.getSource() != pno && arc.getSource().areNotSameType(pno)) {
2306 arc.setTarget(pno);
2307 arc.updateArcPosition();
2308 }
2309 }
2310 }
2311
2312 private void transitionClicked(TimedTransitionComponent pno) {
2313 if (place1 != null && transition == null) {
2314 transition = pno;
2315 arc2 = arc = new TimedTransportArcComponent(pno, -1, false);
2316
2317 //XXX calling zoomUpdate will set the endpoint to 0,0, drawing the arc from source to 0,0
2318 //to avoid this we change the endpoint to set the end point to the same as the end point
2319 //needs further refactorings //kyrke 2019-09-05
2320 arc.setEndPoint(pno.getPositionX(), pno.getPositionY(), false);
2321 CreateGui.getDrawingSurface().addPrototype(arc);
2322 arc.requestFocusInWindow();
2323 arc.setSelectable(false);
2324 arc.enableDrawingKeyBindings(this::clearPendingArc);
2325 }
2326 }
2327
2328 private void placeClicked(TimedPlaceComponent pno) {
2329 if (place1 == null && transition == null) {
2330 place1 = pno;
2331 arc1 = arc = new TimedTransportArcComponent(pno, -1, true);
2332 //XXX calling zoomUpdate will set the endpoint to 0,0, drawing the arc from source to 0,0
2333 //to avoid this we change the endpoint to set the end point to the same as the end point
2334 //needs further refactorings //kyrke 2019-09-05
2335 arc.setEndPoint(pno.getPositionX(), pno.getPositionY(), false);
2336 CreateGui.getDrawingSurface().addPrototype(arc);
2337 arc.requestFocusInWindow();
2338 arc.setSelectable(false);
2339 arc.enableDrawingKeyBindings(this::clearPendingArc);
2340 } else if (transition != null && place2 == null) {
2341 place2 = pno;
2342 CreateGui.getDrawingSurface().clearAllPrototype();
2343 guiModelManager.addTimedTransportArc(getModel(), place1, transition, place2, arc1.getArcPath(), arc2.getArcPath());
2344 clearPendingArc();
2345 }
2346 }
2347
2348 private void clearPendingArc() {
2349 CreateGui.getDrawingSurface().clearAllPrototype();
2350 place1 = place2 = null;
2351 transition = null;
2352 arc = arc1 = arc2 = null;
2353 }
2354
2355 @Override
2356 public void drawingSurfaceMouseMoved(MouseEvent e) {
2357 if(arc!=null) {
2358 arc.setEndPoint(e.getX(), e.getY(), e.isShiftDown());
2359 }
2360 }
2361
2362 @Override
2363 public void drawingSurfaceMousePressed(MouseEvent e) {
2364 if (arc!=null) {
2365 Point p = e.getPoint();
2366 int x = Zoomer.getUnzoomedValue(p.x, CreateGui.getDrawingSurface().getZoom());
2367 int y = Zoomer.getUnzoomedValue(p.y, CreateGui.getDrawingSurface().getZoom());
2368
2369 boolean shiftDown = e.isShiftDown();
2370 //XXX: x,y is ignored is overwritten when mouse is moved, this just add a new point to the end of list
2371 arc.getArcPath().addPoint(arc.getArcPath().getEndIndex(), x,y, shiftDown);
2372 }
2373 }
2374
2375 @Override
2376 public void registerManager(DrawingSurfaceImpl canvas) {
2377 CreateGui.useExtendedBounds = true;
2378 }
2379
2380 @Override
2381 public void deregisterManager() {
2382 clearPendingArc();
2383 CreateGui.useExtendedBounds = false;
2384 }
2385 }
2386
2387 private class CanvasGeneralDrawController extends AbstractDrawingSurfaceManager {
2388 @Override
2389 public void registerEvents() {
2390 registerEvent(
2391 e->e.pno instanceof TimedTransitionComponent && e.a == MouseAction.doubleClicked,
2392 e-> ((TimedTransitionComponent) e.pno).showEditor()
2393 );
2394 registerEvent(
2395 e->e.pno instanceof TimedPlaceComponent && e.a == MouseAction.doubleClicked,
2396 e-> ((TimedPlaceComponent) e.pno).showEditor()
2397 );
2398 registerEvent(
2399 e->e.pno instanceof TimedTransitionComponent && e.a == MouseAction.rightClicked,
2400 e-> ((TimedTransitionComponent) e.pno).getMouseHandler().getPopup(e.e).show(e.pno, e.e.getX(), e.e.getY())
2401 );
2402 registerEvent(
2403 e->e.pno instanceof TimedPlaceComponent && e.a == MouseAction.rightClicked,
2404 e-> ((TimedPlaceComponent) e.pno).getMouseHandler().getPopup(e.e).show(e.pno, e.e.getX(), e.e.getY())
2405 );
2406 registerEvent(
2407 e->e.pno instanceof Arc && e.a == MouseAction.rightClicked,
2408 e-> ((Arc) e.pno).getMouseHandler().getPopup(e.e).show(e.pno, e.e.getX(), e.e.getY())
2409 );
2410 registerEvent(
2411 e->e.pno instanceof AnnotationNote && e.a == MouseAction.doubleClicked,
2412 e-> ((AnnotationNote) e.pno).enableEditMode()
2413 );
2414 registerEvent(
2415 e->e.pno instanceof AnnotationNote && e.a == MouseAction.rightClicked,
2416 e-> ((AnnotationNote) e.pno).getMouseHandler().getPopup(e.e).show(e.pno, e.e.getX(), e.e.getY())
2417 );
2418 registerEvent(
2419 e->e.pno instanceof Arc && e.a == MouseAction.entered,
2420 e -> ((Arc)e.pno).getArcPath().showPoints()
2421 );
2422 registerEvent(
2423 e->e.pno instanceof Arc && e.a == MouseAction.exited,
2424 e -> ((Arc)e.pno).getArcPath().hidePoints()
2425 );
2426 registerEvent(
2427 e->e.pno instanceof Arc && e.a == MouseAction.doubleClicked && e.e.isControlDown(),
2428 e->arcDoubleClickedWithContrl(((Arc) e.pno), e.e)
2429 );
2430
2431 }
2432
2433 private void arcDoubleClickedWithContrl(Arc arc, MouseEvent e) {
2434 CreateGui.getCurrentTab().getUndoManager().addNewEdit(
2435 arc.getArcPath().insertPoint(
2436 new Point2D.Double(
2437 Zoomer.getUnzoomedValue(arc.getX() + e.getX(), arc.getZoom()),
2438 Zoomer.getUnzoomedValue(arc.getY() + e.getY(), arc.getZoom())
2439 ),
2440 e.isAltDown()
2441 )
2442 );
2443 }
2444 }
1528}2445}
15292446
=== modified file 'src/dk/aau/cs/gui/TemplateExplorer.java'
--- src/dk/aau/cs/gui/TemplateExplorer.java 2020-05-27 13:15:44 +0000
+++ src/dk/aau/cs/gui/TemplateExplorer.java 2020-07-09 12:55:48 +0000
@@ -81,12 +81,12 @@
81 private JButton renameButton;81 private JButton renameButton;
82 private JButton copyButton;82 private JButton copyButton;
8383
84 private TabContent parent;84 private final TabContent parent;
85 private UndoManager undoManager;85 private final UndoManager undoManager;
86 private boolean isInAnimationMode;86 private boolean isInAnimationMode;
8787
88 public JButton moveUpButton;88 private JButton moveUpButton;
89 public JButton moveDownButton;89 private JButton moveDownButton;
90 private JButton sortButton;90 private JButton sortButton;
91 91
92 private static final String toolTipNewComponent ="Create a new component";92 private static final String toolTipNewComponent ="Create a new component";
@@ -188,7 +188,7 @@
188188
189 private void initExplorerPanel() {189 private void initExplorerPanel() {
190 templatePanel = new JPanel(new GridBagLayout());190 templatePanel = new JPanel(new GridBagLayout());
191 listModel = new DefaultListModel();191 listModel = new DefaultListModel<>();
192 for (Template net : parent.allTemplates()) {192 for (Template net : parent.allTemplates()) {
193 listModel.addElement(net);193 listModel.addElement(net);
194 }194 }
@@ -214,7 +214,7 @@
214 }214 }
215 });215 });
216216
217 templateList = new NonsearchableJList(listModel);217 templateList = new NonsearchableJList<>(listModel);
218218
219 templateList.setSelectionMode(ListSelectionModel.SINGLE_SELECTION);219 templateList.setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
220 templateList.setSelectedIndex(0);220 templateList.setSelectedIndex(0);
@@ -476,7 +476,7 @@
476 private void onOKRenameTemplate() { 476 private void onOKRenameTemplate() {
477 Template template = selectedModel(); 477 Template template = selectedModel();
478 String newName = nameTextField.getText().trim();478 String newName = nameTextField.getText().trim();
479 if (newName == null || template.model().name().equals(newName)) {479 if (template.model().name().equals(newName)) {
480 exit();480 exit();
481 return;481 return;
482 }482 }
@@ -508,37 +508,34 @@
508 }508 }
509 509
510 private void onOK() {510 private void onOK() {
511 Template template = null; 511 String templateName = nameTextField.getText().trim();
512 String templateName = nameTextField.getText().trim(); 512 if(!isNameAllowed(templateName)) {
513 if (templateName != null) {513 JOptionPane.showMessageDialog(parent.drawingSurface(),
514 if(!isNameAllowed(templateName)) {514 "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.",
515 JOptionPane.showMessageDialog(parent.drawingSurface(),515 "Error Creating Component",
516 "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.",516 JOptionPane.ERROR_MESSAGE);
517 "Error Creating Component",517 exit();
518 JOptionPane.ERROR_MESSAGE);518 ShowNewTemplateDialog(templateName);
519 exit();519 return;
520 ShowNewTemplateDialog(templateName);520 }
521 return;521 else if (parent.network().hasTAPNCalled(templateName)) {
522 }522 JOptionPane.showMessageDialog(parent.drawingSurface(),
523 else if (parent.network().hasTAPNCalled(templateName)) {523 "A component named \"" + templateName + "\" already exists.\n\nThe new component could not be created.",
524 JOptionPane.showMessageDialog(parent.drawingSurface(),524 "Error Creating Component",
525 "A component named \"" + templateName + "\" already exists.\n\nThe new component could not be created.",525 JOptionPane.ERROR_MESSAGE);
526 "Error Creating Component",526 exit();
527 JOptionPane.ERROR_MESSAGE);527 ShowNewTemplateDialog(templateName);
528 exit();528 return;
529 ShowNewTemplateDialog(templateName);529 }
530 return;530 else {
531 }531 Template template = createNewTemplate(templateName);
532 else {532
533 template = createNewTemplate(templateName);533 int index = listModel.size();
534534 undoManager.addNewEdit(new AddTemplateCommand(TemplateExplorer.this, template, index));
535 int index = listModel.size();535 parent.addTemplate(template);
536 undoManager.addNewEdit(new AddTemplateCommand(TemplateExplorer.this, template, index));536 }
537 parent.addTemplate(template);537
538 }538 exit();
539 }
540
541 exit();
542 }539 }
543 540
544 private void exit() {541 private void exit() {
@@ -639,8 +636,7 @@
639 }636 }
640637
641 private void ShowNewTemplateDialog(String nameToShow) {638 private void ShowNewTemplateDialog(String nameToShow) {
642 dialog = new EscapableDialog(CreateGui.getApp(),639 dialog = new EscapableDialog(CreateGui.getApp(), "Enter Component Name", true);
643 "Enter Component Name", true);
644 initComponentsOfNewTemplateDialog(nameToShow);640 initComponentsOfNewTemplateDialog(nameToShow);
645 dialog.add(container);641 dialog.add(container);
646 dialog.setResizable(false);642 dialog.setResizable(false);
@@ -742,8 +738,7 @@
742 }738 }
743739
744 private void showRenameTemplateDialog(String nameToShow) { 740 private void showRenameTemplateDialog(String nameToShow) {
745 dialog = new EscapableDialog(CreateGui.getApp(),741 dialog = new EscapableDialog(CreateGui.getApp(), "Enter Component Name", true);
746 "Enter Component Name", true);
747 Template template = selectedModel();742 Template template = selectedModel();
748 if (nameToShow.equals("")){743 if (nameToShow.equals("")){
749 initComponentsOfRenameTemplateDialog(template.model().name());744 initComponentsOfRenameTemplateDialog(template.model().name());
@@ -777,7 +772,7 @@
777772
778 public void openSelectedTemplate() {773 public void openSelectedTemplate() {
779 Template tapn = selectedModel();774 Template tapn = selectedModel();
780 if (tapn != null && parent.isTabInFocus()) {775 if (tapn != null) {
781 parent.changeToTemplate(tapn);776 parent.changeToTemplate(tapn);
782 }777 }
783 //parent.drawingSurface().repaintAll();778 //parent.drawingSurface().repaintAll();
@@ -789,7 +784,7 @@
789784
790 public void updateTemplateList() {785 public void updateTemplateList() {
791 int selectedIndex = templateList.getSelectedIndex();786 int selectedIndex = templateList.getSelectedIndex();
792 DefaultListModel newList = new DefaultListModel();787 DefaultListModel<Template> newList = new DefaultListModel<>();
793 788
794 if(isInAnimationMode) {789 if(isInAnimationMode) {
795 for (Template net : parent.activeTemplates()) {790 for (Template net : parent.activeTemplates()) {
@@ -852,7 +847,7 @@
852 listModel.setElementAt(o, index+1);847 listModel.setElementAt(o, index+1);
853 }848 }
854 @Override849 @Override
855 public JList getJList(){850 public JList<Template> getJList(){
856 return templateList;851 return templateList;
857 }852 }
858853
@@ -995,21 +990,24 @@
995 }990 }
996 renameButton.setEnabled(true);991 renameButton.setEnabled(true);
997 copyButton.setEnabled(true);992 copyButton.setEnabled(true);
998 if(templateList.getModel().getSize() >= 2)993 if(templateList.getModel().getSize() >= 2) {
999 sortButton.setEnabled(true);994 sortButton.setEnabled(true);
1000 else995 } else {
1001 sortButton.setEnabled(false);996 sortButton.setEnabled(false);
1002 997 }
1003 if(index > 0)998
1004 moveUpButton.setEnabled(true);999 if(index > 0) {
1005 else1000 moveUpButton.setEnabled(true);
1006 moveUpButton.setEnabled(false);1001 } else {
1002 moveUpButton.setEnabled(false);
1003 }
1007 1004
1008 1005
1009 if(index < parent.network().allTemplates().size() - 1)1006 if(index < parent.network().allTemplates().size() - 1) {
1010 moveDownButton.setEnabled(true);1007 moveDownButton.setEnabled(true);
1011 else1008 } else {
1012 moveDownButton.setEnabled(false);1009 moveDownButton.setEnabled(false);
1010 }
1013 }1011 }
1014 templateList.ensureIndexIsVisible(index);1012 templateList.ensureIndexIsVisible(index);
1015 openSelectedTemplate();1013 openSelectedTemplate();
10161014
=== modified file 'src/dk/aau/cs/gui/components/EnabledTransitionsList.java'
--- src/dk/aau/cs/gui/components/EnabledTransitionsList.java 2020-05-18 08:14:37 +0000
+++ src/dk/aau/cs/gui/components/EnabledTransitionsList.java 2020-07-09 12:55:48 +0000
@@ -38,17 +38,14 @@
38 initPanel();38 initPanel();
39 }39 }
4040
41 DefaultListModel<TransitionListItem> transitions;41 final DefaultListModel<TransitionListItem> transitions = new DefaultListModel<>();
42 JList<TransitionListItem> transitionsList;42 final JList<TransitionListItem> transitionsList = new JList<>(transitions);
43 JScrollPane scrollPane;43 final JScrollPane scrollPane = new JScrollPane(transitionsList);
44 TransitionListItem lastSelected;44 TransitionListItem lastSelected;
4545
46 public void initPanel(){46 public void initPanel(){
47 transitions = new DefaultListModel<>();
48 transitionsList = new JList<>(transitions);
49 transitionsList.setCellRenderer(new EnabledTransitionListCellRenderer());
5047
51 transitionsList.addMouseListener(new MouseAdapter() {48 transitionsList.addMouseListener(new MouseAdapter() {
52 @Override49 @Override
53 public void mouseClicked(MouseEvent e) {50 public void mouseClicked(MouseEvent e) {
54 if(e.getClickCount() == 2){51 if(e.getClickCount() == 2){
@@ -64,9 +61,7 @@
64 }61 }
65 });62 });
6663
67 scrollPane = new JScrollPane(transitionsList);64 this.add(scrollPane, BorderLayout.CENTER);
68
69 this.add(scrollPane, BorderLayout.CENTER);
70 }65 }
71 66
72 public void startReInit(){67 public void startReInit(){
@@ -110,18 +105,12 @@
110 public void addTransition(Template template, Transition transition){105 public void addTransition(Template template, Transition transition){
111 TransitionListItem item = new TransitionListItem(transition, template);106 TransitionListItem item = new TransitionListItem(transition, template);
112107
113 transition.isDelayEnabled();
114 if(!transitions.contains(item)){108 if(!transitions.contains(item)){
115 transitions.addElement(item);109 transitions.addElement(item);
116 }110 }
117 }111 }
118112
119 public void removeTransition(Template template, Transition transition){113 public void fireSelectedTransition(){
120 TransitionListItem item = new TransitionListItem(transition, template);
121 transitions.removeElement(item);
122 }
123
124 public void fireSelectedTransition(){
125 TransitionListItem item = transitionsList.getSelectedValue();114 TransitionListItem item = transitionsList.getSelectedValue();
126115
127 if(item != null) {116 if(item != null) {
@@ -131,27 +120,10 @@
131120
132 interface ListItem extends Comparable<ListItem>{}121 interface ListItem extends Comparable<ListItem>{}
133122
134 class SplitterListItem implements ListItem{
135
136 @Override
137 public int compareTo(ListItem o) {
138 if(o instanceof TransitionListItem){
139 return o.compareTo(this);
140 } else {
141 return 0;
142 }
143 }
144
145 @Override
146 public String toString() {
147 return "_";
148 }
149
150 }
151123
152 static class TransitionListItem implements ListItem{124 static class TransitionListItem implements ListItem{
153 private Transition transition;125 private final Transition transition;
154 private Template template;126 private final Template template;
155127
156 public TransitionListItem(Transition transition, Template template){128 public TransitionListItem(Transition transition, Template template){
157 this.transition = transition;129 this.transition = transition;
@@ -160,8 +132,7 @@
160132
161 public String toString(boolean showIntervals) {133 public String toString(boolean showIntervals) {
162134
163 String interval = transition.getDInterval() == null || !showIntervals ? 135 String interval = transition.getDInterval() == null || !showIntervals ? "" : transition.getDInterval().toString() + " ";
164 "" : transition.getDInterval().toString() + " ";
165 136
166 String transitionName = getTransition().getName(); 137 String transitionName = getTransition().getName();
167 if(isShared()){138 if(isShared()){
@@ -237,51 +208,6 @@
237 }208 }
238 }209 }
239210
240 //This class creates the stippled line shown between the enabled transitions and the delay-enabled transitions
241 class EnabledTransitionListCellRenderer extends DefaultListCellRenderer{
242
243 @Override
244 public Component getListCellRendererComponent(JList list, Object value,
245 int index, boolean isSelected, boolean cellHasFocus) {
246 if(value instanceof SplitterListItem){
247 JLabel separator = new JLabel();
248 separator.setBorder(new DashBorder());
249 separator.setPreferredSize(new Dimension(1, 1));
250 return separator;
251 } else {
252 return super.getListCellRendererComponent(list, value, index, isSelected, cellHasFocus);
253 }
254 }
255
256 class DashBorder implements Border {
257 private final Insets insets = new Insets(1, 1, 1, 1);
258 private final int length = 5;
259 private final int space = 3;
260 public boolean isBorderOpaque() {
261 return false;
262 }
263 public void paintBorder(Component c, Graphics g, int x, int y,
264 int width, int height) {
265 g.setColor(Color.BLACK);
266 // --- draw horizontal ---
267 for (int i = 0; i < width; i += length) {
268 g.drawLine(i, y, i + length, y);
269 g.drawLine(i, height - 1, i + length, height - 1);
270 i += space;
271 }
272 // --- draw vertical ---
273 for (int i = 0; i < height; i += length) {
274 g.drawLine(0, i, 0, i + length);
275 g.drawLine(width - 1, i, width - 1, i + length);
276 i += space;
277 }
278 }
279 public Insets getBorderInsets(Component c) {
280 return insets;
281 }
282 }
283 }
284
285 public int getNumberOfTransitions() {211 public int getNumberOfTransitions() {
286 return transitions.size();212 return transitions.size();
287 }213 }
288214
=== modified file 'src/dk/aau/cs/gui/components/NonsearchableJList.java'
--- src/dk/aau/cs/gui/components/NonsearchableJList.java 2020-04-18 12:27:02 +0000
+++ src/dk/aau/cs/gui/components/NonsearchableJList.java 2020-07-09 12:55:48 +0000
@@ -19,7 +19,7 @@
19 removeKeyListener();19 removeKeyListener();
20 }20 }
2121
22 public NonsearchableJList(ListModel dataModel){22 public NonsearchableJList(ListModel<E> dataModel){
23 super (dataModel);23 super (dataModel);
24 removeKeyListener();24 removeKeyListener();
25 }25 }
2626
=== modified file 'src/dk/aau/cs/gui/components/TransitionFireingComponent.java'
--- src/dk/aau/cs/gui/components/TransitionFireingComponent.java 2020-05-18 14:10:47 +0000
+++ src/dk/aau/cs/gui/components/TransitionFireingComponent.java 2020-07-09 12:55:48 +0000
@@ -28,14 +28,19 @@
2828
29 enabledTransitionsList = new EnabledTransitionsList();29 enabledTransitionsList = new EnabledTransitionsList();
3030
31 this.setBorder(BorderFactory.createCompoundBorder(31 this.setBorder(
32 BorderFactory.createCompoundBorder(
32 BorderFactory.createTitledBorder("Enabled Transitions"),33 BorderFactory.createTitledBorder("Enabled Transitions"),
33 BorderFactory.createEmptyBorder(3, 3, 3, 3)));34 BorderFactory.createEmptyBorder(3, 3, 3, 3)
34 this35 )
35 .setToolTipText("List of currently enabled transitions (double click a transition to fire it)");36 );
36 enabledTransitionsList.setPreferredSize(new Dimension(37 this.setToolTipText("List of currently enabled transitions (double click a transition to fire it)");
38 enabledTransitionsList.setPreferredSize(
39 new Dimension(
37 enabledTransitionsList.getPreferredSize().width,40 enabledTransitionsList.getPreferredSize().width,
38 enabledTransitionsList.getMinimumSize().height));41 enabledTransitionsList.getMinimumSize().height
42 )
43 );
3944
40 settingsButton = new JButton("Settings");45 settingsButton = new JButton("Settings");
41 settingsButton.setPreferredSize(new Dimension(0, settingsButton.getPreferredSize().height)); //Make the two buttons equal in size46 settingsButton.setPreferredSize(new Dimension(0, settingsButton.getPreferredSize().height)); //Make the two buttons equal in size
@@ -50,6 +55,7 @@
50 fireSelectedTransition();55 fireSelectedTransition();
51 }56 }
52 });57 });
58
53 fireButton.addKeyListener(new KeyAdapter() { 59 fireButton.addKeyListener(new KeyAdapter() {
54 @Override60 @Override
55 public void keyPressed(KeyEvent e) {61 public void keyPressed(KeyEvent e) {
5662
=== modified file 'src/dk/aau/cs/gui/smartDraw/SmartDrawWorker.java'
--- src/dk/aau/cs/gui/smartDraw/SmartDrawWorker.java 2020-05-23 12:57:37 +0000
+++ src/dk/aau/cs/gui/smartDraw/SmartDrawWorker.java 2020-07-09 12:55:48 +0000
@@ -2,7 +2,6 @@
22
3import java.awt.Point;3import java.awt.Point;
4import java.util.ArrayList;4import java.util.ArrayList;
5import java.util.Iterator;
6import java.util.List;5import java.util.List;
7import java.util.Random;6import java.util.Random;
87
@@ -199,19 +198,16 @@
199 }198 }
200 }199 }
201 200
202 private ArrayList<Arc> getAllArcsFromObject(PlaceTransitionObject object) {201 private ArrayList<Arc> getAllArcsFromObject(PlaceTransitionObject pno) {
203 ArrayList<Arc> arcsForObject = new ArrayList<Arc>();202 ArrayList<Arc> arcsForObject = new ArrayList<Arc>();
204 Iterator<Arc> fromIterator = object.getConnectFromIterator();203
205 Iterator<Arc> toIterator = object.getConnectToIterator();204 for (Arc a : pno.getPreset()) {
206 Arc arc;205 arcsForObject.add(a);
207 while(fromIterator.hasNext()) {206 }
208 arc = fromIterator.next();207 for (Arc a : pno.getPostset()) {
209 arcsForObject.add(arc);208 arcsForObject.add(a);
210 }209 }
211 while(toIterator.hasNext()) {210
212 arc = toIterator.next();
213 arcsForObject.add(arc);
214 }
215 return arcsForObject;211 return arcsForObject;
216 }212 }
217 private void moveObject(PlaceTransitionObject object, Point point) {213 private void moveObject(PlaceTransitionObject object, Point point) {
218214
=== modified file 'src/dk/aau/cs/gui/undo/TimedPlaceMarkingEdit.java'
--- src/dk/aau/cs/gui/undo/TimedPlaceMarkingEdit.java 2011-09-23 21:23:31 +0000
+++ src/dk/aau/cs/gui/undo/TimedPlaceMarkingEdit.java 2020-07-09 12:55:48 +0000
@@ -4,7 +4,7 @@
44
5// TODO: Fix this to work on the model class instead of the GUI class5// TODO: Fix this to work on the model class instead of the GUI class
6public class TimedPlaceMarkingEdit extends Command {6public class TimedPlaceMarkingEdit extends Command {
7 private int numberOfTokens;7 private final int numberOfTokens;
8 private final TimedPlaceComponent timedPlaceComponent;8 private final TimedPlaceComponent timedPlaceComponent;
99
10 public TimedPlaceMarkingEdit(TimedPlaceComponent tpc, int numberOfTokens) {10 public TimedPlaceMarkingEdit(TimedPlaceComponent tpc, int numberOfTokens) {
@@ -15,9 +15,9 @@
15 @Override15 @Override
16 public void redo() {16 public void redo() {
17 if (numberOfTokens > 0) {17 if (numberOfTokens > 0) {
18 timedPlaceComponent.addTokens(Math.abs(numberOfTokens));18 timedPlaceComponent.underlyingPlace().addTokens(Math.abs(numberOfTokens));
19 } else {19 } else {
20 timedPlaceComponent.removeTokens(Math.abs(numberOfTokens));20 timedPlaceComponent.underlyingPlace().removeTokens(Math.abs(numberOfTokens));
21 }21 }
22 timedPlaceComponent.repaint();22 timedPlaceComponent.repaint();
23 }23 }
@@ -25,9 +25,9 @@
25 @Override25 @Override
26 public void undo() {26 public void undo() {
27 if (numberOfTokens > 0) {27 if (numberOfTokens > 0) {
28 timedPlaceComponent.removeTokens(Math.abs(numberOfTokens));28 timedPlaceComponent.underlyingPlace().removeTokens(Math.abs(numberOfTokens));
29 } else {29 } else {
30 timedPlaceComponent.addTokens(Math.abs(numberOfTokens));30 timedPlaceComponent.underlyingPlace().addTokens(Math.abs(numberOfTokens));
31 }31 }
32 timedPlaceComponent.repaint();32 timedPlaceComponent.repaint();
33 }33 }
3434
=== modified file 'src/dk/aau/cs/io/TapnXmlLoader.java'
--- src/dk/aau/cs/io/TapnXmlLoader.java 2020-05-06 15:19:14 +0000
+++ src/dk/aau/cs/io/TapnXmlLoader.java 2020-07-09 12:55:48 +0000
@@ -162,10 +162,9 @@
162 }162 }
163 163
164 SharedPlace place = new SharedPlace(name, invariant);164 SharedPlace place = new SharedPlace(name, invariant);
165 place.addTokens(numberOfTokens);
165 place.setCurrentMarking(marking);166 place.setCurrentMarking(marking);
166 for(int j = 0; j < numberOfTokens; j++){167
167 marking.add(new TimedToken(place));
168 }
169 return place;168 return place;
170 }169 }
171170
172171
=== modified file 'src/dk/aau/cs/model/tapn/LocalTimedPlace.java'
--- src/dk/aau/cs/model/tapn/LocalTimedPlace.java 2019-11-26 13:59:12 +0000
+++ src/dk/aau/cs/model/tapn/LocalTimedPlace.java 2020-07-09 12:55:48 +0000
@@ -1,28 +1,12 @@
1package dk.aau.cs.model.tapn;1package dk.aau.cs.model.tapn;
22
3import java.util.ArrayList;
4import java.util.List;
5import java.util.regex.Pattern;
6
7import dk.aau.cs.model.tapn.TimedPlace.PlaceType;
8import dk.aau.cs.model.tapn.event.TimedPlaceEvent;
9import dk.aau.cs.model.tapn.event.TimedPlaceListener;
10import dk.aau.cs.util.Require;
11import dk.aau.cs.util.Tuple;3import dk.aau.cs.util.Tuple;
124
13public class LocalTimedPlace extends TimedPlace {5public class LocalTimedPlace extends TimedPlace {
14 private static final Pattern namePattern = Pattern.compile("^[a-zA-Z_][a-zA-Z0-9_]*$");
15
16 private String name;
17 private TimeInvariant invariant;
186
19 private TimedArcPetriNet model;7 private TimedArcPetriNet model;
20 private TimedMarking currentMarking;
21 private List<TimedPlaceListener> listeners = new ArrayList<TimedPlaceListener>();
22
23 private Tuple<PlaceType, Integer> extrapolation = new Tuple<TimedPlace.PlaceType, Integer>(PlaceType.Dead, -2);
248
25 public LocalTimedPlace(String name) {9 public LocalTimedPlace(String name) {
26 this(name, TimeInvariant.LESS_THAN_INFINITY);10 this(name, TimeInvariant.LESS_THAN_INFINITY);
27 }11 }
2812
@@ -39,111 +23,10 @@
39 this.model = model;23 this.model = model;
40 }24 }
4125
42 public void addTimedPlaceListener(TimedPlaceListener listener){
43 Require.that(listener != null, "Listener cannot be null");
44 listeners.add(listener);
45 }
46
47 public void removeTimedPlaceListener(TimedPlaceListener listener){
48 Require.that(listener != null, "Listener cannot be null");
49 listeners.remove(listener);
50 }
51
52 public boolean isShared() {26 public boolean isShared() {
53 return false;27 return false;
54 }28 }
5529
56 public void setCurrentMarking(TimedMarking marking) {
57 Require.that(marking != null, "marking cannot be null");
58 currentMarking = marking;
59 fireMarkingChanged();
60 }
61
62 public String name() {
63 return name;
64 }
65
66 public void setName(String newName) {
67 Require.that(newName != null && !newName.isEmpty(), "A timed place must have a name");
68 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_]*");
69 this.name = newName;
70 fireNameChanged();
71 }
72
73 private void fireNameChanged() {
74 for(TimedPlaceListener listener : listeners){
75 listener.nameChanged(new TimedPlaceEvent(this));
76 }
77 }
78
79 private void fireInvariantChanged(){
80 for(TimedPlaceListener listener : listeners){
81 listener.invariantChanged(new TimedPlaceEvent(this));
82 }
83 }
84
85 private void fireMarkingChanged(){
86 for(TimedPlaceListener listener : listeners){
87 listener.markingChanged(new TimedPlaceEvent(this));
88 }
89 }
90
91 private boolean isValid(String newName) {
92 return namePattern.matcher(newName).matches();
93 }
94
95 public TimeInvariant invariant() {
96 return invariant;
97 }
98
99 public void setInvariant(TimeInvariant invariant) {
100 Require.that(invariant != null, "A timed place must have a non-null invariant");
101 this.invariant = invariant;
102 fireInvariantChanged();
103 }
104
105 public List<TimedToken> tokens() {
106 return currentMarking.getTokensFor(this);
107 }
108
109 public int numberOfTokens() {
110 return tokens().size();
111 }
112
113 @Override
114 public void addToken(TimedToken timedToken) {
115 Require.that(timedToken != null, "timedToken cannot be null");
116 Require.that(timedToken.place().equals(this), "token is located in a different place");
117
118 currentMarking.add(timedToken);
119 fireMarkingChanged();
120 }
121
122 @Override
123 public void addTokens(Iterable<TimedToken> tokens) {
124 Require.that(tokens != null, "tokens cannot be null");
125
126 for(TimedToken token : tokens){
127 currentMarking.add(token); // avoid firing marking changed on every add
128 }
129 fireMarkingChanged();
130 }
131
132 @Override
133 public void removeToken(TimedToken timedToken) {
134 Require.that(timedToken != null, "timedToken cannot be null");
135 currentMarking.remove(timedToken);
136 fireMarkingChanged();
137 }
138
139 @Override
140 public void removeToken() {
141 if (numberOfTokens() > 0) {
142 currentMarking.remove(tokens().get(0));
143 fireMarkingChanged();
144 }
145 }
146
147 public LocalTimedPlace copy() {30 public LocalTimedPlace copy() {
148 LocalTimedPlace p = new LocalTimedPlace(name);31 LocalTimedPlace p = new LocalTimedPlace(name);
14932
15033
=== modified file 'src/dk/aau/cs/model/tapn/NetworkMarking.java'
--- src/dk/aau/cs/model/tapn/NetworkMarking.java 2020-05-23 13:29:16 +0000
+++ src/dk/aau/cs/model/tapn/NetworkMarking.java 2020-07-09 12:55:48 +0000
@@ -14,8 +14,8 @@
14import dk.aau.cs.util.Tuple;14import dk.aau.cs.util.Tuple;
1515
16public class NetworkMarking implements TimedMarking {16public class NetworkMarking implements TimedMarking {
17 private HashMap<TimedArcPetriNet, LocalTimedMarking> markings = new HashMap<TimedArcPetriNet, LocalTimedMarking>();17 private final HashMap<TimedArcPetriNet, LocalTimedMarking> markings = new HashMap<TimedArcPetriNet, LocalTimedMarking>();
18 private HashMap<TimedPlace, List<TimedToken>> sharedPlacesTokens = new HashMap<TimedPlace, List<TimedToken>>();18 private final HashMap<TimedPlace, List<TimedToken>> sharedPlacesTokens = new HashMap<TimedPlace, List<TimedToken>>();
1919
20 public NetworkMarking() {20 public NetworkMarking() {
21 }21 }
@@ -130,8 +130,9 @@
130 private Tuple<NetworkMarking, List<TimedToken>> fireSharedTransition(SharedTransition sharedTransition, FiringMode firingMode) {130 private Tuple<NetworkMarking, List<TimedToken>> fireSharedTransition(SharedTransition sharedTransition, FiringMode firingMode) {
131 // validity of arguments already checked above131 // validity of arguments already checked above
132 NetworkMarking clone = clone();132 NetworkMarking clone = clone();
133 Tuple<LocalTimedMarking, List<TimedToken>> ltm;133 Tuple<LocalTimedMarking, List<TimedToken>> ltm;
134 List<TimedToken> consumedTokens = new ArrayList<TimedToken>();134 List<TimedToken> consumedTokens = new ArrayList<TimedToken>();
135
135 for(TimedTransition transition : sharedTransition.transitions()){136 for(TimedTransition transition : sharedTransition.transitions()){
136 if(transition.model().isActive()) {137 if(transition.model().isActive()) {
137 ltm = clone.getMarkingFor(transition.model()).fireTransition(transition, firingMode);138 ltm = clone.getMarkingFor(transition.model()).fireTransition(transition, firingMode);
138139
=== modified file 'src/dk/aau/cs/model/tapn/SharedPlace.java'
--- src/dk/aau/cs/model/tapn/SharedPlace.java 2020-06-03 18:20:30 +0000
+++ src/dk/aau/cs/model/tapn/SharedPlace.java 2020-07-09 12:55:48 +0000
@@ -1,30 +1,16 @@
1package dk.aau.cs.model.tapn;1package dk.aau.cs.model.tapn;
22
3import java.util.ArrayList;3import java.util.ArrayList;
4import java.util.List;
5import java.util.regex.Pattern;
64
7import pipe.dataLayer.Template;5import pipe.dataLayer.Template;
8import pipe.gui.CreateGui;6import pipe.gui.CreateGui;
9import dk.aau.cs.model.tapn.event.TimedPlaceEvent;
10import dk.aau.cs.model.tapn.event.TimedPlaceListener;
11import dk.aau.cs.util.Require;
12import dk.aau.cs.util.Tuple;7import dk.aau.cs.util.Tuple;
138
14public class SharedPlace extends TimedPlace{9public class SharedPlace extends TimedPlace{
15 private static final Pattern namePattern = Pattern.compile("^[a-zA-Z_][a-zA-Z0-9_]*$");10
16 11 private TimedArcPetriNetNetwork network;
17 private String name;12
18 private List<TimedPlace> places = new ArrayList<TimedPlace>();13 public SharedPlace(String name){
19 private TimeInvariant invariant;
20
21 private TimedArcPetriNetNetwork network;
22 private TimedMarking currentMarking;
23 private Tuple<PlaceType, Integer> extrapolation = new Tuple<TimedPlace.PlaceType, Integer>(PlaceType.Dead, -2);
24
25 private List<TimedPlaceListener> listeners = new ArrayList<TimedPlaceListener>();
26
27 public SharedPlace(String name){
28 this(name, TimeInvariant.LESS_THAN_INFINITY);14 this(name, TimeInvariant.LESS_THAN_INFINITY);
29 }15 }
30 16
@@ -32,33 +18,8 @@
32 setName(name);18 setName(name);
33 setInvariant(invariant);19 setInvariant(invariant);
34 }20 }
35 21
36 public String name() {22 public void setNetwork(TimedArcPetriNetNetwork network) {
37 return name;
38 }
39
40 public void setName(String newName) {
41 Require.that(newName != null && !newName.isEmpty(), "A timed transition must have a name");
42 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_]*");
43 name = newName;
44 fireNameChanged();
45 }
46
47 private boolean isValid(String newName) {
48 return namePattern.matcher(newName).matches();
49 }
50
51 public TimeInvariant invariant(){
52 return invariant;
53 }
54
55 public void setInvariant(TimeInvariant invariant) {
56 Require.that(invariant != null, "invariant must not be null");
57 this.invariant = invariant;
58 fireInvariantChanged();
59 }
60
61 public void setNetwork(TimedArcPetriNetNetwork network) {
62 this.network = network; 23 this.network = network;
63 }24 }
64 25
@@ -66,15 +27,7 @@
66 return network;27 return network;
67 }28 }
68 29
69 public void addTimedPlaceListener(TimedPlaceListener listener) {
70 Require.that(listener != null, "Listener cannot be null");
71 listeners.add(listener);
72 }
7330
74 public void removeTimedPlaceListener(TimedPlaceListener listener) {
75 Require.that(listener != null, "Listener cannot be null");
76 listeners.remove(listener);
77 }
7831
79 public TimedPlace copy() {32 public TimedPlace copy() {
80 return new SharedPlace(this.name(), this.invariant().copy());33 return new SharedPlace(this.name(), this.invariant().copy());
@@ -84,71 +37,6 @@
84 return true;37 return true;
85 }38 }
8639
87 public void setCurrentMarking(TimedMarking marking) {
88 Require.that(marking != null, "marking cannot be null");
89 currentMarking = marking;
90 fireMarkingChanged();
91 }
92
93 @Override
94 public void addToken(TimedToken timedToken) {
95 Require.that(timedToken != null, "timedToken cannot be null");
96 Require.that(timedToken.place().equals(this), "token is located in a different place");
97
98 currentMarking.add(timedToken);
99 fireMarkingChanged();
100 }
101
102 @Override
103 public void addTokens(Iterable<TimedToken> tokens) {
104 Require.that(tokens != null, "tokens cannot be null"); // TODO: maybe check that tokens are in this place?
105
106 for(TimedToken token : tokens){
107 currentMarking.add(token); // avoid firing marking changed on every add
108 }
109 fireMarkingChanged();
110 }
111
112 @Override
113 public void removeToken(TimedToken timedToken) {
114 Require.that(timedToken != null, "timedToken cannot be null");
115 currentMarking.remove(timedToken);
116 fireMarkingChanged();
117 }
118
119 @Override
120 public void removeToken() {
121 if (numberOfTokens() > 0) {
122 currentMarking.remove(tokens().get(0));
123 fireMarkingChanged();
124 }
125 }
126
127 public List<TimedToken> tokens() {
128 return currentMarking.getTokensFor(this);
129 }
130
131 public int numberOfTokens() {
132 return tokens().size();
133 }
134
135 private void fireMarkingChanged() {
136 for(TimedPlaceListener listener : listeners){
137 listener.markingChanged(new TimedPlaceEvent(this));
138 }
139 }
140
141 private void fireNameChanged() {
142 for(TimedPlaceListener listener : listeners){
143 listener.nameChanged(new TimedPlaceEvent(this));
144 }
145 }
146
147 private void fireInvariantChanged() {
148 for(TimedPlaceListener listener : listeners){
149 listener.invariantChanged(new TimedPlaceEvent(this));
150 }
151 }
152 40
153 public ArrayList<String> getComponentsUsingThisPlace(){41 public ArrayList<String> getComponentsUsingThisPlace(){
154 ArrayList<String> components = new ArrayList<String>();42 ArrayList<String> components = new ArrayList<String>();
@@ -214,8 +102,4 @@
214 102
215 return new Tuple<TimedPlace.PlaceType, Integer>(type, cmax);103 return new Tuple<TimedPlace.PlaceType, Integer>(type, cmax);
216 }104 }
217
218 public List<TimedPlace> getPlaces() {
219 return places;
220 }
221}105}
222106
=== modified file 'src/dk/aau/cs/model/tapn/TimedArcPetriNet.java'
--- src/dk/aau/cs/model/tapn/TimedArcPetriNet.java 2020-06-03 12:16:19 +0000
+++ src/dk/aau/cs/model/tapn/TimedArcPetriNet.java 2020-07-09 12:55:48 +0000
@@ -18,18 +18,17 @@
18 //This is used when loading big nets as the checking of names is slow.18 //This is used when loading big nets as the checking of names is slow.
19 private boolean checkNames = true; 19 private boolean checkNames = true;
2020
21 private List<TimedPlace> places = new ArrayList<TimedPlace>();21 private final List<TimedPlace> places = new ArrayList<TimedPlace>();
22 private List<TimedTransition> transitions = new ArrayList<TimedTransition>();22 private final List<TimedTransition> transitions = new ArrayList<TimedTransition>();
23 private List<TimedInputArc> inputArcs = new ArrayList<TimedInputArc>();23 private final List<TimedInputArc> inputArcs = new ArrayList<TimedInputArc>();
24 private List<TimedOutputArc> outputArcs = new ArrayList<TimedOutputArc>();24 private final List<TimedOutputArc> outputArcs = new ArrayList<TimedOutputArc>();
25 private List<TimedInhibitorArc> inhibitorArcs = new ArrayList<TimedInhibitorArc>();25 private final List<TimedInhibitorArc> inhibitorArcs = new ArrayList<TimedInhibitorArc>();
26 private List<TransportArc> transportArcs = new ArrayList<TransportArc>();26 private final List<TransportArc> transportArcs = new ArrayList<TransportArc>();
2727
28 private TimedMarking currentMarking;28 private TimedMarking currentMarking = new LocalTimedMarking();
2929
30 public TimedArcPetriNet(String name) {30 public TimedArcPetriNet(String name) {
31 setName(name);31 setName(name);
32 setMarking(new LocalTimedMarking());
33 isActive = true;32 isActive = true;
34 }33 }
3534
@@ -127,11 +126,7 @@
127 currentMarking.add(token);126 currentMarking.add(token);
128 }127 }
129128
130 public void removeToken(TimedToken token) {129 public void remove(TimedPlace place) {
131 currentMarking.remove(token);
132 }
133
134 public void remove(TimedPlace place) {
135 boolean removed = places.remove(place);130 boolean removed = places.remove(place);
136 if (removed && !place.isShared()){131 if (removed && !place.isShared()){
137 currentMarking.removePlaceFromMarking(place);132 currentMarking.removePlaceFromMarking(place);
138133
=== modified file 'src/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java'
--- src/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java 2019-03-22 13:57:03 +0000
+++ src/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java 2020-07-09 12:55:48 +0000
@@ -15,16 +15,16 @@
15import dk.aau.cs.verification.TAPNComposer;15import dk.aau.cs.verification.TAPNComposer;
1616
17public class TimedArcPetriNetNetwork {17public class TimedArcPetriNetNetwork {
18 private List<TimedArcPetriNet> tapns = new ArrayList<TimedArcPetriNet>();18 private final List<TimedArcPetriNet> tapns = new ArrayList<TimedArcPetriNet>();
19 private List<SharedPlace> sharedPlaces = new ArrayList<SharedPlace>();19 private final List<SharedPlace> sharedPlaces = new ArrayList<SharedPlace>();
20 private List<SharedTransition> sharedTransitions = new ArrayList<SharedTransition>();20 private final List<SharedTransition> sharedTransitions = new ArrayList<SharedTransition>();
21 21
22 private NetworkMarking currentMarking;22 private NetworkMarking currentMarking = new NetworkMarking();
23 private ConstantStore constants;23 private final ConstantStore constants;
24 24
25 private int defaultBound = 3;25 private int defaultBound = 3;
26 26
27 private List<ConstantsListener> constantsListeners = new ArrayList<ConstantsListener>();27 private final List<ConstantsListener> constantsListeners = new ArrayList<ConstantsListener>();
28 28
29 private boolean paintNet = true;29 private boolean paintNet = true;
30 30
@@ -34,8 +34,7 @@
34 34
35 public TimedArcPetriNetNetwork(ConstantStore constants){35 public TimedArcPetriNetNetwork(ConstantStore constants){
36 this.constants = constants;36 this.constants = constants;
37 currentMarking = new NetworkMarking();37 buildConstraints();
38 buildConstraints();
39 }38 }
40 39
41 public void addConstantsListener(ConstantsListener listener){40 public void addConstantsListener(ConstantsListener listener){
4241
=== modified file 'src/dk/aau/cs/model/tapn/TimedInhibitorArc.java'
--- src/dk/aau/cs/model/tapn/TimedInhibitorArc.java 2012-09-19 18:15:59 +0000
+++ src/dk/aau/cs/model/tapn/TimedInhibitorArc.java 2020-07-09 12:55:48 +0000
@@ -14,8 +14,12 @@
14 public TimedInhibitorArc(TimedPlace source, TimedTransition destination, TimeInterval interval, Weight weight) {14 public TimedInhibitorArc(TimedPlace source, TimedTransition destination, TimeInterval interval, Weight weight) {
15 super(source, destination, TimeInterval.ZERO_INF, weight);15 super(source, destination, TimeInterval.ZERO_INF, weight);
16 }16 }
17 17
18 public List<TimeInterval> getDEnabledInterval(){18 public TimedInhibitorArc(TimedPlace source, TimedTransition destination) {
19 this(source, destination, TimeInterval.ZERO_INF, new IntWeight(1));
20 }
21
22 public List<TimeInterval> getDEnabledInterval(){
19 if(source().tokens().size() < getWeight().value()){23 if(source().tokens().size() < getWeight().value()){
20 return Arrays.asList(new TimeInterval(true, new RatBound(BigDecimal.ZERO), Bound.Infinity, false));24 return Arrays.asList(new TimeInterval(true, new RatBound(BigDecimal.ZERO), Bound.Infinity, false));
21 } else {25 } else {
2226
=== modified file 'src/dk/aau/cs/model/tapn/TimedPlace.java'
--- src/dk/aau/cs/model/tapn/TimedPlace.java 2020-06-03 12:16:19 +0000
+++ src/dk/aau/cs/model/tapn/TimedPlace.java 2020-07-09 12:55:48 +0000
@@ -1,13 +1,24 @@
1package dk.aau.cs.model.tapn;1package dk.aau.cs.model.tapn;
22
3import java.math.BigDecimal;
3import java.util.ArrayList;4import java.util.ArrayList;
4import java.util.List;5import java.util.List;
6import java.util.regex.Pattern;
57
8import dk.aau.cs.model.tapn.event.TimedPlaceEvent;
6import dk.aau.cs.model.tapn.event.TimedPlaceListener;9import dk.aau.cs.model.tapn.event.TimedPlaceListener;
7import dk.aau.cs.util.Require;10import dk.aau.cs.util.Require;
8import dk.aau.cs.util.Tuple;11import dk.aau.cs.util.Tuple;
912
10public abstract class TimedPlace {13public abstract class TimedPlace {
14
15 protected static final Pattern namePattern = Pattern.compile("^[a-zA-Z_][a-zA-Z0-9_]*$");
16 protected final List<TimedPlaceListener> listeners = new ArrayList<TimedPlaceListener>();
17 protected Tuple<PlaceType, Integer> extrapolation = new Tuple<PlaceType, Integer>(PlaceType.Dead, -2);
18 protected String name;
19 protected TimeInvariant invariant;
20 protected TimedMarking currentMarking;
21
11 private SharedPlace sharedPlace;22 private SharedPlace sharedPlace;
12 private List<TimedOutputArc> postset = new ArrayList<TimedOutputArc>();23 private List<TimedOutputArc> postset = new ArrayList<TimedOutputArc>();
13 private List<TimedInputArc> preset = new ArrayList<TimedInputArc>();24 private List<TimedInputArc> preset = new ArrayList<TimedInputArc>();
@@ -17,28 +28,67 @@
17 public enum PlaceType{28 public enum PlaceType{
18 Standard, Invariant, Dead29 Standard, Invariant, Dead
19 }30 }
20
21 public abstract void addTimedPlaceListener(TimedPlaceListener listener);
22 public abstract void removeTimedPlaceListener(TimedPlaceListener listener);
2331
24 public abstract boolean isShared();32 public abstract boolean isShared();
2533
26 public abstract String name();34 public String name() {
27 public abstract void setName(String newName);35 return name;
2836 }
29 public abstract TimeInvariant invariant();37
30 public abstract void setInvariant(TimeInvariant invariant);38 public void setName(String newName) {
3139 Require.that(newName != null && !newName.isEmpty(), "A timed place must have a name");
32 public abstract List<TimedToken> tokens();40 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_]*");
33 public abstract int numberOfTokens();41 this.name = newName;
3442 fireNameChanged();
35 public abstract void setCurrentMarking(TimedMarking marking);43 }
36 44
37 public abstract void addToken(TimedToken timedToken);45 public TimeInvariant invariant(){
38 public abstract void addTokens(Iterable<TimedToken> tokens);46 return invariant;
3947 }
40 public abstract void removeToken(TimedToken timedToken);48
41 public abstract void removeToken();49 public List<TimedToken> tokens() {
50 return currentMarking.getTokensFor(this);
51 }
52
53 public int numberOfTokens() {
54 return tokens().size();
55 }
56
57 public void addToken(TimedToken timedToken) {
58 Require.that(timedToken != null, "timedToken cannot be null");
59 Require.that(timedToken.place().equals(this), "token is located in a different place");
60
61 currentMarking.add(timedToken);
62 fireMarkingChanged();
63 }
64
65 public void addTokens(Iterable<TimedToken> tokens) {
66 Require.that(tokens != null, "tokens cannot be null");
67
68 for(TimedToken token : tokens){
69 currentMarking.add(token); // avoid firing marking changed on every add
70 }
71 fireMarkingChanged();
72 }
73
74 public void addTokens(int numberOfTokensToAdd) {
75 for (int i = 0; i < numberOfTokensToAdd; i++) {
76 addToken(new TimedToken(this, BigDecimal.ZERO));
77 }
78 }
79
80 public void removeTokens(int numberOfTokensToRemove) {
81 for (int i = 0; i < numberOfTokensToRemove; i++) {
82 removeToken();
83 }
84 }
85
86 public void removeToken() {
87 if (numberOfTokens() > 0) {
88 currentMarking.remove(tokens().get(0));
89 fireMarkingChanged();
90 }
91 }
42 92
43 public abstract Tuple<PlaceType, Integer> extrapolate();93 public abstract Tuple<PlaceType, Integer> extrapolate();
44 94
@@ -65,6 +115,51 @@
65 return name() == other.name();115 return name() == other.name();
66 }116 }
67117
118
119 protected void fireMarkingChanged() {
120 for(TimedPlaceListener listener : listeners){
121 listener.markingChanged(new TimedPlaceEvent(this));
122 }
123 }
124
125 protected void fireNameChanged() {
126 for(TimedPlaceListener listener : listeners){
127 listener.nameChanged(new TimedPlaceEvent(this));
128 }
129 }
130
131 protected void fireInvariantChanged() {
132 for(TimedPlaceListener listener : listeners){
133 listener.invariantChanged(new TimedPlaceEvent(this));
134 }
135 }
136
137 protected boolean isValid(String newName) {
138 return namePattern.matcher(newName).matches();
139 }
140
141 public void setInvariant(TimeInvariant invariant) {
142 Require.that(invariant != null, "invariant must not be null");
143 this.invariant = invariant;
144 fireInvariantChanged();
145 }
146
147 public void addTimedPlaceListener(TimedPlaceListener listener) {
148 Require.that(listener != null, "Listener cannot be null");
149 listeners.add(listener);
150 }
151
152 public void removeTimedPlaceListener(TimedPlaceListener listener) {
153 Require.that(listener != null, "Listener cannot be null");
154 listeners.remove(listener);
155 }
156
157 public void setCurrentMarking(TimedMarking marking) {
158 Require.that(marking != null, "marking cannot be null");
159 currentMarking = marking;
160 fireMarkingChanged();
161 }
162
68 public boolean isOrphan() {163 public boolean isOrphan() {
69 return presetSize() == 0 && postsetSize() == 0;164 return presetSize() == 0 && postsetSize() == 0;
70 }165 }
@@ -112,16 +207,4 @@
112 return postset.size() + transportArcs.size() + inhibitorArcs.size();207 return postset.size() + transportArcs.size() + inhibitorArcs.size();
113 }208 }
114209
115// public abstract void addInhibitorArc(TimedInhibitorArc arc);
116// public abstract void addToPreset(TransportArc arc);
117// public abstract void addToPreset(TimedOutputArc arc);
118// public abstract void addToPostset(TransportArc arc);
119// public abstract void addToPostset(TimedInputArc arc);
120//
121// public abstract void removeFromPostset(TimedInputArc arc);
122// public abstract void removeFromPostset(TransportArc arc);
123// public abstract void removeFromPreset(TransportArc arc);
124// public abstract void removeFromPreset(TimedOutputArc arc);
125// public abstract void removeInhibitorArc(TimedInhibitorArc arc);
126
127}210}
128\ No newline at end of file211\ No newline at end of file
129212
=== modified file 'src/dk/aau/cs/model/tapn/TimedToken.java'
--- src/dk/aau/cs/model/tapn/TimedToken.java 2019-03-23 07:51:29 +0000
+++ src/dk/aau/cs/model/tapn/TimedToken.java 2020-07-09 12:55:48 +0000
@@ -31,8 +31,7 @@
31 }31 }
32 32
33 public TimedToken clone() {33 public TimedToken clone() {
34 return new TimedToken(place, age); // age is immutable so ok to pass it34 return new TimedToken(place, age); // age is immutable so ok to pass it to constructor
35 // to constructor
36 }35 }
3736
38 public TimedToken delay(BigDecimal delay) {37 public TimedToken delay(BigDecimal delay) {
@@ -44,12 +43,7 @@
44 DecimalFormat df = new DecimalFormat();43 DecimalFormat df = new DecimalFormat();
45 df.setMaximumFractionDigits(Pipe.AGE_DECIMAL_PRECISION);44 df.setMaximumFractionDigits(Pipe.AGE_DECIMAL_PRECISION);
4645
47 StringBuilder buffer = new StringBuilder("(");46 return String.format("(%s, %s)", place.toString(), df.format(age));
48 buffer.append(place.toString());
49 buffer.append(", ");
50 buffer.append(df.format(age));
51 buffer.append(')');
52 return buffer.toString();
53 }47 }
5448
55 @Override49 @Override
5650
=== modified file 'src/dk/aau/cs/model/tapn/TimedTransition.java'
--- src/dk/aau/cs/model/tapn/TimedTransition.java 2020-06-18 20:57:07 +0000
+++ src/dk/aau/cs/model/tapn/TimedTransition.java 2020-07-09 12:55:48 +0000
@@ -17,16 +17,16 @@
17 private static final Pattern namePattern = Pattern.compile("^[a-zA-Z_][a-zA-Z0-9_]*$");17 private static final Pattern namePattern = Pattern.compile("^[a-zA-Z_][a-zA-Z0-9_]*$");
1818
19 private String name;19 private String name;
20 private List<TimedOutputArc> postset = new ArrayList<TimedOutputArc>();20 private final List<TimedOutputArc> postset = new ArrayList<TimedOutputArc>();
21 private List<TimedInputArc> preset = new ArrayList<TimedInputArc>();21 private final List<TimedInputArc> preset = new ArrayList<TimedInputArc>();
22 private List<TransportArc> transportArcsGoingThrough = new ArrayList<TransportArc>();22 private final List<TransportArc> transportArcsGoingThrough = new ArrayList<TransportArc>();
23 private List<TimedInhibitorArc> inhibitorArcs = new ArrayList<TimedInhibitorArc>();23 private final List<TimedInhibitorArc> inhibitorArcs = new ArrayList<TimedInhibitorArc>();
24 private TimeInterval dInterval = null;24 private TimeInterval dInterval = null;
25 private boolean isUrgent = false;25 private boolean isUrgent = false;
2626
27 private SharedTransition sharedTransition;27 private SharedTransition sharedTransition;
2828
29 private List<TimedTransitionListener> listeners = new ArrayList<TimedTransitionListener>();29 private final List<TimedTransitionListener> listeners = new ArrayList<TimedTransitionListener>();
3030
31 public TimedTransition(String name) {31 public TimedTransition(String name) {
32 this(name, false);32 this(name, false);
3333
=== modified file 'src/dk/aau/cs/model/tapn/TransportArc.java'
--- src/dk/aau/cs/model/tapn/TransportArc.java 2018-05-13 19:54:55 +0000
+++ src/dk/aau/cs/model/tapn/TransportArc.java 2020-07-09 12:55:48 +0000
@@ -36,8 +36,12 @@
36 setTimeInterval(interval);36 setTimeInterval(interval);
37 this.weight = weight;37 this.weight = weight;
38 }38 }
39 39
40 public Weight getWeight(){40 public TransportArc(TimedPlace source, TimedTransition transitions, TimedPlace destination) {
41 this(source, transitions, destination, TimeInterval.ZERO_INF);
42 }
43
44 public Weight getWeight(){
41 return weight;45 return weight;
42 }46 }
43 47
4448
=== modified file 'src/net/tapaal/gui/DrawingSurfaceManager/AbstractDrawingSurfaceManager.java'
--- src/net/tapaal/gui/DrawingSurfaceManager/AbstractDrawingSurfaceManager.java 2020-04-18 14:41:05 +0000
+++ src/net/tapaal/gui/DrawingSurfaceManager/AbstractDrawingSurfaceManager.java 2020-07-09 12:55:48 +0000
@@ -1,5 +1,7 @@
1package net.tapaal.gui.DrawingSurfaceManager;1package net.tapaal.gui.DrawingSurfaceManager;
22
3import pipe.gui.canvas.DrawingSurfaceImpl;
4import pipe.gui.graphicElements.GraphicalElement;
3import pipe.gui.graphicElements.PetriNetObject;5import pipe.gui.graphicElements.PetriNetObject;
46
5import java.awt.event.MouseEvent;7import java.awt.event.MouseEvent;
@@ -11,6 +13,8 @@
1113
12public abstract class AbstractDrawingSurfaceManager {14public abstract class AbstractDrawingSurfaceManager {
1315
16 protected DrawingSurfaceImpl canvas;
17
14 public void drawingSurfaceMouseClicked(MouseEvent e) {}18 public void drawingSurfaceMouseClicked(MouseEvent e) {}
15 public void drawingSurfaceMousePressed(MouseEvent e) {}19 public void drawingSurfaceMousePressed(MouseEvent e) {}
16 public void drawingSurfaceMouseReleased(MouseEvent e){}20 public void drawingSurfaceMouseReleased(MouseEvent e){}
@@ -20,6 +24,8 @@
2024
21 public enum MouseAction {25 public enum MouseAction {
22 clicked,26 clicked,
27 doubleClicked,
28 rightClicked,
23 pressed,29 pressed,
24 released,30 released,
25 dragged,31 dragged,
@@ -31,12 +37,12 @@
31 public static class DrawingSurfaceEvent {37 public static class DrawingSurfaceEvent {
3238
3339
34 public final PetriNetObject pno;40 public final GraphicalElement pno;
35 public final MouseEvent e;41 public final MouseEvent e;
36 public final MouseAction a;42 public final MouseAction a;
37 //Mouse Event type eg click mouse over etc43 //Mouse Event type eg click mouse over etc
3844
39 public DrawingSurfaceEvent(PetriNetObject pno, MouseEvent e, MouseAction a) {45 public DrawingSurfaceEvent(GraphicalElement pno, MouseEvent e, MouseAction a) {
40 this.pno = pno;46 this.pno = pno;
41 this.e = e;47 this.e = e;
42 this.a = a;48 this.a = a;
@@ -47,8 +53,12 @@
47 private final Map<Predicate<DrawingSurfaceEvent>, Consumer<DrawingSurfaceEvent>> filter = new LinkedHashMap<>();53 private final Map<Predicate<DrawingSurfaceEvent>, Consumer<DrawingSurfaceEvent>> filter = new LinkedHashMap<>();
48 private final AbstractDrawingSurfaceManager next = null;54 private final AbstractDrawingSurfaceManager next = null;
4955
50 public void registerManager(){}56 public void registerManager(DrawingSurfaceImpl canvas){
51 public void deregisterManager(){}57 this.canvas = canvas;
58 }
59 public void deregisterManager(){
60 this.canvas = null;
61 }
5262
53 public AbstractDrawingSurfaceManager() {63 public AbstractDrawingSurfaceManager() {
54 registerEvents();64 registerEvents();
5565
=== added file 'src/net/tapaal/swinghelpers/DispatchEventsToParentHandler.java'
--- src/net/tapaal/swinghelpers/DispatchEventsToParentHandler.java 1970-01-01 00:00:00 +0000
+++ src/net/tapaal/swinghelpers/DispatchEventsToParentHandler.java 2020-07-09 12:55:48 +0000
@@ -0,0 +1,58 @@
1package net.tapaal.swinghelpers;
2
3import javax.swing.*;
4import java.awt.*;
5import java.awt.event.*;
6
7public final class DispatchEventsToParentHandler implements MouseListener, MouseWheelListener, MouseMotionListener {
8
9 private static void dispatchEventToParent(MouseEvent e) {
10 if(e.getSource() instanceof Component) {
11 Component c = ((Component) e.getSource());
12 if (c.getParent() != null) {
13 SwingUtilities.convertPoint(c, e.getPoint(), c.getParent());
14 c.getParent().dispatchEvent(e);
15 }
16 }
17 }
18
19 @Override
20 public final void mouseClicked(MouseEvent e) {
21 dispatchEventToParent(e);
22 }
23
24 @Override
25 public final void mousePressed(MouseEvent e) {
26 dispatchEventToParent(e);
27 }
28
29 @Override
30 public final void mouseReleased(MouseEvent e) {
31 dispatchEventToParent(e);
32 }
33
34 @Override
35 public final void mouseEntered(MouseEvent e) {
36 dispatchEventToParent(e);
37 }
38
39 @Override
40 public final void mouseExited(MouseEvent e) {
41 dispatchEventToParent(e);
42 }
43
44 @Override
45 public final void mouseDragged(MouseEvent e) {
46 dispatchEventToParent(e);
47 }
48
49 @Override
50 public final void mouseMoved(MouseEvent e) {
51 dispatchEventToParent(e);
52 }
53
54 @Override
55 public final void mouseWheelMoved(MouseWheelEvent e) {
56 dispatchEventToParent(e);
57 }
58}
059
=== modified file 'src/pipe/dataLayer/DataLayer.java'
--- src/pipe/dataLayer/DataLayer.java 2020-05-18 10:06:28 +0000
+++ src/pipe/dataLayer/DataLayer.java 2020-07-09 12:55:48 +0000
@@ -29,36 +29,36 @@
29 //migth not be best solution long term.29 //migth not be best solution long term.
30 private void removeFromViewIfConnected(PetriNetObject pno) {30 private void removeFromViewIfConnected(PetriNetObject pno) {
31 if (view != null) {31 if (view != null) {
32 view.removePetriNetObject(pno);32 view.removePetriNetObject(pno.getGraphicalElement());
33 }33 }
34 }34 }
3535
36 private void addToViewIfConnected(PetriNetObject pno) {36 private void addToViewIfConnected(PetriNetObject pno) {
37 if (view != null) {37 if (view != null) {
38 view.addNewPetriNetObject(pno);38 view.addNewPetriNetObject(pno.getGraphicalElement());
39 }39 }
40 }40 }
4141
42 /** PNML File Name */42 /** PNML File Name */
43 public String pnmlName = null;43 public String pnmlName = null;
44 /** List containing all the Place objects in the Petri-Net */44 /** List containing all the Place objects in the Petri-Net */
45 private ArrayList<Place> placesArray = null;45 private final ArrayList<Place> placesArray = new ArrayList<Place>();
46 /** ArrayList containing all the Transition objects in the Petri-Net */46 /** ArrayList containing all the Transition objects in the Petri-Net */
47 private ArrayList<Transition> transitionsArray = null;47 private final ArrayList<Transition> transitionsArray = new ArrayList<Transition>();
48 /** ArrayList containing all the Arc objects in the Petri-Net */48 /** ArrayList containing all the Arc objects in the Petri-Net */
49 private ArrayList<Arc> arcsArray = null;49 private final ArrayList<Arc> arcsArray = new ArrayList<Arc>();
5050
51 /** Set holding all ArcPathPoints51 /** Set holding all ArcPathPoints
52 * Uses the reference as lookup key (not hash code)52 * Uses the reference as lookup key (not hash code)
53 * Collections.newSetFromMap(new IdentityHashMap<E, Boolean>());53 * Collections.newSetFromMap(new IdentityHashMap<E, Boolean>());
54 * */54 * */
55 private Set<ArcPathPoint> arcPathSet = Collections.newSetFromMap(new IdentityHashMap<>());55 private final Set<ArcPathPoint> arcPathSet = Collections.newSetFromMap(new IdentityHashMap<>());
5656
57 /**57 /**
58 * ArrayList for net-level label objects (as opposed to element-level58 * ArrayList for net-level label objects (as opposed to element-level
59 * labels).59 * labels).
60 */60 */
61 private ArrayList<AnnotationNote> labelsArray = null;61 private final ArrayList<AnnotationNote> labelsArray = new ArrayList<AnnotationNote>();
6262
63 /**63 /**
64 * An ArrayList used to point to either the Arc, Place or Transition64 * An ArrayList used to point to either the Arc, Place or Transition
@@ -66,22 +66,23 @@
66 */66 */
67 private ArrayList<? extends PetriNetObject> changeArrayList = null;67 private ArrayList<? extends PetriNetObject> changeArrayList = null;
6868
69 /**69 // may as well do the hashtable here as well
70 /**
70 * Hashtable which maps PlaceTransitionObjects to their list of connected71 * Hashtable which maps PlaceTransitionObjects to their list of connected
71 * arcs72 * arcs
72 */73 */
73 private Hashtable<PlaceTransitionObject, ArrayList<TimedOutputArcComponent>> arcsMap = null;74 private final Hashtable<PlaceTransitionObject, ArrayList<TimedOutputArcComponent>> arcsMap = new Hashtable<PlaceTransitionObject, ArrayList<TimedOutputArcComponent>>();
7475
75 /**76 /**
76 * Hashtable which maps PlaceTransitionObjects to their list of connected77 * Hashtable which maps PlaceTransitionObjects to their list of connected
77 * arcs78 * arcs
78 */79 */
79 private Hashtable<PlaceTransitionObject, ArrayList<TimedInhibitorArcComponent>> tapnInhibitorsMap = null;80 private final Hashtable<PlaceTransitionObject, ArrayList<TimedInhibitorArcComponent>> tapnInhibitorsMap = new Hashtable<PlaceTransitionObject, ArrayList<TimedInhibitorArcComponent>>();
8081
8182
82 //XXX: Added from drawingsurface to have a way to acces all elements added,83 //XXX: Added from drawingsurface to have a way to acces all elements added,
83 //Should be refactored later to combine the existing list, however this is the quick fix during refactoring84 //Should be refactored later to combine the existing list, however this is the quick fix during refactoring
84 private ArrayList<PetriNetObject> petriNetObjects = new ArrayList<PetriNetObject>();85 private final ArrayList<PetriNetObject> petriNetObjects = new ArrayList<PetriNetObject>();
8586
86 public ArrayList<PetriNetObject> getPNObjects() {87 public ArrayList<PetriNetObject> getPNObjects() {
87 return petriNetObjects;88 return petriNetObjects;
@@ -101,16 +102,8 @@
101 * Create empty Petri-Net object102 * Create empty Petri-Net object
102 */103 */
103 public DataLayer() {104 public DataLayer() {
104 placesArray = new ArrayList<Place>();105 super();
105 transitionsArray = new ArrayList<Transition>();106 }
106 arcsArray = new ArrayList<Arc>();
107
108 labelsArray = new ArrayList<AnnotationNote>();
109
110 // may as well do the hashtable here as well
111 arcsMap = new Hashtable<PlaceTransitionObject, ArrayList<TimedOutputArcComponent>>();
112 tapnInhibitorsMap = new Hashtable<PlaceTransitionObject, ArrayList<TimedInhibitorArcComponent>>();
113 }
114107
115108
116 /**109 /**
@@ -162,105 +155,94 @@
162155
163 // Check if the arcs have a valid source and target156 // Check if the arcs have a valid source and target
164 if (arcInput.getSource() == null || arcInput.getTarget() == null) {157 if (arcInput.getSource() == null || arcInput.getTarget() == null) {
165 System.err.println(("Cant add arc" + arcInput + " where source: "158 System.err.println(
159 "Cant add arc" + arcInput + " where source: "
166 + arcInput.getSource() + " or target: "160 + arcInput.getSource() + " or target: "
167 + arcInput.getTarget() + " is null"));161 + arcInput.getTarget() + " is null"
162 );
168 return;163 return;
169 }164 }
170165
171 if (arcInput != null) {166 if (arcInput.getId() != null && arcInput.getId().length() > 0) {
172 if (arcInput.getId() != null && arcInput.getId().length() > 0) {167 for (Arc arc : arcsArray) {
173 for (int i = 0; i < arcsArray.size(); i++) {168 if (arcInput.getId().equals(arc.getId())) {
174 if (arcInput.getId().equals((arcsArray.get(i)).getId())) {169 unique = false;
175 unique = false;170 }
176 }171 }
177 }172 } else {
178 } else {173 String id = null;
179 String id = null;174 if (arcsArray.size() > 0) {
180 if (arcsArray != null && arcsArray.size() > 0) {175 int no = arcsArray.size();
181 int no = arcsArray.size();176 do {
182 do {177 for (Arc arc : arcsArray) {
183 for (int i = 0; i < arcsArray.size(); i++) {178 id = "A" + no;
184 id = "A" + no;179 if (arc != null) {
185 if (arcsArray.get(i) != null) {180 if (id.equals(arc.getId())) {
186 if (id.equals((arcsArray.get(i)).getId())) {181 unique = false;
187 unique = false;182 no++;
188 no++;183 } else {
189 } else {184 unique = true;
190 unique = true;185 }
191 }186 }
192 }187 }
193 }188 } while (!unique);
194 } while (!unique);189 } else {
195 } else {190 id = "A0";
196 id = "A0";191 }
197 }192 arcInput.setId(id);
198 if (id != null) {193 }
199 arcInput.setId(id);194
200 } else {195 //XXX: this is still nedede as nets loaded from file (XML/tapn) does not set connectedTo correctly //2019-09-18
201 arcInput.setId("error");196 // Transportarc fix boddy
202 }197 if (arcInput instanceof TimedTransportArcComponent) {
203 }198 TimedTransportArcComponent tmp = (TimedTransportArcComponent) arcInput;
204199 PlaceTransitionObject first = tmp.getSource();
205 //XXX: this is still nedede as nets loaded from file (XML/tapn) does not set connectedTo correctly //2019-09-18200
206 // Transportarc fix boddy201 if (tmp.getConnectedTo() == null) {
207 if (arcInput instanceof TimedTransportArcComponent) {202 if (first instanceof TimedPlaceComponent) {
208 TimedTransportArcComponent tmp = (TimedTransportArcComponent) arcInput;203
209 PlaceTransitionObject first = tmp.getSource();204 for (Object o : tmp.getTarget().getPostset()) {
210205
211 if (tmp.getConnectedTo() == null) {206 if (o instanceof TimedTransportArcComponent) {
212 if (first instanceof TimedPlaceComponent) {207 if (tmp.getGroupNr() == ((TimedTransportArcComponent) o).getGroupNr()) {
213208 // Found partner
214 for (Object o : tmp.getTarget().getPostset()) {209
215210 tmp.setConnectedTo(((TimedTransportArcComponent) o));
216 if (o instanceof TimedTransportArcComponent) {211 ((TimedTransportArcComponent) o).setConnectedTo(tmp);
217 if (tmp.getGroupNr() == ((TimedTransportArcComponent) o)212
218 .getGroupNr()) {213 break;
219 // Found partner214 }
220215 }
221 tmp216
222 .setConnectedTo(((TimedTransportArcComponent) o));217 }
223 ((TimedTransportArcComponent) o)218
224 .setConnectedTo(tmp);219 } else {
225220 // First is TimedTransition
226 break;221
227 }222 for (Object o : tmp.getSource().getPreset()) {
228 }223
229224 if (o instanceof TimedTransportArcComponent) {
230 }225 if (tmp.getGroupNr() == ((TimedTransportArcComponent) o).getGroupNr()) {
231226 // Found partner
232 } else {227
233 // First is TimedTransition228 tmp.setConnectedTo(((TimedTransportArcComponent) o));
234 tmp = (TimedTransportArcComponent) arcInput;229 ((TimedTransportArcComponent) o).setConnectedTo(tmp);
235230
236 for (Object o : tmp.getSource().getPreset()) {231 break;
237232 }
238 if (o instanceof TimedTransportArcComponent) {233 }
239 if (tmp.getGroupNr() == ((TimedTransportArcComponent) o)234
240 .getGroupNr()) {235 }
241 // Found partner236
242237 }
243 tmp238 }
244 .setConnectedTo(((TimedTransportArcComponent) o));239
245 ((TimedTransportArcComponent) o)240 }
246 .setConnectedTo(tmp);241
247242 arcsArray.add(arcInput);
248 break;243 addArcToArcsMap(arcInput);
249 }244
250 }245 }
251
252 }
253
254 }
255 }
256
257 }
258
259 arcsArray.add(arcInput);
260 addArcToArcsMap(arcInput);
261
262 }
263 }
264246
265 private void addTransportArc(TimedTransportArcComponent transportArc) {247 private void addTransportArc(TimedTransportArcComponent transportArc) {
266 arcsArray.add(transportArc);248 arcsArray.add(transportArc);
@@ -271,40 +253,34 @@
271 boolean unique = true;253 boolean unique = true;
272254
273 if (inhibitorArcInput != null) {255 if (inhibitorArcInput != null) {
274 if (inhibitorArcInput.getId() != null256 if (inhibitorArcInput.getId() != null && inhibitorArcInput.getId().length() > 0) {
275 && inhibitorArcInput.getId().length() > 0) {257 for (Arc arc : arcsArray) {
276 for (int i = 0; i < arcsArray.size(); i++) {258 if (inhibitorArcInput.getId().equals(arc.getId())) {
277 if (inhibitorArcInput.getId().equals(259 unique = false;
278 (arcsArray.get(i)).getId())) {260 }
279 unique = false;261 }
280 }
281 }
282 } else {262 } else {
283 String id = null;263 String id = null;
284 if (arcsArray != null && arcsArray.size() > 0) {264 if (arcsArray.size() > 0) {
285 int no = arcsArray.size();265 int no = arcsArray.size();
286 do {266 do {
287 for (int i = 0; i < arcsArray.size(); i++) {267 for (Arc arc : arcsArray) {
288 id = "I" + no;268 id = "I" + no;
289 if (arcsArray.get(i) != null) {269 if (arc != null) {
290 if (id.equals((arcsArray.get(i)).getId())) {270 if (id.equals(arc.getId())) {
291 unique = false;271 unique = false;
292 no++;272 no++;
293 } else {273 } else {
294 unique = true;274 unique = true;
295 }275 }
296 }276 }
297 }277 }
298 } while (!unique);278 } while (!unique);
299 } else {279 } else {
300 id = "I0";280 id = "I0";
301 }281 }
302 if (id != null) {282 inhibitorArcInput.setId(id);
303 inhibitorArcInput.setId(id);283 }
304 } else {
305 inhibitorArcInput.setId("error");
306 }
307 }
308284
309 arcsArray.add(inhibitorArcInput);285 arcsArray.add(inhibitorArcInput);
310 addInhibitorArcToInhibitorsMap(inhibitorArcInput);286 addInhibitorArcToInhibitorsMap(inhibitorArcInput);
@@ -529,18 +505,13 @@
529 attached = ((Arc) pnObject).getTarget();505 attached = ((Arc) pnObject).getTarget();
530506
531 if (attached != null) {507 if (attached != null) {
532 if (tapnInhibitorsMap.get(attached) != null) { // causing508 if (tapnInhibitorsMap.get(attached) != null) { // causing null pointer exceptions (!)
533 // null
534 // pointer
535 // exceptions
536 // (!)
537 tapnInhibitorsMap.get(attached).remove(pnObject);509 tapnInhibitorsMap.get(attached).remove(pnObject);
538 }510 }
539511
540 attached.removeToArc((Arc) pnObject);512 attached.removeToArc((Arc) pnObject);
541 if (attached instanceof Transition) {513 if (attached instanceof Transition) {
542 ((Transition) attached)514 ((Transition) attached).removeArcCompareObject((Arc) pnObject);
543 .removeArcCompareObject((Arc) pnObject);
544 }515 }
545 // attached.updateConnected(); //causing null pointer516 // attached.updateConnected(); //causing null pointer
546 // exceptions (?)517 // exceptions (?)
@@ -567,10 +538,7 @@
567538
568 attached = ((Arc) pnObject).getTarget();539 attached = ((Arc) pnObject).getTarget();
569 if (attached != null) {540 if (attached != null) {
570 if (arcsMap.get(attached) != null) { // causing null541 if (arcsMap.get(attached) != null) { // causing null pointer exceptions (!)
571 // pointer
572 // exceptions
573 // (!)
574 arcsMap.get(attached).remove(pnObject);542 arcsMap.get(attached).remove(pnObject);
575 }543 }
576544
@@ -586,8 +554,7 @@
586554
587 }555 }
588 } catch (NullPointerException npe) {556 } catch (NullPointerException npe) {
589 System.out.println("NullPointerException [debug]\n"557 System.out.println("NullPointerException [debug]\n" + npe.getMessage());
590 + npe.getMessage());
591 throw npe;558 throw npe;
592 }559 }
593 // we reset to null so that the wrong ArrayList can't get added to560 // we reset to null so that the wrong ArrayList can't get added to
@@ -599,8 +566,10 @@
599 * set all enabled transitions to highlighted566 * set all enabled transitions to highlighted
600 */567 */
601 public Iterable<Transition> transitions() {568 public Iterable<Transition> transitions() {
602 return transitionsArray;569
603 }570 return transitionsArray;
571 }
572
604573
605 /**574 /**
606 * Sets an internal ArrayList according to the class of the object passed575 * Sets an internal ArrayList according to the class of the object passed
@@ -735,16 +704,14 @@
735 public Transition getTransitionById(String transitionID) {704 public Transition getTransitionById(String transitionID) {
736 Transition returnTransition = null;705 Transition returnTransition = null;
737706
738 if (transitionsArray != null) {707 if (transitionID != null) {
739 if (transitionID != null) {708 for (Transition transition : transitionsArray) {
740 for (Transition transition : transitionsArray) {709 if (transitionID.equalsIgnoreCase(transition.getId())) {
741 if (transitionID.equalsIgnoreCase(transition.getId())) {710 returnTransition = transition;
742 returnTransition = transition;711 }
743 }712 }
744 }713 }
745 }714 return returnTransition;
746 }
747 return returnTransition;
748 }715 }
749716
750 /**717 /**
@@ -758,16 +725,14 @@
758 public Transition getTransitionByName(String transitionName) {725 public Transition getTransitionByName(String transitionName) {
759 Transition returnTransition = null;726 Transition returnTransition = null;
760727
761 if (transitionsArray != null) {728 if (transitionName != null) {
762 if (transitionName != null) {729 for (Transition transition : transitionsArray) {
763 for (Transition transition : transitionsArray) {730 if (transitionName.equalsIgnoreCase(transition.getName())) {
764 if (transitionName.equalsIgnoreCase(transition.getName())) {731 returnTransition = transition;
765 returnTransition = transition;732 }
766 }733 }
767 }734 }
768 }735 return returnTransition;
769 }
770 return returnTransition;
771 }736 }
772737
773 /**738 /**
@@ -780,16 +745,14 @@
780 public Place getPlaceById(String placeID) {745 public Place getPlaceById(String placeID) {
781 Place returnPlace = null;746 Place returnPlace = null;
782747
783 if (placesArray != null) {748 if (placeID != null) {
784 if (placeID != null) {749 for (Place place : placesArray) {
785 for (Place place : placesArray) {750 if (placeID.equalsIgnoreCase(place.getId())) {
786 if (placeID.equalsIgnoreCase(place.getId())) {751 returnPlace = place;
787 returnPlace = place;752 }
788 }753 }
789 }754 }
790 }755 return returnPlace;
791 }
792 return returnPlace;
793 }756 }
794757
795 /**758 /**
@@ -802,16 +765,14 @@
802 public Place getPlaceByName(String placeName) {765 public Place getPlaceByName(String placeName) {
803 Place returnPlace = null;766 Place returnPlace = null;
804767
805 if (placesArray != null) {768 if (placeName != null) {
806 if (placeName != null) {769 for (Place place : placesArray) {
807 for (Place place : placesArray) {770 if (placeName.equalsIgnoreCase(place.getName())) {
808 if (placeName.equalsIgnoreCase(place.getName())) {771 returnPlace = place;
809 returnPlace = place;772 }
810 }773 }
811 }774 }
812 }775 return returnPlace;
813 }
814 return returnPlace;
815 }776 }
816777
817 /**778 /**
818779
=== modified file 'src/pipe/dataLayer/Template.java'
--- src/pipe/dataLayer/Template.java 2020-01-12 10:11:08 +0000
+++ src/pipe/dataLayer/Template.java 2020-07-09 12:55:48 +0000
@@ -5,9 +5,9 @@
5import dk.aau.cs.util.Require;5import dk.aau.cs.util.Require;
66
7public class Template {7public class Template {
8 private TimedArcPetriNet net;8 private final TimedArcPetriNet net;
9 private DataLayer guiModel;9 private final DataLayer guiModel;
10 private Zoomer zoomer;10 private final Zoomer zoomer;
11 private boolean hasPositionalInfo = false;11 private boolean hasPositionalInfo = false;
12 12
13 public Template(TimedArcPetriNet net, DataLayer guiModel, Zoomer zoomer) {13 public Template(TimedArcPetriNet net, DataLayer guiModel, Zoomer zoomer) {
@@ -37,11 +37,6 @@
37 net.setActive(isActive);37 net.setActive(isActive);
38 }38 }
3939
40 public void setGuiModel(DataLayer guiModel) {
41 Require.notNull(guiModel, "GuiModel cannot be null");
42 this.guiModel = guiModel;
43 }
44
45 public Template copy() {40 public Template copy() {
46 TimedArcPetriNet tapn = net.copy();41 TimedArcPetriNet tapn = net.copy();
47 tapn.setName(tapn.name() + "Copy");42 tapn.setName(tapn.name() + "Copy");
4843
=== modified file 'src/pipe/gui/AnimationHistoryList.java'
--- src/pipe/gui/AnimationHistoryList.java 2020-05-18 11:23:28 +0000
+++ src/pipe/gui/AnimationHistoryList.java 2020-07-09 12:55:48 +0000
@@ -152,7 +152,7 @@
152 }152 }
153 for (Template t : CreateGui.getCurrentTab().activeTemplates()){153 for (Template t : CreateGui.getCurrentTab().activeTemplates()){
154 for(Transition trans : t.guiModel().getTransitions()){154 for(Transition trans : t.guiModel().getTransitions()){
155 if(trans.isEnabled(true) || trans.isDelayEnabledTransition(true)){155 if(trans.isTransitionEnabled() || trans.isDelayEnabled()){
156 return;156 return;
157 }157 }
158 }158 }
159159
=== modified file 'src/pipe/gui/Animator.java'
--- src/pipe/gui/Animator.java 2020-05-25 07:16:04 +0000
+++ src/pipe/gui/Animator.java 2020-07-09 12:55:48 +0000
@@ -39,659 +39,648 @@
39import dk.aau.cs.verification.VerifyTAPN.TraceType;39import dk.aau.cs.verification.VerifyTAPN.TraceType;
4040
41public class Animator {41public class Animator {
42 private final ArrayList<TAPNNetworkTraceStep> actionHistory = new ArrayList<TAPNNetworkTraceStep>();42 private final ArrayList<TAPNNetworkTraceStep> actionHistory = new ArrayList<TAPNNetworkTraceStep>();
43 private int currentAction;43 private int currentAction = -1;
44 private final ArrayList<NetworkMarking> markings = new ArrayList<NetworkMarking>();44 private final ArrayList<NetworkMarking> markings = new ArrayList<NetworkMarking>();
45 private int currentMarkingIndex = 0;45 private int currentMarkingIndex = 0;
46 private TAPNNetworkTrace trace = null;46 private TAPNNetworkTrace trace = null;
4747
48 public FiringMode firingmode = new RandomFiringMode();48 public FiringMode firingmode = new RandomFiringMode();
49 private TabContent tab;49 private final TabContent tab;
50 private NetworkMarking initialMarking;50 private NetworkMarking initialMarking;
5151
52 private boolean isDisplayingUntimedTrace = false;52 private boolean isDisplayingUntimedTrace = false;
53 private static boolean isUrgentTransitionEnabled = false;53 private static boolean isUrgentTransitionEnabled = false;
54 54
55 public static boolean isUrgentTransitionEnabled(){55 public static boolean isUrgentTransitionEnabled(){
56 return isUrgentTransitionEnabled;56 return isUrgentTransitionEnabled;
57 }57 }
5858
59 public Animator(TabContent tab) {59 public Animator(TabContent tab) {
60 currentAction = -1;60 super();
61 setTabContent(tab);61
62 }62 this.tab = tab;
6363 }
64 private void setTabContent(TabContent tab) {64
65 this.tab = tab;65 private NetworkMarking currentMarking() {
66 }66 return markings.get(currentMarkingIndex);
6767 }
68 private NetworkMarking currentMarking() {68
69 return markings.get(currentMarkingIndex);69 public void setTrace(TAPNNetworkTrace trace) {
70 }
71
72 public void setTrace(TAPNNetworkTrace trace) {
73 CreateGui.getCurrentTab().setAnimationMode(true);70 CreateGui.getCurrentTab().setAnimationMode(true);
7471
75 if (trace.isConcreteTrace()) {72 if (trace.isConcreteTrace()) {
76 this.trace = trace;73 this.trace = trace;
77 setTimedTrace(trace);74 setTimedTrace(trace);
78 } else {75 } else {
79 setUntimedTrace(trace);76 setUntimedTrace(trace);
80 isDisplayingUntimedTrace = true;77 isDisplayingUntimedTrace = true;
81 }78 }
82 currentAction = -1;79 currentAction = -1;
83 currentMarkingIndex = 0;80 currentMarkingIndex = 0;
84 tab.network().setMarking(markings.get(currentMarkingIndex));81 tab.network().setMarking(markings.get(currentMarkingIndex));
85 tab.getAnimationHistorySidePanel().setSelectedIndex(0);82 tab.getAnimationHistorySidePanel().setSelectedIndex(0);
86 updateAnimationButtonsEnabled();83 updateAnimationButtonsEnabled();
87 updateFireableTransitions();84 updateFireableTransitions();
88 }85 }
8986
90 private void setUntimedTrace(TAPNNetworkTrace trace) {87 private void setUntimedTrace(TAPNNetworkTrace trace) {
91 tab.addAbstractAnimationPane();88 tab.addAbstractAnimationPane();
92 AnimationHistoryList untimedAnimationHistory = tab.getUntimedAnimationHistory();89 AnimationHistoryList untimedAnimationHistory = tab.getUntimedAnimationHistory();
9390
94 for(TAPNNetworkTraceStep step : trace){91 for(TAPNNetworkTraceStep step : trace){
95 untimedAnimationHistory.addHistoryItem(step.toString());92 untimedAnimationHistory.addHistoryItem(step.toString());
96 }93 }
9794
98 tab.getUntimedAnimationHistory().setSelectedIndex(0);95 tab.getUntimedAnimationHistory().setSelectedIndex(0);
99 setFiringmode("Random");96 setFiringmode("Random");
10097
101 JOptionPane.showMessageDialog(CreateGui.getApp(),98 JOptionPane.showMessageDialog(CreateGui.getApp(),
102 "The verification process returned an untimed trace.\n\n"99 "The verification process returned an untimed trace.\n\n"
103 + "This means that with appropriate time delays the displayed\n"100 + "This means that with appropriate time delays the displayed\n"
104 + "sequence of discrete transitions can become a concrete trace.\n"101 + "sequence of discrete transitions can become a concrete trace.\n"
105 + "In case of liveness properties (EG, AF) the untimed trace\n"102 + "In case of liveness properties (EG, AF) the untimed trace\n"
106 + "either ends in a deadlock, a time divergent computation without\n"103 + "either ends in a deadlock, a time divergent computation without\n"
107 + "any discrete transitions, or it loops back to some earlier configuration.\n"104 + "any discrete transitions, or it loops back to some earlier configuration.\n"
108 + "The user may experiment in the simulator with different time delays\n"105 + "The user may experiment in the simulator with different time delays\n"
109 + "in order to realize the suggested untimed trace in the model.",106 + "in order to realize the suggested untimed trace in the model.",
110 "Verification Information", JOptionPane.INFORMATION_MESSAGE);107 "Verification Information", JOptionPane.INFORMATION_MESSAGE);
111 }108 }
112109
113 private void setTimedTrace(TAPNNetworkTrace trace) {110 private void setTimedTrace(TAPNNetworkTrace trace) {
114 for (TAPNNetworkTraceStep step : trace) {111 for (TAPNNetworkTraceStep step : trace) {
115 addMarking(step, step.performStepFrom(currentMarking()));112 addMarking(step, step.performStepFrom(currentMarking()));
116 }113 }
117 if(getTrace().getTraceType() != TraceType.NOT_EG){ //If the trace was not explicitly set, maybe we have calculated it is deadlock.114 if(getTrace().getTraceType() != TraceType.NOT_EG){ //If the trace was not explicitly set, maybe we have calculated it is deadlock.
118 tab.getAnimationHistorySidePanel().setLastShown(getTrace().getTraceType());115 tab.getAnimationHistorySidePanel().setLastShown(getTrace().getTraceType());
119 }116 }
120 }117 }
121118
122 private void addToTimedTrace(List<TAPNNetworkTraceStep> stepList){119 private void addToTimedTrace(List<TAPNNetworkTraceStep> stepList){
123 for (TAPNNetworkTraceStep step : stepList) {120 for (TAPNNetworkTraceStep step : stepList) {
124 addMarking(step, step.performStepFrom(currentMarking()));121 addMarking(step, step.performStepFrom(currentMarking()));
125 }122 }
126 }123 }
127124
128 public NetworkMarking getInitialMarking(){125 public NetworkMarking getInitialMarking(){
129 return initialMarking;126 return initialMarking;
130 }127 }
131 128
132 /**129 /**
133 * Highlights enabled transitions130 * Highlights enabled transitions
134 */131 */
135 public void highlightEnabledTransitions() {132 public void highlightEnabledTransitions() {
136 updateFireableTransitions();133 updateFireableTransitions();
137 DataLayer current = activeGuiModel();134 }
138135
139 for (Transition tempTransition : current.transitions()) {136 /**
140 if (tempTransition.isEnabled(true) || (tempTransition.isDelayEnabledTransition(true) && !isUrgentTransitionEnabled)) {137 * Called during animation to unhighlight previously highlighted transitions
141 tempTransition.repaint();138 */
142 }139 private void unhighlightDisabledTransitions() {
143 }140 disableTransitions();
144 }141 }
145142
146 /**143 public void updateFireableTransitions(){
147 * Called during animation to unhighlight previously highlighted transitions144 TransitionFireingComponent transFireComponent = tab.getTransitionFireingComponent();
148 */145 transFireComponent.startReInit();
149 private void unhighlightDisabledTransitions() {146 isUrgentTransitionEnabled = false;
150 DataLayer current = activeGuiModel();147
151148 outer: for( Template template : tab.activeTemplates()){
152 for (Transition t : current.transitions()) {149 for (TimedTransition t : template.model().transitions()) {
153 if (!(t.isEnabled(true)) || !t.isDelayEnabledTransition(true) || (t.isDelayEnabledTransition(true) && isUrgentTransitionEnabled)) {150 if (t.isUrgent() && t.isEnabled()) {
154 t.repaint();
155 }
156 }
157 }
158
159 public void updateFireableTransitions(){
160 TransitionFireingComponent transFireComponent = tab.getTransitionFireingComponent();
161 transFireComponent.startReInit();
162 isUrgentTransitionEnabled = false;
163
164 outer: for( Template temp : tab.activeTemplates()){
165 for (Transition tempTransition : temp.guiModel().transitions()) {
166 if (tempTransition.isEnabled(true) && temp.model().getTransitionByName(tempTransition.getName()).isUrgent()) {
167 isUrgentTransitionEnabled = true;151 isUrgentTransitionEnabled = true;
168 break outer;152 break outer;
169 }153 }
170 }154 }
171 }155 }
172 156
173 for( Template temp : tab.activeTemplates()){157 for( Template template : tab.activeTemplates()){
174 for (Transition tempTransition : temp.guiModel().transitions()) {158 for (Transition t : template.guiModel().transitions()) {
175 if (tempTransition.isEnabled(true) || (tempTransition.isDelayEnabledTransition(true) && CreateGui.getApp().isShowingDelayEnabledTransitions() && !isUrgentTransitionEnabled)) {159 if (t.isTransitionEnabled()) {
176 transFireComponent.addTransition(temp, tempTransition);160 t.markTransitionEnabled(true);
161 transFireComponent.addTransition(template, t);
162 } else if (CreateGui.getApp().isShowingDelayEnabledTransitions() &&
163 t.isDelayEnabled() && !isUrgentTransitionEnabled
164 ) {
165 t.markTransitionDelayEnabled(true);
166 transFireComponent.addTransition(template, t);
177 }167 }
168
178 }169 }
179 }170 }
180171
181 transFireComponent.reInitDone();172 transFireComponent.reInitDone();
182 }173 }
183174
184 /**175 /**
185 * Called at end of animation and resets all Transitions to false and176 * Called at end of animation and resets all Transitions to false and
186 * unhighlighted177 * unhighlighted
187 */178 */
188 private void disableTransitions() {179 private void disableTransitions() {
189 for(Template template : tab.allTemplates())180 for(Template template : tab.allTemplates())
190 {181 {
191 for (Transition tempTransition : template.guiModel().transitions()) {182 for (Transition tempTransition : template.guiModel().transitions()) {
192 tempTransition.setEnabledFalse();183 tempTransition.disableHightligh();
193 tempTransition.setDelayEnabledTransitionFalse();184
194 tempTransition.repaint();185 tempTransition.repaint();
195 }186 }
196 }187 }
197 }188 }
198189
199 /**190 /**
200 * Stores model at start of animation191 * Stores model at start of animation
201 */192 */
202 public void storeModel() {193 public void storeModel() {
203 initialMarking = tab.network().marking();194 initialMarking = tab.network().marking();
204 resethistory();195 resethistory();
205 markings.add(initialMarking);196 markings.add(initialMarking);
206 }197 }
207198
208 /**199 /**
209 * Restores model at end of animation and sets all transitions to false and200 * Restores model at end of animation and sets all transitions to false and
210 * unhighlighted201 * unhighlighted
211 */202 */
212 public void restoreModel() {203 public void restoreModel() {
213 if (tab != null) {204 if (tab != null) {
214 disableTransitions();205 disableTransitions();
215 if (initialMarking != null) {206 tab.network().setMarking(initialMarking);
216 tab.network().setMarking(initialMarking);207 currentAction = -1;
217 }208 }
218 currentAction = -1;209 }
219 }210
220 }211 /**
221212 * Steps back through previously fired transitions
222 /**213 *
223 * Steps back through previously fired transitions214 * @author jokke refactored and added backwards firing for TAPNTransitions
224 * 215 */
225 * @author jokke refactored and added backwards firing for TAPNTransitions216
226 */217 public void stepBack() {
227
228 public void stepBack() {
229 tab.getAnimationHistorySidePanel().stepBackwards();218 tab.getAnimationHistorySidePanel().stepBackwards();
230 if (!actionHistory.isEmpty()){219 if (!actionHistory.isEmpty()){
231 TAPNNetworkTraceStep lastStep = actionHistory.get(currentAction);220 TAPNNetworkTraceStep lastStep = actionHistory.get(currentAction);
232 if(isDisplayingUntimedTrace && lastStep instanceof TAPNNetworkTimedTransitionStep){221 if(isDisplayingUntimedTrace && lastStep instanceof TAPNNetworkTimedTransitionStep){
233 AnimationHistoryList untimedAnimationHistory = tab.getUntimedAnimationHistory();222 AnimationHistoryList untimedAnimationHistory = tab.getUntimedAnimationHistory();
234 String previousInUntimedTrace = untimedAnimationHistory.getElement(untimedAnimationHistory.getSelectedIndex());223 String previousInUntimedTrace = untimedAnimationHistory.getElement(untimedAnimationHistory.getSelectedIndex());
235 if(previousInUntimedTrace.equals(lastStep.toString())){224 if(previousInUntimedTrace.equals(lastStep.toString())){
236 untimedAnimationHistory.stepBackwards();225 untimedAnimationHistory.stepBackwards();
237 }226 }
238 } 227 }
239 tab.network().setMarking(markings.get(currentMarkingIndex - 1));228 tab.network().setMarking(markings.get(currentMarkingIndex - 1));
240229
241 activeGuiModel().repaintPlaces();230 activeGuiModel().repaintPlaces();
242 unhighlightDisabledTransitions();231 unhighlightDisabledTransitions();
243 highlightEnabledTransitions();232 highlightEnabledTransitions();
244 currentAction--;233 currentAction--;
245 currentMarkingIndex--;234 currentMarkingIndex--;
246235
247 updateAnimationButtonsEnabled();236 updateAnimationButtonsEnabled();
248 updateMouseOverInformation();237 updateMouseOverInformation();
249 reportBlockingPlaces();238 reportBlockingPlaces();
250 }239 }
251 }240 }
252241
253 /**242 /**
254 * Steps forward through previously fired transitions243 * Steps forward through previously fired transitions
255 */244 */
256245
257 public void stepForward() {246 public void stepForward() {
258 tab.getAnimationHistorySidePanel().stepForward();247 tab.getAnimationHistorySidePanel().stepForward();
259 if(currentAction == actionHistory.size()-1 && trace != null){248 if(currentAction == actionHistory.size()-1 && trace != null){
260 int selectedIndex = tab.getAnimationHistorySidePanel().getSelectedIndex();249 int selectedIndex = tab.getAnimationHistorySidePanel().getSelectedIndex();
261 int action = currentAction;250 int action = currentAction;
262 int markingIndex = currentMarkingIndex;251 int markingIndex = currentMarkingIndex;
263252
264 if(getTrace().getTraceType() == TraceType.EG_DELAY_FOREVER){253 if(getTrace().getTraceType() == TraceType.EG_DELAY_FOREVER){
265 addMarking(new TAPNNetworkTimeDelayStep(BigDecimal.ONE), currentMarking().delay(BigDecimal.ONE));254 addMarking(new TAPNNetworkTimeDelayStep(BigDecimal.ONE), currentMarking().delay(BigDecimal.ONE));
266 }255 }
267 if(getTrace().getLoopToIndex() != -1){256 if(getTrace().getLoopToIndex() != -1){
268 addToTimedTrace(getTrace().getLoopSteps());257 addToTimedTrace(getTrace().getLoopSteps());
269 }258 }
270259
271 tab.getAnimationHistorySidePanel().setSelectedIndex(selectedIndex);260 tab.getAnimationHistorySidePanel().setSelectedIndex(selectedIndex);
272 currentAction = action;261 currentAction = action;
273 currentMarkingIndex = markingIndex;262 currentMarkingIndex = markingIndex;
274 }263 }
275264
276 if (currentAction < actionHistory.size() - 1) {265 if (currentAction < actionHistory.size() - 1) {
277 TAPNNetworkTraceStep nextStep = actionHistory.get(currentAction+1);266 TAPNNetworkTraceStep nextStep = actionHistory.get(currentAction+1);
278 if(isDisplayingUntimedTrace && nextStep instanceof TAPNNetworkTimedTransitionStep){267 if(isDisplayingUntimedTrace && nextStep instanceof TAPNNetworkTimedTransitionStep){
279 AnimationHistoryList untimedAnimationHistory = tab.getUntimedAnimationHistory();268 AnimationHistoryList untimedAnimationHistory = tab.getUntimedAnimationHistory();
280 String nextInUntimedTrace = untimedAnimationHistory.getElement(untimedAnimationHistory.getSelectedIndex()+1);269 String nextInUntimedTrace = untimedAnimationHistory.getElement(untimedAnimationHistory.getSelectedIndex()+1);
281 if(nextInUntimedTrace.equals(nextStep.toString())){270 if(nextInUntimedTrace.equals(nextStep.toString())){
282 untimedAnimationHistory.stepForward();271 untimedAnimationHistory.stepForward();
283 }272 }
284 } 273 }
285 tab.network().setMarking(markings.get(currentMarkingIndex + 1));274 tab.network().setMarking(markings.get(currentMarkingIndex + 1));
286275
287 activeGuiModel().repaintPlaces();276 activeGuiModel().repaintPlaces();
288 unhighlightDisabledTransitions();277 unhighlightDisabledTransitions();
289 highlightEnabledTransitions();278 highlightEnabledTransitions();
290 currentAction++;279 currentAction++;
291 currentMarkingIndex++;280 currentMarkingIndex++;
292 activeGuiModel().redrawVisibleTokenLists();281 activeGuiModel().redrawVisibleTokenLists();
293282
294 updateAnimationButtonsEnabled();283 updateAnimationButtonsEnabled();
295 updateMouseOverInformation();284 updateMouseOverInformation();
296 reportBlockingPlaces();285 reportBlockingPlaces();
297286
298 }287 }
299 } 288 }
300 289
301 /**290 /**
302 * Make the selected transition in the animation box blink, based on the291 * Make the selected transition in the animation box blink, based on the
303 * list element label292 * list element label
304 */293 */
305 294
306 public void blinkSelected(String label){295 public void blinkSelected(String label){
307 if(label.contains(".")){296 if(label.contains(".")){
308 label = label.split("\\.")[1];297 label = label.split("\\.")[1];
309 }298 }
310 299
311 Transition t = activeGuiModel().getTransitionByName(label);300 Transition t = activeGuiModel().getTransitionByName(label);
312 if(t != null){301 if(t != null){
313 t.blink();302 t.blink();
314 }303 }
315 }304 }
316 305
317 public void dFireTransition(TimedTransition transition){306 public void dFireTransition(TimedTransition transition){
318 if(!CreateGui.getApp().isShowingDelayEnabledTransitions() || isUrgentTransitionEnabled()){307 if(!CreateGui.getApp().isShowingDelayEnabledTransitions() || isUrgentTransitionEnabled()){
319 fireTransition(transition);308 fireTransition(transition);
320 return;309 return;
321 }310 }
322 311
323 TimeInterval dInterval = transition.getdInterval();312 TimeInterval dInterval = transition.getdInterval();
324 313
325 BigDecimal delayGranularity = tab.getDelayEnabledTransitionControl().getValue();314 BigDecimal delayGranularity = tab.getDelayEnabledTransitionControl().getValue();
326 //Make sure the granularity is small enough315 //Make sure the granularity is small enough
327 BigDecimal lowerBound = IntervalOperations.getRatBound(dInterval.lowerBound()).getBound();316 BigDecimal lowerBound = IntervalOperations.getRatBound(dInterval.lowerBound()).getBound();
328 if(!dInterval.IsLowerBoundNonStrict() && !dInterval.isIncluded(lowerBound.add(delayGranularity))){317 if(!dInterval.IsLowerBoundNonStrict() && !dInterval.isIncluded(lowerBound.add(delayGranularity))){
329 do{318 do{
330 delayGranularity = delayGranularity.divide(BigDecimal.TEN);319 delayGranularity = delayGranularity.divide(BigDecimal.TEN);
331 } while (delayGranularity.compareTo(new BigDecimal("0.00001")) >= 0 && !dInterval.isIncluded(lowerBound.add(delayGranularity)));320 } while (delayGranularity.compareTo(new BigDecimal("0.00001")) >= 0 && !dInterval.isIncluded(lowerBound.add(delayGranularity)));
332 }321 }
333 322
334 if(delayGranularity.compareTo(new BigDecimal("0.00001")) < 0){323 if(delayGranularity.compareTo(new BigDecimal("0.00001")) < 0){
335 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>");324 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>");
336 } else {325 } else {
337 BigDecimal delay = tab.getDelayEnabledTransitionControl().getDelayMode().GetDelay(transition, dInterval, delayGranularity);326 BigDecimal delay = tab.getDelayEnabledTransitionControl().getDelayMode().GetDelay(transition, dInterval, delayGranularity);
338 if(delay != null){327 if(delay != null){
339 if(delay.compareTo(BigDecimal.ZERO) != 0){ //Don't delay if the chosen delay is 0328 if(delay.compareTo(BigDecimal.ZERO) != 0){ //Don't delay if the chosen delay is 0
340 if(!letTimePass(delay)){329 if(!letTimePass(delay)){
341 return;330 return;
342 }331 }
343 }332 }
344 333
345 fireTransition(transition);334 fireTransition(transition);
346335 }
347 }336 }
348 }337 }
349 }338
350339 // TODO: Clean up this method
351 // TODO: Clean up this method340 private void fireTransition(TimedTransition transition) {
352 private void fireTransition(TimedTransition transition) {341
353342 if(!clearStepsForward()){
354 if(!clearStepsForward()){343 return;
355 return;344 }
356 }345
357346 Tuple<NetworkMarking, List<TimedToken>> next = null;
358 Tuple<NetworkMarking, List<TimedToken>> next = null;347 List<TimedToken> tokensToConsume = null;
359 List<TimedToken> tokensToConsume = null;348 try{
360349 if (getFiringmode() != null) {
361 try{350 next = currentMarking().fireTransition(transition, getFiringmode());
362 if (getFiringmode() != null) {351 } else {
363 next = currentMarking().fireTransition(transition, getFiringmode());352 tokensToConsume = getTokensToConsume(transition);
364 } else {353 if(tokensToConsume == null) return; // Cancelled
365 tokensToConsume = getTokensToConsume(transition);354 next = new Tuple<NetworkMarking, List<TimedToken>> (currentMarking().fireTransition(transition, tokensToConsume), tokensToConsume);
366 if(tokensToConsume == null) return; // Cancelled355 }
367 next = new Tuple<NetworkMarking, List<TimedToken>> (currentMarking().fireTransition(transition, tokensToConsume), tokensToConsume);356 }catch(RequireException e){
368 }357 JOptionPane.showMessageDialog(CreateGui.getApp(), "There was an error firing the transition. Reason: " + e.getMessage(), "Error", JOptionPane.ERROR_MESSAGE);
369 }catch(RequireException e){358 return;
370 JOptionPane.showMessageDialog(CreateGui.getApp(), "There was an error firing the transition. Reason: " + e.getMessage(), "Error", JOptionPane.ERROR_MESSAGE);359 }
371 return;360
372 }361 // It is important that this comes after the above, since
373362 // cancelling the token selection dialogue above should not result in changes
374 // It is important that this comes after the above, since 363 // to the untimed animation history
375 // cancelling the token selection dialogue above should not result in changes 364 if (isDisplayingUntimedTrace){
376 // to the untimed animation history365 AnimationHistoryList untimedAnimationHistory = tab.getUntimedAnimationHistory();
377 if (isDisplayingUntimedTrace){366 if(untimedAnimationHistory.isStepForwardAllowed()){
378 AnimationHistoryList untimedAnimationHistory = tab.getUntimedAnimationHistory();367 String nextFromUntimedTrace = untimedAnimationHistory.getElement(untimedAnimationHistory.getSelectedIndex()+1);
379 if(untimedAnimationHistory.isStepForwardAllowed()){368
380 String nextFromUntimedTrace = untimedAnimationHistory.getElement(untimedAnimationHistory.getSelectedIndex()+1);369 if(nextFromUntimedTrace.equals(transition.model().name() + "." + transition.name()) || transition.isShared() && nextFromUntimedTrace.equals(transition.name())){
381370 untimedAnimationHistory.stepForward();
382 if(nextFromUntimedTrace.equals(transition.model().name() + "." + transition.name()) || transition.isShared() && nextFromUntimedTrace.equals(transition.name())){371 }else{
383 untimedAnimationHistory.stepForward();372 int fireTransition = JOptionPane.showConfirmDialog(CreateGui.getApp(),
384 }else{373 "Are you sure you want to fire a transition which does not follow the untimed trace?\n"
385 int fireTransition = JOptionPane.showConfirmDialog(CreateGui.getApp(),374 + "Firing this transition will discard the untimed trace and revert to standard simulation.",
386 "Are you sure you want to fire a transition which does not follow the untimed trace?\n"375 "Discrading Untimed Trace", JOptionPane.YES_NO_OPTION );
387 + "Firing this transition will discard the untimed trace and revert to standard simulation.",376
388 "Discrading Untimed Trace", JOptionPane.YES_NO_OPTION );377 if (fireTransition == JOptionPane.NO_OPTION){
389378 return;
390 if (fireTransition == JOptionPane.NO_OPTION){379 }else{
391 return;380 removeSetTrace(false);
392 }else{381 }
393 removeSetTrace(false);382 }
394 }383 }
395 }384 }
396 }385
397 }386 tab.network().setMarking(next.value1());
398387
399 tab.network().setMarking(next.value1());388 activeGuiModel().repaintPlaces();
400 389 unhighlightDisabledTransitions();
401 activeGuiModel().repaintPlaces();390 highlightEnabledTransitions();
402 highlightEnabledTransitions();391
403 unhighlightDisabledTransitions();392 addMarking(new TAPNNetworkTimedTransitionStep(transition, next.value2()), next.value1());
404 addMarking(new TAPNNetworkTimedTransitionStep(transition, next.value2()), next.value1());393
405394 updateAnimationButtonsEnabled();
406 updateAnimationButtonsEnabled();395 updateMouseOverInformation();
407 updateMouseOverInformation();396 reportBlockingPlaces();
408 reportBlockingPlaces();397
409398 }
410 }399
411400 public boolean letTimePass(BigDecimal delay) {
412 public boolean letTimePass(BigDecimal delay) {401
413402 if(!clearStepsForward()){
414 if(!clearStepsForward()){403 return false;
415 return false;404 }
416 }405
417406 boolean result = false;
418 boolean result = false;407 if (delay.compareTo(new BigDecimal(0))==0 || (currentMarking().isDelayPossible(delay) && !isUrgentTransitionEnabled)) {
419 if (delay.compareTo(new BigDecimal(0))==0 || (currentMarking().isDelayPossible(delay) && !isUrgentTransitionEnabled)) {408 NetworkMarking delayedMarking = currentMarking().delay(delay);
420 NetworkMarking delayedMarking = currentMarking().delay(delay);409 tab.network().setMarking(delayedMarking);
421 tab.network().setMarking(delayedMarking);410 addMarking(new TAPNNetworkTimeDelayStep(delay), delayedMarking);
422 addMarking(new TAPNNetworkTimeDelayStep(delay), delayedMarking);411 result = true;
423 result = true;412 }
424 }413
425414 activeGuiModel().repaintPlaces();
426 activeGuiModel().repaintPlaces();415 unhighlightDisabledTransitions();
427 highlightEnabledTransitions();416 highlightEnabledTransitions();
428 unhighlightDisabledTransitions();417
429418 updateAnimationButtonsEnabled();
430 updateAnimationButtonsEnabled();419 updateMouseOverInformation();
431 updateMouseOverInformation();420 reportBlockingPlaces();
432 reportBlockingPlaces();421 return result;
433422 }
434 return result;423
435 }424 public void reportBlockingPlaces() {
436425
437 public void reportBlockingPlaces(){426 try {
438427 BigDecimal delay = tab.getAnimationController().getCurrentDelay();
439 try{428
440 BigDecimal delay = tab.getAnimationController().getCurrentDelay();429 if (isUrgentTransitionEnabled && !delay.equals(BigDecimal.ZERO) ) {
441 if(isUrgentTransitionEnabled && delay.compareTo(new BigDecimal(0))>0){430 tab.getAnimationController().getOkButton().setEnabled(false);
442 tab.getAnimationController().getOkButton().setEnabled(false);431
443 StringBuilder sb = new StringBuilder();432 StringBuilder sb = new StringBuilder();
444 sb.append("<html>Time delay is disabled due to the<br /> following enabled urgent transitions:<br /><br />");433 sb.append("<html>Time delay is disabled due to the<br /> following enabled urgent transitions:<br /><br />");
445 for( Template temp : tab.activeTemplates()){434 for (Template template : tab.activeTemplates()) {
446 for (Transition tempTransition : temp.guiModel().transitions()) {435 for (Transition t : template.guiModel().transitions()) {
447 if (tempTransition.isEnabled(true) && temp.model().getTransitionByName(tempTransition.getName()).isUrgent()) {436 if (t.isTransitionEnabled() && template.model().getTransitionByName(t.getName()).isUrgent()) {
448 sb.append(temp.toString() + "." + tempTransition.getName() + "<br />");437 sb.append(template.toString() + "." + t.getName() + "<br />");
449 }438 }
450 }439 }
451 }440 }
452 sb.append("</html>");441 sb.append("</html>");
453 tab.getAnimationController().getOkButton().setToolTipText(sb.toString());442
454 return;443 tab.getAnimationController().getOkButton().setToolTipText(sb.toString());
455 }444
456 if(delay.compareTo(new BigDecimal(0))<0){445 return;
457 tab.getAnimationController().getOkButton().setEnabled(false);446 }
458 tab.getAnimationController().getOkButton().setToolTipText("Time delay is possible only for nonnegative rational numbers");447
459 } else {448 if (delay.compareTo(new BigDecimal(0)) < 0) {
460 List<TimedPlace> blockingPlaces = currentMarking().getBlockingPlaces(delay);449 tab.getAnimationController().getOkButton().setEnabled(false);
461 if(blockingPlaces.size() == 0){450 tab.getAnimationController().getOkButton().setToolTipText("Time delay is possible only for nonnegative rational numbers");
462 tab.getAnimationController().getOkButton().setEnabled(true);451 } else {
463 tab.getAnimationController().getOkButton().setToolTipText("Press to add the delay");452 List<TimedPlace> blockingPlaces = currentMarking().getBlockingPlaces(delay);
464 } else {453 if (blockingPlaces.size() == 0) {
465 StringBuilder sb = new StringBuilder();454 tab.getAnimationController().getOkButton().setEnabled(true);
466 sb.append("<html>Time delay of " + delay + " time unit(s) is disabled due to <br /> age invariants in the following places:<br /><br />");455 tab.getAnimationController().getOkButton().setToolTipText("Press to add the delay");
467 for (TimedPlace t :blockingPlaces){456 } else {
468 sb.append(t.toString() + "<br />");457 StringBuilder sb = new StringBuilder();
469 }458 sb.append("<html>Time delay of " + delay + " time unit(s) is disabled due to <br /> age invariants in the following places:<br /><br />");
470 //JOptionPane.showMessageDialog(null, sb.toString());459 for (TimedPlace t : blockingPlaces) {
471 sb.append("</html>");460 sb.append(t.toString() + "<br />");
472 tab.getAnimationController().getOkButton().setEnabled(false);461 }
473 tab.getAnimationController().getOkButton().setToolTipText(sb.toString());462 //JOptionPane.showMessageDialog(null, sb.toString());
474 }463 sb.append("</html>");
475 }464 tab.getAnimationController().getOkButton().setEnabled(false);
476 } catch (NumberFormatException e) {465 tab.getAnimationController().getOkButton().setToolTipText(sb.toString());
477 // Do nothing, invalud number466 }
478 } catch (ParseException e) {467 }
479 tab.getAnimationController().getOkButton().setEnabled(false);468 } catch (ParseException | NumberFormatException e) {
480 tab.getAnimationController().getOkButton().setToolTipText("The text in the input field is not a number");469 tab.getAnimationController().getOkButton().setEnabled(false);
481 }470 tab.getAnimationController().getOkButton().setToolTipText("The text in the input field is not a number");
482 }471 }
483472 }
484 private DataLayer activeGuiModel() {473
485 return tab.currentTemplate().guiModel();474 private DataLayer activeGuiModel() {
486 }475 return tab.currentTemplate().guiModel();
487476 }
488 private void resethistory() {477
489 actionHistory.clear();478 private void resethistory() {
490 markings.clear();479 actionHistory.clear();
491 currentAction = -1;480 markings.clear();
492 currentMarkingIndex = 0;481 currentAction = -1;
493 tab.getAnimationHistorySidePanel().reset();482 currentMarkingIndex = 0;
494 if(tab.getUntimedAnimationHistory() != null){483 tab.getAnimationHistorySidePanel().reset();
495 tab.getUntimedAnimationHistory().reset();484 if(tab.getUntimedAnimationHistory() != null){
496 }485 tab.getUntimedAnimationHistory().reset();
497 }486 }
498487 }
499 public FiringMode getFiringmode() {488
500 return firingmode;489 public FiringMode getFiringmode() {
501 }490 return firingmode;
502491 }
503 // removes stored markings and actions from index "startWith" (included)492
504 private void removeStoredActions(int startWith) {493 // removes stored markings and actions from index "startWith" (included)
505 int lastIndex = actionHistory.size() - 1;494 private void removeStoredActions(int startWith) {
506 for (int i = startWith; i <= lastIndex; i++) {495 int lastIndex = actionHistory.size() - 1;
507 removeLastHistoryStep();496 for (int i = startWith; i <= lastIndex; i++) {
508 }497 removeLastHistoryStep();
509 }498 }
510499 }
511 private void addMarking(TAPNNetworkTraceStep action, NetworkMarking marking) {500
512 if (currentAction < actionHistory.size() - 1) {501 private void addMarking(TAPNNetworkTraceStep action, NetworkMarking marking) {
502 if (currentAction < actionHistory.size() - 1) {
513 removeStoredActions(currentAction + 1);503 removeStoredActions(currentAction + 1);
514 }504 }
515505
516 tab.network().setMarking(marking);506 tab.network().setMarking(marking);
517 tab.getAnimationHistorySidePanel().addHistoryItem(action.toString());507 tab.getAnimationHistorySidePanel().addHistoryItem(action.toString());
518 actionHistory.add(action);508 actionHistory.add(action);
519 markings.add(marking);509 markings.add(marking);
520 currentAction++;510 currentAction++;
521 currentMarkingIndex++;511 currentMarkingIndex++;
522 }512 }
523513
524 private void removeLastHistoryStep() {514 private void removeLastHistoryStep() {
525 actionHistory.remove(actionHistory.size() - 1);515 actionHistory.remove(actionHistory.size() - 1);
526 markings.remove(markings.size() - 1);516 markings.remove(markings.size() - 1);
527 }517 }
528518
529 //XXX: should be enum?519 //XXX: should be enum?
530 public static final String[] FIRINGMODES = { "Random", "Oldest", "Youngest", "Manual" };520 public static final String[] FIRINGMODES = { "Random", "Oldest", "Youngest", "Manual" };
531 public void setFiringmode(String t) {521 public void setFiringmode(String t) {
532 switch (t) {522 switch (t) {
533 case "Random":523 case "Random":
534 firingmode = new RandomFiringMode();524 firingmode = new RandomFiringMode();
535 break;525 break;
536 case "Youngest":526 case "Youngest":
537 firingmode = new YoungestFiringMode();527 firingmode = new YoungestFiringMode();
538 break;528 break;
539 case "Oldest":529 case "Oldest":
540 firingmode = new OldestFiringMode();530 firingmode = new OldestFiringMode();
541 break;531 break;
542 case "Manual":532 case "Manual":
543 firingmode = null;533 firingmode = null;
544 break;534 break;
545 default:535 default:
546 System.err536 System.err
547 .println("Illegal firing mode mode: " + t + " not found.");537 .println("Illegal firing mode mode: " + t + " not found.");
548 break;538 break;
549 }539 }
550540
551 tab.getAnimationController().updateFiringModeComboBox();541 tab.getAnimationController().updateFiringModeComboBox();
552 tab.getAnimationController().setToolTipText("Select a method for choosing tokens during transition firing");542 tab.getAnimationController().setToolTipText("Select a method for choosing tokens during transition firing");
553 } 543 }
554544
555 enum FillListStatus{545 enum FillListStatus{
556 lessThanWeight,546 lessThanWeight,
557 weight,547 weight,
558 moreThanWeight548 moreThanWeight
559 }549 }
560550
561 //Creates a list of tokens if there is only weight tokens in each of the places551 //Creates a list of tokens if there is only weight tokens in each of the places
562 //Used by getTokensToConsume552 //Used by getTokensToConsume
563 private FillListStatus fillList(TimedTransition transition, List<TimedToken> listToFill){553 private FillListStatus fillList(TimedTransition transition, List<TimedToken> listToFill){
564 for(TimedInputArc in: transition.getInputArcs()){554 for(TimedInputArc in: transition.getInputArcs()){
565 List<TimedToken> elligibleTokens = in.getElligibleTokens();555 List<TimedToken> elligibleTokens = in.getElligibleTokens();
566 if(elligibleTokens.size() < in.getWeight().value()){556 if(elligibleTokens.size() < in.getWeight().value()){
567 return FillListStatus.lessThanWeight;557 return FillListStatus.lessThanWeight;
568 } else if(elligibleTokens.size() == in.getWeight().value()){558 } else if(elligibleTokens.size() == in.getWeight().value()){
569 listToFill.addAll(elligibleTokens);559 listToFill.addAll(elligibleTokens);
570 } else {560 } else {
571 return FillListStatus.moreThanWeight;561 return FillListStatus.moreThanWeight;
572 }562 }
573 }563 }
574 for(TransportArc in: transition.getTransportArcsGoingThrough()){564 for(TransportArc in: transition.getTransportArcsGoingThrough()){
575 List<TimedToken> elligibleTokens = in.getElligibleTokens();565 List<TimedToken> elligibleTokens = in.getElligibleTokens();
576 if(elligibleTokens.size() < in.getWeight().value()){566 if(elligibleTokens.size() < in.getWeight().value()){
577 return FillListStatus.lessThanWeight;567 return FillListStatus.lessThanWeight;
578 } else if(elligibleTokens.size() == in.getWeight().value()){568 } else if(elligibleTokens.size() == in.getWeight().value()){
579 listToFill.addAll(elligibleTokens);569 listToFill.addAll(elligibleTokens);
580 } else {570 } else {
581 return FillListStatus.moreThanWeight;571 return FillListStatus.moreThanWeight;
582 }572 }
583 }573 }
584 return FillListStatus.weight;574 return FillListStatus.weight;
585 }575 }
586576
587 private List<TimedToken> getTokensToConsume(TimedTransition transition){577 private List<TimedToken> getTokensToConsume(TimedTransition transition){
588 //If there are only "weight tokens in each place578 //If there are only "weight tokens in each place
589 List<TimedToken> result = new ArrayList<TimedToken>();579 List<TimedToken> result = new ArrayList<TimedToken>();
590 boolean userShouldChoose = false;580 boolean userShouldChoose = false;
591 if(transition.isShared()){581 if(transition.isShared()){
592 for(TimedTransition t : transition.sharedTransition().transitions()){582 for(TimedTransition t : transition.sharedTransition().transitions()){
593 FillListStatus status = fillList(t, result);583 FillListStatus status = fillList(t, result);
594 if(status == FillListStatus.lessThanWeight){584 if(status == FillListStatus.lessThanWeight){
595 return null;585 return null;
596 } else if(status == FillListStatus.moreThanWeight){586 } else if(status == FillListStatus.moreThanWeight){
597 userShouldChoose = true;587 userShouldChoose = true;
598 break;588 break;
599 }589 }
600 }590 }
601 } else {591 } else {
602 FillListStatus status = fillList(transition, result);592 FillListStatus status = fillList(transition, result);
603 if(status == FillListStatus.lessThanWeight){593 if(status == FillListStatus.lessThanWeight){
604 return null;594 return null;
605 } else if(status == FillListStatus.moreThanWeight){595 } else if(status == FillListStatus.moreThanWeight){
606 userShouldChoose = true;596 userShouldChoose = true;
607 }597 }
608 }598 }
609599
610 if (userShouldChoose){600 if (userShouldChoose){
611 return showSelectSimulatorDialogue(transition);601 return showSelectSimulatorDialogue(transition);
612 } else {602 } else {
613 return result;603 return result;
614 }604 }
615 }605 }
616606
617 private List<TimedToken> showSelectSimulatorDialogue(TimedTransition transition) {607 private List<TimedToken> showSelectSimulatorDialogue(TimedTransition transition) {
618 EscapableDialog guiDialog = new EscapableDialog(CreateGui.getApp(), "Select Tokens", true);608 EscapableDialog guiDialog = new EscapableDialog(CreateGui.getApp(), "Select Tokens", true);
619609
620 Container contentPane = guiDialog.getContentPane();610 Container contentPane = guiDialog.getContentPane();
621 contentPane.setLayout(new BoxLayout(contentPane, BoxLayout.PAGE_AXIS));611 contentPane.setLayout(new BoxLayout(contentPane, BoxLayout.PAGE_AXIS));
622 AnimationTokenSelectDialog animationTokenSelectDialog = new AnimationTokenSelectDialog(transition);612 AnimationTokenSelectDialog animationSelectmodeDialog = new AnimationTokenSelectDialog(transition);
623 contentPane.add(animationTokenSelectDialog);613 contentPane.add(animationSelectmodeDialog);
624 guiDialog.setResizable(true);614 guiDialog.setResizable(true);
625615
626 // Make window fit contents' preferred size616 // Make window fit contents' preferred size
627 guiDialog.pack();617 guiDialog.pack();
628618
629 // Move window to the middle of the screen619 // Move window to the middle of the screen
630 guiDialog.setLocationRelativeTo(null);620 guiDialog.setLocationRelativeTo(null);
631 guiDialog.setVisible(true);621 guiDialog.setVisible(true);
632622
633 return animationTokenSelectDialog.getTokens();623 return animationSelectmodeDialog.getTokens();
634 }624 }
635625
636 public void reset(boolean keepInitial){626 public void reset(boolean keepInitial){
637 resethistory();627 resethistory();
638 removeSetTrace(false);628 removeSetTrace(false);
639 if(keepInitial && initialMarking != null){629 if(keepInitial && initialMarking != null){
640 markings.add(initialMarking);630 markings.add(initialMarking);
641 tab.network().setMarking(initialMarking);631 tab.network().setMarking(initialMarking);
642 currentAction = -1;632 currentAction = -1;
643 updateFireableTransitions();633 updateFireableTransitions();
644 }634 }
645 }635 }
646636
647 private boolean removeSetTrace(boolean askUser){637 private boolean removeSetTrace(boolean askUser){
648 if(askUser && isShowingTrace()){ //Warn about deleting trace638 if(askUser && isShowingTrace()){ //Warn about deleting trace
649 int answer = JOptionPane.showConfirmDialog(CreateGui.getApp(), 639 int answer = JOptionPane.showConfirmDialog(CreateGui.getApp(),
650 "You are about to remove the current trace.", 640 "You are about to remove the current trace.",
651 "Removing Trace", JOptionPane.OK_CANCEL_OPTION, JOptionPane.WARNING_MESSAGE);641 "Removing Trace", JOptionPane.OK_CANCEL_OPTION, JOptionPane.WARNING_MESSAGE);
652 if(answer != JOptionPane.OK_OPTION) return false;642 if(answer != JOptionPane.OK_OPTION) return false;
653 }643 }
654 if(isDisplayingUntimedTrace){644 if(isDisplayingUntimedTrace){
655 tab.removeAbstractAnimationPane();645 tab.removeAbstractAnimationPane();
656 }646 }
657 isDisplayingUntimedTrace = false;647 isDisplayingUntimedTrace = false;
658 trace = null;648 trace = null;
659 return true;649 return true;
660 }650 }
661651
662 public TimedTAPNNetworkTrace getTrace(){652 public TimedTAPNNetworkTrace getTrace(){
663 return (TimedTAPNNetworkTrace)trace;653 return (TimedTAPNNetworkTrace)trace;
664 }654 }
665655
666 private boolean clearStepsForward(){656 private boolean clearStepsForward(){
667 boolean answer = true;657 boolean answer = true;
668 if(!isDisplayingUntimedTrace){658 if(!isDisplayingUntimedTrace){
669 answer = removeSetTrace(true);659 answer = removeSetTrace(true);
670 }660 }
671 if(answer){661 if(answer){
672 tab.getAnimationHistorySidePanel().clearStepsForward();662 tab.getAnimationHistorySidePanel().clearStepsForward();
673 }663 }
674 return answer;664 return answer;
675 }665 }
676666
677 private boolean isShowingTrace(){667 private boolean isShowingTrace(){
678 return isDisplayingUntimedTrace || trace != null;668 return isDisplayingUntimedTrace || trace != null;
679 }669 }
680 670
681 public ArrayList<TAPNNetworkTraceStep> getActionHistory() {671 public ArrayList<TAPNNetworkTraceStep> getActionHistory() {
682 return actionHistory;672 return actionHistory;
683 }673 }
684674
685675
686 private void setEnabledStepbackwardAction(boolean b) {676 private void setEnabledStepbackwardAction(boolean b) {
687 stepbackwardAction.setEnabled(b);677 stepbackwardAction.setEnabled(b);
688
689 }678 }
690679
691 private void setEnabledStepforwardAction(boolean b) {680 private void setEnabledStepforwardAction(boolean b) {
692 stepforwardAction.setEnabled(b);681 stepforwardAction.setEnabled(b);
682 }
693683
694 }
695 public final GuiAction stepforwardAction = CreateGui.getAppGui().stepforwardAction;684 public final GuiAction stepforwardAction = CreateGui.getAppGui().stepforwardAction;
696 public final GuiAction stepbackwardAction = CreateGui.getAppGui().stepbackwardAction;685 public final GuiAction stepbackwardAction = CreateGui.getAppGui().stepbackwardAction;
697686
@@ -703,8 +692,6 @@
703692
704 }693 }
705694
706 /* GUI Model / Actions helpers */
707 //XXX: Should be moved to animationController or similar
708 /**695 /**
709 * Updates the mouseOver label showing token ages in animationmode696 * Updates the mouseOver label showing token ages in animationmode
710 * when a "animation" action is happening. "live updates" any mouseOver label697 * when a "animation" action is happening. "live updates" any mouseOver label
@@ -717,4 +704,5 @@
717 }704 }
718 }705 }
719 }706 }
707
720}708}
721709
=== modified file 'src/pipe/gui/CreateGui.java'
--- src/pipe/gui/CreateGui.java 2020-05-27 13:07:27 +0000
+++ src/pipe/gui/CreateGui.java 2020-07-09 12:55:48 +0000
@@ -14,16 +14,14 @@
1414
15public class CreateGui {15public class CreateGui {
1616
17 private static GuiFrame appGui;17 private final static GuiFrame appGui = new GuiFrame(TAPAAL.getProgramName());
18 private static GuiFrameController appGuiController;18 private final static GuiFrameController appGuiController = new GuiFrameController(appGui);
1919
20 private static ArrayList<TabContent> tabs = new ArrayList<TabContent>();20 private static final ArrayList<TabContent> tabs = new ArrayList<TabContent>();
2121
22 public static void init() {22 public static void init() {
23 appGui = new GuiFrame(TAPAAL.getProgramName());
24 appGuiController = new GuiFrameController(appGui);
2523
26 if (Platform.isMac()){24 if (Platform.isMac()){
27 try {25 try {
28 SpecialMacHandler.postprocess();26 SpecialMacHandler.postprocess();
29 } catch (NoClassDefFoundError e) {27 } catch (NoClassDefFoundError e) {
@@ -37,8 +35,7 @@
3735
38 @Deprecated36 @Deprecated
39 public static DataLayer getModel() {37 public static DataLayer getModel() {
40 if (appGui==null) return null;38 return getModel(appGui.getSelectedTabIndex());
41 return getModel(appGui.getSelectedTabIndex());
42 }39 }
4340
44 @Deprecated41 @Deprecated
@@ -140,4 +137,6 @@
140 }137 }
141138
142139
140 public static boolean useExtendedBounds = false;
141
143}142}
144143
=== modified file 'src/pipe/gui/DelayEnabledTransitionControl.java'
--- src/pipe/gui/DelayEnabledTransitionControl.java 2020-05-18 14:33:45 +0000
+++ src/pipe/gui/DelayEnabledTransitionControl.java 2020-07-09 12:55:48 +0000
@@ -30,11 +30,11 @@
30 private static BigDecimal defaultGranularity = new BigDecimal("0.1");30 private static BigDecimal defaultGranularity = new BigDecimal("0.1");
31 private static boolean defaultIsRandomTrasition;31 private static boolean defaultIsRandomTrasition;
32 32
33 private JLabel precitionLabel;33 private final JLabel precitionLabel;
34 private JSlider delayEnabledPrecision;34 private final JSlider delayEnabledPrecision;
35 private JLabel delayModeLabel;35 private final JLabel delayModeLabel;
36 private JComboBox<DelayMode> delayMode;36 private final JComboBox<DelayMode> delayMode;
37 JCheckBox randomMode;37 final JCheckBox randomMode = new JCheckBox("Choose next transition randomly");
38 38
39 private DelayEnabledTransitionControl() {39 private DelayEnabledTransitionControl() {
40 super(new GridBagLayout());40 super(new GridBagLayout());
@@ -61,9 +61,8 @@
61 DelayMode[] items = {ShortestDelayMode.getInstance(), RandomDelayMode.getInstance(), ManualDelayMode.getInstance()};61 DelayMode[] items = {ShortestDelayMode.getInstance(), RandomDelayMode.getInstance(), ManualDelayMode.getInstance()};
62 delayMode = new JComboBox(items);62 delayMode = new JComboBox(items);
63 setDelayMode(defaultDelayMode);63 setDelayMode(defaultDelayMode);
64 64
65 randomMode = new JCheckBox("Choose next transition randomly");65 setRandomTransitionMode(defaultIsRandomTrasition);
66 setRandomTransitionMode(defaultIsRandomTrasition);
67 66
68 GridBagConstraints gbc = new GridBagConstraints();67 GridBagConstraints gbc = new GridBagConstraints();
69 gbc.gridwidth = 2;68 gbc.gridwidth = 2;
7069
=== modified file 'src/pipe/gui/GuiFrame.java'
--- src/pipe/gui/GuiFrame.java 2020-06-22 08:06:22 +0000
+++ src/pipe/gui/GuiFrame.java 2020-07-09 12:55:48 +0000
@@ -40,1103 +40,1175 @@
40import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNDiscreteVerification;40import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNDiscreteVerification;
4141
4242
43public class GuiFrame extends JFrame implements GuiFrameActions, SafeGuiFrameActions {43public class GuiFrame extends JFrame implements GuiFrameActions, SafeGuiFrameActions {
4444
45 // for zoom combobox and dropdown45 // for zoom combobox and dropdown
46 private final int[] zoomLevels = { 40, 60, 80, 100, 120, 140, 160, 180, 200, 300 };46 private final int[] zoomLevels = {40, 60, 80, 100, 120, 140, 160, 180, 200, 300};
47 47
48 private String frameTitle;48 private String frameTitle;
4949
50 private Pipe.ElementType mode;50 private Pipe.ElementType mode;
5151
52 private int newNameCounter = 1;52 private int newNameCounter = 1;
5353
54 final MutableReference<GuiFrameControllerActions> guiFrameController = new MutableReference<>();54 final MutableReference<GuiFrameControllerActions> guiFrameController = new MutableReference<>();
5555
56 private ExtendedJTabbedPane<TabContent> appTab;56 private ExtendedJTabbedPane<TabContent> appTab;
5757
58 private StatusBar statusBar;58 private StatusBar statusBar;
59 private JMenuBar menuBar;59 private JMenuBar menuBar;
60 private JToolBar drawingToolBar;60 private JToolBar drawingToolBar;
61 private JComboBox<String> zoomComboBox;61 private JComboBox<String> zoomComboBox;
6262
63 private GuiAction createAction;63 private static final int shortcutkey = Toolkit.getDefaultToolkit().getMenuShortcutKeyMask();
64 private GuiAction openAction;64
65 private GuiAction closeAction;65 private final GuiAction createAction = new GuiAction("New", "Create a new Petri net", KeyStroke.getKeyStroke('N', shortcutkey)) {
66 private GuiAction saveAction;66 public void actionPerformed(ActionEvent arg0) {
67 private GuiAction saveAsAction;67 guiFrameController.ifPresent(GuiFrameControllerActions::showNewPNDialog);
68 private GuiAction exitAction;68 }
69 private GuiAction printAction;69 };
70 private GuiAction importPNMLAction;70 private final GuiAction openAction = new GuiAction("Open", "Open", KeyStroke.getKeyStroke('O', shortcutkey)) {
71 private GuiAction importSUMOAction;71 public void actionPerformed(ActionEvent arg0) {
72 private GuiAction importXMLAction;72 guiFrameController.ifPresent(GuiFrameControllerActions::openTAPNFile);
73 private GuiAction exportPNGAction;73 }
74 private GuiAction exportPSAction;74 };
75 private GuiAction exportToTikZAction;75 private final GuiAction closeAction = new GuiAction("Close", "Close the current tab", KeyStroke.getKeyStroke('W', shortcutkey)) {
76 private GuiAction exportToPNMLAction;76 public void actionPerformed(ActionEvent arg0) {
77 private GuiAction exportToXMLAction;77 TabContent index = (TabContent) appTab.getSelectedComponent();
78 private GuiAction exportTraceAction;78 guiFrameController.ifPresent(o -> o.closeTab(index));
79 private GuiAction importTraceAction;79 }
80 private GuiAction exportBatchAction;80 };
8181 private final GuiAction saveAction = new GuiAction("Save", "Save", KeyStroke.getKeyStroke('S', shortcutkey)) {
82 private GuiAction /* copyAction, cutAction, pasteAction, */undoAction, redoAction;82 public void actionPerformed(ActionEvent arg0) {
83 private GuiAction toggleGrid;83 if (canNetBeSavedAndShowMessage()) {
84 private GuiAction alignToGrid;84 guiFrameController.ifPresent(GuiFrameControllerActions::save);
85 private GuiAction netStatisticsAction;85 }
86 private GuiAction batchProcessingAction;86 }
87 private GuiAction engineSelectionAction;87 };
88 private GuiAction clearPreferencesAction;88 private final GuiAction saveAsAction = new GuiAction("Save as", "Save as...", KeyStroke.getKeyStroke('S', (shortcutkey + InputEvent.SHIFT_MASK))) {
8989 public void actionPerformed(ActionEvent arg0) {
90 private GuiAction verifyAction;90 if (canNetBeSavedAndShowMessage()) {
91 private GuiAction workflowDialogAction;91 guiFrameController.ifPresent(GuiFrameControllerActions::saveAs);
92 private GuiAction smartDrawAction;92 }
93 private GuiAction mergeComponentsDialogAction;93 }
94 private GuiAction stripTimeDialogAction;94 };
9595 private final GuiAction exitAction = new GuiAction("Exit", "Close the program", KeyStroke.getKeyStroke('Q', shortcutkey)) {
96 private GuiAction zoomOutAction;96 public void actionPerformed(ActionEvent arg0) {
97 private GuiAction zoomInAction;97 guiFrameController.ifPresent(GuiFrameControllerActions::exit);
98 private GuiAction zoomToAction;98 }
9999 };
100 private GuiAction incSpacingAction;100 private final GuiAction printAction = new GuiAction("Print", "Print", KeyStroke.getKeyStroke('P', shortcutkey)) {
101 private GuiAction decSpacingAction;101 public void actionPerformed(ActionEvent arg0) {
102 public GuiAction deleteAction;102 Export.exportGuiView(getCurrentTab().drawingSurface(), Export.PRINTER, null);
103103 }
104 private GuiAction annotationAction;104 };
105 private GuiAction inhibarcAction;105 private final GuiAction importPNMLAction = new GuiAction("PNML untimed net", "Import an untimed net in the PNML format", KeyStroke.getKeyStroke('X', shortcutkey)) {
106 private GuiAction transAction;106 public void actionPerformed(ActionEvent arg0) {
107 private GuiAction tokenAction;107 guiFrameController.ifPresent(GuiFrameControllerActions::importPNMLFile);
108 private GuiAction selectAction;108 }
109 private GuiAction deleteTokenAction;109 };
110 private GuiAction timedPlaceAction;110 private final GuiAction importSUMOAction = new GuiAction("SUMO queries (.txt)", "Import SUMO queries in a plain text format") {
111111 public void actionPerformed(ActionEvent arg0) {
112 private GuiAction timedArcAction;112 currentTab.ifPresent(TabContentActions::importSUMOQueries);
113 private GuiAction transportArcAction;113 }
114114 };
115 private GuiAction showTokenAgeAction;115 private final GuiAction importXMLAction = new GuiAction("XML queries (.xml)", "Import MCC queries in XML format", KeyStroke.getKeyStroke('R', shortcutkey)) {
116 private GuiAction showComponentsAction;116 public void actionPerformed(ActionEvent arg0) {
117 private GuiAction showSharedPTAction;117 currentTab.ifPresent(TabContentActions::importXMLQueries);
118 private GuiAction showQueriesAction;118 }
119 private GuiAction showConstantsAction;119 };
120 private GuiAction showZeroToInfinityIntervalsAction;120 private final GuiAction exportPNGAction = new GuiAction("PNG", "Export the net to PNG format", KeyStroke.getKeyStroke('G', shortcutkey)) {
121 private GuiAction showEnabledTransitionsAction;121 public void actionPerformed(ActionEvent arg0) {
122 private GuiAction showDelayEnabledTransitionsAction;122 if (canNetBeSavedAndShowMessage()) {
123 private GuiAction showToolTipsAction;123 Export.exportGuiView(getCurrentTab().drawingSurface(), Export.PNG, null);
124 private GuiAction showAdvancedWorkspaceAction;124 }
125 private GuiAction showSimpleWorkspaceAction;125 }
126 private GuiAction saveWorkSpaceAction;126 };
127 private GuiAction showAboutAction;127 private final GuiAction exportPSAction = new GuiAction("PostScript", "Export the net to PostScript format", KeyStroke.getKeyStroke('T', shortcutkey)) {
128 private GuiAction showHomepage;128 public void actionPerformed(ActionEvent arg0) {
129 private GuiAction showAskQuestionAction;129 if (canNetBeSavedAndShowMessage()) {
130 private GuiAction showReportBugAction;130 Export.exportGuiView(getCurrentTab().drawingSurface(), Export.POSTSCRIPT, null);
131 private GuiAction showFAQAction;131 }
132 private GuiAction checkUpdate;132 }
133 133 };
134134 private final GuiAction exportToTikZAction = new GuiAction("TikZ", "Export the net to LaTex (TikZ) format", KeyStroke.getKeyStroke('L', shortcutkey)) {
135 private GuiAction selectAllAction;135 public void actionPerformed(ActionEvent arg0) {
136136 if (canNetBeSavedAndShowMessage()) {
137 private GuiAction startAction;137 Export.exportGuiView(getCurrentTab().drawingSurface(), Export.TIKZ, getCurrentTab().drawingSurface().getGuiModel());
138 public GuiAction stepforwardAction;138 }
139 public GuiAction stepbackwardAction;139 }
140 private GuiAction timeAction;140 };
141 private GuiAction delayFireAction;141 private final GuiAction exportToPNMLAction = new GuiAction("PNML", "Export the net to PNML format", KeyStroke.getKeyStroke('D', shortcutkey)) {
142 private GuiAction prevcomponentAction;142 public void actionPerformed(ActionEvent arg0) {
143 private GuiAction nextcomponentAction;143 if (canNetBeSavedAndShowMessage()) {
144144 if (Preferences.getInstance().getShowPNMLWarning()) {
145 public enum GUIMode {145 JCheckBox showAgain = new JCheckBox("Do not show this warning.");
146 draw, animation, noNet146 String message = "In the saved PNML all timing information will be lost\n" +
147 }
148
149 private JCheckBoxMenuItem showZeroToInfinityIntervalsCheckBox;
150 private JCheckBoxMenuItem showTokenAgeCheckBox;
151
152 private JMenu zoomMenu;
153
154 public GuiFrame(String title) {
155 // HAK-arrange for frameTitle to be initialized and the default file
156 // name to be appended to basic window title
157
158 frameTitle = title;
159 setTitle(null);
160 trySetLookAndFeel();
161
162 Dimension screenSize = Toolkit.getDefaultToolkit().getScreenSize();
163 this.setSize(screenSize.width * 80 / 100, screenSize.height * 80 / 100);
164 this.setLocationRelativeTo(null);
165 this.setMinimumSize(new Dimension(825, 480));
166
167 setDefaultCloseOperation(DO_NOTHING_ON_CLOSE);
168
169 //XXX: Moved appTab from creategui needs further refacotring
170 //kyrke 2018-05-20
171 appTab = new ExtendedJTabbedPane<TabContent>() {
172 @Override
173 public Component generator() {
174 return new TabComponent(this) {
The diff has been truncated for viewing.

Subscribers

People subscribed via source and target branches