Generating Documents with ProB and Latex - ProB Documentation

Generating Documents with ProB and Latex

Revision as of 12:48, 26 July 2016 by Michael Leuschel (talk | contribs) (Created page with "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....")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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 (see below).