Difference between revisions of "MCInstrumentation"
From BP Wiki
(New page: = 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 nextVerification...) |
|||
| Line 1: | Line 1: | ||
= Application Instrumentation and Assistance in BPmc | = Application Instrumentation and Assistance in BPmc | ||
| − | The following API calls can be used inside Java b-thread to control the model checking process. | + | 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. | + | Throughout, the term nextVerificationState refers to the applictation's (composite) state at next synchronization point, when all b-threads are synchronized. |
| − | == markNextVerificationStateAsBad() == | + | == markNextVerificationStateAsBad() == |
| − | * Indicates safety property violation. MC stops and prints a counterexample. | + | * Indicates safety property violation. MC stops and prints a counterexample. |
| − | == markNextVerificationStateAsHot() == | + | == 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. | + | * 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. | |
| − | pruneAtNextVerificationState() | + | |
| − | labelNextVerificationState(…): | + | == pruneAtNextVerificationState() |
| − | When BPmc reaches a state that was already fully checked – it backtracks. | + | * forces backtracking after all b-threads reach the next state and after its badness is determined. |
| − | If | + | |
| − | + | == 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. | ||
Revision as of 14:32, 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.
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.
