redex icon indicating copy to clipboard operation
redex copied to clipboard

`generate-term` from reduction relation bypasses `#:domain`.

Open florence opened this issue 6 years ago • 0 comments

Concider:

#lang racket
(require redex/reduction-semantics)
(define-language L)
(define r
  (reduction-relation
   L
   #:domain 1
   (--> any any)))

(generate-term #:source r 5)

This will generate things like, say strings, which are not 1. I would expect this generation to, at least, fail when it attempts to generate a term outside of the domain of the relation.

florence avatar Dec 19 '19 16:12 florence