From c590b339703b6e98f90cd71a5574ceedb994e008 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 23 Oct 2015 17:17:47 +0200
Subject: [PATCH] Fix ugliness in InterruptManager
---
.../scala/leon/utils/InterruptManager.scala | 22 ++++++++-----------
1 file changed, 9 insertions(+), 13 deletions(-)
diff --git a/src/main/scala/leon/utils/InterruptManager.scala b/src/main/scala/leon/utils/InterruptManager.scala
index 29a79bafb..40d8dd183 100644
--- a/src/main/scala/leon/utils/InterruptManager.scala
+++ b/src/main/scala/leon/utils/InterruptManager.scala
@@ -5,36 +5,32 @@ package utils
import scala.collection.JavaConversions._
-import java.util.concurrent.atomic.AtomicBoolean
+import java.util.concurrent.atomic.{AtomicLong, AtomicBoolean}
import sun.misc.{Signal, SignalHandler}
import java.util.WeakHashMap
class InterruptManager(reporter: Reporter) extends Interruptible {
private[this] val interruptibles = new WeakHashMap[Interruptible, Boolean]()
private[this] val sigINT = new Signal("INT")
- private[this] val withinTimeout: AtomicBoolean = new AtomicBoolean(false)
+
+ private[this] val lastTimestamp = new AtomicLong(0L)
+ private val exitWindow = 1000L
+
private[this] val handler = new SignalHandler {
def handle(sig: Signal) {
- println()
- if (withinTimeout.get()) {
+ def now(): Long = System.currentTimeMillis()
+ reporter.info("")
+ if (now() - lastTimestamp.get < exitWindow) {
reporter.warning("Aborting Leon...")
System.exit(1)
}
else {
reporter.warning("Interrupted...")
- setTimeout()
+ lastTimestamp.set(now())
interrupt()
}
}
}
- private val exitWindow = 1000
- private[this] def setTimeout() = {
- import scala.concurrent.Future
- import scala.concurrent.ExecutionContext.Implicits.global
- withinTimeout.set(true)
- Future { Thread.sleep(exitWindow) } onComplete { _ => withinTimeout.set(false) }
- ()
- }
val interrupted: AtomicBoolean = new AtomicBoolean(false)
--
GitLab