- ⬆️ Improved and updated documentation, especially regarding analysis, verification, and general top-level views (life cycle, classes, packages).
- ⬆️ Improved tests package structure, so that it's less confusing.
- ⬆️ Improved state hashing
- ⬆️ More tests for the verifier
- ✨ Proper JavaScript error reporting at runtime (e.g. invoking methods of
null
). (#52) - ✨ Proper JavaScript error reporting at for verification. To this end, a new violation,
JSErrorViolation
, was added. (#79) - ⬆️ Updated error message when calling
bp.sync
from a non-b-thread context.
- 🐛 Fixed a bug in the verifier, where a non-cyclic path ending in a visited node is not inspected.
- 🐛 Hash code fixes.
- ⬆️ Interface cleanups in the DfsBProgramVerifier: some method exposed the internal DFS nodes, and now they don't do that anymore.
- ⬆️ More tests
- 🚮 Code cleanup.
- ✨ Serious makeover for the composable event suite. Users can no compose event sets using
or
,and
, andnot
(and evenxor
,nor
andnand
) and get semantically correct sets that support verification. for example, this works:
EventSet sutA = theEventSet(E_A).or(E_B).and( theEventSet(E_B).or(E_C) );
EventSet sutB = theEventSet(E_C).or(E_B).and( theEventSet(E_B).or(E_A) );
assertEquals( sutA, sutB );
- ⬆️
ComposableEventSet
refactored to haveequals
andhashCode
that can hold during verification. - ⬆️ More tests.
- ⬆️ Improved hash functions for
ContinuationProgramState
(affects b-thread sync snapshots as well).
- 🐛 Instances of the constant sets class
EventSets
now cannot be duplicated even when they are serialized. - 🐛 Fixed a bug in the verifier, where inspections were invoked twice.
- ⬆️ Improved hash functions for
SyncStatement
s andComposableEventSet
s. - ⬆️
ExecutionTrace
s can now return the last event, in addition to returning the last state. - ⬆️ More tests.
- 🚮 Removed duplicate functionality of "all events except" (had two classes that did this).
- ⬆️ More robust JavaScript error handling.
- ⬆️ Updated the Tic-Tac-Toe code.
- 🚮 Removed dependencies from
pom.xml
- ⬆️ Updated versions of dependencies in
pom.xml
.
- ⬆️ More tests
- ✨ Detection of multiple violations/general program space traversal:
DFSBProgramVerifier
can continue its traversal of b-program state space after a violation was detected. - ⬆️ Tests clean up after their executor services.
- ⬆️ More tests
- ⬆️⬆️✨ 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.
- ⬆️ Improved state hashing algorithm in the hash-based visited state storage.
- ⬆️ Updated documentation of the verification parts.
- ⬆️ More tests.
- ⬆️ Updated maven compiler plugin.
- 🐛 Fixed a corner case where b-programs with immediate failed assertions would still attempt running certain machines.
- ⬆️ 🎉 Event selection strategies now accept
BProgramSyncSnapshot
, rather than a set of sync statements and external events.
- ✨ Testing infrastructure for execution traces.
- ⬆️ More terminology cleanups in the api (e.g. "bsync" converted to "sync")
- ⬆️
VisitedStateStore
now stores states, not DFS nodes. So it's more reusable that way.
- ✨ More tests.
- ⬆️
BriefPrintDfsVerifierListener
=>PrintDfsVerifierListener
, so that it's consistent withPrintBProgramRunnerListener
. - ⬆️ Incorporated the "BPjs Tips" file to the central documentation.
- 🐛 Fixed a that cause equality tests of JS event sets to return false negatives.
- 🐛 The
bp
object no longer collected by the state comparators. - ✨
BEvent
has a bit more informativetoString()
method, that can also look abit into the JavaScript objects (not a full JSON.stringify, since we don't want to deal with arbirtarily large strings for a simple toString op. Not to mention circular references and such). - ✨
BEvent::hashCode
now hashes data the event might have. - ✨
ScriptableUtils
got some new utility methods that dig a bit intoScriptableObject
s. This makes BPjs better at handling events with JS data objects.
- ⬆️ Hot BThread Cycle now more informative (reporting event and index of return-to).
- ✨ Commandline verifier accepts optional
--max-trace-length
parameter, that limits the trace length during verification. - ⬆️ Removed the internal
scope
field fromBThreadSyncSnapshot
s. This cuts the size of the serialized form significantly. - ⬆️ better hashing algorithm.
- 🎉 Happy new year - 2018 changes moved here.
Legend:
- 🔄 Change
- ✨New feature
- 🚮 Deprecation
- ⬆️ Upgrade
- 🐛 Bug fix