racket - redex-check で成功を出力する

Question

モデルを別のモデルに対して検証するために redex-check を使用していますが、デバッグ目的で中間 (成功) の結果を確認したいと考えています。これを行う最も明白な方法は、property-expr に与えられた用語を副作用として出力させることですが、これは洗練されていません。中間の redex-check 試行を調べる別の方法はありますか?

Answer 1

これを行う方法について正しい考えがあるようです。実際、ドキュメントの例はredex-check実際にこれを行います:

(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)