MOAR TESTSTS

bThink-BGU · Feb 17, 2019 · 547c2a9 · 547c2a9
1 parent cca3f6f
commit 547c2a9
Show file tree

Hide file tree

Showing 11 changed files with 60 additions and 36 deletions.
diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifier.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifier.java
@@ -25,7 +25,6 @@
 
 import il.ac.bgu.cs.bp.bpjs.analysis.violations.Violation;
 import java.util.ArrayList;
-import java.util.Collections;
 import java.util.List;
 
 import il.ac.bgu.cs.bp.bpjs.model.BProgram;

diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/Violation.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/Violation.java
@@ -33,7 +33,7 @@
  */
 public abstract class Violation {
 
-    private ExecutionTrace counterExampleTrace;
+    private final ExecutionTrace counterExampleTrace;
 
     public Violation(ExecutionTrace counterExampleTrace) {
         this.counterExampleTrace = counterExampleTrace;
@@ -50,10 +50,5 @@ public Violation(ExecutionTrace counterExampleTrace) {
     public ExecutionTrace getCounterExampleTrace() {
         return counterExampleTrace;
     }
-
-    public void setCounterExampleTrace(ExecutionTrace counterExampleTrace) {
-        this.counterExampleTrace = counterExampleTrace;
-    }
-
 
 }
diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshot.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshot.java
@@ -145,36 +145,30 @@ public BProgramSyncSnapshot triggerEvent(BEvent anEvent, ExecutorService exSvc,
         }
 
         BPEngineTask.Listener halter = new ViolationRecorder(bprog, violationRecord);
-
-        try {
-            // add the run results of all those who advance this stage
-            nextRound.addAll(exSvc.invokeAll(
-                                resumingThisRound.stream()
-                                                 .map(bt -> new ResumeBThread(bt, anEvent, halter))
-                                                 .collect(toList())
-                    ).stream().map(f -> safeGet(f)).filter(Objects::nonNull).collect(toList())
-            );
 
-            // inform listeners which b-threads completed
-            Set<String> nextRoundIds = nextRound.stream().map(t->t.getName()).collect(toSet());
-            resumingThisRound.stream()
-                    .filter(t->!nextRoundIds.contains(t.getName()))
-                    .forEach(t->listeners.forEach(l->l.bthreadDone(bprog, t)));
+        // add the run results of all those who advance this stage
+        nextRound.addAll(exSvc.invokeAll(
+                            resumingThisRound.stream()
+                                             .map(bt -> new ResumeBThread(bt, anEvent, halter))
+                                             .collect(toList())
+                ).stream().map(f -> safeGet(f)).filter(Objects::nonNull).collect(toList())
+        );
 
-            executeAllAddedBThreads(nextRound, exSvc, halter);
-            nextExternalEvents.addAll( bprog.drainEnqueuedExternalEvents() );
+        // inform listeners which b-threads completed
+        Set<String> nextRoundIds = nextRound.stream().map(t->t.getName()).collect(toSet());
+        resumingThisRound.stream()
+                .filter(t->!nextRoundIds.contains(t.getName()))
+                .forEach(t->listeners.forEach(l->l.bthreadDone(bprog, t)));
 
-            // carry over BThreads that did not advance this round to next round.
-            nextRound.addAll(sleepingThisRound);
+        executeAllAddedBThreads(nextRound, exSvc, halter);
+        nextExternalEvents.addAll( bprog.drainEnqueuedExternalEvents() );
 
+        // carry over BThreads that did not advance this round to next round.
+        nextRound.addAll(sleepingThisRound);
 
-            return new BProgramSyncSnapshot(bprog, nextRound, nextExternalEvents, violationRecord.get());
+
+        return new BProgramSyncSnapshot(bprog, nextRound, nextExternalEvents, violationRecord.get());
 
-        } catch ( RejectedExecutionException ree ) {
-            // The executor thread pool must have been shut down, e.g. due to program violation.
-            return new BProgramSyncSnapshot(bprog, Collections.emptySet(), nextExternalEvents, violationRecord.get());
-
-        }
     }
 
     private void handleInterrupts(BEvent anEvent, Iterable<BProgramRunnerListener> listeners, BProgram bprog, Context ctxt) {

diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/GeneralTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/GeneralTest.java
@@ -116,6 +116,8 @@ public void ended(BProgram bp) {
             actualFinalEventNames.stream().sorted().forEach( System.out::println );
         }
 
+        svc.shutdown();
+
     }
 
 }
diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifierTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifierTest.java
@@ -45,6 +45,17 @@
  * @author michael
  */
 public class DfsBProgramVerifierTest {
+
+    @Test
+    public void sanity() throws Exception {
+        BProgram program = new ResourceBProgram("DFSVerifierTests/AAABTrace.js");
+        DfsBProgramVerifier sut = new DfsBProgramVerifier();
+        sut.setDebugMode(true);
+        sut.setMaxTraceLength(3);
+        sut.setIterationCountGap(1);
+        sut.verify(program);
+        assertEquals( ExecutionTraceInspections.DEFAULT_SET, sut.getInspections() );
+    }
 
     @Test
     public void simpleAAABTrace_forgetfulStore() throws Exception {

diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/MultipleViolationsTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/MultipleViolationsTest.java
@@ -25,7 +25,9 @@
 
 import il.ac.bgu.cs.bp.bpjs.analysis.violations.Violation;
 import il.ac.bgu.cs.bp.bpjs.model.ResourceBProgram;
+import java.util.HashSet;
 import java.util.List;
+import java.util.Set;
 import java.util.concurrent.atomic.AtomicBoolean;
 import java.util.concurrent.atomic.AtomicInteger;
 import static org.junit.Assert.assertEquals;
@@ -44,6 +46,7 @@ public void testMultipleFailedAssertions() throws Exception {
         final ResourceBProgram bprog = new ResourceBProgram("DFSVerifierTests/MultipleFailedAssertions.js");
         AtomicInteger violationCount = new AtomicInteger();
         AtomicBoolean maxLengthHit = new AtomicBoolean(false);
+        final Set<Violation> violations = new HashSet<>();
 
         DfsBProgramVerifier vfr = new DfsBProgramVerifier();
         vfr.setMaxTraceLength(6);
@@ -62,6 +65,7 @@ public void maxTraceLengthHit(List<DfsTraversalNode> aTrace, DfsBProgramVerifier
             public boolean violationFound(Violation aViolation, DfsBProgramVerifier vfr) {
                 int num = violationCount.incrementAndGet();
                 System.out.println("Violation " + num + ": " + aViolation.decsribe() );
+                violations.add(aViolation);
                 return true;
             }
 
@@ -72,7 +76,11 @@ public boolean violationFound(Violation aViolation, DfsBProgramVerifier vfr) {
 
         assertFalse( res.isViolationFound() );
         assertEquals( 3, violationCount.get() );
+        assertEquals( 3, violations.size() );
         assertTrue( maxLengthHit.get() );
+        Violation v = violations.iterator().next();
+        assertFalse( v.equals(null) );
+        assertFalse( v.equals("Not a Violation") );
     }
 
     @Test

diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/NodeEqualsTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/NodeEqualsTest.java
@@ -11,6 +11,7 @@
 import il.ac.bgu.cs.bp.bpjs.model.StringBProgram;
 import il.ac.bgu.cs.bp.bpjs.model.BEvent;
 import java.util.concurrent.ExecutorService;
+import org.junit.After;
 import org.junit.Before;
 
 public class NodeEqualsTest {
@@ -96,4 +97,9 @@ public void basicsTest() throws Exception {
     public void setup() {
         exSvc = ExecutorServiceMaker.makeWithName("Test");
     }
+
+    @After
+    public void teardown() {
+        exSvc.shutdown();
+    }
 }
diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/StateStoreTests.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/StateStoreTests.java
@@ -24,6 +24,8 @@ public void ForgetfulStore() throws Exception {
 
         DfsTraversalNode next = sut.getUnvisitedNextNode(initial, execSvc);
         assertFalse(forgetful.isVisited(next.getSystemState()));
+
+        execSvc.shutdown();
     }
 
     @Test
@@ -54,6 +56,7 @@ private void TestAAABTraceStore(VisitedStateStore storeToUse) throws Exception {
         storeToUse.clear();
         assertFalse(storeToUse.isVisited(next.getSystemState()));
         assertFalse(storeToUse.isVisited(initial.getSystemState()));
+        execSvc.shutdown();
     }
 
     @Test
@@ -103,6 +106,7 @@ private void TestDiffJSVar(VisitedStateStore storeToUse) throws Exception {
         BProgramSyncSnapshot state1 = snapshots.get(1).getSystemState();
         BProgramSyncSnapshot state2 = snapshots.get(2).getSystemState();
         assertNotEquals(state1, state2);
+        execSvc.shutdown();
     }
 
     @Test
@@ -153,6 +157,7 @@ private void TestEqualJSVar(VisitedStateStore storeToUse) throws Exception {
         BProgramSyncSnapshot state1 = snapshots.get(1).getSystemState();
         BProgramSyncSnapshot state2 = snapshots.get(2).getSystemState();
         assertEquals(state1, state2);
+        execSvc.shutdown();
     }
 
     /*
@@ -198,6 +203,7 @@ private void testEqualRuns(VisitedStateStore storeToUse) throws Exception {
             storeToUse.store(next1.getSystemState());
             assertTrue(storeToUse.isVisited(next2.getSystemState()));
         }
+        execSvc.shutdown();
     }
 
     @Test
@@ -242,7 +248,7 @@ private void testStateStoreJavaVars(VisitedStateStore storeToUse) throws Excepti
         //and now we should see the node
         next = sut.getUnvisitedNextNode(next, execSvc);
         assertTrue(storeToUse.isVisited(next.getSystemState()));
-
+        execSvc.shutdown();
     }
 }
 
diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/bprogramio/BProgramSyncSnapshotClonerTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/bprogramio/BProgramSyncSnapshotClonerTest.java
@@ -73,6 +73,7 @@ public void testSerialization() throws Exception {
         BProgramSyncSnapshotIO io = new BProgramSyncSnapshotIO(bprog);
         byte[] out = io.serialize(cur);
         io.deserialize(out);
+        exSvc.shutdown();
     }
 
     @Test
@@ -92,6 +93,7 @@ public void testSerializatioWithExternals() throws Exception {
         BProgramSyncSnapshot deserialized = io.deserialize(out);
 
         assertEquals( Arrays.asList(new BEvent("External1"), new BEvent("External2")), deserialized.getExternalEvents());
+        exSvc.shutdown();
     }
 
     @Test

diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/ContinuationGames.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/ContinuationGames.java
@@ -41,6 +41,7 @@
 import il.ac.bgu.cs.bp.bpjs.model.BEvent;
 import java.util.HashMap;
 import java.util.Map;
+import java.util.concurrent.ExecutorService;
 import org.mozilla.javascript.NativeContinuation;
 import org.mozilla.javascript.ScriptRuntime;
 
@@ -70,17 +71,17 @@ public static void main(String[] args) throws Exception {
 
         // Run the top-level code (b-threads are registered but not yet run)
         BProgramSyncSnapshot cur = bprog.setup();
+        ExecutorService execSvc = ExecutorServiceMaker.makeWithName("TEST");
 
         // Run to first bp.sync
-        cur = cur.start( ExecutorServiceMaker.makeWithName("TEST"));
+        cur = cur.start(execSvc);
 
         // Get a snapshot
         final BThreadSyncSnapshot snapshot = cur.getBThreadSnapshots().iterator().next();
         System.out.println(snapshot);
 
         // Serialize snapshot
         byte[] serializedContinuationAndScope = null;
-        Object bp = null;
         try {
             Context ctxt = Context.enter(); // need Javascript environment for this, even though we're not executing code per se.
 
@@ -91,7 +92,6 @@ public static void main(String[] args) throws Exception {
             for ( Scriptable sc=scope; sc!=null; sc = sc.getParentScope() ) {
                 System.out.println("SCOPE START");
                 if ( sc.has("bp", sc) ) {
-                    bp = sc.get("bp", sc);
                     sc.delete("bp");
                     System.out.println("bp deleted.");
                 }
@@ -111,6 +111,7 @@ public static void main(String[] args) throws Exception {
             }
             System.out.println("Seriazlied to " + serializedContinuationAndScope.length + " bytes.");
         } finally {
+            execSvc.shutdown();
             Context.exit();
         }
 

diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/model/BThreadSyncSnapshotTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/model/BThreadSyncSnapshotTest.java
@@ -92,7 +92,7 @@ public void testJavaVarState() throws InterruptedException {
         EventSelectionResult esr = bprog.getEventSelectionStrategy().select(postSync1, possibleEvents).get();
         BProgramSyncSnapshot postSync2 = postSync1.triggerEvent(esr.getEvent(), execSvcA, listeners);
         assertNotEquals(postSync1.getBThreadSnapshots(), postSync2.getBThreadSnapshots());
-        execSvcA.shutdown();;
+        execSvcA.shutdown();
     }