The Event-B Explorer (Rodin User Manual)

From Event-B

TODO: Update this page to talk about the unified Event-B Explorer

The "Event-B Explorer" window shows the projects' tree structures. It has projects as main entries and for each one its contexts and machines.In expanding a machine(respectively a context), you can explore its elements. When they exist, proof obligations are displayed at tree structure's leafs.

To browse through a proof, you can use the Proof Skeleton View.

As can be seen in the screen shot above, machine "celebrity_1" of project "celebrity" is expanded. We find seven proof obligations. Each of them has got a compound name as indicated in the tables below. A green logo situated on the left of the proof obligation name states that it has been proved (an A means it has been proved automatically). If you switch in proving perspective and click on the proof obligation name in the Event-B Explorer, you are transferred into a window where you can handle your proof. We are going to describe it more precisely in subsequent sections.

Next is a table describing the names of context proof obligations:

Well-definedness of an Axiom	m / WD	m is the axiom name
Well-definedness of a Derived Axiom	m / WD	m is the axiom name
Derived Axiom	m / THM	m is the axiom name

Next is a table showing the name of machine proof obligations:

Well-definedness of an Invariant	v / WD	v is the invariant name
Well-definedness of a Derived Invariant	m / WD	m is the invariant name
Well-definedness of an event Guard	t / d / WD	t is the event name d is the action name
Well-definedness of an event Action	t / d / WD	t is the event name d is the action name
Feasibility of a non-det. event Action	t / d / FIS	t is the event name d is the action name
Derived Invariant	m / THM	m is the invariant name
Invariant Establishment	INIT. / v / INV	v is the invariant name
Invariant Preservation	t / v / INV	t is the event name v is the invariant name

Next are the proof obligations concerned with machine refinements:

Guard Strengthening	t / d / GRD	t is the concrete event name d is the abstract guard name
Guard Strengthening (merge)	t / MRG	t is the concrete event name
Action Simulation	t / d / SIM	t is the concrete event name d is the abstract action name
Equality of a preserved Variable	t / v / EQL	t is the concrete event name v is the preserved variable

Next are the proof obligations concerned with the new events variant:

Well definedness of Variant	VWD
Finiteness for a set Variant	FIN
Natural number for a numeric Variant	t / NAT	t is the new event name
Decreasing of Variant	t / VAR	t is the new event name

Finally, here are the proof obligations concerned with witnesses:

Well definedness of Witness	t / p / WWD	t is the concrete event name p is parameter name or a primed variable name
Feasibility of non-det. Witness	t / p / WFIS	t is the concrete event name p is parameter name or a primed variable name

Remark: At the moment, the deadlock freeness proof obligation generation is missing. If you need it, you can generate it yourself as a derived invariant saying the the disjunction of the abstract guards imply the disjunction of the concrete guards.

Filtering

The text field above the explorer tree can be used to filter displayed POs. Only POs with a name that contains the input text will appear in the view. We will start an example from the following:

If we type 'inv' in the filter area, we'll obtain the following:

This is exactly the same, nothing was filtered out because all PO names contain 'inv' as substring. Now, if we add '2', we will only have POs related to invariant 'inv2', as follows:

Now, let's see what we obtain if we type in 'THM':

Only theorems are displayed, the entry 'INITIALISATION/inv1/inv' has been filtered out because it contains no 'THM' substring.

Note: filtering is case sensitive, thus 'thm' is different from 'THM'.

Beside the input text box is a green button, the same that is used in the explorer for discharged POs. Clicking this button hides discharged POs:

It's also possible to combine text filter and discharged filter:

In the above example, INITIALISATION/inv1/INV is filtered out by the text filter (does not contain 'THM') and inv3/THM is filtered out by the discharged PO filter.

Proof Obligation Commands

See Proof Obligation Commands.