Now, also working in theory

This version of BPjs is informed by requirements from users of the verification functionality. It is much more aligned with theory behind BP. For example, event selection strategies accept a state of a b-program as a parameter, when they have to select and event (as opposed to a set of synchronization statements).

The verification area has been refactored towards re-use: execution traces no longer assume they were created by the DFS verifier, trace inspections (deadlock detections etc.) can accept any execution trace.

Other notable changes:

• Improved testing infrastructure for verification and analysis (e.g. mock b-program states)
• Improved hashing algorithm for BProgramSyncSnapshots
• More tests
• Code and documentation cleanups.