Merge lp:~tapaal-contributor/tapaal/fix-urgent-missing-check-1951292 into lp:tapaal

[Kristian Morsing Pedersen]

Now checks if valid action when toggeling a transition to urgent when pressing U, or using the draw menu

When selecting a transition and pressing U (or use the "Toggle urgent transition" in the draw menu), it now checks if the transition can be changed to urgent. It will display an error, if the action is invalid.

[Jiri Srba (srba)]

review: Approve

=== modified file 'src/dk/aau/cs/gui/TabContent.java'
--- src/dk/aau/cs/gui/TabContent.java	2021-11-05 14:11:49 +0000
+++ src/dk/aau/cs/gui/TabContent.java	2021-11-17 19:47:04 +0000
@@ -568,8 +568,12 @@
             for (PetriNetObject o : selection) {
                 if (o instanceof TimedTransitionComponent) {
                     TimedTransitionComponent transition = (TimedTransitionComponent) o;
+                    if(!transition.underlyingTransition().hasUntimedPreset()) {
+                        JOptionPane.showMessageDialog(null,"Incoming arcs to urgent transitions must have the interval [0,\u221e).", "Error", JOptionPane.ERROR_MESSAGE);
+                        return;
+                    }
+
                     Command cmd = new ToggleTransitionUrgent(transition.underlyingTransition(), currentTab);
-
                     cmd.redo();
                     getUndoManager().addEdit(cmd);
                 }
 
=== modified file 'src/pipe/gui/widgets/TAPNTransitionEditor.java'
--- src/pipe/gui/widgets/TAPNTransitionEditor.java	2021-08-24 08:23:25 +0000
+++ src/pipe/gui/widgets/TAPNTransitionEditor.java	2021-11-17 19:47:04 +0000
@@ -40,7 +40,7 @@
 
 public class TAPNTransitionEditor extends JPanel {
 
-	private static final String untimed_preset_warning = "Incoming arcs to urgent transitions must have the interval [0,inf).";
+	private static final String untimed_preset_warning = "Incoming arcs to urgent transitions must have the interval [0,\u221e).";
 	private static final String transport_destination_invariant_warning = "Transport arcs going through urgent transitions cannot have an invariant at the destination.";
 	private final TimedTransitionComponent transition;
 	private final JRootPane rootPane;