Compare commits
No commits in common. "main" and "690f9e65a821070ac75469feff7f797188aa4547" have entirely different histories.
main
...
690f9e65a8
|
|
@ -36,8 +36,3 @@
|
|||
"scribble-lib"
|
||||
"sha"
|
||||
))
|
||||
|
||||
(define test-omit-paths
|
||||
;; There's some shared library related build issue with the syndicate-gl things
|
||||
'("syndicate-gl/"
|
||||
"syndicate-ide/"))
|
||||
|
|
|
|||
|
|
@ -803,7 +803,7 @@
|
|||
#:macro-definer-name define-event-expander
|
||||
#:introducer-parameter-name current-event-expander-introducer
|
||||
#:local-introduce-name syntax-local-event-expander-introduce
|
||||
#:expander-form-predicate-name event-expander-form?
|
||||
#:expander-id-predicate-name event-expander-id?
|
||||
#:expander-transform-name event-expander-transform)
|
||||
|
||||
(provide (for-syntax
|
||||
|
|
@ -811,7 +811,7 @@
|
|||
event-expander?
|
||||
event-expander-proc
|
||||
syntax-local-event-expander-introduce
|
||||
event-expander-form?
|
||||
event-expander-id?
|
||||
event-expander-transform)
|
||||
define-event-expander)
|
||||
|
||||
|
|
@ -949,8 +949,8 @@
|
|||
(define event-stx (syntax-disarm armed-event-stx orig-insp))
|
||||
(syntax-parse event-stx
|
||||
#:literals [core:message asserted retracted rising-edge know forget realize]
|
||||
[expander
|
||||
#:when (event-expander-form? #'expander)
|
||||
[(expander args ...)
|
||||
#:when (event-expander-id? #'expander)
|
||||
(event-expander-transform
|
||||
event-stx
|
||||
(lambda (result)
|
||||
|
|
|
|||
|
|
@ -76,7 +76,7 @@
|
|||
(define cleaned-acts (clean-actions acts))
|
||||
(for ([act (in-list cleaned-acts)]
|
||||
#:unless (actor? act))
|
||||
(raise-argument-error 'syndicate-module "top-level actor creation action" act))
|
||||
(error "only actor creation actions allowed at module level"))
|
||||
cleaned-acts)
|
||||
|
||||
(define-syntax (syndicate-module stx)
|
||||
|
|
|
|||
|
|
@ -60,10 +60,7 @@
|
|||
(quit))]
|
||||
[_ #f]))
|
||||
|
||||
(actor (lambda (e s) (quit))
|
||||
#f
|
||||
(message (set-timer 'tick 1000 'relative)))
|
||||
|
||||
(message (set-timer 'tick 1000 'relative))
|
||||
(actor ticker
|
||||
1
|
||||
(patch-seq (sub (observe (set-timer ? ? ?)))
|
||||
|
|
|
|||
|
|
@ -7,7 +7,4 @@
|
|||
'(;; Sam: example-plain is interactive, I think
|
||||
"examples/example-plain.rkt"
|
||||
;; Sam: for whatever reason I get a failure to load libcrypto for f-to-c
|
||||
"examples/actor/f-to-c.rkt"
|
||||
;; Sam: this test displays to stderr which the package server does not like
|
||||
"tests/nested-spawn-exceptions.rkt"
|
||||
))
|
||||
"examples/actor/f-to-c.rkt"))
|
||||
|
|
|
|||
|
|
@ -13,7 +13,6 @@
|
|||
(require (for-syntax syntax/parse))
|
||||
(require rackunit)
|
||||
(require racket/engine)
|
||||
(require racket/exn)
|
||||
|
||||
(define mt-scn (scn trie-empty))
|
||||
|
||||
|
|
@ -290,7 +289,7 @@
|
|||
;; leaf behavior function
|
||||
(define (actor-behavior e s)
|
||||
(when e
|
||||
(with-handlers ([exn:fail? (lambda (e) (printf "exception: ~v\n" (exn->string e)) (quit #:exception e (list)))])
|
||||
(with-handlers ([exn:fail? (lambda (e) (eprintf "exception: ~v\n" e) (quit #:exception e (list)))])
|
||||
(match-define (actor-state π-old fts) s)
|
||||
(define-values (actions next-fts)
|
||||
(for/fold ([as '()]
|
||||
|
|
@ -546,7 +545,7 @@
|
|||
;; boot-actor : actor Γ -> Action
|
||||
(define (boot-actor a Γ)
|
||||
(with-handlers ([exn:fail? (lambda (e)
|
||||
(printf "booting actor died with: ~a\n" (exn->string e))
|
||||
(eprintf "booting actor died with: ~v\n" e)
|
||||
#f)])
|
||||
(match a
|
||||
[`(spawn ,O ...)
|
||||
|
|
|
|||
|
|
@ -28,7 +28,7 @@
|
|||
#:macro-definer-name define-assertion-expander
|
||||
#:introducer-parameter-name current-assertion-expander-introducer
|
||||
#:local-introduce-name syntax-local-assertion-expander-introduce
|
||||
#:expander-form-predicate-name assertion-expander-form?
|
||||
#:expander-id-predicate-name assertion-expander-id?
|
||||
#:expander-transform-name assertion-expander-transform)
|
||||
|
||||
(provide (for-syntax
|
||||
|
|
@ -36,7 +36,7 @@
|
|||
assertion-expander?
|
||||
assertion-expander-proc
|
||||
syntax-local-assertion-expander-introduce
|
||||
assertion-expander-form?
|
||||
assertion-expander-id?
|
||||
assertion-expander-transform)
|
||||
define-assertion-expander)
|
||||
|
||||
|
|
@ -153,8 +153,8 @@
|
|||
bs
|
||||
ins))]
|
||||
|
||||
[expander
|
||||
(assertion-expander-form? #'expander)
|
||||
[(expander args ...)
|
||||
(assertion-expander-id? #'expander)
|
||||
(assertion-expander-transform pat-stx (lambda (r) (walk (syntax-rearm r pat-stx))))]
|
||||
|
||||
[(ctor p ...)
|
||||
|
|
|
|||
|
|
@ -1,4 +0,0 @@
|
|||
*.pml
|
||||
*.trail
|
||||
*.rktd
|
||||
*.tmp
|
||||
|
|
@ -34,14 +34,14 @@
|
|||
(define-type-alias τc
|
||||
(U BookQuote
|
||||
(Observe (BookQuoteT String ★/t))
|
||||
(Observe (Observe★ BookQuoteT))
|
||||
(Observe (Observe (BookQuoteT ★/t ★/t)))
|
||||
ClubMember
|
||||
(Observe★ ClubMemberT)
|
||||
(Observe (ClubMemberT ★/t))
|
||||
BookInterest
|
||||
(Observe (BookInterestT String ★/t ★/t))
|
||||
(Observe (Observe★ BookInterestT))
|
||||
(Observe (Observe (BookInterestT ★/t ★/t ★/t)))
|
||||
BookOfTheMonth
|
||||
(Observe★ BookOfTheMonthT)))
|
||||
(Observe (BookOfTheMonthT ★/t))))
|
||||
|
||||
(define-type-alias Inventory (List (Tuple String Int)))
|
||||
|
||||
|
|
@ -71,7 +71,7 @@
|
|||
;; Give quotes to interested parties.
|
||||
(during (observe (book-quote $title _))
|
||||
;; TODO - lookup
|
||||
(assert (book-quote title (lookup title (! books))))))))))
|
||||
(assert (book-quote title (lookup title (ref books))))))))))
|
||||
|
||||
(define-type-alias leader-role
|
||||
(Role (leader)
|
||||
|
|
@ -111,52 +111,52 @@
|
|||
[title String (first titles)])
|
||||
(define (next-book)
|
||||
(cond
|
||||
[(empty? (! book-list))
|
||||
[(empty? (ref book-list))
|
||||
(printf "leader fails to find a suitable book\n")
|
||||
(stop get-quotes)]
|
||||
[#t
|
||||
(:= title (first (! book-list)))
|
||||
(:= book-list (rest (! book-list)))]))
|
||||
(set! title (first (ref book-list)))
|
||||
(set! book-list (rest (ref book-list)))]))
|
||||
|
||||
;; keep track of book club members
|
||||
(define/query-set members (club-member $name) name
|
||||
#;#:on-add #;(printf "leader acknowledges member ~a\n" name))
|
||||
|
||||
(on (asserted (book-quote (! title) $quantity))
|
||||
(printf "leader learns that there are ~a copies of ~a\n" quantity (! title))
|
||||
(on (asserted (book-quote (ref title) $quantity))
|
||||
(printf "leader learns that there are ~a copies of ~a\n" quantity (ref title))
|
||||
(cond
|
||||
[(< quantity (+ 1 (set-count (! members))))
|
||||
[(< quantity (+ 1 (set-count (ref members))))
|
||||
;; not enough in stock for each member
|
||||
(next-book)]
|
||||
[#t
|
||||
;; find out if at least half of the members want to read the book
|
||||
(start-facet poll-members
|
||||
(define/query-set yays (book-interest (! title) $name #t) name)
|
||||
(define/query-set nays (book-interest (! title) $name #f) name)
|
||||
(on (asserted (book-interest (! title) $name _))
|
||||
(define/query-set yays (book-interest (ref title) $name #t) name)
|
||||
(define/query-set nays (book-interest (ref title) $name #f) name)
|
||||
(on (asserted (book-interest (ref title) $name _))
|
||||
;; count the leader as a 'yay'
|
||||
(when (>= (set-count (! yays))
|
||||
(/ (set-count (! members)) 2))
|
||||
(printf "leader finds enough affirmation for ~a\n" (! title))
|
||||
(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 (! title))))))
|
||||
(when (> (set-count (! nays))
|
||||
(/ (set-count (! members)) 2))
|
||||
(printf "leader finds enough negative nancys for ~a\n" (! title))
|
||||
(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 (! yays))
|
||||
(/ (set-count (! members)) 2))
|
||||
(printf "leader finds enough affirmation for ~a\n" (! title))
|
||||
(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 (! title))))))
|
||||
(when (> (set-count (! nays))
|
||||
(/ (set-count (! members)) 2))
|
||||
(printf "leader finds enough negative nancys for ~a\n" (! title))
|
||||
(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)))))])))))))
|
||||
|
||||
(define-type-alias member-role
|
||||
|
|
|
|||
|
|
@ -22,7 +22,7 @@
|
|||
(Role (cell-factory)
|
||||
(Reacts (Message (CreateCellT ID Value))
|
||||
;; want to say that what it spawns is a Cell
|
||||
(ActorWithRole ★/t Cell))))
|
||||
(Spawns ★/t))))
|
||||
|
||||
(define-type-alias Reader
|
||||
(Role (reader)
|
||||
|
|
|
|||
|
|
@ -161,12 +161,12 @@ The JobManager then performs the job and, when finished, asserts
|
|||
(Observe (Observe (TaskPerformance ID ★/t ★/t)))
|
||||
(JobManagerAlive)
|
||||
(Observe (JobManagerAlive))
|
||||
(Observe★ TaskRunner)
|
||||
(Observe (TaskRunner ★/t))
|
||||
(TaskManager ID Int)
|
||||
(Observe★ TaskManager)
|
||||
(Observe (TaskManager ★/t ★/t))
|
||||
(JobCompletion ID (List InputTask) TaskResult)
|
||||
(Observe (JobCompletion ID (List InputTask) ★/t))
|
||||
(Observe (Observe★ JobCompletion))))
|
||||
(Observe (Observe (JobCompletion ★/t ★/t ★/t)))))
|
||||
|
||||
;; ---------------------------------------------------------------------------------------------------
|
||||
;; Util Macros
|
||||
|
|
@ -471,7 +471,7 @@ The JobManager then performs the job and, when finished, asserts
|
|||
;; Requires (task-ready? t)
|
||||
(define (∀ (ρ) (perform-task [t : ConcreteTask]
|
||||
[k : (proc TaskID TaskResult -> ★/t
|
||||
#:effects (ρ))]))
|
||||
#:roles (ρ))]))
|
||||
(start-facet perform
|
||||
(on start (set! tasks-in-progress (add1 (ref tasks-in-progress))))
|
||||
(on stop (set! tasks-in-progress (sub1 (ref tasks-in-progress))))
|
||||
|
|
@ -479,8 +479,8 @@ The JobManager then performs the job and, when finished, asserts
|
|||
(log "JM begins on task ~a" this-id)
|
||||
|
||||
;; ID -> ...
|
||||
(define (∀ (ρ) (assign-task [mngr : ID]
|
||||
[request-again! : (proc -> ★/t #:effects (ρ))]))
|
||||
(define (assign-task [mngr : ID]
|
||||
[request-again! : (→fn ★/t)])
|
||||
(start-facet assign
|
||||
(on (retracted (task-manager mngr _))
|
||||
;; our task manager has crashed
|
||||
|
|
|
|||
|
|
@ -1,21 +0,0 @@
|
|||
#lang typed/syndicate
|
||||
;; Expected Output:
|
||||
;; got: new
|
||||
|
||||
(define-constructor* (something : SomethingT new blue)
|
||||
#:with Something (SomethingT String Int))
|
||||
|
||||
(define-type-alias τc
|
||||
(U Something
|
||||
(Observe★ SomethingT)))
|
||||
|
||||
(run-ground-dataspace
|
||||
τc
|
||||
(spawn
|
||||
(start-facet _
|
||||
(assert (something "new" 42))))
|
||||
(spawn
|
||||
(start-facet _
|
||||
(on (asserted (something $x 42))
|
||||
(printf "got: ~a\n" x))))
|
||||
)
|
||||
|
|
@ -1,17 +0,0 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
;; using different syntax than "client.rkt"
|
||||
|
||||
(require/typed "driver.rkt" [#:struct msg])
|
||||
|
||||
(define m : (MsgT Int String) (msg 1 "hi"))
|
||||
|
||||
(msg-in m)
|
||||
(msg-out m)
|
||||
|
||||
(match m
|
||||
[(msg (bind x Int) discard)
|
||||
(displayln x)])
|
||||
|
||||
;; error: msg/checked: arity mismatch
|
||||
#;(msg 1 2 3)
|
||||
|
|
@ -1,22 +0,0 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
(define (wf1)
|
||||
(spawn
|
||||
(with-facets
|
||||
([onn (facet (assert (tuple 'on))
|
||||
(on start (printf "on\n")))]
|
||||
[off (facet (on (asserted (tuple 'go))
|
||||
(stop off
|
||||
(start onn)))
|
||||
(on start (printf "off\n")))])
|
||||
off)))
|
||||
|
||||
(run-ground-dataspace
|
||||
(wf1)
|
||||
(spawn (start-facet _ (assert (tuple 'go)))))
|
||||
|
||||
;; BAD
|
||||
#;(spawn
|
||||
(with-facets
|
||||
[on (facet (on start (start on)))]
|
||||
on))
|
||||
|
|
@ -7,7 +7,4 @@
|
|||
"tests"))
|
||||
|
||||
(define test-omit-paths
|
||||
;; a number of the examples use SPIN for model checking which I need
|
||||
;; to figure out how to get working on the package server
|
||||
'("examples/"
|
||||
"tests/spin/"))
|
||||
'("examples/roles/chat-tcp2.rkt"))
|
||||
|
|
|
|||
|
|
@ -364,9 +364,7 @@ Like @racket[during], but spawns an actor for the behavior @racket[expr ...].
|
|||
(code:line #:on-add on-add-expr))
|
||||
(maybe-on-remove (code:line)
|
||||
(code:line #:on-remove on-remove-expr))]]{
|
||||
Equivalent to the untyped @racket[untyped:define/query-value]. The
|
||||
@racket[on-add-expr] and @racket[on-remove-expr], when given, execute after
|
||||
@racket[name] has been updated.
|
||||
Equivalent to the untyped @racket[untyped:define/query-value].
|
||||
}
|
||||
|
||||
@defform[(define/query-set name pattern expr
|
||||
|
|
|
|||
|
|
@ -6,11 +6,10 @@
|
|||
(require "ltl.rkt")
|
||||
(require racket/runtime-path)
|
||||
(require syndicate/trace syndicate/trace/msd)
|
||||
(require (prefix-in synd: (only-in syndicate/core assert retract message))
|
||||
(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))
|
||||
(require syntax/parse/define)
|
||||
|
||||
(module+ test
|
||||
(require rackunit)
|
||||
|
|
@ -19,22 +18,12 @@
|
|||
|
||||
|
||||
;; a SpinProgram is a
|
||||
;; (sprog Assignment
|
||||
;; [Listof SpinProcess]
|
||||
;; MessageTable
|
||||
;; SpinLTL
|
||||
;; [Setof SName]
|
||||
;; NameEnvironment)
|
||||
(struct sprog [assignment procs spec msg-tabe assertion-tys name-env] #:transparent)
|
||||
;; (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]
|
||||
;; SName
|
||||
;; Assignment
|
||||
;; [Listof SAction]
|
||||
;; [Setof SpinState])
|
||||
(struct sproc [name state-names st0 locals init-actions 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]
|
||||
|
||||
|
|
@ -69,7 +58,6 @@
|
|||
;; a SAction is one of
|
||||
;; - (assert ?)
|
||||
;; - (retract ?)
|
||||
;; - (unlearn ?)
|
||||
;; - (send ?)
|
||||
;; - (incorporate D+)
|
||||
;; - (add-message-interest ?)
|
||||
|
|
@ -77,7 +65,6 @@
|
|||
;; - (transition-to SName)
|
||||
(struct assert [ty] #:prefab)
|
||||
(struct retract [ty] #:prefab)
|
||||
(struct unlearn [ty] #:prefab)
|
||||
(struct add-message-interest [ty] #:prefab)
|
||||
(struct remove-message-interest [ty] #:prefab)
|
||||
;; send defined in proto.rkt
|
||||
|
|
@ -103,23 +90,22 @@
|
|||
(define assertion-tys (all-assertions rgs))
|
||||
(define message-tys (all-messages rgs))
|
||||
(define event-tys (all-events rgs))
|
||||
(define-values (spec-asserts spec-msgs) (spec-types spec))
|
||||
(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 spec-msgs))
|
||||
(define event-subty# (make-event-map assertion-tys (set-union assertion-evts spec-asserts)))
|
||||
(define all-assertion-tys (set-union assertion-tys assertion-evts spec-asserts))
|
||||
(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 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 assertion-nms (for/set ([τ (in-set all-assertion-tys)]) (hash-ref 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 msg-table assertion-nms 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)
|
||||
|
|
@ -145,22 +131,19 @@
|
|||
(define all-events (all-event-types (in-hash-values states)))
|
||||
(define state-renaming (make-state-rename (hash-keys states)))
|
||||
(define states- (for/list ([st (in-hash-values states)])
|
||||
(state->spin st states all-events event-subty# name-env state-renaming)))
|
||||
(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-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 all-events event-subty# name-env))
|
||||
(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))
|
||||
(define relevant-assertions (for/set ([evt (in-set all-events)]
|
||||
#:unless (Message? evt))
|
||||
(hash-ref name-env evt)))
|
||||
(sproc name (hash-values-set state-renaming) st0- relevant-assertions init-acts (list->set states-)))
|
||||
(sproc name (hash-values-set state-renaming) assignment init-acts (list->set states-)))
|
||||
|
||||
;; State [Sequenceof State] [Setof [U τ (Message τ)]] [Hashof τ [Setof τ]] NameEnvironment [Hashof StateName SName] -> SpinState
|
||||
(define (state->spin st states all-events event-subty# name-env state-env)
|
||||
;; 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))
|
||||
|
|
@ -170,7 +153,7 @@
|
|||
(match-define (state _ dest-txns dest-assertions) (hash-ref states dest))
|
||||
(define dest- (hash-ref state-env dest))
|
||||
(define dest-msg-txns (message-transitions dest-txns))
|
||||
(branch-on D+ assertions msg-txns dest- dest-assertions dest-msg-txns effs all-events event-subty# name-env)))
|
||||
(branch-on D+ assertions msg-txns dest- dest-assertions dest-msg-txns effs event-subty# name-env)))
|
||||
(sstate name- branches))
|
||||
|
||||
;; (Hashof D+ _) -> (Setof τ)
|
||||
|
|
@ -199,10 +182,6 @@
|
|||
(define (assertions-var-name s)
|
||||
(string->symbol (format "~a_assertions" s)))
|
||||
|
||||
;; SName -> SName
|
||||
(define (assertions-update-var-name s)
|
||||
(string->symbol (format "~a_update" s)))
|
||||
|
||||
;; SName -> SName
|
||||
(define (active-var-name s)
|
||||
(string->symbol (format "know_~a" s)))
|
||||
|
|
@ -241,10 +220,8 @@
|
|||
|
||||
;; [Setof τ] NameEnvironment -> Assignment
|
||||
(define (initial-assertion-vars-for assertion-tys name-env)
|
||||
(for*/hash ([τ (in-set assertion-tys)]
|
||||
[bucket? (in-list '(#t #f))])
|
||||
(define namer (if bucket? assertions-var-name assertions-update-var-name))
|
||||
(values (svar (namer (hash-ref name-env τ)) SInt)
|
||||
(for/hash ([τ (in-set assertion-tys)])
|
||||
(values (svar (assertions-var-name (hash-ref name-env τ)) SInt)
|
||||
0)))
|
||||
|
||||
;; [Setof τ] NameEnvironment -> Assignment
|
||||
|
|
@ -304,7 +281,7 @@
|
|||
(set-union as (all-events-of rg)))
|
||||
)
|
||||
|
||||
;; [Sequenceof State] -> [Setof [U τ (Message τ)]]
|
||||
;; [Sequenceof State] -> ?
|
||||
(define (all-event-types states)
|
||||
(for*/set ([st states]
|
||||
[D+ (in-hash-keys (state-transitions st))])
|
||||
|
|
@ -316,34 +293,6 @@
|
|||
[_
|
||||
(raise-argument-error 'all-event-types "internal events not allowed" D+)])))
|
||||
|
||||
;; SpinLTL -> (Values (Setof τ) (Setof τ))
|
||||
;; extract the types of assertions and messages mentioned in a spec
|
||||
(define (spec-types ltl)
|
||||
(let loop ([ltls (list ltl)]
|
||||
[asserts (set)]
|
||||
[msgs (set)])
|
||||
(match ltls
|
||||
['()
|
||||
(values asserts msgs)]
|
||||
[(cons ltl more-ltls)
|
||||
(match ltl
|
||||
[(or (always more-ltl)
|
||||
(eventually more-ltl)
|
||||
(ltl-not more-ltl))
|
||||
(loop (cons more-ltl more-ltls) asserts msgs)]
|
||||
[(or (weak-until ltl1 ltl2)
|
||||
(strong-until ltl1 ltl2)
|
||||
(ltl-implies ltl1 ltl2)
|
||||
(ltl-and ltl1 ltl2)
|
||||
(ltl-or ltl1 ltl2))
|
||||
(loop (list* ltl1 ltl2 more-ltls) asserts msgs)]
|
||||
[(atomic (Message τ))
|
||||
(loop more-ltls asserts (set-add msgs τ))]
|
||||
[(atomic τ)
|
||||
(loop more-ltls (set-add asserts τ) msgs)]
|
||||
[_
|
||||
(loop more-ltls asserts msgs)])])))
|
||||
|
||||
;; SName [Setof [U τ D+] NameEnvironment -> Assignment
|
||||
(define (local-variables-for st0 all-events name-env)
|
||||
(define assign
|
||||
|
|
@ -352,18 +301,11 @@
|
|||
(values (svar (active-var-name (hash-ref name-env evt))
|
||||
SBool)
|
||||
#f)))
|
||||
assign
|
||||
#;(hash-set assign CURRENT-STATE st0))
|
||||
(hash-set assign CURRENT-STATE st0))
|
||||
|
||||
;; [Setof SName] -> Void
|
||||
(define (update-knowledge relevant-assertions)
|
||||
(for ([assert-nm (in-set relevant-assertions)])
|
||||
(define know-nm (active-var-name assert-nm))
|
||||
(indent) (printf "~a = (~a -> ASSERTED(~a) : ~a);\n" know-nm know-nm assert-nm know-nm)))
|
||||
|
||||
;; D+ [Setof τ] [Setof τ] SName [Setof τ] [Setof τ] [Listof TransitionEffect] [Setof [U τ (Message τ)]] [Hashof τ [Setof τ]] NameEnvironment -> SBranch
|
||||
(define (branch-on D+ curr-assertions curr-msg-txns dest dest-assertions dest-msg-txns effs all-events event-subty# name-env)
|
||||
(define assertion-updates (transition-assertions curr-assertions dest-assertions all-events 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))
|
||||
|
|
@ -373,18 +315,14 @@
|
|||
msg-interest-updates
|
||||
effs-))))
|
||||
|
||||
;; [Setof τ] [Setof τ] [Setof [U τ (Message τ)]] [Hashof τ [Setof τ]] NameEnvironment -> [Listof SAction]
|
||||
(define (transition-assertions curr-assertions dest-assertions all-events event-subty# name-env)
|
||||
;; [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)))
|
||||
(define unlearns (for/list ([τ (in-set retractions)]
|
||||
#:when (and (Observe? τ)
|
||||
(set-member? all-events (Observe-ty τ))))
|
||||
(unlearn (lookup (Observe-ty τ)))))
|
||||
(append asserts retracts unlearns))
|
||||
(append asserts retracts))
|
||||
|
||||
;; [Setof τ] [Setof τ] [Hashof τ [Setof τ]] NameEnvironment -> [Listof SAction]
|
||||
(define (transition-msg-interests curr-msg-txns dest-msg-txns event-subty# name-env)
|
||||
|
|
@ -590,101 +528,33 @@
|
|||
;; SpinProgram -> Void
|
||||
(define (gen-spin prog)
|
||||
(match prog
|
||||
[(sprog assignment procs spec msg-table assertion-tys name-env)
|
||||
[(sprog assignment procs spec msg-table name-env)
|
||||
(display SPIN-PRELUDE)
|
||||
(gen-assignment assignment)
|
||||
(newline)
|
||||
(gen-assign GLOBAL-CLOCK-VAR GLOBAL-CLOCK-INIT-VAL #:declare #t)
|
||||
(for ([p procs])
|
||||
(gen-spin-proc p name-env)
|
||||
(newline))
|
||||
(gen-clock-ticker (map sproc-name procs) msg-table assertion-tys)
|
||||
(newline)
|
||||
(gen-msg-dispatcher msg-table (map sproc-name procs))
|
||||
(gen-spec "spec" (lambda () (gen-ltl spec)))
|
||||
(newline)
|
||||
(gen-sanity-ltl assignment)]))
|
||||
|
||||
;; (-> Void) -> Void
|
||||
;; generate the prelude for spin atomic sequences, call `gen-bdy`,
|
||||
;; then end the atomic block
|
||||
(define (with-spin-atomic* gen-bdy)
|
||||
(indent) (displayln "atomic {")
|
||||
(with-indent (gen-bdy))
|
||||
(indent) (displayln "}"))
|
||||
|
||||
(define-syntax-parse-rule (with-spin-atomic bdy ...+)
|
||||
(with-spin-atomic* (lambda () bdy ...)))
|
||||
|
||||
;; (-> Void) -> Void
|
||||
;; generate the prelude for spin dstep sequences, call `gen-bdy`,
|
||||
;; then end the dstep block
|
||||
(define (gen-spin-dstep gen-bdy)
|
||||
(indent) (printf "d_step { ~a\n" (format-as-comment DSTEP-EVENT))
|
||||
(with-indent (gen-bdy))
|
||||
(indent) (displayln "}"))
|
||||
|
||||
(define-syntax-parse-rule (with-spin-dstep bdy ...+)
|
||||
(gen-spin-dstep (lambda () bdy ...)))
|
||||
|
||||
;; (-> Void) -> Void
|
||||
(define (gen-spin-if gen-bdy)
|
||||
(indent) (displayln "if")
|
||||
(with-indent (gen-bdy))
|
||||
(indent) (displayln "fi;"))
|
||||
|
||||
(define-syntax-parse-rule (with-spin-if bdy ...+)
|
||||
(gen-spin-if (lambda () bdy ...)))
|
||||
|
||||
;; (-> Void) -> Void
|
||||
(define (gen-spin-do gen-bdy)
|
||||
(indent) (displayln "do")
|
||||
(with-indent (gen-bdy))
|
||||
(indent) (displayln "od;"))
|
||||
|
||||
(define-syntax-parse-rule (with-spin-do bdy ...+)
|
||||
(gen-spin-do (lambda () bdy ...)))
|
||||
|
||||
(define (gen-spin-branch pred gen-body [comment ""])
|
||||
(indent) (printf ":: ~a -> ~a\n" pred comment)
|
||||
(with-indent (gen-body)))
|
||||
|
||||
(define-syntax-parse-rule (with-spin-branch pred (~optional (~seq #:comment comment))
|
||||
body ...+)
|
||||
(gen-spin-branch pred (lambda () body ...) (~? comment)))
|
||||
|
||||
(define (gen-spin-break)
|
||||
(indent) (displayln "break;"))
|
||||
|
||||
(define (gen-spin-skip)
|
||||
(indent) (displayln "skip;"))
|
||||
|
||||
;; SpinProcess NameEnvironment -> Void
|
||||
(define (gen-spin-proc proc name-env)
|
||||
(match-define (sproc name state-names st0 relevant-assertions init-actions states) proc)
|
||||
(define my-clock (proc-clock-var name))
|
||||
(define locals (for/hash ([evt (in-set relevant-assertions)])
|
||||
(values (svar (active-var-name evt)
|
||||
SBool)
|
||||
#f)))
|
||||
(match-define (sproc name state-names locals init-actions states) proc)
|
||||
(indent) (declare-mtype state-names)
|
||||
(indent) (gen-assign my-clock GLOBAL-CLOCK-INIT-VAL #:declare #t)
|
||||
(indent) (printf "active proctype ~a() {\n" name)
|
||||
(with-indent
|
||||
(gen-assign CURRENT-STATE st0 #:declare #t)
|
||||
(gen-assignment locals)
|
||||
(with-spin-atomic
|
||||
(for ([a init-actions])
|
||||
(gen-spin-form a name-env name)))
|
||||
(indent) (printf "~a: do\n" (format-end-label name))
|
||||
(indent) (displayln "atomic {")
|
||||
(for ([a init-actions])
|
||||
(gen-spin-form a name-env name))
|
||||
(indent) (displayln "}")
|
||||
(indent) (displayln "end: do")
|
||||
(with-indent
|
||||
(with-spin-branch "true"
|
||||
(indent) (printf "~a;\n" (clock-predicate my-clock))
|
||||
(with-spin-atomic
|
||||
(indent) (update-clock my-clock)
|
||||
(with-spin-do
|
||||
(for ([st states])
|
||||
(gen-spin-form st name-env name)))
|
||||
(update-knowledge relevant-assertions))))
|
||||
(for ([st states])
|
||||
(gen-spin-form st name-env name)))
|
||||
(indent) (displayln "od;"))
|
||||
(indent) (displayln "}"))
|
||||
|
||||
|
|
@ -696,26 +566,26 @@
|
|||
(cond
|
||||
[(empty? branches)
|
||||
;; no transitions out of this state
|
||||
#;(gen-spin-skip) (gen-spin-break)
|
||||
]
|
||||
(indent) (displayln "end: false;")]
|
||||
[else
|
||||
(with-indent
|
||||
(with-spin-if
|
||||
(indent) (displayln "if")
|
||||
(with-indent
|
||||
(for ([branch branches])
|
||||
(gen-spin-form branch name-env proc-name))
|
||||
(gen-spin-branch "else" #;gen-spin-skip gen-spin-break)))])]
|
||||
(gen-spin-form branch name-env proc-name)))
|
||||
(indent) (displayln "fi;"))])]
|
||||
[(sbranch event dest actions)
|
||||
(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 proc-name))))]
|
||||
(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))]
|
||||
[(unlearn x)
|
||||
(indent) (printf "~a = false;\n" (active-var-name x))]
|
||||
[(send x)
|
||||
(indent) (printf "SEND(~a); ~a\n" x (embed-value-as-comment send x name-env))]
|
||||
[(add-message-interest x)
|
||||
|
|
@ -729,42 +599,29 @@
|
|||
[(transition-to dest)
|
||||
(indent) (printf "~a = ~a;\n" (svar-name CURRENT-STATE) dest)]))
|
||||
|
||||
;; [Listof SName] MessageTable -> Void
|
||||
(define (gen-clock-ticker proc-names msg-table assertion-tys)
|
||||
(define clock-names (for/list ([pn (in-list proc-names)])
|
||||
(svar-name (proc-clock-var pn))))
|
||||
(indent) (displayln "active proctype __clock_ticker__() {")
|
||||
(with-indent
|
||||
(indent) (displayln "end_clock_ticker:")
|
||||
(with-spin-do
|
||||
(with-spin-branch (all-procs-ready-predicate clock-names)
|
||||
(with-spin-dstep
|
||||
(indent) (update-clock GLOBAL-CLOCK-VAR (format-as-comment TURN-BEGIN-EVENT))
|
||||
(update-all-assertion-vars assertion-tys)
|
||||
(unless (hash-empty? msg-table)
|
||||
(with-spin-do
|
||||
(gen-spin-branch "else" gen-spin-break)
|
||||
(for ([(sent-msg matching-evts) (in-hash msg-table)])
|
||||
(gen-msg-dispatch sent-msg matching-evts proc-names))))))))
|
||||
(indent) (displayln "}"))
|
||||
|
||||
;; (Setof SName) -> Void
|
||||
;; update the assertion bucket variables based on the update variables
|
||||
(define (update-all-assertion-vars assertion-nms)
|
||||
(for ([assertion (in-set assertion-nms)])
|
||||
(define bucket (assertions-var-name assertion))
|
||||
(define update (assertions-update-var-name assertion))
|
||||
(indent) (printf "~a = ~a + ~a;\n" bucket bucket update)
|
||||
(indent) (printf "~a = 0;\n" update)))
|
||||
;; 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) (printf "~a--;\n" mailbox-nm)
|
||||
(for ([proc (in-list proc-names)])
|
||||
(dispatch-to matching-evts proc))))
|
||||
(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)
|
||||
|
|
@ -786,16 +643,12 @@
|
|||
;; Assignment -> Void
|
||||
(define (gen-assignment assign)
|
||||
(for ([(var val) (in-hash assign)])
|
||||
(gen-assign var val #:declare #t)))
|
||||
(indent) (printf "~a = ~a;\n"
|
||||
(declare-var var)
|
||||
(spin-val->string val))))
|
||||
|
||||
;; SVar SValue [Bool] -> Void
|
||||
(define (gen-assign var val #:declare [declare? #f])
|
||||
(indent) (printf "~a = ~a;\n"
|
||||
(if declare? (var-decl var) (svar-name var))
|
||||
(spin-val->string val)))
|
||||
|
||||
;; SVar -> String
|
||||
(define (var-decl var)
|
||||
;; SVar -> Void
|
||||
(define (declare-var var)
|
||||
(match-define (svar name ty) var)
|
||||
(format "~a ~a" (spin-type->string ty) name))
|
||||
|
||||
|
|
@ -812,7 +665,7 @@
|
|||
;; SType -> String
|
||||
(define (spin-type->string ty)
|
||||
(match ty
|
||||
[(== SInt) "short"]
|
||||
[(== SInt) "int"]
|
||||
[(== SBool) "bool"]
|
||||
[(== mtype) "mtype"]))
|
||||
|
||||
|
|
@ -856,11 +709,7 @@
|
|||
;; (τ -> Any) SName NameEnvironment -> String
|
||||
(define (embed-value-as-comment tag sname name-env)
|
||||
(define ty (reverse-lookup name-env sname))
|
||||
(format-as-comment (tag ty)))
|
||||
|
||||
;; Any -> String
|
||||
(define (format-as-comment v)
|
||||
(format "/*~a*/" v))
|
||||
(format "/*~a*/" (tag ty)))
|
||||
|
||||
;; NameEnvironment SName -> τ
|
||||
(define (reverse-lookup name-env sname)
|
||||
|
|
@ -868,35 +717,6 @@
|
|||
#:when (equal? v sname))
|
||||
k))
|
||||
|
||||
;; String -> String
|
||||
;; format a suitable end label based on the process/state name
|
||||
(define (format-end-label s)
|
||||
(format "end_~a" s))
|
||||
|
||||
;; SName -> SVar
|
||||
;; SVar for a process's clock
|
||||
(define (proc-clock-var proc-name)
|
||||
(svar (string->symbol (format "~a_clock" proc-name))
|
||||
SBool))
|
||||
|
||||
(define GLOBAL-CLOCK-VAR (svar 'GLOBAL_CLOCK SBool))
|
||||
(define GLOBAL-CLOCK-INIT-VAL #t)
|
||||
|
||||
;; SVar -> String
|
||||
(define (clock-predicate clock-var)
|
||||
(format "~a == ~a" (svar-name clock-var) (svar-name GLOBAL-CLOCK-VAR)))
|
||||
|
||||
;; SVar -> Void
|
||||
(define (update-clock clock [comment ""])
|
||||
(printf "~a = !~a;~a\n" (svar-name clock) (svar-name clock) comment))
|
||||
|
||||
;; (Listof SName) -> String
|
||||
(define (all-procs-ready-predicate clock-names)
|
||||
(define global-name (svar-name GLOBAL-CLOCK-VAR))
|
||||
(define preds (for/list ([cn (in-list clock-names)])
|
||||
(format "(~a != ~a)" global-name cn)))
|
||||
(string-join preds " && "))
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; LTL
|
||||
|
||||
|
|
@ -926,8 +746,6 @@
|
|||
(gen-ltl-bin-op "W" p q)]
|
||||
[(strong-until p q)
|
||||
(gen-ltl-bin-op "U" p q)]
|
||||
[(release p q)
|
||||
(gen-ltl-bin-op "V" p q)]
|
||||
[(ltl-implies p q)
|
||||
(gen-ltl-bin-op "->" p q)]
|
||||
[(ltl-and p q)
|
||||
|
|
@ -957,17 +775,12 @@
|
|||
(indent) (display "(") (gen-ltl q) (displayln ")"))
|
||||
|
||||
;; Assignment -> Void
|
||||
;; SPIN sometimes errors (seemingly in the front end) if this is "too big." What
|
||||
;; constitutes too big seems to change. At first setting the limit to 33 worked,
|
||||
;; but then I lowered it again, so IDK. It gives an error message like:
|
||||
;; tl_spin: expected ')', saw 'predicate'
|
||||
(define (gen-sanity-ltl assignment)
|
||||
(gen-spec "sanity"
|
||||
(lambda ()
|
||||
(indent) (displayln "[](")
|
||||
(with-indent
|
||||
(for ([assertion-var (in-hash-keys assignment)]
|
||||
[i (in-range 14)])
|
||||
(for ([assertion-var (in-hash-keys assignment)])
|
||||
(indent) (printf "~a >= 0 &&\n" (svar-name assertion-var)))
|
||||
(indent) (displayln "true"))
|
||||
(indent) (displayln ")"))))
|
||||
|
|
@ -980,38 +793,25 @@
|
|||
|
||||
;; [LTL τ] [Listof Role] -> Bool
|
||||
(define (compile+verify spec roles)
|
||||
(let/ec stop
|
||||
(define role-graphs
|
||||
(for/list ([r (in-list roles)])
|
||||
(define ans (compile/internal-events (compile r)))
|
||||
(when (detected-cycle? ans)
|
||||
(printf "detected cycle!\n")
|
||||
(describe-detected-cycle ans)
|
||||
(stop #f))
|
||||
ans))
|
||||
(run-spin (program->spin role-graphs spec))))
|
||||
(define role-graphs (for/list ([r (in-list roles)]) (compile/internal-events (compile r))))
|
||||
(run-spin (program->spin role-graphs spec)))
|
||||
|
||||
;; SpinThang String -> Bool
|
||||
(define (run-spin spin [spec-name "spec"])
|
||||
(define tmp (make-temporary-file "typed-syndicate-spin~a.pml"))
|
||||
(gen-spin/to-file spin tmp)
|
||||
(define-values (script-completed? script-output script-err)
|
||||
(run-script RUN-SPIN.EXE (list tmp spec-name)))
|
||||
(define out (with-output-to-string
|
||||
(thunk (system* RUN-SPIN.EXE tmp spec-name))))
|
||||
(define trail-file (format "~a.trail" (path->string tmp)))
|
||||
(define trail-exists? (file-exists? trail-file))
|
||||
(cond
|
||||
[(not script-completed?)
|
||||
(displayln "Error running SPIN; Output:")
|
||||
(display script-err)
|
||||
(display script-output)]
|
||||
[trail-exists?
|
||||
(displayln "Detected Trail File!")
|
||||
(copy-file tmp (build-path (current-directory) "model.pml") #t)
|
||||
(copy-file trail-file (build-path (current-directory) "model.pml.trail") #t)
|
||||
(analyze-spin-trail tmp)
|
||||
(delete-file trail-file)])
|
||||
(when (file-exists? trail-file)
|
||||
(displayln "Detected Trail File!")
|
||||
(analyze-spin-trail tmp)
|
||||
(copy-file tmp (build-path (current-directory) "model.pml") #t)
|
||||
(copy-file trail-file (build-path (current-directory) "model.pml.trail") #t)
|
||||
(delete-file trail-file))
|
||||
(delete-file tmp)
|
||||
(and script-completed? (not trail-exists?)))
|
||||
(not trail-exists?))
|
||||
|
||||
(define SPIN-REPORT-RX #px"(?m:^State-vector \\d+ byte, depth reached \\d+, errors: (\\d+)$)")
|
||||
|
||||
|
|
@ -1029,32 +829,19 @@ Examples:
|
|||
4: proc 2 (proc824:1) model.pml:140 (state 2) [ClubMemberT_String_assertions = (ClubMemberT_String_assertions+1)]
|
||||
<<<<<START OF CYCLE>>>>>
|
||||
|#
|
||||
(define TRAIL-LINE-RX #px"(?m:^\\s*<<<<<START OF CYCLE>>>>>|^\\s*\\d+:\\s*proc\\s*(\\d+)\\s*\\(.*\\) \\S+\\.pml:(\\d+))")
|
||||
(define TRAIL-LINE-RX #px"(?m:^ <<<<<START OF CYCLE>>>>>|^\\s*\\d+:\\s*proc\\s*(\\d+)\\s*\\(.*\\) \\S+\\.pml:(\\d+))")
|
||||
|
||||
;; Path -> Void
|
||||
;; assume the trail file exists in the same directory as the spin (model) file
|
||||
(define (analyze-spin-trail spin-file)
|
||||
(define-values (_ out __) (run-script REPLAY-TRAIL.EXE (list spin-file)))
|
||||
#;(pretty-display out)
|
||||
(define trace (spin-trace->syndicate-trace out spin-file))
|
||||
(print-trace trace)
|
||||
#;(log-trace-msd trace))
|
||||
|
||||
;; String Path -> (Listof TraceStep)
|
||||
(define (spin-trace->syndicate-trace spin-out spin-file)
|
||||
(define pid/line-trace (regexp-match* TRAIL-LINE-RX spin-out #:match-select cdr))
|
||||
(define out (with-output-to-string
|
||||
(thunk (system* REPLAY-TRAIL.EXE spin-file))))
|
||||
(pretty-display out)
|
||||
(define pid/line-trace (regexp-match* TRAIL-LINE-RX out #:match-select cdr))
|
||||
(define model-lines (file->vector spin-file))
|
||||
(interpret-spin-trace pid/line-trace model-lines))
|
||||
|
||||
;; String (Listof String) -> (Values Bool String String)
|
||||
(define (run-script cmd args)
|
||||
(match-define (list stdo stdin pid stderr ctrl)
|
||||
(apply process* cmd args))
|
||||
(define script-output (port->string stdo))
|
||||
(define script-err (port->string stderr))
|
||||
(define script-completed? (equal? (ctrl 'status) 'done-ok))
|
||||
(close-output-port stdin)
|
||||
(values script-completed? script-output script-err))
|
||||
(define trace (interpret-spin-trace pid/line-trace model-lines))
|
||||
(print-trace trace)
|
||||
(log-trace-msd trace))
|
||||
|
||||
;; a PID is a Nat
|
||||
|
||||
|
|
@ -1069,13 +856,6 @@ Examples:
|
|||
;; - (retract τ)
|
||||
;; - (Asserted τ)
|
||||
;; - (Retracted τ)
|
||||
;; - 'dstep
|
||||
;; - 'turn-begin
|
||||
|
||||
;; the first statement in a d_step sequence (possibly atomic too) has the line
|
||||
;; number of the d_step block itself in the trace
|
||||
(define DSTEP-EVENT 'dstep)
|
||||
(define TURN-BEGIN-EVENT 'turn-begin)
|
||||
|
||||
;; (Listof (List String String)) (Vectorof String) -> (Listof TraceStep)
|
||||
(define (interpret-spin-trace pid/line-trace model-lines)
|
||||
|
|
@ -1085,102 +865,71 @@ Examples:
|
|||
['(#f #f)
|
||||
START-OF-CYCLE]
|
||||
[(list pid-str line-no-str)
|
||||
(define line-no (string->number line-no-str))
|
||||
(extract-trace-step pid-str line-no model-lines)])))
|
||||
(define line (vector-ref model-lines (sub1 (string->number line-no-str))))
|
||||
(define evt (extract-comment-value line))
|
||||
(and evt
|
||||
(trace-step (string->number pid-str) evt))]
|
||||
)))
|
||||
(filter values maybe-steps))
|
||||
|
||||
;; String Nat (Vectorof String) -> (Maybe TraceEvent)
|
||||
(define (extract-trace-step pid-str line-no model-lines)
|
||||
(define line (vector-ref model-lines (sub1 line-no)))
|
||||
(define evt (extract-comment-value line))
|
||||
(cond
|
||||
[(equal? evt DSTEP-EVENT)
|
||||
(extract-trace-step pid-str (add1 line-no) model-lines)]
|
||||
[evt
|
||||
(trace-step (string->number pid-str) evt)]
|
||||
[else
|
||||
#f]))
|
||||
|
||||
;; (Listof TraceStep) -> Void
|
||||
(define (print-trace trace)
|
||||
(when (empty? trace)
|
||||
(printf "Starting state of program violates specification\n"))
|
||||
(for ([ts (in-list trace)])
|
||||
(match ts
|
||||
[(== START-OF-CYCLE)
|
||||
(printf "Start of Cycle (if this is the last step that means the final state is stuttered):\n")]
|
||||
[(trace-step pid evt)
|
||||
(match evt
|
||||
[(== TURN-BEGIN-EVENT)
|
||||
(printf "A new turn begins\n")]
|
||||
[(== DSTEP-EVENT)
|
||||
(printf "\nERROR ERROR!! SAW DSTEP EVENT!! ERROR ERROR\n\n")]
|
||||
[(assert ty)
|
||||
(printf "Process ~a ASSERTS ~a\n" pid (τ->string ty))]
|
||||
[(retract ty)
|
||||
(printf "Process ~a RETRACTS ~a\n" pid (τ->string ty))]
|
||||
[(send ty)
|
||||
(printf "Process ~a SENDS ~a\n" pid (τ->string ty))]
|
||||
[(Asserted ty)
|
||||
(printf "Process ~a REACTS to the ASSERTION of ~a\n" pid (τ->string ty))]
|
||||
[(Retracted ty)
|
||||
(printf "Process ~a REACTS to the RETRACTION of ~a\n" pid (τ->string ty))]
|
||||
[(Message ty)
|
||||
(printf "Process ~a REACTS to the MESSAGE of ~a\n" pid (τ->string ty))])])))
|
||||
(printf "Process ~a REACTS to the RETRACTION of ~a\n" pid (τ->string ty))])])))
|
||||
|
||||
;; (Listof TraceStep) -> Void
|
||||
;; use syndicate's msd logger logging
|
||||
(define (log-trace-msd trace)
|
||||
(start-tracing! "trace.msd")
|
||||
(define (end-turn! pid point patch messages)
|
||||
(define (end-turn! pid point patch)
|
||||
(let* ([p (trace-turn-end point pid #f)]
|
||||
[p (trace-actions-produced p pid (cons patch messages))]
|
||||
[p (trace-actions-produced p pid (list patch))]
|
||||
[p (trace-action-interpreted p pid patch)])
|
||||
p))
|
||||
(define-values (final-pid final-point final-patch final-messages)
|
||||
(define-values (final-pid final-point final-patch)
|
||||
(for/fold ([current-actor #f]
|
||||
[point #f]
|
||||
[current-patch synd:patch-empty]
|
||||
[messages (list)])
|
||||
[current-patch synd:patch-empty])
|
||||
([ts (in-list trace)])
|
||||
(match ts
|
||||
[(== START-OF-CYCLE)
|
||||
(values current-actor point current-patch messages)]
|
||||
(values current-actor point current-patch)]
|
||||
[(trace-step pid evt)
|
||||
(define-values (next-point next-patch)
|
||||
(cond
|
||||
;; either startup or the begin of a new actor's turn
|
||||
[(and current-actor (not (equal? pid current-actor)))
|
||||
(define p (end-turn! current-actor point current-patch messages))
|
||||
(define p (end-turn! current-actor point current-patch))
|
||||
(values (trace-turn-begin p pid #f)
|
||||
synd:patch-empty)]
|
||||
[else
|
||||
(values point current-patch)]))
|
||||
(match evt
|
||||
[(== DSTEP-EVENT)
|
||||
(printf "\nERROR ERROR!! SAW DSTEP EVENT!! ERROR ERROR\n\n")]
|
||||
[(assert ty)
|
||||
(define p (synd:assert ty))
|
||||
(values pid next-point (synd:patch-seq next-patch p) messages)]
|
||||
(values pid next-point (synd:patch-seq next-patch p))]
|
||||
[(retract ty)
|
||||
(define p (synd:retract ty))
|
||||
(values pid next-point (synd:patch-seq next-patch p) messages)]
|
||||
[(send ty)
|
||||
(define a (synd:message ty))
|
||||
(values pid next-point next-patch (cons a messages))]
|
||||
(values pid next-point (synd:patch-seq next-patch p))]
|
||||
[(Asserted ty)
|
||||
#;(trace-event-consumed ??? ??? pid ???)
|
||||
(values pid next-point next-patch messages)]
|
||||
(values pid next-point next-patch)]
|
||||
[(Retracted ty)
|
||||
#;(trace-event-consumed ??? ??? pid ???)
|
||||
(values pid next-point next-patch messages)]
|
||||
[(Message ty)
|
||||
#;(trace-event-consumed ??? ??? pid ???)
|
||||
(values pid next-point next-patch messages)]
|
||||
[(or (== TURN-BEGIN-EVENT)
|
||||
(== DSTEP-EVENT))
|
||||
(values pid next-point next-patch messages)])])))
|
||||
(end-turn! final-pid final-point final-patch final-messages))
|
||||
(values pid next-point next-patch)])])))
|
||||
(end-turn! final-pid final-point final-patch))
|
||||
|
||||
(define COMMENT-RX #px"/\\*(.*)\\*/")
|
||||
|
||||
|
|
@ -1195,13 +944,10 @@ Examples:
|
|||
"extracting values back out from spin model"
|
||||
(define evt-str " :: ASSERTED(BookQuoteT_String_Int) && !know_BookQuoteT_String_Int -> /*#s(Asserted #s(Struct BookQuoteT (#s(Base String) #s(Base Int))))*/\n")
|
||||
(define assert-str " ASSERT(Obs_Obs_BookInterestT); /*#s(assert #s(Observe #s(Observe #s(Struct BookInterestT (#s(Base String) #s(Mk⋆) #s(Mk⋆))))))*/\n")
|
||||
(define send-str " SEND(FlipSwitchCmdT_Symbol); /*#s(send #s(Struct FlipSwitchCmdT (#s(Base Symbol))))*/\n")
|
||||
(check-equal? (extract-comment-value evt-str)
|
||||
#s(Asserted #s(Struct BookQuoteT (#s(Base String) #s(Base Int)))))
|
||||
(check-equal? (extract-comment-value assert-str)
|
||||
#s(assert #s(Observe #s(Observe #s(Struct BookInterestT (#s(Base String) #s(Mk⋆) #s(Mk⋆)))))))
|
||||
(check-equal? (extract-comment-value send-str)
|
||||
#s(send #s(Struct FlipSwitchCmdT (#s(Base Symbol)))))))
|
||||
#s(assert #s(Observe #s(Observe #s(Struct BookInterestT (#s(Base String) #s(Mk⋆) #s(Mk⋆)))))))))
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Misc Utils
|
||||
|
|
|
|||
|
|
@ -44,30 +44,39 @@
|
|||
|
||||
;; copied from stlc
|
||||
(define-typed-syntax (ann e (~optional (~datum :)) τ:type) ≫
|
||||
[⊢ e ≫ e- (⇐ : τ.norm) (⇒ ν (~effs eff ...))]
|
||||
[⊢ e ≫ e- (⇐ : τ.norm)]
|
||||
#:fail-unless (pure? #'e-) "expression must be pure"
|
||||
------------------------------------------------
|
||||
[⊢ e- (⇒ : τ.norm) (⇒ ν (eff ...))])
|
||||
[⊢ e- (⇒ : τ.norm) ])
|
||||
|
||||
;; copied from ext-stlc
|
||||
(define-typed-syntax if
|
||||
[(_ e_tst e1 e2) ⇐ τ-expected ≫
|
||||
[⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy.
|
||||
#:fail-unless (pure? #'e_tst-) "expression must be pure"
|
||||
[⊢ e1 ≫ e1- (⇐ : τ-expected) (⇒ ν (~effs eff1 ...))]
|
||||
[⊢ e2 ≫ e2- (⇐ : τ-expected) (⇒ ν (~effs eff2 ...))]
|
||||
[⊢ e1 ≫ e1- (⇐ : τ-expected)
|
||||
(⇒ ν-ep (~effs eps1 ...)) (⇒ ν-f (~effs fs1 ...)) (⇒ ν-s (~effs ss1 ...))]
|
||||
[⊢ e2 ≫ e2- (⇐ : τ-expected)
|
||||
(⇒ ν-ep (~effs eps2 ...)) (⇒ ν-f (~effs fs2 ...)) (⇒ ν-s (~effs ss2 ...))]
|
||||
--------
|
||||
[⊢ (if- e_tst- e1- e2-)
|
||||
(⇒ : τ-expected)
|
||||
(⇒ ν #,(make-Branch #'((eff1 ...) (eff2 ...))))]]
|
||||
(⇒ ν-ep (eps1 ... eps2 ...))
|
||||
(⇒ ν-f #,(make-Branch #'((fs1 ...) (fs2 ...))))
|
||||
(⇒ ν-s (ss1 ... ss2 ...))]]
|
||||
[(_ e_tst e1 e2) ≫
|
||||
[⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy.
|
||||
#:fail-unless (pure? #'e_tst-) "expression must be pure"
|
||||
[⊢ e1 ≫ e1- (⇒ : τ1) (⇒ ν (~effs eff1 ...))]
|
||||
[⊢ e2 ≫ e2- (⇒ : τ2) (⇒ ν (~effs eff2 ...))]
|
||||
[⊢ e1 ≫ e1- (⇒ : τ1)
|
||||
(⇒ ν-ep (~effs eps1 ...)) (⇒ ν-f (~effs fs1 ...)) (⇒ ν-s (~effs ss1 ...))]
|
||||
[⊢ e2 ≫ e2- (⇒ : τ2)
|
||||
(⇒ ν-ep (~effs eps2 ...)) (⇒ ν-f (~effs fs2 ...)) (⇒ ν-s (~effs ss2 ...))]
|
||||
#:with τ (mk-U- #'(τ1 τ2))
|
||||
--------
|
||||
[⊢ (if- e_tst- e1- e2-) (⇒ : τ)
|
||||
(⇒ ν #,(make-Branch #'((eff1 ...) (eff2 ...))))]])
|
||||
(⇒ ν-ep (eps1 ... eps2 ...))
|
||||
(⇒ ν-f #,(make-Branch #'((fs1 ...) (fs2 ...))))
|
||||
(⇒ ν-s (ss1 ... ss2 ...))]])
|
||||
|
||||
(define-typed-syntax (when e s ...+) ≫
|
||||
------------------------------------
|
||||
|
|
@ -84,18 +93,26 @@
|
|||
[⊢ e ≫ e- ⇒ : τ_x] ...
|
||||
#:fail-unless (stx-andmap pure? #'(e- ...)) "expressions must be pure"
|
||||
[[x ≫ x- : τ_x] ... ⊢ (block e_body ...) ≫ e_body- (⇐ : τ_expected)
|
||||
(⇒ ν (~effs eff ...))]
|
||||
(⇒ ν-ep (~effs eps ...))
|
||||
(⇒ ν-f (~effs fs ...))
|
||||
(⇒ ν-s (~effs ss ...))]
|
||||
----------------------------------------------------------
|
||||
[⊢ (let- ([x- e-] ...) e_body-) (⇒ : τ_expected)
|
||||
(⇒ ν (eff ...))]]
|
||||
(⇒ ν-ep (eps ...))
|
||||
(⇒ ν-f (fs ...))
|
||||
(⇒ ν-s (ss ...))]]
|
||||
[(_ ([x e] ...) e_body ...) ≫
|
||||
[⊢ e ≫ e- ⇒ : τ_x] ...
|
||||
#:fail-unless (stx-andmap pure? #'(e- ...)) "expressions must be pure"
|
||||
[[x ≫ x- : τ_x] ... ⊢ (block e_body ...) ≫ e_body- (⇒ : τ_body)
|
||||
(⇒ ν (~effs eff ...))]
|
||||
(⇒ ν-ep (~effs eps ...))
|
||||
(⇒ ν-f (~effs fs ...))
|
||||
(⇒ ν-s (~effs ss ...))]
|
||||
----------------------------------------------------------
|
||||
[⊢ (let- ([x- e-] ...) e_body-) (⇒ : τ_body)
|
||||
(⇒ ν (eff ...))]])
|
||||
(⇒ ν-ep (eps ...))
|
||||
(⇒ ν-f (fs ...))
|
||||
(⇒ ν-s (ss ...))]])
|
||||
|
||||
;; copied from ext-stlc
|
||||
(define-typed-syntax let*
|
||||
|
|
@ -110,10 +127,14 @@
|
|||
[⊢ pred ≫ pred- (⇐ : Bool)] ...
|
||||
#:fail-unless (stx-andmap pure? #'(pred- ...)) "predicates must be pure"
|
||||
[⊢ (block s ...) ≫ s- (⇒ : τ-s)
|
||||
(⇒ ν (~effs eff ...))] ...
|
||||
(⇒ ν-ep (~effs eps ...))
|
||||
(⇒ ν-f (~effs fs ...))
|
||||
(⇒ ν-s (~effs ss ...))] ...
|
||||
------------------------------------------------
|
||||
[⊢ (cond- [pred- s-] ...) (⇒ : (U τ-s ...))
|
||||
(⇒ ν #,(make-Branch #'((eff ...) ...)))])
|
||||
(⇒ ν-ep (eps ... ...))
|
||||
(⇒ ν-f #,(make-Branch #'((fs ...) ...)))
|
||||
(⇒ ν-s (ss ... ...))])
|
||||
|
||||
(define else #t)
|
||||
|
||||
|
|
@ -124,7 +145,9 @@
|
|||
(elaborate-pattern/with-type pat #'τ-e))
|
||||
#:with (([x τ:type] ...) ...) (stx-map pat-bindings #'(p/e ...))
|
||||
[[x ≫ x- : τ.norm] ... ⊢ (block s ...) ≫ s- (⇒ : τ-s)
|
||||
(⇒ ν (~effs eff ...))] ...
|
||||
(⇒ ν-ep (~effs eps ...))
|
||||
(⇒ ν-f (~effs fs ...))
|
||||
(⇒ ν-s (~effs ss ...))] ...
|
||||
;; REALLY not sure how to handle p/p-/p.match-pattern,
|
||||
;; particularly w.r.t. typed terms that appear in p.match-pattern
|
||||
[⊢ p/e ≫ p-- ⇒ τ-p] ...
|
||||
|
|
@ -138,7 +161,9 @@
|
|||
[⊢ (match- e- [p- s-] ...
|
||||
[_ (#%app- error- "incomplete pattern match")])
|
||||
(⇒ : (U τ-s ...))
|
||||
(⇒ ν #,(make-Branch #'((eff ...) ...)))])
|
||||
(⇒ ν-ep #,(make-Branch #'((eps ...) ...)))
|
||||
(⇒ ν-f #,(make-Branch #'((fs ...) ...)))
|
||||
(⇒ ν-s #,(make-Branch #'((ss ...) ...)))])
|
||||
|
||||
|
||||
;; (Listof Value) -> Value
|
||||
|
|
@ -146,21 +171,21 @@
|
|||
(#%app- cons- 'tuple es))
|
||||
|
||||
(define-typed-syntax (tuple e:expr ...) ≫
|
||||
[⊢ e ≫ e- (⇒ : τ) (⇒ ν (~effs F ...))] ...
|
||||
[⊢ e ≫ e- (⇒ : τ)] ...
|
||||
#:fail-unless (stx-andmap pure? #'(e- ...)) "expressions not allowed to have effects"
|
||||
-----------------------
|
||||
[⊢ (#%app- mk-tuple (#%app- list- e- ...))
|
||||
(⇒ : (Tuple τ ...))
|
||||
(⇒ ν (F ... ...))])
|
||||
[⊢ (#%app- mk-tuple (#%app- list- e- ...)) (⇒ : (Tuple τ ...))])
|
||||
|
||||
(define unit : Unit (tuple))
|
||||
|
||||
(define-typed-syntax (select n:nat e:expr) ≫
|
||||
[⊢ e ≫ e- (⇒ : (~Tuple τ ...)) (⇒ ν (~effs F ...))]
|
||||
[⊢ e ≫ e- (⇒ : (~Tuple τ ...))]
|
||||
#:fail-unless (pure? #'e-) "expression not allowed to have effects"
|
||||
#:do [(define i (syntax->datum #'n))]
|
||||
#:fail-unless (< i (stx-length #'(τ ...))) "index out of range"
|
||||
#:with τr (list-ref (stx->list #'(τ ...)) i)
|
||||
--------------------------------------------------------------
|
||||
[⊢ (#%app- tuple-select n e-) (⇒ : τr) (⇒ ν (F ...))])
|
||||
[⊢ (#%app- tuple-select n e-) (⇒ : τr)])
|
||||
|
||||
(define- (tuple-select n t)
|
||||
(#%app- list-ref- t (#%app- add1- n)))
|
||||
|
|
@ -239,15 +264,8 @@
|
|||
(quasisyntax/loc pat
|
||||
(tuple #,@(stx-map elaborate-pattern #'(p ...))))]
|
||||
[(~constructor-exp ctor p ...)
|
||||
(define field-tys (ctor-field-tys #'ctor))
|
||||
(define sub-pats
|
||||
(for/list ([field-pat (in-syntax #'(p ...))]
|
||||
[field-ty? (in-list field-tys)])
|
||||
(if field-ty?
|
||||
(elaborate-pattern/with-type field-pat field-ty?)
|
||||
(elaborate-pattern field-pat))))
|
||||
(quasisyntax/loc pat
|
||||
(ctor #,@sub-pats))]
|
||||
(ctor #,@(stx-map elaborate-pattern #'(p ...))))]
|
||||
[e:expr
|
||||
#'e]))
|
||||
|
||||
|
|
@ -358,6 +376,7 @@
|
|||
[⊢ e ≫ e- (⇒ (~Tuple τ ...))]
|
||||
#:fail-unless (stx-length=? #'(x ...) #'(τ ...))
|
||||
"mismatched size"
|
||||
#:fail-unless (pure? #'e-) "expr must be pure"
|
||||
#:with (sel ...) (for/list ([y (in-syntax #'(x ...))]
|
||||
[t (in-syntax #'(τ ...))]
|
||||
[i (in-naturals)])
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load Diff
|
|
@ -62,7 +62,7 @@
|
|||
(U (Observe (Observe (TcpConnection ★/t (TcpListener ★/t))))
|
||||
(Observe (TcpConnection ★/t (TcpListener Int)))
|
||||
(Observe (TcpConnection ★/t (TcpListener Int)))
|
||||
(Advertise (Observe (TcpChannel ★/t (TcpListener (TcpHandle (Seal ★/t))) ★/t)))
|
||||
(Advertise (Observe (TcpChannel ★/t (TcpListener (TcpHandle (Seal ★/t)) ★/t))))
|
||||
(Observe (Advertise (TcpChannel (TcpAddress String Int) (TcpHandle (Seal ★/t)) ★/t)))
|
||||
(TcpAccepted ★/t)
|
||||
(Advertise (TcpChannel (TcpHandle (Seal ★/t)) (TcpAddress String Int) ★/t))
|
||||
|
|
@ -102,7 +102,7 @@
|
|||
|
||||
(require/typed syndicate/drivers/tcp2)
|
||||
(require/typed (submod syndicate/drivers/tcp2 syndicate-main)
|
||||
[activate! : (proc → (U) #:effects ((Actor Tcp2Driver))) #;(→ (Computation (Value (U))
|
||||
[activate! : (→ (Computation (Value (U))
|
||||
(Endpoints)
|
||||
(Roles)
|
||||
(Spawns (Actor Tcp2Driver))))])
|
||||
|
|
|
|||
|
|
@ -12,7 +12,7 @@
|
|||
(require (only-in "list.rkt" List ~List))
|
||||
(require (only-in "set.rkt" Set ~Set))
|
||||
(require (only-in "hash.rkt" Hash ~Hash))
|
||||
(require (only-in "prim.rkt" Int Bool + #%datum))
|
||||
(require (only-in "prim.rkt" Bool + #%datum))
|
||||
(require (only-in "core-expressions.rkt" let unit tuple-select mk-tuple))
|
||||
(require "maybe.rkt")
|
||||
|
||||
|
|
@ -139,14 +139,18 @@
|
|||
[[[x ≫ x-- : τ] ...]
|
||||
[[acc ≫ acc- : τ-acc] ...] ⊢ (block e-body ...) ≫ e-body-
|
||||
(⇐ : body-ty)
|
||||
(⇒ ν (~effs F ...))]
|
||||
(⇒ ν-ep (~effs τ-ep ...))
|
||||
(⇒ ν-s (~effs τ-s ...))
|
||||
(⇒ ν-f (~effs τ-f ...))]
|
||||
-------------------------------------------------------
|
||||
[⊢ (values->tuple #,num-accs
|
||||
(for/fold- ([acc- init-] ...)
|
||||
clauses-
|
||||
#,(bind-renames #'([x-- x-] ...) #`(tuple->values #,num-accs e-body-))))
|
||||
(⇒ : body-ty)
|
||||
(⇒ ν (F ...))]]
|
||||
(⇒ ν-ep (τ-ep ...))
|
||||
(⇒ ν-s (τ-s ...))
|
||||
(⇒ ν-f (τ-f ...))]]
|
||||
[(for/fold (accs ... [acc:id init] more-accs ...)
|
||||
clauses
|
||||
e-body ...+) ≫
|
||||
|
|
@ -204,17 +208,21 @@
|
|||
#:with (clauses- ([x x- τ] ...)) (analyze-for-clauses #'(clause.parend ...))
|
||||
[[x ≫ x-- : τ] ... ⊢ (block e-body ...) ≫ e-body-
|
||||
(⇒ : τ-body)
|
||||
(⇒ ν (~effs F ...))]
|
||||
(⇒ ν-ep (~effs τ-ep ...))
|
||||
(⇒ ν-s (~effs τ-s ...))
|
||||
(⇒ ν-f (~effs τ-f ...))]
|
||||
----------------------------------------------------------------------
|
||||
[⊢ (for/set- clauses-
|
||||
#,(bind-renames #'([x-- x-] ...) #'e-body-))
|
||||
(⇒ : (Set τ-body))
|
||||
(⇒ ν (F ...))])
|
||||
(⇒ ν-ep (τ-ep ...))
|
||||
(⇒ ν-s (τ-s ...))
|
||||
(⇒ ν-f (τ-f ...))])
|
||||
|
||||
(define-typed-syntax (for/sum (clause ...)
|
||||
e-body ...+) ≫
|
||||
----------------------------------------------------------------------
|
||||
[≻ (for/fold ([acc Int 0])
|
||||
[≻ (for/fold ([acc 0])
|
||||
(clause ...)
|
||||
(+ acc (let () e-body ...)))])
|
||||
|
||||
|
|
@ -231,7 +239,9 @@
|
|||
#:with (clauses- ([x x- τ] ...)) (analyze-for-clauses #'(clause.parend ...))
|
||||
[[x ≫ x-- : τ] ... ⊢ (block e-body ...) ≫ e-body-
|
||||
(⇒ : τ-body)
|
||||
(⇒ ν (~effs F ...))]
|
||||
(⇒ ν-ep (~effs τ-ep ...))
|
||||
(⇒ ν-s (~effs τ-s ...))
|
||||
(⇒ ν-f (~effs τ-f ...))]
|
||||
[[res ≫ _ : τ-body] ⊢ res ≫ res- (⇒ : _)]
|
||||
----------------------------------------------------------------------
|
||||
[⊢ (let- ()
|
||||
|
|
@ -242,4 +252,6 @@
|
|||
(some res-)
|
||||
none))
|
||||
(⇒ : (Maybe τ-body))
|
||||
(⇒ ν (F ...))])
|
||||
(⇒ ν-ep (τ-ep ...))
|
||||
(⇒ ν-s (τ-s ...))
|
||||
(⇒ ν-f (τ-f ...))])
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@
|
|||
(for-syntax ~List)
|
||||
list
|
||||
(typed-out [[empty- : (List ⊥)] empty]
|
||||
[[empty?- : (∀ (X) (→fn (List X) Bool))] empty?]
|
||||
[[empty?- : (∀ (X) (→fn X (List X) Bool))] empty?]
|
||||
[[cons- : (∀ (X) (→fn X (List X) (List X)))] cons]
|
||||
[[cons?- : (∀ (X) (→fn X (List X) Bool))] cons?]
|
||||
[[first- : (∀ (X) (→fn (List X) X))] first]
|
||||
|
|
|
|||
|
|
@ -7,10 +7,9 @@
|
|||
;; - (eventually [LTL X])
|
||||
;; - (weak-until [LTL X] [LTL X])
|
||||
;; - (strong-until [LTL X] [LTL X])
|
||||
;; - (release [LTL X] [LTL X])
|
||||
;; - (ltl-implies [LTL X] [LTL X])
|
||||
;; - (ltl-and [LTL X] [LTL X])
|
||||
;; - (ltl-or [LTL X] [LTL X])
|
||||
;; - (ltl-and [Listof [LTL X]])
|
||||
;; - (ltl-or [Listof [LTL X]])
|
||||
;; - (ltl-not [LTL X])
|
||||
;; - (atomic X)
|
||||
;; - Bool
|
||||
|
|
@ -21,7 +20,6 @@
|
|||
(struct atomic [p] #:prefab)
|
||||
(struct weak-until [p q] #:prefab)
|
||||
(struct strong-until [p q] #:prefab)
|
||||
(struct release [p q] #:prefab)
|
||||
(struct ltl-implies [p q] #:prefab)
|
||||
(struct ltl-and [p q] #:prefab)
|
||||
(struct ltl-or [p q] #:prefab)
|
||||
|
|
@ -39,8 +37,6 @@
|
|||
(weak-until (loop p) (loop q))]
|
||||
[(strong-until p q)
|
||||
(strong-until (loop p) (loop q))]
|
||||
[(release p q)
|
||||
(release (loop p) (loop q))]
|
||||
[(ltl-implies p q)
|
||||
(ltl-implies (loop p) (loop q))]
|
||||
[(ltl-and p q)
|
||||
|
|
|
|||
|
|
@ -5,12 +5,9 @@
|
|||
None*
|
||||
Some
|
||||
some
|
||||
none
|
||||
has?)
|
||||
none)
|
||||
|
||||
(require "core-types.rkt")
|
||||
(require "prim.rkt")
|
||||
(require "core-expressions.rkt")
|
||||
|
||||
|
||||
(define-constructor* (none* : None*))
|
||||
|
|
@ -38,10 +35,3 @@
|
|||
(error "some")]
|
||||
[none
|
||||
(error "none")]))
|
||||
|
||||
(define (∀ (X) (has? [v : (Maybe X)] [p : (→fn X Bool)] -> Bool))
|
||||
(match v
|
||||
[none
|
||||
#f]
|
||||
[(some $x)
|
||||
(p x)]))
|
||||
|
|
|
|||
|
|
@ -1,31 +1,28 @@
|
|||
#lang turnstile
|
||||
|
||||
(provide (all-defined-out)
|
||||
True False Bool
|
||||
(for-syntax (all-defined-out)))
|
||||
|
||||
(require "core-types.rkt")
|
||||
(require (rename-in racket/math [exact-truncate exact-truncate-]))
|
||||
(require (postfix-in - (only-in racket/format ~a ~v)))
|
||||
(require (postfix-in - (only-in racket/format ~a)))
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Primitives
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
|
||||
(define-base-types Zero NonZero String ByteString Symbol)
|
||||
|
||||
(define-type-alias Int (U Zero NonZero))
|
||||
(define-base-types Int Bool String ByteString Symbol)
|
||||
|
||||
;; hmmm
|
||||
(define-primop + (→fn Int Int Int))
|
||||
(define-primop - (→fn Int Int Int))
|
||||
(define-primop * (→fn Int Int Int))
|
||||
(define-primop not (→fn Bool Bool))
|
||||
(define-primop < (→fn Int Int Bool))
|
||||
(define-primop > (→fn Int Int Bool))
|
||||
(define-primop <= (→fn Int Int Bool))
|
||||
(define-primop >= (→fn Int Int Bool))
|
||||
(define-primop = (→fn Int Int Bool))
|
||||
(define-primop + (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns))))
|
||||
(define-primop - (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns))))
|
||||
(define-primop * (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns))))
|
||||
(define-primop not (→ Bool (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
|
||||
(define-primop < (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
|
||||
(define-primop > (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
|
||||
(define-primop <= (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
|
||||
(define-primop >= (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
|
||||
(define-primop = (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
|
||||
(define-primop even? (→fn Int Bool))
|
||||
(define-primop odd? (→fn Int Bool))
|
||||
(define-primop add1 (→fn Int Int))
|
||||
|
|
@ -38,11 +35,11 @@
|
|||
(define-primop current-inexact-milliseconds (→fn Int))
|
||||
(define-primop string=? (→fn String String Bool))
|
||||
|
||||
(define-primop bytes->string/utf-8 (→fn ByteString String))
|
||||
(define-primop string->bytes/utf-8 (→fn String ByteString))
|
||||
(define-primop gensym (→fn Symbol Symbol))
|
||||
(define-primop symbol->string (→fn Symbol String))
|
||||
(define-primop string->symbol (→fn String Symbol))
|
||||
(define-primop bytes->string/utf-8 (→ ByteString (Computation (Value String) (Endpoints) (Roles) (Spawns))))
|
||||
(define-primop string->bytes/utf-8 (→ String (Computation (Value ByteString) (Endpoints) (Roles) (Spawns))))
|
||||
(define-primop gensym (→ Symbol (Computation (Value Symbol) (Endpoints) (Roles) (Spawns))))
|
||||
(define-primop symbol->string (→ Symbol (Computation (Value String) (Endpoints) (Roles) (Spawns))))
|
||||
(define-primop string->symbol (→ String (Computation (Value Symbol) (Endpoints) (Roles) (Spawns))))
|
||||
|
||||
(define-typed-syntax (/ e1 e2) ≫
|
||||
[⊢ e1 ≫ e1- (⇐ : Int)]
|
||||
|
|
@ -99,35 +96,17 @@
|
|||
--------------------------------------------------
|
||||
[⊢ (#%app- ~a- e- ...) (⇒ : String)])
|
||||
|
||||
(define-typed-syntax (~v e ...) ≫
|
||||
[⊢ e ≫ e- (⇒ : τ)] ...
|
||||
#:fail-unless (stx-andmap flat-type? #'(τ ...))
|
||||
"expressions must be string-able"
|
||||
--------------------------------------------------
|
||||
[⊢ (#%app- ~v- e- ...) (⇒ : String)])
|
||||
|
||||
(define-typed-syntax (format s e ...) ≫
|
||||
[⊢ s ≫ s- (⇐ : String)]
|
||||
[⊢ e ≫ e- (⇒ : τ)] ...
|
||||
#:fail-unless (stx-andmap flat-type? #'(τ ...))
|
||||
"expressions must be string-able"
|
||||
--------------------------------------------------
|
||||
[⊢ (#%app- format- s- e- ...) (⇒ : String)])
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Basic Values
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
|
||||
(define-typed-syntax #%datum
|
||||
[(_ . n:integer) ≫
|
||||
#:with T (if (zero? (syntax-e #'n)) #'Zero #'NonZero)
|
||||
----------------
|
||||
[⊢ (#%datum- . n) (⇒ : T)]]
|
||||
[(_ . b:boolean)
|
||||
≫
|
||||
#:with T (if (syntax-e #'b) #'True #'False)
|
||||
[⊢ (#%datum- . n) (⇒ : Int)]]
|
||||
[(_ . b:boolean) ≫
|
||||
----------------
|
||||
[⊢ (#%datum- . b) (⇒ : T)]]
|
||||
[⊢ (#%datum- . b) (⇒ : Bool)]]
|
||||
[(_ . s:string) ≫
|
||||
----------------
|
||||
[⊢ (#%datum- . s) (⇒ : String)]])
|
||||
|
|
|
|||
|
|
@ -13,7 +13,6 @@
|
|||
;; Role Type Data Definitions
|
||||
|
||||
;; a FacetName is a symbol
|
||||
;; a Name is a Symbol
|
||||
|
||||
;; a T is one of
|
||||
;; - (Role FacetName (Listof EP)), also abbreviated as just Role
|
||||
|
|
@ -21,24 +20,19 @@
|
|||
;; - (Sends τ)
|
||||
;; - (Realizes τ)
|
||||
;; - (Stop FacetName Body)
|
||||
;; - (WriteField Name τ)
|
||||
(struct Role (nm eps) #:prefab)
|
||||
(struct Spawn (ty) #:prefab)
|
||||
(struct Sends (ty) #:prefab)
|
||||
(struct Realizes (ty) #:prefab)
|
||||
(struct Stop (nm body) #:prefab)
|
||||
(struct WriteField (nm ty) #:prefab)
|
||||
(struct ReadField (nm) #:prefab)
|
||||
|
||||
;; a EP is one of
|
||||
;; - (Reacts D Body), describing an event handler
|
||||
;; - (Shares τ), describing an assertion
|
||||
;; - (Know τ), describing an internal assertion
|
||||
;; - (Field Name τ), describing a field declaration
|
||||
(struct Reacts (evt body) #:prefab)
|
||||
(struct Shares (ty) #:prefab)
|
||||
(struct Know (ty) #:prefab)
|
||||
(struct Field (nm ty) #:prefab)
|
||||
|
||||
;; a Body describes actions carried out in response to some event, and
|
||||
;; is one of
|
||||
|
|
@ -90,8 +84,6 @@
|
|||
;; - ⋆
|
||||
;; - (Base Symbol)
|
||||
;; - (internal-label Symbol τ)
|
||||
;; - (VarTy Name (NEListof (List τ τ))), describing an assertion endpoint
|
||||
;; whose type varies depending on the type of the named field
|
||||
(struct U (tys) #:prefab)
|
||||
(struct Struct (nm tys) #:prefab)
|
||||
(struct Observe (ty) #:prefab)
|
||||
|
|
@ -100,7 +92,6 @@
|
|||
(struct Hash (ty-k ty-v) #:prefab)
|
||||
(struct Mk⋆ () #:prefab)
|
||||
(struct internal-label (actor-id ty) #:prefab)
|
||||
(struct VarTy (nm tys) #:prefab)
|
||||
;; TODO this might be a problem when used as a match pattern
|
||||
(define ⋆ (Mk⋆))
|
||||
(struct Base (name) #:prefab)
|
||||
|
|
@ -142,8 +133,8 @@
|
|||
;; a TransitionEffect is one of
|
||||
;; - (send τ)
|
||||
;; - (realize τ)
|
||||
(struct send (ty) #:prefab)
|
||||
(struct realize (ty) #:prefab)
|
||||
(struct send (ty) #:transparent)
|
||||
(struct realize (ty) #:transparent)
|
||||
|
||||
;; a TransitionDesc is a (Hashof D+ (Setof (Listof RoleEffect)), describing the
|
||||
;; possible ways an event (+/- of an assertion) can alter the facet tree.
|
||||
|
|
@ -213,14 +204,13 @@
|
|||
(values D txns)))
|
||||
(define assertions (assertions-in-state current assertion#))
|
||||
(define new-work
|
||||
(for*/set ([txns (in-hash-values transitions)]
|
||||
(for*/list ([txns (in-hash-values transitions)]
|
||||
[txn (in-set txns)]
|
||||
[st (in-value (transition-dest txn))]
|
||||
#:unless (or (equal? st current)
|
||||
(hash-has-key? states st)
|
||||
(member st more)))
|
||||
#:unless (equal? st current)
|
||||
#:unless (hash-has-key? states st))
|
||||
st))
|
||||
(loop (append more (set->list new-work))
|
||||
(loop (append more new-work)
|
||||
(hash-set states current (state current transitions assertions)))]
|
||||
['()
|
||||
(role-graph (set (Role-nm role)) states)])))
|
||||
|
|
@ -387,15 +377,6 @@
|
|||
(set)
|
||||
(hash))))
|
||||
|
||||
#|
|
||||
(define input (file->value "va2.rktd"))
|
||||
(define rg (compile input))
|
||||
(render-to-file rg "va2.dot")
|
||||
|
||||
(define rgi (compile/internal-events rg))
|
||||
(render-to-file rgi "va2i.dot")
|
||||
|#
|
||||
|
||||
;; (Listof TraceStep) D StateName (DetectedCycle -> X) -> (U X Void)
|
||||
;; the path is in reverse, and the final step is the pair evt/dest;
|
||||
;; so their is a cycle if the sequence from the first occurrence of
|
||||
|
|
@ -2909,9 +2890,7 @@
|
|||
(define jm (run/timeout (thunk (compile jmr)) 5000))
|
||||
(check-true (role-graph? jm))
|
||||
(define jmi (run/timeout (thunk (compile/internal-events jm)) 5000))
|
||||
(check-true (role-graph? jmi))
|
||||
;; TODO : times out, probably due to infinite loop
|
||||
#;(check-true (run/timeout (thunk (simulates?/rg jmi jmi)) 100000))))
|
||||
(check-true (run/timeout (thunk (simulates?/rg jmi jmi)) 5000))))
|
||||
|
||||
(define task-runner-ty
|
||||
'(Role
|
||||
|
|
@ -3046,7 +3025,7 @@
|
|||
(check-false (simulates? tm (parse-T task-performer-spec)))))
|
||||
|
||||
|
||||
#;(module+ test
|
||||
(module+ test
|
||||
(test-case
|
||||
"job manager subgraph(s) implement task assigner"
|
||||
(define jmr (run/timeout (thunk (parse-T job-manager-actual))))
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load Diff
|
|
@ -1,21 +1,12 @@
|
|||
#!/bin/sh
|
||||
|
||||
pushd ${1%/*}/ > /dev/null
|
||||
pushd ${1%/*}/
|
||||
|
||||
EXE="$1-verifier.o"
|
||||
|
||||
spin -a $1
|
||||
if [[ $? -ne 0 ]]; then
|
||||
popd > /dev/null
|
||||
exit 1
|
||||
fi
|
||||
|
||||
gcc -o $EXE -D NFAIR=3 pan.c
|
||||
|
||||
# -a to analyze, -f for (weak) fairness
|
||||
# -n to elide report of unreached states
|
||||
# -N spec-name to verify a particular specification
|
||||
gcc -o $EXE pan.c
|
||||
$EXE -a -f -n -N $2
|
||||
rm $EXE pan.*
|
||||
rm $EXE pan.c
|
||||
|
||||
popd > /dev/null
|
||||
popd
|
||||
|
|
|
|||
|
|
@ -2,8 +2,8 @@
|
|||
|
||||
#define ASSERTED(x) (x##_assertions > 0)
|
||||
#define RETRACTED(x) (x##_assertions == 0)
|
||||
#define ASSERT(x) x##_update = x##_update + 1
|
||||
#define RETRACT(x) x##_update = x##_update - 1
|
||||
#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 */
|
||||
|
|
|
|||
|
|
@ -1,56 +0,0 @@
|
|||
#lang turnstile
|
||||
|
||||
(provide Observe★
|
||||
RoleNTimes
|
||||
(for-syntax RoleNTimes*))
|
||||
|
||||
(require "core-types.rkt")
|
||||
(require turnstile/typedefs)
|
||||
|
||||
(define-syntax (Observe★ stx)
|
||||
(define star (type-eval #'★/t))
|
||||
(syntax-parse stx
|
||||
[(_ TyCons:id)
|
||||
#:do [(define arity? (get-type-arity #'TyCons))]
|
||||
#:when arity?
|
||||
(mk-Observe- (list (reassemble-type #'TyCons (make-list (arity-min arity?) star))))]
|
||||
[(_ t)
|
||||
#:with (~Any/new TyCons τ ...) (type-eval #'t)
|
||||
#:when (reassemblable? #'TyCons)
|
||||
(mk-Observe- (list (reassemble-type #'TyCons (stx-map (lambda (_) star) #'(τ ...)))))]
|
||||
[_
|
||||
(raise-syntax-error #f "Not a type that can automatically be subscribed to" stx)]))
|
||||
|
||||
(begin-for-syntax
|
||||
;; Arity -> Nat
|
||||
(define (arity-min a)
|
||||
(match a
|
||||
[(arity-eq n) n]
|
||||
[(arity-ge n) n])))
|
||||
|
||||
(define-for-syntax (RoleNTimes* n Step behav)
|
||||
(let loop ([i 1])
|
||||
(define nm (format-id behav "step~a" i))
|
||||
(quasisyntax/loc behav
|
||||
(Role (#,nm)
|
||||
#,@(if (= i 1)
|
||||
(list #'(Shares Unit))
|
||||
(list))
|
||||
(Reacts #,(if (= i 1)
|
||||
#'(Asserted Unit)
|
||||
#`(Message #,Step))
|
||||
#,@(if (= i n)
|
||||
(list)
|
||||
(list #`(Sends #,Step))))
|
||||
(Reacts (Message #,Step)
|
||||
(Effs #,behav
|
||||
(Stop #,nm
|
||||
#,@(if (< i n)
|
||||
(if (= i 1)
|
||||
(list #`(Sends #,Step) (loop (add1 i)))
|
||||
(list (loop (add1 i))))
|
||||
(list)))))))))
|
||||
|
||||
(define-syntax-parser RoleNTimes
|
||||
[(_ ~! n:nat Step:type behav:type)
|
||||
(RoleNTimes* (syntax-e #'n) #'Step.norm #'behav.norm)])
|
||||
|
|
@ -1,22 +0,0 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
(define-constructor* (trust lvl))
|
||||
|
||||
(check-type (trust 5) : (TrustT Int))
|
||||
|
||||
(define-constructor* (hungry-hippos count appetite)
|
||||
#:with HungryHippos (HungryHipposT Int String))
|
||||
|
||||
(check-type (hungry-hippos 12 "massive") : HungryHippos)
|
||||
|
||||
(define-constructor* (doggy [color : String] [weight : Int]))
|
||||
|
||||
(check-type (doggy "black" 60) : (DoggyT String Int))
|
||||
(check-type (doggy "brown" 45) : Doggy)
|
||||
|
||||
(define-constructor* (leaf))
|
||||
|
||||
(check-type (leaf) : (LeafT))
|
||||
(check-type (leaf) : Leaf)
|
||||
|
|
@ -2,21 +2,16 @@
|
|||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
(define (∀ (ρ) (assert-something! [p : (proc → ★/t #:effects (ρ))]))
|
||||
(define (∀ (ρ) (assert-something! [p : (proc → ★/t #:endpoints (ρ))]))
|
||||
(p))
|
||||
|
||||
(define (test-fun)
|
||||
(call/inst assert-something! (lambda () (assert 5))))
|
||||
|
||||
(check-type test-fun : (proc → ★/t #:effects ((Shares NonZero))))
|
||||
|
||||
(check-type test-fun : (proc → ★/t #:endpoints ((Shares Int))))
|
||||
|
||||
(define (test-call/inst-insertion)
|
||||
(assert-something! (lambda () (assert 5))))
|
||||
|
||||
(check-type test-call/inst-insertion : (proc → ★/t #:effects ((Shares NonZero))))
|
||||
|
||||
(define (∀ (ρ) (start-something! [p : (proc → ★/t #:effects (ρ))]))
|
||||
(p))
|
||||
|
||||
(define (test-call-start-something)
|
||||
(start-something! (lambda () (start-facet x (assert 5)))))
|
||||
(check-type test-call/inst-insertion : (proc → ★/t #:endpoints ((Shares Int))))
|
||||
|
|
|
|||
|
|
@ -1,7 +0,0 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
(lambda ()
|
||||
(start-facet x
|
||||
(if #f
|
||||
(assert (tuple 0))
|
||||
(assert (tuple 1)))))
|
||||
|
|
@ -9,7 +9,7 @@
|
|||
: Int
|
||||
⇒ 0)
|
||||
|
||||
(check-type (for/fold ([x : Int 0])
|
||||
(check-type (for/fold ([x 0])
|
||||
([y (list 1 2 3)])
|
||||
y)
|
||||
: Int
|
||||
|
|
@ -20,13 +20,13 @@
|
|||
(define inventory0 (list (tuple "The Wind in the Willows" 5)
|
||||
(tuple "Catch 22" 2)
|
||||
(tuple "Candide" 33)))
|
||||
(check-type (for/fold ([stock : Int 0])
|
||||
(check-type (for/fold ([stock 0])
|
||||
([item inventory0])
|
||||
(select 1 item))
|
||||
: Int
|
||||
⇒ 33)
|
||||
|
||||
(check-type (for/fold ([stock : Int 0])
|
||||
(check-type (for/fold ([stock 0])
|
||||
([item inventory0])
|
||||
(if (equal? "Catch 22" (select 0 item))
|
||||
(select 1 item)
|
||||
|
|
@ -36,7 +36,7 @@
|
|||
|
||||
(define (lookup [title : String]
|
||||
[inv : Inventory] -> Int)
|
||||
(for/fold ([stock : Int 0])
|
||||
(for/fold ([stock 0])
|
||||
([item inv])
|
||||
(if (equal? title (select 0 item))
|
||||
(select 1 item)
|
||||
|
|
|
|||
|
|
@ -18,4 +18,4 @@
|
|||
(on start (call/inst perform-task push-results))))
|
||||
: (List String)
|
||||
-> (list
|
||||
"(Role (x) (Reacts OnStart (Role (perform) (Reacts OnStart (Stop perform (Branch (Effs (Role (done) (Shares True))) (Effs)))))))"))
|
||||
"(Role (x) (Reacts OnStart (Role (perform) (Reacts OnStart (Stop perform (Branch (Effs (Role (done) (Shares Bool))) (Effs)))))))"))
|
||||
|
|
|
|||
|
|
@ -1,41 +0,0 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
(define-constructor* (run [distance : Int] [windy? : Bool]))
|
||||
|
||||
(check-type
|
||||
(spawn
|
||||
(start-facet runner
|
||||
(assert (run 5 #t))))
|
||||
: ★/t)
|
||||
|
||||
(check-type
|
||||
(spawn
|
||||
(start-facet longer
|
||||
(on (asserted (run $d $w?))
|
||||
(printf "run ~a ~a\n" (add1 d) (if w? "brr" "")))))
|
||||
: ★/t)
|
||||
|
||||
(check-type
|
||||
(dataspace
|
||||
(spawn
|
||||
(start-facet runner
|
||||
(assert (run 5 #t))))
|
||||
(spawn
|
||||
(start-facet longer
|
||||
(on (asserted (run $d $w?))
|
||||
(printf "run ~a ~a\n" (add1 d) (if w? "brr" ""))))))
|
||||
: ★/t)
|
||||
|
||||
(typecheck-fail
|
||||
(dataspace
|
||||
(spawn
|
||||
(start-facet runner
|
||||
;; NB
|
||||
(assert (run "FAR" #t))))
|
||||
(spawn
|
||||
(start-facet longer
|
||||
(on (asserted (run $d $w?))
|
||||
(printf "run ~a ~a\n" (add1 d) (if w? "brr" ""))))))
|
||||
#:verb-msg "unprepared to handle inputs: (RunT String True)")
|
||||
|
|
@ -1,21 +0,0 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
(require/typed "struct-provider.rkt"
|
||||
[#:struct donkey [weight : Int] [grey? : Bool]])
|
||||
|
||||
(check-type (donkey 5 #t)
|
||||
: (DonkeyT Int Bool))
|
||||
|
||||
(check-type (donkey 5 #t)
|
||||
: Donkey)
|
||||
|
||||
(check-type (donkey-grey? (donkey 5 #t))
|
||||
: Bool)
|
||||
|
||||
(require/typed "struct-provider.rkt"
|
||||
[#:struct pot])
|
||||
|
||||
(check-type (pot) : (PotT))
|
||||
(check-type (pot) : Pot)
|
||||
|
|
@ -1,26 +0,0 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
(define-constructor* (ping [v : Int]))
|
||||
(define-constructor* (pong))
|
||||
|
||||
(define (spawn-asserter)
|
||||
(spawn
|
||||
(lift+define-role ar
|
||||
(start-facet a
|
||||
(assert (ping 0))))))
|
||||
|
||||
(define (spawn-responder)
|
||||
(spawn
|
||||
(lift+define-role rr
|
||||
(start-facet r
|
||||
(on (asserted (ping $x))
|
||||
(start-facet go
|
||||
(assert (pong))))))))
|
||||
|
||||
(module+ test
|
||||
(verify-actors (Eventually (A Pong))
|
||||
ar
|
||||
rr)
|
||||
|
||||
(verify-actors/fail (Eventually (A Pong))
|
||||
rr))
|
||||
|
|
@ -1,20 +0,0 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
(define (spawn-asserter)
|
||||
(spawn
|
||||
(lift+define-role ar
|
||||
(start-facet a
|
||||
(assert (tuple 0))))))
|
||||
|
||||
(module+ test
|
||||
(verify-actors (Eventually (A (Tuple Int)))
|
||||
ar)
|
||||
|
||||
(verify-actors/fail (Not (Eventually (A (Tuple Int))))
|
||||
ar)
|
||||
|
||||
(verify-actors/fail (Always (A (Tuple Int)))
|
||||
ar)
|
||||
|
||||
(verify-actors (Eventually (Always (A (Tuple Int))))
|
||||
ar))
|
||||
|
|
@ -1,38 +0,0 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
(define (fut1)
|
||||
(lift+define-role va1
|
||||
(start-facet X
|
||||
(field [state Bool #t])
|
||||
(assert (tuple (! state))))))
|
||||
|
||||
(module+ test
|
||||
(verify-actors (Eventually (A (Tuple Bool)))
|
||||
va1)
|
||||
)
|
||||
|
||||
(define-constructor* (go-true))
|
||||
(define-constructor* (go-false))
|
||||
|
||||
(define (fut2)
|
||||
(lift+define-role va2
|
||||
(export-roles "va2.rktd"
|
||||
(print-role
|
||||
(start-facet X
|
||||
(field [state Bool #f])
|
||||
(assert (tuple (! state)))
|
||||
(on (message (go-true))
|
||||
(:= state #t))))))
|
||||
|
||||
(lift+define-role gt
|
||||
(start-facet Y
|
||||
(on (asserted (tuple _))
|
||||
(send! (go-true))))))
|
||||
|
||||
(module+ test
|
||||
(verify-actors (Eventually (A (Tuple True)))
|
||||
va2
|
||||
gt)
|
||||
(verify-actors/fail (Always (Not (A (Tuple False))))
|
||||
va2
|
||||
gt))
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
#lang racket
|
||||
|
||||
(struct donkey (weight stubborn?) #:transparent)
|
||||
|
||||
(provide (struct-out donkey))
|
||||
|
||||
(struct pot () #:transparent)
|
||||
|
||||
(provide (struct-out pot))
|
||||
|
|
@ -1,23 +0,0 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
(check-type
|
||||
(role-strings
|
||||
(start-facet X
|
||||
(field [state Bool #t])
|
||||
(assert (tuple (! state)))))
|
||||
: (List String)
|
||||
-> (list "(Role (X) (VarAssert state (--> (U False True) (Tuple (U False True))) (--> False (Tuple False)) (--> True (Tuple True))) (MakesField state (U False True) True))"))
|
||||
|
||||
(define (spawn-B)
|
||||
(spawn
|
||||
(start-facet B
|
||||
(field [Bst Bool #t])
|
||||
(assert (tuple (! Bst))))))
|
||||
|
||||
(lambda ()
|
||||
(lift+define-role rA
|
||||
(start-facet A (on start (spawn-B))
|
||||
(field [Ast Bool #t])
|
||||
(assert (tuple (! Ast))))))
|
||||
Loading…
Reference in New Issue