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.
