Merge lp:~tapaal-contributor/tapaal/untimed-timed-gui into lp:tapaal

Proposed by Peter Haahr Taankvist on 2020-08-10
Status: Merged
Approved by: Jiri Srba on 2020-08-19
Approved revision: 1105
Merged at revision: 1084
Proposed branch: lp:~tapaal-contributor/tapaal/untimed-timed-gui
Merge into: lp:tapaal
Diff against target: 3103 lines (+872/-562)
60 files modified
src/dk/aau/cs/TCTL/AritmeticOperator.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLAFNode.java (+7/-2)
src/dk/aau/cs/TCTL/TCTLAGNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLAUNode.java (+8/-2)
src/dk/aau/cs/TCTL/TCTLAXNode.java (+7/-2)
src/dk/aau/cs/TCTL/TCTLAbstractProperty.java (+1/-1)
src/dk/aau/cs/TCTL/TCTLAndListNode.java (+14/-1)
src/dk/aau/cs/TCTL/TCTLAtomicPropositionNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLConstNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLDeadlockNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLEFNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLEGNode.java (+7/-2)
src/dk/aau/cs/TCTL/TCTLEUNode.java (+7/-1)
src/dk/aau/cs/TCTL/TCTLEXNode.java (+7/-2)
src/dk/aau/cs/TCTL/TCTLFalseNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLNotNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLOrListNode.java (+14/-1)
src/dk/aau/cs/TCTL/TCTLPathPlaceHolder.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLPathToStateConverter.java (+7/-2)
src/dk/aau/cs/TCTL/TCTLPlaceNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLPlusListNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLStatePlaceHolder.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLStateToPathConverter.java (+7/-2)
src/dk/aau/cs/TCTL/TCTLTermListNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLTransitionNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLTrueNode.java (+6/-1)
src/dk/aau/cs/gui/TabContent.java (+298/-71)
src/dk/aau/cs/gui/TabContentActions.java (+4/-0)
src/dk/aau/cs/gui/TabTransformer.java (+6/-3)
src/dk/aau/cs/gui/components/EnabledTransitionsList.java (+3/-2)
src/dk/aau/cs/gui/components/TransitionFireingComponent.java (+9/-5)
src/dk/aau/cs/io/LoadedModel.java (+13/-11)
src/dk/aau/cs/io/PNMLoader.java (+8/-6)
src/dk/aau/cs/io/TapnLegacyXmlLoader.java (+9/-9)
src/dk/aau/cs/io/TapnXmlLoader.java (+18/-33)
src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java (+10/-9)
src/dk/aau/cs/verification/TAPNComposer.java (+33/-25)
src/pipe/dataLayer/TAPNQuery.java (+10/-4)
src/pipe/gui/AnimationControlSidePanel.java (+23/-8)
src/pipe/gui/AnimationSettingsDialog.java (+13/-8)
src/pipe/gui/Animator.java (+4/-0)
src/pipe/gui/CreateGui.java (+4/-0)
src/pipe/gui/DelayEnabledTransitionControl.java (+6/-39)
src/pipe/gui/GuiFrame.java (+90/-166)
src/pipe/gui/GuiFrameActions.java (+9/-2)
src/pipe/gui/GuiFrameController.java (+3/-3)
src/pipe/gui/SimulationControl.java (+39/-6)
src/pipe/gui/StatusBar.java (+2/-93)
src/pipe/gui/action/GuiAction.java (+8/-0)
src/pipe/gui/canvas/DrawingSurfaceImpl.java (+4/-4)
src/pipe/gui/graphicElements/PetriNetObject.java (+11/-0)
src/pipe/gui/graphicElements/tapn/TimedInputArcComponent.java (+10/-2)
src/pipe/gui/graphicElements/tapn/TimedOutputArcComponent.java (+1/-0)
src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java (+12/-7)
src/pipe/gui/graphicElements/tapn/TimedTransitionComponent.java (+8/-4)
src/pipe/gui/handler/PetriNetObjectHandler.java (+4/-4)
src/pipe/gui/widgets/GuardDialogue.java (+5/-1)
src/pipe/gui/widgets/PlaceEditorPanel.java (+11/-0)
src/pipe/gui/widgets/QueryPane.java (+1/-1)
src/pipe/gui/widgets/TAPNTransitionEditor.java (+7/-3)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/untimed-timed-gui
Reviewer Review Type Date Requested Status
Jiri Srba 2020-08-10 Approve on 2020-08-19
Kenneth Yrke Jørgensen 2020-08-10 Approve on 2020-08-19
Peter Haahr Taankvist (community) Resubmit on 2020-08-17
Review via email: mp+388982@code.launchpad.net

Commit message

Hide time information if net is chosen to untimed.

To post a comment you must log in.
Kenneth Yrke Jørgensen (yrke) wrote :

please see DM.

review: Needs Fixing (code)
Peter Haahr Taankvist (ptaank) wrote :

Fixed an issue with pnObjects being set as untimed while actually being timed when opening files. DrawMenu will now be disabled if there are no available items (NoNet mode).

review: Resubmit
Kenneth Yrke Jørgensen (yrke) wrote :

The logic for loading nets has changed in order to get this working correctly:

  - pnml nets imported will be untimed, nongame
  - old format TAPAAL files, will be timed, nongame
  - new format TAPAAL files:
     - if they have lens/feature: features set in file
     - if they do not have lense/feature: timed, nongame

We can readd the feature to detect the type in a later branch, if we really need it. But right now it complicates things more that whats it good for, and with the new dropdowns its easy to change the net types.

review: Approve
1099. By Kenneth Yrke Jørgensen on 2020-08-14

Merged trunk

Jiri Srba (srba) wrote :

Open intro example and go to simulator and select Setting. Even though the net is timed,
the dialog is reduced and does not contain the granuality, delay mode etc.

Also, please move Choose next transition randomly to "Simulation controller" so that this one shows for untimed nets.

Finally, the two arrows < and > in "Simulation Control" should be visible also for untimed nets.

review: Needs Fixing
Jiri Srba (srba) wrote :

Another issue: open intro example and untime it; then open the query and it shows the reachability dialog instead of CTL dialog.

review: Needs Fixing
Kenneth Yrke Jørgensen (yrke) wrote :

> Another issue: open intro example and untime it; then open the query and it
> shows the reachability dialog instead of CTL dialog.

There is a similar issue if you go from an untimed net with CTL query to timed, the net will keep the CTL query. I guess we never implemented logic for converting queries.

1100. By Peter Haahr Taankvist on 2020-08-17

Show forward backward buttons in simulation mode. Show choose next transition randomly checkbox in simulation control in settings

1101. By Peter Haahr Taankvist on 2020-08-17

Remove affected queries when changing to timed. Show info message about queries

1102. By Peter Haahr Taankvist on 2020-08-17

Only show dialog if any queries have been removed

1103. By Peter Haahr Taankvist on 2020-08-17

Show CTL dialog if untimed, else show Reachability

Peter Haahr Taankvist (ptaank) wrote :

Moved "Choose next transition randomly" to simulation controller. Arrows in simulation mode are now visible. The QueryDialog will now use the lens to choose whether or not to show the CTL query or the Reachability query.

Finally, when converting to timed nets, CTL queries are removed and a dialog is shown informing about the removed queries.

review: Resubmit
Kenneth Yrke Jørgensen (yrke) wrote :

insted of using the hasNestedPathQuantifiers function i guess it should implement a visitor. But I can see the files has already been modified in a similar way, so I guess it ok.

review: Approve
Jiri Srba (srba) wrote :

Open intro example and go to simulation mode. When you hover over places,
it shows { 0 } and if you hover over transitions, it shows [0, inf). These
should be disabled for untimed nets.

review: Needs Fixing
1104. By Peter Taankvist <email address hidden> on 2020-08-19

only show age of tokens if timed

1105. By Peter Taankvist <email address hidden> on 2020-08-19

Only show interval if net is timed

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/TCTL/AritmeticOperator.java'
2--- src/dk/aau/cs/TCTL/AritmeticOperator.java 2017-03-12 00:33:00 +0000
3+++ src/dk/aau/cs/TCTL/AritmeticOperator.java 2020-08-19 11:36:17 +0000
4@@ -50,7 +50,12 @@
5 return false;
6 }
7
8- @Override
9+ @Override
10+ public boolean hasNestedPathQuantifiers() {
11+ return false;
12+ }
13+
14+ @Override
15 public TCTLAbstractProperty findFirstPlaceHolder() {
16 return null;
17 }
18
19=== modified file 'src/dk/aau/cs/TCTL/TCTLAFNode.java'
20--- src/dk/aau/cs/TCTL/TCTLAFNode.java 2017-03-12 00:33:00 +0000
21+++ src/dk/aau/cs/TCTL/TCTLAFNode.java 2020-08-19 11:36:17 +0000
22@@ -82,8 +82,13 @@
23 public boolean containsPlaceHolder() {
24 return property.containsPlaceHolder();
25 }
26-
27- public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
28+
29+ @Override
30+ public boolean hasNestedPathQuantifiers() {
31+ return property instanceof TCTLPathToStateConverter || property.hasNestedPathQuantifiers();
32+ }
33+
34+ public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
35 return property.containsAtomicPropositionWithSpecificPlaceInTemplate(templateName, placeName);
36 }
37
38
39=== modified file 'src/dk/aau/cs/TCTL/TCTLAGNode.java'
40--- src/dk/aau/cs/TCTL/TCTLAGNode.java 2017-03-12 00:33:00 +0000
41+++ src/dk/aau/cs/TCTL/TCTLAGNode.java 2020-08-19 11:36:17 +0000
42@@ -84,7 +84,12 @@
43 return property.containsPlaceHolder();
44 }
45
46- public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
47+ @Override
48+ public boolean hasNestedPathQuantifiers() {
49+ return property instanceof TCTLPathToStateConverter || property.hasNestedPathQuantifiers();
50+ }
51+
52+ public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
53 return property.containsAtomicPropositionWithSpecificPlaceInTemplate(templateName, placeName);
54 }
55
56
57=== modified file 'src/dk/aau/cs/TCTL/TCTLAUNode.java'
58--- src/dk/aau/cs/TCTL/TCTLAUNode.java 2017-03-12 00:33:00 +0000
59+++ src/dk/aau/cs/TCTL/TCTLAUNode.java 2020-08-19 11:36:17 +0000
60@@ -105,8 +105,14 @@
61 return left.containsPlaceHolder()
62 || right.containsPlaceHolder();
63 }
64-
65- public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
66+
67+ @Override
68+ public boolean hasNestedPathQuantifiers() {
69+ return left instanceof TCTLPathToStateConverter || right instanceof TCTLPathToStateConverter
70+ || left.hasNestedPathQuantifiers() || right.hasNestedPathQuantifiers();
71+ }
72+
73+ public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
74 return left.containsAtomicPropositionWithSpecificPlaceInTemplate(templateName, placeName)
75 || right.containsAtomicPropositionWithSpecificPlaceInTemplate(templateName, placeName);
76 }
77
78=== modified file 'src/dk/aau/cs/TCTL/TCTLAXNode.java'
79--- src/dk/aau/cs/TCTL/TCTLAXNode.java 2017-03-12 00:33:00 +0000
80+++ src/dk/aau/cs/TCTL/TCTLAXNode.java 2020-08-19 11:36:17 +0000
81@@ -82,8 +82,13 @@
82 public boolean containsPlaceHolder() {
83 return property.containsPlaceHolder();
84 }
85-
86- public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
87+
88+ @Override
89+ public boolean hasNestedPathQuantifiers() {
90+ return property instanceof TCTLPathToStateConverter || property.hasNestedPathQuantifiers();
91+ }
92+
93+ public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
94 return property.containsAtomicPropositionWithSpecificPlaceInTemplate(templateName, placeName);
95 }
96
97
98=== modified file 'src/dk/aau/cs/TCTL/TCTLAbstractProperty.java'
99--- src/dk/aau/cs/TCTL/TCTLAbstractProperty.java 2017-03-12 00:33:00 +0000
100+++ src/dk/aau/cs/TCTL/TCTLAbstractProperty.java 2020-08-19 11:36:17 +0000
101@@ -57,7 +57,7 @@
102 public abstract boolean containsAtomicPropositionWithSpecificTransitionInTemplate(String templateName, String transitionName);
103
104 public abstract boolean containsPlaceHolder();
105-
106+ public abstract boolean hasNestedPathQuantifiers();
107 // This method assumes that a place holder exists in the current query
108 public abstract TCTLAbstractProperty findFirstPlaceHolder();
109
110
111=== modified file 'src/dk/aau/cs/TCTL/TCTLAndListNode.java'
112--- src/dk/aau/cs/TCTL/TCTLAndListNode.java 2017-03-12 00:33:00 +0000
113+++ src/dk/aau/cs/TCTL/TCTLAndListNode.java 2020-08-19 11:36:17 +0000
114@@ -194,7 +194,20 @@
115 return placeHolderFound;
116 }
117
118- @Override
119+ @Override
120+ public boolean hasNestedPathQuantifiers() {
121+ boolean foundNestedQuantifier = false;
122+
123+ for (TCTLAbstractStateProperty p : properties) {
124+ foundNestedQuantifier = foundNestedQuantifier || p instanceof TCTLPathToStateConverter || p.hasNestedPathQuantifiers();
125+ if(foundNestedQuantifier){
126+ break;
127+ }
128+ }
129+ return foundNestedQuantifier;
130+ }
131+
132+ @Override
133 public TCTLAbstractProperty findFirstPlaceHolder() {
134 TCTLAbstractProperty ph = null;
135 for (TCTLAbstractStateProperty p : properties) {
136
137=== modified file 'src/dk/aau/cs/TCTL/TCTLAtomicPropositionNode.java'
138--- src/dk/aau/cs/TCTL/TCTLAtomicPropositionNode.java 2017-03-12 00:33:00 +0000
139+++ src/dk/aau/cs/TCTL/TCTLAtomicPropositionNode.java 2020-08-19 11:36:17 +0000
140@@ -83,7 +83,12 @@
141 return left.containsPlaceHolder() || right.containsPlaceHolder();
142 }
143
144- @Override
145+ @Override
146+ public boolean hasNestedPathQuantifiers() {
147+ return false;
148+ }
149+
150+ @Override
151 public TCTLAbstractProperty findFirstPlaceHolder() {
152 TCTLAbstractProperty rightP = right.findFirstPlaceHolder();
153
154
155=== modified file 'src/dk/aau/cs/TCTL/TCTLConstNode.java'
156--- src/dk/aau/cs/TCTL/TCTLConstNode.java 2017-03-12 00:33:00 +0000
157+++ src/dk/aau/cs/TCTL/TCTLConstNode.java 2020-08-19 11:36:17 +0000
158@@ -54,7 +54,12 @@
159 return false;
160 }
161
162- @Override
163+ @Override
164+ public boolean hasNestedPathQuantifiers() {
165+ return false;
166+ }
167+
168+ @Override
169 public TCTLAbstractProperty findFirstPlaceHolder() {
170 return null;
171 }
172
173=== modified file 'src/dk/aau/cs/TCTL/TCTLDeadlockNode.java'
174--- src/dk/aau/cs/TCTL/TCTLDeadlockNode.java 2017-03-12 00:33:00 +0000
175+++ src/dk/aau/cs/TCTL/TCTLDeadlockNode.java 2020-08-19 11:36:17 +0000
176@@ -35,7 +35,12 @@
177 return false;
178 }
179
180- public TCTLAbstractProperty findFirstPlaceHolder() {
181+ @Override
182+ public boolean hasNestedPathQuantifiers() {
183+ return false;
184+ }
185+
186+ public TCTLAbstractProperty findFirstPlaceHolder() {
187 return null;
188 }
189
190
191=== modified file 'src/dk/aau/cs/TCTL/TCTLEFNode.java'
192--- src/dk/aau/cs/TCTL/TCTLEFNode.java 2017-03-12 00:33:00 +0000
193+++ src/dk/aau/cs/TCTL/TCTLEFNode.java 2020-08-19 11:36:17 +0000
194@@ -83,7 +83,12 @@
195 return property.containsPlaceHolder();
196 }
197
198- public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
199+ @Override
200+ public boolean hasNestedPathQuantifiers() {
201+ return property instanceof TCTLPathToStateConverter || property.hasNestedPathQuantifiers();
202+ }
203+
204+ public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
205 return property.containsAtomicPropositionWithSpecificPlaceInTemplate(templateName, placeName);
206 }
207
208
209=== modified file 'src/dk/aau/cs/TCTL/TCTLEGNode.java'
210--- src/dk/aau/cs/TCTL/TCTLEGNode.java 2017-03-12 00:33:00 +0000
211+++ src/dk/aau/cs/TCTL/TCTLEGNode.java 2020-08-19 11:36:17 +0000
212@@ -82,8 +82,13 @@
213 public boolean containsPlaceHolder() {
214 return property.containsPlaceHolder();
215 }
216-
217- public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
218+
219+ @Override
220+ public boolean hasNestedPathQuantifiers() {
221+ return property instanceof TCTLPathToStateConverter || property.hasNestedPathQuantifiers();
222+ }
223+
224+ public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
225 return property.containsAtomicPropositionWithSpecificPlaceInTemplate(templateName, placeName);
226 }
227
228
229=== modified file 'src/dk/aau/cs/TCTL/TCTLEUNode.java'
230--- src/dk/aau/cs/TCTL/TCTLEUNode.java 2017-03-12 00:33:00 +0000
231+++ src/dk/aau/cs/TCTL/TCTLEUNode.java 2020-08-19 11:36:17 +0000
232@@ -106,7 +106,13 @@
233 || right.containsPlaceHolder();
234 }
235
236- public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
237+ @Override
238+ public boolean hasNestedPathQuantifiers() {
239+ return left instanceof TCTLPathToStateConverter || right instanceof TCTLPathToStateConverter
240+ || left.hasNestedPathQuantifiers() || right.hasNestedPathQuantifiers();
241+ }
242+
243+ public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
244 return left.containsAtomicPropositionWithSpecificPlaceInTemplate(templateName, placeName)
245 || right.containsAtomicPropositionWithSpecificPlaceInTemplate(templateName, placeName);
246 }
247
248=== modified file 'src/dk/aau/cs/TCTL/TCTLEXNode.java'
249--- src/dk/aau/cs/TCTL/TCTLEXNode.java 2017-03-12 00:33:00 +0000
250+++ src/dk/aau/cs/TCTL/TCTLEXNode.java 2020-08-19 11:36:17 +0000
251@@ -82,8 +82,13 @@
252 public boolean containsPlaceHolder() {
253 return property.containsPlaceHolder();
254 }
255-
256- public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
257+
258+ @Override
259+ public boolean hasNestedPathQuantifiers() {
260+ return property instanceof TCTLPathToStateConverter || property.hasNestedPathQuantifiers();
261+ }
262+
263+ public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
264 return property.containsAtomicPropositionWithSpecificPlaceInTemplate(templateName, placeName);
265 }
266
267
268=== modified file 'src/dk/aau/cs/TCTL/TCTLFalseNode.java'
269--- src/dk/aau/cs/TCTL/TCTLFalseNode.java 2017-03-12 00:33:00 +0000
270+++ src/dk/aau/cs/TCTL/TCTLFalseNode.java 2020-08-19 11:36:17 +0000
271@@ -35,7 +35,12 @@
272 return false;
273 }
274
275- public TCTLAbstractProperty findFirstPlaceHolder() {
276+ @Override
277+ public boolean hasNestedPathQuantifiers() {
278+ return false;
279+ }
280+
281+ public TCTLAbstractProperty findFirstPlaceHolder() {
282 return null;
283 }
284
285
286=== modified file 'src/dk/aau/cs/TCTL/TCTLNotNode.java'
287--- src/dk/aau/cs/TCTL/TCTLNotNode.java 2017-03-12 00:33:00 +0000
288+++ src/dk/aau/cs/TCTL/TCTLNotNode.java 2020-08-19 11:36:17 +0000
289@@ -88,7 +88,12 @@
290 return property.containsPlaceHolder();
291 }
292
293- @Override
294+ @Override
295+ public boolean hasNestedPathQuantifiers() {
296+ return property instanceof TCTLPathToStateConverter || property.hasNestedPathQuantifiers();
297+ }
298+
299+ @Override
300 public TCTLAbstractProperty findFirstPlaceHolder() {
301 return property.findFirstPlaceHolder();
302
303
304=== modified file 'src/dk/aau/cs/TCTL/TCTLOrListNode.java'
305--- src/dk/aau/cs/TCTL/TCTLOrListNode.java 2017-03-12 00:33:00 +0000
306+++ src/dk/aau/cs/TCTL/TCTLOrListNode.java 2020-08-19 11:36:17 +0000
307@@ -194,7 +194,20 @@
308 return placeHolderFound;
309 }
310
311- @Override
312+ @Override
313+ public boolean hasNestedPathQuantifiers() {
314+ boolean foundNestedQuantifier = false;
315+
316+ for (TCTLAbstractStateProperty p : properties) {
317+ foundNestedQuantifier = foundNestedQuantifier || p instanceof TCTLPathToStateConverter || p.hasNestedPathQuantifiers();
318+ if(foundNestedQuantifier){
319+ break;
320+ }
321+ }
322+ return foundNestedQuantifier;
323+ }
324+
325+ @Override
326 public TCTLAbstractProperty findFirstPlaceHolder() {
327 TCTLAbstractProperty ph = null;
328 for (TCTLAbstractStateProperty p : properties) {
329
330=== modified file 'src/dk/aau/cs/TCTL/TCTLPathPlaceHolder.java'
331--- src/dk/aau/cs/TCTL/TCTLPathPlaceHolder.java 2017-03-12 00:33:00 +0000
332+++ src/dk/aau/cs/TCTL/TCTLPathPlaceHolder.java 2020-08-19 11:36:17 +0000
333@@ -26,7 +26,12 @@
334 return true;
335 }
336
337- @Override
338+ @Override
339+ public boolean hasNestedPathQuantifiers() {
340+ return false;
341+ }
342+
343+ @Override
344 public boolean equals(Object o) {
345 if (o instanceof TCTLPathPlaceHolder) {
346 return true;
347
348=== modified file 'src/dk/aau/cs/TCTL/TCTLPathToStateConverter.java'
349--- src/dk/aau/cs/TCTL/TCTLPathToStateConverter.java 2017-03-12 00:33:00 +0000
350+++ src/dk/aau/cs/TCTL/TCTLPathToStateConverter.java 2020-08-19 11:36:17 +0000
351@@ -76,8 +76,13 @@
352 public boolean containsPlaceHolder() {
353 return property.containsPlaceHolder();
354 }
355-
356- public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
357+
358+ @Override
359+ public boolean hasNestedPathQuantifiers() {
360+ return false;
361+ }
362+
363+ public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
364 return property.containsAtomicPropositionWithSpecificPlaceInTemplate(templateName, placeName);
365 }
366
367
368=== modified file 'src/dk/aau/cs/TCTL/TCTLPlaceNode.java'
369--- src/dk/aau/cs/TCTL/TCTLPlaceNode.java 2017-03-12 00:33:00 +0000
370+++ src/dk/aau/cs/TCTL/TCTLPlaceNode.java 2020-08-19 11:36:17 +0000
371@@ -57,7 +57,12 @@
372 return false;
373 }
374
375- @Override
376+ @Override
377+ public boolean hasNestedPathQuantifiers() {
378+ return false;
379+ }
380+
381+ @Override
382 public TCTLAbstractProperty findFirstPlaceHolder() {
383 return null;
384 }
385
386=== modified file 'src/dk/aau/cs/TCTL/TCTLPlusListNode.java'
387--- src/dk/aau/cs/TCTL/TCTLPlusListNode.java 2017-03-12 00:33:00 +0000
388+++ src/dk/aau/cs/TCTL/TCTLPlusListNode.java 2020-08-19 11:36:17 +0000
389@@ -84,7 +84,12 @@
390 return false;
391 }
392
393- @Override
394+ @Override
395+ public boolean hasNestedPathQuantifiers() {
396+ return false;
397+ }
398+
399+ @Override
400 public TCTLAbstractProperty findFirstPlaceHolder() {
401 for(TCTLAbstractStateProperty term : terms){
402 TCTLAbstractProperty placeholder = term.findFirstPlaceHolder();
403
404=== modified file 'src/dk/aau/cs/TCTL/TCTLStatePlaceHolder.java'
405--- src/dk/aau/cs/TCTL/TCTLStatePlaceHolder.java 2017-03-12 00:33:00 +0000
406+++ src/dk/aau/cs/TCTL/TCTLStatePlaceHolder.java 2020-08-19 11:36:17 +0000
407@@ -26,7 +26,12 @@
408 return true;
409 }
410
411- @Override
412+ @Override
413+ public boolean hasNestedPathQuantifiers() {
414+ return false;
415+ }
416+
417+ @Override
418 public boolean equals(Object o) {
419 if (o instanceof TCTLStatePlaceHolder) {
420 return true;
421
422=== modified file 'src/dk/aau/cs/TCTL/TCTLStateToPathConverter.java'
423--- src/dk/aau/cs/TCTL/TCTLStateToPathConverter.java 2017-03-12 00:33:00 +0000
424+++ src/dk/aau/cs/TCTL/TCTLStateToPathConverter.java 2020-08-19 11:36:17 +0000
425@@ -76,8 +76,13 @@
426 public boolean containsPlaceHolder() {
427 return property.containsPlaceHolder();
428 }
429-
430- public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
431+
432+ @Override
433+ public boolean hasNestedPathQuantifiers() {
434+ return property.hasNestedPathQuantifiers();
435+ }
436+
437+ public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
438 return property.containsAtomicPropositionWithSpecificPlaceInTemplate(templateName, placeName);
439 }
440
441
442=== modified file 'src/dk/aau/cs/TCTL/TCTLTermListNode.java'
443--- src/dk/aau/cs/TCTL/TCTLTermListNode.java 2017-06-23 08:38:31 +0000
444+++ src/dk/aau/cs/TCTL/TCTLTermListNode.java 2020-08-19 11:36:17 +0000
445@@ -84,7 +84,12 @@
446 return false;
447 }
448
449- @Override
450+ @Override
451+ public boolean hasNestedPathQuantifiers() {
452+ return false;
453+ }
454+
455+ @Override
456 public TCTLAbstractProperty findFirstPlaceHolder() {
457 for(TCTLAbstractStateProperty factor : factors){
458 TCTLAbstractProperty placeholder = factor.findFirstPlaceHolder();
459
460=== modified file 'src/dk/aau/cs/TCTL/TCTLTransitionNode.java'
461--- src/dk/aau/cs/TCTL/TCTLTransitionNode.java 2017-03-12 00:33:00 +0000
462+++ src/dk/aau/cs/TCTL/TCTLTransitionNode.java 2020-08-19 11:36:17 +0000
463@@ -57,7 +57,12 @@
464 return false;
465 }
466
467- @Override
468+ @Override
469+ public boolean hasNestedPathQuantifiers() {
470+ return false;
471+ }
472+
473+ @Override
474 public TCTLAbstractProperty findFirstPlaceHolder() {
475 return null;
476 }
477
478=== modified file 'src/dk/aau/cs/TCTL/TCTLTrueNode.java'
479--- src/dk/aau/cs/TCTL/TCTLTrueNode.java 2017-03-12 00:33:00 +0000
480+++ src/dk/aau/cs/TCTL/TCTLTrueNode.java 2020-08-19 11:36:17 +0000
481@@ -35,7 +35,12 @@
482 return false;
483 }
484
485- public TCTLAbstractProperty findFirstPlaceHolder() {
486+ @Override
487+ public boolean hasNestedPathQuantifiers() {
488+ return false;
489+ }
490+
491+ public TCTLAbstractProperty findFirstPlaceHolder() {
492 return null;
493 }
494
495
496=== modified file 'src/dk/aau/cs/gui/TabContent.java'
497--- src/dk/aau/cs/gui/TabContent.java 2020-08-11 11:33:28 +0000
498+++ src/dk/aau/cs/gui/TabContent.java 2020-08-19 11:36:17 +0000
499@@ -1,5 +1,17 @@
500 package dk.aau.cs.gui;
501
502+import java.awt.*;
503+import java.awt.event.ActionEvent;
504+import java.awt.event.MouseAdapter;
505+import java.awt.event.MouseEvent;
506+import java.awt.geom.Point2D;
507+import java.io.*;
508+import java.math.BigDecimal;
509+import java.util.*;
510+import java.util.List;
511+
512+import javax.swing.*;
513+import javax.swing.border.BevelBorder;
514 import dk.aau.cs.debug.Logger;
515 import dk.aau.cs.gui.components.BugHandledJXMultisplitPane;
516 import dk.aau.cs.gui.components.StatisticsPanel;
517@@ -27,6 +39,7 @@
518 import pipe.dataLayer.TAPNQuery;
519 import pipe.dataLayer.Template;
520 import pipe.gui.*;
521+import pipe.gui.action.GuiAction;
522 import pipe.gui.canvas.DrawingSurfaceImpl;
523 import pipe.gui.graphicElements.*;
524 import pipe.gui.graphicElements.tapn.*;
525@@ -36,17 +49,7 @@
526 import pipe.gui.widgets.WorkflowDialog;
527 import pipe.gui.widgets.filebrowser.FileBrowser;
528
529-import javax.swing.*;
530-import javax.swing.border.BevelBorder;
531-import java.awt.*;
532-import java.awt.event.MouseAdapter;
533-import java.awt.event.MouseEvent;
534 import java.awt.event.MouseWheelEvent;
535-import java.awt.geom.Point2D;
536-import java.io.*;
537-import java.math.BigDecimal;
538-import java.util.List;
539-import java.util.*;
540
541 public class TabContent extends JSplitPane implements TabContentActions{
542
543@@ -56,7 +59,8 @@
544 this.guiFrameControllerActions.setReference(guiFrameControllerActions);
545 }
546
547- public static class TAPNLens {
548+ public static final class TAPNLens {
549+ public static final TAPNLens Default = new TAPNLens(true, true);
550 public boolean isTimed() {
551 return timed;
552 }
553@@ -68,7 +72,7 @@
554 private final boolean timed;
555 private final boolean game;
556
557- TAPNLens(boolean timed, boolean game) {
558+ public TAPNLens(boolean timed, boolean game) {
559 this.timed = timed;
560 this.game = game;
561 }
562@@ -156,7 +160,7 @@
563 Require.notNull(p, "Point can't be null");
564
565 dk.aau.cs.model.tapn.LocalTimedPlace tp = new dk.aau.cs.model.tapn.LocalTimedPlace(drawingSurface.getNameGenerator().getNewPlaceName(guiModelToModel.get(c)));
566- TimedPlaceComponent pnObject = new TimedPlaceComponent(p.x, p.y, tp);
567+ TimedPlaceComponent pnObject = new TimedPlaceComponent(p.x, p.y, tp, lens);
568 guiModelToModel.get(c).add(tp);
569 c.addPetriNetObject(pnObject);
570
571@@ -167,7 +171,7 @@
572 public Result<TimedTransitionComponent, ModelViolation> addNewTimedTransitions(DataLayer c, Point p) {
573 dk.aau.cs.model.tapn.TimedTransition transition = new dk.aau.cs.model.tapn.TimedTransition(drawingSurface.getNameGenerator().getNewTransitionName(guiModelToModel.get(c)));
574
575- TimedTransitionComponent pnObject = new TimedTransitionComponent(p.x, p.y, transition);
576+ TimedTransitionComponent pnObject = new TimedTransitionComponent(p.x, p.y, transition, lens);
577
578 guiModelToModel.get(c).add(transition);
579 c.addPetriNetObject(pnObject);
580@@ -207,7 +211,7 @@
581 TimeInterval.ZERO_INF
582 );
583
584- TimedInputArcComponent tiac = new TimedInputArcComponent(p, t, tia);
585+ TimedInputArcComponent tiac = new TimedInputArcComponent(p, t, tia, lens);
586
587 if (path != null) {
588 tiac.setArcPath(new ArcPath(tiac, path));
589@@ -563,7 +567,7 @@
590 }).start();
591 }
592
593- TabContent tab = new TabContent(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), loadedModel.isTimed(), loadedModel.isGame());
594+ TabContent tab = new TabContent(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), loadedModel.getLens());
595
596 tab.setInitialName(name);
597
598@@ -784,6 +788,9 @@
599 addGuiModel(template.model(), template.guiModel());
600 zoomLevels.put(template.model(), template.zoomer());
601 hasPositionalInfos.put(template.model(), template.getHasPositionalInfo());
602+ for(PetriNetObject o : template.guiModel().getPetriNetObjects()){
603+ o.setLens(this.lens);
604+ }
605 }
606
607 drawingSurface = new DrawingSurfaceImpl(new DataLayer(), this, managerRef);
608@@ -831,7 +838,7 @@
609 private TabContent(TimedArcPetriNetNetwork network, Collection<Template> templates, Iterable<TAPNQuery> tapnqueries) {
610 this(network, templates, tapnqueries, new TAPNLens(true, false));
611 }
612- private TabContent(TimedArcPetriNetNetwork network, Collection<Template> templates, Iterable<TAPNQuery> tapnqueries, TAPNLens lens) {
613+ public TabContent(TimedArcPetriNetNetwork network, Collection<Template> templates, Iterable<TAPNQuery> tapnqueries, TAPNLens lens) {
614 this(network, templates, lens);
615
616 setNetwork(network, templates);
617@@ -1133,9 +1140,15 @@
618 showEnabledTransitionsList(showEnabledTransitions);
619
620 this.setLeftComponent(animatorSplitPaneScroller);
621-
622 }
623
624+ private void hideTimedInformation(){
625+ if(!lens.isTimed()){
626+ animControlerBox.setVisible(false);
627+ }
628+
629+ }
630+
631 public void switchToEditorComponents() {
632
633 //Remove dummy
634@@ -1220,7 +1233,7 @@
635 }
636
637 private void createAnimationControlSidePanel() {
638- animControlerBox = new AnimationControlSidePanel(animator);
639+ animControlerBox = new AnimationControlSidePanel(animator, lens);
640 }
641
642 public AnimationHistoryList getAnimationHistorySidePanel() {
643@@ -1228,7 +1241,7 @@
644 }
645
646 private void createTransitionFireing() {
647- transitionFireing = new TransitionFireingComponent(CreateGui.getApp().isShowingDelayEnabledTransitions());
648+ transitionFireing = new TransitionFireingComponent(CreateGui.getApp().isShowingDelayEnabledTransitions(), lens);
649 }
650
651 public TransitionFireingComponent getTransitionFireingComponent() {
652@@ -1486,13 +1499,13 @@
653 }
654
655 private void createNewAndConvertUntimed() {
656- TabContent tab = duplicateTab(FeatureOption.TIME, false);
657+ TabContent tab = duplicateTab(new TAPNLens(false, lens.isGame()), "-untimed");
658 convertToUntimedTab(tab);
659 guiFrameControllerActions.ifPresent(o -> o.openTab(tab));
660 }
661
662 private void createNewAndConvertNonGame() {
663- TabContent tab = duplicateTab(FeatureOption.GAME, false);
664+ TabContent tab = duplicateTab(new TAPNLens(lens.isTimed(), false), "-nongame");
665 TabTransformer.removeGameInformation(tab);
666 guiFrameControllerActions.ifPresent(o -> o.openTab(tab));
667 }
668@@ -1512,13 +1525,31 @@
669 createNewAndConvertUntimed();
670 }
671 } else {
672- TabContent tab = duplicateTab(FeatureOption.TIME, isTime);
673+ TabContent tab = duplicateTab(new TAPNLens(true, lens.isGame()), "-timed");
674+ findAndRemoveAffectedQueries(tab);
675 guiFrameControllerActions.ifPresent(o -> o.openTab(tab));
676 }
677 updateFeatureText();
678 }
679 }
680
681+ private void findAndRemoveAffectedQueries(TabContent tab){
682+ List<TAPNQuery> queriesToRemove = new ArrayList<TAPNQuery>();
683+ for (TAPNQuery q : tab.queries()){
684+ if(q.hasUntimedOnlyProperties()){
685+ queriesToRemove.add(q);
686+ tab.removeQuery(q);
687+ }
688+ }
689+ String message = "The following queries will be removed in the conversion:";
690+ for(TAPNQuery q : queriesToRemove){
691+ message += "\n" + q.getName();
692+ }
693+ if(!queriesToRemove.isEmpty()){
694+ JOptionPane.showMessageDialog(this,message,"Information", JOptionPane.INFORMATION_MESSAGE);
695+ }
696+ }
697+
698 @Override
699 public void changeGameFeature(boolean isGame) {
700 if (isGame != lens.isGame()) {
701@@ -1534,7 +1565,7 @@
702 createNewAndConvertNonGame();
703 }
704 } else {
705- TabContent tab = duplicateTab(FeatureOption.GAME, isGame);
706+ TabContent tab = duplicateTab(new TAPNLens(lens.isTimed(), true), "-game");
707 guiFrameControllerActions.ifPresent(o -> o.openTab(tab));
708 }
709 updateFeatureText();
710@@ -1642,6 +1673,8 @@
711 drawingSurface().setCursor(Cursor.getPredefinedCursor(Cursor.DEFAULT_CURSOR));
712
713 animationmode = true; //XXX: Must be called after setGuiMode as guiMode uses last state,
714+ app.ifPresent(o->o.setStatusBarText(textforAnimation));
715+
716 } else {
717 JOptionPane.showMessageDialog(CreateGui.getApp(),
718 "You need at least one active template to enter simulation mode",
719@@ -1669,6 +1702,7 @@
720 // Undo/Redo is enabled based on undo/redo manager
721 getUndoManager().setUndoRedoStatus();
722 animationmode = false;
723+ app.ifPresent(o->o.setStatusBarText(textforDrawing));
724 }
725 animator.updateAnimationButtonsEnabled(); //Update stepBack/Forward
726 }
727@@ -1679,11 +1713,13 @@
728 @Override
729 public void setMode(Pipe.ElementType mode) {
730
731- app.ifPresent(o->o.updateMode(mode));
732+ CreateGui.guiMode = mode;
733+ changeStatusbarText(mode);
734
735 //Disable selection and deselect current selection
736 drawingSurface().getSelectionObject().clearSelection();
737 editorMode = mode;
738+ updateMode();
739 switch (mode) {
740 case ADDTOKEN:
741 setManager(new AbstractDrawingSurfaceManager() {
742@@ -1851,6 +1887,11 @@
743 app.ifPresent(o->o.setGUIMode(GuiFrame.GUIMode.draw));
744 app.ifPresent(o->setMode(Pipe.ElementType.SELECT));
745 }
746+ app.ifPresent(o->o.registerDrawingActions(getAvailableDrawActions()));
747+ app.ifPresent(o->o.registerAnimationActions(getAvailableSimActions()));
748+
749+ //TODO: this is a temporary implementation untill actions can be moved
750+ app.ifPresent(o->o.registerViewActions(List.of()));
751
752 }
753
754@@ -1947,8 +1988,7 @@
755 allTemplates(),
756 queriesOverwrite,
757 network().constants(),
758- lens.timed,
759- lens.game
760+ lens
761 );
762
763 tapnWriter.savePNML(outFile);
764@@ -2026,51 +2066,26 @@
765 drawingSurface().updatePreferredSize();
766 }
767
768- public TabContent duplicateTab(FeatureOption option, boolean isYes) {
769- NetWriter tapnWriter = new TimedArcPetriNetNetworkWriter(
770- network(),
771- allTemplates(),
772- queries(),
773- network().constants()
774- );
775-
776- option = isNetChanged(option, isYes) ? option : FeatureOption.TIME;
777-
778- try {
779- ByteArrayOutputStream outputStream = tapnWriter.savePNML();
780- String composedName = getTabTitle();
781- composedName = composedName.replace(".tapn", "");
782-
783- switch (option) {
784- case TIME:
785- composedName += isYes ? "-timed" : "-untimed";
786- break;
787- case GAME:
788- composedName += isYes ? "-game" : "-noGame";
789- break;
790- }
791-
792- if (isNetChanged(option, isYes)) {
793- return createNewTabFromInputStream(new ByteArrayInputStream(outputStream.toByteArray()), composedName, option, isYes);
794- } else {
795- return createNewTabFromInputStream(new ByteArrayInputStream(outputStream.toByteArray()), composedName);
796- }
797- } catch (Exception e1) {
798- e1.printStackTrace();
799- System.console().printf(e1.getMessage());
800- }
801- return null;
802- }
803-
804- private boolean isNetChanged(FeatureOption option, boolean isYes) {
805- switch (option) {
806- case TIME:
807- return lens.isTimed() != isYes;
808- case GAME:
809- return lens.isGame() != isYes;
810- default:
811- return false;
812+ public TabContent duplicateTab(TAPNLens overwriteLens, String appendName) {
813+ NetWriter tapnWriter = new TimedArcPetriNetNetworkWriter(
814+ network(),
815+ allTemplates(),
816+ queries(),
817+ network().constants(),
818+ overwriteLens
819+ );
820+
821+ try {
822+ ByteArrayOutputStream outputStream = tapnWriter.savePNML();
823+ String composedName = getTabTitle();
824+ composedName = composedName.replace(".tapn", "");
825+ composedName += appendName;
826+ return createNewTabFromInputStream(new ByteArrayInputStream(outputStream.toByteArray()), composedName);
827+ } catch (Exception e1) {
828+ Logger.log("Could not load model");
829+ e1.printStackTrace();
830 }
831+ return null;
832 }
833
834 class CanvasPlaceDrawController extends AbstractDrawingSurfaceManager {
835@@ -2651,4 +2666,216 @@
836 );
837 }
838 }
839+ public List<GuiAction> getAvailableDrawActions(){
840+ if(lens.isTimed()){
841+ return new ArrayList<>(Arrays.asList(selectAction, timedPlaceAction,transAction, timedArcAction, transportArcAction, inhibarcAction, tokenAction, deleteTokenAction));
842+ } else{
843+ return new ArrayList<>(Arrays.asList(selectAction, timedPlaceAction,transAction, timedArcAction, inhibarcAction, tokenAction, deleteTokenAction));
844+ }
845+ }
846+
847+ public List<GuiAction> getAvailableSimActions(){
848+ if(lens.isTimed()){
849+ return new ArrayList<>(Arrays.asList(timeAction, delayFireAction));
850+ } else{
851+ delayFireAction.setName("Fire");
852+ delayFireAction.setTooltip("Fire Selected Transition");
853+ return new ArrayList<>(Arrays.asList(delayFireAction));
854+ }
855+ }
856+
857+ private final GuiAction selectAction = new GuiAction("Select", "Select components (S)", "S", true) {
858+ public void actionPerformed(ActionEvent e) {
859+ setMode(Pipe.ElementType.SELECT);
860+ }
861+ };
862+ private final GuiAction annotationAction = new GuiAction("Annotation", "Add an annotation (N)", "N", true) {
863+ public void actionPerformed(ActionEvent e) {
864+ setMode(Pipe.ElementType.ANNOTATION);
865+ }
866+ };
867+ private final GuiAction inhibarcAction = new GuiAction("Inhibitor arc", "Add an inhibitor arc (I)", "I", true) {
868+ public void actionPerformed(ActionEvent e) {
869+ setMode(Pipe.ElementType.TAPNINHIBITOR_ARC);
870+ }
871+ };
872+ private final GuiAction transAction = new GuiAction("Transition", "Add a transition (T)", "T", true) {
873+ public void actionPerformed(ActionEvent e) {
874+ setMode(Pipe.ElementType.TAPNTRANS);
875+ }
876+ };
877+ private final GuiAction tokenAction = new GuiAction("Add token", "Add a token (+)", "typed +", true) {
878+ public void actionPerformed(ActionEvent e) {
879+ setMode(Pipe.ElementType.ADDTOKEN);
880+ }
881+ };
882+
883+ private final GuiAction deleteTokenAction = new GuiAction("Delete token", "Delete a token (-)", "typed -", true) {
884+ public void actionPerformed(ActionEvent e) {
885+ setMode(Pipe.ElementType.DELTOKEN);
886+ }
887+ };
888+ private final GuiAction timedPlaceAction = new GuiAction("Place", "Add a place (P)", "P", true) {
889+ public void actionPerformed(ActionEvent e) {
890+ setMode(Pipe.ElementType.TAPNPLACE);
891+ }
892+ };
893+
894+ private final GuiAction timedArcAction = new GuiAction("Arc", "Add an arc (A)", "A", true) {
895+ public void actionPerformed(ActionEvent e) {
896+ setMode(Pipe.ElementType.TAPNARC);
897+ }
898+ };
899+ private final GuiAction transportArcAction = new GuiAction("Transport arc", "Add a transport arc (R)", "R", true) {
900+ public void actionPerformed(ActionEvent e) {
901+ setMode(Pipe.ElementType.TRANSPORTARC);
902+ }
903+ };
904+ private final GuiAction timeAction = new GuiAction("Delay one time unit", "Let time pass one time unit", "W") {
905+ public void actionPerformed(ActionEvent e) {
906+ timeDelay();
907+ }
908+ };
909+ private final GuiAction delayFireAction = new GuiAction("Delay and fire", "Delay and fire selected transition", "F") {
910+ public void actionPerformed(ActionEvent e) {
911+ delayAndFire();
912+ }
913+ };
914+
915+ public void updateMode() {
916+ // deselect other actions
917+ selectAction.setSelected(CreateGui.guiMode == Pipe.ElementType.SELECT);
918+ transAction.setSelected(editorMode == Pipe.ElementType.TAPNTRANS);
919+ timedPlaceAction.setSelected(editorMode == Pipe.ElementType.TAPNPLACE);
920+ timedArcAction.setSelected(editorMode == Pipe.ElementType.TAPNARC);
921+ transportArcAction.setSelected(editorMode == Pipe.ElementType.TRANSPORTARC);
922+ inhibarcAction.setSelected(editorMode == Pipe.ElementType.TAPNINHIBITOR_ARC);
923+ tokenAction.setSelected(editorMode == Pipe.ElementType.ADDTOKEN);
924+ deleteTokenAction.setSelected(editorMode == Pipe.ElementType.DELTOKEN);
925+ annotationAction.setSelected(editorMode == Pipe.ElementType.ANNOTATION);
926+ }
927+ @Override
928+ public void updateEnabledActions(GuiFrame.GUIMode mode){
929+ switch(mode){
930+ case draw:
931+ selectAction.setEnabled(true);
932+ transAction.setEnabled(true);
933+ timedPlaceAction.setEnabled(true);
934+ timedArcAction.setEnabled(true);
935+ transportArcAction.setEnabled(true);
936+ inhibarcAction.setEnabled(true);
937+ tokenAction.setEnabled(true);
938+ deleteTokenAction.setEnabled(true);
939+ annotationAction.setEnabled(true);
940+ delayFireAction.setEnabled(false);
941+ timeAction.setEnabled(false);
942+ break;
943+ case noNet:
944+ selectAction.setEnabled(false);
945+ transAction.setEnabled(false);
946+ timedPlaceAction.setEnabled(false);
947+ timedArcAction.setEnabled(false);
948+ transportArcAction.setEnabled(false);
949+ inhibarcAction.setEnabled(false);
950+ tokenAction.setEnabled(false);
951+ deleteTokenAction.setEnabled(false);
952+ annotationAction.setEnabled(false);
953+ delayFireAction.setEnabled(false);
954+ timeAction.setEnabled(false);
955+ case animation:
956+ selectAction.setEnabled(false);
957+ transAction.setEnabled(false);
958+ timedPlaceAction.setEnabled(false);
959+ timedArcAction.setEnabled(false);
960+ transportArcAction.setEnabled(false);
961+ inhibarcAction.setEnabled(false);
962+ tokenAction.setEnabled(false);
963+ deleteTokenAction.setEnabled(false);
964+ annotationAction.setEnabled(false);
965+ delayFireAction.setEnabled(true);
966+ if(lens.isTimed())
967+ timeAction.setEnabled(true);
968+ break;
969+ }
970+ }
971+
972+
973+ public static final String textforDrawing = "Drawing Mode: Click on a button to start adding components to the Editor";
974+ public static final String textforPlace = "Place Mode: Right click on a place to see menu options ";
975+ public static final String textforTAPNPlace = "Place Mode: Right click on a place to see menu options ";
976+ public static final String textforTrans = "Transition Mode: Right click on a transition to see menu options [Mouse wheel -> rotate]";
977+ public static final String textforTimedTrans = "Timed Transition Mode: Right click on a transition to see menu options [Mouse wheel -> rotate]";
978+ public static final String textforAddtoken = "Add Token Mode: Click on a place to add a token";
979+ public static final String textforDeltoken = "Delete Token Mode: Click on a place to delete a token ";
980+ public static final String textforAnimation = "Simulation Mode: Red transitions are enabled, click a transition to fire it";
981+ public static final String textforArc = "Arc Mode: Right click on an arc to see menu options ";
982+ public static final String textforTransportArc = "Transport Arc Mode: Right click on an arc to see menu options ";
983+ public static final String textforInhibArc = "Inhibitor Mode: Right click on an arc to see menu options ";
984+ public static final String textforMove = "Select Mode: Click/drag to select objects; drag to move them";
985+ public static final String textforAnnotation = "Annotation Mode: Right click on an annotation to see menu options; double click to edit";
986+ public static final String textforDrag = "Drag Mode";
987+
988+ public void changeStatusbarText(Pipe.ElementType type) {
989+ switch (type) {
990+ case PLACE:
991+ app.ifPresent(o13 -> o13.setStatusBarText(textforPlace));
992+ break;
993+
994+ case TAPNPLACE:
995+ app.ifPresent(o12 -> o12.setStatusBarText(textforTAPNPlace));
996+ break;
997+
998+ case IMMTRANS:
999+ case TAPNTRANS:
1000+ app.ifPresent(o11 -> o11.setStatusBarText(textforTrans));
1001+ break;
1002+
1003+ case TIMEDTRANS:
1004+ app.ifPresent(o10 -> o10.setStatusBarText(textforTimedTrans));
1005+ break;
1006+
1007+ case ARC:
1008+ case TAPNARC:
1009+ app.ifPresent(o9 -> o9.setStatusBarText(textforArc));
1010+ break;
1011+
1012+ case TRANSPORTARC:
1013+ app.ifPresent(o8 -> o8.setStatusBarText(textforTransportArc));
1014+ break;
1015+
1016+ case TAPNINHIBITOR_ARC:
1017+ case INHIBARC:
1018+ app.ifPresent(o7 -> o7.setStatusBarText(textforInhibArc));
1019+ break;
1020+
1021+ case ADDTOKEN:
1022+ app.ifPresent(o6 -> o6.setStatusBarText(textforAddtoken));
1023+ break;
1024+
1025+ case DELTOKEN:
1026+ app.ifPresent(o5 -> o5.setStatusBarText(textforDeltoken));
1027+ break;
1028+
1029+ case SELECT:
1030+ app.ifPresent(o4 -> o4.setStatusBarText(textforMove));
1031+ break;
1032+
1033+ case DRAW:
1034+ app.ifPresent(o3 -> o3.setStatusBarText(textforDrawing));
1035+ break;
1036+
1037+ case ANNOTATION:
1038+ app.ifPresent(o2 -> o2.setStatusBarText(textforAnnotation));
1039+ break;
1040+
1041+ case DRAG:
1042+ app.ifPresent(o1 -> o1.setStatusBarText(textforDrag));
1043+ break;
1044+
1045+ default:
1046+ app.ifPresent(o->o.setStatusBarText("To-do (textfor" + type));
1047+ break;
1048+ }
1049+ }
1050+
1051 }
1052
1053=== modified file 'src/dk/aau/cs/gui/TabContentActions.java'
1054--- src/dk/aau/cs/gui/TabContentActions.java 2020-08-11 11:33:28 +0000
1055+++ src/dk/aau/cs/gui/TabContentActions.java 2020-08-19 11:36:17 +0000
1056@@ -1,5 +1,6 @@
1057 package dk.aau.cs.gui;
1058
1059+import pipe.gui.GuiFrame;
1060 import pipe.gui.GuiFrameActions;
1061 import pipe.gui.Pipe;
1062 import pipe.gui.SafeGuiFrameActions;
1063@@ -89,7 +90,10 @@
1064
1065 void setResizeingDefault();
1066
1067+ void updateEnabledActions(GuiFrame.GUIMode mode);
1068+
1069 void changeTimeFeature(boolean isTime);
1070
1071 void changeGameFeature(boolean isGame);
1072+
1073 }
1074
1075=== modified file 'src/dk/aau/cs/gui/TabTransformer.java'
1076--- src/dk/aau/cs/gui/TabTransformer.java 2020-08-10 09:25:25 +0000
1077+++ src/dk/aau/cs/gui/TabTransformer.java 2020-08-19 11:36:17 +0000
1078@@ -51,12 +51,15 @@
1079 DataLayer guiModel = template.guiModel();
1080 Place guiSource = guiModel.getPlaceByName(arc.getSource().getName());
1081 Transition guiTarget = guiModel.getTransitionByName(arc.getTarget().getName());
1082- TimedInputArcComponent newArc = new TimedInputArcComponent(new TimedOutputArcComponent(
1083- guiSource,
1084+ TimedInputArcComponent newArc = new TimedInputArcComponent(
1085+ new TimedOutputArcComponent(
1086+ guiSource,
1087 guiTarget,
1088 arc.getWeight().value(),
1089 arc.getSource().getName() + "_to_" + arc.getTarget().getName()
1090- ));
1091+ ),
1092+ tab.getLens()
1093+ );
1094
1095 // Build ArcPath
1096 Place oldGuiSource = guiModel.getPlaceByName(arc.getSource().getName());
1097
1098=== modified file 'src/dk/aau/cs/gui/components/EnabledTransitionsList.java'
1099--- src/dk/aau/cs/gui/components/EnabledTransitionsList.java 2020-07-20 12:17:24 +0000
1100+++ src/dk/aau/cs/gui/components/EnabledTransitionsList.java 2020-08-19 11:36:17 +0000
1101@@ -20,6 +20,7 @@
1102 import org.jetbrains.annotations.NotNull;
1103 import pipe.dataLayer.Template;
1104 import pipe.gui.CreateGui;
1105+import pipe.gui.SimulationControl;
1106 import pipe.gui.graphicElements.Transition;
1107 import pipe.gui.graphicElements.tapn.TimedTransitionComponent;
1108 //TODO clean up!!!
1109@@ -63,7 +64,7 @@
1110 }
1111
1112 public void reInitDone(){
1113- if(CreateGui.getCurrentTab().getDelayEnabledTransitionControl().isRandomTransitionMode()){
1114+ if(SimulationControl.getInstance().isRandomTransitionMode()){
1115 selectRandom();
1116 return;
1117 }
1118@@ -125,7 +126,7 @@
1119
1120 public String toString(boolean showIntervals) {
1121
1122- String interval = transition.getDInterval() == null || !showIntervals ? "" : transition.getDInterval().toString() + " ";
1123+ String interval = transition.getDInterval() == null || !showIntervals || !transition.isTimed() ? "" : transition.getDInterval().toString() + " ";
1124
1125 String transitionName = getTransition().getName();
1126 if(isShared()){
1127
1128=== modified file 'src/dk/aau/cs/gui/components/TransitionFireingComponent.java'
1129--- src/dk/aau/cs/gui/components/TransitionFireingComponent.java 2020-07-13 13:58:47 +0000
1130+++ src/dk/aau/cs/gui/components/TransitionFireingComponent.java 2020-08-19 11:36:17 +0000
1131@@ -10,6 +10,7 @@
1132 import javax.swing.JButton;
1133 import javax.swing.JPanel;
1134
1135+import dk.aau.cs.gui.TabContent;
1136 import pipe.dataLayer.Template;
1137 import pipe.gui.AnimationSettingsDialog;
1138 import pipe.gui.DelayEnabledTransitionControl;
1139@@ -22,12 +23,12 @@
1140 private final EnabledTransitionsList enabledTransitionsList;
1141 private final JButton fireButton;
1142 private final JButton settingsButton;
1143+ private final TabContent.TAPNLens lens;
1144
1145- public TransitionFireingComponent(boolean showDelayEnabledTransitions) {
1146+ public TransitionFireingComponent(boolean showDelayEnabledTransitions, TabContent.TAPNLens lens) {
1147 super(new GridBagLayout());
1148-
1149 enabledTransitionsList = new EnabledTransitionsList();
1150-
1151+ this.lens = lens;
1152 this.setBorder(
1153 BorderFactory.createCompoundBorder(
1154 BorderFactory.createTitledBorder("Enabled Transitions"),
1155@@ -44,7 +45,7 @@
1156
1157 settingsButton = new JButton("Settings");
1158 settingsButton.setPreferredSize(new Dimension(0, settingsButton.getPreferredSize().height)); //Make the two buttons equal in size
1159- settingsButton.addActionListener(e -> AnimationSettingsDialog.showAnimationSettings());
1160+ settingsButton.addActionListener(e -> AnimationSettingsDialog.showAnimationSettings(lens));
1161
1162 fireButton = new JButton("Delay & Fire");
1163 fireButton.setPreferredSize(new Dimension(0, fireButton.getPreferredSize().height)); //Make the two buttons equal in size
1164@@ -125,7 +126,10 @@
1165 fireButton.setToolTipText(SIMULATE_ACTIVATED_TOOL_TIP);
1166 }
1167 } else { //If random simulation is not enabled.
1168- fireButton.setText(CreateGui.getApp().isShowingDelayEnabledTransitions() ? "Delay & Fire" : "Fire");
1169+ fireButton.setText(CreateGui.getApp().isShowingDelayEnabledTransitions() ? "Delay & Fire" : "Fire");
1170+ if(!lens.isTimed()){
1171+ fireButton.setText("Fire");
1172+ }
1173
1174 if(enabledTransitionsList.getNumberOfTransitions() == 0){
1175 fireButton.setEnabled(false);
1176
1177=== modified file 'src/dk/aau/cs/io/LoadedModel.java'
1178--- src/dk/aau/cs/io/LoadedModel.java 2020-08-04 08:53:19 +0000
1179+++ src/dk/aau/cs/io/LoadedModel.java 2020-08-19 11:36:17 +0000
1180@@ -3,6 +3,7 @@
1181 import java.util.Collection;
1182 import java.util.List;
1183
1184+import dk.aau.cs.gui.TabContent;
1185 import dk.aau.cs.io.batchProcessing.LoadedBatchProcessingModel;
1186 import pipe.dataLayer.TAPNQuery;
1187 import pipe.dataLayer.Template;
1188@@ -13,23 +14,21 @@
1189 private final Collection<Template> templates;
1190 private final Collection<TAPNQuery> queries;
1191 private final TimedArcPetriNetNetwork network;
1192- private final boolean isTimed;
1193- private final boolean isGame;
1194 private final Collection<String> messages;
1195-
1196- public LoadedModel(TimedArcPetriNetNetwork network, Collection<Template> templates, Collection<TAPNQuery> queries, Collection<String> messages){
1197- this(network, templates, queries, messages, true, false);
1198+ private final TabContent.TAPNLens lens;
1199+
1200+ public LoadedModel(TimedArcPetriNetNetwork network, Collection<Template> templates, Collection<TAPNQuery> queries, Collection<String> messages){
1201+ this(network, templates, queries, messages, TabContent.TAPNLens.Default);
1202 }
1203 public LoadedModel(TimedArcPetriNetNetwork network, Collection<Template> templates, Collection<TAPNQuery> queries){
1204- this(network, templates, queries, List.of(), true, false);
1205+ this(network, templates, queries, List.of(), TabContent.TAPNLens.Default);
1206 }
1207
1208- public LoadedModel(TimedArcPetriNetNetwork network, Collection<Template> templates, Collection<TAPNQuery> queries, Collection<String> messages, boolean isTimed, boolean isGame){
1209+ public LoadedModel(TimedArcPetriNetNetwork network, Collection<Template> templates, Collection<TAPNQuery> queries, Collection<String> messages, TabContent.TAPNLens lens){
1210 this.templates = templates;
1211 this.network = network;
1212 this.queries = queries;
1213- this.isTimed = isTimed;
1214- this.isGame = isGame;
1215+ this.lens = lens;
1216 this.messages = messages;
1217 }
1218
1219@@ -38,12 +37,15 @@
1220 public TimedArcPetriNetNetwork network(){ return network; }
1221 public Collection<String> getMessages() { return messages; }
1222
1223+ public TabContent.TAPNLens getLens(){
1224+ return lens;
1225+ }
1226
1227 public boolean isTimed() {
1228- return isTimed;
1229+ return lens.isTimed();
1230 }
1231 public boolean isGame() {
1232- return isGame;
1233+ return lens.isGame();
1234 }
1235
1236 }
1237\ No newline at end of file
1238
1239=== modified file 'src/dk/aau/cs/io/PNMLoader.java'
1240--- src/dk/aau/cs/io/PNMLoader.java 2020-07-20 09:53:59 +0000
1241+++ src/dk/aau/cs/io/PNMLoader.java 2020-08-19 11:36:17 +0000
1242@@ -15,6 +15,7 @@
1243 import javax.xml.parsers.DocumentBuilderFactory;
1244 import javax.xml.parsers.ParserConfigurationException;
1245
1246+import dk.aau.cs.gui.TabContent;
1247 import org.w3c.dom.Document;
1248 import org.w3c.dom.Element;
1249 import org.w3c.dom.Node;
1250@@ -51,8 +52,10 @@
1251 import pipe.gui.graphicElements.tapn.TimedTransitionComponent;
1252
1253 public class PNMLoader {
1254-
1255- enum GraphicsType { Position, Offset }
1256+
1257+ private final TabContent.TAPNLens lens = new TabContent.TAPNLens(false, false);
1258+
1259+ enum GraphicsType { Position, Offset }
1260
1261 private final NameGenerator nameGenerator = new NameGenerator();
1262 private final IdResolver idResolver = new IdResolver();
1263@@ -192,7 +195,7 @@
1264
1265 if(isNetDrawable()){
1266 //We parse the id as both the name and id as in tapaal name = id, and name/id has to be unique
1267- TimedPlaceComponent placeComponent = new TimedPlaceComponent(position.x, position.y, id, name.point.x, name.point.y);
1268+ TimedPlaceComponent placeComponent = new TimedPlaceComponent(position.x, position.y, id, name.point.x, name.point.y, lens);
1269 placeComponent.setUnderlyingPlace(place);
1270 template.guiModel().addPetriNetObject(placeComponent);
1271 }
1272@@ -236,8 +239,7 @@
1273 if(isNetDrawable()){
1274 TimedTransitionComponent transitionComponent =
1275 //We parse the id as both the name and id as in tapaal name = id, and name/id has to be unique
1276- new TimedTransitionComponent(position.x, position.y, id, name.point.x, name.point.y,
1277- true, false, 0, 0);
1278+ new TimedTransitionComponent(position.x, position.y, id, name.point.x, name.point.y, true, false, 0, 0, lens);
1279 transitionComponent.setUnderlyingTransition(transition);
1280 template.guiModel().addPetriNetObject(transitionComponent);
1281 }
1282@@ -423,7 +425,7 @@
1283 TimedInputArcComponent arc = null;
1284
1285 if(isNetDrawable()){
1286- arc = new TimedInputArcComponent(new TimedOutputArcComponent(source, target, weight, arcId));
1287+ arc = new TimedInputArcComponent(new TimedOutputArcComponent(source, target, weight, arcId), lens);
1288 arc.setUnderlyingArc(inputArc);
1289
1290 template.guiModel().addPetriNetObject(arc);
1291
1292=== modified file 'src/dk/aau/cs/io/TapnLegacyXmlLoader.java'
1293--- src/dk/aau/cs/io/TapnLegacyXmlLoader.java 2020-08-04 08:53:19 +0000
1294+++ src/dk/aau/cs/io/TapnLegacyXmlLoader.java 2020-08-19 11:36:17 +0000
1295@@ -13,6 +13,7 @@
1296 import javax.xml.parsers.DocumentBuilderFactory;
1297 import javax.xml.parsers.ParserConfigurationException;
1298
1299+import dk.aau.cs.gui.TabContent;
1300 import org.w3c.dom.Document;
1301 import org.w3c.dom.Element;
1302 import org.w3c.dom.Node;
1303@@ -83,9 +84,10 @@
1304 private final IdResolver idResolver = new IdResolver();
1305
1306 private final Collection<String> messages = new ArrayList<>(10);
1307-
1308-
1309- public TapnLegacyXmlLoader() {}
1310+ private final TabContent.TAPNLens lens = new TabContent.TAPNLens(true, false);
1311+
1312+
1313+ public TapnLegacyXmlLoader() {}
1314
1315 public LoadedModel load(InputStream file) throws FormatException {
1316 Require.that(file != null, "file must be non-null and exist");
1317@@ -278,7 +280,7 @@
1318 PlaceTransitionObject targetIn,
1319 int _endx, int _endy) throws FormatException {
1320
1321- TimedInputArcComponent tempArc = new TimedInputArcComponent(new TimedOutputArcComponent(sourceIn, targetIn, 1, idInput));
1322+ TimedInputArcComponent tempArc = new TimedInputArcComponent(new TimedOutputArcComponent(sourceIn, targetIn, 1, idInput), lens);
1323
1324 TimedPlace place = tapn.getPlaceByName(sourceIn.getName());
1325 TimedTransition transition = tapn.getTransitionByName(targetIn.getName());
1326@@ -523,7 +525,7 @@
1327 TimedTransitionComponent transition = new TimedTransitionComponent(
1328 positionXInput, positionYInput, idInput,
1329 nameOffsetXInput, nameOffsetYInput, timedTransition,
1330- infiniteServer, angle, priority);
1331+ infiniteServer, angle, priority, lens);
1332 transition.setUnderlyingTransition(t);
1333 guiModel.addPetriNetObject(transition);
1334 tapn.add(t);
1335@@ -556,7 +558,7 @@
1336 }
1337 idResolver.add(tapn.name(), idInput, nameInput);
1338
1339- TimedPlaceComponent place = new TimedPlaceComponent(positionXInput, positionYInput, idInput, nameOffsetXInput, nameOffsetYInput);
1340+ TimedPlaceComponent place = new TimedPlaceComponent(positionXInput, positionYInput, idInput, nameOffsetXInput, nameOffsetYInput, lens);
1341
1342 LocalTimedPlace p = new LocalTimedPlace(nameInput, TimeInvariant.parse(invariant, constants));
1343 tapn.add(p);
1344@@ -615,9 +617,7 @@
1345
1346 } else {
1347 if (type.equals("timed")) {
1348- tempArc = parseAndAddTimedInputArc(idInput, taggedArc,
1349- inscriptionTempStorage, sourceIn, targetIn,
1350- aEndx, aEndy);
1351+ tempArc = parseAndAddTimedInputArc(idInput, taggedArc, inscriptionTempStorage, sourceIn, targetIn, aEndx, aEndy);
1352
1353 } else if (type.equals("transport")) {
1354 tempArc = parseAndAddTransportArc(idInput, taggedArc,
1355
1356=== modified file 'src/dk/aau/cs/io/TapnXmlLoader.java'
1357--- src/dk/aau/cs/io/TapnXmlLoader.java 2020-08-10 06:46:22 +0000
1358+++ src/dk/aau/cs/io/TapnXmlLoader.java 2020-08-19 11:36:17 +0000
1359@@ -14,6 +14,7 @@
1360 import javax.xml.parsers.ParserConfigurationException;
1361
1362 import dk.aau.cs.debug.Logger;
1363+import dk.aau.cs.gui.TabContent;
1364 import org.w3c.dom.Document;
1365 import org.w3c.dom.Element;
1366 import org.w3c.dom.Node;
1367@@ -26,10 +27,7 @@
1368 import pipe.gui.CreateGui;
1369 import pipe.gui.Pipe;
1370 import pipe.gui.Zoomer;
1371-import pipe.gui.graphicElements.AnnotationNote;
1372-import pipe.gui.graphicElements.Arc;
1373-import pipe.gui.graphicElements.Place;
1374-import pipe.gui.graphicElements.PlaceTransitionObject;
1375+import pipe.gui.graphicElements.*;
1376 import pipe.gui.graphicElements.tapn.TimedInhibitorArcComponent;
1377 import pipe.gui.graphicElements.tapn.TimedInputArcComponent;
1378 import pipe.gui.graphicElements.tapn.TimedOutputArcComponent;
1379@@ -73,9 +71,7 @@
1380 private final IdResolver idResolver = new IdResolver();
1381 private final Collection<String> messages = new ArrayList<>(10);
1382
1383- private boolean isTimed;
1384- private boolean isGame;
1385- private boolean isUncontrollable = false;
1386+ private TabContent.TAPNLens lens;
1387
1388 public TapnXmlLoader() {
1389
1390@@ -118,6 +114,8 @@
1391
1392 private LoadedModel parse(Document doc) throws FormatException {
1393 idResolver.clear();
1394+
1395+ parseFeature(doc);
1396
1397 ConstantStore constants = new ConstantStore(parseConstants(doc));
1398
1399@@ -133,9 +131,9 @@
1400
1401 parseBound(doc, network);
1402
1403- parseFeature(doc, network);
1404-
1405- return new LoadedModel(network, templates, queries,messages, isTimed, isGame);
1406+
1407+
1408+ return new LoadedModel(network, templates, queries,messages, lens);
1409 }
1410
1411 private void parseBound(Document doc, TimedArcPetriNetNetwork network){
1412@@ -145,27 +143,16 @@
1413 }
1414 }
1415
1416- private void parseFeature(Document doc, TimedArcPetriNetNetwork network) {
1417- boolean networkIsTimed = !network.isUntimed();
1418-
1419+ private void parseFeature(Document doc) {
1420 if (doc.getElementsByTagName("feature").getLength() > 0) {
1421 NodeList nodeList = doc.getElementsByTagName("feature");
1422
1423- isTimed = Boolean.parseBoolean(nodeList.item(0).getAttributes().getNamedItem("isTimed").getNodeValue());
1424- isGame = Boolean.parseBoolean(nodeList.item(0).getAttributes().getNamedItem("isGame").getNodeValue());
1425-
1426- if (networkIsTimed && !isTimed) {
1427- isTimed = true;
1428- Logger.log("The net contains time features. The entire net will be changed to include time features.");
1429- }
1430- if (isUncontrollable && !isGame) {
1431- isGame = true;
1432- Logger.log("The net contains game features. The entire net will be changed to include game features.");
1433-
1434- }
1435+ var isTimed = Boolean.parseBoolean(nodeList.item(0).getAttributes().getNamedItem("isTimed").getNodeValue());
1436+ var isGame = Boolean.parseBoolean(nodeList.item(0).getAttributes().getNamedItem("isGame").getNodeValue());
1437+
1438+ lens = new TabContent.TAPNLens(isTimed, isGame);
1439 } else {
1440- isTimed = networkIsTimed;
1441- isGame = isUncontrollable;
1442+ lens = new TabContent.TAPNLens(true, false);
1443 }
1444 }
1445
1446@@ -380,9 +367,6 @@
1447 boolean isUrgent = Boolean.parseBoolean(transition.getAttribute("urgent"));
1448
1449 String player = transition.getAttribute("player");
1450- if (player.length() > 0 && player.equals("1")) {
1451- isUncontrollable = true;
1452- }
1453
1454 idResolver.add(tapn.name(), idInput, nameInput);
1455
1456@@ -417,7 +401,7 @@
1457 TimedTransitionComponent transitionComponent = new TimedTransitionComponent(
1458 positionXInput, positionYInput, idInput,
1459 nameOffsetXInput, nameOffsetYInput, true,
1460- infiniteServer, angle, priority);
1461+ infiniteServer, angle, priority, lens);
1462 transitionComponent.setUnderlyingTransition(t);
1463
1464 if (!displayName){
1465@@ -468,7 +452,7 @@
1466 }
1467 }
1468 nameGenerator.updateIndicesForAllModels(nameInput);
1469- TimedPlaceComponent placeComponent = new TimedPlaceComponent(positionXInput, positionYInput, idInput, nameOffsetXInput, nameOffsetYInput);
1470+ TimedPlaceComponent placeComponent = new TimedPlaceComponent(positionXInput, positionYInput, idInput, nameOffsetXInput, nameOffsetYInput, lens);
1471 placeComponent.setUnderlyingPlace(p);
1472
1473 if (!displayName){
1474@@ -646,7 +630,8 @@
1475 String inscriptionTempStorage, PlaceTransitionObject sourceIn,
1476 PlaceTransitionObject targetIn,
1477 int _endx, int _endy, Template template, ConstantStore constants, Weight weight) throws FormatException {
1478- TimedInputArcComponent tempArc = new TimedInputArcComponent(new TimedOutputArcComponent(sourceIn, targetIn, 1, idInput));
1479+
1480+ TimedInputArcComponent tempArc = new TimedInputArcComponent(new TimedOutputArcComponent(sourceIn, targetIn, 1, idInput), lens);
1481
1482 TimedPlace place = template.model().getPlaceByName(sourceIn.getName());
1483 TimedTransition transition = template.model().getTransitionByName(targetIn.getName());
1484
1485=== modified file 'src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java'
1486--- src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java 2020-08-10 06:46:22 +0000
1487+++ src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java 2020-08-19 11:36:17 +0000
1488@@ -17,6 +17,7 @@
1489 import javax.xml.transform.dom.DOMSource;
1490 import javax.xml.transform.stream.StreamResult;
1491
1492+import dk.aau.cs.gui.TabContent;
1493 import org.w3c.dom.Attr;
1494 import org.w3c.dom.DOMException;
1495 import org.w3c.dom.Document;
1496@@ -55,18 +56,19 @@
1497 private final Iterable<TAPNQuery> queries;
1498 private final Iterable<Constant> constants;
1499 private final TimedArcPetriNetNetwork network;
1500- private boolean isTimed;
1501- private boolean isGame;
1502+ private final TabContent.TAPNLens lens;
1503
1504 public TimedArcPetriNetNetworkWriter(
1505 TimedArcPetriNetNetwork network,
1506 Iterable<Template> templates,
1507 Iterable<TAPNQuery> queries,
1508- Iterable<Constant> constants) {
1509+ Iterable<Constant> constants
1510+ ) {
1511 this.network = network;
1512 this.templates = templates;
1513 this.queries = queries;
1514 this.constants = constants;
1515+ this.lens = TabContent.TAPNLens.Default;
1516 }
1517
1518 public TimedArcPetriNetNetworkWriter(
1519@@ -74,14 +76,13 @@
1520 Iterable<Template> templates,
1521 Iterable<TAPNQuery> queries,
1522 Iterable<Constant> constants,
1523- boolean isTimed,
1524- boolean isGame) {
1525+ TabContent.TAPNLens lens
1526+ ) {
1527 this.network = network;
1528 this.templates = templates;
1529 this.queries = queries;
1530 this.constants = constants;
1531- this.isTimed = isTimed;
1532- this.isGame = isGame;
1533+ this.lens = lens;
1534 }
1535
1536 public ByteArrayOutputStream savePNML() throws IOException, ParserConfigurationException, DOMException, TransformerConfigurationException, TransformerException {
1537@@ -161,10 +162,10 @@
1538 private void appendFeature(Document document, Element root) {
1539 String isTimed = "true";
1540 String isGame = "true";
1541- if (!this.isTimed) {
1542+ if (!lens.isTimed()) {
1543 isTimed = "false";
1544 }
1545- if (!this.isGame) {
1546+ if (!lens.isGame()) {
1547 isGame = "false";
1548 }
1549
1550
1551=== modified file 'src/dk/aau/cs/verification/TAPNComposer.java'
1552--- src/dk/aau/cs/verification/TAPNComposer.java 2020-08-10 06:46:22 +0000
1553+++ src/dk/aau/cs/verification/TAPNComposer.java 2020-08-19 11:36:17 +0000
1554@@ -4,6 +4,7 @@
1555 import java.util.HashSet;
1556 import java.util.Map.Entry;
1557
1558+import dk.aau.cs.gui.TabContent;
1559 import pipe.dataLayer.DataLayer;
1560 import pipe.gui.ExportBatchDialog;
1561 import pipe.gui.graphicElements.Arc;
1562@@ -45,8 +46,9 @@
1563 private HashSet<String> processedSharedObjects;
1564 private HashMap<TimedArcPetriNet, DataLayer> guiModels;
1565 private DataLayer composedGuiModel;
1566+ private final TabContent.TAPNLens lens = TabContent.TAPNLens.Default;
1567
1568- public TAPNComposer(Messenger messenger, HashMap<TimedArcPetriNet, DataLayer> guiModels, boolean singleComponentNoPrefix, boolean inlineConstants){
1569+ public TAPNComposer(Messenger messenger, HashMap<TimedArcPetriNet, DataLayer> guiModels, boolean singleComponentNoPrefix, boolean inlineConstants){
1570 this.messenger = messenger;
1571
1572 HashMap<TimedArcPetriNet, DataLayer> newGuiModels = new HashMap<TimedArcPetriNet, DataLayer>();
1573@@ -185,8 +187,9 @@
1574 oldPlace.getPositionY(),
1575 oldPlace.getId(),
1576 oldPlace.getNameOffsetX(),
1577- oldPlace.getNameOffsetY()
1578- );
1579+ oldPlace.getNameOffsetY(),
1580+ lens
1581+ );
1582 newPlace.setUnderlyingPlace(constructedPlace);
1583 newPlace.setName(uniquePlaceName);
1584 guiModel.addPetriNetObject(newPlace);
1585@@ -227,13 +230,14 @@
1586 // Gui work
1587 if (this.guiModels != null) {
1588 Place oldPlace = currentGuiModel.getPlaceByName(timedPlace.name());
1589- TimedPlaceComponent newPlace = new TimedPlaceComponent(
1590- oldPlace.getPositionX() + offset.value1() * greatestWidth,
1591- oldPlace.getPositionY() + offset.value2() * greatestHeight,
1592- oldPlace.getId(),
1593- oldPlace.getNameOffsetX(),
1594- oldPlace.getNameOffsetY()
1595- );
1596+ TimedPlaceComponent newPlace = new TimedPlaceComponent(
1597+ oldPlace.getPositionX() + offset.value1() * greatestWidth,
1598+ oldPlace.getPositionY() + offset.value2() * greatestHeight,
1599+ oldPlace.getId(),
1600+ oldPlace.getNameOffsetX(),
1601+ oldPlace.getNameOffsetY(),
1602+ lens
1603+ );
1604 newPlace.setGuiModel(guiModel);
1605
1606 newPlace.setUnderlyingPlace(place);
1607@@ -284,15 +288,17 @@
1608 if (this.guiModels != null) {
1609 Transition oldTransition = currentGuiModel.getTransitionByName(timedTransition.name());
1610 TimedTransitionComponent newTransition = new TimedTransitionComponent(
1611- oldTransition.getPositionX() + offset.value1() * greatestWidth,
1612- oldTransition.getPositionY() + offset.value2() * greatestHeight,
1613- oldTransition.getId(),
1614- oldTransition.getNameOffsetX(),
1615- oldTransition.getNameOffsetY(),
1616- true,
1617- false,
1618- oldTransition.getAngle(),
1619- 0);
1620+ oldTransition.getPositionX() + offset.value1() * greatestWidth,
1621+ oldTransition.getPositionY() + offset.value2() * greatestHeight,
1622+ oldTransition.getId(),
1623+ oldTransition.getNameOffsetX(),
1624+ oldTransition.getNameOffsetY(),
1625+ true,
1626+ false,
1627+ oldTransition.getAngle(),
1628+ 0,
1629+ lens
1630+ );
1631 newTransition.setUnderlyingTransition(transition);
1632 newTransition.setName(uniqueTransitionName);
1633 guiModel.addPetriNetObject(newTransition);
1634@@ -380,12 +386,14 @@
1635 Place guiSource = guiModel.getPlaceByName(mapping.map(sourceTemplate, arc.source().name()));
1636 Transition guiTarget = guiModel.getTransitionByName(mapping.map(targetTemplate, arc.destination().name()));
1637
1638- TimedInputArcComponent newArc = new TimedInputArcComponent(new TimedOutputArcComponent(
1639- guiSource,
1640- guiTarget,
1641- arc.getWeight().value(),
1642- mapping.map(sourceTemplate, arc.source().name()) + "_to_" + mapping.map(targetTemplate, arc.destination().name())
1643- )
1644+ TimedInputArcComponent newArc = new TimedInputArcComponent(
1645+ new TimedOutputArcComponent(
1646+ guiSource,
1647+ guiTarget,
1648+ arc.getWeight().value(),
1649+ mapping.map(sourceTemplate, arc.source().name()) + "_to_" + mapping.map(targetTemplate, arc.destination().name())
1650+ ),
1651+ lens
1652 );
1653
1654 // Build ArcPath
1655
1656=== modified file 'src/pipe/dataLayer/TAPNQuery.java'
1657--- src/pipe/dataLayer/TAPNQuery.java 2019-03-22 11:36:50 +0000
1658+++ src/pipe/dataLayer/TAPNQuery.java 2020-08-19 11:36:17 +0000
1659@@ -1,11 +1,8 @@
1660 package pipe.dataLayer;
1661
1662+import dk.aau.cs.TCTL.*;
1663 import pipe.dataLayer.TAPNQuery.QueryCategory;
1664 import pipe.gui.widgets.InclusionPlaces;
1665-import dk.aau.cs.TCTL.TCTLAFNode;
1666-import dk.aau.cs.TCTL.TCTLAbstractProperty;
1667-import dk.aau.cs.TCTL.TCTLEFNode;
1668-import dk.aau.cs.TCTL.TCTLEGNode;
1669 import dk.aau.cs.translations.ReductionOption;
1670 import dk.aau.cs.verification.QueryType;
1671
1672@@ -416,4 +413,13 @@
1673 public AlgorithmOption getAlgorithmOption(){
1674 return this.algorithmOption;
1675 }
1676+
1677+ public boolean hasUntimedOnlyProperties(){
1678+ if(!(property instanceof TCTLAFNode || property instanceof TCTLAGNode || property instanceof TCTLEFNode || property instanceof TCTLEGNode)){
1679+ return true;
1680+ } else if(property.hasNestedPathQuantifiers()){
1681+ return true;
1682+ }
1683+ return false;
1684+ }
1685 }
1686
1687=== modified file 'src/pipe/gui/AnimationControlSidePanel.java'
1688--- src/pipe/gui/AnimationControlSidePanel.java 2020-07-16 09:52:11 +0000
1689+++ src/pipe/gui/AnimationControlSidePanel.java 2020-08-19 11:36:17 +0000
1690@@ -21,6 +21,7 @@
1691 import javax.swing.border.EmptyBorder;
1692 import javax.swing.text.AbstractDocument;
1693
1694+import dk.aau.cs.gui.TabContent;
1695 import dk.aau.cs.util.Require;
1696 import net.tapaal.swinghelpers.DecimalOnlyDocumentFilter;
1697 import dk.aau.cs.gui.components.NonsearchableJComboBox;
1698@@ -46,14 +47,17 @@
1699 private int delayScale = 10;
1700 private static final String PRECISION_ERROR_MESSAGE = "The precision is limited to 5 decimal places, the number will be truncated.";
1701 private static final String PRECISION_ERROR_DIALOG_TITLE = "Precision of Time Delay Exceeded";
1702-
1703-
1704-
1705- JTextField TimeDelayField = new JTextField();
1706+ private JPanel sliderPanel;
1707+ private JPanel timedelayPanel;
1708+ JPanel firemode;
1709+
1710+
1711+
1712+ JTextField TimeDelayField = new JTextField();
1713 JComboBox<String> firermodebox;
1714
1715
1716- public AnimationControlSidePanel(Animator animator) {
1717+ public AnimationControlSidePanel(Animator animator, TabContent.TAPNLens lens) {
1718 Require.notNull(animator, "Animator can't be null");
1719
1720 this.animator = animator;
1721@@ -80,7 +84,7 @@
1722 c.gridy = 2;
1723 add(animationToolBar, c);
1724
1725- JPanel firemode = new JPanel(new FlowLayout(FlowLayout.LEFT));
1726+ firemode = new JPanel(new FlowLayout(FlowLayout.LEFT));
1727
1728 JLabel label = new JLabel("Token selection: ");
1729
1730@@ -104,10 +108,21 @@
1731 this.setMinimumSize(new Dimension(275, 180));
1732
1733 initializeDocumentFilterForDelayInput();
1734+ hideIrrelevantInformation(lens);
1735 }
1736
1737+ private void hideIrrelevantInformation(TabContent.TAPNLens lens){
1738+ sliderPanel.setVisible(lens.isTimed());
1739+ timedelayPanel.setVisible(lens.isTimed());
1740+ firemode.setVisible(lens.isTimed());
1741+ if(!lens.isTimed()){
1742+ this.setPreferredSize(new Dimension(275, 50));
1743+ this.setMinimumSize(new Dimension(275, 50));
1744+ }
1745+ }
1746+
1747 private void initDelaySlider() {
1748- JPanel sliderPanel = new JPanel(new FlowLayout(FlowLayout.CENTER));
1749+ sliderPanel = new JPanel(new FlowLayout(FlowLayout.CENTER));
1750 JButton decrese = new JButton("-");
1751 decrese.setPreferredSize(new Dimension(20, 30));
1752 decrese.addActionListener(e -> {
1753@@ -174,7 +189,7 @@
1754
1755
1756 private void initDelayTimePanel(JToolBar animationToolBar) {
1757- JPanel timedelayPanel = new JPanel(new FlowLayout(FlowLayout.LEFT));
1758+ timedelayPanel = new JPanel(new FlowLayout(FlowLayout.LEFT));
1759
1760 okButton = new javax.swing.JButton();
1761
1762
1763=== modified file 'src/pipe/gui/AnimationSettingsDialog.java'
1764--- src/pipe/gui/AnimationSettingsDialog.java 2020-07-20 07:19:51 +0000
1765+++ src/pipe/gui/AnimationSettingsDialog.java 2020-08-19 11:36:17 +0000
1766@@ -9,6 +9,7 @@
1767 import javax.swing.JDialog;
1768 import javax.swing.JPanel;
1769
1770+import dk.aau.cs.gui.TabContent;
1771 import pipe.gui.widgets.EscapableDialog;
1772
1773 public class AnimationSettingsDialog {
1774@@ -16,8 +17,8 @@
1775 private static JDialog dialog;
1776 private static DelayEnabledTransitionControl delayEnabled;
1777 private static SimulationControl simControl;
1778-
1779- private static JPanel getContent(){
1780+
1781+ private static JPanel getContent(TabContent.TAPNLens lens){
1782 JPanel content = new JPanel(new BorderLayout());
1783
1784 delayEnabled = DelayEnabledTransitionControl.getInstance();
1785@@ -26,28 +27,32 @@
1786
1787 simControl.addRandomSimulationActionListener(e -> {
1788 if(simControl.randomSimulation()){
1789- delayEnabled.randomMode.setSelected(true);
1790+ simControl.randomMode.setSelected(true);
1791 }
1792 CreateGui.getCurrentTab().getTransitionFireingComponent().updateFireButton();
1793 });
1794
1795 content.add(delayEnabled, BorderLayout.NORTH);
1796 content.add(simControl, BorderLayout.SOUTH);
1797+ hideTimedInformation(lens);
1798 return content;
1799 }
1800-
1801-
1802- public static void showAnimationSettings(){
1803+
1804+ private static void hideTimedInformation(TabContent.TAPNLens lens){
1805+ delayEnabled.setVisible(lens.isTimed());
1806+ }
1807+
1808+ public static void showAnimationSettings(TabContent.TAPNLens lens){
1809 JPanel contentPane = new JPanel(new GridBagLayout());
1810
1811 JButton closeDialogButton = new JButton("Close");
1812 closeDialogButton.addActionListener(o -> dialog.setVisible(false));
1813-
1814+
1815 GridBagConstraints gbc = new GridBagConstraints();
1816 gbc.anchor = GridBagConstraints.NORTHWEST;
1817 gbc.insets = new Insets(0, 3, 0, 3);
1818 gbc.fill = GridBagConstraints.BOTH;
1819- contentPane.add(getContent(), gbc);
1820+ contentPane.add(getContent(lens), gbc);
1821
1822 gbc = new GridBagConstraints();
1823 gbc.anchor = GridBagConstraints.NORTHWEST;
1824
1825=== modified file 'src/pipe/gui/Animator.java'
1826--- src/pipe/gui/Animator.java 2020-07-20 12:17:24 +0000
1827+++ src/pipe/gui/Animator.java 2020-08-19 11:36:17 +0000
1828@@ -705,4 +705,8 @@
1829 }
1830 }
1831
1832+ public TabContent getTab(){
1833+ return tab;
1834+ }
1835+
1836 }
1837
1838=== modified file 'src/pipe/gui/CreateGui.java'
1839--- src/pipe/gui/CreateGui.java 2020-07-22 10:39:07 +0000
1840+++ src/pipe/gui/CreateGui.java 2020-08-19 11:36:17 +0000
1841@@ -157,4 +157,8 @@
1842
1843 public static boolean useExtendedBounds = false;
1844
1845+ //XXX Moved from guiframe to static access, while refactoring.
1846+ @Deprecated
1847+ public static Pipe.ElementType guiMode;
1848+
1849 }
1850
1851=== modified file 'src/pipe/gui/DelayEnabledTransitionControl.java'
1852--- src/pipe/gui/DelayEnabledTransitionControl.java 2020-07-20 08:04:40 +0000
1853+++ src/pipe/gui/DelayEnabledTransitionControl.java 2020-08-19 11:36:17 +0000
1854@@ -23,14 +23,12 @@
1855
1856 private static DelayMode defaultDelayMode = ShortestDelayMode.getInstance();
1857 private static BigDecimal defaultGranularity = new BigDecimal("0.1");
1858- private static boolean defaultIsRandomTrasition;
1859-
1860+
1861 private final JLabel precitionLabel;
1862 private final JSlider delayEnabledPrecision;
1863 private final JLabel delayModeLabel;
1864 private final JComboBox<DelayMode> delayMode;
1865- final JCheckBox randomMode = new JCheckBox("Choose next transition randomly");
1866-
1867+
1868 private DelayEnabledTransitionControl() {
1869 super(new GridBagLayout());
1870
1871@@ -57,8 +55,7 @@
1872 delayMode = new JComboBox<>(items);
1873 setDelayMode(defaultDelayMode);
1874
1875- setRandomTransitionMode(defaultIsRandomTrasition);
1876-
1877+
1878 GridBagConstraints gbc = new GridBagConstraints();
1879 gbc.gridwidth = 2;
1880 gbc.anchor = GridBagConstraints.WEST;
1881@@ -92,13 +89,6 @@
1882 gbc.gridy = 2;
1883 add(delayMode, gbc);
1884
1885- gbc = new GridBagConstraints();
1886- gbc.anchor = GridBagConstraints.WEST;
1887- gbc.weightx = 1.0;
1888- gbc.gridx = 0;
1889- gbc.gridy = 3;
1890- add(randomMode, gbc);
1891-
1892 setBorder(BorderFactory.createCompoundBorder(
1893 BorderFactory.createTitledBorder("Delay controller"),
1894 BorderFactory.createEmptyBorder(3, 3, 3, 3)));
1895@@ -130,19 +120,9 @@
1896 public void setDelayMode(DelayMode delayMode){
1897 this.delayMode.setSelectedItem(delayMode);
1898 }
1899-
1900- public boolean isRandomTransitionMode(){
1901- if(SimulationControl.getInstance().randomSimulation()){
1902- return true;
1903- } else {
1904- return randomMode.isSelected();
1905- }
1906- }
1907-
1908- public void setRandomTransitionMode(boolean randomTransition){
1909- randomMode.setSelected(randomTransition);
1910- }
1911-
1912+
1913+
1914+
1915 private static DelayEnabledTransitionControl instance;
1916
1917 public static DelayEnabledTransitionControl getInstance(){
1918@@ -176,18 +156,6 @@
1919 }
1920 }
1921
1922- public static void setDefaultIsRandomTransition(boolean delayEnabledTransitionIsRandomTransition) {
1923- defaultIsRandomTrasition = delayEnabledTransitionIsRandomTransition;
1924- }
1925-
1926- public static boolean isRandomTransition(){
1927- if(instance != null){
1928- return getInstance().isRandomTransitionMode();
1929- } else {
1930- return defaultIsRandomTrasition;
1931- }
1932- }
1933-
1934 @Override
1935 public void setEnabled(boolean enabled) {
1936 super.setEnabled(enabled);
1937@@ -195,6 +163,5 @@
1938 delayEnabledPrecision.setEnabled(enabled);
1939 delayModeLabel.setEnabled(enabled);
1940 delayMode.setEnabled(enabled);
1941- randomMode.setEnabled(enabled);
1942 }
1943 }
1944
1945=== modified file 'src/pipe/gui/GuiFrame.java'
1946--- src/pipe/gui/GuiFrame.java 2020-08-13 08:58:53 +0000
1947+++ src/pipe/gui/GuiFrame.java 2020-08-19 11:36:17 +0000
1948@@ -11,6 +11,7 @@
1949 import java.net.*;
1950 import java.nio.charset.StandardCharsets;
1951 import java.util.*;
1952+import java.util.List;
1953 import java.util.jar.JarEntry;
1954 import java.util.jar.JarFile;
1955 import javax.swing.*;
1956@@ -25,6 +26,7 @@
1957 import net.tapaal.helpers.Reference.Reference;
1958 import net.tapaal.swinghelpers.ExtendedJTabbedPane;
1959 import net.tapaal.swinghelpers.ToggleButtonWithoutText;
1960+import org.jetbrains.annotations.NotNull;
1961 import pipe.gui.Pipe.ElementType;
1962 import pipe.gui.action.GuiAction;
1963 import pipe.gui.widgets.WorkflowDialog;
1964@@ -43,8 +45,6 @@
1965
1966 private final String frameTitle;
1967
1968- private Pipe.ElementType mode;
1969-
1970 private int newNameCounter = 1;
1971
1972 final MutableReference<GuiFrameControllerActions> guiFrameController = new MutableReference<>();
1973@@ -53,6 +53,9 @@
1974
1975 private final StatusBar statusBar;
1976 private JMenuBar menuBar;
1977+ JMenu drawMenu;
1978+ JMenu animateMenu;
1979+ JMenu viewMenu;
1980 private JToolBar drawingToolBar;
1981 private final JLabel featureInfoText = new JLabel();
1982 private JComboBox<String> timeFeatureOptions = new JComboBox(new String[]{"No", "Yes"});
1983@@ -281,47 +284,6 @@
1984 currentTab.ifPresent(o -> o.setMode(ElementType.ANNOTATION));
1985 }
1986 };
1987- private final GuiAction inhibarcAction = new GuiAction("Inhibitor arc", "Add an inhibitor arc (I)", "I", true) {
1988- public void actionPerformed(ActionEvent e) {
1989- currentTab.ifPresent(o -> o.setMode(ElementType.TAPNINHIBITOR_ARC));
1990- }
1991- };
1992- private final GuiAction transAction = new GuiAction("Transition", "Add a transition (T)", "T", true) {
1993- public void actionPerformed(ActionEvent e) {
1994- currentTab.ifPresent(o -> o.setMode(ElementType.TAPNTRANS));
1995- }
1996- };
1997- private final GuiAction tokenAction = new GuiAction("Add token", "Add a token (+)", "typed +", true) {
1998- public void actionPerformed(ActionEvent e) {
1999- currentTab.ifPresent(o -> o.setMode(ElementType.ADDTOKEN));
2000- }
2001- };
2002- private final GuiAction selectAction = new GuiAction("Select", "Select components (S)", "S", true) {
2003- public void actionPerformed(ActionEvent e) {
2004- currentTab.ifPresent(o -> o.setMode(ElementType.SELECT));
2005- }
2006- };
2007- private final GuiAction deleteTokenAction = new GuiAction("Delete token", "Delete a token (-)", "typed -", true) {
2008- public void actionPerformed(ActionEvent e) {
2009- currentTab.ifPresent(o -> o.setMode(ElementType.DELTOKEN));
2010- }
2011- };
2012- private final GuiAction timedPlaceAction = new GuiAction("Place", "Add a place (P)", "P", true) {
2013- public void actionPerformed(ActionEvent e) {
2014- currentTab.ifPresent(o -> o.setMode(ElementType.TAPNPLACE));
2015- }
2016- };
2017-
2018- private final GuiAction timedArcAction = new GuiAction("Arc", "Add an arc (A)", "A", true) {
2019- public void actionPerformed(ActionEvent e) {
2020- currentTab.ifPresent(o -> o.setMode(ElementType.TAPNARC));
2021- }
2022- };
2023- private final GuiAction transportArcAction = new GuiAction("Transport arc", "Add a transport arc (R)", "R", true) {
2024- public void actionPerformed(ActionEvent e) {
2025- currentTab.ifPresent(o -> o.setMode(ElementType.TRANSPORTARC));
2026- }
2027- };
2028
2029 private final GuiAction showTokenAgeAction = new GuiAction("Display token age", "Show/hide displaying the token age 0.0 (when hidden the age 0.0 is drawn as a dot)", KeyStroke.getKeyStroke('9', shortcutkey), true) {
2030 public void actionPerformed(ActionEvent e) {
2031@@ -436,17 +398,9 @@
2032 currentTab.ifPresent(TabContentActions::stepBackwards);
2033 }
2034 };
2035- private final GuiAction timeAction = new GuiAction("Delay one time unit", "Let time pass one time unit", "W") {
2036- public void actionPerformed(ActionEvent e) {
2037- currentTab.ifPresent(TabContentActions::timeDelay);
2038- }
2039- };
2040- private final GuiAction delayFireAction = new GuiAction("Delay and fire", "Delay and fire selected transition", "F") {
2041- public void actionPerformed(ActionEvent e) {
2042- currentTab.ifPresent(TabContentActions::delayAndFire);
2043- }
2044- };
2045- private final GuiAction prevcomponentAction = new GuiAction("Previous component", "Previous component", "pressed UP") {
2046+
2047+
2048+ private GuiAction prevcomponentAction = new GuiAction("Previous component", "Previous component", "pressed UP") {
2049 public void actionPerformed(ActionEvent e) {
2050 currentTab.ifPresent(TabContentActions::previousComponent);
2051 }
2052@@ -477,6 +431,7 @@
2053
2054 private JCheckBoxMenuItem showZeroToInfinityIntervalsCheckBox;
2055 private JCheckBoxMenuItem showTokenAgeCheckBox;
2056+ private JCheckBoxMenuItem showDelayEnabledTransitionsCheckbox;
2057
2058 private JMenu zoomMenu;
2059
2060@@ -496,7 +451,7 @@
2061 this.setMinimumSize(new Dimension(825, 480));
2062
2063 setDefaultCloseOperation(DO_NOTHING_ON_CLOSE);
2064- appTab= new ExtendedJTabbedPane<TabContent>() {
2065+ appTab = new ExtendedJTabbedPane<TabContent>() {
2066 @Override
2067 public Component generator() {
2068 return new TabComponent(this) {
2069@@ -586,7 +541,7 @@
2070 }
2071
2072
2073- if (Platform.isMac()){
2074+ if (Platform.isMac()) {
2075
2076 //Set specific settings
2077 System.setProperty("apple.laf.useScreenMenuBar", "true");
2078@@ -616,11 +571,11 @@
2079 **/
2080 private void buildMenus() {
2081 menuBar = new JMenuBar();
2082-
2083 menuBar.add(buildMenuFiles());
2084 menuBar.add(buildMenuEdit());
2085 menuBar.add(buildMenuView());
2086 menuBar.add(buildMenuDraw());
2087+
2088 menuBar.add(buildMenuAnimation());
2089 menuBar.add(buildMenuTools());
2090 menuBar.add(buildMenuHelp());
2091@@ -658,35 +613,14 @@
2092
2093 private JMenu buildMenuDraw() {
2094 /* Draw menu */
2095- JMenu drawMenu = new JMenu("Draw");
2096+ drawMenu = new JMenu("Draw");
2097 drawMenu.setMnemonic('D');
2098-
2099- drawMenu.add(selectAction);
2100- drawMenu.addSeparator();
2101-
2102- drawMenu.add(timedPlaceAction);
2103-
2104- drawMenu.add(transAction);
2105-
2106- drawMenu.add(timedArcAction);
2107-
2108- drawMenu.add(transportArcAction);
2109-
2110- drawMenu.add(inhibarcAction);
2111-
2112- drawMenu.add(annotationAction);
2113-
2114- drawMenu.addSeparator();
2115-
2116- drawMenu.add(tokenAction);
2117-
2118- drawMenu.add(deleteTokenAction);
2119 return drawMenu;
2120 }
2121
2122 private JMenu buildMenuView() {
2123 /* ViewMenu */
2124- JMenu viewMenu = new JMenu("View");
2125+ viewMenu = new JMenu("View");
2126 viewMenu.setMnemonic('V');
2127
2128 zoomMenu = new JMenu("Zoom");
2129@@ -725,7 +659,7 @@
2130
2131 addCheckboxMenuItem(viewMenu, showEnabledTransitionsAction);
2132
2133- addCheckboxMenuItem(viewMenu, showDelayEnabledTransitionsAction);
2134+ showDelayEnabledTransitionsCheckbox = addCheckboxMenuItem(viewMenu, showDelayEnabledTransitionsAction);
2135
2136 showZeroToInfinityIntervalsCheckBox = addCheckboxMenuItem(viewMenu, showZeroToInfinityIntervals(), showZeroToInfinityIntervalsAction);
2137
2138@@ -744,7 +678,7 @@
2139
2140 private JMenu buildMenuAnimation() {
2141 /* Simulator */
2142- JMenu animateMenu = new JMenu("Simulator");
2143+ animateMenu = new JMenu("Simulator");
2144 animateMenu.setMnemonic('A');
2145 animateMenu.add(startAction);
2146
2147@@ -752,10 +686,6 @@
2148 animateMenu.add(stepbackwardAction);
2149 animateMenu.add(stepforwardAction);
2150
2151- animateMenu.add(timeAction);
2152-
2153- animateMenu.add(delayFireAction);
2154-
2155 animateMenu.add(prevcomponentAction);
2156
2157 animateMenu.add(nextcomponentAction);
2158@@ -878,25 +808,6 @@
2159 drawingToolBar.addSeparator();
2160 drawingToolBar.setRequestFocusEnabled(false);
2161
2162- // Normal arraw
2163- drawingToolBar.add(new ToggleButtonWithoutText(selectAction));
2164-
2165-
2166- // Drawing elements
2167- drawingToolBar.addSeparator();
2168- drawingToolBar.add(new ToggleButtonWithoutText(timedPlaceAction));
2169- drawingToolBar.add(new ToggleButtonWithoutText(transAction));
2170- drawingToolBar.add(new ToggleButtonWithoutText(timedArcAction));
2171- drawingToolBar.add(new ToggleButtonWithoutText(transportArcAction));
2172- drawingToolBar.add(new ToggleButtonWithoutText(inhibarcAction));
2173-
2174- drawingToolBar.add(new ToggleButtonWithoutText(annotationAction));
2175-
2176- // Tokens
2177- drawingToolBar.addSeparator();
2178- drawingToolBar.add(new ToggleButtonWithoutText(tokenAction));
2179- drawingToolBar.add(new ToggleButtonWithoutText(deleteTokenAction));
2180-
2181 // Create panel to put toolbars in
2182 JPanel toolBarPanel = new JPanel();
2183 toolBarPanel.setLayout(new FlowLayout(FlowLayout.LEFT, 0, 0));
2184@@ -1001,21 +912,10 @@
2185 exportTraceAction.setEnabled(false);
2186 importTraceAction.setEnabled(false);
2187
2188- timedPlaceAction.setEnabled(true);
2189- timedArcAction.setEnabled(true);
2190- inhibarcAction.setEnabled(true);
2191- transportArcAction.setEnabled(true);
2192-
2193 annotationAction.setEnabled(true);
2194- transAction.setEnabled(true);
2195- tokenAction.setEnabled(true);
2196 deleteAction.setEnabled(true);
2197 selectAllAction.setEnabled(true);
2198- selectAction.setEnabled(true);
2199- deleteTokenAction.setEnabled(true);
2200
2201- timeAction.setEnabled(false);
2202- delayFireAction.setEnabled(false);
2203 stepbackwardAction.setEnabled(false);
2204 stepforwardAction.setEnabled(false);
2205 prevcomponentAction.setEnabled(false);
2206@@ -1038,7 +938,6 @@
2207 WorkflowDialog.showDialog();
2208 }
2209
2210- statusBar.changeText(StatusBar.textforDrawing);
2211 //Enable editor focus traversal policy
2212 setFocusTraversalPolicy(new EditorFocusTraversalPolicy());
2213 fixBug812694GrayMenuAfterSimulationOnMac();
2214@@ -1047,18 +946,9 @@
2215 case animation:
2216 enableAllActions(true);
2217
2218- timedPlaceAction.setEnabled(false);
2219- timedArcAction.setEnabled(false);
2220- inhibarcAction.setEnabled(false);
2221- transportArcAction.setEnabled(false);
2222-
2223 annotationAction.setEnabled(false);
2224- transAction.setEnabled(false);
2225- tokenAction.setEnabled(false);
2226 deleteAction.setEnabled(false);
2227 selectAllAction.setEnabled(false);
2228- selectAction.setEnabled(false);
2229- deleteTokenAction.setEnabled(false);
2230
2231 alignToGrid.setEnabled(false);
2232
2233@@ -1066,9 +956,6 @@
2234 showConstantsAction.setEnabled(false);
2235 showQueriesAction.setEnabled(false);
2236
2237- timeAction.setEnabled(true);
2238-
2239- delayFireAction.setEnabled(true);
2240 stepbackwardAction.setEnabled(true);
2241 stepforwardAction.setEnabled(true);
2242 prevcomponentAction.setEnabled(true);
2243@@ -1091,7 +978,6 @@
2244
2245 getCurrentTab().getAnimationController().requestFocusInWindow();
2246
2247- statusBar.changeText(StatusBar.textforAnimation);
2248 //Enable simulator focus traversal policy
2249 setFocusTraversalPolicy(new SimulatorFocusTraversalPolicy());
2250
2251@@ -1101,21 +987,9 @@
2252 importTraceAction.setEnabled(false);
2253 verifyAction.setEnabled(false);
2254
2255- timedPlaceAction.setEnabled(false);
2256- timedArcAction.setEnabled(false);
2257- inhibarcAction.setEnabled(false);
2258- transportArcAction.setEnabled(false);
2259-
2260 annotationAction.setEnabled(false);
2261- transAction.setEnabled(false);
2262- tokenAction.setEnabled(false);
2263- deleteAction.setEnabled(false);
2264 selectAllAction.setEnabled(false);
2265- selectAction.setEnabled(false);
2266- deleteTokenAction.setEnabled(false);
2267
2268- timeAction.setEnabled(false);
2269- delayFireAction.setEnabled(false);
2270 stepbackwardAction.setEnabled(false);
2271 stepforwardAction.setEnabled(false);
2272
2273@@ -1135,7 +1009,7 @@
2274 enableAllActions(false);
2275
2276 // Disable All Actions
2277- statusBar.changeText(StatusBar.textforNoNet);
2278+ statusBar.changeText("Open a net to start editing");
2279 setFocusTraversalPolicy(null);
2280
2281 break;
2282@@ -1262,6 +1136,9 @@
2283 break;
2284 case noNet:
2285 setFeatureInfoText(null);
2286+ registerDrawingActions(List.of());
2287+ registerAnimationActions(List.of());
2288+ //registerViewActions(List.of());
2289 break;
2290
2291 default:
2292@@ -1270,7 +1147,74 @@
2293
2294 // Enable actions based on GUI mode
2295 enableGUIActions(mode);
2296-
2297+ if (currentTab != null) {
2298+ currentTab.ifPresent(o -> o.updateEnabledActions(mode));
2299+ }
2300+ }
2301+
2302+ @Override
2303+ public void registerDrawingActions(@NotNull List<GuiAction> drawActions) {
2304+
2305+ drawingToolBar.removeAll();
2306+ drawMenu.removeAll();
2307+
2308+ if (drawActions.size() > 0) {
2309+ drawMenu.setEnabled(true);
2310+ drawingToolBar.addSeparator();
2311+
2312+ for (GuiAction action : drawActions) {
2313+ drawingToolBar.add(new ToggleButtonWithoutText(action));
2314+ drawMenu.add(action);
2315+ }
2316+
2317+ drawingToolBar.addSeparator();
2318+ drawingToolBar.add(featureInfoText);
2319+ } else {
2320+ drawMenu.setEnabled(false);
2321+ }
2322+
2323+ }
2324+ @Override
2325+ public void registerAnimationActions(@NotNull List<GuiAction> animationActions) {
2326+
2327+ animateMenu.removeAll();
2328+
2329+ if (animationActions.size() > 0) {
2330+
2331+ animateMenu.setEnabled(true);
2332+ animateMenu.add(startAction);
2333+
2334+ animateMenu.add(stepbackwardAction);
2335+ animateMenu.add(stepforwardAction);
2336+
2337+ for (GuiAction action : animationActions) {
2338+ animateMenu.add(action);
2339+ }
2340+
2341+ animateMenu.add(prevcomponentAction);
2342+ animateMenu.add(nextcomponentAction);
2343+
2344+ animateMenu.addSeparator();
2345+ animateMenu.add(exportTraceAction);
2346+ animateMenu.add(importTraceAction);
2347+ } else {
2348+ animateMenu.setEnabled(false);
2349+ }
2350+ }
2351+
2352+ @Override
2353+ public void registerViewActions(@NotNull List<GuiAction> viewActions) {
2354+ //TODO: This is a temporary implementation until view actions can be moved to tab content
2355+
2356+ if (!getCurrentTab().getLens().isTimed()) {
2357+ showZeroToInfinityIntervalsCheckBox.setVisible(false);
2358+ showTokenAgeCheckBox.setVisible(false);
2359+ showDelayEnabledTransitionsCheckbox.setVisible(false);
2360+ } else {
2361+ showZeroToInfinityIntervalsCheckBox.setVisible(true);
2362+ showTokenAgeCheckBox.setVisible(true);
2363+ showDelayEnabledTransitionsCheckbox.setVisible(true);
2364+ }
2365 }
2366
2367 private void fixBug812694GrayMenuAfterSimulationOnMac() {
2368@@ -1284,24 +1228,9 @@
2369 a.dispose();
2370 }
2371
2372- //XXX temp while refactoring, kyrke - 2019-07-25, should only be called from TabContent
2373 @Override
2374- public void updateMode(Pipe.ElementType _mode) {
2375-
2376- mode = _mode;
2377-
2378- // deselect other actions
2379- transAction.setSelected(mode == ElementType.TAPNTRANS);
2380- timedPlaceAction.setSelected(mode == ElementType.TAPNPLACE);
2381- timedArcAction.setSelected(mode == ElementType.TAPNARC);
2382- transportArcAction.setSelected(mode == ElementType.TRANSPORTARC);
2383- inhibarcAction.setSelected(mode == ElementType.TAPNINHIBITOR_ARC);
2384- tokenAction.setSelected(mode == ElementType.ADDTOKEN);
2385- deleteTokenAction.setSelected(mode == ElementType.DELTOKEN);
2386- selectAction.setSelected(mode == ElementType.SELECT);
2387- annotationAction.setSelected(mode == ElementType.ANNOTATION);
2388-
2389- statusBar.changeText(mode);
2390+ public void setStatusBarText(String s) {
2391+ statusBar.changeText(Objects.requireNonNullElse(s, ""));
2392 }
2393
2394
2395@@ -1368,10 +1297,6 @@
2396 showTokenAgeAction.setSelected(b);
2397 }
2398
2399- public Pipe.ElementType getMode() {
2400- return mode;
2401- }
2402-
2403 public void setTitle(String title) {
2404 super.setTitle((title == null) ? frameTitle : frameTitle + ": " + title);
2405 }
2406@@ -1403,7 +1328,6 @@
2407 zoomComboBox.addActionListener(zoomComboListener);
2408 }
2409
2410-
2411 private boolean canNetBeSavedAndShowMessage() {
2412 if (getCurrentTab().network().paintNet()) {
2413 return true;
2414
2415=== modified file 'src/pipe/gui/GuiFrameActions.java'
2416--- src/pipe/gui/GuiFrameActions.java 2020-08-04 19:07:12 +0000
2417+++ src/pipe/gui/GuiFrameActions.java 2020-08-19 11:36:17 +0000
2418@@ -3,8 +3,10 @@
2419 import dk.aau.cs.gui.TabContent;
2420 import dk.aau.cs.gui.TabContentActions;
2421 import net.tapaal.helpers.Reference.Reference;
2422+import pipe.gui.action.GuiAction;
2423
2424 import java.awt.*;
2425+import java.util.List;
2426
2427 /**
2428 * Used to delegate control of the state of AppGUI to tabs
2429@@ -26,8 +28,13 @@
2430
2431 void setGUIMode(GuiFrame.GUIMode animation);
2432
2433- //XXX temp while refactoring, kyrke - 2019-07-25
2434- void updateMode(Pipe.ElementType mode);
2435+ void registerDrawingActions(List<GuiAction> drawActions);
2436+
2437+ void registerAnimationActions(List<GuiAction> animationActions);
2438+
2439+ void registerViewActions(List<GuiAction> viewActions);
2440+
2441+ void setStatusBarText(String s);
2442
2443 void registerController(GuiFrameControllerActions guiFrameController, Reference<TabContentActions> currentTab);
2444
2445
2446=== modified file 'src/pipe/gui/GuiFrameController.java'
2447--- src/pipe/gui/GuiFrameController.java 2020-08-10 09:25:25 +0000
2448+++ src/pipe/gui/GuiFrameController.java 2020-08-19 11:36:17 +0000
2449@@ -85,7 +85,7 @@
2450
2451 DelayEnabledTransitionControl.setDefaultDelayMode(prefs.getDelayEnabledTransitionDelayMode());
2452 DelayEnabledTransitionControl.setDefaultGranularity(prefs.getDelayEnabledTransitionGranularity());
2453- DelayEnabledTransitionControl.setDefaultIsRandomTransition(prefs.getDelayEnabledTransitionIsRandomTransition());
2454+ SimulationControl.setDefaultIsRandomTransition(prefs.getDelayEnabledTransitionIsRandomTransition());
2455
2456 showToolTips = prefs.getShowToolTips();
2457 setDisplayToolTips(showToolTips);
2458@@ -221,7 +221,7 @@
2459 prefs.setShowTokenAge(guiFrameDirectAccess.showTokenAge());
2460 prefs.setDelayEnabledTransitionDelayMode(DelayEnabledTransitionControl.getDefaultDelayMode());
2461 prefs.setDelayEnabledTransitionGranularity(DelayEnabledTransitionControl.getDefaultGranularity());
2462- prefs.setDelayEnabledTransitionIsRandomTransition(DelayEnabledTransitionControl.isRandomTransition());
2463+ prefs.setDelayEnabledTransitionIsRandomTransition(SimulationControl.isRandomTransition());
2464
2465 JOptionPane.showMessageDialog(guiFrameDirectAccess,
2466 "The workspace has now been saved into your preferences.\n"
2467@@ -726,7 +726,7 @@
2468 //showDelayEnabledTransitions(advanced);
2469 DelayEnabledTransitionControl.getInstance().setValue(new BigDecimal("0.1"));
2470 DelayEnabledTransitionControl.getInstance().setDelayMode(ShortestDelayMode.getInstance());
2471- DelayEnabledTransitionControl.getInstance().setRandomTransitionMode(false);
2472+ SimulationControl.getInstance().setRandomTransitionMode(false);
2473 }
2474
2475 }
2476
2477=== modified file 'src/pipe/gui/SimulationControl.java'
2478--- src/pipe/gui/SimulationControl.java 2020-06-21 11:16:52 +0000
2479+++ src/pipe/gui/SimulationControl.java 2020-08-19 11:36:17 +0000
2480@@ -22,9 +22,10 @@
2481
2482 final JSlider simulationSpeed = new JSlider();
2483 final JCheckBox randomSimulation = new JCheckBox("Enable automatic random simulation");
2484- final Timer timer = new Timer(simulationSpeed.getValue()*20, e -> CreateGui.getCurrentTab().getTransitionFireingComponent().fireSelectedTransition());
2485-
2486- private static SimulationControl instance;
2487+ final JCheckBox randomMode = new JCheckBox("Choose next transition randomly");
2488+ final Timer timer = new Timer(simulationSpeed.getValue()*20, e -> CreateGui.getCurrentTab().getTransitionFireingComponent().fireSelectedTransition());
2489+ private static boolean defaultIsRandomTrasition;
2490+ private static SimulationControl instance;
2491
2492 public static SimulationControl getInstance(){
2493 if(instance == null){
2494@@ -62,13 +63,23 @@
2495 gbc.gridx = 0;
2496 gbc.gridy = 0;
2497 add(randomSimulation, gbc);
2498-
2499+
2500 gbc = new GridBagConstraints();
2501+ gbc.anchor = GridBagConstraints.WEST;
2502+ gbc.fill = GridBagConstraints.HORIZONTAL;
2503+ gbc.weightx = 1.0;
2504+ gbc.gridx = 0;
2505+ gbc.gridy = 1;
2506+ add(randomMode, gbc);
2507+
2508+ setRandomTransitionMode(defaultIsRandomTrasition);
2509+
2510+ gbc = new GridBagConstraints();
2511 gbc.anchor = GridBagConstraints.WEST;
2512 gbc.fill = GridBagConstraints.HORIZONTAL;
2513 gbc.weightx = 1.0;
2514 gbc.gridx = 0;
2515- gbc.gridy = 1;
2516+ gbc.gridy = 2;
2517 add(new JLabel("Set simulation speed:"), gbc);
2518
2519 gbc = new GridBagConstraints();
2520@@ -76,7 +87,7 @@
2521 gbc.fill = GridBagConstraints.HORIZONTAL;
2522 gbc.weightx = 1.0;
2523 gbc.gridx = 0;
2524- gbc.gridy = 2;
2525+ gbc.gridy = 3;
2526 add(simulationSpeed, gbc);
2527
2528 setBorder(BorderFactory.createCompoundBorder(
2529@@ -159,4 +170,26 @@
2530 dialog.setLocation(x, y);
2531 dialog.setVisible(true);
2532 }
2533+
2534+ public boolean isRandomTransitionMode(){
2535+ if(SimulationControl.getInstance().randomSimulation()){
2536+ return true;
2537+ } else {
2538+ return randomMode.isSelected();
2539+ }
2540+ }
2541+
2542+ public void setRandomTransitionMode(boolean randomTransition){
2543+ randomMode.setSelected(randomTransition);
2544+ }
2545+ public static boolean isRandomTransition(){
2546+ if(instance != null){
2547+ return getInstance().isRandomTransitionMode();
2548+ } else {
2549+ return defaultIsRandomTrasition;
2550+ }
2551+ }
2552+ public static void setDefaultIsRandomTransition(boolean delayEnabledTransitionIsRandomTransition) {
2553+ defaultIsRandomTrasition = delayEnabledTransitionIsRandomTransition;
2554+ }
2555 }
2556
2557=== modified file 'src/pipe/gui/StatusBar.java'
2558--- src/pipe/gui/StatusBar.java 2020-07-13 13:58:47 +0000
2559+++ src/pipe/gui/StatusBar.java 2020-08-19 11:36:17 +0000
2560@@ -8,41 +8,11 @@
2561 /* Status Bar to let users know what to do*/
2562 public class StatusBar extends JPanel {
2563
2564- /* Provides the appropriate text for the mode that the user is in */
2565- public static final String textforNoNet = "Open a net to start editing";
2566-
2567- public static final String textforDrawing = "Drawing Mode: Click on a button to start adding components to the "
2568- + "Editor";
2569- public static final String textforPlace = "Place Mode: Right click on a place to see menu options "
2570- + "";
2571- public static final String textforTAPNPlace = "Place Mode: Right click on a place to see menu options "
2572- + "";
2573- public static final String textforTrans = "Transition Mode: Right click on a transition to see menu "
2574- + "options [Mouse wheel -> rotate]";
2575- public static final String textforTimedTrans = "Timed Transition Mode: Right click on a transition to see menu "
2576- + "options [Mouse wheel -> rotate]";
2577- public static final String textforAddtoken = "Add Token Mode: Click on a place to add a token";
2578- public static final String textforDeltoken = "Delete Token Mode: Click on a place to delete a token ";
2579- public static final String textforAnimation = "Simulation Mode: Red transitions are enabled, click a transition to "
2580- + "fire it";
2581- public static final String textforArc = "Arc Mode: Right click on an arc to see menu options "
2582- + "";
2583- public static final String textforTransportArc = "Transport Arc Mode: Right click on an arc to see menu options "
2584- + "";
2585- public static final String textforInhibArc = "Inhibitor Mode: Right click on an arc to see menu options "
2586- + "";
2587- public static final String textforMove = "Select Mode: Click/drag to select objects; drag to move them";
2588- public static final String textforAnnotation = "Annotation Mode: Right click on an annotation to see menu options; "
2589- + "double click to edit";
2590-
2591- public static final String textforDrag = "Drag Mode";
2592-
2593-
2594 private final JLabel label;
2595
2596 public StatusBar() {
2597 super();
2598- label = new JLabel(textforDrawing); // got to put something in there
2599+ label = new JLabel("");
2600 this.setLayout(new BorderLayout(0, 0));
2601 this.add(label);
2602 }
2603@@ -51,67 +21,6 @@
2604 label.setText(newText);
2605 }
2606
2607- public void changeText(Pipe.ElementType type) {
2608- switch (type) {
2609- case PLACE:
2610- changeText(textforPlace);
2611- break;
2612-
2613- case TAPNPLACE:
2614- changeText(textforTAPNPlace);
2615- break;
2616-
2617- case IMMTRANS:
2618- case TAPNTRANS:
2619- changeText(textforTrans);
2620- break;
2621-
2622- case TIMEDTRANS:
2623- changeText(textforTimedTrans);
2624- break;
2625-
2626- case ARC:
2627- case TAPNARC:
2628- changeText(textforArc);
2629- break;
2630-
2631- case TRANSPORTARC:
2632- changeText(textforTransportArc);
2633- break;
2634-
2635- case TAPNINHIBITOR_ARC:
2636- case INHIBARC:
2637- changeText(textforInhibArc);
2638- break;
2639-
2640- case ADDTOKEN:
2641- changeText(textforAddtoken);
2642- break;
2643-
2644- case DELTOKEN:
2645- changeText(textforDeltoken);
2646- break;
2647-
2648- case SELECT:
2649- changeText(textforMove);
2650- break;
2651-
2652- case DRAW:
2653- changeText(textforDrawing);
2654- break;
2655-
2656- case ANNOTATION:
2657- changeText(textforAnnotation);
2658- break;
2659-
2660- case DRAG:
2661- changeText(textforDrag);
2662- break;
2663-
2664- default:
2665- changeText("To-do (textfor" + type);
2666- break;
2667- }
2668- }
2669+
2670
2671 }
2672
2673=== modified file 'src/pipe/gui/action/GuiAction.java'
2674--- src/pipe/gui/action/GuiAction.java 2020-07-20 07:19:51 +0000
2675+++ src/pipe/gui/action/GuiAction.java 2020-08-19 11:36:17 +0000
2676@@ -109,4 +109,12 @@
2677
2678 }
2679
2680+ public void setName(String newName){
2681+ putValue(NAME, newName);
2682+ }
2683+
2684+ public void setTooltip(String newTooltip){
2685+ putValue(SHORT_DESCRIPTION, newTooltip);
2686+ }
2687+
2688 }
2689
2690=== modified file 'src/pipe/gui/canvas/DrawingSurfaceImpl.java'
2691--- src/pipe/gui/canvas/DrawingSurfaceImpl.java 2020-08-10 06:46:22 +0000
2692+++ src/pipe/gui/canvas/DrawingSurfaceImpl.java 2020-08-19 11:36:17 +0000
2693@@ -412,7 +412,7 @@
2694
2695 if (SwingUtilities.isLeftMouseButton(e)) {
2696
2697- Pipe.ElementType mode = app.getMode();
2698+ Pipe.ElementType mode = CreateGui.guiMode;
2699
2700 switch (mode) {
2701 case DRAG:
2702@@ -443,7 +443,7 @@
2703 dragStart = null;
2704 setCursor(Cursor.getPredefinedCursor(Cursor.DEFAULT_CURSOR));
2705 }
2706- if (app.getMode() == ElementType.SELECT) {
2707+ if (CreateGui.guiMode == ElementType.SELECT) {
2708 getSelectionObject().dispatchEvent(e);
2709 }
2710 }
2711@@ -461,9 +461,9 @@
2712 if (managerRef!=null && managerRef.get() != null) {
2713 managerRef.get().drawingSurfaceMouseDragged(e);
2714 }
2715- if (dragStart != null) {
2716+ if (dragStart != null) {
2717 view.drag(dragStart, e.getPoint());
2718- } else if (app.getMode() == ElementType.SELECT) {
2719+ } else if (CreateGui.guiMode == ElementType.SELECT) {
2720 getSelectionObject().dispatchEvent(e);
2721 }
2722 }
2723
2724=== modified file 'src/pipe/gui/graphicElements/PetriNetObject.java'
2725--- src/pipe/gui/graphicElements/PetriNetObject.java 2020-06-30 06:41:30 +0000
2726+++ src/pipe/gui/graphicElements/PetriNetObject.java 2020-08-19 11:36:17 +0000
2727@@ -3,6 +3,8 @@
2728 import java.awt.Graphics;
2729 import java.awt.Rectangle;
2730 import java.awt.event.*;
2731+
2732+import dk.aau.cs.gui.TabContent;
2733 import pipe.dataLayer.DataLayer;
2734 import pipe.gui.canvas.DrawingSurfaceImpl;
2735 import pipe.gui.Pipe;
2736@@ -19,6 +21,7 @@
2737 /** x/y position position on screen (zoomed) */
2738 protected int positionX;
2739 protected int positionY;
2740+ protected TabContent.TAPNLens lens = TabContent.TAPNLens.Default;
2741
2742 // The x/y coordinate of object at 100% zoom.
2743 //XXX: pushed down from PlaceTransitionObject and consolidated from note, need further refactoring and rename, //kyrke 2019-08-23
2744@@ -285,6 +288,14 @@
2745 return positionY;
2746 }
2747
2748+ public boolean isTimed(){
2749+ return lens.isTimed();
2750+ }
2751+
2752+ public void setLens(TabContent.TAPNLens lens){
2753+ this.lens = lens;
2754+ }
2755+
2756 @Override
2757 public GraphicalElement getGraphicalElement() {
2758 return this;
2759
2760=== modified file 'src/pipe/gui/graphicElements/tapn/TimedInputArcComponent.java'
2761--- src/pipe/gui/graphicElements/tapn/TimedInputArcComponent.java 2020-07-20 07:19:51 +0000
2762+++ src/pipe/gui/graphicElements/tapn/TimedInputArcComponent.java 2020-08-19 11:36:17 +0000
2763@@ -2,6 +2,7 @@
2764
2765 import java.util.Hashtable;
2766
2767+import dk.aau.cs.gui.TabContent;
2768 import pipe.gui.CreateGui;
2769 import pipe.gui.Pipe;
2770 import pipe.gui.graphicElements.PlaceTransitionObject;
2771@@ -24,11 +25,12 @@
2772 updateLabel(true);
2773 }
2774
2775- public TimedInputArcComponent(PlaceTransitionObject source, PlaceTransitionObject target, TimedInputArc modelArc){
2776+ public TimedInputArcComponent(PlaceTransitionObject source, PlaceTransitionObject target, TimedInputArc modelArc, TabContent.TAPNLens lens){
2777 super(source);
2778 setTarget(target);
2779 setUnderlyingArc(modelArc);
2780 updateLabel(true);
2781+ this.lens = lens;
2782 sealArc();
2783 }
2784
2785@@ -37,6 +39,12 @@
2786 updateLabel(true);
2787 }
2788
2789+ public TimedInputArcComponent(TimedOutputArcComponent arc, TabContent.TAPNLens lens) {
2790+ super(arc);
2791+ updateLabel(true);
2792+ this.lens = lens;
2793+ }
2794+
2795 @Override
2796 protected void addMouseHandler() {
2797 //XXX: kyrke 2018-09-06, this is bad as we leak "this", think its ok for now, as it alwas constructed when
2798@@ -82,7 +90,7 @@
2799 if (inputArc == null)
2800 getNameLabel().setText("");
2801 else {
2802- if (!CreateGui.getApp().showZeroToInfinityIntervals()) {
2803+ if (!CreateGui.getApp().showZeroToInfinityIntervals() || !lens.isTimed()) {
2804 if (inputArc.interval().toString(showConstantNames).equals("[0,inf)")){
2805 getNameLabel().setText("");
2806 }
2807
2808=== modified file 'src/pipe/gui/graphicElements/tapn/TimedOutputArcComponent.java'
2809--- src/pipe/gui/graphicElements/tapn/TimedOutputArcComponent.java 2020-07-16 08:39:06 +0000
2810+++ src/pipe/gui/graphicElements/tapn/TimedOutputArcComponent.java 2020-08-19 11:36:17 +0000
2811@@ -51,6 +51,7 @@
2812 Grid.getModifiedX((int) (arc.getNameLabel().getXPosition() + Zoomer.getZoomedValue(getNameOffsetX(), getZoom()))),
2813 Grid.getModifiedY((int) (arc.getNameLabel().getYPosition() + Zoomer.getZoomedValue(getNameOffsetY(), getZoom())))
2814 );
2815+ this.lens = arc.lens;
2816
2817 }
2818
2819
2820=== modified file 'src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java'
2821--- src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java 2020-07-20 07:19:51 +0000
2822+++ src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java 2020-08-19 11:36:17 +0000
2823@@ -23,6 +23,7 @@
2824 import javax.swing.BoxLayout;
2825 import javax.swing.JTextArea;
2826
2827+import dk.aau.cs.gui.TabContent;
2828 import pipe.gui.CreateGui;
2829 import pipe.gui.Pipe;
2830 import pipe.gui.graphicElements.Place;
2831@@ -49,11 +50,11 @@
2832 private Window ageOfTokensWindow = new Window(new Frame());
2833 private final Shape dashedOutline = createDashedOutline();
2834
2835- public TimedPlaceComponent(int positionXInput, int positionYInput, dk.aau.cs.model.tapn.TimedPlace place) {
2836+ public TimedPlaceComponent(int positionXInput, int positionYInput, dk.aau.cs.model.tapn.TimedPlace place, TabContent.TAPNLens lens) {
2837 super(positionXInput, positionYInput);
2838 this.place = place;
2839 this.place.addTimedPlaceListener(listener);
2840-
2841+ this.lens = lens;
2842 attributesVisible = true;
2843
2844 }
2845@@ -63,15 +64,17 @@
2846 int positionYInput,
2847 String idInput,
2848 int nameOffsetXInput,
2849- int nameOffsetYInput
2850+ int nameOffsetYInput,
2851+ TabContent.TAPNLens lens
2852 ) {
2853
2854 super(positionXInput, positionYInput, idInput, nameOffsetXInput, nameOffsetYInput);
2855 attributesVisible = true;
2856+ this.lens = lens;
2857
2858 }
2859
2860- @Override
2861+ @Override
2862 protected void addMouseHandler() {
2863 //XXX: kyrke 2018-09-06, this is bad as we leak "this", think its ok for now, as it alwas constructed when
2864 //XXX: handler is called. Make static constructor and add handler from there, to make it safe.
2865@@ -173,7 +176,9 @@
2866 }
2867 }
2868 }
2869-
2870+ if(!lens.isTimed()){
2871+ drawDots = (marking > 0 && marking < 6);
2872+ }
2873 // structure sees how many markings there are and fills the place in
2874 // with the appropriate number or tokens.
2875 if(drawDots) {
2876@@ -277,7 +282,7 @@
2877 }
2878
2879 // Build interface
2880- if (show) {
2881+ if (show && isTimed()) {
2882 ageOfTokensWindow = new Window(new Frame());
2883 ageOfTokensWindow.add(new JTextArea(getStringOfTokens()));
2884 ageOfTokensWindow.getComponent(0).setBackground(Color.lightGray);
2885@@ -410,7 +415,7 @@
2886 }
2887
2888 public TimedPlaceComponent copy(TimedArcPetriNet tapn) {
2889- TimedPlaceComponent placeComponent = new TimedPlaceComponent(getOriginalX(), getOriginalY(), id, getNameOffsetX(), getNameOffsetY());
2890+ TimedPlaceComponent placeComponent = new TimedPlaceComponent(getOriginalX(), getOriginalY(), id, getNameOffsetX(), getNameOffsetY(), lens);
2891 placeComponent.setUnderlyingPlace(tapn.getPlaceByName(place.name()));
2892
2893 return placeComponent;
2894
2895=== modified file 'src/pipe/gui/graphicElements/tapn/TimedTransitionComponent.java'
2896--- src/pipe/gui/graphicElements/tapn/TimedTransitionComponent.java 2020-08-10 06:46:22 +0000
2897+++ src/pipe/gui/graphicElements/tapn/TimedTransitionComponent.java 2020-08-19 11:36:17 +0000
2898@@ -16,6 +16,7 @@
2899 import javax.swing.BoxLayout;
2900 import javax.swing.JTextArea;
2901
2902+import dk.aau.cs.gui.TabContent;
2903 import pipe.gui.CreateGui;
2904 import pipe.gui.Pipe;
2905 import pipe.gui.graphicElements.Transition;
2906@@ -36,12 +37,13 @@
2907 private final dk.aau.cs.model.tapn.event.TimedTransitionListener listener;
2908 private GeneralPath dashedOutline;
2909
2910- public TimedTransitionComponent(int positionXInput, int positionYInput, dk.aau.cs.model.tapn.TimedTransition transition) {
2911+ public TimedTransitionComponent(int positionXInput, int positionYInput, dk.aau.cs.model.tapn.TimedTransition transition, TabContent.TAPNLens lens) {
2912 super(positionXInput, positionYInput);
2913 this.transition = transition;
2914 listener = timedTransitionListener();
2915 transition.addTimedTransitionListener(listener);
2916 attributesVisible = true;
2917+ this.lens = lens;
2918
2919 }
2920
2921@@ -54,7 +56,8 @@
2922 boolean timedTransition,
2923 boolean infServer,
2924 int angleInput,
2925- int priority
2926+ int priority,
2927+ TabContent.TAPNLens lens
2928 ) {
2929 super(
2930 positionXInput,
2931@@ -66,6 +69,7 @@
2932 );
2933 listener = timedTransitionListener();
2934 attributesVisible = true;
2935+ this.lens = lens;
2936
2937 }
2938
2939@@ -222,7 +226,7 @@
2940 }
2941
2942 public TimedTransitionComponent copy(TimedArcPetriNet tapn) {
2943- TimedTransitionComponent transitionComponent = new TimedTransitionComponent(getOriginalX(), getOriginalY(), id, getNameOffsetX(), getNameOffsetY(), true, false, getAngle(), 0);
2944+ TimedTransitionComponent transitionComponent = new TimedTransitionComponent(getOriginalX(), getOriginalY(), id, getNameOffsetX(), getNameOffsetY(), true, false, getAngle(), 0, lens);
2945 transitionComponent.setUnderlyingTransition(tapn.getTransitionByName(transition.name()));
2946
2947 return transitionComponent;
2948@@ -237,7 +241,7 @@
2949 }
2950
2951 // Build interface
2952- if (show && (transition.getdInterval() != null)) {
2953+ if (show && (transition.getdInterval() != null) && isTimed()) {
2954 dIntervalWindow = new Window(new Frame());
2955 dIntervalWindow.add(new JTextArea(transition.getdInterval().toString()));
2956
2957
2958=== modified file 'src/pipe/gui/handler/PetriNetObjectHandler.java'
2959--- src/pipe/gui/handler/PetriNetObjectHandler.java 2020-07-20 07:19:51 +0000
2960+++ src/pipe/gui/handler/PetriNetObjectHandler.java 2020-08-19 11:36:17 +0000
2961@@ -66,8 +66,8 @@
2962 @Override
2963 public void mousePressed(MouseEvent e) {
2964 if(CreateGui.getCurrentTab().isInAnimationMode()) return;
2965-
2966- if (CreateGui.getApp().getMode() == ElementType.SELECT) {
2967+
2968+ if (CreateGui.guiMode == ElementType.SELECT) {
2969 if (!myObject.isSelected()) {
2970 if (!e.isShiftDown()) {
2971 myObject.getParent().getSelectionObject().clearSelection();
2972@@ -92,7 +92,7 @@
2973 return;
2974 }
2975
2976- if (CreateGui.getApp().getMode() == ElementType.SELECT) {
2977+ if (CreateGui.guiMode == ElementType.SELECT) {
2978 if (isDragging) {
2979 isDragging = false;
2980 CreateGui.getDrawingSurface().translateSelection(myObject.getParent().getSelectionObject().getSelection(), totalX, totalY);
2981@@ -124,7 +124,7 @@
2982 return;
2983 }
2984
2985- if (CreateGui.getApp().getMode() == ElementType.SELECT) {
2986+ if (CreateGui.guiMode == ElementType.SELECT) {
2987 if (myObject.isDraggable()) {
2988 if (!isDragging) {
2989 isDragging = true;
2990
2991=== modified file 'src/pipe/gui/widgets/GuardDialogue.java'
2992--- src/pipe/gui/widgets/GuardDialogue.java 2020-07-20 08:14:17 +0000
2993+++ src/pipe/gui/widgets/GuardDialogue.java 2020-08-19 11:36:17 +0000
2994@@ -27,6 +27,7 @@
2995 import javax.swing.SpinnerNumberModel;
2996 import javax.swing.event.ChangeEvent;
2997
2998+import dk.aau.cs.gui.TabContent;
2999 import dk.aau.cs.model.tapn.*;
3000 import net.tapaal.swinghelpers.WidthAdjustingComboBox;
3001 import pipe.gui.CreateGui;
3002@@ -76,7 +77,10 @@
3003 if(objectToBeEdited instanceof TimedInputArcComponent && !(objectToBeEdited instanceof TimedInhibitorArcComponent)){
3004 initTimeGuardPanel();
3005 }
3006-
3007+ if(!objectToBeEdited.isTimed() ){
3008+ guardEditPanel.setVisible(false);
3009+ }
3010+
3011 initWeightPanel();
3012 initButtonPanel(objectToBeEdited);
3013
3014
3015=== modified file 'src/pipe/gui/widgets/PlaceEditorPanel.java'
3016--- src/pipe/gui/widgets/PlaceEditorPanel.java 2020-07-23 09:18:11 +0000
3017+++ src/pipe/gui/widgets/PlaceEditorPanel.java 2020-08-19 11:36:17 +0000
3018@@ -22,6 +22,7 @@
3019 import javax.swing.JSpinner;
3020 import javax.swing.event.ChangeListener;
3021
3022+import dk.aau.cs.gui.TabContent;
3023 import net.tapaal.swinghelpers.CustomJSpinner;
3024 import net.tapaal.swinghelpers.GridBagHelper;
3025 import net.tapaal.swinghelpers.WidthAdjustingComboBox;
3026@@ -67,17 +68,26 @@
3027 private final Context context;
3028 private boolean makeNewShared = false;
3029 private boolean doNewEdit = true;
3030+ private final TabContent currentTab;
3031
3032 private Vector<TimedPlace> sharedPlaces;
3033 private final int maxNumberOfPlacesToShowAtOnce = 20;
3034
3035 public PlaceEditorPanel(JRootPane rootPane, TimedPlaceComponent placeComponent, Context context) {
3036 this.rootPane = rootPane;
3037+ currentTab = context.tabContent();
3038 place = placeComponent;
3039 this.context = context;
3040 initComponents();
3041+ hideTimedInformation();
3042 }
3043
3044+ private void hideTimedInformation(){
3045+ if(!place.isTimed()) {
3046+ timeInvariantPanel.setVisible(false);
3047+ }
3048+ }
3049+
3050 private void initComponents() {
3051 setLayout(new java.awt.GridBagLayout());
3052
3053@@ -90,6 +100,7 @@
3054 gridBagConstraints = GridBagHelper.as(0,1, WEST, HORIZONTAL, new Insets(0, 8, 0, 8));
3055 add(timeInvariantPanel, gridBagConstraints);
3056
3057+
3058 initButtonPanel();
3059
3060 gridBagConstraints = GridBagHelper.as(0,2, new Insets(0, 8, 5, 8));
3061
3062=== modified file 'src/pipe/gui/widgets/QueryPane.java'
3063--- src/pipe/gui/widgets/QueryPane.java 2020-08-10 06:46:22 +0000
3064+++ src/pipe/gui/widgets/QueryPane.java 2020-08-19 11:36:17 +0000
3065@@ -372,7 +372,7 @@
3066 TAPNQuery newQuery = null;
3067
3068 if(q.isActive()) {
3069- if(q.getCategory() == TAPNQuery.QueryCategory.CTL) {
3070+ if(!tabContent.getLens().isTimed()) {
3071 newQuery = CTLQueryDialog.showQueryDialogue(CTLQueryDialog.QueryDialogueOption.Save, q, tabContent.network(), tabContent.getGuiModels(), tabContent.getLens());
3072 } else {
3073 newQuery = QueryDialog.showQueryDialogue(QueryDialogueOption.Save, q, tabContent.network(), tabContent.getGuiModels(), tabContent.getLens());
3074
3075=== modified file 'src/pipe/gui/widgets/TAPNTransitionEditor.java'
3076--- src/pipe/gui/widgets/TAPNTransitionEditor.java 2020-08-10 06:46:22 +0000
3077+++ src/pipe/gui/widgets/TAPNTransitionEditor.java 2020-08-19 11:36:17 +0000
3078@@ -16,8 +16,6 @@
3079 import javax.swing.JRootPane;
3080 import javax.swing.JTextField;
3081 import javax.swing.event.CaretListener;
3082-
3083-
3084 import net.tapaal.swinghelpers.GridBagHelper;
3085 import dk.aau.cs.gui.undo.*;
3086 import net.tapaal.swinghelpers.WidthAdjustingComboBox;
3087@@ -52,10 +50,16 @@
3088 transition = _transition;
3089 this.context = context;
3090 initComponents();
3091-
3092+ hideTimedInformation();
3093 rootPane.setDefaultButton(okButton);
3094 }
3095
3096+ private void hideTimedInformation(){
3097+ if(!transition.isTimed()) {
3098+ urgentCheckBox.setVisible(false);
3099+ }
3100+ }
3101+
3102 private void initComponents() {
3103 GridBagConstraints gridBagConstraints;
3104

Subscribers

People subscribed via source and target branches