Merge pull request #237 from bThink-BGU/develop

pre-0.14.0

Author: michbarsinai

README.md

@@ -32,7 +32,7 @@ If you use BPjs in an academic work, please consider citing it as:
     <dependency>
         <groupId>com.github.bthink-bgu</groupId>
         <artifactId>BPjs</artifactId>
-        <version>0.13.0</version>
+        <version>0.14.0</version>
     </dependency>
     ...
 </dependencies>
@@ -52,6 +52,22 @@ If you use BPjs in an academic work, please consider citing it as:
 
 ## Change Log for the BPjs Library.
 
+### 2025-12
+
+> [!IMPORTANT]
+> This update breaks backward compatibility in some minor ways around logging and custom executor services, as some methods were 
+> added and some classes were moved. See below for details. Updates should be pretty straightforward. Contact us if there's any
+> issue, we'll be happy to help.
+
+* :arrow_up: Upgraded to Rhino 1.8.1.
+* :arrow_up: Upgraded build and test dependencies.
+* :bug: Fixed and issued which prevented executor sevices from being re-used. Users who use custom executor services in managed environments now need to use the new methods on `ExecutorService`: `borrow()`/`borrowWithName()` and `returnService()`. Most users will not be affected by this change.[#236](https://github.com/bThink-BGU/BPjs/issues/236)
+* :tada: BPLog moved to own package. BPjs now has a central static logger, and no prints should go to `Systen.(out|err)` if you don't want them to. This is still the default behavior, but now messages go through the logging system first, so they can be directed to other logging destinations as well. [#231](https://github.com/bThink-BGU/BPjs/issues/231)
+* :arrow_up: `BpLog` is now easier to subclass, as core functionality moved to the interface using `default` methods.
+* :sparkles: Added a new logging level: `Error`. Exposed via `bp.log.error("ouch!")`.
+* :arrow_up: When logger is in `Fine` level, sotrage modifications are printed to the b-program's logger. [#230](https://github.com/bThink-BGU/BPjs/issues/230)
+* :tada: Violations now have location and stack trace. [#224](https://github.com/bThink-BGU/BPjs/issues/224)
+
 ### 2025-02
 * :arrow_up: Upgraded to Rhino 1.8.0 with updated JavaScript version. See the many updates [here](https://github.com/mozilla/rhino/releases/tag/Rhino1_8_0_Release).
 * :arrow_up: ``DfsBProgramVerifier.ProgressListener` now supports default methods for easier implementation.
@@ -64,7 +80,7 @@ If you use BPjs in an academic work, please consider citing it as:
 * :bug: Fixed a crash when accessing a b-program's global scope before the program starts to run.
 * :arrow_up: Added method `BProgramRunner::getListeners` ([#190](https://github.com/bThink-BGU/BPjs/issues/190)).
 * :arrow_up: Setting a non-function interrupt handler (which you should never do anyway) now throws an exception with informative message, rather than being siletly ignored. ([#114](https://github.com/bThink-BGU/BPjs/issues/114)).
-* :part_altertion_mark: Stack traces now use standard V8 formatting ([#198](https://github.com/bThink-BGU/BPjs/issues/198)).
+* :part_alternation_mark: Stack traces now use standard V8 formatting ([#198](https://github.com/bThink-BGU/BPjs/issues/198)).
 
 ### 2023-09
 * :sparkles: EventSets now have an `except` method, that allows removal of events from the set. e.g. `allMotionEvents.except(moveDownEvent)`. ([#218](https://github.com/bThink-BGU/BPjs/issues/218))

docs/source/BPjsTutorial/code/logging.js

@@ -12,11 +12,12 @@ bp.registerBThread( "event logging", function() {
   while (true) {
     var evt = bp.sync({waitFor:bp.all});
     bp.log.setLevel(LOG_LEVELS[idx]);
+    bp.log.error( evt.name );
     bp.log.warn( evt.name );
     bp.log.info( evt.name );
     bp.log.fine( evt.name );
     idx++;
   }
-})
+});
 
 bp.log.info("registering b-threads - done");

docs/source/BPjsTutorial/logging.rst

@@ -14,23 +14,21 @@ The "event generator" creates four events, one for each logging level. The "even
 
 .. code:: 
 
-  #  [READ] /.../logging.js
-  [JS][Info] registering b-threads - start
-    -:BPjs Added event generator
-    -:BPjs Added event logging
-  [JS][Info] registering b-threads - done
-  #  [ OK ] logging.js
   ---:BPjs Started
    --:BPjs Event [BEvent name:event 0]
-  [JS][Warn] event 0
-  [JS][Info] event 0
-  [JS][Fine] event 0
+  [BP][Error] event 0
+  [BP][Warn] event 0
+  [BP][Info] event 0
+  [BP][Fine] event 0
    --:BPjs Event [BEvent name:event 1]
-  [JS][Warn] event 1
-  [JS][Info] event 1
+  [BP][Error] event 1
+  [BP][Warn] event 1
+  [BP][Info] event 1
    --:BPjs Event [BEvent name:event 2]
-  [JS][Warn] event 2
+  [BP][Error] event 2
+  [BP][Warn] event 2
    --:BPjs Event [BEvent name:event 3]
+    -:BPjs Done event generator
   ---:BPjs No Event Selected
   ---:BPjs Ended
 

pom.xml

@@ -64,7 +64,7 @@
         <dependency>
             <groupId>org.mozilla</groupId>
             <artifactId>rhino</artifactId>
-            <version>1.8.0</version>
+            <version>1.8.1</version>
         </dependency>
         <dependency>
             <groupId>junit</groupId>
@@ -113,7 +113,7 @@
             <plugin>
                 <groupId>org.apache.maven.plugins</groupId>
                 <artifactId>maven-javadoc-plugin</artifactId>
-                <version>3.11.2</version>
+                <version>3.12.0</version>
                 <configuration>
                     <source>11</source>
                 </configuration>
@@ -186,7 +186,7 @@
                     <plugin>
                         <groupId>org.apache.maven.plugins</groupId>
                         <artifactId>maven-shade-plugin</artifactId>
-                        <version>3.3.0</version>
+                        <version>3.6.1</version>
                         <executions>
                             <execution>
                                 <phase>package</phase>
@@ -239,7 +239,7 @@
                     <plugin>
                         <groupId>org.apache.maven.plugins</groupId>
                         <artifactId>maven-javadoc-plugin</artifactId>
-                        <version>3.11.2</version>
+                        <version>3.12.0</version>
                         <configuration>
                             <source>8</source>
                         </configuration>
@@ -255,7 +255,7 @@
                     <plugin>
                         <groupId>org.apache.maven.plugins</groupId>
                         <artifactId>maven-gpg-plugin</artifactId>
-                        <version>3.2.7</version>
+                        <version>3.2.8</version>
                         <executions>
                             <execution>
                                 <id>sign-artifacts</id>

src/main/java/il/ac/bgu/cs/bp/bpjs/BPjs.java

@@ -23,17 +23,12 @@
  */
 package il.ac.bgu.cs.bp.bpjs;
 
-import il.ac.bgu.cs.bp.bpjs.bprogramio.BPJSStubInputStream;
-import il.ac.bgu.cs.bp.bpjs.bprogramio.BPJSStubOutputStream;
 import il.ac.bgu.cs.bp.bpjs.bprogramio.BuiltInStubberFactory;
-import il.ac.bgu.cs.bp.bpjs.bprogramio.SerializationStubber;
 import il.ac.bgu.cs.bp.bpjs.bprogramio.SerializationStubberFactory;
+import il.ac.bgu.cs.bp.bpjs.bprogramio.log.BpLog;
+import il.ac.bgu.cs.bp.bpjs.bprogramio.log.PrintStreamBpLog;
 import il.ac.bgu.cs.bp.bpjs.internal.BPjsRhinoContextFactory;
 import il.ac.bgu.cs.bp.bpjs.internal.ExecutorServiceMaker;
-import il.ac.bgu.cs.bp.bpjs.model.BProgram;
-import java.io.IOException;
-import java.io.InputStream;
-import java.io.OutputStream;
 import java.util.HashSet;
 import java.util.Set;
 import java.util.function.Consumer;
@@ -62,16 +57,18 @@ public class BPjs {
     private static boolean logDuringVerification = false;
 
     private static final Set<SerializationStubberFactory> STUBBER_FACTORIES = new HashSet<>();
-
+    
+    private static BpLog MAIN_LOGGER;
+    
     static {
-        ContextFactory.initGlobal( new BPjsRhinoContextFactory()) ;
-        try (Context cx = enterRhinoContext()) {
+        ContextFactory.initGlobal(new BPjsRhinoContextFactory());
+        try ( Context cx = enterRhinoContext() ) {
             ImporterTopLevel importer = new ImporterTopLevel(cx);
             BPJS_SCOPE = cx.initStandardObjects(importer, true); // create and seal
             // NOTE: global extensions to BPjs scopes would go here, if we decide to create them.
         }
         RhinoException.setStackStyle(StackStyle.V8);
-        registerStubberFactory(new BuiltInStubberFactory() );
+        registerStubberFactory(new BuiltInStubberFactory());
     }
 
     /**
@@ -193,4 +190,22 @@ public static String getVersion(){
         return mainPackage != null ? mainPackage.getImplementationVersion() : null;
     }
 
+    public static BpLog log() { 
+        if ( MAIN_LOGGER==null ) {
+            MAIN_LOGGER = new PrintStreamBpLog();
+        }
+        return MAIN_LOGGER;
+    }
+
+    /**
+     * Sets the global logger for BPjs.
+     * @param <L> The exact type of the logger, fo fluent API calls.
+     * @param aBpLogger The new logger to use
+     * @return The new logger that is being used (for fluent API etc).
+     */
+    public static <L extends BpLog> L setLogger(L aBpLogger) {
+        BPjs.MAIN_LOGGER = aBpLogger;
+        return aBpLogger;
+    }
+    
 }

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

@@ -27,12 +27,11 @@
 import il.ac.bgu.cs.bp.bpjs.analysis.violations.JsErrorViolation;
 import il.ac.bgu.cs.bp.bpjs.analysis.violations.Violation;
 import il.ac.bgu.cs.bp.bpjs.exceptions.BPjsRuntimeException;
-import il.ac.bgu.cs.bp.bpjs.exceptions.BPjsSyncOutsideBThreadException;
 
 import java.util.ArrayList;
 import java.util.List;
 
-import il.ac.bgu.cs.bp.bpjs.execution.jsproxy.BpLog;
+import il.ac.bgu.cs.bp.bpjs.bprogramio.log.BpLog;
 import il.ac.bgu.cs.bp.bpjs.model.BProgram;
 import il.ac.bgu.cs.bp.bpjs.model.BEvent;
 import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot;
@@ -171,7 +170,7 @@ public VerificationResult verify(BProgram aBp) throws Exception {
             inspections.addAll( ExecutionTraceInspections.DEFAULT_SET );
         }
 
-        ExecutorService execSvc = BPjs.getExecutorServiceMaker().makeWithName("DfsBProgramRunner-" + INSTANCE_COUNTER.incrementAndGet());
+        ExecutorService execSvc = BPjs.getExecutorServiceMaker().borrowWithName("DfsBProgramRunner-" + INSTANCE_COUNTER.incrementAndGet());
 
         BpLog.LogLevel prevLevel = currentBProgram.getLogLevel();
         if ( ! BPjs.isLogDuringVerification() ) {
@@ -196,7 +195,7 @@ public VerificationResult verify(BProgram aBp) throws Exception {
 
         } finally {            
             listener.done(this);
-            execSvc.shutdown();
+            BPjs.getExecutorServiceMaker().returnService(execSvc);
             if ( ! BPjs.isLogDuringVerification() ) {
                 currentBProgram.setLogLevel(prevLevel);
             }
@@ -340,24 +339,24 @@ public BProgram getCurrentBProgram() {
     }
 
     void printStatus(long iteration, List<DfsTraversalNode> path) {
-        System.out.println("Iteration " + iteration);
-        System.out.println("  visited: " + visited.getVisitedStateCount());
-        path.forEach(n -> System.out.println("  " + n.getLastEvent()));
+        BPjs.log().fine("Iteration " + iteration);
+        BPjs.log().fine("  visited: " + visited.getVisitedStateCount());
+        path.forEach(n -> BPjs.log().fine("  " + n.getLastEvent()));
     }
 
     private Violation inspectCurrentTrace() {
         Set<Violation> res = inspections.stream()
                                     .map(v->v.inspectTrace(trace))
                                     .filter(o->o.isPresent()).map(Optional::get)
                                     .collect(toSet());
-        if ( res.size() > 0  ) {
+        if ( !res.isEmpty()  ) {
             for ( Violation v : res ) {
                 if ( ! listener.violationFound(v, this) ) {
                     return v;
                 }
             }
             if (isDebugMode()) {
-                System.out.println("-pop! (violation)-");
+                BPjs.log().fine("-pop! (violation)-");
             }
             pop();
         }
@@ -368,7 +367,7 @@ private void push(DfsTraversalNode n) {
         visited.store(n.getSystemState());
         currentPath.add(n);
         if (isDebugMode()) {
-            System.out.println("-visiting: " + n);
+            BPjs.log().fine("-visiting: " + n);
         }
         if ( trace.getStateCount() == 0 ) {
             trace.push( n.getSystemState() );
@@ -381,7 +380,7 @@ private DfsTraversalNode pop() {
         DfsTraversalNode popped = currentPath.remove(currentPath.size() - 1);
         trace.pop();
         if (isDebugMode()) {
-            System.out.println("-pop!-");
+            BPjs.log().fine("-pop!-");
         }
         return popped;
     }

src/main/java/il/ac/bgu/cs/bp/bpjs/bprogramio/BPJSStubOutputStream.java

@@ -42,7 +42,7 @@
  */
 public class BPJSStubOutputStream extends ScriptableOutputStream {
 
-    private Map<Class, SerializationStubber> stubbers = new HashMap<>();
+    private final Map<Class, SerializationStubber> stubbers = new HashMap<>();
 
     /**
      * Constructor
@@ -55,7 +55,7 @@ public BPJSStubOutputStream(OutputStream out, Set<SerializationStubber> someStub
         for ( var stb : someStubbers ) {
             for ( var clz : stb.getClasses() ) {
                 if ( stubbers.containsKey(clz) ) {
-                    System.err.println("Warning: stubber " + stb.getId() + " overrides stubber for class " + clz.getCanonicalName() + ", previously set by " + stubbers.get(clz).getId() );
+                    BPjs.log().warn("Stubber " + stb.getId() + " overrides stubber for class " + clz.getCanonicalName() + ", previously set by " + stubbers.get(clz).getId() );
                 }
                 stubbers.put(clz, stb);
             }