No edit summary |
No edit summary |
||
| 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 [http://handbook.event-b.org Rodin handbook] also contains material about ProB: | The [http://handbook.event-b.org Rodin handbook] also contains material about ProB: | ||
* [http://handbook.event-b.org/current/html/tut_building_the_model.html#tut:prob Finding Invariant Violations with ProB] | * [http://handbook.event-b.org/current/html/tut_building_the_model.html#tut:prob Finding Invariant Violations with ProB] | ||
* [http://handbook.event-b.org/current/html/tut_populate_context.html#a0000000094 Finding Solutions to Axioms] | * [http://handbook.event-b.org/current/html/tut_populate_context.html#a0000000094 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: