redex
redex copied to clipboard
Generating random expressions sometimes results in an infinite loop
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.