(Created page with "In addition to classical B (aka B for software development), ProB also supports Event-B and the Rodin platform. ProB can be installed as a plugin for Rodin. See the tutorial p...") |
(Update Rodin handbook links) |
||
| (2 intermediate revisions by one other user not shown) | |||
| Line 1: | Line 1: | ||
In addition to classical B (aka B for software development), ProB also supports Event-B and the Rodin platform. | In addition to classical B (aka B for software development), ProB also supports Event-B and the Rodin platform. | ||
ProB can be installed as a plugin for Rodin. | ProB can be installed as a plugin for Rodin. Once installed, one can [[Tutorial Rodin Exporting|export contexts and models]] as *.eventb files and use them within ProB Tcl/Tk and the command-line version [[Using_the_Command-Line_Version_of_ProB|probcli]]. | ||
* [[Tutorial Rodin First Step|Starting ProB for Rodin and | See the tutorial pages for more information about using ProB for Event-B: | ||
* [[Tutorial Rodin First Step|Starting ProB for Rodin and First Animation Steps]] | |||
* [[Tutorial Rodin Parameters|Important Parameters of ProB for Rodin]] | * [[Tutorial Rodin Parameters|Important Parameters of ProB for Rodin]] | ||
* [[Tutorial Rodin Exporting|Exporting Rodin Models for ProB Classic]] | * [[Tutorial Rodin Exporting|Exporting Rodin Models for ProB Classic]] | ||
| Line 9: | Line 10: | ||
* [[Tutorial Disprover|Using the ProB (Dis-)Prover]] | * [[Tutorial Disprover|Using the ProB (Dis-)Prover]] | ||
* [[Tutorial LTL Counter-example View| Visualization of LTL Counter-examples in Rodin]] | * [[Tutorial LTL Counter-example View| Visualization of LTL Counter-examples in Rodin]] | ||
* [[Rodin POs and ProB| Rodin Proof Obligations and Relation to ProB]] | |||
The [ | The [https://www3.hhu.de/stups/handbook/rodin/ Rodin handbook] also contains material about ProB: | ||
* [ | * [https://www3.hhu.de/stups/handbook/rodin/current/html/tut_building_the_model.html#tut:prob Finding Invariant Violations with ProB] | ||
* [ | * [https://www3.hhu.de/stups/handbook/rodin/current/html/tut_populate_context.html Finding Solutions to Axioms] | ||
In addition to classical B (aka B for software development), ProB also supports Event-B and the Rodin platform. ProB can be installed as a plugin for Rodin. Once installed, one can export contexts and models as *.eventb files and use them within ProB Tcl/Tk and the command-line version probcli.
See the tutorial pages for more information about using ProB for Event-B:
The Rodin handbook also contains material about ProB: