Difference between revisions of "RunMode"
From BP Wiki
| Line 8: | Line 8: | ||
* Nondeterminism specification: Ignored. All priorities are considered distinct. | * Nondeterminism specification: Ignored. All priorities are considered distinct. | ||
* Event Selection: Always the first requested event that is not blocked. | * Event Selection: Always the first requested event that is not blocked. | ||
| − | * Backtracking: none. | + | * Backtracking: none. |
| − | * Stops: When all b-threads end, or when there are no enabled events. | + | * Stops: When all b-threads end, or when there are no enabled events. |
| − | == -DrunMode=Random == | + | == -DrunMode=Random == |
* Description: One possible run out of many. | * Description: One possible run out of many. | ||
| − | * Use: Demonstration or manual exploration of different possible runs. | + | * Use: Demonstration or manual exploration of different possible runs. |
* Non-determinism specification: Allowed. | * Non-determinism specification: Allowed. | ||
| − | * Event selection: Random among all non-deterministic choices. | + | * Event selection: Random among all non-deterministic choices. |
| − | * Backtracking: none. | + | * Backtracking: none. |
| − | * Stops: When all b-threads end, or when there are no enabled events. | + | * Stops: When all b-threads end, or when there are no enabled events. |
| − | * Additional related parameters: -DrandomSeed= nnnn. | + | * Additional related parameters: -DrandomSeed= nnnn. |
| − | == -DrunMode=Iter == | + | == -DrunMode=Iter == |
* Description: An iterative run – explore all possible executions. | * Description: An iterative run – explore all possible executions. | ||
| − | * Use: to assess traces and results of all possible runs resulting from non-deterministic choices. | + | * Use: to assess traces and results of all possible runs resulting from non-deterministic choices. |
* Non-determinism specification: Allowed. | * Non-determinism specification: Allowed. | ||
| − | * Event selection: Systematically makes all possible combinations of event selections - in different runs. | + | * Event selection: Systematically makes all possible combinations of event selections - in different runs. |
* Backtracking: When a run ends , it is restarted , and a new combination of event selections is used - from the beginning - not at the next higher nondeterminstic choice. | * Backtracking: When a run ends , it is restarted , and a new combination of event selections is used - from the beginning - not at the next higher nondeterminstic choice. | ||
* Stops: When the last run of all possible runs ends (all possible combinations of event selections exhausted). | * Stops: When the last run of all possible runs ends (all possible combinations of event selections exhausted). | ||
| − | == -DrunMode=MCSafety == | + | == -DrunMode=MCSafety == |
| − | * Description: A model-checking run. Explore all possible executions paths – looking to validate safety properties. | + | * Description: A model-checking run. Explore all possible executions paths – looking to validate safety properties. |
| − | * Use: Model checking: explore safety properties (including deadlocks | + | * Use: Model checking: explore safety properties (including deadlocks), discover desired paths, etc. |
* Nondeterminism specification: Allowed (actually required by definition). | * Nondeterminism specification: Allowed (actually required by definition). | ||
* Event selection: Systematically makes all possible combinations of event selections | * Event selection: Systematically makes all possible combinations of event selections | ||
| − | Backtracking: systematic as part of exploring the state-graph - as described in [[Nondeterminism | section on nondetermism]] | + | * Backtracking: systematic as part of exploring the state-graph - as described in [[Nondeterminism | section on nondetermism]]. |
| − | Stops: When counterexample is found, or when verification of all transitions / states is complete. | + | * Stops: When counterexample is found, or when verification of all transitions / states is complete. |
| − | Additional related parameters: -Dsearch=BFS/DFS, -Drecursive=true/false | + | * Additional related parameters: -Dsearch=BFS/DFS, -Drecursive=true/false |
| − | -DrunMode=MCLiveness | + | |
| − | Description: A model-checking run– explore all execution paths looking to validate liveness properties subject to fairness assumptions. | + | == -DrunMode=MCLiveness == |
| − | Use: Model checking | + | * Description: A model-checking run– explore all execution paths looking to validate liveness properties subject to fairness assumptions. |
| − | Non-determinism specification: Allowed (actually required by definition) | + | * Use: Model checking for liveness properties - (with fairness assumptions),. |
| − | Event selection: Systematically makes all possible combinations of event selections | + | * Non-determinism specification: Allowed (actually required by definition). |
| − | Backtracking | + | * Event selection: Systematically makes all possible combinations of event selections. |
| + | * Backtracking: systematic as part of exploring the state-graph - as described in [[Nondeterminism | section on nondetermism]]. | ||
Stops: When counterexample is found, or when verification of all transitions / states is complete. | Stops: When counterexample is found, or when verification of all transitions / states is complete. | ||
| − | Additional related parameters: Conditional, strong and weak fairness assumptions provided as sets of | + | * Additional related parameters: Conditional, strong and weak fairness assumptions provided as sets of events |
| − | -DrunMode=MCDet | + | |
| − | Description: A deterministic run, with model-checking instrumentation. No non-determinism. Always pick 1st event | + | == -DrunMode=MCDet == |
| − | -DrunMode=Learning/Training (In development) | + | Description: A deterministic run, with model-checking instrumentation. No non-determinism. Always pick 1st event that is requested and not blocked. See [[MCInstrumentation | Application Assistance and Instrumentation for BPmc]] |
| + | |||
| + | == -DrunMode=Learning/Training == | ||
| + | (In development) | ||
Revision as of 14:19, 4 August 2013
Contents
Specifying Run Modes
BPmc is activated by specifying the runmode paramater in the run configuration, under VM parameters, as follows:
-DrunMode=Det
- Description: “Normal” / standard / deterministic run.
- Use: when you want the program to “do something”.
- Nondeterminism specification: Ignored. All priorities are considered distinct.
- Event Selection: Always the first requested event that is not blocked.
- Backtracking: none.
- Stops: When all b-threads end, or when there are no enabled events.
-DrunMode=Random
- Description: One possible run out of many.
- Use: Demonstration or manual exploration of different possible runs.
- Non-determinism specification: Allowed.
- Event selection: Random among all non-deterministic choices.
- Backtracking: none.
- Stops: When all b-threads end, or when there are no enabled events.
- Additional related parameters: -DrandomSeed= nnnn.
-DrunMode=Iter
- Description: An iterative run – explore all possible executions.
- Use: to assess traces and results of all possible runs resulting from non-deterministic choices.
- Non-determinism specification: Allowed.
- Event selection: Systematically makes all possible combinations of event selections - in different runs.
- Backtracking: When a run ends , it is restarted , and a new combination of event selections is used - from the beginning - not at the next higher nondeterminstic choice.
- Stops: When the last run of all possible runs ends (all possible combinations of event selections exhausted).
-DrunMode=MCSafety
- Description: A model-checking run. Explore all possible executions paths – looking to validate safety properties.
- Use: Model checking: explore safety properties (including deadlocks), discover desired paths, etc.
- Nondeterminism specification: Allowed (actually required by definition).
- Event selection: Systematically makes all possible combinations of event selections
- Backtracking: systematic as part of exploring the state-graph - as described in section on nondetermism.
- Stops: When counterexample is found, or when verification of all transitions / states is complete.
- Additional related parameters: -Dsearch=BFS/DFS, -Drecursive=true/false
-DrunMode=MCLiveness
- Description: A model-checking run– explore all execution paths looking to validate liveness properties subject to fairness assumptions.
- Use: Model checking for liveness properties - (with fairness assumptions),.
- Non-determinism specification: Allowed (actually required by definition).
- Event selection: Systematically makes all possible combinations of event selections.
- Backtracking: systematic as part of exploring the state-graph - as described in section on nondetermism.
Stops: When counterexample is found, or when verification of all transitions / states is complete.
- Additional related parameters: Conditional, strong and weak fairness assumptions provided as sets of events
-DrunMode=MCDet
Description: A deterministic run, with model-checking instrumentation. No non-determinism. Always pick 1st event that is requested and not blocked. See Application Assistance and Instrumentation for BPmc
-DrunMode=Learning/Training
(In development)
