|
|
| (6 intermediate revisions by one user not shown) |
| Line 1: |
Line 1: |
| − | = Application Instrumentation and Assistance in BPmc
| + | OLD PAGE - DELETE |
| − | | + | |
| − | The following API calls can be used inside Java b-thread to control the model checking process.
| + | |
| − | Throughout, the term nextVerificationState refers to the applictation's (composite) state at next synchronization point, when all b-threads are synchronized.
| + | |
| − | | + | |
| − | == markNextVerificationStateAsBad() ==
| + | |
| − | * Indicates safety property violation. MC stops and prints a counterexample.
| + | |
| − | | + | |
| − | == markNextVerificationStateAsHot() ==
| + | |
| − | * Used for liveness property checking. BPmc looks for reachable cycles that contains only hot states (and no cold states). By default, states are considered cold.
| + | |
| − | | + | |
| − | == pruneSearchNow()
| + | |
| − | | + | |
| − | - forces backtracking immediately, possibly stopping other b-threads and possibly before the badness of the next state is determined
| + | |
| − | 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.
| + | |
