I'm sorry it took me so long to get back to this. I'm not sure there
is a good thing to be added to Redex for this problem. Overall, it
seems like a graph search problem and there are multiple different
strategies depending on properties of the graph that you're searching.
It's not too hard to code these up in Racket and then find the best
one for your task, I would say. And redex's current support is pretty
simplistic, tailored to models with much less interesting reduction
graphs than yours has, I think.
If you find what seems to be a particularly useful and general purpose
search strategy and want it to be included in Redex, I'd be delighted
if you would make a pull request. In the meantime, I've offered one
that may or may not work well for your model, below.
hth,
Robby
#lang racket
(require redex/reduction-semantics)
(define-language L (n ::= natural))
(define red
(reduction-relation
L
(--> n ,(max 0 (min 20 (+ (term n) 3))))
(--> n ,(max 0 (min 20 (- (term n) 1))))))
(define (find-path red from to)
(define parents (make-hash))
(let/ec done
(let loop ([t from])
(define nexts (apply-reduction-relation red t))
(for ([next (in-list (remove-duplicates nexts))])
(cond
[(equal? next to)
(hash-set! parents to t)
(done)]
[(hash-ref parents next #f)
(void)]
[else
(hash-set! parents next t)
(loop next)]))))
(let loop ([term to])
(cond
[(equal? term from) (list from)]
[else (cons term (loop (hash-ref parents term)))])))
(find-path red 0 10)
On Sun, Dec 20, 2015 at 6:26 AM, Anton Podkopaev <podkoav...@gmail.com> wrote:
> Unfortunately, I need something else, because my semantics is highly
> non-deterministic, and I want to be able to see only paths, which lead to a
> certain term.
>
> BR,
> Anton Podkopaev
>
> 2015-12-18 20:49 GMT+03:00 Robby Findler <ro...@eecs.northwestern.edu>:
>>
>> I think you may want to call apply-reduction-relation* with a
>> #:stop-when argument instead?
>>
>> Robby
>>
>>
>> On Fri, Dec 18, 2015 at 5:33 AM, Anton Podkopaev <podkoav...@gmail.com>
>> wrote:
>> > Hello, colleagues!
>> >
>> > Is there any way to get a term trace from successful test-->>E in Redex?
>> >
>> > BR,
>> > Anton Podkopaev, PhD student, SPbSU
>> >
>> > --
>> > You received this message because you are subscribed to the Google
>> > Groups
>> > "Racket Users" group.
>> > To unsubscribe from this group and stop receiving emails from it, send
>> > an
>> > email to racket-users+unsubscr...@googlegroups.com.
>> > For more options, visit https://groups.google.com/d/optout.
>
>
--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
