is_superset_with_proof sometimes gives incorrect proof

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

Reported by Douglas Creager · June 23rd, 2008 @ 08:52 PM

Activity

Douglas Creager
- 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]
http://github.com/dcreager/hst/c...

June 23rd, 2008 @ 09:12 PM

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.