BPJ Model Checking API
BPmc API: Controlling model checking from your application
B-threads can call the following API methods
- ToDo - of which object
to control the model checking.
- markNextVerificationStateAsBad(): Indicates detection by the b-thread of a violation of a safety property. BPmc stops and prints the sequence of events (the path) to this point as a counter example.
- markNextVerificationStateAsHot(): This is is used for checking of liveness properties. States that are not marked as hot are considered cold. If BPmc detects a cycle in the state graph that does not contain a cold state, it stops and prints the path to this cycle and the cycle as a counter example.
- pruneSearchNow(): This forces backtracking immediately, possibly stopping other b-threads and possibly before the badness of the next state is determined. This call can be used by a b-thread to accelerate the model checking by eliminating states that weren't explored, but are known to lead to results that are known or are symmetric to other states, or are otherwise not relevant in the present run.
pruneAtNextVerificationState() - forces backtracking �after all b-threads reach the next state and after its badness is determined. labelNextVerificationState(…): optionally provides a label for a b-thread state, to be used in constructing the BP-state (concatenating all bt-states). When BPmc reaches a state that was already fully checked – it backtracks. If b-thread doesn’t label its states – it is considered to have one state – and it doesn’t increase the size of the Cartesian product. While in regular runs a b-thread can terminate, in a MC run A b-thread should not terminate. Precede/replace the return with bSync(none,none,none); In a regular run this will just terminate. In MC run it will allow the b-thread to backtrack from the end.
