Merge lp:~tapaal-contributor/tapaal/fixInfSymbol-1945643 into lp:tapaal

[Kristian Morsing Pedersen]

Now uses the infinity symbol

No longer breaks the verification process

[Jiri Srba (srba)]

For some reason show/hide intervals [0,inf) in menu/View does not work anymore (but it works in trunk). To reproduce, open intro example (in File/example nets) and try to trigger the view options but the interval 2x[0,inf) is visible all the time.

review: Needs Fixing

[Jiri Srba (srba)]

This branch broke the verification - open for example intro example and verify the query, the engine returns and exception (probably the infinity symbol is sent to the engine but it should be only used in the GUI for visualization).

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/fixInfSymbol-1945643]

1152. By <email address hidden> on 2021-10-17

merged with trunk

[Jiri Srba (srba)]

Works as expected

review: Approve

=== modified file 'src/pipe/gui/GuiFrame.java'
--- src/pipe/gui/GuiFrame.java	2021-08-05 08:25:38 +0000
+++ src/pipe/gui/GuiFrame.java	2021-10-17 18:42:08 +0000
@@ -310,7 +310,7 @@
             guiFrameController.ifPresent(GuiFrameControllerActions::toggleConstants);
         }
     };
-    private final GuiAction showZeroToInfinityIntervalsAction = new GuiAction("Display intervals [0,inf)", "Show/hide intervals [0,inf) that do not restrict transition firing in any way.", KeyStroke.getKeyStroke('7', shortcutkey), true) {
+    private final GuiAction showZeroToInfinityIntervalsAction = new GuiAction("Display intervals [0," + Character.toString('\u221E') + ")", "Show/hide intervals [0," + Character.toString('\u221E') + ") that do not restrict transition firing in any way.", KeyStroke.getKeyStroke('7', shortcutkey), true) {
         public void actionPerformed(ActionEvent e) {
             guiFrameController.ifPresent(GuiFrameControllerActions::toggleZeroToInfinityIntervals);
         }

=== modified file 'src/pipe/gui/GuiFrameController.java'
--- src/pipe/gui/GuiFrameController.java	2021-09-30 14:12:33 +0000
+++ src/pipe/gui/GuiFrameController.java	2021-10-17 18:42:08 +0000
@@ -246,7 +246,7 @@
         buffer.append("TAPAAL GUI and Translations:\n");
             buffer.append("Mathias Andersen, Sine V. Birch, Jacob Hjort Bundgaard, Joakim Byg, Jakob Dyhr,\nLouise Foshammer, Malte Neve-Graesboell, ");
             buffer.append("Lasse Jacobsen, Morten Jacobsen,\nThomas S. Jacobsen, Jacob J. Jensen, Peter G. Jensen, ");
-            buffer.append("Mads Johannsen,\nKenneth Y. Joergensen, Mikael H. Moeller, Christoffer Moesgaard, Thomas Pedersen,\nLena Said, Niels N. Samuelsen, Jiri Srba, Mathias G. Soerensen, Jakob H. Taankvist\nand Peter H. Taankvist\n");
+            buffer.append("Mads Johannsen,\nKenneth Y. Joergensen, Mikael H. Moeller, Christoffer Moesgaard, Kristian Morsing Pedersen,\nThomas Pedersen, Lena Said, Niels N. Samuelsen, Jiri Srba, Mathias G. Soerensen,\nJakob H. Taankvist and Peter H. Taankvist\n");
 
             buffer.append("Aalborg University 2008-2021\n\n");
 

=== modified file 'src/pipe/gui/graphicElements/tapn/TimedInputArcComponent.java'
--- src/pipe/gui/graphicElements/tapn/TimedInputArcComponent.java	2020-09-10 08:59:28 +0000
+++ src/pipe/gui/graphicElements/tapn/TimedInputArcComponent.java	2021-10-17 18:42:08 +0000
@@ -102,6 +102,11 @@
                 getNameLabel().setText(inputArc.interval().toString(showConstantNames));
             }
 
+            if(getNameLabel().getText().contains("inf")) {
+                String intervalStringWithInfSymbol = getNameLabel().getText().replace("inf", Character.toString('\u221e'));
+                getNameLabel().setText(intervalStringWithInfSymbol);
+            }
+
             getNameLabel().setText(getWeight().toString(showConstantNames)+" "+getNameLabel().getText());
 
             // Handle constant highlighting

=== modified file 'src/pipe/gui/graphicElements/tapn/TimedTransportArcComponent.java'
--- src/pipe/gui/graphicElements/tapn/TimedTransportArcComponent.java	2020-09-10 08:59:28 +0000
+++ src/pipe/gui/graphicElements/tapn/TimedTransportArcComponent.java	2021-10-17 18:42:08 +0000
@@ -107,13 +107,14 @@
 				getNameLabel().setText(underlyingTransportArc.interval().toString(
 						displayConstantNames)
 						+ " : " + getGroup());
+                if(getNameLabel().getText().contains("inf")) {
+                    String intervalStringWithInfSymbol = getNameLabel().getText().replace("inf", Character.toString('\u221e'));
+                    getNameLabel().setText(intervalStringWithInfSymbol);
+                }
 			}
 			else {
-				if (underlyingTransportArc.interval().toString(
-						displayConstantNames).equals("[0,inf)")) {
-
+				if (underlyingTransportArc.interval().toString(displayConstantNames).equals("[0,inf)")) {
 					getNameLabel().setText(" : " + getGroup());
-
 				}
 				else {
 					getNameLabel().setText(underlyingTransportArc.interval().toString(

=== modified file 'src/pipe/gui/widgets/GuardDialogue.java'
--- src/pipe/gui/widgets/GuardDialogue.java	2021-08-24 09:32:59 +0000
+++ src/pipe/gui/widgets/GuardDialogue.java	2021-10-17 18:42:08 +0000
@@ -133,7 +133,7 @@
 				if(objectToBeEdited instanceof TimedInputArcComponent && !(objectToBeEdited instanceof TimedInhibitorArcComponent)
 						&& ((TimedInputArcComponent) objectToBeEdited).isUrgentTransition()){
 					if(!guard.equals(TimeInterval.ZERO_INF)){
-						JOptionPane.showMessageDialog(myRootPane, "Incoming arcs to urgent transitions must have the interval [0,inf).", "Error", JOptionPane.ERROR_MESSAGE);
+						JOptionPane.showMessageDialog(myRootPane, "Incoming arcs to urgent transitions must have the interval [0," + Character.toString('\u221E') + ")", "Error", JOptionPane.ERROR_MESSAGE);
 						return;
 					}
 				}
@@ -347,7 +347,7 @@
 		gridBagConstraints.gridy = 1;
 		guardEditPanel.add(rightDelimiter, gridBagConstraints);
 
-		inf = new JCheckBox("inf", true);
+		inf = new JCheckBox(Character.toString('\u221e'), true);
 		inf.addActionListener(evt -> {
 			if (inf.isSelected()) {
 				secondIntervalNumber.setEnabled(false);

=== modified file 'src/pipe/gui/widgets/PlaceEditorPanel.java'
--- src/pipe/gui/widgets/PlaceEditorPanel.java	2021-08-24 08:23:25 +0000
+++ src/pipe/gui/widgets/PlaceEditorPanel.java	2021-10-17 18:42:08 +0000
@@ -332,7 +332,7 @@
 		gbc = GridBagHelper.as(2,0, new Insets(3, 3, 3, 3));
 		invariantGroup.add(invariantSpinner, gbc);
 
-		invariantInf = new JCheckBox("inf");
+		invariantInf = new JCheckBox(Character.toString('\u221e'));
 		invariantInf.addActionListener(arg0 -> {
 			if(!isUrgencyOK()){
 				invariantInf.setSelected(true);