Sure. The trick is to use the #:reduce argument and then just ignore
the actual reduction relation. A revision of the earlier code
demonstrates, as below.
Robby
#lang racket
(require redex)
(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)]))))
parents)
(define parents (find-path red 0 10))
(define children
(for/hash ([(k v) (in-hash parents)]
#:unless (equal? k 0))
(values v k)))
(traces red 0
#:reduce
(λ (_ t)
(let/ec k
(list (list #f (hash-ref children t (λ () (k '()))))))))
On Wed, Feb 10, 2016 at 4:08 AM, Anton Podkopaev <[email protected]> wrote:
> Robby,
>
> Thank you, it mostly works for my semantics, and I know how to change the
> algorithm for some corner cases.
>
> Then I have one more question --- then I get terms (a result of
> `find-path'), is there a way to show them (and only them) using GUI tools
> like `traces' and `stepper'?
>
>
>
> BR,
> Anton Podkopaev
>
> On Wed, Feb 10, 2016 at 2:42 AM, Robby Findler <[email protected]>
> wrote:
>>
>> 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 <[email protected]>
>> 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 <[email protected]>:
>> >>
>> >> 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 <[email protected]>
>> >> 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 [email protected].
>> >> > 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 [email protected].
For more options, visit https://groups.google.com/d/optout.
