test-->>∃ #:steps n passes test if n > than the number of actual reduction steps for a term.

[xyzwwwww]

I noticed in the redex reference that the default #:steps value is 1000. However, would it be useful if this specific case maybe fails since the reduction require much smaller number of steps.

(test-->>∃ #:steps 8 ->* (term (λ (x : Nat) (car (cons (+ 1 2) 2)))) (term (λ (x : Nat) 3)))

[rfindler]

This isn't a complete program so I'm not entirely sure what you mean, but here are two examples, one where it finishes in the bound and one where it doesn't and I see the expected results.

#lang racket
(require redex/reduction-semantics)
(define-language L
  (n ::= Z (S n)))

(define-judgment-form L
  #:mode (->* I O)
  [-------------
   (->* (S n) n)])

(test-->>∃ #:steps 6 ->*
           (term (S (S (S (S Z)))))
           (term Z))

(test-->>∃ #:steps 2 ->*
           (term (S (S (S (S Z)))))
           (term Z))

(test-results)

namely:

FAILED /Users/robby/tmp.rkt:15.0
term Z not reachable from (S (S (S (S Z)))) (within 2 steps)
1 test failed (out of 2 total).

[xyzwwwww]

I should have explained better.

->* is the compatible closure for the language.

My point here is that if the reduction steps are less than the mentioned steps in #:steps, even then the tests pass. I understand that it is the default behavior of the tests.

However, my thought was if we could have tests passing when the reduction steps are exactly equal to #:steps n, where n is the precise number.

[rfindler]

Can you supply some working code to better illustrate what you mean, please?

[rfindler]

The steps argument is more of an upper-bound to avoid running for a long time than it is to count an exact number of steps. One complexity of adding one is that these relations don't necessarily have exactly one way to reduce each term so we'd have to define something that makes sense for such relations too.