|
|
| Line 1: |
Line 1: |
| − | = Application Instrumentation and Assistance in BPmc =
| + | OLD PAGE - DELETE |
| − | | + | |
| − | The following API calls can be used inside any 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. For example, a logger b-thread that does not request events and does not affect the outcome of the run, does not have to label its states.
| + | |
| − | * A b-thread that incorrectly gives the same label to different states, may cause incorrect model-checking results.
| + | |
| − | * The states of a "linear" b-thread can be just numbered as 1/2/3 etc.. The states of a more complex b-thread can be labeled based on the values of the variables that determine the state change.
| + | |
| − | * State names are local to the b-thread and must be unique only within a b-thread. The BPmc infrastructure properly distinguishes state 1 of b-thread BT1, from state 1 of b-thread BT2.
| + | |
