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...." |
|||
| Line 10: | Line 10: | ||
Note: the FILE and -init commands are optional; they are required in case you want to | 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. | process the commands in the context of a certain model. | ||
Currently the probcli Latex commands mainly support B and Event-B models, | 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>. | 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. | 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 | 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: | |||
[[File:prob_latex_doc.pdf]] | |||
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.
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: