Merge lp:~tapaal-contributor/tapaal/token-truncation-bug-1918913 into lp:tapaal

Proposed by Lena Said
Status: Merged
Approved by: Jiri Srba
Approved revision: 1124
Merged at revision: 1126
Proposed branch: lp:~tapaal-contributor/tapaal/token-truncation-bug-1918913
Merge into: lp:tapaal
Diff against target: 38 lines (+15/-4)
2 files modified
src/pipe/gui/Pipe.java (+1/-1)
src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java (+14/-3)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/token-truncation-bug-1918913
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Review via email: mp+400594@code.launchpad.net

This proposal supersedes a proposal from 2021-03-27.

Commit message

Every digit of the token count is now visible

Description of the change

Made it possible to see more than the 3 most significant digits for the token counts.
However, maximum number of digits is 8, as an "out of memory" error appears with 9 or more digits.

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

It looks as an okay solution. Can the limit of 999 tokens when drawing the net in GUI be increased to say 99999999 tokens? Should some net exceed it when loading, then print >9999 9999 instead of #9999 9999 (just to be sure).

review: Needs Fixing
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/pipe/gui/Pipe.java'
2--- src/pipe/gui/Pipe.java 2021-04-04 09:14:06 +0000
3+++ src/pipe/gui/Pipe.java 2021-04-04 09:43:34 +0000
4@@ -83,5 +83,5 @@
5 public static final int AGE_DECIMAL_PRECISION = 5;
6 public static final int AGE_PRECISION = AGE_DECIMAL_PRECISION + 4;
7
8- public static final int MAX_NUMBER_OF_TOKENS_ALLOWED = 999;
9+ public static final int MAX_NUMBER_OF_TOKENS_ALLOWED = 9999999;
10 }
11
12=== modified file 'src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java'
13--- src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java 2020-08-19 11:34:44 +0000
14+++ src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java 2021-04-04 09:43:34 +0000
15@@ -254,9 +254,20 @@
16 case 0:
17 break;
18 default:
19- if (marking > 999) {
20- // XXX could be better...
21- g.drawString("#" + marking, x, y + 20);
22+ if (marking > 99999999) {
23+ String subMarking1 = String.valueOf(marking).substring(0, 4);
24+ String subMarking2 = String.valueOf(marking).substring(4);
25+ g.drawString(">" + subMarking1, x - 5, y + 15);
26+ g.drawString(subMarking2, x + 4, y + 25);
27+ } else if (marking > 9999) {
28+ // XXX could be better...
29+ String subMarking1 = String.valueOf(marking).substring(0, 4);
30+ String subMarking2 = String.valueOf(marking).substring(4);
31+ g.drawString("#" + subMarking1, x - 5, y + 15);
32+ g.drawString(subMarking2, x + 4, y + 25);
33+ } else if (marking > 999) {
34+ // XXX could be better...
35+ g.drawString("#" + marking, x - 5, y + 20);
36 } else if (marking > 99) {
37 g.drawString("#" + marking, x, y + 20);
38 } else if (marking > 9) {

Subscribers

People subscribed via source and target branches