syndicate-lang
/
syndicate-2017
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

fix a couple bugs

This commit is contained in:
Sam Caldwell 2019-07-31 11:40:12 -04:00
parent 443e1f9ac1
commit 29f589d7c4
1 changed files with 45 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

57
racket/typed/proto.rkt
View File

@ -240,7 +240,7 @@
;; - to is the current state that has been reached ;; - to is the current state that has been reached
;; - by is the external event that kicked off this sequence ;; - by is the external event that kicked off this sequence
;; - with is a list of pending events to be processed ;; - with is a list of pending events to be processed
;; - effs are effects emitted on this path ;; - effs are the external effects emitted on this path
(struct work-item (from path/r to by with effs) #:transparent) (struct work-item (from path/r to by with effs) #:transparent)
(let/ec fail (let/ec fail
(define (walk work visited st#) (define (walk work visited st#)
@ -309,13 +309,14 @@
by by
evt evt
D))) D)))
(define internal-effs (effs->internal-events more-effs)) (define-values (internal-effs external-effs)
(partition-transition-effects more-effs))
(work-item from (work-item from
path/r+ path/r+
dest dest
by by
(append more-pending internal-effs) (append more-pending internal-effs)
(append effs more-effs)))])) (append effs external-effs)))]))
;; NOTE: knowledge of scheduling used here ;; NOTE: knowledge of scheduling used here
(define pending* (define pending*
@ -337,7 +338,9 @@
#:unless (equal? D DataflowEvt) #:unless (equal? D DataflowEvt)
[t (in-set txns)]) [t (in-set txns)])
(match-define (transition es dst) t) (match-define (transition es dst) t)
(work-item to '() dst D (effs->internal-events es) es))) (define-values (internal-effs external-effs)
(partition-transition-effects es))
(work-item to '() dst D internal-effs external-effs)))
(define new-st# (update-path st# from to by effs)) (define new-st# (update-path st# from to by effs))
(walk (append more-work induced-work* new-paths-work) visited+ new-st#)] (walk (append more-work induced-work* new-paths-work) visited+ new-st#)]
[else [else
@ -412,7 +415,24 @@
(set (transition '() (set 'x))))) (set (transition '() (set 'x)))))
(check-true (hash-has-key? st# (set 'x))) (check-true (hash-has-key? st# (set 'x)))
(define x-txns (state-transitions (hash-ref st# (set 'x)))) (define x-txns (state-transitions (hash-ref st# (set 'x))))
(check-equal? x-txns (hash))))) (check-equal? x-txns (hash))))
(test-case
"remove internal effects from transitions"
(define role
(Role 'x
(list (Reacts (Asserted Int)
(list (Realizes String)
(Sends Int)
(Role 'y (list)))))))
(define rg (run/timeout (thunk (compile role))))
(check-true (role-graph? rg))
(define rgi (run/timeout (thunk (compile/internal-events rg role))))
(check-true (role-graph? rgi))
(define state# (role-graph-states rgi))
(check-true (hash-has-key? state# (set 'x)))
(define txn# (state-transitions (hash-ref state# (set 'x))))
(check-equal? txn#
(hash (Asserted Int) (set (transition (list (send Int)) (set 'x 'y)))))))
;; (Setof τ) (Setof τ) -> (Setof D) ;; (Setof τ) (Setof τ) -> (Setof D)
;; Subtyping-based assertion routing (*not* intersection - TODO) ;; Subtyping-based assertion routing (*not* intersection - TODO)
@ -488,12 +508,14 @@
(set))) (set)))
(hash))])) (hash))]))
;; (Listof (TransitionEffect)) -> (Listof D) ;; (Listof (TransitionEffect)) -> (Values (Listof D) (Listof TransitionEffect))
(define (effs->internal-events effs) ;; partition the internal and external effects, translating realize effects to
(for/list ([e (in-list effs)] ;; Realize events along the way
#:when (realize? e)) (define (partition-transition-effects effs)
(match-define (realize m) e) (define-values (internals externals) (partition realize? effs))
(Realize m))) (define (realize->Realize e) (Realize (realize-ty e)))
(values (map realize->Realize internals)
externals))
;; D -> Bool ;; D -> Bool
;; test if D corresponds to an external event (assertion, message) ;; test if D corresponds to an external event (assertion, message)
@ -855,7 +877,8 @@
(match eff (match eff
[(or (send _) [(or (send _)
(realize _)) (realize _))
(set (transition (list eff) st))] (for/set ([txn (in-set (loop st rest))])
(transition (cons eff (transition-effs txn)) (transition-dest txn)))]
[(start nm) [(start nm)
(define st+ (set-add st nm)) (define st+ (set-add st nm))
(define start-effs (hash-ref (hash-ref txn# nm) (StartOf nm))) (define start-effs (hash-ref (hash-ref txn# nm) (StartOf nm)))
@ -886,6 +909,16 @@
(transition-effs next-txn)) (transition-effs next-txn))
(transition-dest next-txn))))])]))) (transition-dest next-txn))))])])))
(module+ test
(test-case
"bug in apply-effects"
;; was dropping everything after the first send or realize effect
(define txns (apply-effects (list (realize Int) (realize String))
(set)
(facet-tree (hash) (hash))
(hash)))
(check-equal? txns (set (transition (list (realize Int) (realize String)) (set))))))
;; FacetTree FacetName (Setof FacetName) -> (List FacetName) ;; FacetTree FacetName (Setof FacetName) -> (List FacetName)
;; return the facets in names that are children of the given facet nm, ordered ;; return the facets in names that are children of the given facet nm, ordered
;; by their distance (farthest children first etc.) ;; by their distance (farthest children first etc.)