Open
Description
When debugging a failing case produced by qcheck-lin
, it would be nice if dscheck
could explore only the interleavings that produce the same intermediate values as reported by qcheck-lin
(and skip the other execution traces that are less likely to have a bug). I think it would be enough to raise a specific exception to indicate that we don't need to continue exploring that way: (but not report it as a failure)
if value <> expected then raise Dscheck.Skip ; (* ... *)
(It almost works if the user does the try...with Skip -> ()
on their side, because the final
postcondition is still called)
Metadata
Assignees
Labels
No labels
Activity