| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The pattern matcher's analysis was correctly finding
models under which the match in the enclosed test
could fail. But, when trying to render that model
as a counter example, it ran into an internal inconsistency
and gave up.
That inconsistency arose from VariableAssignment, which:
> turn the variable assignments into a tree
> the root is the scrutinee (x1), edges are labelled
> by the fields that are assigned a node is a variable
> example (which is later turned into a counter example)
In the process, it notes the unreachable case `V2 = NotHandled`,
which can only arise if `V1 = Op`, ie the scrutinee is `Op(NotHandled())`.
V2 is assosicated with the path `x1.arg`. The code then looked for
any variable assosicated with the prefix `x1` and registered that its
field `arg` was assosicated with this variable assignment.
However, the assignment for `V1 = NotHandled` (another missing case)
is also associated with the path `x1`. Registering this field makes
no sense here; we should only do that for `Op`.
This commit conditionally registers the fields based on the class
of `VariableAssignment#cls`. We no longer hit the inconsistency in
`VariableAssignment#allFieldAssignmentsLegal`.
This favourably changes the results of two existing tests.
I had to tweak the counter example pruning to avoid relying on
CounterExample.==, which is flaky in the light of Nil and List().
It is possible to have:
A, B where A != B && A.coveredBy(B) && B.coveredBy(A)
Luckily it is straightforward to implement pruning entirely with
coveredBy.
|
