;;; SPDX-License-Identifier: LGPL-3.0-or-later
;;; SPDX-FileCopyrightText: Copyright © 2010-2021 Tony Garnock-Jones <tonyg@leastfixedpoint.com>

#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?))