Automode sometimes not entered when running strategy

[FliegendeWurst]

Description

When quickly starting the automated proof search after loading a proof, the "automode" is not activated. This means that every proof step updates the UI, slowing everything down.

Reproducible

Somewhat hard to reproduce.

Steps to reproduce

1. Load one of the examples (I used SumAndMax)
2. Quickly press on the start button in the toolbar

If you do it right, you will get this sequence of automode stops/starts:

stopping interface
current stack
java.base/java.lang.Thread.getStackTrace(Thread.java:1610)
de.uka.ilkd.key.core.KeYMediator.stopInterface(KeYMediator.java:592)
de.uka.ilkd.key.proof.io.ProblemLoader.runAsynchronously(ProblemLoader.java:137)
de.uka.ilkd.key.gui.WindowUserInterfaceControl.loadProblem(WindowUserInterfaceControl.java:102)
de.uka.ilkd.key.gui.WindowUserInterfaceControl.loadProblem(WindowUserInterfaceControl.java:107)
de.uka.ilkd.key.gui.MainWindow.loadProblem(MainWindow.java:1358)
de.uka.ilkd.key.gui.actions.OpenExampleAction.actionPerformed(OpenExampleAction.java:33)
de.uka.ilkd.key.gui.MainWindow.openExamples(MainWindow.java:1354)
de.uka.ilkd.key.gui.WindowUserInterfaceControl.openExamples(WindowUserInterfaceControl.java:284)
de.uka.ilkd.key.core.Main.loadCommandLineFiles(Main.java:224)
de.uka.ilkd.key.core.Main.main(Main.java:185)

stopping interface
current stack
java.base/java.lang.Thread.getStackTrace(Thread.java:1610)
de.uka.ilkd.key.core.KeYMediator.stopInterface(KeYMediator.java:592)
de.uka.ilkd.key.gui.WindowUserInterfaceControl.loadingStarted(WindowUserInterfaceControl.java:466)
de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:273)
de.uka.ilkd.key.proof.io.ProblemLoader.doWork(ProblemLoader.java:64)
de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:117)
de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:110)

[09:25:17.498] INFO  AbstractProblemLoader - Loading environment from /home/arne/src/key/key.ui/examples/heap/vstte10_01_SumAndMax/project.key
[09:25:17.626] INFO  AbstractProblemLoader - Creating init config
stopping interface
current stack
java.base/java.lang.Thread.getStackTrace(Thread.java:1610)
de.uka.ilkd.key.core.KeYMediator.stopInterface(KeYMediator.java:592)
de.uka.ilkd.key.gui.WindowUserInterfaceControl.progressStarted(WindowUserInterfaceControl.java:121)
de.uka.ilkd.key.proof.init.ProblemInitializer.progressStarted(ProblemInitializer.java:86)
de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:441)
de.uka.ilkd.key.proof.io.AbstractProblemLoader.createInitConfig(AbstractProblemLoader.java:557)
de.uka.ilkd.key.proof.io.AbstractProblemLoader.loadEnvironment(AbstractProblemLoader.java:317)
de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:275)
de.uka.ilkd.key.proof.io.ProblemLoader.doWork(ProblemLoader.java:64)
de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:117)
de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:110)

starting interface
current stack
java.base/java.lang.Thread.getStackTrace(Thread.java:1610)
de.uka.ilkd.key.core.KeYMediator.startInterface(KeYMediator.java:618)
de.uka.ilkd.key.gui.WindowUserInterfaceControl.progressStopped(WindowUserInterfaceControl.java:126)
de.uka.ilkd.key.proof.init.ProblemInitializer.progressStopped(ProblemInitializer.java:97)
de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:564)
de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:458)
de.uka.ilkd.key.proof.io.AbstractProblemLoader.createInitConfig(AbstractProblemLoader.java:557)
de.uka.ilkd.key.proof.io.AbstractProblemLoader.loadEnvironment(AbstractProblemLoader.java:317)
de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:275)
de.uka.ilkd.key.proof.io.ProblemLoader.doWork(ProblemLoader.java:64)
de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:117)
de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:110)

stopping interface
current stack
java.base/java.lang.Thread.getStackTrace(Thread.java:1610)
de.uka.ilkd.key.core.KeYMediator.stopInterface(KeYMediator.java:592)
de.uka.ilkd.key.gui.WindowUserInterfaceControl.progressStarted(WindowUserInterfaceControl.java:121)
de.uka.ilkd.key.proof.init.ProblemInitializer.progressStarted(ProblemInitializer.java:86)
de.uka.ilkd.key.proof.init.ProblemInitializer.startProver(ProblemInitializer.java:570)
de.uka.ilkd.key.gui.ProofManagementDialog.findOrStartProof(ProofManagementDialog.java:470)
de.uka.ilkd.key.gui.ProofManagementDialog.lambda$new$5(ProofManagementDialog.java:213)

starting interface
current stack
java.base/java.lang.Thread.getStackTrace(Thread.java:1610)
de.uka.ilkd.key.core.KeYMediator.startInterface(KeYMediator.java:618)
de.uka.ilkd.key.gui.WindowUserInterfaceControl.progressStopped(WindowUserInterfaceControl.java:126)
de.uka.ilkd.key.proof.init.ProblemInitializer.progressStopped(ProblemInitializer.java:97)
de.uka.ilkd.key.proof.init.ProblemInitializer.startProver(ProblemInitializer.java:593)
de.uka.ilkd.key.gui.ProofManagementDialog.findOrStartProof(ProofManagementDialog.java:470)
de.uka.ilkd.key.gui.ProofManagementDialog.lambda$new$5(ProofManagementDialog.java:213)

[09:25:22.437] INFO  JavaCompilerCheckFacade - Javac check is triggered. To disable use property -PKEY_JAVAC_DISABLE=true
[09:25:22.778] INFO  JavaCompilerCheckFacade - Javac check took 298 ms.
stopping interface
current stack
java.base/java.lang.Thread.getStackTrace(Thread.java:1610)
de.uka.ilkd.key.core.KeYMediator.stopInterface(KeYMediator.java:592)
de.uka.ilkd.key.ui.MediatorProofControl.startAutoMode(MediatorProofControl.java:76)
de.uka.ilkd.key.control.AbstractProofControl.startAutoMode(AbstractProofControl.java:597)
de.uka.ilkd.key.gui.actions.useractions.AutoModeUserAction.apply(AutoModeUserAction.java:30)
de.uka.ilkd.key.gui.actions.useractions.UserAction.actionPerformed(UserAction.java:63)
de.uka.ilkd.key.gui.actions.AutoModeAction.actionPerformed(AutoModeAction.java:161)

starting interface
current stack
java.base/java.lang.Thread.getStackTrace(Thread.java:1610)
de.uka.ilkd.key.core.KeYMediator.startInterface(KeYMediator.java:618)
de.uka.ilkd.key.proof.io.ProblemLoader$1.done(ProblemLoader.java:124)

Additional information

If you double click (or triple click) on the start button, you get this exception:

[22:49:35.583] WARN  ApplyStrategy - doWork exceptionde.uka.ilkd.key.util.AssertionFailure: Expected an empty leaf node
	at de.uka.ilkd.key.strategy.feature.AppliedRuleAppsNameCache.get(AppliedRuleAppsNameCache.java:108)
	at de.uka.ilkd.key.strategy.feature.AbstractNonDuplicateAppFeature.noDuplicateFindTaclet(AbstractNonDuplicateAppFeature.java:126)
	at de.uka.ilkd.key.strategy.feature.NonDuplicateAppFeature.filter(NonDuplicateAppFeature.java:21)
	at de.uka.ilkd.key.strategy.feature.BinaryTacletAppFeature.filter(BinaryTacletAppFeature.java:29)
	at de.uka.ilkd.key.strategy.feature.BinaryFeature.computeCost(BinaryFeature.java:23)
	at de.uka.ilkd.key.strategy.feature.SumFeature.computeCost(SumFeature.java:25)
	at de.uka.ilkd.key.strategy.JavaCardDLStrategy.computeCost(JavaCardDLStrategy.java:2046)
	at de.uka.ilkd.key.strategy.TacletAppContainer.createInitialAppContainers(TacletAppContainer.java:188)
	at de.uka.ilkd.key.strategy.RuleAppContainer.createAppContainers(RuleAppContainer.java:113)
	at de.uka.ilkd.key.strategy.QueueRuleApplicationManager.rulesAdded(QueueRuleApplicationManager.java:136)
	at de.uka.ilkd.key.proof.RuleAppIndex.informNewRuleListener(RuleAppIndex.java:361)
	at de.uka.ilkd.key.proof.RuleAppIndex$1.rulesAdded(RuleAppIndex.java:54)
	at de.uka.ilkd.key.proof.TermTacletAppIndex.fireRulesAdded(TermTacletAppIndex.java:595)
	at de.uka.ilkd.key.proof.TermTacletAppIndex.updateLocalApps(TermTacletAppIndex.java:306)
	at de.uka.ilkd.key.proof.TermTacletAppIndex.updateHelp(TermTacletAppIndex.java:275)
	at de.uka.ilkd.key.proof.TermTacletAppIndex.update(TermTacletAppIndex.java:407)
	at de.uka.ilkd.key.proof.SemisequentTacletAppIndex.updateTermIndices(SemisequentTacletAppIndex.java:136)
	at de.uka.ilkd.key.proof.SemisequentTacletAppIndex.updateTermIndices(SemisequentTacletAppIndex.java:147)
	at de.uka.ilkd.key.proof.SemisequentTacletAppIndex.sequentChanged(SemisequentTacletAppIndex.java:217)
	at de.uka.ilkd.key.proof.TacletAppIndex.deltaUpdateIndices(TacletAppIndex.java:173)
	at de.uka.ilkd.key.proof.TacletAppIndex.update(TacletAppIndex.java:159)
	at de.uka.ilkd.key.proof.TacletAppIndex.fillCache(TacletAppIndex.java:131)
	at de.uka.ilkd.key.proof.RuleAppIndex.fillCache(RuleAppIndex.java:324)
	at de.uka.ilkd.key.strategy.QueueRuleApplicationManager.peekNext(QueueRuleApplicationManager.java:223)
	at de.uka.ilkd.key.strategy.QueueRuleApplicationManager.next(QueueRuleApplicationManager.java:246)
	at de.uka.ilkd.key.prover.impl.ApplyStrategy.applyAutomaticRule(ApplyStrategy.java:93)
	at de.uka.ilkd.key.prover.impl.ApplyStrategy.doWork(ApplyStrategy.java:144)
	at de.uka.ilkd.key.prover.impl.ApplyStrategy.executeStrategy(ApplyStrategy.java:293)
	at de.uka.ilkd.key.prover.impl.ApplyStrategy.start(ApplyStrategy.java:261)
	at de.uka.ilkd.key.ui.MediatorProofControl$AutoModeWorker.doInBackground(MediatorProofControl.java:209)
	at de.uka.ilkd.key.ui.MediatorProofControl$AutoModeWorker.doInBackground(MediatorProofControl.java:145)
	at java.desktop/javax.swing.SwingWorker$1.call(SwingWorker.java:304)
	at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
	at java.desktop/javax.swing.SwingWorker.run(SwingWorker.java:343)
	at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1136)
	at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635)
	at java.base/java.lang.Thread.run(Thread.java:833)

Additional information (2)

If you click (once or twice) on the play button (at the right time) whilst a proof is loading, the UI gets 100% stuck (can only force quit KeY). I already have a fix for this issue.

• Commit: 7322c85