Disprover - Revision history

imported>Jens: /* ProB Disprover */

2016-05-02T13:34:14Z

ProB Disprover

← Older revision		Revision as of 13:34, 2 May 2016
Line 3:		Line 3:
	The ProB Disprover plugin for RODIN utilizes the ProB animator and model checker to automatically find counterexamples		The ProB Disprover plugin for RODIN utilizes the ProB animator and model checker to automatically find counterexamples
	or proofs for a given proof obligation.		or proofs for a given proof obligation.

			An early version of the ProB Disprover is described in [http://www.stups.uni-duesseldorf.de/publications_detail.php?id=219 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 [http://stups.hhu.de/w/Special:Publication/disprover_eval the paper describing the disprover as a prover] for more details.

	== Installation ==		== Installation ==

imported>Jens at 13:33, 2 May 2016

2016-05-02T13:33:12Z

← Older revision		Revision as of 13:33, 2 May 2016
Line 3:		Line 3:
	The ProB Disprover plugin for RODIN utilizes the ProB animator and model checker to automatically find counterexamples		The ProB Disprover plugin for RODIN utilizes the ProB animator and model checker to automatically find counterexamples
	or proofs for a given proof obligation.		or proofs for a given proof obligation.

	~~The Disprover is described in [http://www.stups.uni-duesseldorf.de/publications_detail.php?id=219 Debugging Event-B Models using the ProB Disprover Plug-in], Ligot, Bendisposto, Leuschel.~~

	== Installation ==		== Installation ==
Line 13:		Line 11:
	== How to use it, how it works ==		== How to use it, how it works ==

	[~~[Image~~:~~disprover-all~~.~~png]]: 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.~~		[http://www.prob2.de/Tutorial_Disprover Disprover Tutorial]

	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. Unfortunately, sometimes neither a counter example nor a proof can be found.


	[[Category:User documentation]]		[[Category:User documentation]]

imported>Jens at 13:36, 9 April 2013

2013-04-09T13:36:04Z

@@ Line 2: / Line 2: @@
 The ProB Disprover plugin for RODIN utilizes the ProB animator and model checker to automatically find counterexamples
-for a given problematic proof obligation.
+or proofs for a given proof obligation.
 The Disprover is described in [http://www.stups.uni-duesseldorf.de/publications_detail.php?id=219 Debugging Event-B Models using the ProB Disprover Plug-in], Ligot, Bendisposto, Leuschel.
@@ Line 8: / Line 8: @@
 == Installation ==
-The ProB Disprover is available through the ProB Update Site.  To Install it:
+The ProB Disprover is currently only available through the ProB Nightly Build Update Site (http://nightly.cobra.cs.uni-duesseldorf.de/rodin/updatesite/).
 == 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.
+[[Image:disprover-all.png]]: 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.
+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. Unfortunately, sometimes neither a counter example nor a proof can be found.
 [[Category:User documentation]]

imported>Jrloria at 10:49, 26 March 2010

2010-03-26T10:49:54Z

← Older revision		Revision as of 10:49, 26 March 2010
Line 53:		Line 53:

	[[Category:User documentation]]		[[Category:User documentation]]
	~~[[Category:Developer documentation]]~~

imported>Jastram at 15:09, 10 September 2009

2009-09-10T15:09:17Z

← Older revision		Revision as of 15:09, 10 September 2009
Line 54:		Line 54:
	[[Category:User documentation]]		[[Category:User documentation]]
	[[Category:Developer documentation]]		[[Category:Developer documentation]]
	~~[[Category:Requirement Plugin]]~~

imported>Jastram at 15:08, 10 September 2009

2009-09-10T15:08:18Z

← Older revision		Revision as of 15:08, 10 September 2009
Line 26:		Line 26:
	== The Disprover-Modes ==		== The Disprover-Modes ==

	[[~~Bild~~:disprover-relevant-context.png]] '''Using relevant Hypotheses and includes all Contexts''': Rodin determines which Hypotheses it considers relevant, uses those and includes all Context Information (Sets, Constants, Axioms).		[[Image:disprover-relevant-context.png]] '''Using relevant Hypotheses and includes all Contexts''': Rodin determines which Hypotheses it considers relevant, uses those and includes all Context Information (Sets, Constants, Axioms).

	[[~~Bild~~:disprover-all.png]] '''Uses all Hypotheses''': Simply all Hypotheses are used. As this includes the Axioms from the Contexts as well, including them would be redundant.		[[Image:disprover-all.png]] '''Uses all Hypotheses''': Simply all Hypotheses are used. As this includes the Axioms from the Contexts as well, including them would be redundant.

	[[~~Bild~~:disprover-config.png]] '''Allows detailed configuration of the Disprover parameters''': A dialog allows the Disprover to be configured in great detail. Warning: If inproperly used, this may result in counter-examples that are not really counter-examples.		[[Image:disprover-config.png]] '''Allows detailed configuration of the Disprover parameters''': A dialog allows the Disprover to be configured in great detail. Warning: If inproperly used, this may result in counter-examples that are not really counter-examples.

	[[~~Bild~~:disprover-relevant.png]] '''Includes only the relevant hypotheses''': Only those hypotheses that Rodin considers relevant are included. This may result in counter-examples that are not really counter-examples, so this mode is discouraged.		[[Image:disprover-relevant.png]] '''Includes only the relevant hypotheses''': Only those hypotheses that Rodin considers relevant are included. This may result in counter-examples that are not really counter-examples, so this mode is discouraged.

	== Disprover-Preferences ==		== Disprover-Preferences ==

imported>Jastram: New page: == ProB Disprover == The ProB Disprover plugin for RODIN utilizes the ProB animator and model checker to automatically find counterexamples for a given problematic proof obligation. The ...

2009-09-10T15:06:46Z

New page: == ProB Disprover == The ProB Disprover plugin for RODIN utilizes the ProB animator and model checker to automatically find counterexamples for a given problematic proof obligation. The ...

New page

== ProB Disprover ==

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 [http://www.stups.uni-duesseldorf.de/publications_detail.php?id=219 Debugging Event-B Models using the ProB Disprover Plug-in], Ligot, Bendisposto, Leuschel.

== Installation ==

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.

== The Disprover-Modes ==

[[Bild:disprover-relevant-context.png]] '''Using relevant Hypotheses and includes all Contexts''': Rodin determines which Hypotheses it considers relevant, uses those and includes all Context Information (Sets, Constants, Axioms).

[[Bild:disprover-all.png]] '''Uses all Hypotheses''': Simply all Hypotheses are used. As this includes the Axioms from the Contexts as well, including them would be redundant.

[[Bild:disprover-config.png]] '''Allows detailed configuration of the Disprover parameters''': A dialog allows the Disprover to be configured in great detail. Warning: If inproperly used, this may result in counter-examples that are not really counter-examples.

[[Bild:disprover-relevant.png]] '''Includes only the relevant hypotheses''': Only those hypotheses that Rodin considers relevant are included. This may result in counter-examples that are not really counter-examples, so this mode is discouraged.

== Disprover-Preferences ==

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.

[[Category:User documentation]]
[[Category:Developer documentation]]
[[Category:Requirement Plugin]]