Merge lp:~tapaal-contributor/tapaal/hide-show-names-1921393 into lp:tapaal

[Lena Ernstsen]

Visibility of all place/transition names can be changed through the view menu

Place/transition names stay hidden when opening new nets and when switching tabs and templates.

Go to the view menu and then press "Change visibility of transition/place names". This will open a dialog, where you choose which options you want. When pressing "ok", the changes will be executed.
When entering the dialog again, the dialog will remember the options selected last time it was closed.

It is also possible to undo/redo the change of visibility.

[Jiri Srba (srba)]

Open Intro example, select "hide place names" and the names disappear. Then click on the editing surface and the names appear again.

Also, select e.g. Place P2 and unclick in the dialog "Show place name". The disable showing place names and enable it again in the view menu. Showing the name for P2 should be still disabled. This should have a priority over "show place names" in the view menu (i.e. if explicitly disabled, it should not show the place names at all). The same for transitions.

To make the semantics more clear, perhaps rename the View items to "Hide place names" and "Hide transition names" and leave them initially unselected (i.g. a normal behaviour). When you select the "hide" menu option, all transition or place names should be hidden, once you deselect it again, it should return to normal behaviour (i.e. depending on the choice made in the place/transition editing dialog).

Also, when you open a new net, the View options for these two items should be set to default (showing the names).

review: Needs Fixing

[Jiri Srba (srba)]

The logics is broken. Run TAPAAL (notice that hide place/transitions names is set even though
it should not be), open a new net and go to view menu and click on "hide place names" which is now selected. Try to draw a new place and transition. The place has a name (even though it should not) and the transition does not have a name (even though it should).

review: Needs Fixing

[Jiri Srba (srba)]

Undo is broken: to reproduce open intro example, use the dialog to hide both place/transition names and then manually show the name of one selected place. Then try to undo and nothing happens (the selected place should be now without name).

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/hide-show-names-1921393]

1145. By Lena Ernstsen on 2021-08-03

Changed tooltip for 'Merge Composed Net'

1146. By Lena Ernstsen on 2021-08-03

Changed tooltip for 'Merge Composed Net'

[Jiri Srba (srba)]

review: Approve

=== modified file 'src/dk/aau/cs/gui/TabContent.java'
--- src/dk/aau/cs/gui/TabContent.java	2020-10-30 21:14:42 +0000
+++ src/dk/aau/cs/gui/TabContent.java	2021-08-03 09:29:22 +0000
@@ -16,6 +16,7 @@
 import dk.aau.cs.TCTL.*;
 import dk.aau.cs.debug.Logger;
 import dk.aau.cs.gui.components.BugHandledJXMultisplitPane;
+import dk.aau.cs.gui.components.NameVisibilityPanel;
 import dk.aau.cs.gui.components.StatisticsPanel;
 import dk.aau.cs.gui.components.TransitionFireingComponent;
 import dk.aau.cs.gui.undo.*;
@@ -843,8 +844,14 @@
 	
 	private WorkflowDialog workflowDialog = null;
 
-
-	private TabContent(boolean isTimed, boolean isGame) {
+	private NameVisibilityPanel nameVisibilityPanel = null;
+
+    private Boolean showNamesOption = null;
+    private Boolean isSelectedComponentOption = null;
+    private Boolean isPlaceOption = null;
+    private Boolean isTransitionOption = null;
+
+    private TabContent(boolean isTimed, boolean isGame) {
 	    this(new TimedArcPetriNetNetwork(), new ArrayList<>(), new TAPNLens(isTimed,isGame));
     }
 
@@ -903,6 +910,8 @@
         this.setDividerSize(8);
         //XXX must be after the animationcontroller is created
         animationModeController = new CanvasAnimationController(getAnimator());
+
+        nameVisibilityPanel = new NameVisibilityPanel(this);
     }
 
 	public TabContent(TimedArcPetriNetNetwork network, Collection<Template> templates, Iterable<TAPNQuery> tapnqueries, TAPNLens lens) {
@@ -1621,6 +1630,39 @@
         }
     }
 
+    @Override
+    public Map<PetriNetObject, Boolean> showNames(boolean showNames, boolean placeNames, boolean selectedComponent) {
+        Map<PetriNetObject, Boolean> map = new HashMap<>();
+        List<PetriNetObject> components = new ArrayList<>();
+
+	    if (selectedComponent) {
+	        Template template = currentTemplate();
+	        template.guiModel().getPetriNetObjects().forEach(components::add);
+        } else {
+            Iterable<Template> templates = allTemplates();
+            for (Template template : templates) {
+                template.guiModel().getPetriNetObjects().forEach(components::add);
+            }
+        }
+
+        for (Component component : components) {
+            if (placeNames && component instanceof TimedPlaceComponent) {
+                TimedPlaceComponent place = (TimedPlaceComponent) component;
+                map.put(place, place.getAttributesVisible());
+                place.setAttributesVisible(showNames);
+                place.update(true);
+                repaint();
+            } else if (!placeNames && component instanceof TimedTransitionComponent) {
+                TimedTransitionComponent transition = (TimedTransitionComponent) component;
+                map.put(transition, transition.getAttributesVisible());
+                transition.setAttributesVisible(showNames);
+                transition.update(true);
+                repaint();
+            }
+        }
+        return map;
+	}
+
     public static Split getEditorModelRoot(){
 		return editorModelroot;
 	}
@@ -1839,6 +1881,21 @@
         StatisticsPanel.showStatisticsPanel(drawingSurface().getModel().getStatistics());
 	}
 
+    @Override
+    public void showChangeNameVisibility() {
+	    NameVisibilityPanel panel = new NameVisibilityPanel(this);
+	    if (showNamesOption != null && isSelectedComponentOption != null && isPlaceOption != null && isTransitionOption != null) {
+            panel.showNameVisibilityPanel(showNamesOption, isPlaceOption, isTransitionOption, isSelectedComponentOption);
+        } else {
+            panel.showNameVisibilityPanel();
+        }
+
+        showNamesOption = panel.isShowNamesOption();
+        isPlaceOption = panel.isPlaceOption();
+        isTransitionOption = panel.isTransitionOption();
+        isSelectedComponentOption = panel.isSelectedComponentOption();
+    }
+
 	@Override
 	public void importSUMOQueries() {
 		File[] files = FileBrowser.constructor("Import SUMO", "txt", FileBrowser.userPath).openFiles();
 
=== modified file 'src/dk/aau/cs/gui/TabContentActions.java'
--- src/dk/aau/cs/gui/TabContentActions.java	2020-08-11 11:51:55 +0000
+++ src/dk/aau/cs/gui/TabContentActions.java	2021-08-03 09:29:22 +0000
@@ -4,8 +4,10 @@
 import pipe.gui.GuiFrameActions;
 import pipe.gui.Pipe;
 import pipe.gui.SafeGuiFrameActions;
+import pipe.gui.graphicElements.PetriNetObject;
 
 import java.io.File;
+import java.util.Map;
 
 public interface TabContentActions {
 
@@ -96,4 +98,9 @@
 
     void changeGameFeature(boolean isGame);
 
+    Map<PetriNetObject, Boolean> showNames(boolean isVisible, boolean placeNames, boolean selectedComponent);
+
+    void showChangeNameVisibility();
+
+
 }
 
=== added file 'src/dk/aau/cs/gui/components/NameVisibilityPanel.java'
--- src/dk/aau/cs/gui/components/NameVisibilityPanel.java	1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/gui/components/NameVisibilityPanel.java	2021-08-03 09:29:22 +0000
@@ -0,0 +1,247 @@
+package dk.aau.cs.gui.components;
+
+import dk.aau.cs.gui.TabContent;
+import dk.aau.cs.gui.undo.ChangeAllNamesVisibilityCommand;
+import dk.aau.cs.gui.undo.Command;
+import pipe.gui.graphicElements.PetriNetObject;
+
+import javax.swing.*;
+import java.awt.*;
+import java.util.HashMap;
+import java.util.Map;
+
+public class NameVisibilityPanel extends JPanel {
+    private static final String DIALOG_TITLE = "Change Name Visibility";
+
+    private static JDialog dialog;
+    private JRadioButton showNames;
+    private JRadioButton hideNames;
+    private JRadioButton placeOption;
+    private JRadioButton transitionOption;
+    private JRadioButton bothOption;
+    private JRadioButton selectedComponent;
+    private JRadioButton allComponents;
+
+    ButtonGroup visibilityRadioButtonGroup;
+    ButtonGroup objectRadioButtonGroup;
+    ButtonGroup componentRadioButtonGroup;
+
+    JPanel visibilityPanel;
+    JPanel placeTransitionPanel;
+    JPanel componentPanel;
+
+    private final TabContent tab;
+
+    public NameVisibilityPanel(TabContent tab) {
+        super(new GridBagLayout());
+
+        this.tab = tab;
+
+        init();
+    }
+
+    public void showNameVisibilityPanel() {
+        JOptionPane optionPane = new JOptionPane(this, JOptionPane.INFORMATION_MESSAGE);
+
+        dialog = optionPane.createDialog(DIALOG_TITLE);
+        dialog.pack();
+        dialog.setVisible(true);
+
+        Object selectedValue = optionPane.getValue();
+
+        if (selectedValue != null) ChangeNameVisibilityBasedOnSelection();
+    }
+
+    public void showNameVisibilityPanel(boolean isVisible, boolean isPlace, boolean isTransition, boolean isSelectedComponent) {
+        JOptionPane optionPane = new JOptionPane(this, JOptionPane.INFORMATION_MESSAGE);
+
+        showNames.setSelected(isVisible);
+        hideNames.setSelected(!isVisible);
+        placeOption.setSelected(isPlace && !isTransition);
+        transitionOption.setSelected(isTransition && !isPlace);
+        bothOption.setSelected(isPlace && isTransition);
+        selectedComponent.setSelected(isSelectedComponent);
+        allComponents.setSelected(!isSelectedComponent);
+
+        dialog = optionPane.createDialog(DIALOG_TITLE);
+        dialog.pack();
+        dialog.setVisible(true);
+
+        Object selectedValue = optionPane.getValue();
+
+        if (selectedValue != null) ChangeNameVisibilityBasedOnSelection();
+    }
+
+    private void init() {
+        visibilityPanel = initVisibilityOptions();
+        placeTransitionPanel = initPlaceTransitionOptions();
+        componentPanel = initComponentOptions();
+
+        GridBagConstraints gbc = new GridBagConstraints();
+        gbc.gridx = 0;
+        gbc.gridy = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        gbc.gridwidth = 3;
+        gbc.insets = new Insets(5, 5, 5, 5);
+
+        this.add(visibilityPanel, gbc);
+        gbc.gridy = 1;
+        this.add(placeTransitionPanel, gbc);
+        gbc.gridy = 2;
+        this.add(componentPanel, gbc);
+
+        this.setVisible(true);
+    }
+
+    private JPanel initVisibilityOptions() {
+        JPanel panel = new JPanel(new GridBagLayout());
+        visibilityRadioButtonGroup = new ButtonGroup();
+
+        JLabel text = new JLabel("Choose visibility:       ");
+        GridBagConstraints gbc = new GridBagConstraints();
+        gbc.gridx = 0;
+        gbc.gridy = 0;
+        gbc.weightx = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        gbc.insets = new Insets(3, 3, 3, 3);
+        panel.add(text, gbc);
+
+        showNames = new JRadioButton("Show");
+        showNames.setSelected(true);
+        gbc = new GridBagConstraints();
+        gbc.gridx = 1;
+        gbc.gridy = 0;
+        gbc.weightx = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        gbc.insets = new Insets(3, 3, 3, 3);
+        panel.add(showNames, gbc);
+        visibilityRadioButtonGroup.add(showNames);
+
+        hideNames = new JRadioButton("Hide");
+        gbc = new GridBagConstraints();
+        gbc.gridx = 2;
+        gbc.gridy = 0;
+        gbc.weightx = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        gbc.insets = new Insets(3, 3, 3, 3);
+        panel.add(hideNames, gbc);
+        visibilityRadioButtonGroup.add(hideNames);
+
+        return panel;
+    }
+
+    private JPanel initPlaceTransitionOptions() {
+        JPanel panel = new JPanel(new GridBagLayout());
+        objectRadioButtonGroup = new ButtonGroup();
+
+        JLabel text = new JLabel("Choose group:           ");
+        GridBagConstraints gbc = new GridBagConstraints();
+        gbc.gridx = 0;
+        gbc.gridy = 0;
+        gbc.weightx = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        gbc.insets = new Insets(3, 3, 3, 3);
+        panel.add(text, gbc);
+
+        placeOption = new JRadioButton("Places");
+        placeOption.setSelected(true);
+        gbc = new GridBagConstraints();
+        gbc.gridx = 1;
+        gbc.gridy = 0;
+        gbc.weightx = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        gbc.insets = new Insets(3, 3, 3, 3);
+        panel.add(placeOption, gbc);
+        objectRadioButtonGroup.add(placeOption);
+
+        transitionOption = new JRadioButton("Transitions");
+        gbc = new GridBagConstraints();
+        gbc.gridx = 2;
+        gbc.gridy = 0;
+        gbc.weightx = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        gbc.insets = new Insets(3, 3, 3, 3);
+        panel.add(transitionOption, gbc);
+        objectRadioButtonGroup.add(transitionOption);
+
+        bothOption = new JRadioButton("Both");
+        gbc = new GridBagConstraints();
+        gbc.gridx = 3;
+        gbc.gridy = 0;
+        gbc.weightx = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        gbc.insets = new Insets(3, 3, 3, 3);
+        panel.add(bothOption, gbc);
+        objectRadioButtonGroup.add(bothOption);
+
+        return panel;
+    }
+
+    private JPanel initComponentOptions() {
+        JPanel panel = new JPanel(new GridBagLayout());
+        componentRadioButtonGroup = new ButtonGroup();
+
+        JLabel text = new JLabel("Choose components: ");
+        GridBagConstraints gbc = new GridBagConstraints();
+        gbc.gridx = 0;
+        gbc.gridy = 0;
+        gbc.weightx = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        gbc.insets = new Insets(3, 3, 3, 3);
+        panel.add(text, gbc);
+
+        selectedComponent = new JRadioButton("Selected component");
+        selectedComponent.setSelected(true);
+        gbc = new GridBagConstraints();
+        gbc.gridx = 1;
+        gbc.gridy = 0;
+        gbc.weightx = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        gbc.insets = new Insets(3, 3, 3, 3);
+        panel.add(selectedComponent, gbc);
+        componentRadioButtonGroup.add(selectedComponent);
+
+        allComponents = new JRadioButton("All components");
+        gbc = new GridBagConstraints();
+        gbc.gridx = 2;
+        gbc.gridy = 0;
+        gbc.weightx = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        gbc.insets = new Insets(3, 3, 3, 3);
+        panel.add(allComponents, gbc);
+        componentRadioButtonGroup.add(allComponents);
+
+        return panel;
+    }
+
+    protected void ChangeNameVisibilityBasedOnSelection() {
+        Map<PetriNetObject, Boolean> places = new HashMap<>();
+        Map<PetriNetObject, Boolean> transitions = new HashMap<>();
+
+        if (placeOption.isSelected() || bothOption.isSelected()) {
+           places = tab.showNames(showNames.isSelected(), true, selectedComponent.isSelected());
+        }
+        if (transitionOption.isSelected() || bothOption.isSelected()) {
+            transitions = tab.showNames(showNames.isSelected(), false, selectedComponent.isSelected());
+        }
+
+        Command changeVisibilityCommand = new ChangeAllNamesVisibilityCommand(tab, places, transitions, showNames.isSelected());
+        tab.getUndoManager().addNewEdit(changeVisibilityCommand);
+    }
+
+    public boolean isShowNamesOption() {
+        return showNames.isSelected();
+    }
+
+    public boolean isSelectedComponentOption() {
+        return selectedComponent.isSelected();
+    }
+
+    public boolean isPlaceOption() {
+        return placeOption.isSelected() || bothOption.isSelected();
+    }
+
+    public boolean isTransitionOption() {
+        return transitionOption.isSelected() || bothOption.isSelected();
+    }
+}
 
=== added file 'src/dk/aau/cs/gui/undo/ChangeAllNamesVisibilityCommand.java'
--- src/dk/aau/cs/gui/undo/ChangeAllNamesVisibilityCommand.java	1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/gui/undo/ChangeAllNamesVisibilityCommand.java	2021-08-03 09:29:22 +0000
@@ -0,0 +1,70 @@
+package dk.aau.cs.gui.undo;
+
+import dk.aau.cs.gui.TabContent;
+import pipe.gui.graphicElements.PetriNetObject;
+import pipe.gui.graphicElements.tapn.TimedPlaceComponent;
+import pipe.gui.graphicElements.tapn.TimedTransitionComponent;
+
+import java.util.Map;
+
+public class ChangeAllNamesVisibilityCommand extends Command {
+    private final Map<PetriNetObject, Boolean> places;
+    private final Map<PetriNetObject, Boolean> transitions;
+    private final boolean isVisible;
+	private final TabContent tabContent;
+
+	public ChangeAllNamesVisibilityCommand(TabContent tabContent, Map<PetriNetObject, Boolean> places, Map<PetriNetObject, Boolean> transitions, boolean isVisible) {
+		this.tabContent = tabContent;
+		this.places = places;
+		this.transitions= transitions;
+		this.isVisible = isVisible;
+	}
+
+	@Override
+	public void redo() {
+	    if (places != null) {
+            for (PetriNetObject place : places.keySet()) {
+                if (place instanceof TimedPlaceComponent) {
+                    TimedPlaceComponent component = (TimedPlaceComponent) place;
+                    component.setAttributesVisible(isVisible);
+                    component.update(true);
+                    tabContent.repaint();
+                }
+            }
+        }
+        if (transitions != null) {
+            for (PetriNetObject transition : transitions.keySet()) {
+                if (transition instanceof TimedTransitionComponent) {
+                    TimedTransitionComponent component = (TimedTransitionComponent) transition;
+                    component.setAttributesVisible(isVisible);
+                    component.update(true);
+                    tabContent.repaint();
+                }
+            }
+        }
+	}
+
+	@Override
+	public void undo() {
+        if (places != null) {
+            for (PetriNetObject place : places.keySet()) {
+                if (place instanceof TimedPlaceComponent) {
+                    TimedPlaceComponent component = (TimedPlaceComponent) place;
+                    component.setAttributesVisible(places.get(component));
+                    component.update(true);
+                    tabContent.repaint();
+                }
+            }
+        }
+        if (transitions != null) {
+            for (PetriNetObject transition : transitions.keySet()) {
+                if (transition instanceof TimedTransitionComponent) {
+                    TimedTransitionComponent component = (TimedTransitionComponent) transition;
+                    component.setAttributesVisible(transitions.get(component));
+                    component.update(true);
+                    tabContent.repaint();
+                }
+            }
+        }
+	}
+}
 
=== modified file 'src/dk/aau/cs/gui/undo/RenameTimedPlaceCommand.java'
--- src/dk/aau/cs/gui/undo/RenameTimedPlaceCommand.java	2011-03-12 12:12:12 +0000
+++ src/dk/aau/cs/gui/undo/RenameTimedPlaceCommand.java	2021-08-03 09:29:22 +0000
@@ -22,13 +22,13 @@
 	public void redo() {
 		place.setName(newName);
 		updateQueries(oldName, newName);
-	}
+    }
 
 	@Override
 	public void undo() {
 		place.setName(oldName);
 		updateQueries(newName,oldName);
-	}
+    }
 	
 	private void updateQueries(String nameToFind, String nameToInsert){
 		RenamePlaceTCTLVisitor renameVisitor = new RenamePlaceTCTLVisitor(nameToFind, nameToInsert);
 
=== modified file 'src/pipe/gui/GuiFrame.java'
--- src/pipe/gui/GuiFrame.java	2021-04-08 08:39:05 +0000
+++ src/pipe/gui/GuiFrame.java	2021-08-03 09:29:22 +0000
@@ -18,10 +18,8 @@
 
 import com.sun.jna.Platform;
 import dk.aau.cs.gui.*;
-import dk.aau.cs.model.tapn.TimedArcPetriNet;
 import dk.aau.cs.util.JavaUtil;
 import dk.aau.cs.verification.VerifyTAPN.VerifyPN;
-import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNExporter;
 import net.tapaal.Preferences;
 import net.tapaal.TAPAAL;
 import net.tapaal.helpers.Reference.MutableReference;
@@ -30,10 +28,8 @@
 import net.tapaal.swinghelpers.SwingHelper;
 import net.tapaal.swinghelpers.ToggleButtonWithoutText;
 import org.jetbrains.annotations.NotNull;
-import pipe.dataLayer.TAPNQuery;
 import pipe.gui.Pipe.ElementType;
 import pipe.gui.action.GuiAction;
-import pipe.gui.widgets.WorkflowDialog;
 import dk.aau.cs.debug.Logger;
 import dk.aau.cs.gui.smartDraw.SmartDrawDialog;
 import net.tapaal.resourcemanager.ResourceManager;
@@ -241,7 +237,7 @@
             SmartDrawDialog.showSmartDrawDialog();
         }
     };
-    private final GuiAction mergeComponentsDialogAction = new GuiAction("Merge net components", "Export an xml file of composed net and approximated net if enabled", KeyStroke.getKeyStroke(KeyEvent.VK_C, (shortcutkey + InputEvent.SHIFT_MASK))) {
+    private final GuiAction mergeComponentsDialogAction = new GuiAction("Merge net components", "Open a composed net in a new tab and use approximated net if enabled", KeyStroke.getKeyStroke(KeyEvent.VK_C, (shortcutkey + InputEvent.SHIFT_MASK))) {
         public void actionPerformed(ActionEvent e) {
             currentTab.ifPresent(TabContentActions::mergeNetComponents);
         }
@@ -334,6 +330,11 @@
             guiFrameController.ifPresent(GuiFrameControllerActions::toggleDisplayToolTips);
         }
     };
+    private final GuiAction changeNameVisibility = new GuiAction("Change visibility of transition/place names", "Executing this action will open a dialog where you can hide or show place and transition names", true) {
+        public void actionPerformed(ActionEvent e) {
+            currentTab.ifPresent(TabContentActions::showChangeNameVisibility);
+        }
+    };
     private final GuiAction showAdvancedWorkspaceAction = new GuiAction("Show advanced workspace", "Show all panels", false) {
         public void actionPerformed(ActionEvent e) {
             guiFrameController.ifPresent(GuiFrameControllerActions::showAdvancedWorkspace);
@@ -677,6 +678,10 @@
 
         viewMenu.addSeparator();
 
+        viewMenu.add(changeNameVisibility);
+
+        viewMenu.addSeparator();
+
         viewMenu.add(showSimpleWorkspaceAction);
         viewMenu.add(showAdvancedWorkspaceAction);
         viewMenu.add(saveWorkSpaceAction);
@@ -1066,6 +1071,7 @@
         showDelayEnabledTransitionsAction.setEnabled(enable);
         showToolTipsAction.setEnabled(enable);
         showTokenAgeAction.setEnabled(enable);
+        changeNameVisibility.setEnabled(enable);
         showAdvancedWorkspaceAction.setEnabled(enable);
         showSimpleWorkspaceAction.setEnabled(enable);
         saveWorkSpaceAction.setEnabled(enable);
 
=== modified file 'src/pipe/gui/GuiFrameActions.java'
--- src/pipe/gui/GuiFrameActions.java	2020-08-11 11:51:55 +0000
+++ src/pipe/gui/GuiFrameActions.java	2021-08-03 09:29:22 +0000
@@ -47,7 +47,7 @@
     void setShowQueriesSelected(boolean b);
     void setShowEnabledTransitionsSelected(boolean b);
     void setShowDelayEnabledTransitionsSelected(boolean b);
-    void setShowToolTipsSelected(boolean b);
+    void setShowToolTipsSelected(boolean b);;
     void setShowZeroToInfinityIntervalsSelected(boolean b);
     void setShowTokenAgeSelected(boolean b);
 
 
=== modified file 'src/pipe/gui/GuiFrameController.java'
--- src/pipe/gui/GuiFrameController.java	2021-04-05 10:10:17 +0000
+++ src/pipe/gui/GuiFrameController.java	2021-08-03 09:29:22 +0000
@@ -113,7 +113,6 @@
         guiFrame.changeToTab(tab);
         //XXX fixes an issue where on first open of a net the time intervals are not shown
         tab.drawingSurface().repaintAll();
-
     }
 
     //If needed, add boolean forceClose, where net is not checkedForSave and just closed
 
=== modified file 'src/pipe/gui/canvas/DrawingSurfaceImpl.java'
--- src/pipe/gui/canvas/DrawingSurfaceImpl.java	2020-08-11 06:00:12 +0000
+++ src/pipe/gui/canvas/DrawingSurfaceImpl.java	2021-08-03 09:29:22 +0000
@@ -495,9 +495,11 @@
 
 
 	public void translateSelection(ArrayList<PetriNetObject> objects, int transX, int transY) {
-		tabContent.getUndoManager().newEdit(); // new "transaction""
-		for (PetriNetObject pnobject : objects) {
-			tabContent.getUndoManager().addEdit(new TranslatePetriNetObjectEdit(pnobject, transX, transY, this));
-		}
+		if (transX != 0 || transY != 0) {
+            tabContent.getUndoManager().newEdit(); // new "transaction""
+            for (PetriNetObject pnobject : objects) {
+                tabContent.getUndoManager().addEdit(new TranslatePetriNetObjectEdit(pnobject, transX, transY, this));
+            }
+        }
 	}
 }
 
=== modified file 'src/pipe/gui/graphicElements/PlaceTransitionObject.java'
--- src/pipe/gui/graphicElements/PlaceTransitionObject.java	2020-08-20 20:45:38 +0000
+++ src/pipe/gui/graphicElements/PlaceTransitionObject.java	2021-08-03 09:29:22 +0000
@@ -19,9 +19,9 @@
 	private final LinkedList<Arc> connectTo = new LinkedList<Arc>();
 	private final LinkedList<Arc> connectFrom = new LinkedList<Arc>();
 
-	protected boolean attributesVisible = false;
+	protected boolean attributesVisible = true;
 
-	public PlaceTransitionObject(
+    public PlaceTransitionObject(
 	        double componentWidth,
 			double componentHeight,
 			int positionXInput,
 
=== modified file 'src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java'
--- src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java	2021-04-04 09:31:12 +0000
+++ src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java	2021-08-03 09:29:22 +0000
@@ -55,7 +55,6 @@
 		this.place = place;
         this.place.addTimedPlaceListener(listener);
         this.lens = lens;
-		attributesVisible = true;
 
     }
 
 
=== modified file 'src/pipe/gui/graphicElements/tapn/TimedTransitionComponent.java'
--- src/pipe/gui/graphicElements/tapn/TimedTransitionComponent.java	2020-08-19 11:36:09 +0000
+++ src/pipe/gui/graphicElements/tapn/TimedTransitionComponent.java	2021-08-03 09:29:22 +0000
@@ -42,7 +42,6 @@
 		this.transition = transition;
 		listener = timedTransitionListener();
 		transition.addTimedTransitionListener(listener);
-		attributesVisible = true;
 		this.lens = lens;
 
 	}
 
=== modified file 'src/pipe/gui/widgets/PlaceEditorPanel.java'
--- src/pipe/gui/widgets/PlaceEditorPanel.java	2021-04-08 08:30:29 +0000
+++ src/pipe/gui/widgets/PlaceEditorPanel.java	2021-08-03 09:29:22 +0000
@@ -6,10 +6,7 @@
 import java.awt.GridBagLayout;
 import java.awt.Insets;
 import java.awt.event.ItemEvent;
-import java.util.Arrays;
-import java.util.Collection;
-import java.util.Set;
-import java.util.Vector;
+import java.util.*;
 
 import javax.swing.ButtonGroup;
 import javax.swing.DefaultComboBoxModel;
@@ -23,6 +20,7 @@
 import javax.swing.event.ChangeListener;
 
 import dk.aau.cs.gui.TabContent;
+import dk.aau.cs.gui.undo.*;
 import net.tapaal.swinghelpers.CustomJSpinner;
 import net.tapaal.swinghelpers.GridBagHelper;
 import net.tapaal.swinghelpers.SwingHelper;
@@ -30,16 +28,9 @@
 import pipe.dataLayer.Template;
 import pipe.gui.CreateGui;
 import pipe.gui.Pipe;
+import pipe.gui.graphicElements.PetriNetObject;
 import pipe.gui.graphicElements.tapn.TimedPlaceComponent;
 import dk.aau.cs.gui.Context;
-import dk.aau.cs.gui.undo.ChangedInvariantCommand;
-import dk.aau.cs.gui.undo.Command;
-import dk.aau.cs.gui.undo.MakePlaceSharedCommand;
-import dk.aau.cs.gui.undo.MakePlaceNewSharedCommand;
-import dk.aau.cs.gui.undo.MakePlaceNewSharedMultiCommand;
-import dk.aau.cs.gui.undo.RenameTimedPlaceCommand;
-import dk.aau.cs.gui.undo.TimedPlaceMarkingEdit;
-import dk.aau.cs.gui.undo.UnsharePlaceCommand;
 import dk.aau.cs.model.tapn.Bound.InfBound;
 import dk.aau.cs.model.tapn.Constant;
 import dk.aau.cs.model.tapn.ConstantBound;
@@ -585,17 +576,19 @@
 				JOptionPane.showMessageDialog(this, "The specified name is already used by another place or transition.", "Error", JOptionPane.ERROR_MESSAGE);
 				return false;
 			}   	
-			
-			Command renameCommand = new RenameTimedPlaceCommand(context.tabContent(), (LocalTimedPlace)place.underlyingPlace(), oldName, newName);
-			context.undoManager().addEdit(renameCommand);
-			try{ // set name
-				renameCommand.redo();
-			}catch(RequireException e){
-				context.undoManager().undo(); 
-				JOptionPane.showMessageDialog(this, "Acceptable names for transitions are defined by the regular expression:\n[a-zA-Z][_a-zA-Z0-9]*\n\nNote that \"true\" and \"false\" are reserved keywords.", "Error", JOptionPane.ERROR_MESSAGE);
-				return false;
-			}
-			context.nameGenerator().updateIndices(context.activeModel(), newName);
+
+			if (!oldName.equals(newName)) {
+                Command renameCommand = new RenameTimedPlaceCommand(context.tabContent(), (LocalTimedPlace) place.underlyingPlace(), oldName, newName);
+                context.undoManager().addEdit(renameCommand);
+                try { // set name
+                    renameCommand.redo();
+                } catch (RequireException e) {
+                    context.undoManager().undo();
+                    JOptionPane.showMessageDialog(this, "Acceptable names for transitions are defined by the regular expression:\n[a-zA-Z][_a-zA-Z0-9]*\n\nNote that \"true\" and \"false\" are reserved keywords.", "Error", JOptionPane.ERROR_MESSAGE);
+                    return false;
+                }
+                context.nameGenerator().updateIndices(context.activeModel(), newName);
+            }
 		
 			if(makeNewShared){
 				Command command = new MakePlaceNewSharedCommand(context.activeModel(), newName, place.underlyingPlace(), place, context.tabContent(), false);
@@ -637,6 +630,12 @@
 
 		if ((place.getAttributesVisible() && !attributesCheckBox.isSelected()) || (!place.getAttributesVisible() && attributesCheckBox.isSelected())) {
 			place.toggleAttributesVisible();
+
+            Map<PetriNetObject, Boolean> map = new HashMap<>();
+            map.put(place, !place.getAttributesVisible());
+
+            Command changeVisibility = new ChangeAllNamesVisibilityCommand(currentTab, map, null, place.getAttributesVisible());
+			context.undoManager().addEdit(changeVisibility);
 		}
 		place.update(true);
 		place.repaint();
 
=== modified file 'src/pipe/gui/widgets/QueryDialog.java'
--- src/pipe/gui/widgets/QueryDialog.java	2021-03-29 10:08:13 +0000
+++ src/pipe/gui/widgets/QueryDialog.java	2021-08-03 09:29:22 +0000
@@ -314,7 +314,7 @@
 	private final static String TOOL_TIP_SAVE_AND_VERIFY_BUTTON = "Save and verify the query.";
 	private final static String TOOL_TIP_CANCEL_BUTTON = "Cancel the changes made in this dialog.";
 	private final static String TOOL_TIP_SAVE_UPPAAL_BUTTON = "Export an xml file that can be opened in UPPAAL GUI.";
-	private final static String TOOL_TIP_SAVE_COMPOSED_BUTTON = "Export an xml file of composed net and approximated net if enabled";
+	private final static String TOOL_TIP_SAVE_COMPOSED_BUTTON = "Open a composed net in a new tab and use approximated net if enabled";
 	private final static String TOOL_TIP_OPEN_REDUCED_BUTTON = "Open the net produced after applying structural reduction rules";
 	private final static String TOOL_TIP_SAVE_TAPAAL_BUTTON = "Export an xml file that can be used as input for the TAPAAL engine.";
 	private final static String TOOL_TIP_SAVE_PN_BUTTON = "Export an xml file that can be used as input for the untimed Petri net engine.";
 
=== modified file 'src/pipe/gui/widgets/TAPNTransitionEditor.java'
--- src/pipe/gui/widgets/TAPNTransitionEditor.java	2021-04-08 08:30:29 +0000
+++ src/pipe/gui/widgets/TAPNTransitionEditor.java	2021-08-03 09:29:22 +0000
@@ -4,6 +4,8 @@
 import java.awt.event.ActionEvent;
 import java.awt.event.ActionListener;
 import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.Map;
 import java.util.Vector;
 
 import javax.swing.DefaultComboBoxModel;
@@ -21,6 +23,7 @@
 import net.tapaal.swinghelpers.SwingHelper;
 import net.tapaal.swinghelpers.WidthAdjustingComboBox;
 import pipe.gui.CreateGui;
+import pipe.gui.graphicElements.PetriNetObject;
 import pipe.gui.graphicElements.tapn.TimedTransitionComponent;
 import dk.aau.cs.gui.Context;
 import dk.aau.cs.model.tapn.Bound;
@@ -383,11 +386,13 @@
 			}
 			try{
 				String oldName = transition.underlyingTransition().name();
+				if (!oldName.equals(newName)) {
 				transition.underlyingTransition().setName(newName);
 				Command renameCommand = new RenameTimedTransitionCommand(context.tabContent(), transition.underlyingTransition(), oldName, newName);
 				context.undoManager().addEdit(renameCommand);
 				// set name
 				renameCommand.redo();
+				}
 			}catch(RequireException e){
 				context.undoManager().undo(); 
 				JOptionPane.showMessageDialog(this,
@@ -457,6 +462,12 @@
 		
 		if(transition.getAttributesVisible() && !attributesCheckBox.isSelected() || (!transition.getAttributesVisible() && attributesCheckBox.isSelected())) {
 			transition.toggleAttributesVisible();
+
+            Map<PetriNetObject, Boolean> map = new HashMap<>();
+            map.put(transition, !transition.getAttributesVisible());
+
+            Command changeVisibility = new ChangeAllNamesVisibilityCommand(context.tabContent(), null, map, transition.getAttributesVisible());
+            context.undoManager().addEdit(changeVisibility);
 		}
 		
 		transition.update(true);