Fix bug with incorrect dropped action.
This commit is contained in:
parent
dfb0eae02c
commit
1467912f57
|
@ -0,0 +1,13 @@
|
||||||
|
#lang prospect
|
||||||
|
;; Analogous to nc-incremental-meta-drop.rkt in the Redex model.
|
||||||
|
;; Demonstrates (hopefully) correct processing of meta-interests when dropping a patch.
|
||||||
|
|
||||||
|
(spawn-world
|
||||||
|
(spawn (lambda (e u)
|
||||||
|
(match u
|
||||||
|
[0 (transition 1 '())]
|
||||||
|
[1 (transition 2 (retract 'a #:meta-level 1))]
|
||||||
|
[_ #f]))
|
||||||
|
0
|
||||||
|
(assert 'a #:meta-level 1)
|
||||||
|
(assert (observe 'a) #:meta-level 1)))
|
|
@ -53,7 +53,10 @@
|
||||||
;; be minimal with respect to existing interests of its label.
|
;; be minimal with respect to existing interests of its label.
|
||||||
(define old-routing-table (mux-routing-table m))
|
(define old-routing-table (mux-routing-table m))
|
||||||
(define new-routing-table (apply-patch old-routing-table delta))
|
(define new-routing-table (apply-patch old-routing-table delta))
|
||||||
(define delta-aggregate (compute-aggregate-patch delta label old-routing-table))
|
(define delta-aggregate
|
||||||
|
(compute-aggregate-patch delta label old-routing-table))
|
||||||
|
(define delta-aggregate/no-meta
|
||||||
|
(compute-aggregate-patch delta label old-routing-table #:remove-meta? #t))
|
||||||
(define affected-pids (let ((pids (compute-affected-pids old-routing-table delta)))
|
(define affected-pids (let ((pids (compute-affected-pids old-routing-table delta)))
|
||||||
(set-remove (set-add pids label) 'meta))) ;; TODO: removing meta is weird
|
(set-remove (set-add pids label) 'meta))) ;; TODO: removing meta is weird
|
||||||
(values (struct-copy mux m [routing-table new-routing-table])
|
(values (struct-copy mux m [routing-table new-routing-table])
|
||||||
|
@ -69,7 +72,7 @@
|
||||||
[else
|
[else
|
||||||
(cons pid (view-patch delta-aggregate (mux-interests-of m pid)))]))
|
(cons pid (view-patch delta-aggregate (mux-interests-of m pid)))]))
|
||||||
(and (not (meta-label? label))
|
(and (not (meta-label? label))
|
||||||
(drop-patch delta-aggregate)))))
|
(drop-patch delta-aggregate/no-meta)))))
|
||||||
|
|
||||||
(define (compute-affected-pids routing-table delta)
|
(define (compute-affected-pids routing-table delta)
|
||||||
(define cover (matcher-union (patch-added delta) (patch-removed delta)))
|
(define cover (matcher-union (patch-added delta) (patch-removed delta)))
|
||||||
|
|
|
@ -135,9 +135,13 @@
|
||||||
;; from `label`'s own interests, but where interest remains from other
|
;; from `label`'s own interests, but where interest remains from other
|
||||||
;; peers, the overall effect will be nil.
|
;; peers, the overall effect will be nil.
|
||||||
;;
|
;;
|
||||||
|
;; If `remove-meta?` is true, then in addition to ignoring existing
|
||||||
|
;; `label` interests, we also ignore existing `'meta`-labelled
|
||||||
|
;; interests. This is used when computing an outbound/dropped patch.
|
||||||
|
;;
|
||||||
;; PRECONDITION: `p` is (set label)-labelled
|
;; PRECONDITION: `p` is (set label)-labelled
|
||||||
;; PRECONDITION: `base` is (set ...)-labelled
|
;; PRECONDITION: `base` is (set ...)-labelled
|
||||||
(define (compute-aggregate-patch p label base)
|
(define (compute-aggregate-patch p label base #:remove-meta? [remove-meta? #f])
|
||||||
(define (add-combiner v1 v2)
|
(define (add-combiner v1 v2)
|
||||||
;; Keep only points where `p` would add, where no `label` interest
|
;; Keep only points where `p` would add, where no `label` interest
|
||||||
;; is present*, and where no non-`label` interest is present. That
|
;; is present*, and where no non-`label` interest is present. That
|
||||||
|
@ -148,16 +152,32 @@
|
||||||
;; has established that no `label` interest is present at these
|
;; has established that no `label` interest is present at these
|
||||||
;; points), we can always discard such points by returning a
|
;; points), we can always discard such points by returning a
|
||||||
;; constant #f.
|
;; constant #f.
|
||||||
#f)
|
;;
|
||||||
|
;; ...except when `remove-meta?` is true. In that case, we need to
|
||||||
|
;; keep the point in the case that the only interest present is
|
||||||
|
;; `'meta`-labeled interest.
|
||||||
|
(if (and remove-meta? (equal? v2 (set 'meta)))
|
||||||
|
v1
|
||||||
|
#f))
|
||||||
(define (rem-combiner v1 v2)
|
(define (rem-combiner v1 v2)
|
||||||
;; Keep only points where `p` would remove, where `label` interest
|
;; Keep only points where `p` would remove, where `label` interest
|
||||||
;; is present, and where no non-`label` interest is present. We
|
;; is present, and where no non-`label` interest is present. We
|
||||||
;; know that a previous patch-limiting operation has ensured that
|
;; know that a previous patch-limiting operation has ensured that
|
||||||
;; `label` interest is present, so we only need to check whether
|
;; `label` interest is present, so we only need to check whether
|
||||||
;; any other interest exists at each point.
|
;; any other interest exists at each point.
|
||||||
|
;;
|
||||||
|
;; ...and again, for `remove-meta?`, the condition is slightly
|
||||||
|
;; different. We need to keep the point in that case when either
|
||||||
|
;; only label interest exists (which by precondition is always the
|
||||||
|
;; case), or when exactly `label` and `'meta` interest exists, and
|
||||||
|
;; in no other case.
|
||||||
(if (= (set-count v2) 1)
|
(if (= (set-count v2) 1)
|
||||||
v1 ;; only `label` interest (previously established) exists here.
|
v1 ;; only `label` interest (previously established) exists here.
|
||||||
#f)) ;; other interest exists here, so we should discard this removed-point.
|
(if (and remove-meta?
|
||||||
|
(= (set-count v2) 2)
|
||||||
|
(set-member? v2 'meta))
|
||||||
|
v1 ;; remove-meta? is true, and exactly `label` and `'meta` interest exists here.
|
||||||
|
#f))) ;; other interest exists here, so we should discard this removed-point.
|
||||||
(patch (matcher-subtract (patch-added p) base #:combiner add-combiner)
|
(patch (matcher-subtract (patch-added p) base #:combiner add-combiner)
|
||||||
(matcher-subtract (patch-removed p) base #:combiner rem-combiner)))
|
(matcher-subtract (patch-removed p) base #:combiner rem-combiner)))
|
||||||
|
|
||||||
|
@ -387,4 +407,52 @@
|
||||||
(post-checks R1 R1-relabeled p-aggregate1)
|
(post-checks R1 R1-relabeled p-aggregate1)
|
||||||
(post-checks R2 R2-relabeled p-aggregate2)
|
(post-checks R2 R2-relabeled p-aggregate2)
|
||||||
)
|
)
|
||||||
|
|
||||||
|
(let* ((ma (set->matcher (set 'a) (set 1)))
|
||||||
|
(mb (set->matcher (set 'b) (set 1)))
|
||||||
|
(mmeta (set->matcher (set 'meta) (set 1)))
|
||||||
|
(R0 (matcher-empty))
|
||||||
|
(R1 mmeta)
|
||||||
|
(R2 mb)
|
||||||
|
(R3 (matcher-union mb mmeta))
|
||||||
|
(R4 ma)
|
||||||
|
(R5 (matcher-union ma mmeta))
|
||||||
|
(R6 (matcher-union ma mb))
|
||||||
|
(R7 (matcher-union (matcher-union ma mb) mmeta))
|
||||||
|
(p0 empty-patch)
|
||||||
|
(p+ (patch (set->matcher (set 'a) (set 1)) (matcher-empty)))
|
||||||
|
(p- (patch (matcher-empty) (set->matcher (set 'a) (set 1)))))
|
||||||
|
(check-equal? (compute-aggregate-patch p0 'a R0) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p0 'a R1) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p0 'a R2) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p0 'a R3) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p0 'a R4) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p0 'a R5) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p0 'a R6) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p0 'a R7) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p+ 'a R0) p+)
|
||||||
|
(check-equal? (compute-aggregate-patch p+ 'a R1) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p+ 'a R2) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p+ 'a R3) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p- 'a R4) p-)
|
||||||
|
(check-equal? (compute-aggregate-patch p- 'a R5) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p- 'a R6) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p- 'a R7) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p0 'a R0 #:remove-meta? #t) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p0 'a R1 #:remove-meta? #t) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p0 'a R2 #:remove-meta? #t) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p0 'a R3 #:remove-meta? #t) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p0 'a R4 #:remove-meta? #t) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p0 'a R5 #:remove-meta? #t) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p0 'a R6 #:remove-meta? #t) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p0 'a R7 #:remove-meta? #t) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p+ 'a R0 #:remove-meta? #t) p+)
|
||||||
|
(check-equal? (compute-aggregate-patch p+ 'a R1 #:remove-meta? #t) p+)
|
||||||
|
(check-equal? (compute-aggregate-patch p+ 'a R2 #:remove-meta? #t) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p+ 'a R3 #:remove-meta? #t) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p- 'a R4 #:remove-meta? #t) p-)
|
||||||
|
(check-equal? (compute-aggregate-patch p- 'a R5 #:remove-meta? #t) p-)
|
||||||
|
(check-equal? (compute-aggregate-patch p- 'a R6 #:remove-meta? #t) p0)
|
||||||
|
(check-equal? (compute-aggregate-patch p- 'a R7 #:remove-meta? #t) p0)
|
||||||
|
)
|
||||||
)
|
)
|
||||||
|
|
Loading…
Reference in New Issue