Rodin POs and ProB

What is the relationship between Rodin proof obligations (POs) and ProB. In short, ProB can be made to check individual proof obligations. During animation and model checking, ProB will compute its own verification conditions for invariants, theorems, etc. However, if the PROOF_INFO preference is set to true (which it is by default) it will make use of the information about which POs are discharged to simplify the invariant checking for Event-B models.

ProB Prover Disprover

ProB can be applied to individual POs by clicking the ProB button in the Proof Control view of Rodin.

See the tutorial on the ProB Prover/Disprover for more details.

One can also export the POs of a particular Event-B machine for use with the command-line version of ProB.

This will generate a Prolog file (with .pl ending) which can be read by probcli. It will then check the individual proof obligations. Here is an example run:

probcli GearDoor1_mch.pl
...
Disprover Run Summary: [true-9]
Project LandingGearNew
Machine GearDoor1 (exported Sun Feb 08 10:38:51 CET 2015)
Number of  POs: 9 ([INITIALISATION/safety_inv1/INV,env_start_retracting/safety_inv1/INV,env_retract_gear/safety_inv1/INV,env_start_extending/safety_inv1/INV,env_extend_gear/safety_inv1/INV,env_start_open_door/safety_inv1/INV,env_open_door/safety_inv1/INV,env_start_close_door/safety_inv1/INV,env_close_door/safety_inv1/INV])
Number of proven (within Rodin) POs: 9 ([INITIALISATION/safety_inv1/INV,env_start_retracting/safety_inv1/INV,env_retract_gear/safety_inv1/INV,env_start_extending/safety_inv1/INV,env_extend_gear/safety_inv1/INV,env_start_open_door/safety_inv1/INV,env_open_door/safety_inv1/INV,env_start_close_door/safety_inv1/INV,env_close_door/safety_inv1/INV])
ProB Disprover Analysis with timeout 300 ms
Number of proven     (by ProB) POs: 9 ([INITIALISATION/safety_inv1/INV,env_start_retracting/safety_inv1/INV,env_retract_gear/safety_inv1/INV,env_start_extending/safety_inv1/INV,env_extend_gear/safety_inv1/INV,env_start_open_door/safety_inv1/INV,env_open_door/safety_inv1/INV,env_start_close_door/safety_inv1/INV,env_close_door/safety_inv1/INV])
Number of disproven  (by ProB) POs: 0 ([])
Number of unproven   (by ProB) POs: 0 ([])

ProB Model Checker

During animation and model checking, ProB will compute its own verification conditions for invariants, theorems, etc. However, if the PROOF_INFO preference is set to true (which it is by default) it will make use of the information about which POs are discharged to simplify the invariant checking for Event-B models.

The information about discharged proof obligations is automatically obtained by ProB from Rodin. It is also saved in the .eventb export files.

In ProB Tcl/Tk (aka ProB Classic) you can inspect the so obtained specialized (simplified) invariants for each operation, by choosing one of the commands in the Debug menu: