Tips for Large Specifications: Difference between revisions

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 for example this command

 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.

Influencing the Java Parser

You can try giving the Java parser more memory by using the JVM_PARSER_HEAP_MB preference.

 probcli LargeFile.mch -p JVM_PARSER_HEAP_MB 10000

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

 probcli LargeFile.mch -p JVM_PARSER_ARGS "-Xss10m"

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 JVM_PARSER_POSITION_INFOS preference to FALSE 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 JVM_PARSER_POSITION_INFOS 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 -release_java_parser 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.

probcli LargeFile.mch -release_java_parser

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.