diff options
author | 2017-07-07 21:55:00 +0000 | |
---|---|---|
committer | 2017-07-07 21:55:00 +0000 | |
commit | c0751bc990f6a742810cccb778a9df48356e19fb (patch) | |
tree | 4c2f1b0f1ede745b8a492a124032c44dc8419285 | |
parent | /* Verification: forcing opposite values for a flag */ explain (diff) | |
download | glep-c0751bc990f6a742810cccb778a9df48356e19fb.tar.gz glep-c0751bc990f6a742810cccb778a9df48356e19fb.tar.bz2 glep-c0751bc990f6a742810cccb778a9df48356e19fb.zip |
/* Verification: enabling a condition preceding the constraint */ explain
-rw-r--r-- | GLEP:73.mw | 25 |
1 files changed, 25 insertions, 0 deletions
@@ -548,6 +548,31 @@ It should be noted that this also works for corner cases like: 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==== +This check verifies that a constraint will not meaningfully cause a constraint preceding it to start to apply. This effectively means the constraints that will require more than one iteration of the algorithm to enforce them. + +A generic example is: + + b? ( c ) + a? ( b ) + +In this case, having only ''a'' enabled will result in ''b'' being enabled in the first iteration, and ''c'' in the second. + +The first condition verifies the most important symptom of the problem — that is, that the effect of the later constraint matches the condition of an earlier constraint. The remaining conditions rule false positives out. + +Once again, the second condition checks whether the two conditions can occur simultaneously, that is not conflict one with another. A generic example of a false positive ruled out by this is: + + !a? ( b? ( c ) ) + a? ( b ) + +in which case although the second constraint enforces ''b'' that is one of the conditions for the first constraint, both conditions can not occur simultaneously since ''a'' would have to be enabled and disabled at the same time. + +The third rule checks whether the conditions of the later constraint do not enforce the same effect as the earlier constraint anyway. That is, they account for a relatively common pattern of: + + b? ( c ) + a? ( b ) + a? ( c ) + +Even though the second constraint causes the first one to start to apply, having ''a'' enabled will also cause the third constraint to apply. Since the third constraint has the same effect as the first one, applying the first one will have no effect (the constraint will be satisfied already) and the second iteration will not be required. ==Backwards compatibility== |