Difference between revisions of "RunMode"
(New page: =Specifying Run Modes BPmc is activated by specifying the runmode paramater in the run configuration, under VM parameters, as follows: = -DrunMode=Det = Description: “Normal” / s...) |
|||
| Line 1: | Line 1: | ||
| − | =Specifying Run Modes | + | =Specifying Run Modes = |
| − | BPmc is activated by specifying the runmode paramater in the run configuration, under VM parameters, as follows: | + | BPmc is activated by specifying the runmode paramater in the run configuration, under VM parameters, as follows: |
| − | = -DrunMode=Det = | + | == -DrunMode=Det == |
| − | Description: “Normal” / standard / deterministic run . | + | Description: “Normal” / standard / deterministic run . |
Use: when you want the program to “do something”. | Use: when you want the program to “do something”. | ||
Non-determinism specification: Ignored . All priorities are considered distinct. | Non-determinism 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/rerun: none | Backtracking/rerun: 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: None. � | Additional related parameters: None. � | ||
-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. | ||
| Line 25: | Line 25: | ||
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/rerun: When a run ends , it is restarted , and a new combination of event selections is used. | Backtracking/rerun: When a run ends , it is restarted , and a new combination of event selections is used. | ||
| − | 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). |
| − | Additional related parameters: None. | + | Additional related parameters: None. |
-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), liveness properties (with fairness assumptions), discover desired paths, etc. | + | Use: Model checking: explore safety properties (including deadlocks), liveness properties (with fairness assumptions), discover desired paths, etc. |
| − | Non-determinism specification: Allowed (actually required by definition) of MC. | + | Non-determinism specification: Allowed (actually required by definition) of MC. |
Event selection: Systematically makes all possible combinations of event selections | Event selection: Systematically makes all possible combinations of event selections | ||
Backtracking/rerun: extensive backtracking as part of exploring the state-graph | Backtracking/rerun: extensive backtracking as part of exploring the state-graph | ||
| − | 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 | -DrunMode=MCLiveness | ||
Description: A model-checking run– explore all execution paths looking to validate liveness properties subject to fairness assumptions. | Description: A model-checking run– explore all execution paths looking to validate liveness properties subject to fairness assumptions. | ||
| − | Use: Model checking: explore safety properties (including deadlocks), liveness properties (with fairness assumptions), discover desired paths, etc. | + | Use: Model checking: explore safety properties (including deadlocks), liveness properties (with fairness assumptions), discover desired paths, etc. |
| − | Non-determinism specification: Allowed (actually required by definition) of MC. | + | Non-determinism specification: Allowed (actually required by definition) of MC. |
Event selection: Systematically makes all possible combinations of event selections | Event selection: Systematically makes all possible combinations of event selections | ||
Backtracking/rerun: extensive backtracking as part of exploring the state-graph | Backtracking/rerun: extensive backtracking as part of exploring the state-graph | ||
| − | 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 events� | Additional related parameters: Conditional, strong and weak fairness assumptions provided as sets of events� | ||
-DrunMode=MCDet | -DrunMode=MCDet | ||
Description: A deterministic run, with model-checking instrumentation. No non-determinism. Always pick 1st event | Description: A deterministic run, with model-checking instrumentation. No non-determinism. Always pick 1st event | ||
-DrunMode=Learning/Training (In development) | -DrunMode=Learning/Training (In development) | ||
Revision as of 14:06, 4 August 2013
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”. Non-determinism specification: Ignored . All priorities are considered distinct. Event Selection: Always the first requested event that is not blocked. Backtracking/rerun: none Stops: When all b-threads end, or when there are no enabled events Additional related parameters: None. � -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/rerun: 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/rerun: When a run ends , it is restarted , and a new combination of event selections is used. Stops: When the last run of all possible runs ends (all possible combinations of event selections exhausted). Additional related parameters: None.
-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), liveness properties (with fairness assumptions), discover desired paths, etc. Non-determinism specification: Allowed (actually required by definition) of MC. Event selection: Systematically makes all possible combinations of event selections Backtracking/rerun: extensive backtracking as part of exploring the state-graph 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: explore safety properties (including deadlocks), liveness properties (with fairness assumptions), discover desired paths, etc. Non-determinism specification: Allowed (actually required by definition) of MC. Event selection: Systematically makes all possible combinations of event selections Backtracking/rerun: extensive backtracking as part of exploring the state-graph 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 -DrunMode=Learning/Training (In development)
