60 lines
2.2 KiB
Racket
60 lines
2.2 KiB
Racket
#lang syndicate/test-implementation
|
|
;; Tests that adhoc assertions are always removed on termination, even
|
|
;; when being relayed across a dataspace boundary.
|
|
|
|
(require syndicate/bag)
|
|
(require syndicate/pattern)
|
|
|
|
(message-struct trigger ())
|
|
|
|
(define (spawn-seen-monitor)
|
|
(spawn #:name 'monitor
|
|
(on (asserted $x) (printf "Seen: ~v\n" x))))
|
|
|
|
(define (spawn-double-trigger)
|
|
;; Sending the trigger twice is one of the critical factors for this test case
|
|
(spawn* #:name 'double-trigger
|
|
(until (asserted (observe (trigger))))
|
|
(send! (trigger))
|
|
(send! (trigger))))
|
|
|
|
(define (only-seen-monitor-output?)
|
|
(expected-output (list "Seen: '#s(observe #s(capture #s(discard)))")))
|
|
|
|
(define (only-seen-monitor-assertions?)
|
|
(lambda ()
|
|
(define actual-assertions (final-assertions))
|
|
(define expected-assertions (set (observe (capture (discard)))))
|
|
(or (equal? actual-assertions expected-assertions)
|
|
(error 'only-seen-monitor-assertions? "Actual-assertions ~v <> expected-assertions ~v"
|
|
actual-assertions
|
|
expected-assertions))))
|
|
|
|
(test-case
|
|
[(spawn-seen-monitor)
|
|
(dataspace #:name 'middle-dataspace
|
|
(spawn-double-trigger)
|
|
(dataspace #:name 'inner-dataspace
|
|
(spawn #:name 'actor0
|
|
(on (message (inbound (trigger))) (quit-dataspace!))
|
|
(on (message (inbound (trigger)))
|
|
(flush!)
|
|
(assert! (outbound (outbound 'B)))))))]
|
|
no-crashes
|
|
(only-seen-monitor-output?)
|
|
(only-seen-monitor-assertions?))
|
|
|
|
(test-case
|
|
[(spawn-seen-monitor)
|
|
(dataspace #:name 'middle-dataspace
|
|
(spawn-double-trigger)
|
|
(dataspace #:name 'inner-dataspace
|
|
(spawn #:name 'actor0
|
|
(on (message (inbound (trigger))) (quit-dataspace!))
|
|
(on (message (inbound (trigger)))
|
|
(flush!)
|
|
(react (assert (outbound (outbound 'B))))))))]
|
|
no-crashes
|
|
(only-seen-monitor-output?)
|
|
(only-seen-monitor-assertions?))
|