#lang racket/base (require redex) (require "network-calculus.rkt") (require racket/list) (require racket/set) (require racket/match) (require "redex-utils.rkt") ;; Plan: ;; ;; The chat service listens for `(connect ,?) at the metalevel. ;; Spawns a process in response, which ;; - listens for metalevel `(input ,user ,?) ;; - advertises `(chat ,user ,?) ;; - listens for `(chat ,? ,?) and sends metalevel `(output ,user ,line) ;; - listens for metalevel `(disconnect ,?) ;; ;; Acceptor is stateless; relay "closes over" its own user name and a ;; set of active user names. ;;--------------------------------------------------------------------------- ;; Acceptor (define (acceptor-beh e s) (match* (s e) [(s `(meta (send (connect ,user)))) (values (list (boot-relay user)) s)])) (define (boot-acceptor) (term (spawnA acceptor noState (newtable ( (meta (sub (connect *) 0)) ))))) ;;--------------------------------------------------------------------------- ;; Relay (struct relay-state (username peers) #:transparent) (define (subscriptions->peer-set peers) (list->set (filter-map (match-lambda [`(pub (chat ,u *) ,_) u] [_ #f]) peers))) (define (relay-beh e s) (match-define (relay-state username previous-peers) s) (match e [`(newtable ,subscriptions) (define new-peers (subscriptions->peer-set subscriptions)) (define arrived (set-subtract new-peers previous-peers)) (define departed (set-subtract previous-peers new-peers)) (values (append (map (lambda (u) (term (meta (send (output ,username ,(format "~a departed" u)))))) (set->list departed)) (map (lambda (u) (term (meta (send (output ,username ,(format "~a arrived" u)))))) (set->list arrived))) (relay-state username new-peers))] [`(meta (send (input ,_ ,line))) (values (list (term (send (chat ,username ,line)))) s)] [`(meta (send (disconnect ,_))) (values (list (term (newtable ()))) s)] [`(send (chat ,who ,line)) (values (list (term (meta (send (output ,username ,(format "~a says ~a" who line)))))) s)])) (define (boot-relay username) (term (spawnA relay ,(relay-state username (set)) (newtable ( (meta (sub (input ,username *) 0)) (meta (pub (output ,username *) 0)) (meta (sub (disconnect ,username) 0)) (sub (chat * *) 1) (pub (chat ,username *) 0) ))))) ;;--------------------------------------------------------------------------- ;; Main (current-eval0 (lambda (f e u) (write (list 'LEAFSTEP-I f u e)) (newline) (define-values (actions u1) (match* (f e u) [('acceptor e s) (acceptor-beh e s)] [('relay e s) (relay-beh e s)] )) (write (list 'LEAFSTEP-O f u1 actions)) (newline) (values actions u1))) (define (event-bursts initial-sigma . eventss) (if (null? eventss) (void) (apply event-bursts (quasi-trace ==> (term (groundEvents ,@(car eventss) ,initial-sigma))) (cdr eventss)))) (event-bursts (term (bootSigma ,(boot-acceptor))) (term ((send (connect A)) (send (connect B)))) (term ((send (input A "Hello")))) (term ((send (disconnect A)))) (term ((send (connect C)) (send (disconnect B)))))