No edit summary |
(Update Rodin handbook links) |
||
| (One intermediate revision by one other user not shown) | |||
| Line 4: | Line 4: | ||
See the tutorial pages for more information about using ProB for Event-B: | See the tutorial pages for more information about using ProB for Event-B: | ||
* [[Tutorial Rodin First Step|Starting ProB for Rodin and | * [[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 10: | 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: