add messages to proto
This commit is contained in:
Sam Caldwell
parent
fa8822e40d
commit
202bcd6842
|
|
@ -14,9 +14,11 @@
|
|||
;; a T is one of
|
||||
;; - (Role FacetName (Listof EP)), also abbreviated as just Role
|
||||
;; - (Spawn τ)
|
||||
;; - (Sends τ)
|
||||
;; - (Stop FacetName Body)
|
||||
(struct Role (nm eps) #:transparent)
|
||||
(struct Spawn (ty) #:transparent)
|
||||
(struct Sends (ty) #:transparent)
|
||||
(struct Stop (nm body) #:transparent)
|
||||
|
||||
;; a EP is one of
|
||||
|
|
@ -93,10 +95,15 @@
|
|||
;; -----------------------------------------------------------------------------
|
||||
;; Compiling Roles to state machines
|
||||
|
||||
;; a State is a (state StateName (Hashof D (Setof StateName)))
|
||||
;; a State is a (state StateName (Hashof D (Setof Transition)))
|
||||
;; where each D in the hash satisfies external-evt?
|
||||
;; a StateName is a (Setof FacetName)
|
||||
;; let's assume that all FacetNames are unique
|
||||
;; a Transition is a (transition (Listof TransitionEffect) StateName)
|
||||
(struct transition (effs dest) #:transparent)
|
||||
;; a TransitionEffect is one of
|
||||
;; - (send τ)
|
||||
(struct send (ty) #:transparent)
|
||||
;; ok, this is also ignoring Spawn actions for now, would show up in the transitions hash
|
||||
(struct state (name transitions) #:transparent)
|
||||
|
||||
|
|
@ -131,14 +138,15 @@
|
|||
(for/hash ([(D effs) (in-hash agg-txn)]
|
||||
#:when (external-evt? D))
|
||||
;; TODO - may want to remove self loops here
|
||||
(define destinations
|
||||
(define txns
|
||||
(for*/set ([eff* (in-set effs)]
|
||||
[dst (in-set (apply-effects eff* current ft roles#))])
|
||||
dst))
|
||||
(values D destinations)))
|
||||
[txn (in-set (apply-effects eff* current ft roles#))])
|
||||
txn))
|
||||
(values D txns)))
|
||||
(define new-work
|
||||
(for*/list ([st-set (in-hash-values transitions)]
|
||||
[st (in-set st-set)]
|
||||
(for*/list ([txns (in-hash-values transitions)]
|
||||
[txn (in-set txns)]
|
||||
[st (in-value (transition-dest txn))]
|
||||
#:unless (equal? st current)
|
||||
#:unless (hash-has-key? states st))
|
||||
st))
|
||||
|
|
@ -179,7 +187,7 @@
|
|||
(Observe (book-quote String ⋆)))
|
||||
(check-true (hash-has-key? transitions (Asserted quote-request)))
|
||||
(check-equal? (hash-ref transitions (Asserted quote-request))
|
||||
(set (set 'seller 'fulfill))))
|
||||
(set (transition '() (set 'seller 'fulfill)))))
|
||||
(test-case
|
||||
"compile role that quits"
|
||||
(define r
|
||||
|
|
@ -197,7 +205,7 @@
|
|||
(define transitions (state-transitions state0))
|
||||
(check-true (hash-has-key? transitions (Asserted Int)))
|
||||
(check-equal? (hash-ref transitions (Asserted Int))
|
||||
(set (set))))
|
||||
(set (transition '() (set)))))
|
||||
|
||||
(test-case
|
||||
"leader-revised should have a quote/poll cycle"
|
||||
|
|
@ -212,8 +220,11 @@
|
|||
(define bq (Asserted (book-quote String Int)))
|
||||
(check-true (hash? gq-transitions))
|
||||
(check-true (hash-has-key? gq-transitions bq))
|
||||
(define dests (hash-ref gq-transitions bq))
|
||||
(check-true (set? dests))
|
||||
(define txns (hash-ref gq-transitions bq))
|
||||
(check-true (set? txns))
|
||||
(define dests (for/set ([t (in-set txns)])
|
||||
(transition-dest t)))
|
||||
(check-true (set? txns))
|
||||
(check-true (set-member? dests (set 'get-quotes 'poll-members)))
|
||||
(check-true (hash-has-key? state# (set 'get-quotes 'poll-members)))
|
||||
(define gqpm-st (hash-ref state# (set 'get-quotes 'poll-members)))
|
||||
|
|
@ -222,7 +233,10 @@
|
|||
(define bi (Asserted (book-interest String String ⋆)))
|
||||
(check-true (hash? gqpm-transitions))
|
||||
(check-true (hash-has-key? gqpm-transitions bi))
|
||||
(define dests2 (hash-ref gqpm-transitions bi))
|
||||
(define txns2 (hash-ref gqpm-transitions bi))
|
||||
(check-true (set? txns2))
|
||||
(define dests2 (for/set ([t (in-set txns2)])
|
||||
(transition-dest t)))
|
||||
(check-true (set? dests2))
|
||||
(check-true (set-member? dests2 (set 'get-quotes))))
|
||||
|
||||
|
|
@ -284,6 +298,8 @@
|
|||
[(cons (cons parent T) rest)
|
||||
(match T
|
||||
;; TODO - handle Spawn
|
||||
[(Sends _)
|
||||
(loop rest downs ups)]
|
||||
[(Role nm eps)
|
||||
;; record the parent/child relationship
|
||||
(define downs2 (hash-update downs
|
||||
|
|
@ -427,6 +443,7 @@
|
|||
;; a RoleEffect is one of
|
||||
;; - (start RoleName)
|
||||
;; - (stop RoleName)
|
||||
;; - (send τ)
|
||||
;; TODO - leaving out Spawn here
|
||||
(struct start (nm) #:transparent)
|
||||
(struct stop (nm) #:transparent)
|
||||
|
|
@ -436,10 +453,11 @@
|
|||
;; It always includes the keys StartEvt and StopEvt.
|
||||
(define txn-desc0 (hash StartEvt (set) StopEvt (set)))
|
||||
|
||||
;; (Listof RoleEffect) StateName
|
||||
;; (Listof RoleEffect)
|
||||
;; StateName
|
||||
;; FacetTree
|
||||
;; (Hashof FacetName TransitionDesc)
|
||||
;; -> (Setof StateName)
|
||||
;; -> (Setof Transition)
|
||||
;; determine the state resulting from some effects, given the currently active
|
||||
;; facets and a description of possible facet locations and behavior.
|
||||
(define (apply-effects effs st ft txn#)
|
||||
|
|
@ -447,9 +465,11 @@
|
|||
[effs effs])
|
||||
(match effs
|
||||
['()
|
||||
(set st)]
|
||||
(set (transition '() st))]
|
||||
[(cons eff rest)
|
||||
(match eff
|
||||
[(send _)
|
||||
(set (transition (list eff) st))]
|
||||
[(start nm)
|
||||
(define st+ (set-add st nm))
|
||||
(define start-effs (hash-ref (hash-ref txn# nm) StartEvt))
|
||||
|
|
@ -461,25 +481,24 @@
|
|||
[result (in-set (loop st+ (append rest eff*)))])
|
||||
result)])]
|
||||
[(stop nm)
|
||||
;; better include nm
|
||||
(define children (find-children ft nm st))
|
||||
(define st-
|
||||
(for/fold ([st st])
|
||||
([c (in-list children)])
|
||||
(set-remove st c)))
|
||||
(for/fold ([sts (set st-)])
|
||||
(for/fold ([txns (set (transition '() st-))])
|
||||
([f-name (in-list children)])
|
||||
(define stop-effs (hash-ref (hash-ref txn# f-name) StopEvt))
|
||||
(cond
|
||||
[(set-empty? stop-effs)
|
||||
(for*/set ([st (in-set sts)]
|
||||
[result (in-set (loop st rest))])
|
||||
result)]
|
||||
[else
|
||||
(for*/set ([st (in-set sts)]
|
||||
[effs* (in-set stop-effs)]
|
||||
[result (in-set (loop st (append rest effs*)))])
|
||||
result)]))])])))
|
||||
(define stop-effs+ (if (set-empty? stop-effs)
|
||||
(set '())
|
||||
stop-effs))
|
||||
(for*/set ([txn (in-set txns)]
|
||||
[st (in-value (transition-dest txn))]
|
||||
[effs* (in-set stop-effs+)]
|
||||
[next-txn (in-set (loop st (append effs* rest)))])
|
||||
(transition (append (transition-effs txn)
|
||||
(transition-effs next-txn))
|
||||
(transition-dest next-txn))))])])))
|
||||
|
||||
;; FacetTree FacetName (Setof FacetName) -> (List FacetName)
|
||||
;; return the facets in names that are children of the given facet nm, ordered
|
||||
|
|
@ -519,8 +538,10 @@
|
|||
(for*/list ([act (in-list (Body->actions body))]
|
||||
[role (in-list (enumerate-roles act))])
|
||||
role)]
|
||||
[(Sends _)
|
||||
'()]
|
||||
[(Spawn _)
|
||||
(error)]))
|
||||
(error 'enumerate-roles "Spawn not yet implemented")]))
|
||||
|
||||
;; Role -> TransitionDesc
|
||||
;; determine how the event handlers in a role alter the facet tree
|
||||
|
|
@ -645,6 +666,8 @@
|
|||
(set-union agg effs++))]
|
||||
[(Role nm _)
|
||||
(set (list (start nm)))]
|
||||
[(Sends τ)
|
||||
(set (list (send τ)))]
|
||||
[(Stop nm more)
|
||||
(define effects (Body->effects more))
|
||||
(cond
|
||||
|
|
@ -754,6 +777,15 @@
|
|||
[_
|
||||
#f]))
|
||||
|
||||
;; TransitionEffect TransitionEffect -> Bool
|
||||
;; subtyping lifted over transition effects
|
||||
(define (eff<:? e1 e2)
|
||||
(match (list e1 e2)
|
||||
[(list (send t1) (send t2))
|
||||
(<:? t1 t2)]
|
||||
[_
|
||||
#f]))
|
||||
|
||||
;; Role -> (Setof τ)
|
||||
;; Compute the set of assertions the role contributes (on its own, not
|
||||
;; considering parent assertions)
|
||||
|
|
@ -788,17 +820,18 @@
|
|||
(Observe String)))
|
||||
|
||||
;; an Equation is (equiv StateName StateName)
|
||||
;; INVARIANT: lhs is "implementation", rhs is "specification"
|
||||
;;
|
||||
;; a Goal is one of
|
||||
;; - Equation
|
||||
;; - (one-of (Setof StateMatch))
|
||||
;;
|
||||
;; a StateMatch is a (Setof Equation)
|
||||
;; a StateMatch is a (Setof (equiv Transition Transition))
|
||||
(struct equiv (a b) #:transparent)
|
||||
(struct one-of (opts) #:transparent)
|
||||
|
||||
;; (Setof StateName) (Setof StateName) -> (Setof (Setof Equation))
|
||||
;; Create potential state matchings
|
||||
;; (Setof Transition) (Setof Transition) -> (Setof StateMatch)
|
||||
;; Create potential edge matchings
|
||||
;; In each state matching, each element a of the first set (as) is
|
||||
;; matched with an element b of bs, where each b has at least one state
|
||||
;; matched with it.
|
||||
|
|
@ -905,9 +938,22 @@
|
|||
verify/with-current-assumed))]
|
||||
[(one-of matchings)
|
||||
(for/or ([matching (in-set matchings)])
|
||||
(define matching-hypos
|
||||
(for/set ([eq (in-set matching)])
|
||||
(match-define (equiv t1 t2) eq)
|
||||
(equiv (transition-dest t1) (transition-dest t2))))
|
||||
(for/and ([goal (in-set matching)])
|
||||
(define hypotheses (set-remove matching goal))
|
||||
(verify goal (set-union hypotheses assumptions))))])))
|
||||
(match-define (equiv (transition effs1 dest1)
|
||||
(transition effs2 dest2)) goal)
|
||||
(cond
|
||||
[(effects-subsequence? effs2 effs1)
|
||||
(define local-goal (equiv dest1 dest2))
|
||||
(define hypotheses
|
||||
(set-remove matching-hypos local-goal))
|
||||
(verify local-goal (set-union hypotheses assumptions))]
|
||||
[else
|
||||
#f])
|
||||
))])))
|
||||
(verify (equiv st0-1 st0-2) (set)))
|
||||
|
||||
;; (Sequenceof StateName) Role -> (Hashof StateName (Setof τ))
|
||||
|
|
@ -935,8 +981,8 @@
|
|||
(for/or ([assertion1 (in-set as1)])
|
||||
(<:? assertion2 assertion1))))
|
||||
|
||||
;; (Hashof D (Setof StateName))
|
||||
;; (Hashof D (Setof StateName))
|
||||
;; (Hashof D (Setof Transition))
|
||||
;; (Hashof D (Setof Transition))
|
||||
;; (Goal -> Bool) -> Bool
|
||||
;; Determine if:
|
||||
;; for each event D going from sn2,
|
||||
|
|
@ -946,28 +992,45 @@
|
|||
;; for the set of states Y connected to sn1 by E,
|
||||
;; it is possible to pair the states of X and Y such that they are in simulation,
|
||||
;; as determined by the verify procedure
|
||||
;; and the effects on the edge going to Y are a supersequence of the effects
|
||||
;; on the edge to Y
|
||||
(define (same-on-specified-events? transitions1 transitions2 verify)
|
||||
(for/and ([(D2 dests2) (in-hash transitions2)])
|
||||
(define dests1
|
||||
(for/and ([(D2 edges2) (in-hash transitions2)])
|
||||
(define edges1
|
||||
(for/fold ([agg (set)])
|
||||
([(D1 dests) (in-hash transitions1)]
|
||||
([(D1 txns1) (in-hash transitions1)]
|
||||
#:when (D<:? D2 D1)
|
||||
;; only consider dataflow events vs. non-dataflow when
|
||||
;; there is not a dataflow edge in the spec (HACK)
|
||||
#:unless (and (equal? D1 DataflowEvt)
|
||||
(not (equal? D2 DataflowEvt))
|
||||
(hash-has-key? transitions2 D1)))
|
||||
(set-union agg dests)))
|
||||
(set-union agg txns1)))
|
||||
(cond
|
||||
[(set-empty? dests1)
|
||||
[(set-empty? edges1)
|
||||
#f]
|
||||
[else
|
||||
(define combos (make-combinations dests1 dests2))
|
||||
(define combos (make-combinations edges1 edges2))
|
||||
(verify (one-of combos))])))
|
||||
|
||||
;; (Listof TransitionEffect) (Listof TransitionEffect) -> Bool
|
||||
;; determine if actual includes (supertypes of) the effects of spec in the same
|
||||
;; order
|
||||
(define (effects-subsequence? spec actual)
|
||||
(match spec
|
||||
['()
|
||||
#t]
|
||||
[(cons eff1 more-spec)
|
||||
(match actual
|
||||
['()
|
||||
#f]
|
||||
[(cons eff2 more-actual)
|
||||
(if (eff<:? eff1 eff2)
|
||||
(effects-subsequence? more-spec more-actual)
|
||||
(effects-subsequence? spec more-actual))])]))
|
||||
|
||||
;; (Hashof D (Setof StateName))
|
||||
;; (Hashof D (Setof StateName))
|
||||
;; (Hashof D (Setof Transition))
|
||||
;; (Hashof D (Setof Transition))
|
||||
;; StateName
|
||||
;; (Goal -> Bool) -> Bool
|
||||
;; Determine if:
|
||||
|
|
@ -985,8 +1048,8 @@
|
|||
(D<:? evt2 evt1)))
|
||||
evt1))
|
||||
(for*/and ([evt (in-set extra-evts)]
|
||||
[dest (in-set (hash-ref transitions1 evt))])
|
||||
(verify (equiv dest sn2))))
|
||||
[txn (in-set (hash-ref transitions1 evt))])
|
||||
(verify (equiv (transition-dest txn) sn2))))
|
||||
|
||||
(module+ test
|
||||
(test-case
|
||||
|
|
@ -1108,13 +1171,15 @@
|
|||
(for/hash ([st (in-list states*)])
|
||||
(define orig-txn# (state-transitions (hash-ref state# st)))
|
||||
(define txn#
|
||||
(for*/hash ([(D dests) (in-hash orig-txn#)]
|
||||
#:when (event-enabled? D)
|
||||
[dests+ (in-value (set-intersect dests states))]
|
||||
;; empty dests+ might mean want to ignore this set of
|
||||
;; events? TODO
|
||||
#:unless (set-empty? dests+))
|
||||
(values D dests+)))
|
||||
(for/hash ([D (in-hash-keys orig-txn#)]
|
||||
#:when (event-enabled? D))
|
||||
(define orig-txns (hash-ref orig-txn# D))
|
||||
(define new-txns
|
||||
(for/set ([txn (in-set orig-txns)]
|
||||
#:when (set-member? states (transition-dest txn)))
|
||||
txn))
|
||||
;; TODO - what if new-txns is empty?
|
||||
(values D new-txns)))
|
||||
(values st (state st txn#))))
|
||||
(for ([st0 (in-list states*)])
|
||||
(define rg (role-graph st0 st#))
|
||||
|
|
@ -1142,9 +1207,9 @@
|
|||
(search more seen)]
|
||||
[else
|
||||
(define connections
|
||||
(for*/list ([dests (in-hash-values txn#)]
|
||||
[d (in-set dests)])
|
||||
d))
|
||||
(for*/list ([txn* (in-hash-values txn#)]
|
||||
[txn (in-set txn*)])
|
||||
(transition-dest txn)))
|
||||
(search (append more connections)
|
||||
(set-add seen name))])])))
|
||||
|
||||
|
|
@ -1153,10 +1218,10 @@
|
|||
"reachable states"
|
||||
(define rg
|
||||
(role-graph (set 'X 'Y 'Z)
|
||||
(hash (set 'X 'Y 'Z) (state (set 'X 'Y 'Z) (hash (Asserted Int) (set (set 'X 'Y 'Z))
|
||||
(Retracted Int) (set (set 'X 'Y))))
|
||||
(hash (set 'X 'Y 'Z) (state (set 'X 'Y 'Z) (hash (Asserted Int) (set (transition '() (set 'X 'Y 'Z)))
|
||||
(Retracted Int) (set (transition '() (set 'X 'Y)))))
|
||||
(set 'X) (state (set 'X) '#hash())
|
||||
(set 'X 'Y) (state (set 'X 'Y) (hash (Asserted Int) (set (set 'X 'Y 'Z)))))))
|
||||
(set 'X 'Y) (state (set 'X 'Y) (hash (Asserted Int) (set (transition '() (set 'X 'Y 'Z))))))))
|
||||
(define reachable (reachable-states rg))
|
||||
(check-true (set-member? reachable (set 'X 'Y 'Z)))
|
||||
(check-true (set-member? reachable (set 'X 'Y)))
|
||||
|
|
@ -1172,9 +1237,9 @@
|
|||
(set 'during-inner2 'during-inner1 'tm)
|
||||
(hash
|
||||
(Asserted (Struct 'TaskAssignment (list)))
|
||||
(set (set 'during-inner2 'during-inner1 'tm))
|
||||
(set (transition '() (set 'during-inner2 'during-inner1 'tm)))
|
||||
(Retracted (Struct 'TaskAssignment (list)))
|
||||
(set (set 'during-inner1 'tm))))
|
||||
(set (transition '() (set 'during-inner1 'tm)))))
|
||||
(set 'tm)
|
||||
(state (set 'tm) '#hash())
|
||||
(set 'during-inner1 'tm)
|
||||
|
|
@ -1182,7 +1247,7 @@
|
|||
(set 'during-inner1 'tm)
|
||||
(hash
|
||||
(Asserted (Struct 'TaskAssignment (list)))
|
||||
(set (set 'during-inner2 'during-inner1 'tm)))))))
|
||||
(set (transition '() (set 'during-inner2 'during-inner1 'tm))))))))
|
||||
(define reachable (reachable-states rg))
|
||||
(check-true (set-member? reachable (set 'during-inner2 'during-inner1 'tm)))
|
||||
(check-true (set-member? reachable (set 'during-inner1 'tm)))
|
||||
|
|
@ -1205,104 +1270,108 @@
|
|||
;; ---------------------------------------------------------------------------
|
||||
;; Visualization
|
||||
|
||||
(module+ vis
|
||||
;; TODO - for now, assume there are no names that need escaping
|
||||
;; TODO - for now, assume there are no names that need escaping
|
||||
|
||||
;; RoleGraph -> DotString
|
||||
;; name is an optional string
|
||||
;; translate the states to DOT that can be passed to graphviz
|
||||
(define (render rg
|
||||
#:name [name #f])
|
||||
(match-define (role-graph st0 st#) rg)
|
||||
(define graph-name (or name "Roles"))
|
||||
(define entry-node (format "~a [style=bold];" (state-name->dot-name st0)))
|
||||
(define edges
|
||||
(for/list ([(sn st) (in-hash st#)])
|
||||
(define dot-name (state-name->dot-name sn))
|
||||
(define txns (state-transitions st))
|
||||
(define dot-edges
|
||||
(for*/list ([(D targets) (in-hash txns)]
|
||||
[target (in-set targets)])
|
||||
(render-edge dot-name D target)))
|
||||
(string-join dot-edges "\n")))
|
||||
(string-join (cons entry-node edges)
|
||||
"\n"
|
||||
#:before-first (format "digraph ~a {\n" graph-name)
|
||||
#:after-last "\n}"))
|
||||
;; RoleGraph -> DotString
|
||||
;; name is an optional string
|
||||
;; translate the states to DOT that can be passed to graphviz
|
||||
(define (render rg
|
||||
#:name [name #f])
|
||||
(match-define (role-graph st0 st#) rg)
|
||||
(define graph-name (or name "Roles"))
|
||||
(define entry-node (format "~a [style=bold];" (state-name->dot-name st0)))
|
||||
(define edges
|
||||
(for/list ([(sn st) (in-hash st#)])
|
||||
(define dot-name (state-name->dot-name sn))
|
||||
(define txns (state-transitions st))
|
||||
(define dot-edges
|
||||
(for*/list ([(D targets) (in-hash txns)]
|
||||
[target (in-set targets)])
|
||||
(render-edge dot-name D target)))
|
||||
(string-join dot-edges "\n")))
|
||||
(string-join (cons entry-node edges)
|
||||
"\n"
|
||||
#:before-first (format "digraph ~a {\n" graph-name)
|
||||
#:after-last "\n}"))
|
||||
|
||||
;; RoleGraph PathString -> DotString
|
||||
;; Like render but write the output to a file
|
||||
(define (render-to-file rg dest
|
||||
#:name [name #f])
|
||||
(with-output-to-file dest
|
||||
(lambda () (write-string (render rg #:name name)))
|
||||
#:exists 'replace))
|
||||
;; RoleGraph PathString -> DotString
|
||||
;; Like render but write the output to a file
|
||||
(define (render-to-file rg dest
|
||||
#:name [name #f])
|
||||
(with-output-to-file dest
|
||||
(lambda () (write-string (render rg #:name name)))
|
||||
#:exists 'replace))
|
||||
|
||||
;; StateName -> String
|
||||
(define (state-name->dot-name sn)
|
||||
(define nms
|
||||
(for/list ([nm (in-set sn)])
|
||||
(~a nm)))
|
||||
(string-join nms ","
|
||||
#:before-first "\"{"
|
||||
#:after-last "}\""))
|
||||
;; StateName -> String
|
||||
(define (state-name->dot-name sn)
|
||||
(define nms
|
||||
(for/list ([nm (in-set sn)])
|
||||
(~a nm)))
|
||||
(string-join nms ","
|
||||
#:before-first "\"{"
|
||||
#:after-last "}\""))
|
||||
|
||||
;; String D StateName -> DotString
|
||||
;; describe an edge between the states with the corresponding label
|
||||
(define (render-edge from evt to)
|
||||
(define target-dot (state-name->dot-name to))
|
||||
(define edge-label (D->label evt))
|
||||
(format "~a -> ~a [label=\"~a\"];" from target-dot edge-label))
|
||||
;; String D Transition -> DotString
|
||||
;; describe an edge between the states with the corresponding label
|
||||
(define (render-edge from evt txn)
|
||||
(match-define (transition effs to) txn)
|
||||
(define target-dot (state-name->dot-name to))
|
||||
(define evt-label (D->label evt))
|
||||
(define edge-label
|
||||
;; TODO - better presentation of effects
|
||||
(if (empty? effs)
|
||||
evt-label
|
||||
(string-append evt-label "[...]")))
|
||||
(format "~a -> ~a [label=\"~a\"];" from target-dot edge-label))
|
||||
|
||||
;; D -> DotString
|
||||
;; give a description of an event suitable for rendering
|
||||
(define (D->label evt)
|
||||
(match evt
|
||||
[(Asserted τ)
|
||||
(string-append "+" (τ->string τ))]
|
||||
[(Retracted τ)
|
||||
(string-append "-" (τ->string τ))]
|
||||
[(Message τ)
|
||||
(string-append "!" (τ->string τ))]
|
||||
[(Know τ)
|
||||
(string-append "~+" (τ->string τ))]
|
||||
[(Forget τ)
|
||||
(string-append "~-" (τ->string τ))]
|
||||
[(Realize τ)
|
||||
(string-append "~!" (τ->string τ))]
|
||||
[(== StartEvt)
|
||||
"Start"]
|
||||
[(== StopEvt)
|
||||
"Stop"]
|
||||
[(== DataflowEvt)
|
||||
"Dataflow"]))
|
||||
;; D -> DotString
|
||||
;; give a description of an event suitable for rendering
|
||||
(define (D->label evt)
|
||||
(match evt
|
||||
[(Asserted τ)
|
||||
(string-append "+" (τ->string τ))]
|
||||
[(Retracted τ)
|
||||
(string-append "-" (τ->string τ))]
|
||||
[(Message τ)
|
||||
(string-append "!" (τ->string τ))]
|
||||
[(Know τ)
|
||||
(string-append "~+" (τ->string τ))]
|
||||
[(Forget τ)
|
||||
(string-append "~-" (τ->string τ))]
|
||||
[(Realize τ)
|
||||
(string-append "~!" (τ->string τ))]
|
||||
[(== StartEvt)
|
||||
"Start"]
|
||||
[(== StopEvt)
|
||||
"Stop"]
|
||||
[(== DataflowEvt)
|
||||
"Dataflow"]))
|
||||
|
||||
;; τ -> String
|
||||
(define (τ->string τ)
|
||||
;; (Listof String) -> String
|
||||
(define (paren-join xs)
|
||||
(string-join xs
|
||||
#:before-first "("
|
||||
#:after-last ")"))
|
||||
(match τ
|
||||
[(Base name)
|
||||
(symbol->string name)]
|
||||
[(== ⋆) "⋆"]
|
||||
[(Observe τ2)
|
||||
(string-append "?" (τ->string τ2))]
|
||||
[(List τ2)
|
||||
(τ->string (Struct 'List (list τ2)))]
|
||||
[(Set τ2)
|
||||
(τ->string (Struct 'Set (list τ2)))]
|
||||
[(Hash τk τv)
|
||||
(τ->string (Struct 'Hash (list τk τv)))]
|
||||
[(Struct nm τs)
|
||||
(define slots (map τ->string τs))
|
||||
(paren-join (cons (~a nm) slots))]
|
||||
[(U τs)
|
||||
(define slots (map τ->string τs))
|
||||
(paren-join (cons "U" slots))]))
|
||||
)
|
||||
;; τ -> String
|
||||
(define (τ->string τ)
|
||||
;; (Listof String) -> String
|
||||
(define (paren-join xs)
|
||||
(string-join xs
|
||||
#:before-first "("
|
||||
#:after-last ")"))
|
||||
(match τ
|
||||
[(Base name)
|
||||
(symbol->string name)]
|
||||
[(== ⋆) "⋆"]
|
||||
[(Observe τ2)
|
||||
(string-append "?" (τ->string τ2))]
|
||||
[(List τ2)
|
||||
(τ->string (Struct 'List (list τ2)))]
|
||||
[(Set τ2)
|
||||
(τ->string (Struct 'Set (list τ2)))]
|
||||
[(Hash τk τv)
|
||||
(τ->string (Struct 'Hash (list τk τv)))]
|
||||
[(Struct nm τs)
|
||||
(define slots (map τ->string τs))
|
||||
(paren-join (cons (~a nm) slots))]
|
||||
[(U τs)
|
||||
(define slots (map τ->string τs))
|
||||
(paren-join (cons "U" slots))]))
|
||||
|
||||
;; ---------------------------------------------------------------------------
|
||||
;; Converting types from the turnstile implementation
|
||||
|
|
@ -1315,6 +1384,8 @@
|
|||
(Role name parsed-eps)]
|
||||
[(list 'Spawn t)
|
||||
(Spawn (parse-T t))]
|
||||
[(list 'Sends t)
|
||||
(Sends (parse-τ t))]
|
||||
[(list 'Stop name body ...)
|
||||
(define bdy (if (= (length body) 1)
|
||||
(first body)
|
||||
|
|
@ -1994,3 +2065,47 @@
|
|||
(Stop during-inner))))
|
||||
(Reacts (Retracted (TaskManager (Bind Symbol) (Bind Int))))
|
||||
(Reacts (Asserted (TaskManager (Bind Symbol) (Bind Int))))))
|
||||
|
||||
;; ---------------------------------------------------------------------------
|
||||
;; Message Examples/Tests
|
||||
|
||||
(define msgy-r1
|
||||
'(Role (m)
|
||||
(Reacts (Asserted Int)
|
||||
(Sends String)
|
||||
(Role (m2)
|
||||
(Shares (x))))))
|
||||
|
||||
(define msgy-r2
|
||||
'(Role (m)
|
||||
(Reacts (Asserted Int)
|
||||
(Role (m2)
|
||||
(Shares (x))))))
|
||||
|
||||
(define msgy-spec
|
||||
'(Role (n)
|
||||
(Reacts (Asserted Int)
|
||||
(Sends String)
|
||||
(Role (n2)
|
||||
(Shares (x))))))
|
||||
|
||||
(module+ test
|
||||
(test-case
|
||||
"basic functionality of roles with messages"
|
||||
(define mr1 (parse-T msgy-r1))
|
||||
(check-true (Role? mr1))
|
||||
(define mr2 (parse-T msgy-r2))
|
||||
(check-true (Role? mr2))
|
||||
(define mrs (parse-T msgy-spec))
|
||||
(check-true (Role? mrs))
|
||||
(define rg1 (compile mr1))
|
||||
(check-true (role-graph? rg1))
|
||||
(define rg2 (compile mr2))
|
||||
(check-true (role-graph? rg2))
|
||||
(define rgs (compile mrs))
|
||||
(check-true (role-graph? rgs))
|
||||
(check-true (simulates? mr1 mr1))
|
||||
(check-true (simulates? mr2 mr2))
|
||||
(check-true (simulates? mrs mrs))
|
||||
(check-true (simulates? mr1 mrs))
|
||||
(check-false (simulates? mr2 mrs))))
|
||||
|
|
|
|||
Loading…
Reference in New Issue