diff --git a/keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleLauncher.java b/keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleLauncher.java index 7571523bbc2..b79b2388e58 100644 --- a/keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleLauncher.java +++ b/keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleLauncher.java @@ -109,5 +109,10 @@ public void addListener(IsabelleLauncherListener listener) { public void stopAll(IsabelleSolver.ReasonOfInterruption reasonOfInterruption) { shutdown(); runningSolvers.forEach((solver) -> solver.interrupt(reasonOfInterruption)); + solverQueue.forEach((solver) -> solver.interrupt(reasonOfInterruption)); + + runningSolvers.clear(); + solverQueue.clear(); + listener.launcherStopped(this, solverSet); } } diff --git a/keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleLauncherListenerImpl.java b/keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleLauncherProgressDialogMediator.java similarity index 94% rename from keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleLauncherListenerImpl.java rename to keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleLauncherProgressDialogMediator.java index be1ec7f4b7b..a713cc62408 100644 --- a/keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleLauncherListenerImpl.java +++ b/keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleLauncherProgressDialogMediator.java @@ -12,7 +12,7 @@ import java.util.Collection; import java.util.TimerTask; -public class IsabelleLauncherListenerImpl implements IsabelleLauncherListener { +public class IsabelleLauncherProgressDialogMediator implements IsabelleLauncherListener { private final Timer timer = new Timer(); private int finishedCounter = 0; @@ -127,25 +127,23 @@ private void unknownStopped(int x, int y) { private void setProgressText(int value) { JProgressBar bar = progressDialog.getProgressBar(); - if (bar.getMaximum() == 1) { if (value == -1) { bar.setString("Preparing..."); bar.setStringPainted(true); - return; + } else if (value == bar.getMaximum()){ + bar.setString("Finished."); + bar.setStringPainted(true); + } else { + bar.setString("Processed " + value + " of " + bar.getMaximum() + " problems."); + bar.setStringPainted(true); } - bar.setString(value == 0 ? "Processing..." : "Finished."); - bar.setStringPainted(true); - } else { - bar.setString("Processed " + value + " of " + bar.getMaximum() + " problems."); - bar.setStringPainted(true); - } } protected void discardEvent(IsabelleLauncher launcher) { } - public IsabelleLauncherListenerImpl(IsabelleTranslationSettings settings) { + public IsabelleLauncherProgressDialogMediator(IsabelleTranslationSettings settings) { } diff --git a/keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleResourceController.java b/keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleResourceController.java index e0f58688eb3..0e02fe9d11b 100644 --- a/keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleResourceController.java +++ b/keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleResourceController.java @@ -49,13 +49,18 @@ public IsabelleResourceController(int numberOfInstances) { public void init() throws IOException { for (int i = 0; i < numberOfInstances; i++) { - idleInstances.add(createIsabelleResource()); + IsabelleResource newResource = createIsabelleResource(); + if (!isShutdown() && newResource != null) { + idleInstances.add(newResource); + } } } public IsabelleResource getIsabelleResource(IsabelleSolver requestingSolver) throws InterruptedException { waitingSolvers.add(requestingSolver); - return idleInstances.take(); + IsabelleResource freeResource = idleInstances.take(); + waitingSolvers.remove(requestingSolver); + return freeResource; } public void shutdownGracefully() { @@ -73,6 +78,14 @@ public void shutdownGracefully() { public void returnResource(IsabelleSolver returningSolver, IsabelleResource resource) { assert resource != null; + if (isShutdown()) { + if (!resource.isDestroyed()) { + //TODO some kind of race condition happens here + resource.destroy(); + } + return; + } + if (resource.isDestroyed()) { try { resource = createIsabelleResource(); @@ -81,12 +94,16 @@ public void returnResource(IsabelleSolver returningSolver, IsabelleResource reso shutdownGracefully(); LOGGER.error(e.getMessage()); } + } else { + resource.interrupt(); } - resource.interrupt(); - waitingSolvers.remove(returningSolver); idleInstances.offer(resource); } + public boolean isShutdown() { + return isShutdown; + } + private IsabelleResource createIsabelleResource() throws IOException { Callable creationTask = () -> { Isabelle isabelleInstance = startIsabelleInstance(); @@ -96,11 +113,15 @@ private IsabelleResource createIsabelleResource() throws IOException { try { return instanceCreatorService.submit(creationTask).get(); } catch (InterruptedException e) { + shutdownGracefully(); throw new RuntimeException(e); } catch (ExecutionException e) { if (e.getCause() instanceof IOException) { throw (IOException) e.getCause(); } + if (isShutdown()) { + return null; + } LOGGER.error("Error during Isabelle setup"); throw new RuntimeException(e); } catch (RejectedExecutionException e) { @@ -150,7 +171,7 @@ public boolean isDestroyed() { return instance.isDestroyed(); } - public void destroy() { + void destroy() { instance.destroy(); } diff --git a/keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleSolverInstance.java b/keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleSolverInstance.java index f02dd37d834..45392dc50d3 100644 --- a/keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleSolverInstance.java +++ b/keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleSolverInstance.java @@ -129,13 +129,13 @@ public void interrupt(ReasonOfInterruption reason) { thread.interrupt(); } if (isabelleResource != null) { - shutdownAndReturnResource(); + returnResource(); } } - private void shutdownAndReturnResource() { - isabelleResource.interrupt(); + private void returnResource() { resourceController.returnResource(this, isabelleResource); + isabelleResource = null; } private void setSolverState(SolverState solverState) { @@ -316,7 +316,9 @@ fun go_run (state, thy) = this.result = result; notifyProcessTimeout(); } catch (InterruptedException exception) { - interrupt(ReasonOfInterruption.Exception); + if (reasonOfInterruption == ReasonOfInterruption.NoInterruption) { + interrupt(ReasonOfInterruption.Exception); + } result = new SledgehammerResult(Option.apply(null)); this.result = result; notifySledgehammerError(exception); diff --git a/keyext.isabelletranslation/src/main/java/key/isabelletranslation/TranslateAllAction.java b/keyext.isabelletranslation/src/main/java/key/isabelletranslation/TranslateAllAction.java index 8dee50ac958..c8a300c0f8e 100644 --- a/keyext.isabelletranslation/src/main/java/key/isabelletranslation/TranslateAllAction.java +++ b/keyext.isabelletranslation/src/main/java/key/isabelletranslation/TranslateAllAction.java @@ -59,7 +59,7 @@ private void generateTranslation() { throw new RuntimeException(e); } - launcher.addListener(new IsabelleLauncherListenerImpl(settings)); + launcher.addListener(new IsabelleLauncherProgressDialogMediator(settings)); try { launcher.try0ThenSledgehammerAllPooled(translations, 30, 1); } catch (IOException e) { diff --git a/keyext.isabelletranslation/src/main/java/key/isabelletranslation/TranslationAction.java b/keyext.isabelletranslation/src/main/java/key/isabelletranslation/TranslationAction.java index bd52f356b1e..92330b2da3d 100644 --- a/keyext.isabelletranslation/src/main/java/key/isabelletranslation/TranslationAction.java +++ b/keyext.isabelletranslation/src/main/java/key/isabelletranslation/TranslationAction.java @@ -3,8 +3,6 @@ import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.actions.MainWindowAction; -import de.uka.ilkd.key.rule.IBuiltInRuleApp; -import de.uka.ilkd.key.smt.SMTRuleApp; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -58,7 +56,7 @@ private void generateTranslation() { throw new RuntimeException(e); } - launcher.addListener(new IsabelleLauncherListenerImpl(settings)); + launcher.addListener(new IsabelleLauncherProgressDialogMediator(settings)); try { launcher.try0ThenSledgehammerAllPooled(list, 30, 1); } catch (IOException e) {