ProB for Event-B: Difference between revisions

No edit summary
(Update Rodin handbook links)
 
Line 12: Line 12:
* [[Rodin POs and ProB| Rodin Proof Obligations and Relation to ProB]]
* [[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 [https://www3.hhu.de/stups/handbook/rodin/ 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]
* [https://www3.hhu.de/stups/handbook/rodin/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]
* [https://www3.hhu.de/stups/handbook/rodin/current/html/tut_populate_context.html Finding Solutions to Axioms]

Latest revision as of 14:51, 4 February 2021

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: