is_superset_with_proof sometimes gives incorrect proof
Reported by Douglas Creager | June 23rd, 2008 @ 08:52 PM | in 1.0-α2
The is_superset_with_proof function doesn't always return the correct proof when the superset test fails. For instance,
{2} ?>= {1}
should return 1 as the proof, since that's an element in B that's not in A. Instead, it returns 2.
This causes a similar problem with refinement checking. The following CSPM is not a valid refinement:
P = a -> P [] c -> P
Q = a -> Q [] b -> Q
assert P [T= Q
The counterexample to this refinement is
<>: b
In other words, after an empty trace, Q can perform a b action that isn't allowed by P. This exposes the superset bug, giving an incorrect counterexample of
<>: c
Comments and changes to this ticket
-
Douglas Creager June 23rd, 2008 @ 09:12 PM
- State changed from “new” to “resolved”
(from [d9c7dc294b48e2f3a5009e26a27a96b33f562db8]) Fixed superset proof for integer sets
The is_superset_with_proof method would return incorrect proof in
certain situations. When testing A >= B, it's supposed to return an
element of B that's not in A. Since our method works on sorted sets,
it will return the least such element, though this is not a required
part of the method's contract. When A contained an element that was
greater than the least element of B not in A, our method would return
the A element, not the B element. This would cause downstream errors
in the refinement code, in that the wrong counterexample could be
returned in certain situations.
Lighthouse: [#9 state:resolved]
Please Sign in or create a free account to add a new ticket.
With your very own profile, you can contribute to projects, track your activity, watch tickets, receive and update tickets through your email and much more.
Create new ticket
Create your profile
Help contribute to this project by taking a few moments to create your personal profile. Create your profile »
An open-source refinement checker for the CSP process algebra.
Douglas Creager