[plt-scheme] redex: leveraging generated checks and coverage

Hi,

I would like to understand better how I can most interestingly use the  
generative checks supported by PLT Redex. This is a fairly messy  
email, with several related points. I'd appreciate any comment/ 
feedback on them.

* What kind of interesting properties can be checked with check- 
reduction-relation?
for instance, I would imagine useful to check that all well-formed  
program reduces to either a value, or a well-defined error. Ie.  
something like:

(check-reduction-relation red
(λ (t)
   (redex-match lang ((store (l_1 v_1) ...) v_2)
                (apply-reduction-relation* red t)))

Except that means I have to write rules each and every strange program  
that can be produced.
Still, is that good practice? or is that over-specification?

* I was surprised that using a property that does not call reduction,  
check-reduction-relation was able to determine some ambiguity in a  
metafunction (same clause gave possibly different results given the  
same term)
a) how did it get to the metafunction? (my property function was just  
a print function)
b) what kind of testing does it do exactly? (to determine the above,  
it must have run it several times with the same term, at least)
All in all, I guess I don't understand completely what is tested here  
(assuming the property function does not do anything)

* At times, I get:
check-reduction-relation: unable to generate pattern <pattern-here> in  
<x> attempts
what am I supposed to learn from that? (from a language design point  
of view)

* Finally, I really enjoy the coverage report for a reduction  
relation. There does not seem to be a similar functionality for  
metafunctions, though. It would be nice if I could get confidence that  
my test cases, in addition to testing all reduction rules, actually  
cover each possible path in the metafunctions (ie. telling me, for  
each metafunction, how many times each clause has matched).

Best,

-- Éric