Generating Documents with ProB and Latex

ProB can (as of version 1.6.1) be used to process Latex files, i.e., the command-line tool probcli scans a given Latex file and replaces certain commands by processed results.

Usage

A typical usage would be as follows:

   probcli FILE -init -latex Raw.tex Final.tex

Note: the FILE and -init commands are optional; they are required in case you want to process the commands in the context of a certain model. Currently the probcli Latex commands mainly support B and Event-B models, TLA+ and Z models can also be processed but all commands below expect B syntax. You can add more commands if you wish, e.g., set preferences using -p PREF VAL or run model checking --model-check. The Latex processing will take place after most other commands, such as model checking.

You will probably want to put the probcli call into a Makefile, in particular when you want to generate dot graphics using ProB.

The distribution folder of ProB contains an example with a Makefile, producing the following file, which at the same time documents the core features:

File:Prob latex doc.pdf

Commands

The commands are described in the PDF document above. Here is a short summary of some of the commands:

• \probexpr{EXRP} command takes a B expression EXPRas argument and evaluates it. By default it shows the B expression and the value of the expression. Example: \probexpr{{1}\/{2**10}} will be replaced by {1,1024}
  • ascii to print the result as ASCII rather than using Latex math symbols
  • time to display the time taken for the command
  • string the result value is a string, and do not print the quotes around the string
  • value to just print the value, not the expression

• \probrepl{CMD} command takes a probcli REPL command CMD as argument and executes it. By default it shows only the output of the execution, e.g., in case it is a predicate TRUE or FALSE. Example: \probrepl{let DOM = 1..3}. A variation of the latter is the new command \problet{DOM}{1..3} which shows the let construct itself within the generated Latex. Optional arguments for \probrepl are :
  • solution to display the solution bindings (for existential variables) found by ProB
  • store to store the solution bindings as local variables (similar to let)
  • ascii to print the result as ASCII rather than using Latex math symbols
  • time to display the time taken for the command
  • print to print the expression/predicate being evaluated (automatically set by \problet
  • silent to not print the result of the evaluation

• \probtable{EXRP} command takes a B expression EXPRas argument, evaluates it and shows it as a Latex table. Optional arguments are no-tabular, no-hline, no-headings, no-row-numbers, max-table-size=NR.

• \probdot{DOT}{File1} command takes a B expression EXPRas argument, evaluates it as a graph and writes a dot file File1. You can provide a second File as argument, in which case dot is called to generate a PDF document. You can also set sfdp as third argument, in which case the sfdp tool will be used instead of dot.

• \probprint{EXRP} command takes a B expression or predicate EXPRas argument and pretty prints it. Optional arguments are:
  • pred only try to parse first argument as predicate
  • expr only try to parse first argument as expression
  • ascii to print the result as ASCII rather than using Latex math symbols

• \probif{EXPR}{Then}{Else} command takes an expression or predicate EXPR and two Latex texts. If the expression evaluates to TRUE the first branch Then is processed, otherwise the other one Else is processed.

• \probfor{ID}{Set}{Body} command takes an identifier ID, a set expression Set and a Latex text Body, and processes the Latex text for every element of the set expression, setting the identifier to a value of the set.

Some Examples

• Presentation held in Grenoble in September 2016 about "Constraint Programming Puzzles in B" File:Puzzle latex presentation.pdf
• SBMF'2016 keynote article "Formal Model-Based Constraint Solving and Document Generation" File:Sbmf 2016 latex.pdf