RunMode - Revision history

BpAdmin: /* Application-specific parameters */

2014-04-29T08:41:01Z

‎Application-specific parameters

BpAdmin: /* Run-control Parameters */

2014-04-29T08:40:00Z

‎Run-control Parameters

Assaf: /* -Drecursive=true */

2014-04-27T12:43:25Z

‎-Drecursive=true

Assaf: /* -Dsearch=BFS or -Dsearch=DFS */

2014-04-27T12:42:45Z

‎-Dsearch=BFS or -Dsearch=DFS

BpAdmin: /* BPJ Model Checking Parameters */

2014-03-19T09:46:28Z

‎BPJ Model Checking Parameters

Assaf at 13:38, 11 February 2014

2014-02-11T13:38:57Z

Assaf: /* Run-control Parameters */

2014-02-11T13:30:28Z

‎Run-control Parameters

Assaf: /* Application-specific parameters */

2014-02-11T13:27:34Z

‎Application-specific parameters

Assaf: /* Application-specific parameters */

2014-02-11T13:25:10Z

‎Application-specific parameters

Assaf: /* Application-specific parameters */

2014-02-11T13:24:45Z

‎Application-specific parameters

@@ Line 122: / Line 122: @@
     -Drecursive=true
     -Dshallow=true
@@ Line 131: / Line 132: @@
     -DlogBacktracking=false
     -ea

@@ Line 76: / Line 76: @@
 === -ea ===
 Enable assertions. This standard Java JUnit parameter causes assertions in the code to be enabled and evaluated at run time, causing AssertionErrors when not true.
 == Memory Management Parameters ==

@@ Line 60: / Line 60: @@
 === -Drecursive=true ===
-Depth first search by recursive calls instead of by a application-maintained stack (ToDo...elaborate)
+Depth first search by recursive calls instead of by a application-maintained stack
 === -DdisableStateHashing ===

@@ Line 57: / Line 57: @@
 === -Dsearch=BFS or -Dsearch=DFS ===
-breadth or depth first search.
+Breadth-first or depth-first search.
 === -Drecursive=true ===

@@ Line 1: / Line 1: @@
-= BPmc Parameters =
+= BPJ Model Checking Parameters =
 ==Specifying Run Modes ==
-BPmc is activated by specifying the runmode paramater in the run configuration, under VM parameters, as follows:
+BPJ model checking is activated by specifying the runmode paramater in the run configuration, under VM parameters, as follows:
 === -DrunMode=Det ===

@@ Line 24: / Line 24: @@
 * 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).
+* 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 [[Nondeterminism | section on nondetermism]].
@@ Line 33: / Line 33: @@
 * Description: One possible run out of many.
 * Use: Demonstration or manual exploration of different possible runs.
-* Non-determinism specification: Allowed.
+* Nondeterminism specification: Allowed.
-* Event selection: Random among all non-deterministic choices.
+* Event selection: Random among all nondeterministic choices.
 * Backtracking: none.
 * Stops: When all b-threads end, or when there are no enabled events.
@@ Line 41: / Line 41: @@
 === -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.
+* Use: to assess traces and results of all possible runs resulting from nondeterministic choices.
-* Non-determinism specification: Allowed.
+* Nondeterminism 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.
@@ Line 48: / Line 48: @@
 === -DrunMode=MCDet ===
-Description: A deterministic run, with model-checking instrumentation. No non-determinism. The emevent selection mechanism always picks  the first event that is requested and not blocked. It is the same as defining the priority delta for equal priority b-threads as zero.
+Description: A deterministic run, with model-checking instrumentation. No nondeterminism. The event selection mechanism always picks  the first event that is requested and not blocked. It is the same as defining the priority delta for equal priority b-threads as zero.
 === -DrunMode=Learning/Training ===
@@ Line 74: / Line 74: @@
 Issues a message with every visited  BProgram state
 === -ea ===
 Enable assertions. This standard Java JUnit parameter causes assertions in the code to be enabled and evaluated at run time, causing AssertionErrors when not true.
@@ Line 94: / Line 94: @@
 * The Xmx is the maximum Java memory (heap) size within the Java Virtual Memory (JVM). As the JVM gets closer to fully utilizing the initial memory, it checks the Xmx settings to find out if it can draw more memory from the system resources. If it can, it does so. For the JVM to allocate contiguous memory to itself is a very expensive operation. So as the JVM gets closer to the initial memory, the JVM will use aggressive garbage collection (to clean the memory and if possible avoid memory allocation), increasing the load on the system.
 * If JVM is in need of memory beyond the value set in Xmx, the JVM will not be able to draw more memory from system resource (even if available) and run out of memory. Hence, the -Xms and -Xmx memory parameters should be increased depending upon the demand estimation of the system. Ideally both should be the same value (set at maximum possible as per demand estimation). This ensure that the maximum memory is allocated right at the start-up eliminating the need for extra memory allocation during program execution. It is sometimes recommended to use aggressive maximum memory (heap) size of between 1/2 and 3/4 of physical memory.
 * -Xmn: the size of the heap for the young generation.
 See more details in general Java reference information.

← Older revision		Revision as of 13:30, 11 February 2014
Line 74:		Line 74:
	Issues a message with every visited BProgram state		Issues a message with every visited BProgram state

		+	=== -ea ===
		+	Enable assertions. This standard Java JUnit parameter causes assertions in the code to be enabled and evaluated at run time, causing AssertionErrors when not true.

	== Memory Management Parameters ==		== Memory Management Parameters ==

← Older revision		Revision as of 13:27, 11 February 2014
Line 125:		Line 125:
	-DestimatedStates=10000		-DestimatedStates=10000
	-DlogBacktracking=false		-DlogBacktracking=false
		+	-ea

← Older revision		Revision as of 13:25, 11 February 2014
Line 112:		Line 112:


−	Run Configuration ~~Example 1~~:	+	Run Configuration Examples:

	-DrunMode=MCSafety		-DrunMode=MCSafety

@@ Line 114: / Line 114: @@
 Run Configuration Example 1:
--DrunMode=MCSafety
+   -DrunMode=MCSafety
--Drecursive=true
+   -Drecursive=true
--Dshallow=true
+   -Dshallow=true
--DrunMode=MCSafety
+   -DrunMode=MCSafety
--Dsearch=DFS
+   -Dsearch=DFS
--Xms300M
+   -Xms300M
--Xmx1000M
+   -Xmx1000M
--DestimatedStates=10000
+   -DestimatedStates=10000
--DlogBacktracking=false
+   -DlogBacktracking=false