Merge 4836e2e into 8844613

bThink-BGU · Jun 2, 2018 · 189627c · 189627c
2 parents 8844613 + 4836e2e
commit 189627c
Showing 1 changed file with 45 additions and 0 deletions.
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
@@ -199,5 +199,50 @@ private void testEqualRuns(VisitedStateStore storeToUse) throws Exception {
             assertTrue(storeToUse.isVisited(next2));
         }
     }
+
+    @Test
+    public void testStateStoreJavaVarsNoHash() throws Exception {
+        VisitedStateStore noHash = new BThreadSnapshotVisitedStateStore();
+        testStateStoreJavaVars(noHash);
+    }
+
+    @Test
+    public void testStateStoreJavaVarsHash() throws Exception {
+        VisitedStateStore hashStore = new HashVisitedStateStore();
+        testStateStoreJavaVars(hashStore);
+    }
+
+    private void testStateStoreJavaVars(VisitedStateStore storeToUse) throws Exception {
+        BProgram bprog = new StringBProgram("bp.registerBThread(function(){\n" +
+                "        var a = new java.lang.Integer(7);\n" +
+                "        bp.sync({request:bp.Event(\"A\")});\n" +
+                "        while (true) {" +
+                "           //bp.log.warn(a);\n" +
+                "           bp.sync({request:bp.Event(\"R\")});\n" +
+                "           a = java.lang.Integer.reverse(a);\n" +
+                "        }\n" +
+                "});");
+        ExecutorService execSvc = ExecutorServiceMaker.makeWithName("StoreSvcEqualJSVar");
+        DfsBProgramVerifier sut = new DfsBProgramVerifier();
+
+        Node next = Node.getInitialNode(bprog, execSvc);
+        storeToUse.store(next);
+        assertTrue(storeToUse.isVisited(next));
+        //now we enter the loop and generate initial node
+        //a is 7
+        next = sut.getUnvisitedNextNode(next, execSvc);
+        assertFalse(storeToUse.isVisited(next));
+        storeToUse.store(next);
+        //Now loop again, this should also not exist
+        next = sut.getUnvisitedNextNode(next, execSvc);
+        //a should be -536870912
+        assertFalse(storeToUse.isVisited(next));
+        storeToUse.store(next);
+        //now a should be 7 again
+        //and now we should see the node
+        next = sut.getUnvisitedNextNode(next, execSvc);
+        assertTrue(storeToUse.isVisited(next));
+
+    }
 }