redex icon indicating copy to clipboard operation
redex copied to clipboard

`cross` plus small grammar causes infinite loop in term generation

Open florence opened this issue 6 years ago • 0 comments

The program:

#lang racket
(require redex/reduction-semantics)

(define-language esterel-check
  (p ::= nothing (ρ θ p))
  (θ ::= · (S θ)))

(redex-check
 esterel-check
 (cross p)
 (displayln "running")
 #:attempts 100)

Never prints running and eventually consumes all my memory.

This seems to be new behavior since 4bb07c7baa2cb33. I am current on git HEAD.

florence avatar Oct 01 '19 18:10 florence