0.10.2 setup

README.md

@@ -44,6 +44,9 @@ a link to this page somewhere in the documentation/system about section.
 
 ## Change Log for the BPjs Library.
 
+### 2019-03-10
+* :put_litter_in_its_place: Code cleanup.
+
 ### 2019-03-05
 * :sparkles: Serious makeover for the composable event suite. Users can no compose event sets using `or`,`and`, and `not` (and even `xor`, `nor` and `nand`) and get semantically correct sets that support verification.
   for example, this works:

dependency-reduced-pom.xml

@@ -4,7 +4,7 @@
   <groupId>com.github.bthink-bgu</groupId>
   <artifactId>BPjs</artifactId>
   <name>BPjs</name>
-  <version>0.10.1-SNAPSHOT</version>
+  <version>0.10.1</version>
   <description>Provides a runtime for behavioral programs written in Javascript. It can 
         run stand-alone (from the commmandline) or be embedded in larger 
         JVM-based systems.</description>
@@ -260,8 +260,8 @@
     </snapshotRepository>
   </distributionManagement>
   <properties>
-    <exec.mainClass>il.ac.bgu.cs.bp.bpjs.mains.BPJsCliRunner</exec.mainClass>
     <java.version>1.8</java.version>
+    <exec.mainClass>il.ac.bgu.cs.bp.bpjs.mains.BPJsCliRunner</exec.mainClass>
     <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
   </properties>
 </project>

pom.xml

@@ -5,15 +5,15 @@
 
     <groupId>com.github.bthink-bgu</groupId>
     <artifactId>BPjs</artifactId>
-    <version>0.10.1</version>
+    <version>0.10.2</version>
     <packaging>jar</packaging>
 
     <name>BPjs</name>
     <url>https://github.com/bThink-BGU/</url>
     <description>
-        Provides a runtime for behavioral programs written in Javascript. It can 
-        run stand-alone (from the commmandline) or be embedded in larger 
-        JVM-based systems.
+        Provides runtime and analysis for behavioral programs written in 
+        JavaScript. It can run stand-alone (from the commmandline) or be 
+        embedded in larger JVM-based systems.
     </description>
 
     <licenses>
@@ -144,6 +144,18 @@
                     </archive>
                 </configuration>
             </plugin>
+            <plugin>
+                <groupId>org.apache.maven.plugins</groupId>
+                <artifactId>maven-jar-plugin</artifactId>
+                <version>3.1.1</version>
+                <configuration>
+                    <archive>
+                        <manifest>
+                            <mainClass>il.ac.bgu.cs.bp.bpjs.mains.BPJsCliRunner</mainClass>
+                        </manifest>
+                    </archive>
+                </configuration>
+            </plugin>
         </plugins>        
     </build>
     <profiles>

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

@@ -265,11 +265,11 @@ public long getMaxTraceLength() {
         return maxTraceLength;
     }
 
-    public void setVisitedNodeStore(VisitedStateStore aVisitedNodeStore) {
-        visited = aVisitedNodeStore;
+    public void setVisitedStateStore(VisitedStateStore aVisitedStateStore) {
+        visited = aVisitedStateStore;
     }
 
-    public VisitedStateStore getVisitedNodeStore() {
+    public VisitedStateStore getVisitedStateStore() {
         return visited;
     }
 

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

@@ -24,35 +24,26 @@
 package il.ac.bgu.cs.bp.bpjs.analysis;
 
 import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot;
-import il.ac.bgu.cs.bp.bpjs.model.BThreadSyncSnapshot;
+import java.util.HashSet;
 import java.util.Set;
-import java.util.TreeSet;
 
 /**
  * A {@link VisitedStateStore} that uses a hash function over the BProgram's states.
  * @author michael
  */
 public class HashVisitedStateStore implements VisitedStateStore {
-    private final Set<Long> visited = new TreeSet<>();
+    private final Set<Integer> visited = new HashSet<>();
 
     @Override
     public void store(BProgramSyncSnapshot bss) {
-        visited.add( hash(bss.getBThreadSnapshots()) );
+        visited.add( bss.hashCode() );
     }
 
     @Override
     public boolean isVisited(BProgramSyncSnapshot bss) {
-        return visited.contains( hash(bss.getBThreadSnapshots()) );
+        return visited.contains( bss.hashCode() );
     }
 
-    private long hash( Set<BThreadSyncSnapshot> snapshots ) {
-        long hash = 1;
-        for ( BThreadSyncSnapshot snp : snapshots ) {
-            hash = hash * snp.getContinuationProgramState().hashCode();// * (snp.getName().hashCode()+1);
-        }
-        return hash;
-    }
-
     @Override
     public long getVisitedStateCount() {
         return visited.size();

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

@@ -62,7 +62,7 @@ public long getScannedStatesCount() {
         return statesScanned;
     }
 
-    public long getEdgesScanned() {
+    public long getScannedEdgesCount() {
         return edgesScanned;
     }
 

src/main/java/il/ac/bgu/cs/bp/bpjs/mains/BPJsCliRunner.java

@@ -117,9 +117,9 @@ private void logScriptExceptionAndQuit(EvaluatorException ee, String arg) {
 
             if ( switchPresent("--full-state-storage", args) ) {
                 println("Using full state storage");
-                vfr.setVisitedNodeStore( new BThreadSnapshotVisitedStateStore() );
+                vfr.setVisitedStateStore( new BThreadSnapshotVisitedStateStore() );
             } else {
-                vfr.setVisitedNodeStore( new HashVisitedStateStore() );
+                vfr.setVisitedStateStore( new HashVisitedStateStore() );
             }
             if ( switchPresent("--liveness", args) ) {
                 vfr.addInspection(ExecutionTraceInspections.HOT_BPROGRAM_CYCLES);

src/main/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshot.java

@@ -49,6 +49,7 @@ public class BProgramSyncSnapshot {
     private final List<BEvent> externalEvents;
     private final BProgram bprog;
     private final AtomicReference<FailedAssertion> violationRecord = new AtomicReference<>();
+    private transient int hashCodeCache = Integer.MIN_VALUE;
 
     /** A flag to ensure the snapshot is only triggered once. */
     private boolean triggered=false;
@@ -327,7 +328,10 @@ Stream<StartFork> convertToTasks(ForkStatement fkStmt, BPEngineTask.Listener lis
 
     @Override
     public int hashCode() {
-        return Objects.hash(threadSnapshots, externalEvents);
+        if ( hashCodeCache == Integer.MIN_VALUE  ) {
+            hashCodeCache = Objects.hash(threadSnapshots, externalEvents);
+        }
+        return hashCodeCache;
     }
 
     @Override

src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventsets/EventSets.java

@@ -1,6 +1,7 @@
 package il.ac.bgu.cs.bp.bpjs.model.eventsets;
 
 import il.ac.bgu.cs.bp.bpjs.model.BEvent;
+import java.io.ObjectStreamException;
 
 /**
  * Utility class for commonly used event sets.
@@ -27,7 +28,7 @@ public String toString() {
             return ("{all}");
         }
 
-        private Object readResolve() {
+        private Object readResolve() throws ObjectStreamException {
             return all;
         }
     };
@@ -47,7 +48,7 @@ public String toString() {
             return "{none}";
         }
 
-        private Object readResolve() {
+        private Object readResolve() throws ObjectStreamException {
             return none;
         }
     };

src/test/java/il/ac/bgu/cs/bp/bpjs/TicTacToe/TicTacToeVerificationMain.java

@@ -46,7 +46,7 @@ public static void main(String[] args) throws InterruptedException {
 
             vfr.setMaxTraceLength(70);
 //            vfr.setDebugMode(true);
-            vfr.setVisitedNodeStore(new BThreadSnapshotVisitedStateStore());
+            vfr.setVisitedStateStore(new BThreadSnapshotVisitedStateStore());
             vfr.setProgressListener(new PrintDfsVerifierListener() );
 
             final VerificationResult res = vfr.verify(bprog);

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

@@ -26,15 +26,8 @@
 import static il.ac.bgu.cs.bp.bpjs.TestUtils.makeBPSS;
 import il.ac.bgu.cs.bp.bpjs.mocks.MockBThreadSyncSnapshot;
 import il.ac.bgu.cs.bp.bpjs.model.BEvent;
-import il.ac.bgu.cs.bp.bpjs.model.BProgram;
-import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot;
 import il.ac.bgu.cs.bp.bpjs.model.StringBProgram;
 import il.ac.bgu.cs.bp.bpjs.model.SyncStatement;
-import java.util.List;
-import org.junit.After;
-import org.junit.AfterClass;
-import org.junit.Before;
-import org.junit.BeforeClass;
 import org.junit.Test;
 import static org.junit.Assert.*;
 

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

@@ -63,7 +63,7 @@ public void simpleAAABTrace_forgetfulStore() throws Exception {
         DfsBProgramVerifier sut = new DfsBProgramVerifier();
         sut.setProgressListener(new PrintDfsVerifierListener());
         program.appendSource(Requirements.eventNotSelected("B"));
-        sut.setVisitedNodeStore(new ForgetfulVisitedStateStore());
+        sut.setVisitedStateStore(new ForgetfulVisitedStateStore());
         VerificationResult res = sut.verify(program);
         assertTrue(res.isViolationFound());
         assertEquals("AAAB", traceEventNamesString(res, ""));
@@ -77,7 +77,7 @@ public void simpleAAABTrace() throws Exception {
 
         sut.setProgressListener(new PrintDfsVerifierListener());
         program.appendSource(Requirements.eventNotSelected("B"));
-        sut.setVisitedNodeStore(new BThreadSnapshotVisitedStateStore());
+        sut.setVisitedStateStore(new BThreadSnapshotVisitedStateStore());
         VerificationResult res = sut.verify(program);
         assertTrue(res.isViolationFound());
         assertEquals("AAAB", traceEventNamesString(res, ""));
@@ -91,12 +91,12 @@ public void simpleAAABTrace_hashedNodeStore() throws Exception {
         sut.setProgressListener(new PrintDfsVerifierListener());
         program.appendSource(Requirements.eventNotSelected("B"));
         VisitedStateStore stateStore = new HashVisitedStateStore();
-        sut.setVisitedNodeStore(stateStore);
+        sut.setVisitedStateStore(stateStore);
         VerificationResult res = sut.verify(program);
         assertTrue(res.isViolationFound());
         assertEquals("AAAB", traceEventNamesString(res, ""));
         //Add trivial getter check
-        VisitedStateStore retStore = sut.getVisitedNodeStore();
+        VisitedStateStore retStore = sut.getVisitedStateStore();
         assertSame(retStore, stateStore);
     }
 
@@ -117,7 +117,7 @@ public void testAAABRun() {
     public void deadlockTrace() throws Exception {
         BProgram program = new ResourceBProgram("DFSVerifierTests/deadlocking.js");
         DfsBProgramVerifier sut = new DfsBProgramVerifier();
-        sut.setVisitedNodeStore(new ForgetfulVisitedStateStore());
+        sut.setVisitedStateStore(new ForgetfulVisitedStateStore());
         VerificationResult res = sut.verify(program);
 
         assertTrue(res.isViolationFound());
@@ -163,7 +163,7 @@ public void testTwoSimpleBThreads() throws Exception {
 
         assertFalse(res.isViolationFound());
         assertEquals(4, res.getScannedStatesCount());
-        assertEquals(4, res.getEdgesScanned());
+        assertEquals(4, res.getScannedEdgesCount());
     }
 
     @Test(timeout = 2000)
@@ -236,7 +236,7 @@ public void testVariablesEquailtyInBT() throws Exception {
         assertEquals(5, res.getScannedStatesCount());
 
         // in this case only one option per state
-        assertEquals(5, res.getEdgesScanned()); 
+        assertEquals(5, res.getScannedEdgesCount()); 
 
     }
 
@@ -299,7 +299,7 @@ public void testJavaVariablesInBT() throws Exception {
         assertTrue(res.isViolationFound());
         assertTrue(res.getViolation().get() instanceof FailedAssertionViolation);
         assertEquals(2, res.getScannedStatesCount());
-        assertEquals(1, res.getEdgesScanned());
+        assertEquals(1, res.getScannedEdgesCount());
     }
 
 }

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

@@ -152,9 +152,9 @@ private static BenchmarkResult measureProgram(int object_type) throws Exception
                 System.gc();
                 snapshotSet[i] = getStateSizes(makeBProgram(IMPLEMENTATION, valueMap), NUM_STEPS);
                 System.gc();
-                verifier.setVisitedNodeStore(store);
+                verifier.setVisitedStateStore(store);
                 verificationTimes[i] = getVerification(verifier, IMPLEMENTATION, valueMap, ITERATIONS);
-                verifier.setVisitedNodeStore(storeHash);
+                verifier.setVisitedStateStore(storeHash);
                 verificationTimesHash[i] = getVerification(verifier, IMPLEMENTATION, valueMap, ITERATIONS);
                 System.gc();
 
@@ -229,9 +229,9 @@ private static BenchmarkResult measureProgram(EventSelectionStrategy strategy, i
                 System.gc();
                 snapshotSet[i] = getStateSizes(makeBProgram(IMPLEMENTATION, valueMap, strategy), NUM_STEPS);
                 System.gc();
-                verifier.setVisitedNodeStore(store);
+                verifier.setVisitedStateStore(store);
                 verificationTimes[i] = getVerificationTime(verifier, IMPLEMENTATION, valueMap, ITERATIONS, strategy);
-                verifier.setVisitedNodeStore(storeHash);
+                verifier.setVisitedStateStore(storeHash);
                 verificationTimesHash[i] = getVerificationTime(verifier, IMPLEMENTATION, valueMap, ITERATIONS, strategy);
                 System.gc();
 
@@ -252,7 +252,7 @@ private static BProgram makeBProgram(String programPath, Map<String, Object> val
         }
 
         static VerificationResult[] getVerificationTime(DfsBProgramVerifier vfr, String programPath, Map<String, Object> valueMap, int iteration_count, EventSelectionStrategy strategy) {
-            String res = String.format("Measuring Verification time with %s store", vfr.getVisitedNodeStore().getClass().getName());
+            String res = String.format("Measuring Verification time with %s store", vfr.getVisitedStateStore().getClass().getName());
             LOGGER.info(res);
             return LongStream.range(0, iteration_count).mapToObj(i -> {
                 try {

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

@@ -93,7 +93,7 @@ public void testHotBProgramCycle_withJsEventSets() throws Exception {
         DfsBProgramVerifier vfr = new DfsBProgramVerifier();
         // Adding the inspector means it will be the only inspector run, as the default set will not be used.
         vfr.addInspection(ExecutionTraceInspections.HOT_BPROGRAM_CYCLES);
-        vfr.setVisitedNodeStore( new BThreadSnapshotVisitedStateStore() );
+        vfr.setVisitedStateStore( new BThreadSnapshotVisitedStateStore() );
         final VerificationResult res = vfr.verify(bprog);
 
         assertTrue(res.isViolationFound());

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

@@ -87,8 +87,8 @@ public void verify() throws InterruptedException {
 
             vfr.setProgressListener(new PrintDfsVerifierListener());
             vfr.setIterationCountGap(10);
-            vfr.setVisitedNodeStore(new BThreadSnapshotVisitedStateStore());
-//            vfr.setVisitedNodeStore(new ForgetfulVisitedStateStore());
+            vfr.setVisitedStateStore(new BThreadSnapshotVisitedStateStore());
+//            vfr.setVisitedStateStore(new ForgetfulVisitedStateStore());
 
             vfr.addInspection(ExecutionTraceInspections.FAILED_ASSERTIONS); // We only want failed assertions, deadlocks are OK here, in the greateer program(!)
             final VerificationResult res = vfr.verify(bprog);

src/test/java/il/ac/bgu/cs/bp/bpjs/execution/jsproxy/BProgramJsProxyTest.java

@@ -100,7 +100,7 @@ public void testEquality() {
     public void DeadlockSameThread() throws Exception{
         BProgram bpr = new ResourceBProgram("bpsync-blockrequest.js");
         DfsBProgramVerifier sut = new DfsBProgramVerifier();
-        sut.setVisitedNodeStore(new BThreadSnapshotVisitedStateStore());
+        sut.setVisitedStateStore(new BThreadSnapshotVisitedStateStore());
         VerificationResult res = sut.verify(bpr);
         assertTrue(res.isViolationFound());
         assertTrue(res.getViolation().get() instanceof DeadlockViolation);

src/test/java/il/ac/bgu/cs/bp/bpjs/mains/CaseofTheHotFruitBProgram.java

@@ -60,7 +60,7 @@ public static void verify(BProgram bprog) throws Exception {
         DfsBProgramVerifier vfr = new DfsBProgramVerifier();
         // Adding the inspector means it will be the only inspector run, as the default set will not be used.
         vfr.addInspection(ExecutionTraceInspections.HOT_BPROGRAM_CYCLES);
-        vfr.setVisitedNodeStore( new BThreadSnapshotVisitedStateStore() );
+        vfr.setVisitedStateStore( new BThreadSnapshotVisitedStateStore() );
         final VerificationResult res = vfr.verify(bprog);
 
         System.out.println("Violation found: " + res.isViolationFound());

src/test/java/il/ac/bgu/cs/bp/bpjs/mains/StateStorePerformanceComparison.java

@@ -61,11 +61,11 @@ public static void main(String[] args) throws Exception {
         verifier.addInspection(ExecutionTraceInspections.FAILED_ASSERTIONS);
 
         // test
-        verifier.setVisitedNodeStore(new BThreadSnapshotVisitedStateStore());
+        verifier.setVisitedStateStore(new BThreadSnapshotVisitedStateStore());
         runVerifier(verifier);
-        verifier.setVisitedNodeStore(new HashVisitedStateStore());
+        verifier.setVisitedStateStore(new HashVisitedStateStore());
         runVerifier(verifier);
-        verifier.setVisitedNodeStore(new ForgetfulVisitedStateStore());
+        verifier.setVisitedStateStore(new ForgetfulVisitedStateStore());
         runVerifier(verifier);
 
     }
@@ -80,7 +80,7 @@ private static BProgram makeBProgram() {
     }
 
     private static void runVerifier(DfsBProgramVerifier vfr) throws Exception {
-        System.out.println("Testing " + vfr.getVisitedNodeStore());
+        System.out.println("Testing " + vfr.getVisitedStateStore());
         System.out.println("Heating up");
         for (int i = 0; i < HEAT_UP_ITERATIONS; i++) {
             vfr.verify(makeBProgram());