Difference between revisions of "Disprover"
|Line 53:||Line 53:|
Revision as of 10:49, 26 March 2010
The ProB Disprover plugin for RODIN utilizes the ProB animator and model checker to automatically find counterexamples for a given problematic proof obligation.
The Disprover is described in Debugging Event-B Models using the ProB Disprover Plug-in, Ligot, Bendisposto, Leuschel.
The ProB Disprover is available through the ProB Update Site. To Install it:
- Go to the Update manager (Help -> Software Updates...)
- Open the ProB Update Site (http://www.stups.uni-duesseldorf.de/update)
- Select all items under "ProB Disprover"
How to use it, how it works
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 an Event-B context from the Hypotheses and the Goal (see below). The ProB model checker then tries to set up the constants. If that is possible, this state is a counter example that will be presented back to the user in the proof tree.
Unfortunately, if no counter example is found, there may still be a solution, so we cannot consider the proof to be discharged. Thus, the Disprover will merely mark the proof as "Reviewed".
There are a number of different modes for the Disprover, all with advantages and disadvantages.
There is an entry for the Disprover in the preferences. These are the same preferences that are presented to the user when running in the configuration mode. These preferences are NOT used for the other modes. When using another use, the ProB-Preferences are used.
The newly constructed context and machine
The generated machine is completely empty (besides an empty INITIALISATION event). It is only generated, because ProB requires it.
The context contains:
- The negated Goals as an Axiom
- The Hypotheses, as Axioms
- The Variables, as Constants
- The Sets
- The Constants
In some modes, those Contexts that are referred from the Sequent are referred through SEES clauses.