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

[Lena Ernstsen]

Every digit of the token count is now visible

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.

[Jiri Srba (srba)]

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

[lp:~tapaal-contributor/tapaal/token-truncation-bug-1918913]

1123. By Lena Ernstsen on 2021-04-04

Added extra check for markings with more than 8 digits

1124. By Lena Ernstsen on 2021-04-04

Merged with trunk

Unmerged revisions

=== modified file 'src/pipe/gui/Pipe.java'
--- src/pipe/gui/Pipe.java	2021-04-04 09:14:06 +0000
+++ src/pipe/gui/Pipe.java	2021-04-04 09:32:12 +0000
@@ -83,5 +83,5 @@
 	public static final int AGE_DECIMAL_PRECISION = 5;
 	public static final int AGE_PRECISION = AGE_DECIMAL_PRECISION + 4;
 
-	public static final int MAX_NUMBER_OF_TOKENS_ALLOWED = 999;
+	public static final int MAX_NUMBER_OF_TOKENS_ALLOWED = 9999999;
 }

=== modified file 'src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java'
--- src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java	2020-08-19 11:34:44 +0000
+++ src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java	2021-04-04 09:32:12 +0000
@@ -254,9 +254,20 @@
                 case 0:
                     break;
                 default:
-                    if (marking > 999) {
-                        // XXX could be better...
-                        g.drawString("#" + marking, x, y + 20);
+                    if (marking > 99999999) {
+                        String subMarking1 = String.valueOf(marking).substring(0, 4);
+                        String subMarking2 = String.valueOf(marking).substring(4);
+                        g.drawString(">" + subMarking1, x - 5, y + 15);
+                        g.drawString(subMarking2, x + 4, y + 25);
+                    } else if (marking > 9999) {
+                        // XXX could be better...
+                        String subMarking1 = String.valueOf(marking).substring(0, 4);
+                        String subMarking2 = String.valueOf(marking).substring(4);
+                        g.drawString("#" + subMarking1, x - 5, y + 15);
+                        g.drawString(subMarking2, x + 4, y + 25);
+                    } else if (marking > 999) {
+                        // XXX could be better...
+                        g.drawString("#" + marking, x - 5, y + 20);
                     } else if (marking > 99) {
                         g.drawString("#" + marking, x, y + 20);
                     } else if (marking > 9) {