RunMode
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)
