CODEWITHSUNDEEP
racketplt-redex
ckfinite
ckfinite

Reputation: 437

Print successes with redex-check

I am using redex-check to validate a model against another, and would like to see the intermediate (successful) results for debugging purposes. The most obvious way to do this would be to have the property-expr print the given term as a side-effect, but this is inelegant. Is there another way to look at intermediate redex-check attempts?

Upvotes: 2

Views: 63

Answers (1)

Leif Andersen
Leif Andersen

Reputation: 22332

It looks like you have the right idea on how to do this. In fact, the example for redex-check in the docs actually does this:

(let ([R (reduction-relation
            empty-lang
            (--> (Σ) 0)
            (--> (Σ number) number)
            (--> (Σ number_1 number_2 number_3 ...)
                 (Σ ,(+ (term number_1) (term number_2))
                    number_3 ...)))])
    (redex-check
     empty-lang
     (Σ number ...)
     (printf "~s\n" (term (number ...)))
      #:attempts 3
      #:source R))

Writes the following result to current-output-port:

()
(0)
(2 0)
redex-check: no counterexamples in 1 attempt (with each clause)

Upvotes: 1

Related Questions