look into leader impl simulating spec a bit
This commit is contained in:
Sam Caldwell
parent
47dc84f034
commit
c726fb2bdd
|
|
@ -129,7 +129,20 @@
|
|||
(start-facet poll-members
|
||||
(define/query-set yays (book-interest (ref title) (bind name String) #t) name)
|
||||
(define/query-set nays (book-interest (ref title) (bind name String) #f) name)
|
||||
(begin/dataflow
|
||||
(on (asserted (book-interest (ref title) (bind name String) discard))
|
||||
;; count the leader as a 'yay'
|
||||
(when (>= (set-count (ref yays))
|
||||
(/ (set-count (ref members)) 2))
|
||||
(printf "leader finds enough affirmation for ~a\n" (ref title))
|
||||
(stop get-quotes
|
||||
(start-facet announce
|
||||
(assert (book-of-the-month (ref title))))))
|
||||
(when (> (set-count (ref nays))
|
||||
(/ (set-count (ref members)) 2))
|
||||
(printf "leader finds enough negative nancys for ~a\n" (ref title))
|
||||
(stop poll-members (next-book))))
|
||||
;; begin/dataflow is a problem for simulation checking
|
||||
#;(begin/dataflow
|
||||
;; count the leader as a 'yay'
|
||||
(when (>= (set-count (ref yays))
|
||||
(/ (set-count (ref members)) 2))
|
||||
|
|
|
|||
|
|
@ -100,26 +100,55 @@
|
|||
(Stop 'leader
|
||||
(Role 'announce
|
||||
(list
|
||||
(Shares (Struct 'book-of-the-month String)))))
|
||||
(Shares (Struct 'book-of-the-month (list String))))))
|
||||
(Stop 'poll (list)))))))))))
|
||||
|
||||
#;(define-type-alias leader-actual
|
||||
(Role (get-quotes31)
|
||||
(Reacts (Know (BookQuoteT String (Bind Int)))
|
||||
(Stop get-quotes)
|
||||
(Role (poll-members36)
|
||||
(Reacts OnDataflow
|
||||
(Stop poll-members
|
||||
(Stop get-quotes))
|
||||
(Stop get-quotes
|
||||
(Role (announce39)
|
||||
(Shares (BookOfTheMonthT String)))))
|
||||
(Reacts (¬Know (BookInterestT String (Bind String) Bool)))
|
||||
(Reacts (Know (BookInterestT String (Bind String) Bool)))
|
||||
(Reacts (¬Know (BookInterestT String (Bind String) Bool)))
|
||||
(Reacts (Know (BookInterestT String (Bind String) Bool)))))
|
||||
(Reacts (¬Know (ClubMemberT (Bind String))))
|
||||
(Reacts (Know (ClubMemberT (Bind String))))))
|
||||
(define leader-actual
|
||||
(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-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)))))
|
||||
|
||||
(define leader-fixed?
|
||||
(Role 'get-quotes
|
||||
(list
|
||||
(Reacts (Know (book-quote String Int))
|
||||
(Branch (list
|
||||
(Role 'poll-members
|
||||
(list
|
||||
(Reacts (Know (book-interest String String ⋆))
|
||||
(Branch (list
|
||||
(Stop 'poll-members
|
||||
'())
|
||||
(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)))))
|
||||
|
||||
;; -----------------------------------------------------------------------------
|
||||
;; Compiling Roles to state machines
|
||||
|
|
@ -760,7 +789,11 @@
|
|||
(check-false (simulates? seller client)))
|
||||
(test-case
|
||||
"leader-spec identity simulation"
|
||||
(check-true (simulates? leader-spec leader-spec))))
|
||||
(check-true (simulates? leader-spec leader-spec)))
|
||||
(test-case
|
||||
"things aren't quite right with leader-actual"
|
||||
(check-false (simulates? leader-actual leader-spec))
|
||||
(check-true (simulates? leader-fixed? leader-spec))))
|
||||
|
||||
;; ---------------------------------------------------------------------------
|
||||
;; Visualization
|
||||
|
|
@ -775,6 +808,7 @@
|
|||
#:name [name #f])
|
||||
(match-define (role-graph st0 st#) rg)
|
||||
(define graph-name (or name "Roles"))
|
||||
(define entry-node (format "~a;" (state-name->dot-name st0)))
|
||||
(define edges
|
||||
(for/list ([(sn st) (in-hash st#)])
|
||||
(define dot-name (state-name->dot-name sn))
|
||||
|
|
@ -784,7 +818,7 @@
|
|||
[target (in-set targets)])
|
||||
(render-edge dot-name D target)))
|
||||
(string-join dot-edges "\n")))
|
||||
(string-join edges
|
||||
(string-join (cons entry-node edges)
|
||||
"\n"
|
||||
#:before-first (format "digraph ~a {\n" graph-name)
|
||||
#:after-last "\n}"))
|
||||
|
|
@ -794,7 +828,7 @@
|
|||
(define (render-to-file rg dest
|
||||
#:name [name #f])
|
||||
(with-output-to-file dest
|
||||
(lambda () (write-string (render rg)))
|
||||
(lambda () (write-string (render rg #:name name)))
|
||||
#:exists 'replace))
|
||||
|
||||
;; StateName -> String
|
||||
|
|
|
|||
|
|
@ -1782,14 +1782,14 @@
|
|||
|
||||
(define-typed-syntax (print-type e) ≫
|
||||
[⊢ e ≫ e- (⇒ : τ) (⇒ ν-ep (~effs eps ...)) (⇒ ν-f (~effs fs ...)) (⇒ ν-s (~effs ss ...))]
|
||||
#:do [(displayln (type->str #'τ))]
|
||||
#:do [(pretty-display (type->str #'τ))]
|
||||
----------------------------------
|
||||
[⊢ e- (⇒ : τ) (⇒ ν-ep (eps ...)) (⇒ ν-f (fs ...)) (⇒ ν-s (ss ...))])
|
||||
|
||||
(define-typed-syntax (print-role e) ≫
|
||||
[⊢ e ≫ e- (⇒ : τ) (⇒ ν-ep (~effs eps ...)) (⇒ ν-f (~effs fs ...)) (⇒ ν-s (~effs ss ...))]
|
||||
#:do [(for ([r (in-syntax #'(fs ...))])
|
||||
(displayln (type->str r)))]
|
||||
(pretty-display (type->str r)))]
|
||||
----------------------------------
|
||||
[⊢ e- (⇒ : τ) (⇒ ν-ep (eps ...)) (⇒ ν-f (fs ...)) (⇒ ν-s (ss ...))])
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue