KeYProject · mattulbrich · Jun 22, 2026 · Jun 22, 2026 · Jun 22, 2026 · Jun 23, 2026
diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/AutoPilotPrepareProofMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/AutoPilotPrepareProofMacro.java
@@ -36,7 +36,7 @@ public class AutoPilotPrepareProofMacro extends StrategyProofMacro {
 
     @Override
     public String getName() {
-        return "Auto Pilot (Preparation Only)";
+        return "Structured Automation (Prep. Only)";
     }
 
     @Override
@@ -46,8 +46,13 @@ public String getCategory() {
 
     @Override
     public String getDescription() {
-        return "<html><ol><li>Finish symbolic execution" + "<li>Separate proof obligations"
-            + "<li>Expand invariant definitions</ol>";
+        return "<html>This configures the automation such that it preserves<br>" +
+            "the program structure and makes it easier to comprehend the<br>" +
+            "resulting proof. It produces proof goals without program<br>" +
+            "references, but does not try to close these goals.<br>" +
+            "The steps are:<ol><li>Finish symbolic execution" +
+            "<li>Separate proof obligations" +
+            "<li>Expand invariant definitions</ol>";
     }
 
     @Override

diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/DefaultAutoMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/DefaultAutoMacro.java
@@ -0,0 +1,90 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.macros;
+
+import java.util.List;
+import java.util.stream.Collectors;
+
+import de.uka.ilkd.key.control.UserInterfaceControl;
+import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.proof.Node;
+import de.uka.ilkd.key.proof.Proof;
+import de.uka.ilkd.key.prover.impl.ApplyStrategy;
+
+import org.key_project.prover.engine.GoalChooser;
+import org.key_project.prover.engine.ProverCore;
+import org.key_project.prover.engine.ProverTaskListener;
+import org.key_project.prover.sequent.PosInOccurrence;
+import org.key_project.util.collection.ImmutableList;
+
+/**
+ * The macro {@link DefaultAutoMacro} runs the active proof strategy on all enabled goals
+ * in the selected subtree. This is equivalent to pressing the Auto button but can be
+ * invoked from context menus or keyboard shortcuts.
+ *
+ * This is used to show traditional strategy application as an item in the context menus.
+ *
+ * @author mattias ulbrich
+ */
+public class DefaultAutoMacro extends AbstractProofMacro {
+
+    @Override
+    public String getName() {
+        return "Full Automation";
+    }
+
+    @Override
+    public String getCategory() {
+        return "Auto Pilot";
+    }
+
+    @Override
+    public String getScriptCommandName() {
+        return "auto";
+    }
+
+    @Override
+    public String getDescription() {
+        return "<html>Runs the full proof strategy on the selected subtree.<br>" +
+            "The strategy can be configured in 'Proof Search Strategy' tab.";
+    }
+
+    @Override
+    public boolean canApplyTo(Proof proof, ImmutableList<Goal> goals,
+            PosInOccurrence posInOcc) {
+        return goals != null && !goals.isEmpty();
+    }
+
+    @Override
+    public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
+            ImmutableList<Goal> goals, PosInOccurrence posInOcc, ProverTaskListener listener)
+            throws InterruptedException {
+        if (goals == null || goals.isEmpty()) {
+            return null;
+        }
+
+        List<Node> nodes = goals.stream().map(Goal::node).collect(Collectors.toList());
+
+        final GoalChooser goalChooser =
+            proof.getInitConfig().getProfile().getSelectedGoalChooserBuilder().create();
+        final ProverCore applyStrategy = new ApplyStrategy(goalChooser);
+
+        final ProofMacroListener pml =
+            new ProgressBarListener(goals.size(), getMaxSteps(proof), listener);
+        applyStrategy.addProverTaskObserver(pml);
+
+        try {
+            applyStrategy.start(proof, goals);
+            synchronized (applyStrategy) {
+                if (applyStrategy.hasBeenInterrupted()) {
+                    throw new InterruptedException();
+                }
+            }
+        } finally {
+            applyStrategy.removeProverTaskObserver(pml);
+        }
+
+        return new ProofMacroFinishedInfo(this, proof.openGoals(), nodes);
+    }
+}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/FullAutoPilotProofMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/FullAutoPilotProofMacro.java
@@ -29,7 +29,7 @@ public class FullAutoPilotProofMacro extends SequentialProofMacro {
 
     @Override
     public String getName() {
-        return "Full Auto Pilot";
+        return "Structured Automation";
     }
 
     @Override
@@ -44,8 +44,14 @@ public String getScriptCommandName() {
 
     @Override
     public String getDescription() {
-        return "<html><ol><li>Finish symbolic execution" + "<li>Separate proof obligations"
-            + "<li>Expand invariant definitions" + "<li>Try to close all proof obligations</ol>";
+        return "<html>This configures the automation such that it preserves<br>" +
+            "the program structure and makes it easier to comprehend the<br>" +
+            "resulting proof.<br>" +
+            "The steps are:" +
+            "<ol><li>Finish symbolic execution" +
+            "<li>Separate proof obligations" +
+            "<li>Expand invariant definitions" +
+            "<li>Try to close all proof obligations</ol>";
     }
 
     @Override

diff --git a/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.macros.ProofMacro b/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.macros.ProofMacro
@@ -4,6 +4,7 @@
 #
 # warning: subject to change of package name
 
+de.uka.ilkd.key.macros.DefaultAutoMacro
 de.uka.ilkd.key.macros.FullAutoPilotProofMacro
 #de.uka.ilkd.key.macros.FullAutoPilotWithJMLSpecJoinsProofMacro
 de.uka.ilkd.key.macros.AutoPilotPrepareProofMacro

diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java
@@ -55,6 +55,7 @@
 import de.uka.ilkd.key.gui.smt.DropdownSelectionButton;
 import de.uka.ilkd.key.gui.sourceview.SourceViewFrame;
 import de.uka.ilkd.key.gui.utilities.LruCached;
+import de.uka.ilkd.key.macros.DefaultAutoMacro;
 import de.uka.ilkd.key.proof.*;
 import de.uka.ilkd.key.proof.init.Profile;
 import de.uka.ilkd.key.proof.io.ProblemLoader;
@@ -240,6 +241,7 @@ public final class MainWindow extends JFrame {
     private ChangeListener selectAllListener;
     private JCheckBoxMenuItem selectAll;
     private JSeparator separator;
+    private DropdownSelectionButton automationComponent;
     private ExitMainAction exitMainAction;
     private ShowActiveSettingsAction showActiveSettingsAction;
     private UnicodeToggleAction unicodeToggleAction;
@@ -283,6 +285,12 @@ public final class MainWindow extends JFrame {
     private final LruCached<HTMLSyntaxHighlighter.Args, String> highlightCache =
         new LruCached<>(HTMLSyntaxHighlighter.Args::run);
 
+    /**
+     * List of automation actions for the dropdown button.
+     * To add new automation modes, add them to {@link #createAutomationActions()}.
+     */
+    private final List<Action> automationActions;
+
     /*
      * This class should only be instantiated once!
      */
@@ -329,6 +337,19 @@ private MainWindow() {
         strategySelectionView = new StrategySelectionView(this, mediator);
         openGoalsView = new GoalList(mediator);
 
+        // Initialize automation actions
+        automationActions = createAutomationActions();
+
+        // Register keyboard shortcut for default automation action (Ctrl+Space)
+        if (!automationActions.isEmpty()) {
+            Action defaultAction = automationActions.get(0);
+            KeyStroke accelerator = (KeyStroke) defaultAction.getValue(Action.ACCELERATOR_KEY);
+            if (accelerator != null) {
+                inputMap.put(accelerator, "defaultAutomation");
+                getRootPane().getActionMap().put("defaultAutomation", defaultAction);
+            }
+        }
+
         layoutMain();
         SwingUtilities.updateComponentTreeUI(this);
         ToolTipManager.sharedInstance().setDismissDelay(30000);
@@ -652,7 +673,9 @@ private JToolBar createProofControlToolBar() {
         toolBar.setFloatable(false);
         toolBar.setRollover(true);
 
-        toolBar.add(createWiderAutoModeButton());
+        DropdownSelectionButton autoComp = createAutomationComponent();
+        toolBar.add(autoComp.getActionComponent());
+        toolBar.add(autoComp.getSelectionComponent());
         toolBar.addSeparator();
         toolBar.addSeparator();
         toolBar.addSeparator();
@@ -748,6 +771,89 @@ private DropdownSelectionButton createSMTComponent() {
         return smtComponent;
     }
 
+    // @formatter:off
+    /**
+     * Creates the list of automation actions for the dropdown button.
+     * <p>
+     * The first action in the list is the default and will be triggered by the {@code Ctrl+Space}
+     * keyboard shortcut. Actions are displayed in the dropdown menu in the order they are added.
+     * </p>
+     * <p>
+     * To add new automation modes, simply add them to this list. No configuration file or service
+     * loader is needed. For macro-based automations, use {@link MacroAutomationAction}. For custom
+     * behaviors, extend {@link MainWindowAction}.
+     * </p>
+     * <p>
+     * Example:
+     *
+     * <pre>
+     * {@code
+     * actions.add(new MacroAutomationAction(this,
+     *     new YourCustomMacro(),
+     *     "Your Automation Name",
+     *     IconFactory.yourIcon(TOOLBAR_ICON_SIZE)));
+     * }
+     * </pre>
+     * </p>
+     *
+     * @return list of automation actions
+     * @see MacroAutomationAction
+     * @see AutoModeAction
+     */
+    // @formatter:on
+    private List<Action> createAutomationActions() {
+        return List.of(
+            new MacroAutomationAction(this,
+                new DefaultAutoMacro(),
+                IconFactory.automationWithOverlay(TOOLBAR_ICON_SIZE, "")),
+            new MacroAutomationAction(this,
+                new de.uka.ilkd.key.macros.FullAutoPilotProofMacro(),
+                IconFactory.automationFullPilotLogo(TOOLBAR_ICON_SIZE)),
+            new MacroAutomationAction(this,
+                new de.uka.ilkd.key.macros.AutoPilotPrepareProofMacro(),
+                IconFactory.automationPrepareLogo(TOOLBAR_ICON_SIZE)));
+    }
+
+    /**
+     * Create the automation component dropdown button.
+     * This replaces the old auto mode button with a configurable dropdown selector.
+     *
+     * @return the automation {@link DropdownSelectionButton}
+     */
+    private DropdownSelectionButton createAutomationComponent() {
+        automationComponent = new DropdownSelectionButton(TOOLBAR_ICON_SIZE);
+
+        // Convert list to array
+        Action[] actionArray = automationActions.toArray(new Action[0]);
+
+        // Identity reducer - just return the single selected action
+        Function<Action[], Action> identityReducer = a -> {
+            if (a.length == 0) {
+                return null;
+            }
+            return a[0];
+        };
+
+        // Set items with single selection (maxChoiceAmount = 1)
+        automationComponent.setItems(actionArray, identityReducer, 1);
+
+        // Add change listener to update enabled state based on proof status
+        automationComponent.addListener(e -> {
+            Proof proof = mediator.getSelectedProof();
+            boolean hasProof = proof != null && !proof.closed();
+            automationComponent.setEnabled(hasProof);
+        });
+
+        // Initialize enabled state
+        Proof initialProof = mediator.getSelectedProof();
+        automationComponent.setEnabled(initialProof != null && !initialProof.closed());
+
+        automationComponent.getActionComponent().putClientProperty("hideActionText", Boolean.TRUE);
+        automationComponent.getActionComponent().putClientProperty("isAutoButton", Boolean.TRUE);
+
+        return automationComponent;
+    }
+
     private JComponent createWiderAutoModeButton() {
         JButton b = new JButton(autoModeAction);
         b.putClientProperty("hideActionText", Boolean.TRUE);
@@ -966,7 +1072,12 @@ public JMenu createProofMenu(Proof selected) {
         proof.setMnemonic(KeyEvent.VK_P);
 
         if (selected == null) {
-            proof.add(autoModeAction);
+            JMenu automationMenu = new JMenu("Automation");
+            for (Action action : automationActions) {
+                JMenuItem item = new JMenuItem(action);
+                automationMenu.add(item);
+            }
+            proof.add(automationMenu);
             GoalBackAction goalBack = new GoalBackAction(this, true);
             proof.addMenuListener(new MenuListener() {
                 @Override
@@ -1599,10 +1710,17 @@ private void redispatchMouseEvent(MouseEvent e) {
                 Component component = SwingUtilities.getDeepestComponentAt(contentPane,
                     containerPoint.x, containerPoint.y);
 
-                if (eventID == MouseEvent.MOUSE_PRESSED && isLiveComponent(component)) {
-                    currentComponent = component;
-                    dispatchForCurrentComponent(e);
+                if (isLiveComponent(component)) {
+                    if (eventID == MouseEvent.MOUSE_PRESSED) {
+                        currentComponent = component;
+                        dispatchForCurrentComponent(e);
+                    }
+                    glassPane.setCursor(new Cursor(Cursor.DEFAULT_CURSOR));
+                } else {
+                    glassPane.setCursor(new Cursor(Cursor.WAIT_CURSOR));
                 }
+
+
             }
         }
 
@@ -1611,8 +1729,8 @@ private boolean isLiveComponent(Component c) {
             // this is not the most elegant way to identify the right
             // components, but it scales well ;-)
             while (c != null) {
-                if ((c instanceof JComponent)
-                        && AUTO_MODE_TEXT.equals(((JComponent) c).getToolTipText())) {
+                if (c instanceof JComponent jc
+                        && jc.getClientProperty("isAutoButton") == Boolean.TRUE) {
                     return true;
                 }
                 c = c.getParent();

diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java
@@ -20,17 +20,14 @@
 
 import org.key_project.util.collection.ImmutableList;
 
-public final class AutoModeAction extends MainWindowAction {
+public class AutoModeAction extends MainWindowAction {
 
     private static final KeyStroke START_KEY =
         KeyStroke.getKeyStroke(KeyEvent.VK_SPACE, InputEvent.CTRL_DOWN_MASK);
     private static final KeyStroke STOP_KEY = KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0);
-    /**
-     *
-     */
     private static final long serialVersionUID = -7702898691162947994L;
-    final Icon startLogo = IconFactory.autoModeStartLogo(MainWindow.TOOLBAR_ICON_SIZE);
-    final Icon stopLogo = IconFactory.autoModeStopLogo(MainWindow.TOOLBAR_ICON_SIZE);
+    private final Icon startLogo;
+    private final Icon stopLogo = IconFactory.autoModeStopLogo(MainWindow.TOOLBAR_ICON_SIZE);
 
     private Proof associatedProof;
 
@@ -63,11 +60,16 @@ public void proofGoalsAdded(ProofTreeEvent e) {
     };
 
     public AutoModeAction(MainWindow mainWindow) {
+        this(mainWindow, IconFactory.automationWithOverlay(MainWindow.TOOLBAR_ICON_SIZE, ""));
+    }
+
+    public AutoModeAction(MainWindow mainWindow, Icon startLogo) {
         super(mainWindow);
         associatedProof = getMediator().getSelectedProof();
         putValue("hideActionText", Boolean.TRUE);
         setName(getStartCommand());
         setTooltip(MainWindow.AUTO_MODE_TEXT);
+        this.startLogo = startLogo;
         setIcon(startLogo);
 
         enable();
@@ -173,4 +175,8 @@ public void actionPerformed(ActionEvent e) {
         }
     }
 
+    @Override
+    public String toString() {
+        return "Full Automation";
+    }
 }