Add timeout option for verification.

Primarily to help perform some benchmarks
But also generally helpful

src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifier.java

@@ -72,6 +72,10 @@ public static interface ProgressListener {
         void done(DfsBProgramVerifier v);
     }
 
+    private long start;
+
+
+    private long timeout; //timeout in ms
     private long visitedEdgeCount;
     private long visitedStatesCount;
     private VisitedStateStore visited = new BThreadSnapshotVisitedStateStore();
@@ -90,7 +94,7 @@ public VerificationResult verify(BProgram aBp) throws Exception {
         currentPath.clear();
         visited.clear();
         ExecutorService execSvc = ExecutorServiceMaker.makeWithName("DfsBProgramRunner-" + INSTANCE_COUNTER.incrementAndGet());
-        long start = System.currentTimeMillis();
+        start = System.currentTimeMillis();
         listenerOpt.ifPresent(l -> l.started(this));
         VerificationResult vr = dfsUsingStack(Node.getInitialNode(aBp, execSvc), execSvc);
         long end = System.currentTimeMillis();
@@ -107,9 +111,20 @@ protected VerificationResult dfsUsingStack(Node aStartNode, ExecutorService exec
         push(aStartNode);
 
         while (!isPathEmpty()) {
+
             if (debugMode) {
                 printStatus(iterationCount, Collections.unmodifiableList(currentPath));
             }
+            if (timeout != 0) {
+                long currTime = System.currentTimeMillis();
+                if ((currTime - start) > timeout) {
+                    //done
+                    if (debugMode) {
+                        System.out.println("Timeout exceeded, returning current state");
+                    }
+                    return new VerificationResult(VerificationResult.ViolationType.Timeout, null, null);
+                }
+            }
 
             Node curNode = peek();
             if (curNode != null) {
@@ -131,9 +146,7 @@ protected VerificationResult dfsUsingStack(Node aStartNode, ExecutorService exec
             iterationCount++;
 
             if (pathLength() == maxTraceLength) {
-                if (listenerOpt.isPresent()) {
-                    listenerOpt.get().maxTraceLengthHit(currentPath, this);
-                }
+                listenerOpt.ifPresent(progressListener -> progressListener.maxTraceLengthHit(currentPath, this));
                 // fold stack;
                 pop();
 
@@ -146,7 +159,7 @@ protected VerificationResult dfsUsingStack(Node aStartNode, ExecutorService exec
                         System.out.println("-pop!-");
                     }
                 } else {
-                    // go deeper 
+                    // go deeper
                     visited.store(nextNode);
                     if (isDebugMode()) {
                         System.out.println("-visiting: " + nextNode);
@@ -156,8 +169,9 @@ protected VerificationResult dfsUsingStack(Node aStartNode, ExecutorService exec
                 }
             }
 
-            if (iterationCount % iterationCountGap == 0 && listenerOpt.isPresent()) {
-                listenerOpt.get().iterationCount(iterationCount, visitedStatesCount, this);
+            if (iterationCount % iterationCountGap == 0) {
+                long finalIterationCount = iterationCount;
+                listenerOpt.ifPresent(progressListener -> progressListener.iterationCount(finalIterationCount, visitedStatesCount, this));
             }
         }
 
@@ -176,6 +190,18 @@ protected Node getUnvisitedNextNode(Node src, ExecutorService execSvc) throws Ex
         return null;
     }
 
+    public long getTimeout() {
+        return timeout;
+    }
+
+    /**
+     * Set timeout, 0 to disable timeout checks
+     * @param timeout - 0 to disable timeout
+     */
+    public void setTimeout(long timeout) {
+        this.timeout = timeout;
+    }
+
     public long getVisitedEdgeCount() {
         return visitedEdgeCount;
     }

src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/VerificationResult.java

@@ -55,7 +55,12 @@ public enum ViolationType {
         /**
          * Program can generate an illegal event trace
          */
-        FailedAssertion
+        FailedAssertion,
+
+        /**
+         * Program verification can time out
+         */
+        Timeout,
     }
 
     private final long timeMillies;

src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifierTest.java

@@ -219,7 +219,7 @@ public void testVariablesEquailtyInBT() throws Exception {
         assertFalse(res.isCounterExampleFound());
         assertEquals(res.getViolationType(), VerificationResult.ViolationType.None);
         assertEquals(10, res.getScannedStatesCount());
-        assertEquals(10, res.getEdgesScanned()); //in this case only one option per state
+        assertEquals(11, res.getEdgesScanned()); //in this case only one option per state
 
     }
 

src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/VerificationResultOptionsTest.java

@@ -116,5 +116,27 @@ public void testImmediateAssert() throws Exception {
         assertEquals(0, res.getScannedStatesCount());
     }
 
+    @Test(timeout=2000)
+    public void testTimeout() throws Exception {
+        //simple program with enough states that shouldn't take less than 10 ms
+        final BProgram bprog = new StringBProgram("bp.registerBThread('timeout', function(){" + //
+                "    while(true) \n" + //
+                "      for(var i=0; i<10; i++){\n" + //
+                "         var e = bp.sync({ waitFor:[ bp.Event(\"X\") ] });\n" + //
+                "      }\n" + //
+                "});\n" + "bp.registerBThread('bt2', function(){" + //
+                "    while(true){\n" + //
+                "       var y = bp.sync({ request:[ bp.Event(\"X\") ] });\n" + //
+                "}});\n");
+        DfsBProgramVerifier vfr = new DfsBProgramVerifier();
+        long timeout = 2;
+        vfr.setTimeout(timeout);
+        final VerificationResult res = vfr.verify(bprog);
+        assertEquals(VerificationResult.ViolationType.Timeout, res.getViolationType());
+        assertTrue(res.getTimeMillies() >= timeout);
+
+
+    }
+
 
 }