View source for 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: 

<pre>
   probcli FILE -init -latex Raw.tex Final.tex
</pre>

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 <tt>-p PREF VAL</tt> or run model checking <tt>--model-check</tt>.
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:
* <tt>\probexpr{EXRP}</tt> command takes a B expression <tt>EXPR</tt>as argument and evaluates it. By default it shows the B expression and the value of the expression. Example: <tt>\probexpr{{1}\/{2**10}}</tt> will be replaced by <tt>{1,1024}</tt>
** <tt>ascii</tt> to print the result as ASCII rather than using Latex math symbols
** <tt>time</tt> to display the time taken for the command
** <tt>string</tt> the result value is a string, and do not print the quotes around the string
** <tt>value</tt> to just print the value, not the expression

* <tt>\probrepl{CMD}</tt> command takes a probcli REPL command <tt>CMD</tt> 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: <tt>\probrepl{let DOM = 1..3}</tt>. A variation of the latter is the new command <tt>\problet{DOM}{1..3}</tt> which shows the let construct itself within the generated Latex. Optional arguments for <tt>\probrepl</tt> are :
**<tt>solution</tt> to display the solution bindings (for existential variables) found by ProB
**<tt>store</tt> to store the solution bindings as local variables (similar to let)
** <tt>ascii</tt> to print the result as ASCII rather than using Latex math symbols
** <tt>time</tt> to display the time taken for the command
** <tt>print</tt> to print the expression/predicate being evaluated (automatically set by <tt>\problet</tt>
** <tt>silent</tt> to not print the result of the evaluation

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

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

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

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

* <tt>\probfor{ID}{Set}{Body}</tt> command takes an identifier <tt>ID</tt>, a set expression <tt>Set</tt> and a Latex text <tt>Body</tt>, 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_presentation.pdf slides as PDF]]