You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
Load one of the examples (I used SumAndMax)
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.
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
If you do it right, you will get this sequence of automode stops/starts:
Additional information
If you double click (or triple click) on the start button, you get this exception:
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.
The text was updated successfully, but these errors were encountered: