Difference between revisions of "MCInstrumentation"
From BP Wiki
| Line 10: | Line 10: | ||
* 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. | * 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() | + | == pruneSearchNow()== |
| − | * Forces backtracking immediately, possibly stopping other b-threads and possibly before the badness of the next state is determined. | + | * Forces backtracking immediately, possibly stopping other b-threads and possibly before the badness of the next state is determined. |
| − | == pruneAtNextVerificationState() | + | == pruneAtNextVerificationState() == |
* forces backtracking after all b-threads reach the next state and after its badness is determined. | * forces backtracking after all b-threads reach the next state and after its badness is determined. | ||
| − | == labelNextVerificationState(…) | + | == labelNextVerificationState(…) == |
* Optionally provides a label for a b-thread state, to be used in constructing the BP-state (concatenating all bt-states - creating their Cartesian product). | * Optionally provides a label for a b-thread state, to be used in constructing the BP-state (concatenating all bt-states - creating their Cartesian product). | ||
* When BPmc reaches a BP-state that was already fully checked – it backtracks. | * When BPmc reaches a BP-state that was already fully checked – it backtracks. | ||
* If a b-thread does not label any of its states – it is considered to have one state – and it does not increase the size of the Cartesian product. | * If a b-thread does not label any of its states – it is considered to have one state – and it does not increase the size of the Cartesian product. | ||
Revision as of 14:34, 4 August 2013
= Application Instrumentation and Assistance in BPmc
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.
Contents
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 - creating their Cartesian product).
- When BPmc reaches a BP-state that was already fully checked – it backtracks.
- If a b-thread does not label any of its states – it is considered to have one state – and it does not increase the size of the Cartesian product.
