first draft of verifying messages in spin backend
This commit is contained in:
Sam Caldwell
parent
ff1ac58a36
commit
6b46be34f9
|
|
@ -9,18 +9,21 @@
|
|||
(require (prefix-in synd: (only-in syndicate/core assert retract))
|
||||
(prefix-in synd: (only-in syndicate/patch patch-empty patch-seq)))
|
||||
|
||||
(require (only-in racket/hash hash-union))
|
||||
|
||||
(module+ test
|
||||
(require rackunit)
|
||||
(require "test-utils.rkt"))
|
||||
|
||||
;; a SpinProgram is a
|
||||
;; (sprog Assignment [Listof SpinProcess] [LTL SName] NameEnvironment)
|
||||
(struct sprog [assignment procs spec name-env] #:transparent)
|
||||
|
||||
|
||||
;; a SpinProgram is a
|
||||
;; (sprog Assignment [Listof SpinProcess] MessageTable SpinLTL NameEnvironment)
|
||||
(struct sprog [assignment procs spec msg-tabe name-env] #:transparent)
|
||||
|
||||
;; a SpinProcess is a
|
||||
;; (sproc SName [Setof SName] Assignment [Listof SName] [Setof SpinState])
|
||||
(struct sproc [name state-names init initial-assertions states] #:transparent)
|
||||
;; (sproc SName [Setof SName] Assignment [Listof SAction] [Setof SpinState])
|
||||
(struct sproc [name state-names locals init-actions states] #:transparent)
|
||||
|
||||
;; an Assignment is a [Hashof SVar SValue]
|
||||
|
||||
|
|
@ -57,9 +60,13 @@
|
|||
;; - (retract ?)
|
||||
;; - (send ?)
|
||||
;; - (incorporate D+)
|
||||
;; - (add-message-interest ?)
|
||||
;; - (remove-message-interest ?)
|
||||
;; - (transition-to SName)
|
||||
(struct assert [ty] #:prefab)
|
||||
(struct retract [ty] #:prefab)
|
||||
(struct add-message-interest [ty] #:prefab)
|
||||
(struct remove-message-interest [ty] #:prefab)
|
||||
;; send defined in proto.rkt
|
||||
(struct incorporate [evt] #:transparent)
|
||||
(struct transition-to [dest] #:transparent)
|
||||
|
|
@ -69,17 +76,54 @@
|
|||
|
||||
;; a NameEnvironment is a [Hashof τ SName]
|
||||
|
||||
;; [Sequenceof RoleGraph] [LTL τ] -> SpinProgram
|
||||
;; a MessageTable is a [Hashof SName [Setof SName]]
|
||||
;; mapping each possible message that can be sent to the names of each event
|
||||
;; that message can match
|
||||
|
||||
|
||||
;; a SpinLTL is a [LTL [U τ (Message τ)]]
|
||||
;; where τ represents an assertion and (Message τ) a message
|
||||
|
||||
|
||||
;; [Sequenceof RoleGraph] SpinLTL -> SpinProgram
|
||||
(define (program->spin rgs [spec #t])
|
||||
(define assertion-tys (all-assertions rgs))
|
||||
(define message-tys (all-messages rgs))
|
||||
(define event-tys (all-events rgs))
|
||||
(define event-subty# (make-event-map assertion-tys event-tys))
|
||||
(define all-mentioned-tys (set-union assertion-tys event-tys))
|
||||
(define-values (message-evts assertion-evts) (set-partition Message? event-tys))
|
||||
(define msg-event-tys (list->set (set-map message-evts Message-ty)))
|
||||
(define msg-bodies (set-union message-tys msg-event-tys))
|
||||
(define event-subty# (make-event-map assertion-tys assertion-evts))
|
||||
(define all-assertion-tys (set-union assertion-tys assertion-evts))
|
||||
(define all-mentioned-tys (set-union all-assertion-tys msg-bodies))
|
||||
(define name-env (make-name-env all-mentioned-tys))
|
||||
(define globals (initial-assertion-vars-for all-mentioned-tys name-env))
|
||||
(define procs (for/list ([rg rgs]) (rg->spin rg event-subty# name-env)))
|
||||
(define assertion-vars (initial-assertion-vars-for all-assertion-tys name-env))
|
||||
(define messages-vars (initial-message-vars-for msg-bodies name-env))
|
||||
(define mailbox-vars (initial-mailbox-vars msg-bodies (map sproc-name procs) name-env))
|
||||
(define msg-table (make-message-table message-tys msg-event-tys name-env))
|
||||
;; TODO : should make sure all types mentioned in spec have variables, too
|
||||
(define globals (hash-union assertion-vars messages-vars mailbox-vars))
|
||||
(define spec-spin (rename-ltl spec name-env))
|
||||
(sprog globals procs spec-spin name-env))
|
||||
(sprog globals procs spec-spin msg-table name-env))
|
||||
|
||||
;; [Setof τ] [Setof τ] NameEnvironment -> MessageTable
|
||||
(define (make-message-table message-tys msg-event-tys name-env)
|
||||
(define msg-subty# (make-event-map message-tys msg-event-tys))
|
||||
(define (lookup nm) (hash-ref name-env nm))
|
||||
(for/hash ([m (in-set message-tys)])
|
||||
(values (lookup m)
|
||||
(rename-all name-env (set-add (hash-ref msg-subty# m) m)))))
|
||||
|
||||
;; [Setof X] [Pred X] -> (Values [Setof X] [Setof X])
|
||||
;; like partition on lists but for sets
|
||||
(define (set-partition p s)
|
||||
(for/fold ([yays (set)]
|
||||
[nays (set)])
|
||||
([x (in-set s)])
|
||||
(if (p x)
|
||||
(values (set-add yays x) nays)
|
||||
(values yays (set-add nays x)))))
|
||||
|
||||
;; RoleGraph [Hashof τ [Setof τ]] NameEnvironment -> SpinProcess
|
||||
(define (rg->spin rg event-subty# name-env #:name [name (gensym 'proc)])
|
||||
|
|
@ -90,22 +134,34 @@
|
|||
(state->spin st states event-subty# name-env state-renaming)))
|
||||
(define st0- (hash-ref state-renaming st0))
|
||||
;; ergh the invariant for when I tack on _assertions to a name is getting tricksy
|
||||
(define st0-assertions (rename-all name-env (super-type-closure (state-assertions (hash-ref states st0)) event-subty#)))
|
||||
(define st0-asserts (state-assertions (hash-ref states st0)))
|
||||
(define st0-msg-interests (message-transitions (state-transitions (hash-ref states st0))))
|
||||
(define initial-asserts (transition-assertions (set) st0-asserts event-subty# name-env))
|
||||
(define initial-msg-interests (transition-msg-interests (set) st0-msg-interests event-subty# name-env))
|
||||
(define init-acts (append initial-asserts initial-msg-interests))
|
||||
(define assignment (local-variables-for st0- all-events name-env))
|
||||
(sproc name (hash-values-set state-renaming) assignment st0-assertions (list->set states-)))
|
||||
(sproc name (hash-values-set state-renaming) assignment init-acts (list->set states-)))
|
||||
|
||||
;; State [Sequenceof State] [Hashof τ [Setof τ]] NameEnvironment [Hashof StateName SName] -> SpinState
|
||||
(define (state->spin st states event-subty# name-env state-env)
|
||||
(match-define (state name transitions assertions) st)
|
||||
(define name- (hash-ref state-env name))
|
||||
(define msg-txns (message-transitions transitions))
|
||||
(define branches (for*/list ([(D+ txns) (in-hash transitions)]
|
||||
[txn (in-set txns)])
|
||||
(match-define (transition effs dest) txn)
|
||||
(match-define (state _ _ dest-assertions) (hash-ref states dest))
|
||||
(match-define (state _ dest-txns dest-assertions) (hash-ref states dest))
|
||||
(define dest- (hash-ref state-env dest))
|
||||
(branch-on D+ assertions dest- dest-assertions effs event-subty# name-env)))
|
||||
(define dest-msg-txns (message-transitions dest-txns))
|
||||
(branch-on D+ assertions msg-txns dest- dest-assertions dest-msg-txns effs event-subty# name-env)))
|
||||
(sstate name- branches))
|
||||
|
||||
;; (Hashof D+ _) -> (Setof τ)
|
||||
(define (message-transitions transitions)
|
||||
(for/set ([D+ (in-hash-keys transitions)]
|
||||
#:when (Message? D+))
|
||||
(Message-ty D+)))
|
||||
|
||||
;; [Setof τ] -> NameEnvironment
|
||||
(define (make-name-env tys)
|
||||
(let loop ([name-depth 3])
|
||||
|
|
@ -130,6 +186,18 @@
|
|||
(define (active-var-name s)
|
||||
(string->symbol (format "know_~a" s)))
|
||||
|
||||
;; SName -> SName
|
||||
(define (messages-var-name s)
|
||||
(string->symbol (format "~a_messages" s)))
|
||||
|
||||
;; SName SName -> SName
|
||||
(define (msg-mailbox-var-name msg-ty proc-name)
|
||||
(string->symbol (format "~a_~a_mailbox" proc-name msg-ty)))
|
||||
|
||||
;; SName SName -> SName
|
||||
(define (msg-interest-var-name msg-ty proc-name)
|
||||
(string->symbol (format "~a_~a_interest" proc-name msg-ty)))
|
||||
|
||||
;; [Setof τ] [Setof τ] -> [Hashof τ [Setof τ]]
|
||||
(define (make-event-map assertion-tys event-tys)
|
||||
;; TODO - potentially use non-empty intersection
|
||||
|
|
@ -156,6 +224,23 @@
|
|||
(values (svar (assertions-var-name (hash-ref name-env τ)) SInt)
|
||||
0)))
|
||||
|
||||
;; [Setof τ] NameEnvironment -> Assignment
|
||||
(define (initial-message-vars-for msg-bodies name-env)
|
||||
(for/hash ([τ (in-set msg-bodies)])
|
||||
(values (svar (messages-var-name (hash-ref name-env τ)) SInt)
|
||||
0)))
|
||||
|
||||
;; [Setof τ] [Listof SName] NameEnvironment -> Assignment
|
||||
(define (initial-mailbox-vars msg-bodies proc-names name-env)
|
||||
(for*/fold ([assign (hash)])
|
||||
([proc-name (in-list proc-names)]
|
||||
[msg-ty (in-set msg-bodies)])
|
||||
(define ty- (hash-ref name-env msg-ty))
|
||||
(define mailbox (svar (msg-mailbox-var-name ty- proc-name) SInt))
|
||||
(define interest (svar (msg-interest-var-name ty- proc-name) SBool))
|
||||
(hash-set (hash-set assign mailbox 0)
|
||||
interest #f)))
|
||||
|
||||
;; NameEnvironment [Setof τ] -> [Sequenceof SName]
|
||||
(define (rename-all name-env asserts)
|
||||
(for/set ([a (in-set asserts)])
|
||||
|
|
@ -172,6 +257,20 @@
|
|||
([rg rgs])
|
||||
(set-union as (all-assertions-of rg))))
|
||||
|
||||
;; [Sequenceof RoleGraph] -> [Setof τ]
|
||||
(define (all-messages rgs)
|
||||
;; RoleGraph -> (Setof τ)
|
||||
(define (all-messages-of rg)
|
||||
(for*/set ([st (in-hash-values (role-graph-states rg))]
|
||||
[txns (in-hash-values (state-transitions st))]
|
||||
[txn (in-set txns)]
|
||||
[eff (in-list (transition-effs txn))]
|
||||
#:when (send? eff))
|
||||
(send-ty eff)))
|
||||
(for/fold ([ms (set)])
|
||||
([rg rgs])
|
||||
(set-union ms (all-messages-of rg))))
|
||||
|
||||
;; [Sequenceof RoleGraph] -> [Setof τ]
|
||||
(define (all-events rgs)
|
||||
;; RoleGraph -> (Setof τ)
|
||||
|
|
@ -190,32 +289,59 @@
|
|||
[(or (Asserted τ) (Retracted τ))
|
||||
τ]
|
||||
[(Message τ)
|
||||
(raise-argument-error 'all-event-types "messages not supported yet" D+)]
|
||||
D+]
|
||||
[_
|
||||
(raise-argument-error 'all-event-types "internal events not allowed" D+)])))
|
||||
|
||||
;; SName [Setof τ] NameEnvironment -> Assignment
|
||||
;; SName [Setof [U τ D+] NameEnvironment -> Assignment
|
||||
(define (local-variables-for st0 all-events name-env)
|
||||
(define assign
|
||||
(for/hash ([evt (in-set all-events)])
|
||||
(for/hash ([evt (in-set all-events)]
|
||||
#:unless (Message? evt))
|
||||
(values (svar (active-var-name (hash-ref name-env evt))
|
||||
SBool)
|
||||
#f)))
|
||||
(hash-set assign CURRENT-STATE st0))
|
||||
|
||||
;; D+ [Setof τ] SName [Setof τ] [Listof TransitionEffect] [Hashof τ [Setof τ]] NameEnvironment -> SBranch
|
||||
(define (branch-on D+ curr-assertions dest dest-assertions effs event-subty# name-env)
|
||||
;; D+ [Setof τ] [Setof τ] SName [Setof τ] [Setof τ] [Listof TransitionEffect] [Hashof τ [Setof τ]] NameEnvironment -> SBranch
|
||||
(define (branch-on D+ curr-assertions curr-msg-txns dest dest-assertions dest-msg-txns effs event-subty# name-env)
|
||||
(define assertion-updates (transition-assertions curr-assertions dest-assertions event-subty# name-env))
|
||||
(define msg-interest-updates (transition-msg-interests curr-msg-txns dest-msg-txns event-subty# name-env))
|
||||
(define effs- (rename-effects effs name-env))
|
||||
(define renamed-evt (rename-event D+ name-env))
|
||||
(sbranch renamed-evt dest (list* (transition-to dest)
|
||||
(incorporate renamed-evt)
|
||||
(append assertion-updates
|
||||
msg-interest-updates
|
||||
effs-))))
|
||||
|
||||
;; [Setof τ] [Setof τ] [Hashof τ [Setof τ]] NameEnvironment -> [Listof SAction]
|
||||
(define (transition-assertions curr-assertions dest-assertions event-subty# name-env)
|
||||
(define new-assertions (super-type-closure (set-subtract dest-assertions curr-assertions) event-subty#))
|
||||
(define retractions (super-type-closure (set-subtract curr-assertions dest-assertions) event-subty#))
|
||||
(define (lookup ty) (hash-ref name-env ty))
|
||||
(define asserts (set-map new-assertions (compose assert lookup)))
|
||||
(define retracts (set-map retractions (compose retract lookup)))
|
||||
(unless (empty? effs)
|
||||
(raise-argument-error 'branch-on "messages not supported" effs))
|
||||
(define renamed-evt (rename-event D+ name-env))
|
||||
(sbranch renamed-evt dest (list* (transition-to dest)
|
||||
(incorporate renamed-evt)
|
||||
(append asserts retracts effs))))
|
||||
(append asserts retracts))
|
||||
|
||||
;; [Setof τ] [Setof τ] [Hashof τ [Setof τ]] NameEnvironment -> [Listof SAction]
|
||||
(define (transition-msg-interests curr-msg-txns dest-msg-txns event-subty# name-env)
|
||||
;; TODO - not sure if super-type-closure needed here
|
||||
(define new-interests (set-subtract dest-msg-txns curr-msg-txns))
|
||||
(define lost-interests (set-subtract curr-msg-txns dest-msg-txns))
|
||||
(define (lookup ty) (hash-ref name-env ty))
|
||||
(define add-interests (set-map new-interests (compose add-message-interest lookup)))
|
||||
(define remove-interests (set-map lost-interests (compose remove-message-interest lookup)))
|
||||
(append add-interests remove-interests))
|
||||
|
||||
;; [Listof TransitionEffect] NameEnvironment -> [Listof SAction]
|
||||
(define (rename-effects effs name-env)
|
||||
(for/list ([eff (in-list effs)])
|
||||
(match eff
|
||||
[(send ty)
|
||||
(send (hash-ref name-env ty))]
|
||||
[_
|
||||
(raise-argument-error 'rename-effects "only send effects supported" eff)])))
|
||||
|
||||
;; D+ NameEnvironment -> D+
|
||||
(define (rename-event D+ name-env)
|
||||
|
|
@ -225,11 +351,14 @@
|
|||
[(Retracted τ)
|
||||
(Retracted (hash-ref name-env τ))]
|
||||
[(Message τ)
|
||||
(raise-argument-error 'rename-event "messages not implemented yet" D+)]))
|
||||
(Message (hash-ref name-env τ))]))
|
||||
|
||||
;; [LTL τ] -> [LTL SName]
|
||||
;; SpinLTL -> [LTL SName]
|
||||
(define (rename-ltl ltl name-env)
|
||||
(define (lookup τ) (hash-ref name-env τ))
|
||||
(define (lookup x)
|
||||
(match x
|
||||
[(Message τ) (Message (hash-ref name-env τ))]
|
||||
[τ (hash-ref name-env τ)]))
|
||||
(map-atomic ltl lookup))
|
||||
|
||||
(module+ test
|
||||
|
|
@ -399,35 +528,39 @@
|
|||
;; SpinProgram -> Void
|
||||
(define (gen-spin prog)
|
||||
(match prog
|
||||
[(sprog assignment procs spec name-env)
|
||||
[(sprog assignment procs spec msg-table name-env)
|
||||
(display SPIN-PRELUDE)
|
||||
(gen-assignment assignment)
|
||||
(newline)
|
||||
(for ([p procs])
|
||||
(gen-spin-form p name-env)
|
||||
(gen-spin-proc p name-env)
|
||||
(newline))
|
||||
(gen-msg-dispatcher msg-table (map sproc-name procs))
|
||||
(gen-spec "spec" (lambda () (gen-ltl spec)))
|
||||
(newline)
|
||||
(gen-sanity-ltl assignment)]))
|
||||
|
||||
;; SpinThang NameEnvironment-> Void
|
||||
(define (gen-spin-form spin name-env)
|
||||
;; SpinProcess NameEnvironment -> Void
|
||||
(define (gen-spin-proc proc name-env)
|
||||
(match-define (sproc name state-names locals init-actions states) proc)
|
||||
(indent) (declare-mtype state-names)
|
||||
(indent) (printf "active proctype ~a() {\n" name)
|
||||
(with-indent
|
||||
(gen-assignment locals)
|
||||
(indent) (displayln "atomic {")
|
||||
(for ([a init-actions])
|
||||
(gen-spin-form a name-env name))
|
||||
(indent) (displayln "}")
|
||||
(indent) (displayln "end: do")
|
||||
(with-indent
|
||||
(for ([st states])
|
||||
(gen-spin-form st name-env name)))
|
||||
(indent) (displayln "od;"))
|
||||
(indent) (displayln "}"))
|
||||
|
||||
;; SpinThang NameEnvironment SName -> Void
|
||||
(define (gen-spin-form spin name-env proc-name)
|
||||
(match spin
|
||||
[(sproc name state-names init asserts states)
|
||||
(indent) (declare-mtype state-names)
|
||||
(indent) (printf "active proctype ~a() {\n" name)
|
||||
(with-indent
|
||||
(gen-assignment init)
|
||||
(indent) (displayln "atomic {")
|
||||
(for ([a asserts])
|
||||
(gen-spin-form (assert a) name-env))
|
||||
(indent) (displayln "}")
|
||||
(indent) (displayln "end: do")
|
||||
(with-indent
|
||||
(for ([st states])
|
||||
(gen-spin-form st name-env)))
|
||||
(indent) (displayln "od;"))
|
||||
(indent) (displayln "}")]
|
||||
[(sstate name branches)
|
||||
(indent) (printf ":: ~a == ~a ->\n" (svar-name CURRENT-STATE) name)
|
||||
(cond
|
||||
|
|
@ -439,27 +572,68 @@
|
|||
(indent) (displayln "if")
|
||||
(with-indent
|
||||
(for ([branch branches])
|
||||
(gen-spin-form branch name-env)))
|
||||
(gen-spin-form branch name-env proc-name)))
|
||||
(indent) (displayln "fi;"))])]
|
||||
[(sbranch event dest actions)
|
||||
(indent) (printf ":: ~a -> ~a\n" (predicate-for event) (embed-event-as-comment event name-env))
|
||||
(indent) (printf ":: ~a -> ~a\n" (predicate-for event proc-name) (embed-event-as-comment event name-env))
|
||||
(with-indent
|
||||
(indent) (displayln "atomic {")
|
||||
(with-indent
|
||||
(for ([act actions])
|
||||
(gen-spin-form act name-env)))
|
||||
(gen-spin-form act name-env proc-name)))
|
||||
(indent) (displayln "}"))]
|
||||
[(assert x)
|
||||
(indent) (printf "ASSERT(~a); ~a\n" x (embed-value-as-comment assert x name-env))]
|
||||
[(retract x)
|
||||
(indent) (printf "RETRACT(~a); ~a\n" x (embed-value-as-comment retract x name-env))]
|
||||
[(send x)
|
||||
(raise-argument-error 'gen-spin-form "message sending not supported yet" spin)]
|
||||
(indent) (printf "SEND(~a); ~a\n" x (embed-value-as-comment send x name-env))]
|
||||
[(add-message-interest x)
|
||||
(define interest-var-nm (msg-interest-var-name x proc-name))
|
||||
(indent) (printf "~a = true;\n" interest-var-nm)]
|
||||
[(remove-message-interest x)
|
||||
(define interest-var-nm (msg-interest-var-name x proc-name))
|
||||
(indent) (printf "~a = false;\n" interest-var-nm)]
|
||||
[(incorporate evt)
|
||||
(indent) (update-for evt)]
|
||||
(indent) (update-for evt proc-name)]
|
||||
[(transition-to dest)
|
||||
(indent) (printf "~a = ~a;\n" (svar-name CURRENT-STATE) dest)]))
|
||||
|
||||
;; MessageTable [Listof SName] -> Void
|
||||
(define (gen-msg-dispatcher msg-table proc-names)
|
||||
(unless (hash-empty? msg-table)
|
||||
(indent) (displayln "active proctype __msg_dispatcher__() {")
|
||||
(with-indent
|
||||
(indent) (displayln "end: do")
|
||||
(with-indent
|
||||
(for ([(sent-msg matching-evts) (in-hash msg-table)])
|
||||
(gen-msg-dispatch sent-msg matching-evts proc-names)))
|
||||
(indent) (displayln "od;"))
|
||||
(indent) (displayln "}")))
|
||||
|
||||
;; SName (Setof SName) [Listof SName] -> Void
|
||||
(define (gen-msg-dispatch sent-msg matching-evts proc-names)
|
||||
(define mailbox-nm (messages-var-name sent-msg))
|
||||
(indent) (printf ":: ~a > 0 ->\n" mailbox-nm)
|
||||
(with-indent
|
||||
(indent) (displayln "atomic {")
|
||||
(with-indent
|
||||
(indent) (printf "~a--;\n" mailbox-nm)
|
||||
(for ([proc (in-list proc-names)])
|
||||
(dispatch-to matching-evts proc)))
|
||||
(indent) (displayln "}")))
|
||||
|
||||
;; [Setof SName] SName -> Void
|
||||
(define (dispatch-to matching-evts proc)
|
||||
(indent) (displayln "if")
|
||||
(with-indent
|
||||
(for ([msg (in-set matching-evts)])
|
||||
(define mailbox-nm (msg-mailbox-var-name msg proc))
|
||||
(define interest-nm (msg-interest-var-name msg proc))
|
||||
(indent) (printf ":: ~a > 0 -> ~a++\n" interest-nm mailbox-nm))
|
||||
(indent) (displayln ":: else -> skip;"))
|
||||
(indent) (displayln "fi;"))
|
||||
|
||||
;; [Setof SName] -> Void
|
||||
(define (declare-mtype state-names)
|
||||
(display "mtype = {")
|
||||
|
|
@ -496,7 +670,7 @@
|
|||
[(== mtype) "mtype"]))
|
||||
|
||||
;; D+ -> String
|
||||
(define (predicate-for event)
|
||||
(define (predicate-for event proc-name)
|
||||
(match event
|
||||
[(Asserted nm)
|
||||
(define assertion-var nm)
|
||||
|
|
@ -507,10 +681,11 @@
|
|||
(define active-var (active-var-name nm))
|
||||
(format "RETRACTED(~a) && ~a" assertion-var active-var)]
|
||||
[(Message nm)
|
||||
(raise-argument-error 'predicate-for "message sending not supported yet" event)]))
|
||||
(define mailbox-var (msg-mailbox-var-name nm proc-name))
|
||||
(format "~a > 0" mailbox-var)]))
|
||||
|
||||
;; D+ -> Void
|
||||
(define (update-for event)
|
||||
(define (update-for event proc-name)
|
||||
(match event
|
||||
[(Asserted nm)
|
||||
(define active-var (active-var-name nm))
|
||||
|
|
@ -519,7 +694,8 @@
|
|||
(define active-var (active-var-name nm))
|
||||
(printf "~a = ~a;\n" active-var (spin-val->string #f))]
|
||||
[(Message nm)
|
||||
(raise-argument-error 'predicate-for "message sending not supported yet" event)]))
|
||||
(define mailbox-var (msg-mailbox-var-name nm proc-name))
|
||||
(printf "~a--;\n" mailbox-var)]))
|
||||
|
||||
;; D+ NameEnvironment -> String
|
||||
(define (embed-event-as-comment event name-env)
|
||||
|
|
@ -527,7 +703,7 @@
|
|||
(match event
|
||||
[(Asserted nm) (values Asserted nm)]
|
||||
[(Retracted nm) (values Retracted nm)]
|
||||
[(Message nm) (error 'embed-event-as-comment "messages not supported yet")]))
|
||||
[(Message nm) (values Message nm)]))
|
||||
(embed-value-as-comment kons id name-env))
|
||||
|
||||
;; (τ -> Any) SName NameEnvironment -> String
|
||||
|
|
@ -552,7 +728,8 @@
|
|||
(newline)
|
||||
(indent) (displayln "}"))
|
||||
|
||||
;; [LTL SName] -> Void
|
||||
;; SpinLTL -> Void
|
||||
;; SpinLTL isn't quite right, not types but identifiers
|
||||
(define (gen-ltl ltl)
|
||||
(match ltl
|
||||
[(always p)
|
||||
|
|
@ -579,8 +756,12 @@
|
|||
(indent) (display "!(")
|
||||
(gen-ltl p)
|
||||
(displayln ")")]
|
||||
[(atomic nm)
|
||||
(printf "ASSERTED(~a)\n" nm)]
|
||||
[(atomic x)
|
||||
(match x
|
||||
[(Message nm)
|
||||
(printf "(~a > 0)\n" (messages-var-name nm))]
|
||||
[nm
|
||||
(printf "ASSERTED(~a)\n" nm)])]
|
||||
[#t
|
||||
(display "true")]
|
||||
[#f
|
||||
|
|
|
|||
|
|
@ -3,18 +3,34 @@
|
|||
;; Expected Output
|
||||
;; pong: 8339
|
||||
|
||||
(message-struct ping : Ping (v))
|
||||
(message-struct pong : Pong (v))
|
||||
|
||||
(define-type-alias ds-type
|
||||
(U (Message (Tuple String Int))
|
||||
(Observe (Tuple String ★/t))))
|
||||
(U (Message (Ping Int))
|
||||
(Message (Pong Int))
|
||||
(Observe (Ping ★/t))
|
||||
(Observe (Pong ★/t))
|
||||
(Observe (Observe (Ping ★/t)))))
|
||||
|
||||
(run-ground-dataspace ds-type
|
||||
(spawn ds-type
|
||||
(lift+define-role ponger
|
||||
(start-facet echo
|
||||
(on (message (tuple "ping" (bind x Int)))
|
||||
(send! (tuple "pong" x)))))
|
||||
(on (message (ping $v))
|
||||
(send! (pong v))))))
|
||||
(spawn ds-type
|
||||
(lift+define-role pinger
|
||||
(start-facet serve
|
||||
(on start
|
||||
(send! (tuple "ping" 8339)))
|
||||
(on (message (tuple "pong" (bind x Int)))
|
||||
(printf "pong: ~v\n" x)))))
|
||||
(on (asserted (observe (ping _)))
|
||||
(send! (ping 8339)))
|
||||
(on (message (pong $x))
|
||||
(printf "pong: ~v\n" x))))))
|
||||
|
||||
(module+ test
|
||||
(verify-actors (And (Eventually (M (Ping Int)))
|
||||
(Eventually (M (Pong Int)))
|
||||
(Always (Implies (M (Ping Int))
|
||||
(Eventually (M (Pong Int))))))
|
||||
pinger
|
||||
ponger))
|
||||
|
|
|
|||
|
|
@ -67,7 +67,7 @@
|
|||
export-roles export-type check-simulates check-has-simulating-subgraph lift+define-role
|
||||
verify-actors
|
||||
;; LTL Syntax
|
||||
True False Always Eventually Until WeakUntil Implies And Or Not A
|
||||
True False Always Eventually Until WeakUntil Implies And Or Not A M
|
||||
;; Extensions
|
||||
match cond
|
||||
submod for-syntax for-meta only-in except-in
|
||||
|
|
@ -660,7 +660,8 @@
|
|||
(define-type And : LTL * -> LTL)
|
||||
(define-type Or : LTL * -> LTL)
|
||||
(define-type Not : LTL -> LTL)
|
||||
(define-type A : Type -> LTL)
|
||||
(define-type A : Type -> LTL) ;; Assertions
|
||||
(define-type M : Type -> LTL) ;; Messages
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Behavioral Analysis
|
||||
|
|
@ -712,7 +713,8 @@
|
|||
And proto:&&
|
||||
Or proto:||
|
||||
Not proto:ltl-not
|
||||
A proto:atomic))
|
||||
A proto:atomic
|
||||
M (compose proto:atomic proto:Message)))
|
||||
|
||||
(define (double-check)
|
||||
(for/first ([id (in-dict-keys TRANSLATION#)]
|
||||
|
|
|
|||
|
|
@ -4,6 +4,7 @@
|
|||
#define RETRACTED(x) (x##_assertions == 0)
|
||||
#define ASSERT(x) x##_assertions = x##_assertions + 1
|
||||
#define RETRACT(x) x##_assertions = x##_assertions - 1
|
||||
#define SEND(x) x##_messages = x##_messages + 1
|
||||
|
||||
/* Rest of Program */
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue