dscheck icon indicating copy to clipboard operation
dscheck copied to clipboard

Add a way to skip execution of traces

Open art-w opened this issue 1 year ago • 0 comments

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)

art-w avatar Nov 28 '22 20:11 art-w