/* Verification: forcing opposite values for a flag */ explain

1 files changed, 32 insertions, 0 deletions

diff --git a/GLEP:73.mw b/GLEP:73.mw
index 071c7c6..d8b07bf 100644
--- a/GLEP:73.mw
+++ b/GLEP:73.mw
@@ -514,6 +514,38 @@ As it can clearly be seen here, this condition will never evaluate to true becau
 An occurrence of such a constraint is extremely unlikely. However, it effectively breaks some of the assumptions for the algorithms since it is impossible to provide a valid set of flags that would satisfy the condition. It is therefore explicitly rejected as invalid.
 
 ====Verification: forcing opposite values for a flag====
+This check is meant to account for the case where a combination of two different constraints would require a flag to be both enabled and disabled at the same time. A generic example is:
+
+ a? ( c )
+ b? ( !c )
+
+Here, the first constraint requires ''c'' enabled while the second one requires it disabled. Therefore, if the user enables both ''a'' and ''b'', the constraint can not be satisfied. The only enforcements explicitly allowed here are enabling and disabling ''c'' in order, neither of which is capable of solving the problem.
+
+The first condition listed in the algorithm verifies the most important symptom of the problem — that two flattened constraints require the opposite values of a flag. The remaining conditions are meant to rule out false positives.
+
+The second rule states that both conditions need to be able to simultaneously evaluate to true, or in other words the two conditions can not contain opposite values. For example, this rules out the following case:
+
+ a? ( c )
+ !a? ( b? ( !c ) )
+
+where both conditions can never evaluate to true simultaneously because they require the opposite values of ''a''.
+
+The third and fourth rules aim to verify that the condition can realistically occur after considering all the constraints preceding it. This is meant to avoid the following kind of false positives:
+
+ !a? ( !b )
+ !a? ( !c )
+ b? ( c )
+
+Here, after considering the first two conditions the second and third constraints can occur simultaneously because ''!a'' and ''b'' do not conflict with each other. However, after considering the constraints preceding it is clear that they can't since ''!a'' will implicitly disable ''b'', rendering the third condition false.
+
+It should be noted that this also works for corner cases like:
+
+ c? ( a )
+ a? ( b )
+ d? ( !a )
+ !a? ( !b )
+
+because even though the algorithm would incorrectly presume that the second and the fourth conditions can not occur simultaneously, it will detect a conflict between the first and the third conditions.
 
 ====Verification: enabling a condition preceding the constraint====