remove self loops, things working better
This commit is contained in:
parent
16175c7bb4
commit
b17cba59ed
|
@ -139,14 +139,18 @@
|
||||||
([nm (in-set current)])
|
([nm (in-set current)])
|
||||||
(define txns (hash-ref roles# nm))
|
(define txns (hash-ref roles# nm))
|
||||||
(hash-union agg txns #:combine combine-effect-sets)))
|
(hash-union agg txns #:combine combine-effect-sets)))
|
||||||
|
(define (build-transitions D effs)
|
||||||
|
(for*/set ([eff* (in-set effs)]
|
||||||
|
[txn (in-set (apply-effects eff* current ft roles#))]
|
||||||
|
;; filter effect-free self-loops
|
||||||
|
#:unless (and (empty? (transition-effs txn))
|
||||||
|
(equal? (transition-dest txn) current)))
|
||||||
|
txn))
|
||||||
(define transitions
|
(define transitions
|
||||||
(for/hash ([(D effs) (in-hash agg-txn)]
|
(for/hash ([(D effs) (in-hash agg-txn)]
|
||||||
#:when (external-evt? D))
|
#:unless (start/stop-evt? D)
|
||||||
;; TODO - may want to remove self loops here
|
[txns (in-value (build-transitions D effs))]
|
||||||
(define txns
|
#:unless (set-empty? txns))
|
||||||
(for*/set ([eff* (in-set effs)]
|
|
||||||
[txn (in-set (apply-effects eff* current ft roles#))])
|
|
||||||
txn))
|
|
||||||
(values D txns)))
|
(values D txns)))
|
||||||
(define new-work
|
(define new-work
|
||||||
(for*/list ([txns (in-hash-values transitions)]
|
(for*/list ([txns (in-hash-values transitions)]
|
||||||
|
@ -172,7 +176,8 @@
|
||||||
;; (work-item StateName (Listof StateName) D (Listof D) (Listof TransitionEffect))
|
;; (work-item StateName (Listof StateName) D (Listof D) (Listof TransitionEffect))
|
||||||
;; such as (work-item from path/r to by with effs), where
|
;; such as (work-item from path/r to by with effs), where
|
||||||
;; - from is the origin state for this chain of events
|
;; - from is the origin state for this chain of events
|
||||||
;; - path/r is the list of states in the path to this point, in reverse
|
;; - path/r is the list of states in the path to this point, *after* from, in reverse
|
||||||
|
;; (meaning that all of these transitions are due to *internal* events)
|
||||||
;; - to is the current state that has been reached
|
;; - to is the current state that has been reached
|
||||||
;; - by is the external event that kicked off this sequence
|
;; - by is the external event that kicked off this sequence
|
||||||
;; - with is a list of pending events to be processed
|
;; - with is a list of pending events to be processed
|
||||||
|
@ -192,26 +197,28 @@
|
||||||
;; TODO - st0 might have changed
|
;; TODO - st0 might have changed
|
||||||
(role-graph st0 states)]
|
(role-graph st0 states)]
|
||||||
[(cons (work-item from path/r to by with effs) more-work)
|
[(cons (work-item from path/r to by with effs) more-work)
|
||||||
(define prev (first path/r))
|
(define prev (if (empty? path/r) from (first path/r)))
|
||||||
(define txn# (state-transitions (hash-ref orig-st#+ to)))
|
(define txn# (state-transitions (hash-ref orig-st#+ to)))
|
||||||
(define visited+ (set-add visited to))
|
(define visited+ (set-add visited to))
|
||||||
(define st#+ (if (hash-has-key? st# to) st# (hash-set st# to (hash))))
|
(define st#+ (if (hash-has-key? st# to) st# (hash-set st# to (hash))))
|
||||||
(define new-paths-work
|
(define new-events (route-internal (hash-ref assertion# prev)
|
||||||
|
(hash-ref assertion# to)))
|
||||||
|
;; -> (Listof WorkItem)
|
||||||
|
;; when this state is the end of a path, it can be the start of some new paths
|
||||||
|
(define (new-paths-work)
|
||||||
(for*/list (#:unless (set-member? visited to)
|
(for*/list (#:unless (set-member? visited to)
|
||||||
[(D txns) (in-hash txn#)]
|
[(D txns) (in-hash txn#)]
|
||||||
#:when (external-evt? D)
|
#:when (external-evt? D)
|
||||||
#:unless (equal? D DataflowEvt)
|
#:unless (equal? D DataflowEvt)
|
||||||
[t (in-set txns)])
|
[t (in-set txns)])
|
||||||
(match-define (transition es dst) t)
|
(match-define (transition es dst) t)
|
||||||
(work-item to (list to) dst D (effs->internal-events es) es)))
|
(work-item to '() dst D (effs->internal-events es) es)))
|
||||||
(define new-events (route-internal (hash-ref assertion# prev)
|
|
||||||
(hash-ref assertion# to)))
|
|
||||||
(cond
|
(cond
|
||||||
[(and (empty? with)
|
[(and (empty? with)
|
||||||
(set-empty? new-events)
|
(set-empty? new-events)
|
||||||
(not (hash-has-key? txn# DataflowEvt)))
|
(not (hash-has-key? txn# DataflowEvt)))
|
||||||
(define new-st# (update-path st#+ from to by effs))
|
(define new-st# (update-path st#+ from to by effs))
|
||||||
(walk (append more-work new-paths-work) visited+ new-st#)]
|
(walk (append more-work (new-paths-work)) visited+ new-st#)]
|
||||||
[else
|
[else
|
||||||
;; TODO - this is saying something about how the implementation schedules handlers;
|
;; TODO - this is saying something about how the implementation schedules handlers;
|
||||||
;; I think it should be something like exploring (append with (permutations new-events))
|
;; I think it should be something like exploring (append with (permutations new-events))
|
||||||
|
@ -228,7 +235,7 @@
|
||||||
(match pending/first-relevant
|
(match pending/first-relevant
|
||||||
['()
|
['()
|
||||||
(define new-st# (update-path st#+ from to by effs))
|
(define new-st# (update-path st#+ from to by effs))
|
||||||
(walk (append more-work new-paths-work) visited+ new-st#)]
|
(walk (append more-work (new-paths-work)) visited+ new-st#)]
|
||||||
[(cons evt more-pending)
|
[(cons evt more-pending)
|
||||||
(define path/r+ (cons to path/r))
|
(define path/r+ (cons to path/r))
|
||||||
(define more-labor
|
(define more-labor
|
||||||
|
@ -248,7 +255,7 @@
|
||||||
by
|
by
|
||||||
(append more-pending internal-effs)
|
(append more-pending internal-effs)
|
||||||
(append effs more-effs))))
|
(append effs more-effs))))
|
||||||
(walk (append more-work more-labor new-paths-work) visited+ st#+)])])]))
|
(walk (append more-work more-labor) visited+ st#+)])])]))
|
||||||
(walk (list (work-item (set) (list (set)) st0 StartEvt '() '()))
|
(walk (list (work-item (set) (list (set)) st0 StartEvt '() '()))
|
||||||
(set)
|
(set)
|
||||||
(hash))))
|
(hash))))
|
||||||
|
@ -288,16 +295,21 @@
|
||||||
;; -> (Hashof StateName (Hashof D (Setof Transition)))
|
;; -> (Hashof StateName (Hashof D (Setof Transition)))
|
||||||
;; record an edge between from and to based on the given event and emitting some effects
|
;; record an edge between from and to based on the given event and emitting some effects
|
||||||
(define (update-path st# from to by effs)
|
(define (update-path st# from to by effs)
|
||||||
(define txn (transition effs to))
|
(cond
|
||||||
(hash-update st#
|
[(and (equal? from to)
|
||||||
from
|
(empty? effs))
|
||||||
(lambda (txn#)
|
st#]
|
||||||
(hash-update txn#
|
[else
|
||||||
by
|
(define txn (transition effs to))
|
||||||
(lambda (txns)
|
(hash-update st#
|
||||||
(set-add txns txn))
|
from
|
||||||
(set)))
|
(lambda (txn#)
|
||||||
(hash)))
|
(hash-update txn#
|
||||||
|
by
|
||||||
|
(lambda (txns)
|
||||||
|
(set-add txns txn))
|
||||||
|
(set)))
|
||||||
|
(hash))]))
|
||||||
|
|
||||||
;; (Listof (TransitionEffect)) -> (Listof D)
|
;; (Listof (TransitionEffect)) -> (Listof D)
|
||||||
(define (effs->internal-events effs)
|
(define (effs->internal-events effs)
|
||||||
|
@ -320,6 +332,12 @@
|
||||||
[_
|
[_
|
||||||
#f]))
|
#f]))
|
||||||
|
|
||||||
|
;; D -> Bool
|
||||||
|
;; test if D corresponds to Start or Stop event
|
||||||
|
(define (start/stop-evt? D)
|
||||||
|
(or (equal? D StartEvt)
|
||||||
|
(equal? D StopEvt)))
|
||||||
|
|
||||||
(module+ test
|
(module+ test
|
||||||
(test-case
|
(test-case
|
||||||
"compile seller"
|
"compile seller"
|
||||||
|
@ -1333,12 +1351,10 @@
|
||||||
(define tpr (parse-T task-performer-spec))
|
(define tpr (parse-T task-performer-spec))
|
||||||
(define tmr (parse-T task-manager-ty))
|
(define tmr (parse-T task-manager-ty))
|
||||||
(define ans (simulating-subgraphs tmr tpr))
|
(define ans (simulating-subgraphs tmr tpr))
|
||||||
(check-equal? (length ans) 4)
|
(check-equal? (length ans) 2)
|
||||||
(define tprg (compile tpr))
|
(define tprg (compile tpr))
|
||||||
(check-true (simulates?/rg (first ans) tmr tprg tpr))
|
(check-true (simulates?/rg (first ans) tmr tprg tpr))
|
||||||
(check-true (simulates?/rg (second ans) tmr tprg tpr))
|
(check-true (simulates?/rg (second ans) tmr tprg tpr))))
|
||||||
(check-true (simulates?/rg (third ans) tmr tprg tpr))
|
|
||||||
(check-true (simulates?/rg (fourth ans) tmr tprg tpr))))
|
|
||||||
|
|
||||||
;; RoleGraph (Setof τ) -> (Sequenceof RoleGraph)
|
;; RoleGraph (Setof τ) -> (Sequenceof RoleGraph)
|
||||||
;; generate non-empty subgraphs, where at least the given assertions are enabled
|
;; generate non-empty subgraphs, where at least the given assertions are enabled
|
||||||
|
@ -2189,6 +2205,7 @@
|
||||||
(check-false (simulates? tm (parse-T task-assigner-spec)))
|
(check-false (simulates? tm (parse-T task-assigner-spec)))
|
||||||
(check-false (simulates? tm (parse-T task-performer-spec)))))
|
(check-false (simulates? tm (parse-T task-performer-spec)))))
|
||||||
|
|
||||||
|
;; has a bug with done facet dying too soon
|
||||||
(define job-manager-v2
|
(define job-manager-v2
|
||||||
'(Role
|
'(Role
|
||||||
(jm)
|
(jm)
|
||||||
|
@ -2293,6 +2310,95 @@
|
||||||
(check-true (list? ans))
|
(check-true (list? ans))
|
||||||
(check-false (empty? ans))))
|
(check-false (empty? ans))))
|
||||||
|
|
||||||
|
;; fixed above bug
|
||||||
|
(define job-manager-v3
|
||||||
|
'(Role
|
||||||
|
(jm)
|
||||||
|
(Shares (JobManagerAlive))
|
||||||
|
(Reacts
|
||||||
|
(Asserted
|
||||||
|
(Job
|
||||||
|
(Bind Symbol)
|
||||||
|
(Bind (List (Task Int (U (MapWork String) (ReduceWork Int Int)))))))
|
||||||
|
(Role
|
||||||
|
(during-inner)
|
||||||
|
(Reacts
|
||||||
|
OnStart
|
||||||
|
(Role
|
||||||
|
(delegate-tasks)
|
||||||
|
(Reacts
|
||||||
|
OnDataflow
|
||||||
|
(Role
|
||||||
|
(perform)
|
||||||
|
(Reacts
|
||||||
|
OnStart
|
||||||
|
(Role
|
||||||
|
(select)
|
||||||
|
(Reacts (Forget (SelectedTM (Bind Symbol))))
|
||||||
|
(Reacts
|
||||||
|
OnDataflow
|
||||||
|
(Branch
|
||||||
|
(Effs
|
||||||
|
(Branch
|
||||||
|
(Effs
|
||||||
|
(Role
|
||||||
|
(assign)
|
||||||
|
(Shares
|
||||||
|
(TaskAssignment
|
||||||
|
Symbol
|
||||||
|
Symbol
|
||||||
|
(Task
|
||||||
|
Int
|
||||||
|
(U
|
||||||
|
(MapWork String)
|
||||||
|
(ReduceWork (Hash String Int) (Hash String Int))))))
|
||||||
|
(Know (SelectedTM Symbol))
|
||||||
|
(Reacts
|
||||||
|
(Asserted
|
||||||
|
(TaskState
|
||||||
|
Symbol
|
||||||
|
Symbol
|
||||||
|
Int
|
||||||
|
(Bind (U (Finished (Hash String Int)) Symbol))))
|
||||||
|
(Branch
|
||||||
|
(Effs)
|
||||||
|
(Effs)
|
||||||
|
(Effs (Stop assign))
|
||||||
|
(Effs
|
||||||
|
(Stop
|
||||||
|
perform
|
||||||
|
(Branch
|
||||||
|
(Effs
|
||||||
|
(Realizes (TasksFinished Symbol (Hash String Int))))
|
||||||
|
(Effs))))))
|
||||||
|
(Reacts
|
||||||
|
OnStart
|
||||||
|
(Role
|
||||||
|
(take-slot)
|
||||||
|
(Reacts
|
||||||
|
(Asserted (TaskState Symbol Symbol Int Discard))
|
||||||
|
(Stop take-slot))))
|
||||||
|
(Reacts
|
||||||
|
(Retracted (TaskManager Symbol Discard))
|
||||||
|
(Stop assign))))
|
||||||
|
(Effs)))
|
||||||
|
(Effs)))))
|
||||||
|
(Reacts OnStop)
|
||||||
|
(Reacts OnStart)))
|
||||||
|
(Reacts
|
||||||
|
(Realize (TasksFinished Symbol (Bind (Hash String Int))))
|
||||||
|
(Stop
|
||||||
|
delegate-tasks
|
||||||
|
(Role (done) (Shares (JobFinished Symbol (Hash String Int))))))))
|
||||||
|
(Reacts
|
||||||
|
(Retracted
|
||||||
|
(Job
|
||||||
|
Symbol
|
||||||
|
(List (Task Int (U (MapWork String) (ReduceWork Int Int))))))
|
||||||
|
(Stop during-inner))))
|
||||||
|
(Reacts (Retracted (TaskManager (Bind Symbol) (Bind Int))))
|
||||||
|
(Reacts (Asserted (TaskManager (Bind Symbol) (Bind Int))))))
|
||||||
|
|
||||||
;; ---------------------------------------------------------------------------
|
;; ---------------------------------------------------------------------------
|
||||||
;; Message Examples/Tests
|
;; Message Examples/Tests
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue