使用 redex-check 打印成功

【问题标题】：Print successes with redex-check使用 redex-check 打印成功
【发布时间】：2016-01-19 14:16:25
【问题描述】：

我正在使用 redex-check 来验证一个模型与另一个模型，并希望查看中间（成功）结果以进行调试。最明显的方法是让 property-expr 打印给定的术语作为副作用，但这是不优雅的。还有其他方法可以查看中间的 redex-check 尝试吗？

【问题讨论】：

标签： racket plt-redex

【解决方案1】：

看来您对如何执行此操作有正确的想法。其实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))

将以下结果写入current-output-port：

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

【讨论】：