Line 49: | Line 49: | ||

You can also inspect which of the non-selected hypotheses are false for this counter example. | You can also inspect which of the non-selected hypotheses are false for this counter example. | ||

These hypotheses are good candidates for inclusion in the selected hypotheses. | These hypotheses are good candidates for inclusion in the selected hypotheses. | ||

=== Example === | |||

Camille version of context: | |||

<pre> | |||

context ProBDisproverTest | |||

constants f n | |||

axioms | |||

@axm0 n=10 | |||

@axm1 f∈1‥n → BOOL | |||

@axm2 f(1) ≠ f(n) | |||

theorem @thm1 ran(f)=BOOL | |||

end | |||

</pre> | |||

If we just select axm0 and axm1 in the hypothesis this will be the generated B machine. | |||

As you can see the selected hypotheses are put into the PROPERTIES and the proof | |||

goal into the ASSERTIONS. | |||

The Disprover also generates the OPERATION CheckRemainingHypotheses which checks the remaining unselected hypotheses. | |||

<pre> | |||

MACHINE ProofObligation_SelectedHyps | |||

/* Exported: 4/3/2022 10:16 */ | |||

/* Origin: context : package(event_b_project) */ | |||

CONSTANTS | |||

f, n | |||

PROPERTIES /* Selected Hypotheses: */ | |||

f : POW(INTEGER * BOOL) | |||

& | |||

n : INTEGER | |||

& | |||

n = 10 | |||

& | |||

f : 1 .. 10 --> BOOL | |||

ASSERTIONS /* Proof Goal: */ | |||

ran(f) = BOOL | |||

OPERATIONS | |||

CheckRemainingHypotheses = SELECT | |||

not( | |||

f(1) = f(n) | |||

) | |||

& | |||

f : INTEGER +-> BOOL | |||

& | |||

f : 1 .. n --> BOOL | |||

& | |||

n : dom(f) | |||

& | |||

1 : dom(f) | |||

& | |||

f(1) /= f(n) | |||

THEN skip | |||

END /* CheckRemainingHypotheses */ | |||

DEFINITIONS | |||

SET_PREF_DISPROVER_MODE == TRUE; | |||

SET_PREF_TRY_FIND_ABORT == FALSE | |||

END | |||

</pre> |

We believe the Disprover to be useful to find counter examples and avoid spending time to try and prove an unprovable proof obligation (PO). The disprover plugin can also be used as a prover, in case its search for counter examples is exhaustive. This, however, means that if your PO involves deferred sets (carrier sets which are not fixed) the disprover will never be able to prove it (as ProB only checks one particular cardinality of the deferred set). Please keep in mind, that you might run into some rough edges (please inform us about any issues).

The ProB Disprover plugin for RODIN utilizes the ProB animator and model checker to automatically find counterexamples or proofs for a given proof obligation.

An early version of the ProB Disprover is described in Debugging Event-B Models using the ProB Disprover Plug-in, Ligot, Bendisposto, Leuschel.

Recently, the Disprover has been extended to detect cases in which the search for a counter-example was complete, yet there was no result. In this cases, the absence of a counter-example will be reported as a proof. See the paper describing the disprover as a prover for more details.

The ProB Disprover is currently only available through the ProB Nightly Build Update Site (http://nightly.cobra.cs.uni-duesseldorf.de/rodin/updatesite/).

: The proof obligation editor in Rodin presents the user with a number of Hypotheses and one Goal, to be proved. If the Disprover is installed, it is available in the tool bar alongside the other provers:

Upon selecting the Disprover, it builds a formula from the Hypotheses and the negated Goal. The ProB model checker then tries to find a model for that formula. If that is possible, this model is a counter example that will be presented back to the user in the proof tree. The disprover also checks if there cannot be a model for the formula. If this is the case it acts like a decision procedure, i.e., absence of a model is a proof for the goal. This is shown in the proof tree as follows:

Unfortunately, sometimes neither a counter example nor a proof can be found.

The disprover has a variety of preferences, shown below:

If you wish you can increase the time out in milliseconds using the first preference. The last preference allows you to export the PO to a classical B machine at a standard location (/tmp/ProB_Rodin_PO_SelectedHyps.mch). This file can be loaded with ProB Tcl/Tk or ProB2-UI. To find counter examples you should run a constraint-based assertion check. If successful, you can inspect the counter example in the state view. You can also inspect which of the non-selected hypotheses are false for this counter example. These hypotheses are good candidates for inclusion in the selected hypotheses.

Camille version of context:

context ProBDisproverTest constants f n axioms @axm0 n=10 @axm1 f∈1‥n → BOOL @axm2 f(1) ≠ f(n) theorem @thm1 ran(f)=BOOL end

If we just select axm0 and axm1 in the hypothesis this will be the generated B machine. As you can see the selected hypotheses are put into the PROPERTIES and the proof goal into the ASSERTIONS. The Disprover also generates the OPERATION CheckRemainingHypotheses which checks the remaining unselected hypotheses.

MACHINE ProofObligation_SelectedHyps /* Exported: 4/3/2022 10:16 */ /* Origin: context : package(event_b_project) */ CONSTANTS f, n PROPERTIES /* Selected Hypotheses: */ f : POW(INTEGER * BOOL) & n : INTEGER & n = 10 & f : 1 .. 10 --> BOOL ASSERTIONS /* Proof Goal: */ ran(f) = BOOL OPERATIONS CheckRemainingHypotheses = SELECT not( f(1) = f(n) ) & f : INTEGER +-> BOOL & f : 1 .. n --> BOOL & n : dom(f) & 1 : dom(f) & f(1) /= f(n) THEN skip END /* CheckRemainingHypotheses */ DEFINITIONS SET_PREF_DISPROVER_MODE == TRUE; SET_PREF_TRY_FIND_ABORT == FALSE END