ProB for Event-B: Difference between revisions

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 first animation steps]]
* [[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]

Revision as of 10:15, 5 March 2020

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: