redex icon indicating copy to clipboard operation
redex copied to clipboard

Generating random expressions sometimes results in an infinite loop

Open joshuaharry opened this issue 3 years ago • 0 comments

Consider the following program:

#lang racket/base

(require redex/reduction-semantics)

(define-language L
  (self ::= (self)))

(define-judgment-form L
  #:mode (--> I O)
  #:contract (--> self self)
  [----------- "Do Nothing"
   (--> (self) (self))])

(define (f el)
  (printf "F ran!\n")
  (if (redex-match L val el) #true
      (= 1 (length (apply-reduction-relation --> el)))))

(printf "Start generation...\n")
(redex-check L self (f (term self)))

This code appears to print "Start generation..." before getting stuck while generating test cases.

joshuaharry avatar Sep 17 '21 19:09 joshuaharry