Setting up 0.9.8...

README.md

@@ -1,4 +1,4 @@
-# BPjs: A Javascript-based Behavioral Programming Runtime.
+# BPjs: A JavaScript-based Behavioral Programming Runtime.
 
 This repository contains a javascript-based [BP](http://www.b-prog.org) library.
 
@@ -24,7 +24,7 @@ a link to this page somewhere in the documentation/system about section.
     <dependency>
         <groupId>com.github.bthink-bgu</groupId>
         <artifactId>BPjs</artifactId>
-        <version>0.9.7</version>
+        <version>0.9.8</version>
     </dependency>
     ...
 </dependencies>
@@ -44,8 +44,28 @@ a link to this page somewhere in the documentation/system about section.
 
 ## Change Log for the BPjs Library.
 
+### 2019-02-06
+* :arrow_up::arrow_up::sparkles: Verification areas refactored and generalized towards code reuse. Inspectors and traces are now general, and do not assume they were created from the DFS verifier.
+* :arrow_up: Improved state hashing algorithm in the hash-based visited state storage.
+* :arrow_up: Updated documentation of the verification parts.
+* :arrow_up: More tests.
+* :arrow_up: Updated maven compiler plugin.
+* :bug: Fixed a corner case where b-programs with immediate failed assertions would still attempt running certain machines.
+
+### 2019-02-05
+* :arrow_up: :tada: Event selection strategies now accept `BProgramSyncSnapshot`, rather than a set of sync statements and external events.
+
+### 2019-02-04
+* :sparkles: Testing infrastructure for execution traces.
+* :arrow_up: More terminology cleanups in the api (e.g. "bsync" converted to "sync")
+
+### 2019-02-03
+* :arrow_up: `VisitedStateStore` now stores *states*, not DFS nodes. So it's more reusable that way.
+
 ### 2019-01-19
 * :sparkles: More tests.
+* :arrow_up: `BriefPrintDfsVerifierListener` => `PrintDfsVerifierListener`, so that it's consistent with `PrintBProgramRunnerListener`.
+* :arrow_up: Incorporated the "BPjs Tips" file to the central documentation.
 
 ### 2019-01-18
 * :bug: Fixed a that cause equality tests of JS event sets to return false negatives.

dependency-reduced-pom.xml

@@ -4,7 +4,7 @@
   <groupId>com.github.bthink-bgu</groupId>
   <artifactId>BPjs</artifactId>
   <name>BPjs</name>
-  <version>0.9.7-SNAPSHOT</version>
+  <version>0.9.8-SNAPSHOT</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>
@@ -32,7 +32,7 @@
     <plugins>
       <plugin>
         <artifactId>maven-compiler-plugin</artifactId>
-        <version>3.1</version>
+        <version>3.8.0</version>
         <configuration>
           <source>${java.version}</source>
           <target>${java.version}</target>

docs/source/Examples_code/DfsVerifierSample.java

@@ -4,6 +4,7 @@
 vrf.setProgressListener(new BriefPrintDfsVerifierListener());  // add a listener to print progress
 VerificationResult res = vrf.verify(program);                  // this might take a while
 
-res.isCounterExampleFound();  // true iff a counter example was found
-res.getViolationType();       // Failed assertion, or a deadlock
-res.getCounterExampleTrace(); // trace of events leading to the violation.
+res.isViolationFound();  // true iff a counter example was found
+res.getViolation();      // an Optional<Violation>
+res.getViolation().ifPresent( v -> v.getCounterExampleTrace() );
+     // ExecutionTrace leading to the violation.

docs/source/embed-bpjs.rst

@@ -81,7 +81,7 @@ At Runtime
 * If the host Java program will push external events to the b-program, make the b-program wait for these events by calling ``bprog.setWaitForExternalEvents(true)``.
 * Instantiate a ``BProgramRunner`` object, and supply it with the ``BProgram`` instance.
 * Add listeners to the runner.
-* In the common case when the program needs to wait for external events (such as GUI interactions), set the ``isDaemon`` property of the ``BProgram`` to ``true``.
+* In the common case when the program needs to wait for external events (such as GUI interactions), set the ``isWaitForExternalEvents`` property of the ``BProgram`` to ``true``.
 * Call ``BProgramRunner::start()``.
 
 The BProgram will start running. Life-cycle and behavioral events will be passed to the listener objects. In case the host application would like to push an external event to the embedded b-program (e.g. because of a network request, or a user click), it should use the ``BProgram``'s `enqueueExternalEvent`_ method.
@@ -98,8 +98,7 @@ External Events vs. Internal Events
 
 There is no difference between external and internal events -- both are instances of the Java ``BEvent`` class, or a subclass of it. However, there may be a difference in how these events are treated by the event selection strategy. External events are made available to the strategy using an "external event queue". An event selection strategy may choose to ignore this queue whenever it can choose an event requested by a b-thread. But a strategy can also decide to choose an event from the queue even when there are internal events that are requested and not blocked.
 
-All event selection strategies currently included with BPjs ignore external events when there are choosable internal ones. This choice makes the system easier to reason about, as it gets to complete its reaction to one external event before it starts reacting to a new one. But this does not *have* to be the case.
-
+All event selection strategies currently included with BPjs ignore external events when there are internal ones available for selection. This choice makes the system easier to reason about, as it gets to complete its reaction to one external event before it starts reacting to a new one. But this does not *have* to be the case.
 
 
 .. _import directives: https://developer.mozilla.org/en-US/docs/Mozilla/Projects/Rhino/Scripting_Java

docs/source/images/bprogram-running.puml

@@ -9,7 +9,7 @@ class BProgramRunner {
 
 abstract class BProgram {
     - source
-    + isDaemon:boolean
+    + isWaitForExternalEvents:boolean
     + globalScope
     enqueueExternalEvent(e)
 

docs/source/index.rst

@@ -46,6 +46,7 @@ Topics:
    extendBPjs/index
    glossary
    examples
+   tips
 
 
 

docs/source/tips.rst

@@ -0,0 +1,106 @@
+BPjs tips
+=========
+
+Mainly for commands that are useful, but not in frequent use.
+
+Build jar with tests
+--------------------
+
+Useful for running long verifications outside of NetBeans
+
+::
+
+   mvn jar:test-jar
+
+NOTE: The build must use jdk8 for now. Execution can be done on any jdk
+(at least, worked for us with jdk11).
+
+Running verifications that live in the tests directory from the terminal
+------------------------------------------------------------------------
+
+to run the actual test, also build the uber-jar:
+
+::
+
+   mvn package -P uber-jar
+
+Now both live in the ``target`` directory. You can now run the test
+using Java, as usual, with both jars in the ``-cp`` parameter:
+
+::
+
+   java -cp target/BPjs-0.9.2-SNAPSHOT.uber.jar:target/BPjs-0.9.2-SNAPSHOT-tests.jar il.ac.bgu.cs.bp.bpjs.TicTacToe.TicTacToeVerMain
+
+Event comparison
+----------------
+
+Better to use non-strict JavaScript object comparison for now. So prefer
+
+.. code:: javascript
+
+     var evt = bp.sync({waitFor:ANY_ADDITION, block:chooseBlock(bias)});
+     if ( evt.name == ADD_WETS.name ) {
+       ...
+
+over
+
+.. code:: javascript
+
+     var evt = bp.sync({waitFor:ANY_ADDITION, block:chooseBlock(bias)});
+     if ( evt === ADD_WETS ) {
+       ...
+
+as the latter may return a false negative, especially during
+verification.
+
+Implementing Custom Events and Using Custom Objects as Event Data
+-----------------------------------------------------------------
+
+ALWAYS make sure that you have state-based, meaningful ``equals()`` and
+``hashCode()``. Or verification fails.
+
+State minimization
+------------------
+
+(yes, this is informed by the “data minimization” directive of privacy
+by design) It’s better to store least amount of data. E.g. in the
+fruitRatio.js file, this version of the b-threads yields three states:
+
+.. code:: javascript
+
+   bp.registerBThread( "RaspberryAdder", function(){
+       var fruitIndex=0;
+       while (true) {
+           var evt = null;
+           if ( fruitIndex > 0 ) {
+               evt = bp.hot(true).sync({request:ADD_RASPB,
+                                        waitFor:ADD_FRUIT});
+           } else {
+               evt = bp.sync({waitFor:ADD_FRUIT});
+           }
+           fruitIndex = fruitIndex + 
+                       evt.data.blueberries-evt.data.raspberries;
+       }
+   });
+
+Where this version yields 4 (note different location of ``var evt``) :
+
+.. code:: javascript
+
+   bp.registerBThread( "RaspberryAdder", function(){
+       var fruitIndex=0;
+       var evt = null;
+       while (true) {
+           if ( fruitIndex > 0 ) {
+               evt = bp.hot(true).sync({request:ADD_RASPB,
+                                        waitFor:ADD_FRUIT});
+           } else {
+               evt = bp.sync({waitFor:ADD_FRUIT});
+           }
+           fruitIndex = fruitIndex + 
+                       evt.data.blueberries-evt.data.raspberries;
+       }
+   });
+
+That’s because the former does not store the event from the previous
+iteration.

docs/source/verification/index.rst

@@ -72,9 +72,11 @@ A more in-depth discussion of verification in BPjs, including some techniques, c
 From the Command Line
 ~~~~~~~~~~~~~~~~~~~~~
 
-To verify a b-program from the commandline, simply add the ``--verify`` switch. Use ``--full-state-storage`` to force the verification to use the full state data when determining whether a state was visited (requires more memory).
+To verify a b-program from the commandline, simply add the ``--verify`` switch. Use ``--full-state-storage`` to force the verification to use the full state data when determining whether a state was visited (requires more memory). To concentrate on liveness violations, add the ``--liveness`` switch. To limit the (possibly infinite) depth of the scan, use ``--mac-trace-length``.
 
   $ java -jar bpjs.jar --verify hello-possibly-broken-world.js
+  $ java -jar bpjs.jar --verify --full-state-storage hello-possibly-broken-world.js
+  $ java -jar bpjs.jar --verify --liveness --full-state-storage hello-possibly-broken-world.js
 
 
 Assertions During Runtime

pom.xml

@@ -5,7 +5,7 @@
 
     <groupId>com.github.bthink-bgu</groupId>
     <artifactId>BPjs</artifactId>
-    <version>0.9.7</version>
+    <version>0.9.8</version>
     <packaging>jar</packaging>
 
     <name>BPjs</name>
@@ -105,7 +105,7 @@
             <plugin>
                 <groupId>org.apache.maven.plugins</groupId>
                 <artifactId>maven-compiler-plugin</artifactId>
-                <version>3.1</version>
+                <version>3.8.0</version>
                 <configuration>
                     <source>${java.version}</source>
                     <target>${java.version}</target>