Merge lp:~tapaal-contributor/tapaal/draw-urgent-transition-timed-net-icon-1951026 into lp:tapaal

Proposed by Kristian Morsing Pedersen
Status: Merged
Approved by: Jiri Srba
Approved revision: 1161
Merged at revision: 1160
Proposed branch: lp:~tapaal-contributor/tapaal/draw-urgent-transition-timed-net-icon-1951026
Merge into: lp:tapaal
Diff against target: 189 lines (+68/-10)
2 files modified
src/dk/aau/cs/gui/TabContent.java (+67/-9)
src/pipe/gui/Pipe.java (+1/-1)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/draw-urgent-transition-timed-net-icon-1951026
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Review via email: mp+412179@code.launchpad.net

This proposal supersedes a proposal from 2021-11-20.

Commit message

Added support, and icon, for drawing urgent transitions and uncontrollable urgent transitions.

Description of the change

In the menu, when the lens is set to a timed net, a new icon with an urgent transition will appear in the menu beside the transition icon. Clicking this will allow to directly draw urgent transitions.
This option has also been added to the "Draw menu"

To post a comment you must log in.
Revision history for this message
Jiri Srba (srba) wrote : Posted in a previous version of this proposal

Looks good but for timed and game, there has to be also added uncontrollable urgent transition icon (empty rectangle with black dot) and option in the draw menu.

review: Needs Fixing
Revision history for this message
Jiri Srba (srba) : Posted in a previous version of this proposal
review: Approve
Revision history for this message
Jiri Srba (srba) wrote : Posted in a previous version of this proposal

Has a merge conflict with trunk

review: Needs Fixing
Revision history for this message
Jiri Srba (srba) :
review: Approve
1162. By Kristian Morsing Pedersen <email address hidden>

Toggle uncontrollable transition is now greyed out while in simulation mode

Revision history for this message
Jiri Srba (srba) :
review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/dk/aau/cs/gui/TabContent.java'
2--- src/dk/aau/cs/gui/TabContent.java 2021-11-20 20:35:25 +0000
3+++ src/dk/aau/cs/gui/TabContent.java 2021-11-20 21:20:51 +0000
4@@ -171,10 +171,11 @@
5 return new Result<>(pnObject);
6 }
7
8- public Result<TimedTransitionComponent, ModelViolation> addNewTimedTransitions(DataLayer c, Point p, boolean isUncontrollable) {
9+ public Result<TimedTransitionComponent, ModelViolation> addNewTimedTransitions(DataLayer c, Point p, boolean isUncontrollable, boolean isUrgent) {
10 dk.aau.cs.model.tapn.TimedTransition transition = new dk.aau.cs.model.tapn.TimedTransition(drawingSurface.getNameGenerator().getNewTransitionName(guiModelToModel.get(c)));
11
12 transition.setUncontrollable(isUncontrollable);
13+ transition.setUrgent(isUrgent);
14 TimedTransitionComponent pnObject = new TimedTransitionComponent(p.x, p.y, transition, lens);
15
16 guiModelToModel.get(c).add(transition);
17@@ -1859,9 +1860,15 @@
18 case TAPNTRANS:
19 setManager(new CanvasTransitionDrawController());
20 break;
21+ case TAPNURGENTTRANS:
22+ setManager(new CanvasUrgentTransitionDrawController());
23+ break;
24 case UNCONTROLLABLETRANS:
25 setManager(new CanvasUncontrollableTransitionDrawController());
26 break;
27+ case TAPNURGENTUNCONTROLLABLETRANS:
28+ setManager(new CanvasUncontrollableUrgentTransitionDrawController());
29+ break;
30 case ANNOTATION:
31 setManager(new CanvasAnnotationNoteDrawController());
32 break;
33@@ -2235,7 +2242,22 @@
34 public void drawingSurfaceMousePressed(MouseEvent e) {
35 Point p = canvas.adjustPointToGridAndZoom(e.getPoint(), canvas.getZoom());
36
37- guiModelManager.addNewTimedTransitions(drawingSurface.getGuiModel(), p, false);
38+ guiModelManager.addNewTimedTransitions(drawingSurface.getGuiModel(), p, false, false);
39+ }
40+
41+ @Override
42+ public void registerEvents() {
43+
44+ }
45+ }
46+
47+ class CanvasUrgentTransitionDrawController extends AbstractDrawingSurfaceManager {
48+
49+ @Override
50+ public void drawingSurfaceMousePressed(MouseEvent e) {
51+ Point p = canvas.adjustPointToGridAndZoom(e.getPoint(), canvas.getZoom());
52+
53+ guiModelManager.addNewTimedTransitions(drawingSurface.getGuiModel(), p, false, true);
54 }
55
56 @Override
57@@ -2250,7 +2272,22 @@
58 public void drawingSurfaceMousePressed(MouseEvent e) {
59 Point p = canvas.adjustPointToGridAndZoom(e.getPoint(), canvas.getZoom());
60
61- guiModelManager.addNewTimedTransitions(drawingSurface.getGuiModel(), p, true);
62+ guiModelManager.addNewTimedTransitions(drawingSurface.getGuiModel(), p, true, false);
63+ }
64+
65+ @Override
66+ public void registerEvents() {
67+
68+ }
69+ }
70+
71+ class CanvasUncontrollableUrgentTransitionDrawController extends AbstractDrawingSurfaceManager {
72+
73+ @Override
74+ public void drawingSurfaceMousePressed(MouseEvent e) {
75+ Point p = canvas.adjustPointToGridAndZoom(e.getPoint(), canvas.getZoom());
76+
77+ guiModelManager.addNewTimedTransitions(drawingSurface.getGuiModel(), p, true, true);
78 }
79
80 @Override
81@@ -2387,7 +2424,7 @@
82 var r = guiModelManager.addNewTimedPlace(getModel(), p);
83 placeClicked(r.result, e);
84 } else { //Transition
85- var r = guiModelManager.addNewTimedTransitions(getModel(), p, false);
86+ var r = guiModelManager.addNewTimedTransitions(getModel(), p, false, false);
87 transitionClicked(r.result, e);
88 }
89 }
90@@ -2831,11 +2868,11 @@
91 }
92 }
93 public List<GuiAction> getAvailableDrawActions(){
94- if (lens.isTimed() && !lens.isGame()) {
95- return new ArrayList<>(Arrays.asList(selectAction, timedPlaceAction, transAction, timedArcAction, transportArcAction, inhibarcAction, tokenAction, deleteTokenAction, annotationAction, toggleUrgentAction));
96- } else if (lens.isTimed()) {
97- return new ArrayList<>(Arrays.asList(selectAction, timedPlaceAction, transAction, uncontrollableTransAction, timedArcAction, transportArcAction, inhibarcAction, tokenAction, deleteTokenAction, annotationAction, toggleUrgentAction, toggleUncontrollableAction));
98- } else if (lens.isGame()){
99+ if (lens.isTimed() && lens.isGame()) {
100+ return new ArrayList<>(Arrays.asList(selectAction, timedPlaceAction, transAction, urgentTransAction, uncontrollableTransAction, uncontrollableUrgentTransAction, timedArcAction, transportArcAction, inhibarcAction, tokenAction, deleteTokenAction, annotationAction, toggleUrgentAction, toggleUncontrollableAction));
101+ } else if (lens.isTimed() && !lens.isGame()) {
102+ return new ArrayList<>(Arrays.asList(selectAction, timedPlaceAction, transAction, urgentTransAction, timedArcAction, transportArcAction, inhibarcAction, tokenAction, deleteTokenAction, annotationAction, toggleUrgentAction));
103+ } else if (!lens.isTimed() && lens.isGame()){
104 return new ArrayList<>(Arrays.asList(selectAction, timedPlaceAction, transAction, uncontrollableTransAction, timedArcAction, inhibarcAction, tokenAction, deleteTokenAction, annotationAction, toggleUncontrollableAction));
105 } else {
106 return new ArrayList<>(Arrays.asList(selectAction, timedPlaceAction, transAction, timedArcAction, inhibarcAction, tokenAction, deleteTokenAction, annotationAction));
107@@ -2872,11 +2909,21 @@
108 setMode(Pipe.ElementType.TAPNTRANS);
109 }
110 };
111+ private final GuiAction urgentTransAction = new GuiAction("Urgent transition", "Add an urgent transition (Y)", "Y", true) {
112+ public void actionPerformed(ActionEvent e) {
113+ setMode(Pipe.ElementType.TAPNURGENTTRANS);
114+ }
115+ };
116 private final GuiAction uncontrollableTransAction = new GuiAction("Uncontrollable transition", "Add an uncontrollable transition (L)", "L", true) {
117 public void actionPerformed(ActionEvent e) {
118 setMode(Pipe.ElementType.UNCONTROLLABLETRANS);
119 }
120 };
121+ private final GuiAction uncontrollableUrgentTransAction = new GuiAction("Uncontrollable urgent transition", "Add an uncontrollable urgent transition (O)", "O", true) {
122+ public void actionPerformed(ActionEvent e) {
123+ setMode(Pipe.ElementType.TAPNURGENTUNCONTROLLABLETRANS);
124+ }
125+ };
126 private final GuiAction tokenAction = new GuiAction("Add token", "Add a token (+)", "typed +", true) {
127 public void actionPerformed(ActionEvent e) {
128 setMode(Pipe.ElementType.ADDTOKEN);
129@@ -2929,7 +2976,9 @@
130 // deselect other actions
131 selectAction.setSelected(CreateGui.guiMode == Pipe.ElementType.SELECT);
132 transAction.setSelected(editorMode == Pipe.ElementType.TAPNTRANS);
133+ urgentTransAction.setSelected(editorMode == Pipe.ElementType.TAPNURGENTTRANS);
134 uncontrollableTransAction.setSelected(editorMode == Pipe.ElementType.UNCONTROLLABLETRANS);
135+ uncontrollableUrgentTransAction.setSelected(editorMode == Pipe.ElementType.TAPNURGENTUNCONTROLLABLETRANS);
136 timedPlaceAction.setSelected(editorMode == Pipe.ElementType.TAPNPLACE);
137 timedArcAction.setSelected(editorMode == Pipe.ElementType.TAPNARC);
138 transportArcAction.setSelected(editorMode == Pipe.ElementType.TRANSPORTARC);
139@@ -2944,7 +2993,10 @@
140 case draw:
141 selectAction.setEnabled(true);
142 transAction.setEnabled(true);
143+ urgentTransAction.setEnabled(true);
144 uncontrollableTransAction.setEnabled(true);
145+ toggleUncontrollableAction.setEnabled(true);
146+ uncontrollableUrgentTransAction.setEnabled(true);
147 toggleUrgentAction.setEnabled(true);
148 timedPlaceAction.setEnabled(true);
149 timedArcAction.setEnabled(true);
150@@ -2959,7 +3011,10 @@
151 case noNet:
152 selectAction.setEnabled(false);
153 transAction.setEnabled(false);
154+ urgentTransAction.setEnabled(false);
155 uncontrollableTransAction.setEnabled(false);
156+ toggleUncontrollableAction.setEnabled(false);
157+ uncontrollableUrgentTransAction.setEnabled(false);
158 toggleUrgentAction.setEnabled(false);
159 timedPlaceAction.setEnabled(false);
160 timedArcAction.setEnabled(false);
161@@ -2973,7 +3028,10 @@
162 case animation:
163 selectAction.setEnabled(false);
164 transAction.setEnabled(false);
165+ urgentTransAction.setEnabled(false);
166 uncontrollableTransAction.setEnabled(false);
167+ toggleUncontrollableAction.setEnabled(false);
168+ uncontrollableUrgentTransAction.setEnabled(false);
169 toggleUrgentAction.setEnabled(false);
170 timedPlaceAction.setEnabled(false);
171 timedArcAction.setEnabled(false);
172
173=== modified file 'src/pipe/gui/Pipe.java'
174--- src/pipe/gui/Pipe.java 2021-04-04 09:31:58 +0000
175+++ src/pipe/gui/Pipe.java 2021-11-20 21:20:51 +0000
176@@ -8,7 +8,7 @@
177 public enum ElementType {
178 PLACE, IMMTRANS, TIMEDTRANS, ANNOTATION, ARC, INHIBARC,
179 //TAPN Elements
180- TAPNPLACE, TAPNTRANS, UNCONTROLLABLETRANS, TAPNARC, TRANSPORTARC, TAPNINHIBITOR_ARC,
181+ TAPNPLACE, TAPNTRANS, TAPNURGENTTRANS, UNCONTROLLABLETRANS, TAPNURGENTUNCONTROLLABLETRANS, TAPNARC, TRANSPORTARC, TAPNINHIBITOR_ARC,
182 //Others (might refactore)
183 ADDTOKEN, DELTOKEN, SELECT, DRAW, DRAG,
184 }
185
186=== added file 'src/resources/Images/Uncontrollable urgent transition.png'
187Binary files src/resources/Images/Uncontrollable urgent transition.png 1970-01-01 00:00:00 +0000 and src/resources/Images/Uncontrollable urgent transition.png 2021-11-20 21:20:51 +0000 differ
188=== added file 'src/resources/Images/Urgent transition.png'
189Binary files src/resources/Images/Urgent transition.png 1970-01-01 00:00:00 +0000 and src/resources/Images/Urgent transition.png 2021-11-20 21:20:51 +0000 differ

Subscribers

People subscribed via source and target branches