- BPjs is open sourced under the MIT license. If you use it in a system, please provide a link to this page somewhere in the documentation/system about section.
- For Maven projects: Add BPjs as dependency. Note that the version number changes.
<dependencies> ... <dependency> <groupId>com.github.bthink-bgu</groupId> <artifactId>BPjs</artifactId> <version>0.9.3</version> </dependency> ... </dependencies>
- Clone, fork, or download the starting project.
- Download the
.jarfiles directly from Maven Central.
- The project's Google group
Change log for the BPjs library.
BProgramRunnernow has a
✨Documentation now covering verification (well, the basics). ✨A b-progrm's logging level can be set from Java (#50) 🚮Removed old exception code. More tests. 🚮
bsync, deprecated long ago, was removed.
PrioritizedBSyncEventSelectionStrategyselected wrong event.
BPJsCliRunnercan now directly executed from Maven, using
mvn exec:java. Pass arguments using
-Dexec.args="args go here".
BPJsCliRunnercan verify a program. Pass
--verifyas a commandline argument. Use
--full-state-storageto force the verification to use the full state data when determining whether a state was visited (requires more memory).
🐛B-Program setup sequence is consistent for all b-threads, including those in appended code.
✨Decorating event selection strategies just go easier with the introduction of
✨Added a pausing event selection strategy, to allow pausing and rate-limiting the execution of a BProgram. 🐛
✨Added a "what do you want to do" section to the docs, to help newcomers.
✨Many more tests and benchmarks.
🐛Verifiers can be re-used. ✨Support for modern JS features, such as let expressions and generators. ✨
bp.syncprints a warning when a b-thread blocks an event it requests #10.
🚮Removed extra logging. ⬆️More tests. ⬆️Fixed TicTacToe example: now split into two executing classes (interactive GUI and verification). Same core TTT code is used in both, which proves the point that BPjs can be used for smooth transition from verified model to a full application. 🎉 ✨Added a file with useful tips. ✨MOAR UNIT TESTSTSSSTTTSTSS!!!!!!!
bsyncis deprecated, in favor of
bp.sync. The latter can be called from any function, not just the immediate b-thread function.
BProgramRunnernow implements Java's
DfsBProgramVerifierinstances can now be re-used.
⬆️Improved hashing algorithm on
✨Transient caching of thread state in
BThreadSyncSnapshots. This improves verification performance, with low memory cost.
🐛Removed visited state stores that took incoming state into consideration. 🔄More mazes in the Mazes example.
🐛Fixed a crash where program with failed assertions were intermittently crashing.
🐛Verifier now correctly identifies deadlock as a state where there are requested events, but they are all blocked (formerly it just looked for the existence of b-threads).
🐛 ✨Refactored analysis code, removing the invalid (easy to understand, but invalid)
PathRequirementbased analysis, and using only b-thread now. This design is much cleaner, as it uses less concepts. Also moves us towards "everything is a b-thread" world.
✨Added tests to demonstrate the various states a verification can end in. 🐛Verifiers and runners terminate their threadpools when they are done using them.
✨During forward execution, b-threads can halt execution using
⬆️Refactored the engine tasks to support raising assertions. Reduced some code duplication in the way. ⬆️Thread pools executing b-threads are now allocated per-executor/verifier (as opposed to using a single static pool).
🔄Change ✨New feature 🚮Deprecation ⬆️Upgrade 🐛Bug fix