MCInstrumentation - Revision history

Assaf: Replacing page with 'OLD PAGE - DELETE'

2014-02-11T14:04:42Z

Replacing page with 'OLD PAGE - DELETE'

Assaf at 03:59, 16 January 2014

2014-01-16T03:59:25Z

Assaf at 03:58, 16 January 2014

2014-01-16T03:58:47Z

Assaf at 14:39, 4 August 2013

2013-08-04T14:39:19Z

Assaf at 14:37, 4 August 2013

2013-08-04T14:37:16Z

Assaf at 14:34, 4 August 2013

2013-08-04T14:34:17Z

Assaf at 14:32, 4 August 2013

2013-08-04T14:32:20Z

Assaf: 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...

2013-08-04T14:28:57Z

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...

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 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.

@@ 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.

@@ Line 1: / Line 1: @@
 = 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 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.

← Older revision		Revision as of 03:58, 16 January 2014
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.

@@ Line 20: / Line 20: @@
 * 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-threads 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.
+* 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.

@@ 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.
 == 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.
+* 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.