diff --git a/racket/typed/examples/roles/book-club.rkt b/racket/typed/examples/roles/book-club.rkt index 240256e..724706a 100644 --- a/racket/typed/examples/roles/book-club.rkt +++ b/racket/typed/examples/roles/book-club.rkt @@ -62,13 +62,14 @@ (define (spawn-seller [inventory : Inventory]) (spawn τc + (begin (start-facet seller (field [books Inventory inventory]) ;; Give quotes to interested parties. (during (observe (book-quote (bind title String) discard)) ;; TODO - lookup - (assert (book-quote title (lookup title (ref books)))))))) + (assert (book-quote title (lookup title (ref books))))))))) (define-type-alias leader-role (Role (leader) @@ -101,7 +102,7 @@ (define (spawn-leader [titles : (List String)]) (spawn τc - (print-role + (begin (start-facet get-quotes (field [book-list (List String) (rest titles)] [title String (first titles)]) @@ -162,10 +163,11 @@ (Reacts (Know (Observe (BookInterestT String ★/t ★/t))) (Role (_) (Shares (BookInterestT String String Bool)))))) - + (define (spawn-club-member [name : String] [titles : (List String)]) (spawn τc + (begin (start-facet member ;; assert our presence (assert (club-member name)) @@ -173,7 +175,7 @@ (during (observe (book-interest (bind title String) discard discard)) (define answer (member? title titles)) (printf "~a responds to suggested book ~a: ~a\n" name title answer) - (assert (book-interest title name answer)))))) + (assert (book-interest title name answer))))))) (run-ground-dataspace τc (spawn-seller (list (tuple "The Wind in the Willows" 5) diff --git a/racket/typed/proto.rkt b/racket/typed/proto.rkt index e750f1d..8e1db5b 100644 --- a/racket/typed/proto.rkt +++ b/racket/typed/proto.rkt @@ -60,6 +60,18 @@ ;; a StructName is a Symbol +;; -------------------------------------------------------------------------- +;; Derived Types + +;; τ (Listof EP) -> EP +(define (During assertion eps) + (define facet-name (gensym 'during-inner)) + (Reacts (Know assertion) + (Role facet-name + (cons (Reacts (¬Know assertion) + (Stop facet-name '())) + eps)))) + ;; -------------------------------------------------------------------------- ;; Examples @@ -71,13 +83,6 @@ (Role 'client (list (Reacts (Know (Struct 'account (list Int))) '())))) -(define seller - (Role 'seller - (list - (Reacts (Know (Observe (Struct 'BookQuoteT (list String ⋆)))) - (Role 'fulfill - (list (Shares (Struct 'BookQuoteT (list String Int))))))))) - ;; τ τ -> τ ;; short hand for creating a book quote struct type (define (book-quote ty1 ty2) @@ -88,45 +93,83 @@ (define (book-interest ty1 ty2 ty3) (Struct 'book-interest (list ty1 ty2 ty3))) +;; τ -> τ +;; short hand for creating a book of the month type +(define (book-of-the-month ty) + (Struct 'book-of-the-month (list ty))) + +;; τ -> τ +;; short hand for creating a club member type +(define (club-member ty) + (Struct 'club-member (list ty))) + +(define seller + (Role 'seller + (list + (Reacts (Know (Observe (book-quote String ⋆))) + (Role 'fulfill + (list (Shares (book-quote String Int)))))))) + +(define seller-actual + (Role + 'seller27 + (list + (Reacts + (Know (Observe (book-quote String ⋆))) + (Role + 'during-inner29 + (list + (Shares (book-quote String (U (list Int Int)))) + (Reacts + (¬Know (Observe (book-quote String ⋆))) + (Stop 'during-inner29 '())))))))) + (define leader-spec (Role 'leader (list - (Reacts (Know (book-quote String Int)) - (Role 'poll - (list - (Reacts (Know (book-interest String String Bool)) - (Branch - (list - (Stop 'leader - (Role 'announce - (list - (Shares (Struct 'book-of-the-month (list String)))))) - (Stop 'poll (list))))))))))) + (Reacts + (Know (book-quote String Int)) + (Role 'poll + (list + (Reacts + (Know (book-interest String String Bool)) + (Branch + (list + (Stop 'leader + (Role 'announce + (list + (Shares (book-of-the-month String))))) + (Stop 'poll (list))))))))))) (define leader-actual - (Role 'get-quotes + (Role + 'get-quotes + (list + (Reacts + (Know (book-quote String Int)) + (Branch + (list + ;; problem 1: spec doesn't say actor can give up when running out of books + (Stop 'get-quotes '()) + (Role + 'poll-members (list - (Reacts (Know (book-quote String Int)) - (Branch (list - ;; problem 1: spec doesn't say actor can give up when running out of books - (Stop 'get-quotes '()) - (Role 'poll-members - (list - (Reacts (Know (book-interest String String ⋆)) - (Branch (list - ;; problem 2: combining poll-members and get-quotes here (should be another branch) - (Stop 'poll-members - (Stop 'get-quotes '())) - (Stop 'get-quotes - (Role 'announce - (list - (Shares (Struct 'book-of-the-month (list String))))))))) - (Reacts (¬Know (book-interest String String Bool)) (list)) - (Reacts (Know (book-interest String String Bool)) (list)) - (Reacts (¬Know (book-interest String String Bool)) (list)) - (Reacts (Know (book-interest String String Bool)) (list))))))) - (Reacts (¬Know (Struct 'club-member (list String))) (list)) - (Reacts (Know (Struct 'club-member (list String))) (list))))) + (Reacts + (Know (book-interest String String ⋆)) + (Branch (list + ;; problem 2: combining poll-members and get-quotes here (should be another branch) + (Stop 'poll-members + (Stop 'get-quotes '())) + (Stop 'get-quotes + (Role 'announce + (list + (Shares (book-of-the-month String)))))))) + (Reacts (¬Know (book-interest String String Bool)) (list)) + (Reacts (Know (book-interest String String Bool)) (list)) + (Reacts (¬Know (book-interest String String Bool)) (list)) + (Reacts (Know (book-interest String String Bool)) (list))))))) + (Reacts (¬Know (club-member String)) (list)) + (Reacts (Know (club-member String)) (list))))) (define leader-fixed? (Role 'get-quotes @@ -142,13 +185,13 @@ (Stop 'get-quotes (Role 'announce (list - (Shares (Struct 'book-of-the-month (list String))))))))) + (Shares (book-of-the-month String)))))))) (Reacts (¬Know (book-interest String String Bool)) (list)) (Reacts (Know (book-interest String String Bool)) (list)) (Reacts (¬Know (book-interest String String Bool)) (list)) (Reacts (Know (book-interest String String Bool)) (list))))))) - (Reacts (¬Know (Struct 'club-member (list String))) (list)) - (Reacts (Know (Struct 'club-member (list String))) (list))))) + (Reacts (¬Know (club-member String)) (list)) + (Reacts (Know (club-member String)) (list))))) (define leader-revised (Role @@ -176,14 +219,40 @@ (list (Stop 'get-quotes - (Role 'announce (list (Shares (Struct 'book-of-the-month (list String)))))) + (Role 'announce (list (Shares (book-of-the-month String))))) (list))))) (Reacts (¬Know (book-interest String String Bool)) (list)) (Reacts (Know (book-interest String String Bool)) (list)) (Reacts (¬Know (book-interest String String Bool)) (list)) (Reacts (Know (book-interest String String Bool)) (list))))))) - (Reacts (¬Know (Struct 'club-member (list String))) (list)) - (Reacts (Know (Struct 'club-member (list String))) (list))))) + (Reacts (¬Know (club-member String)) (list)) + (Reacts (Know (club-member String)) (list))))) + +(define member-spec + (Role + 'member + (list + (Shares (club-member String)) + (Reacts (Know (Observe (book-interest String ⋆ ⋆))) + (Role 'respond + (list + (Shares (book-interest String String Bool)))))))) + +(define member-actual + (Role + 'member41 + (list + (Shares (club-member String)) + (Reacts + (Know (Observe (book-interest String ⋆ ⋆))) + (Role + 'during-inner42 + (list + (Shares (book-interest String String Bool)) + (Reacts + (¬Know (Observe (book-interest String ⋆ ⋆))) + ;; this bit is a noticeable deviation from the spec + (Stop 'during-inner42 '())))))))) ;; ----------------------------------------------------------------------------- ;; Compiling Roles to state machines @@ -257,7 +326,7 @@ (define st0 (hash-ref seller# (set 'seller))) (define transitions (state-transitions st0)) (define quote-request - (Observe (Struct 'BookQuoteT (list String ⋆)))) + (Observe (book-quote String ⋆))) (check-true (hash-has-key? transitions (Know quote-request))) (check-equal? (hash-ref transitions (Know quote-request)) (set (set 'seller 'fulfill)))) @@ -586,7 +655,7 @@ (hash)) (define seller-txns (hash-ref desc 'seller)) (define quote-request - (Observe (Struct 'BookQuoteT (list String ⋆)))) + (Observe (book-quote String ⋆))) (check-true (hash-has-key? seller-txns (Know quote-request))) (check-equal? (hash-ref seller-txns (Know quote-request)) (set (list (start 'fulfill))))) @@ -911,7 +980,36 @@ (check-true (simulates? leader-fixed? leader-spec))) (test-case "things aren't quite right with leader-revised" - (check-false (simulates? leader-revised leader-spec)))) + (check-false (simulates? leader-revised leader-spec))) + (test-case + "things aren't quite right with member role" + (check-false (simulates? member-actual member-spec)) + (define member-actual/revised + (Role + 'member41 + (list + (Shares (club-member String)) + (Reacts + (Know (Observe (book-interest String ⋆ ⋆))) + (Role + 'during-inner42 + (list + (Shares (book-interest String String Bool)) + (Reacts + (¬Know (Observe (book-interest String ⋆ ⋆))) + ;; removed (Stop 'during-inner42 '()) here + '()))))))) + (check-true (simulates? member-actual/revised member-spec))) + (test-case + "things aren't quite right with seller role" + (check-false (simulates? seller-actual seller)) + (define seller-spec/revised + (Role 'seller + ;; change body to a During + (list + (During (Observe (book-quote String ⋆)) + (list (Shares (book-quote String Int))))))) + (check-true (simulates? seller-actual seller-spec/revised)))) ;; --------------------------------------------------------------------------- ;; Visualization