Implication inside an Existential Quantifier - Revision history

Michael Leuschel at 12:46, 3 April 2025

2025-04-03T12:46:18Z

← Older revision		Revision as of 12:46, 3 April 2025
Line 40:		Line 40:

	You may be surprised to see that @thm3_true is actually provable within Rodin.		You may be surprised to see that @thm3_true is actually provable within Rodin.
	One may expect the predicate to be equivalent to <tt>x:1..3 = y=44</tt> which is false.		One may expect the predicate to be equivalent to <tt>x:1..3 => y=44</tt> which is false.
	Rodin, however parses the formula as an existential quantifier with the implication <b>inside</b> the body.		Rodin, however parses the formula as an existential quantifier with the implication <b>inside</b> the body.
	Hence, z=0 or z=4 are solutions to the existential quantifier and the predicate is true.		Hence, z=0 or z=4 are solutions to the existential quantifier and the predicate is true.

Michael Leuschel at 11:56, 25 February 2025

2025-02-25T11:56:03Z

← Older revision		Revision as of 11:56, 25 February 2025
Line 43:		Line 43:
	Rodin, however parses the formula as an existential quantifier with the implication <b>inside</b> the body.		Rodin, however parses the formula as an existential quantifier with the implication <b>inside</b> the body.
	Hence, z=0 or z=4 are solutions to the existential quantifier and the predicate is true.		Hence, z=0 or z=4 are solutions to the existential quantifier and the predicate is true.
			(See also page 11 of <em>The Event-B Mathematical Language</em> by Métayer and Voisin.)

	When adding additional parentheses, the predicate becomes false and probably corresponds to what we expected to write:		When adding additional parentheses, the predicate becomes false and probably corresponds to what we expected to write:

Michael Leuschel at 11:35, 25 February 2025

2025-02-25T11:35:28Z

← Older revision		Revision as of 11:35, 25 February 2025
Line 51:		Line 51:
	ProB will now emit a warning for @thm3_true (but not for @thm4_false).		ProB will now emit a warning for @thm3_true (but not for @thm4_false).

	Note that this ~~pitfall~~ is ~~present~~ in one of the solutions to the ABZ 2014 landing gear case study.		Note that this new warning is triggered for invariant inv2 in one of the solutions to the ABZ 2014 landing gear case study:
	After adding the check for implications inside existential quantifiers to ProB, two tests using files from that case study solution were failing due to the new warnings. The culprit was the following invariant, which can also be found in the published article:
	<pre>		<pre>
	@inv2 ∃po·(po∈ PositionsDG∧ gear_extended_p(po)=FALSE ∧ gear_retracted_p(po)=FALSE)		@inv2 ∃po·(po∈ PositionsDG∧ gear_extended_p(po)=FALSE ∧ gear_retracted_p(po)=FALSE)
Line 59:		Line 58:
	</pre>		</pre>
	The interpretation of Rodin of this invariant does not correspond to the intended meaning of the authors as described in the article (<em>" we express an invariant to state that when a gear is partly-extended then all the doors are open."</em>).		The interpretation of Rodin of this invariant does not correspond to the intended meaning of the authors as described in the article (<em>" we express an invariant to state that when a gear is partly-extended then all the doors are open."</em>).
	~~We were also initially surprised and suspected that ProB had erroneously generated the warnings.~~		Hence, the new warning by ProB is correct and useful.
	~~But it turns out that~~ the warning is correct and useful~~, and that the~~ priority rules of Rodin can be misleading, in particular to persons used to the classical B syntax.		The priority rules of Rodin can thus be misleading, in particular to persons used to the classical B syntax.

	Note: the case study has now been corrected and all invariants are proven and no events had to be changed.		Note: the case study has now been corrected and all invariants are proven and no events had to be changed. The corrected invariant simply moves the parentheses around the existential quantifier:
			<pre>
			@inv2 ( ∃po· po∈ PositionsDG∧ gear_extended_p(po)=FALSE ∧ gear_retracted_p(po)=FALSE)
			⇒
			door_open_p=PositionsDG×{TRUE}
			</pre>

Michael Leuschel at 10:26, 25 February 2025

2025-02-25T10:26:53Z

← Older revision		Revision as of 10:26, 25 February 2025
Line 51:		Line 51:
	ProB will now emit a warning for @thm3_true (but not for @thm4_false).		ProB will now emit a warning for @thm3_true (but not for @thm4_false).

	Note that this ~~error~~ is present in one of the solutions to the ABZ 2014 landing gear case study.		Note that this pitfall is present in one of the solutions to the ABZ 2014 landing gear case study.
	After adding the check for implications inside existential quantifiers to ProB, two tests using files from that case study solution were failing due to the new warnings. The culprit was the following invariant, which can also be found in the published article:		After adding the check for implications inside existential quantifiers to ProB, two tests using files from that case study solution were failing due to the new warnings. The culprit was the following invariant, which can also be found in the published article:
	<pre>		<pre>
Line 61:		Line 61:
	We were also initially surprised and suspected that ProB had erroneously generated the warnings.		We were also initially surprised and suspected that ProB had erroneously generated the warnings.
	But it turns out that the warning is correct and useful, and that the priority rules of Rodin can be misleading, in particular to persons used to the classical B syntax.		But it turns out that the warning is correct and useful, and that the priority rules of Rodin can be misleading, in particular to persons used to the classical B syntax.

			Note: the case study has now been corrected and all invariants are proven and no events had to be changed.

Michael Leuschel at 17:43, 22 February 2025

2025-02-22T17:43:59Z

← Older revision		Revision as of 17:43, 22 February 2025
Line 10:		Line 10:
	</pre>		</pre>

	~~You may be~~ surprised ~~to learn~~ that the existential quantifier on the third line is true, even though no element of the array f is greater than 0.		Maybe you are surprised that the existential quantifier on the third line is true, even though no element of the array f is greater than 0.
	Indeed, for i=0 or i=-1 or i=4 the body of the quantifier is true as <tt>i:dom(f)</tt> is false and hence the implication is true.		Indeed, for i=0 or i=-1 or i=4 the body of the quantifier is true as <tt>i:dom(f)</tt> is false and hence the implication is true.
			Quite often, existential quantifiers with a top-level implication are vacuously true.
	~~Usually~~, one intended to write a conjunction inside the quantifier, such as the following (which is now false given <tt>f=[0,0,0]</tt>):		Hence, usually, one intended to write a conjunction inside the quantifier, such as the following formula (which is now false given <tt>f=[0,0,0]</tt>):
	<pre>		<pre>
	#i.(i:dom(f) & f(i)>0)		#i.(i:dom(f) & f(i)>0)
Line 25:		Line 25:
	</pre>		</pre>

	~~Note that in particular in~~ Rodin ~~you~~ can accidentally introduce an implication ~~due to its subtly different~~ priorities.		ProB will also issue a warning for this slightly "hidden" implication.

			In Rodin one can accidentally introduce an implication inside an existential quantifier, because the operator priorities of the implication and exists symbol can be surprising.
	Let us look at the next Event-B context (in Camille syntax):		Let us look at the next Event-B context (in Camille syntax):
	<pre>		<pre>
Line 50:		Line 52:

	Note that this error is present in one of the solutions to the ABZ 2014 landing gear case study.		Note that this error is present in one of the solutions to the ABZ 2014 landing gear case study.
	After adding the check to ProB, two tests using files from that case study solution ~~where~~ failing due to the warnings. The culprit was the following invariant, which can also be found in the published article:		After adding the check for implications inside existential quantifiers to ProB, two tests using files from that case study solution were failing due to the new warnings. The culprit was the following invariant, which can also be found in the published article:
	<pre>		<pre>
	@inv2 ∃po·(po∈ PositionsDG∧ gear_extended_p(po)=FALSE ∧ gear_retracted_p(po)=FALSE)		@inv2 ∃po·(po∈ PositionsDG∧ gear_extended_p(po)=FALSE ∧ gear_retracted_p(po)=FALSE)
Line 56:		Line 58:
	door_open_p=PositionsDG×{TRUE}		door_open_p=PositionsDG×{TRUE}
	</pre>		</pre>
	The interpretation of Rodin of this invariant does not correspond to the intended meaning		The interpretation of Rodin of this invariant does not correspond to the intended meaning of the authors as described in the article (<em>" we express an invariant to state that when a gear is partly-extended then all the doors are open."</em>).
	as described in the article (<em>" we express an invariant to state that when a gear is partly-extended then all the doors are open."</em>).		We were also initially surprised and suspected that ProB had erroneously generated the warnings.
	~~This shows~~ that the ~~new~~ warning ~~in ProB~~ is useful, and that the priority rules of Rodin can be misleading, in particular to persons used to the classical B syntax.		But it turns out that the warning is correct and useful, and that the priority rules of Rodin can be misleading, in particular to persons used to the classical B syntax.

Michael Leuschel at 07:32, 22 February 2025

2025-02-22T07:32:50Z

← Older revision		Revision as of 07:32, 22 February 2025
Line 58:		Line 58:
	The interpretation of Rodin of this invariant does not correspond to the intended meaning		The interpretation of Rodin of this invariant does not correspond to the intended meaning
	as described in the article (<em>" we express an invariant to state that when a gear is partly-extended then all the doors are open."</em>).		as described in the article (<em>" we express an invariant to state that when a gear is partly-extended then all the doors are open."</em>).
	This shows that the new warning in ProB is useful, and that the priority rules of Rodin ~~are surprising~~, in particular to persons used to the classical B syntax.		This shows that the new warning in ProB is useful, and that the priority rules of Rodin can be misleading, in particular to persons used to the classical B syntax.

Michael Leuschel at 07:32, 22 February 2025

2025-02-22T07:32:04Z

← Older revision		Revision as of 07:32, 22 February 2025
Line 3:		Line 3:
	Here we explain why.		Here we explain why.

	Take a look at		Take a look at the following formula:
	<pre>		<pre>
	f: 1..3 --> NAT &		f: 1..3 --> NAT &
Line 13:		Line 13:
	Indeed, for i=0 or i=-1 or i=4 the body of the quantifier is true as <tt>i:dom(f)</tt> is false and hence the implication is true.		Indeed, for i=0 or i=-1 or i=4 the body of the quantifier is true as <tt>i:dom(f)</tt> is false and hence the implication is true.

	Usually, one intended to write a conjunction inside the quantifier, such as the following (which is false ~~for~~ <tt>f=[0,0,0]</tt>):		Usually, one intended to write a conjunction inside the quantifier, such as the following (which is now false given <tt>f=[0,0,0]</tt>):
	<pre>		<pre>
	#i.(i:dom(f) & f(i)>0)		#i.(i:dom(f) & f(i)>0)

Michael Leuschel at 07:30, 22 February 2025

2025-02-22T07:30:40Z

← Older revision		Revision as of 07:30, 22 February 2025
Line 52:		Line 52:
	After adding the check to ProB, two tests using files from that case study solution where failing due to the warnings. The culprit was the following invariant, which can also be found in the published article:		After adding the check to ProB, two tests using files from that case study solution where failing due to the warnings. The culprit was the following invariant, which can also be found in the published article:
	<pre>		<pre>
	@inv2 ∃po·(po∈ PositionsDG∧ gear_extended_p(po)=FALSE ∧ gear_retracted_p(po)=FALSE) ~~⇒door_open_p~~=PositionsDG×{TRUE}		@inv2 ∃po·(po∈ PositionsDG∧ gear_extended_p(po)=FALSE ∧ gear_retracted_p(po)=FALSE)
			⇒
			door_open_p=PositionsDG×{TRUE}
	</pre>		</pre>
	The interpretation of Rodin of this invariant does not correspond to the intended meaning		The interpretation of Rodin of this invariant does not correspond to the intended meaning
	as described in the article (<em>" we express an invariant to state that when a gear is partly-extended then all the doors are open."</em>).		as described in the article (<em>" we express an invariant to state that when a gear is partly-extended then all the doors are open."</em>).
	This shows that the new warning in ProB is useful, and that the priority rules of Rodin are surprising, in particular to persons used to the classical B syntax.		This shows that the new warning in ProB is useful, and that the priority rules of Rodin are surprising, in particular to persons used to the classical B syntax.

Michael Leuschel at 07:30, 22 February 2025

2025-02-22T07:30:16Z

← Older revision		Revision as of 07:30, 22 February 2025
Line 45:		Line 45:
	<pre>		<pre>
	theorem @thm4_false (∃z2·(z2∈1‥3 ∧ x=z2)) ⇒ y=44		theorem @thm4_false (∃z2·(z2∈1‥3 ∧ x=z2)) ⇒ y=44
	~~end~~
	</pre>		</pre>

	ProB will now emit a warning for @thm3_true (but not for @thm4_false).		ProB will now emit a warning for @thm3_true (but not for @thm4_false).

			Note that this error is present in one of the solutions to the ABZ 2014 landing gear case study.
			After adding the check to ProB, two tests using files from that case study solution where failing due to the warnings. The culprit was the following invariant, which can also be found in the published article:
			<pre>
			@inv2 ∃po·(po∈ PositionsDG∧ gear_extended_p(po)=FALSE ∧ gear_retracted_p(po)=FALSE) ⇒door_open_p=PositionsDG×{TRUE}
			</pre>
			The interpretation of Rodin of this invariant does not correspond to the intended meaning
			as described in the article (<em>" we express an invariant to state that when a gear is partly-extended then all the doors are open."</em>).
			This shows that the new warning in ProB is useful, and that the priority rules of Rodin are surprising, in particular to persons used to the classical B syntax.

Michael Leuschel at 07:24, 22 February 2025

2025-02-22T07:24:36Z

← Older revision		Revision as of 07:24, 22 February 2025
Line 33:		Line 33:
	@axm1 x=1		@axm1 x=1
	@axm2 y=2		@axm2 y=2
	theorem @thm3_true ∃z·(z∈1‥3 ∧ x=z) ⇒ y=44 // ~~suprinsingly~~ this formula is true~~; see invariant in Mammar/Laleau landing gear model~~		theorem @thm3_true ∃z·(z∈1‥3 ∧ x=z) ⇒ y=44 // surprisingly this formula is true
	~~theorem @thm4_false ¬( (∃z2·(z2∈1‥3 ∧ x=z2)) ⇒ y=44 )~~
	end		end
	</pre>		</pre>