Tips for Large Specifications - Revision history

Michael Leuschel: /* Speeding up the Loading Process */

2021-10-02T16:39:15Z

Speeding up the Loading Process

← Older revision		Revision as of 16:39, 2 October 2021
Line 45:		Line 45:
	probcli LargeFile.mch -release_java_parser		probcli LargeFile.mch -release_java_parser
	</pre>		</pre>


			Other useful tips are:
			* try to split your B model into separate machines. Typically the larges machine will determine the memory required for loading.
			* you may investigate to store your data not in B format, but in XML or CSV format and use ProB's external functions to load the data into B constants.

Michael Leuschel: /* Speeding up the Loading Process */

2021-10-02T16:36:35Z

Speeding up the Loading Process

← Older revision		Revision as of 16:36, 2 October 2021
Line 34:		Line 34:
	To reduce the size of the generated .prob file and to speed up loading the .prob file you can set the <tt>JVM_PARSER_POSITION_INFOS</tt> preference to <tt>FALSE</tt>		To reduce the size of the generated .prob file and to speed up loading the .prob file you can set the <tt>JVM_PARSER_POSITION_INFOS</tt> preference to <tt>FALSE</tt>
	This, however, means that ProB will no longer be able to provide source code locations for error messages.		This, however, means that ProB will no longer be able to provide source code locations for error messages.


	Note, that as of version October 2021, ProB uses a more compact representation of the position information. This in itself (without setting the <tt> JVM_PARSER_POSITION_INFOS </tt> flagto false) can amount in about 40 percent reduction in the size of the .prob files and much reduced memory and runtime for very large files.		Note, that as of version October 2021, ProB uses a more compact representation of the position information. This in itself (without setting the <tt> JVM_PARSER_POSITION_INFOS </tt> flagto false) can amount in about 40 percent reduction in the size of the .prob files and much reduced memory and runtime for very large files.

Michael Leuschel: /* Influencing the Java Parser */

2021-10-02T16:36:25Z

Influencing the Java Parser

← Older revision		Revision as of 16:36, 2 October 2021
Line 21:		Line 21:
	You can try giving the Java parser more memory by using the <tt>JVM_PARSER_HEAP_MB</tt> preference.		You can try giving the Java parser more memory by using the <tt>JVM_PARSER_HEAP_MB</tt> preference.
	<pre>		<pre>
	probcli ~~File~~.mch -p JVM_PARSER_HEAP_MB 10000		probcli LargeFile.mch -p JVM_PARSER_HEAP_MB 10000
	</pre>		</pre>

Line 27:		Line 27:

	<pre>		<pre>
	probcli ~~File~~.mch -p JVM_PARSER_ARGS "-Xss10m"		probcli LargeFile.mch -p JVM_PARSER_ARGS "-Xss10m"
	</pre>		</pre>

Michael Leuschel: /* Speeding up the Loading Process */

2021-10-02T16:36:08Z

Speeding up the Loading Process

← Older revision		Revision as of 16:36, 2 October 2021
Line 42:		Line 42:
	* after parsing, the Java parser will be restarted, freeing all memory that was required for parsing.		* after parsing, the Java parser will be restarted, freeing all memory that was required for parsing.
	* ProB then automatically switches to an alternate way of loading the .prob files, which tends to be much faster for very large .prob files.		* ProB then automatically switches to an alternate way of loading the .prob files, which tends to be much faster for very large .prob files.

			<pre>
			probcli LargeFile.mch -release_java_parser
			</pre>

Michael Leuschel at 16:35, 2 October 2021

2021-10-02T16:35:30Z

← Older revision		Revision as of 16:35, 2 October 2021
Line 8:		Line 8:
	In case the file is not up-to-date, a Java parser (included as probcliparser.jar in the lib folder) will be used to generate a fresh .prob file.		In case the file is not up-to-date, a Java parser (included as probcliparser.jar in the lib folder) will be used to generate a fresh .prob file.

	You can find out the parser version by using		You can find out the parser version by using for example this command
			<pre>
			probcli -java-version
			Result of checking Java version:
			Java is correctly installed and version 1.15.36-1562"
			is compatible with ProB requirements (>= 1.7).
			ProB B Java Parser available in version: 2.9.29-SNAPSHOT-d7ae8c2824c33fd8784bbeae4bbf66e99b423e4c.
			</pre>

			=== Influencing the Java Parser ===

			You can try giving the Java parser more memory by using the <tt>JVM_PARSER_HEAP_MB</tt> preference.
			<pre>
			probcli File.mch -p JVM_PARSER_HEAP_MB 10000
			</pre>

			It is also possible to provide directly arguments to the JVM using the <tt>JVM_PARSER_ARGS</tt> preference. For example:

			<pre>
			probcli File.mch -p JVM_PARSER_ARGS "-Xss10m"
			</pre>

			=== Speeding up the Loading Process ===

			To reduce the size of the generated .prob file and to speed up loading the .prob file you can set the <tt>JVM_PARSER_POSITION_INFOS</tt> preference to <tt>FALSE</tt>
			This, however, means that ProB will no longer be able to provide source code locations for error messages.


			Note, that as of version October 2021, ProB uses a more compact representation of the position information. This in itself (without setting the <tt> JVM_PARSER_POSITION_INFOS </tt> flagto false) can amount in about 40 percent reduction in the size of the .prob files and much reduced memory and runtime for very large files.

			Another useful option is the <tt>-release_java_parser</tt> flag.
			This has two effects:
			* after parsing, the Java parser will be restarted, freeing all memory that was required for parsing.
			* ProB then automatically switches to an alternate way of loading the .prob files, which tends to be much faster for very large .prob files.

Michael Leuschel: Created page with " If you have very large B machines, the following tips can be useful. Indeed, when you have very large B machines with hundreds of thousands or millions of lines of code, the..."

2021-10-02T16:25:58Z

Created page with " If you have very large B machines, the following tips can be useful. Indeed, when you have very large B machines with hundreds of thousands or millions of lines of code, the..."

New page

If you have very large B machines, the following tips can be useful.
Indeed, when you have very large B machines with hundreds of thousands or millions of lines of code, the parsing and loading process can become a bottleneck.

When ProB loads a B machine, it first checks if an up-to-date .prob file is available.
To be up-to-date the file must be newer than the main B file and all subsidiary files, and the
parser version used to produce the .prob file must match the current version.
In case the file is not up-to-date, a Java parser (included as probcliparser.jar in the lib folder) will be used to generate a fresh .prob file.

You can find out the parser version by using