syndicate-lang
/
syndicate-2017
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Change type names Know -> Asserted, \negKnow -> Retracted

This commit is contained in:
Sam Caldwell 2019-06-13 08:34:34 -04:00
parent e0d1975e2d
commit cefe70c590
6 changed files with 138 additions and 138 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
racket/typed/core-types.rkt
View File

@ -202,8 +202,8 @@
(define-type-constructor Shares #:arity = 1) (define-type-constructor Shares #:arity = 1)
(define-type-constructor Sends #:arity = 1) (define-type-constructor Sends #:arity = 1)
(define-type-constructor Reacts #:arity >= 1) (define-type-constructor Reacts #:arity >= 1)
(define-type-constructor Know #:arity = 1) (define-type-constructor Asserted #:arity = 1)
(define-type-constructor ¬Know #:arity = 1) (define-type-constructor Retracted #:arity = 1)
(define-type-constructor Stop #:arity >= 1) (define-type-constructor Stop #:arity >= 1)
(define-type-constructor Field #:arity = 1) (define-type-constructor Field #:arity = 1)
(define-type-constructor Bind #:arity = 1) (define-type-constructor Bind #:arity = 1)
@ -762,8 +762,8 @@
;; EventDescriptorType -> Type ;; EventDescriptorType -> Type
(define-for-syntax (event-desc-type desc) (define-for-syntax (event-desc-type desc)
(syntax-parse desc (syntax-parse desc
[(~Know τ) #'τ] [(~Asserted τ) #'τ]
[(~¬Know τ) #'τ] [(~Retracted τ) #'τ]
[(~Message τ) desc] [(~Message τ) desc]
[_ (mk-U*- '())])) [_ (mk-U*- '())]))
@ -1023,10 +1023,10 @@
;; covers Start,Stop,Dataflow ;; covers Start,Stop,Dataflow
(type=? x y) (type=? x y)
(syntax-parse #`(#,x #,y) (syntax-parse #`(#,x #,y)
[((~Know τ1) (~Know τ2)) [((~Asserted τ1) (~Asserted τ2))
(<: (pattern-matching-assertions #'τ2) (<: (pattern-matching-assertions #'τ2)
(pattern-matching-assertions #'τ1))] (pattern-matching-assertions #'τ1))]
[((~¬Know τ1) (~¬Know τ2)) [((~Retracted τ1) (~Retracted τ2))
(<: (pattern-matching-assertions #'τ2) (<: (pattern-matching-assertions #'τ2)
(pattern-matching-assertions #'τ1))] (pattern-matching-assertions #'τ1))]
[((~Message τ1) (~Message τ2)) [((~Message τ1) (~Message τ2))

22
racket/typed/examples/roles/book-club.rkt
View File

@ -55,7 +55,7 @@
(define-type-alias seller-role (define-type-alias seller-role
(Role (seller) (Role (seller)
(Reacts (Know (Observe (BookQuoteT String ★/t))) (Reacts (Asserted (Observe (BookQuoteT String ★/t)))
(Role (_) (Role (_)
;; nb no mention of retracting this assertion ;; nb no mention of retracting this assertion
(Shares (BookQuoteT String Int)))))) (Shares (BookQuoteT String Int))))))
@ -73,9 +73,9 @@
(define-type-alias leader-role (define-type-alias leader-role
(Role (leader) (Role (leader)
(Reacts (Know (BookQuoteT String Int)) (Reacts (Asserted (BookQuoteT String Int))
(Role (poll) (Role (poll)
(Reacts (Know (BookInterestT String String Bool)) (Reacts (Asserted (BookInterestT String String Bool))
;; this is actually implemented indirectly through dataflow ;; this is actually implemented indirectly through dataflow
(U (Stop leader (U (Stop leader
(Role (_) (Role (_)
@ -84,7 +84,7 @@
(define-type-alias leader-actual (define-type-alias leader-actual
(Role (get-quotes31) (Role (get-quotes31)
(Reacts (Know (BookQuoteT String (Bind Int))) (Reacts (Asserted (BookQuoteT String (Bind Int)))
(Stop get-quotes) (Stop get-quotes)
(Role (poll-members36) (Role (poll-members36)
(Reacts OnDataflow (Reacts OnDataflow
@ -93,12 +93,12 @@
(Stop get-quotes (Stop get-quotes
(Role (announce39) (Role (announce39)
(Shares (BookOfTheMonthT String))))) (Shares (BookOfTheMonthT String)))))
(Reacts (¬Know (BookInterestT String (Bind String) Bool))) (Reacts (Retracted (BookInterestT String (Bind String) Bool)))
(Reacts (Know (BookInterestT String (Bind String) Bool))) (Reacts (Asserted (BookInterestT String (Bind String) Bool)))
(Reacts (¬Know (BookInterestT String (Bind String) Bool))) (Reacts (Retracted (BookInterestT String (Bind String) Bool)))
(Reacts (Know (BookInterestT String (Bind String) Bool))))) (Reacts (Asserted (BookInterestT String (Bind String) Bool)))))
(Reacts (¬Know (ClubMemberT (Bind String)))) (Reacts (Retracted (ClubMemberT (Bind String))))
(Reacts (Know (ClubMemberT (Bind String)))))) (Reacts (Asserted (ClubMemberT (Bind String))))))
(define (spawn-leader [titles : (List String)]) (define (spawn-leader [titles : (List String)])
(spawn τc (spawn τc
@ -160,7 +160,7 @@
(Role (member) (Role (member)
(Shares (ClubMemberT String)) (Shares (ClubMemberT String))
;; should this be the type of the pattern? or lowered to concrete types? ;; should this be the type of the pattern? or lowered to concrete types?
(Reacts (Know (Observe (BookInterestT String ★/t ★/t))) (Reacts (Asserted (Observe (BookInterestT String ★/t ★/t)))
(Role (_) (Role (_)
(Shares (BookInterestT String String Bool)))))) (Shares (BookInterestT String String Bool))))))

2
racket/typed/examples/roles/flink.rkt
View File

@ -116,7 +116,7 @@ TaskRunners.
(Role (assign) (Role (assign)
(Shares (TaskAssignment ID ID ConcreteTask)) (Shares (TaskAssignment ID ID ConcreteTask))
;; would be nice to say how the IDs relate to each other (first two are the same) ;; would be nice to say how the IDs relate to each other (first two are the same)
(Reacts (Know (TaskState ID ID TaskID ★/t)) (Reacts (Asserted (TaskState ID ID TaskID ★/t))
(Branch (Stop assign) (Branch (Stop assign)
(Effs))))) (Effs)))))

2
racket/typed/examples/roles/two-buyer-protocol.rkt
View File

@ -62,7 +62,7 @@
(define-type-alias seller-role (define-type-alias seller-role
(Role (seller) (Role (seller)
(Reacts (Know (Observe (QuoteT String ★/t))) (Reacts (Asserted (Observe (QuoteT String ★/t)))
(Role (_) (Role (_)
(Shares (QuoteT String Int)))))) (Shares (QuoteT String Int))))))

228
racket/typed/proto.rkt
View File

@ -33,13 +33,13 @@
(struct Branch (arms) #:transparent) (struct Branch (arms) #:transparent)
;; a D is one of ;; a D is one of
;; - (Know τ), reaction to assertion ;; - (Asserted τ), reaction to assertion
;; - (¬Know τ), reaction to retraction ;; - (Retracted τ), reaction to retraction
;; - StartEvt, reaction to facet startup ;; - StartEvt, reaction to facet startup
;; - StopEvt, reaction to facet shutdown ;; - StopEvt, reaction to facet shutdown
;; - DataflowEvt, reaction to field updates ;; - DataflowEvt, reaction to field updates
(struct Know (ty) #:transparent) (struct Asserted (ty) #:transparent)
(struct ¬Know (ty) #:transparent) (struct Retracted (ty) #:transparent)
(define StartEvt 'Start) (define StartEvt 'Start)
(define StopEvt 'Stop) (define StopEvt 'Stop)
(define DataflowEvt 'Dataflow) (define DataflowEvt 'Dataflow)
@ -76,9 +76,9 @@
;; τ (Listof EP) -> EP ;; τ (Listof EP) -> EP
(define (During assertion eps) (define (During assertion eps)
(define facet-name (gensym 'during-inner)) (define facet-name (gensym 'during-inner))
(Reacts (Know assertion) (Reacts (Asserted assertion)
(Role facet-name (Role facet-name
(cons (Reacts (¬Know assertion) (cons (Reacts (Retracted assertion)
(Stop facet-name '())) (Stop facet-name '()))
eps)))) eps))))
@ -88,10 +88,10 @@
(define manager (define manager
(Role 'account-manager (Role 'account-manager
(list (Shares (Struct 'account (list Int))) (list (Shares (Struct 'account (list Int)))
(Reacts (Know (Struct 'deposit '())) '())))) (Reacts (Asserted (Struct 'deposit '())) '()))))
(define client (define client
(Role 'client (Role 'client
(list (Reacts (Know (Struct 'account (list Int))) '())))) (list (Reacts (Asserted (Struct 'account (list Int))) '()))))
;; τ τ -> τ ;; τ τ -> τ
;; short hand for creating a book quote struct type ;; short hand for creating a book quote struct type
@ -116,7 +116,7 @@
(define seller (define seller
(Role 'seller (Role 'seller
(list (list
(Reacts (Know (Observe (book-quote String ⋆))) (Reacts (Asserted (Observe (book-quote String ⋆)))
(Role 'fulfill (Role 'fulfill
(list (Shares (book-quote String Int)))))))) (list (Shares (book-quote String Int))))))))
@ -125,24 +125,24 @@
'seller27 'seller27
(list (list
(Reacts (Reacts
(Know (Observe (book-quote String ⋆))) (Asserted (Observe (book-quote String ⋆)))
(Role (Role
'during-inner29 'during-inner29
(list (list
(Shares (book-quote String (U (list Int Int)))) (Shares (book-quote String (U (list Int Int))))
(Reacts (Reacts
(¬Know (Observe (book-quote String ⋆))) (Retracted (Observe (book-quote String ⋆)))
(Stop 'during-inner29 '())))))))) (Stop 'during-inner29 '()))))))))
(define leader-spec (define leader-spec
(Role 'leader (Role 'leader
(list (list
(Reacts (Reacts
(Know (book-quote String Int)) (Asserted (book-quote String Int))
(Role 'poll (Role 'poll
(list (list
(Reacts (Reacts
(Know (book-interest String String Bool)) (Asserted (book-interest String String Bool))
(Branch (Branch
(list (list
(Stop 'leader (Stop 'leader
@ -156,7 +156,7 @@
'get-quotes 'get-quotes
(list (list
(Reacts (Reacts
(Know (book-quote String Int)) (Asserted (book-quote String Int))
(Branch (Branch
(list (list
;; problem 1: spec doesn't say actor can give up when running out of books ;; problem 1: spec doesn't say actor can give up when running out of books
@ -165,7 +165,7 @@
'poll-members 'poll-members
(list (list
(Reacts (Reacts
(Know (book-interest String String ⋆)) (Asserted (book-interest String String ⋆))
(Branch (list (Branch (list
;; problem 2: combining poll-members and get-quotes here (should be another branch) ;; problem 2: combining poll-members and get-quotes here (should be another branch)
(Stop 'poll-members (Stop 'poll-members
@ -174,21 +174,21 @@
(Role 'announce (Role 'announce
(list (list
(Shares (book-of-the-month String)))))))) (Shares (book-of-the-month String))))))))
(Reacts (¬Know (book-interest String String Bool)) (list)) (Reacts (Retracted (book-interest String String Bool)) (list))
(Reacts (Know (book-interest String String Bool)) (list)) (Reacts (Asserted (book-interest String String Bool)) (list))
(Reacts (¬Know (book-interest String String Bool)) (list)) (Reacts (Retracted (book-interest String String Bool)) (list))
(Reacts (Know (book-interest String String Bool)) (list))))))) (Reacts (Asserted (book-interest String String Bool)) (list)))))))
(Reacts (¬Know (club-member String)) (list)) (Reacts (Retracted (club-member String)) (list))
(Reacts (Know (club-member String)) (list))))) (Reacts (Asserted (club-member String)) (list)))))
(define leader-fixed? (define leader-fixed?
(Role 'get-quotes (Role 'get-quotes
(list (list
(Reacts (Know (book-quote String Int)) (Reacts (Asserted (book-quote String Int))
(Branch (list (Branch (list
(Role 'poll-members (Role 'poll-members
(list (list
(Reacts (Know (book-interest String String ⋆)) (Reacts (Asserted (book-interest String String ⋆))
(Branch (list (Branch (list
(Stop 'poll-members (Stop 'poll-members
'()) '())
@ -196,19 +196,19 @@
(Role 'announce (Role 'announce
(list (list
(Shares (book-of-the-month String)))))))) (Shares (book-of-the-month String))))))))
(Reacts (¬Know (book-interest String String Bool)) (list)) (Reacts (Retracted (book-interest String String Bool)) (list))
(Reacts (Know (book-interest String String Bool)) (list)) (Reacts (Asserted (book-interest String String Bool)) (list))
(Reacts (¬Know (book-interest String String Bool)) (list)) (Reacts (Retracted (book-interest String String Bool)) (list))
(Reacts (Know (book-interest String String Bool)) (list))))))) (Reacts (Asserted (book-interest String String Bool)) (list)))))))
(Reacts (¬Know (club-member String)) (list)) (Reacts (Retracted (club-member String)) (list))
(Reacts (Know (club-member String)) (list))))) (Reacts (Asserted (club-member String)) (list)))))
(define leader-revised (define leader-revised
(Role (Role
'get-quotes 'get-quotes
(list (list
(Reacts (Reacts
(Know (book-quote String Int)) (Asserted (book-quote String Int))
(Branch (Branch
(list (list
(Branch (list (Stop 'get-quotes (list)) (list))) (Branch (list (Stop 'get-quotes (list)) (list)))
@ -216,7 +216,7 @@
'poll-members 'poll-members
(list (list
(Reacts (Reacts
(Know (book-interest String String ⋆)) (Asserted (book-interest String String ⋆))
(list (list
(Branch (Branch
(list (list
@ -231,19 +231,19 @@
'get-quotes 'get-quotes
(Role 'announce (list (Shares (book-of-the-month String))))) (Role 'announce (list (Shares (book-of-the-month String)))))
(list))))) (list)))))
(Reacts (¬Know (book-interest String String Bool)) (list)) (Reacts (Retracted (book-interest String String Bool)) (list))
(Reacts (Know (book-interest String String Bool)) (list)) (Reacts (Asserted (book-interest String String Bool)) (list))
(Reacts (¬Know (book-interest String String Bool)) (list)) (Reacts (Retracted (book-interest String String Bool)) (list))
(Reacts (Know (book-interest String String Bool)) (list))))))) (Reacts (Asserted (book-interest String String Bool)) (list)))))))
(Reacts (¬Know (club-member String)) (list)) (Reacts (Retracted (club-member String)) (list))
(Reacts (Know (club-member String)) (list))))) (Reacts (Asserted (club-member String)) (list)))))
(define member-spec (define member-spec
(Role (Role
'member 'member
(list (list
(Shares (club-member String)) (Shares (club-member String))
(Reacts (Know (Observe (book-interest String ⋆ ⋆))) (Reacts (Asserted (Observe (book-interest String ⋆ ⋆)))
(Role 'respond (Role 'respond
(list (list
(Shares (book-interest String String Bool)))))))) (Shares (book-interest String String Bool))))))))
@ -254,13 +254,13 @@
(list (list
(Shares (club-member String)) (Shares (club-member String))
(Reacts (Reacts
(Know (Observe (book-interest String ⋆ ⋆))) (Asserted (Observe (book-interest String ⋆ ⋆)))
(Role (Role
'during-inner42 'during-inner42
(list (list
(Shares (book-interest String String Bool)) (Shares (book-interest String String Bool))
(Reacts (Reacts
(¬Know (Observe (book-interest String ⋆ ⋆))) (Retracted (Observe (book-interest String ⋆ ⋆)))
;; this bit is a noticeable deviation from the spec ;; this bit is a noticeable deviation from the spec
(Stop 'during-inner42 '())))))))) (Stop 'during-inner42 '()))))))))
@ -328,8 +328,8 @@
;; test if D corresponds to an external event (assertion, message) ;; test if D corresponds to an external event (assertion, message)
(define (external-evt? D) (define (external-evt? D)
(match D (match D
[(or (Know _) [(or (Asserted _)
(¬Know _)) (Retracted _))
#t] #t]
[(== DataflowEvt) [(== DataflowEvt)
#t] #t]
@ -352,14 +352,14 @@
(define transitions (state-transitions st0)) (define transitions (state-transitions st0))
(define quote-request (define quote-request
(Observe (book-quote String ⋆))) (Observe (book-quote String ⋆)))
(check-true (hash-has-key? transitions (Know quote-request))) (check-true (hash-has-key? transitions (Asserted quote-request)))
(check-equal? (hash-ref transitions (Know quote-request)) (check-equal? (hash-ref transitions (Asserted quote-request))
(set (set 'seller 'fulfill)))) (set (set 'seller 'fulfill))))
(test-case (test-case
"compile role that quits" "compile role that quits"
(define r (define r
(Role 'x (Role 'x
(list (Reacts (Know Int) (list (Reacts (Asserted Int)
(Stop 'x '()))))) (Stop 'x '())))))
(define rg (compile r)) (define rg (compile r))
(check-true (role-graph? rg)) (check-true (role-graph? rg))
@ -370,8 +370,8 @@
(check-true (hash-has-key? state# (set 'x))) (check-true (hash-has-key? state# (set 'x)))
(define state0 (hash-ref state# (set 'x))) (define state0 (hash-ref state# (set 'x)))
(define transitions (state-transitions state0)) (define transitions (state-transitions state0))
(check-true (hash-has-key? transitions (Know Int))) (check-true (hash-has-key? transitions (Asserted Int)))
(check-equal? (hash-ref transitions (Know Int)) (check-equal? (hash-ref transitions (Asserted Int))
(set (set)))) (set (set))))
(test-case (test-case
@ -384,7 +384,7 @@
(define gq-st (hash-ref state# (set 'get-quotes))) (define gq-st (hash-ref state# (set 'get-quotes)))
(check-true (state? gq-st)) (check-true (state? gq-st))
(match-define (state _ gq-transitions) gq-st) (match-define (state _ gq-transitions) gq-st)
(define bq (Know (book-quote String Int))) (define bq (Asserted (book-quote String Int)))
(check-true (hash? gq-transitions)) (check-true (hash? gq-transitions))
(check-true (hash-has-key? gq-transitions bq)) (check-true (hash-has-key? gq-transitions bq))
(define dests (hash-ref gq-transitions bq)) (define dests (hash-ref gq-transitions bq))
@ -394,7 +394,7 @@
(define gqpm-st (hash-ref state# (set 'get-quotes 'poll-members))) (define gqpm-st (hash-ref state# (set 'get-quotes 'poll-members)))
(check-true (state? gqpm-st)) (check-true (state? gqpm-st))
(match-define (state _ gqpm-transitions) gqpm-st) (match-define (state _ gqpm-transitions) gqpm-st)
(define bi (Know (book-interest String String ⋆))) (define bi (Asserted (book-interest String String ⋆)))
(check-true (hash? gqpm-transitions)) (check-true (hash? gqpm-transitions))
(check-true (hash-has-key? gqpm-transitions bi)) (check-true (hash-has-key? gqpm-transitions bi))
(define dests2 (hash-ref gqpm-transitions bi)) (define dests2 (hash-ref gqpm-transitions bi))
@ -408,7 +408,7 @@
'poll-members 'poll-members
(list (list
(Reacts (Reacts
(Know (book-interest String String ⋆)) (Asserted (book-interest String String ⋆))
(list (list
(Branch (Branch
(list (list
@ -419,7 +419,7 @@
(list)))))))) (list))))))))
(define transition# (describe-role poll/simpl)) (define transition# (describe-role poll/simpl))
(check-true (hash? transition#)) (check-true (hash? transition#))
(define bi (Know (book-interest String String ⋆))) (define bi (Asserted (book-interest String String ⋆)))
(check-true (hash-has-key? transition# bi)) (check-true (hash-has-key? transition# bi))
(define effs (hash-ref transition# bi)) (define effs (hash-ref transition# bi))
(check-true (set? effs)) (check-true (set? effs))
@ -756,14 +756,14 @@
(define seller-txns (hash-ref desc 'seller)) (define seller-txns (hash-ref desc 'seller))
(define quote-request (define quote-request
(Observe (book-quote String ⋆))) (Observe (book-quote String ⋆)))
(check-true (hash-has-key? seller-txns (Know quote-request))) (check-true (hash-has-key? seller-txns (Asserted quote-request)))
(check-equal? (hash-ref seller-txns (Know quote-request)) (check-equal? (hash-ref seller-txns (Asserted quote-request))
(set (list (start 'fulfill))))) (set (list (start 'fulfill)))))
(test-case (test-case
"describe-roles bug" "describe-roles bug"
(define role (Role 'poll (define role (Role 'poll
(list (list
(Reacts (Know Int) (Reacts (Asserted Int)
(Branch (Branch
(list (Stop 'leader (Role 'announce (list (Shares Int)))) (list (Stop 'leader (Role 'announce (list (Shares Int))))
(Stop 'poll (list)))))))) (Stop 'poll (list))))))))
@ -771,8 +771,8 @@
(check-true (hash? desc)) (check-true (hash? desc))
(check-true (hash-has-key? desc 'poll)) (check-true (hash-has-key? desc 'poll))
(define txns (hash-ref desc 'poll)) (define txns (hash-ref desc 'poll))
(check-true (hash-has-key? txns (Know Int))) (check-true (hash-has-key? txns (Asserted Int)))
(check-equal? (hash-ref txns (Know Int)) (check-equal? (hash-ref txns (Asserted Int))
(set (list (stop 'leader) (start 'announce)) (set (list (stop 'leader) (start 'announce))
(list (stop 'poll))))) (list (stop 'poll)))))
(test-case (test-case
@ -786,7 +786,7 @@
(define desc (describe-roles leader-spec)) (define desc (describe-roles leader-spec))
(check-true (hash-has-key? desc 'poll)) (check-true (hash-has-key? desc 'poll))
(define poll-txns (hash-ref desc 'poll)) (define poll-txns (hash-ref desc 'poll))
(define evt (Know (book-interest String String Bool))) (define evt (Asserted (book-interest String String Bool)))
(check-true (hash-has-key? poll-txns evt)) (check-true (hash-has-key? poll-txns evt))
(define effs (hash-ref poll-txns evt)) (define effs (hash-ref poll-txns evt))
(check-true (set-member? effs (list (stop 'poll)))))) (check-true (set-member? effs (list (stop 'poll))))))
@ -910,9 +910,9 @@
;; TODO - sketchy, intuition "dataflow can happen at any time", though it ;; TODO - sketchy, intuition "dataflow can happen at any time", though it
;; might actually take the place of multiple transitions ;; might actually take the place of multiple transitions
#t] #t]
[(list (Know τ1) (Know τ2)) [(list (Asserted τ1) (Asserted τ2))
(<:? τ1 τ2)] (<:? τ1 τ2)]
[(list (¬Know τ1) (¬Know τ2)) [(list (Retracted τ1) (Retracted τ2))
(<:? τ1 τ2)] (<:? τ1 τ2)]
[(list (== StartEvt) (== StartEvt)) [(list (== StartEvt) (== StartEvt))
#t] #t]
@ -939,8 +939,8 @@
τ] τ]
[(Reacts D _) [(Reacts D _)
(match D (match D
[(or (Know τ) [(or (Asserted τ)
(¬Know τ)) (Retracted τ))
;; TODO - this doesn't put ⋆ in where an underlying pattern uses a capture ;; TODO - this doesn't put ⋆ in where an underlying pattern uses a capture
(Observe τ)] (Observe τ)]
[_ [_
@ -948,9 +948,9 @@
(module+ test (module+ test
;; make sure the or pattern above works the way I think it does ;; make sure the or pattern above works the way I think it does
(check-equal? (EP-assertion (Reacts (Know Int) #f)) (check-equal? (EP-assertion (Reacts (Asserted Int) #f))
(Observe Int)) (Observe Int))
(check-equal? (EP-assertion (Reacts (¬Know String) #f)) (check-equal? (EP-assertion (Reacts (Retracted String) #f))
(Observe String))) (Observe String)))
;; an Equation is (equiv StateName StateName) ;; an Equation is (equiv StateName StateName)
@ -1191,13 +1191,13 @@
(list (list
(Shares (club-member String)) (Shares (club-member String))
(Reacts (Reacts
(Know (Observe (book-interest String ⋆ ⋆))) (Asserted (Observe (book-interest String ⋆ ⋆)))
(Role (Role
'during-inner42 'during-inner42
(list (list
(Shares (book-interest String String Bool)) (Shares (book-interest String String Bool))
(Reacts (Reacts
(¬Know (Observe (book-interest String ⋆ ⋆))) (Retracted (Observe (book-interest String ⋆ ⋆)))
;; removed (Stop 'during-inner42 '()) here ;; removed (Stop 'during-inner42 '()) here
'()))))))) '())))))))
(check-true (simulates? member-actual/revised member-spec))) (check-true (simulates? member-actual/revised member-spec)))
@ -1248,7 +1248,7 @@
[txn# (in-value (state-transitions st))] [txn# (in-value (state-transitions st))]
[D (in-hash-keys txn#)]) [D (in-hash-keys txn#)])
(match D (match D
[(or (Know τ) (¬Know τ)) [(or (Asserted τ) (Retracted τ))
τ] τ]
[_ D]))) [_ D])))
(in-generator (in-generator
@ -1261,8 +1261,8 @@
(define (event-enabled? D) (define (event-enabled? D)
(for/or ([e (in-set event-set)]) (for/or ([e (in-set event-set)])
(or (equal? DataflowEvt e) (or (equal? DataflowEvt e)
(D<:? D (Know e)) (D<:? D (Asserted e))
(D<:? D (¬Know e))))) (D<:? D (Retracted e)))))
(define st# (define st#
(for/hash ([st (in-list states*)]) (for/hash ([st (in-list states*)])
(define orig-txn# (state-transitions (hash-ref state# st))) (define orig-txn# (state-transitions (hash-ref state# st)))
@ -1312,10 +1312,10 @@
"reachable states" "reachable states"
(define rg (define rg
(role-graph (set 'X 'Y 'Z) (role-graph (set 'X 'Y 'Z)
(hash (set 'X 'Y 'Z) (state (set 'X 'Y 'Z) (hash (Know Int) (set (set 'X 'Y 'Z)) (hash (set 'X 'Y 'Z) (state (set 'X 'Y 'Z) (hash (Asserted Int) (set (set 'X 'Y 'Z))
(¬Know Int) (set (set 'X 'Y)))) (Retracted Int) (set (set 'X 'Y))))
(set 'X) (state (set 'X) '#hash()) (set 'X) (state (set 'X) '#hash())
(set 'X 'Y) (state (set 'X 'Y) (hash (Know Int) (set (set 'X 'Y 'Z))))))) (set 'X 'Y) (state (set 'X 'Y) (hash (Asserted Int) (set (set 'X 'Y 'Z)))))))
(define reachable (reachable-states rg)) (define reachable (reachable-states rg))
(check-true (set-member? reachable (set 'X 'Y 'Z))) (check-true (set-member? reachable (set 'X 'Y 'Z)))
(check-true (set-member? reachable (set 'X 'Y))) (check-true (set-member? reachable (set 'X 'Y)))
@ -1330,9 +1330,9 @@
(state (state
(set 'during-inner2 'during-inner1 'tm) (set 'during-inner2 'during-inner1 'tm)
(hash (hash
(Know (Struct 'TaskAssignment (list))) (Asserted (Struct 'TaskAssignment (list)))
(set (set 'during-inner2 'during-inner1 'tm)) (set (set 'during-inner2 'during-inner1 'tm))
(¬Know (Struct 'TaskAssignment (list))) (Retracted (Struct 'TaskAssignment (list)))
(set (set 'during-inner1 'tm)))) (set (set 'during-inner1 'tm))))
(set 'tm) (set 'tm)
(state (set 'tm) '#hash()) (state (set 'tm) '#hash())
@ -1340,7 +1340,7 @@
(state (state
(set 'during-inner1 'tm) (set 'during-inner1 'tm)
(hash (hash
(Know (Struct 'TaskAssignment (list))) (Asserted (Struct 'TaskAssignment (list)))
(set (set 'during-inner2 'during-inner1 'tm))))))) (set (set 'during-inner2 'during-inner1 'tm)))))))
(define reachable (reachable-states rg)) (define reachable (reachable-states rg))
(check-true (set-member? reachable (set 'during-inner2 'during-inner1 'tm))) (check-true (set-member? reachable (set 'during-inner2 'during-inner1 'tm)))
@ -1356,7 +1356,7 @@
[txn# (in-value (state-transitions st))] [txn# (in-value (state-transitions st))]
[D (in-hash-keys txn#)]) [D (in-hash-keys txn#)])
(match D (match D
[(or (Know τ) (¬Know τ)) [(or (Asserted τ) (Retracted τ))
τ] τ]
[_ D]))) [_ D])))
@ -1416,9 +1416,9 @@
;; give a description of an event suitable for rendering ;; give a description of an event suitable for rendering
(define (D->label evt) (define (D->label evt)
(match evt (match evt
[(Know τ) [(Asserted τ)
(string-append "+" (τ->string τ))] (string-append "+" (τ->string τ))]
[(¬Know τ) [(Retracted τ)
(string-append "-" (τ->string τ))] (string-append "-" (τ->string τ))]
[(== StartEvt) [(== StartEvt)
"Start"] "Start"]
@ -1497,10 +1497,10 @@
(define (parse-D d) (define (parse-D d)
(match d (match d
[(list 'Know t) [(list 'Asserted t)
(Know (parse-τ t))] (Asserted (parse-τ t))]
[(list '¬Know t) [(list 'Retracted t)
(¬Know (parse-τ t))] (Retracted (parse-τ t))]
['OnStart ['OnStart
StartEvt] StartEvt]
['OnStop ['OnStop
@ -1565,12 +1565,12 @@
'(Role '(Role
(seller) (seller)
(Reacts (Reacts
(Know (Observe (BookQuoteT (Bind String) Discard))) (Asserted (Observe (BookQuoteT (Bind String) Discard)))
(Role (Role
(during-inner) (during-inner)
(Shares (BookQuoteT String Int)) (Shares (BookQuoteT String Int))
(Reacts (Reacts
(¬Know (Observe (BookQuoteT String Discard))) (Retracted (Observe (BookQuoteT String Discard)))
(Stop during-inner)))))) (Stop during-inner))))))
(define real-member-ty (define real-member-ty
@ -1578,26 +1578,26 @@
(member) (member)
(Shares (ClubMemberT String)) (Shares (ClubMemberT String))
(Reacts (Reacts
(Know (Observe (BookInterestT (Bind String) Discard Discard))) (Asserted (Observe (BookInterestT (Bind String) Discard Discard)))
(Role (Role
(during-inner) (during-inner)
(Shares (BookInterestT String String Bool)) (Shares (BookInterestT String String Bool))
(Reacts (Reacts
(¬Know (Observe (BookInterestT String Discard Discard))) (Retracted (Observe (BookInterestT String Discard Discard)))
(Stop during-inner)))))) (Stop during-inner))))))
(define real-leader-ty (define real-leader-ty
'(Role '(Role
(get-quotes) (get-quotes)
(Reacts (Reacts
(Know (BookQuoteT String (Bind Int))) (Asserted (BookQuoteT String (Bind Int)))
(Branch (Branch
(Effs (Branch (Effs (Stop get-quotes)) (Effs))) (Effs (Branch (Effs (Stop get-quotes)) (Effs)))
(Effs (Effs
(Role (Role
(poll-members) (poll-members)
(Reacts (Reacts
(Know (BookInterestT String (Bind String) Discard)) (Asserted (BookInterestT String (Bind String) Discard))
(Branch (Branch
(Effs (Stop poll-members (Branch (Effs (Stop get-quotes)) (Effs)))) (Effs (Stop poll-members (Branch (Effs (Stop get-quotes)) (Effs))))
(Effs)) (Effs))
@ -1605,12 +1605,12 @@
(Effs (Effs
(Stop get-quotes (Role (announce) (Shares (BookOfTheMonthT String))))) (Stop get-quotes (Role (announce) (Shares (BookOfTheMonthT String)))))
(Effs))) (Effs)))
(Reacts (¬Know (BookInterestT String (Bind String) Bool))) (Reacts (Retracted (BookInterestT String (Bind String) Bool)))
(Reacts (Know (BookInterestT String (Bind String) Bool))) (Reacts (Asserted (BookInterestT String (Bind String) Bool)))
(Reacts (¬Know (BookInterestT String (Bind String) Bool))) (Reacts (Retracted (BookInterestT String (Bind String) Bool)))
(Reacts (Know (BookInterestT String (Bind String) Bool))))))) (Reacts (Asserted (BookInterestT String (Bind String) Bool)))))))
(Reacts (¬Know (ClubMemberT (Bind String)))) (Reacts (Retracted (ClubMemberT (Bind String))))
(Reacts (Know (ClubMemberT (Bind String)))))) (Reacts (Asserted (ClubMemberT (Bind String))))))
;; --------------------------------------------------------------------------- ;; ---------------------------------------------------------------------------
;; Flink Examples ;; Flink Examples
@ -1620,7 +1620,7 @@
(jm) (jm)
(Shares (JobManagerAlive)) (Shares (JobManagerAlive))
(Reacts (Reacts
(Know (Asserted
(Job (Job
(Bind Symbol) (Bind Symbol)
(Bind (List (Task Int (U (MapWork String) (ReduceWork Int Int))))))) (Bind (List (Task Int (U (MapWork String) (ReduceWork Int Int)))))))
@ -1652,7 +1652,7 @@
(MapWork String) (MapWork String)
(ReduceWork (Hash String Int) (Hash String Int)))))) (ReduceWork (Hash String Int) (Hash String Int))))))
(Reacts (Reacts
(Know (Asserted
(TaskState (TaskState
Symbol Symbol
Symbol Symbol
@ -1676,21 +1676,21 @@
(Role (Role
(take-slot) (take-slot)
(Reacts (Reacts
(Know (TaskState Symbol Symbol Int Discard)) (Asserted (TaskState Symbol Symbol Int Discard))
(Stop take-slot)))) (Stop take-slot))))
(Reacts (¬Know (TaskManager Symbol Discard)) (Stop assign)))) (Reacts (Retracted (TaskManager Symbol Discard)) (Stop assign))))
(Effs))) (Effs)))
(Effs))))) (Effs)))))
(Reacts OnStop) (Reacts OnStop)
(Reacts OnStart))) (Reacts OnStart)))
(Reacts (Reacts
(¬Know (Retracted
(Job (Job
Symbol Symbol
(List (Task Int (U (MapWork String) (ReduceWork Int Int)))))) (List (Task Int (U (MapWork String) (ReduceWork Int Int))))))
(Stop during-inner)))) (Stop during-inner))))
(Reacts (¬Know (TaskManager (Bind Symbol) (Bind Int)))) (Reacts (Retracted (TaskManager (Bind Symbol) (Bind Int))))
(Reacts (Know (TaskManager (Bind Symbol) (Bind Int)))))) (Reacts (Asserted (TaskManager (Bind Symbol) (Bind Int))))))
(module+ test (module+ test
(test-case (test-case
@ -1705,7 +1705,7 @@
'(Role '(Role
(listen) (listen)
(Reacts (Reacts
(Know (Asserted
(TaskAssignment (TaskAssignment
Symbol Symbol
Symbol Symbol
@ -1717,7 +1717,7 @@
(Role (Role
(during-inner) (during-inner)
(Reacts (Reacts
(¬Know (Retracted
(TaskAssignment (TaskAssignment
Symbol Symbol
Symbol Symbol
@ -1744,7 +1744,7 @@
(runner) (runner)
(Shares (TaskRunner Symbol (U (Executing Int) Symbol))) (Shares (TaskRunner Symbol (U (Executing Int) Symbol)))
(Reacts (Reacts
(Know (Asserted
(TaskAssignment (TaskAssignment
Symbol Symbol
(Bind Symbol) (Bind Symbol)
@ -1759,7 +1759,7 @@
(Shares (Shares
(TaskState Symbol Symbol Int (U (Finished (Hash String Int)) Symbol))) (TaskState Symbol Symbol Int (U (Finished (Hash String Int)) Symbol)))
(Reacts (Reacts
(¬Know (Retracted
(TaskAssignment (TaskAssignment
Symbol Symbol
Symbol Symbol
@ -1791,7 +1791,7 @@
(MapWork String) (MapWork String)
(ReduceWork (Hash String Int) (Hash String Int)))))) (ReduceWork (Hash String Int) (Hash String Int))))))
(Reacts (Reacts
(Know (TaskState Symbol Symbol Int ★/t)) (Asserted (TaskState Symbol Symbol Int ★/t))
()))) ())))
(module+ test (module+ test
@ -1803,12 +1803,12 @@
'(Role '(Role
(tm) (tm)
(Reacts (Reacts
(Know (JobManagerAlive)) (Asserted (JobManagerAlive))
(Role (Role
(during-inner1) (during-inner1)
(Shares (TaskManager Symbol Int)) (Shares (TaskManager Symbol Int))
(Reacts (Reacts
(Know (Asserted
(TaskAssignment (TaskAssignment
Symbol Symbol
(Bind Symbol) (Bind Symbol)
@ -1832,7 +1832,7 @@
(Shares (Shares
(TaskState Symbol Symbol Int (U (Finished (Hash String Int)) Symbol))) (TaskState Symbol Symbol Int (U (Finished (Hash String Int)) Symbol)))
(Reacts (Reacts
(Know (Asserted
(TaskState (TaskState
Symbol Symbol
Symbol Symbol
@ -1840,7 +1840,7 @@
(Bind (U (Finished (Hash String Int)) Symbol))))) (Bind (U (Finished (Hash String Int)) Symbol)))))
(Reacts OnStop) (Reacts OnStop)
(Reacts (Reacts
(¬Know (Retracted
(TaskAssignment (TaskAssignment
Symbol Symbol
Symbol Symbol
@ -1850,11 +1850,11 @@
(MapWork String) (MapWork String)
(ReduceWork (Hash String Int) (Hash String Int)))))) (ReduceWork (Hash String Int) (Hash String Int))))))
(Stop during-inner2)))) (Stop during-inner2))))
(Reacts (¬Know (TaskRunner (Bind Symbol) (U (Executing Int) Symbol)))) (Reacts (Retracted (TaskRunner (Bind Symbol) (U (Executing Int) Symbol))))
(Reacts (Know (TaskRunner (Bind Symbol) (U (Executing Int) Symbol)))) (Reacts (Asserted (TaskRunner (Bind Symbol) (U (Executing Int) Symbol))))
(Reacts (¬Know (TaskRunner (Bind Symbol) Discard))) (Reacts (Retracted (TaskRunner (Bind Symbol) Discard)))
(Reacts (Know (TaskRunner (Bind Symbol) Discard))) (Reacts (Asserted (TaskRunner (Bind Symbol) Discard)))
(Reacts (¬Know (JobManagerAlive)) (Stop during-inner1)))))) (Reacts (Retracted (JobManagerAlive)) (Stop during-inner1))))))
(module+ test (module+ test
(test-case "parse and compile task-manager-ty" (test-case "parse and compile task-manager-ty"

10
racket/typed/roles.rkt
View File

@ -9,7 +9,7 @@
run-ground-dataspace run-ground-dataspace
;; Types ;; Types
Tuple Bind Discard → ∀ Tuple Bind Discard → ∀
Role Reacts Shares Know ¬Know Message OnDataflow Stop OnStart OnStop Role Reacts Shares Asserted Retracted Message OnDataflow Stop OnStart OnStop
Branch Effs Branch Effs
FacetName Field ★/t FacetName Field ★/t
Observe Inbound Outbound Actor U ⊥ Observe Inbound Outbound Actor U ⊥
@ -186,10 +186,10 @@
#:datum-literals (asserted retracted message) #:datum-literals (asserted retracted message)
(pattern (~or (~and asserted (pattern (~or (~and asserted
(~bind [syndicate-kw #'syndicate:asserted] (~bind [syndicate-kw #'syndicate:asserted]
[react-con #'Know])) [react-con #'Asserted]))
(~and retracted (~and retracted
(~bind [syndicate-kw #'syndicate:retracted] (~bind [syndicate-kw #'syndicate:retracted]
[react-con #'¬Know])) [react-con #'Retracted]))
(~and message (~and message
(~bind [syndicate-kw #'syndicate:message] (~bind [syndicate-kw #'syndicate:message]
[react-con #'Message]))))) [react-con #'Message])))))
@ -340,9 +340,9 @@
(define-simple-macro (During τ:type EP ...) (define-simple-macro (During τ:type EP ...)
#:with τ/inst (instantiate-pattern-type #'τ.norm) #:with τ/inst (instantiate-pattern-type #'τ.norm)
(Reacts (Know τ) (Reacts (Asserted τ)
(Role (during-inner) (Role (during-inner)
(Reacts (¬Know τ/inst) (Reacts (Retracted τ/inst)
(Stop during-inner)) (Stop during-inner))
EP ...))) EP ...)))