Menu
▾
▴
[Golok-commit] SF.net SVN: golok:[14] trunk
|
From: <sr...@us...> - 2010-03-10 19:54:22
|
Revision: 14
http://golok.svn.sourceforge.net/golok/?rev=14&view=rev
Author: sralmai
Date: 2010-03-10 19:54:16 +0000 (Wed, 10 Mar 2010)
Log Message:
-----------
[IMPLEMENTATION CHANGE]: non-parameterized processes are filtered out of 1e model (use --npp <name> to specify a non-parameterized process)
Modified Paths:
--------------
trunk/examples/producer-consumer.amf
trunk/find-k.scm
trunk/model-builder.scm
trunk/search.scm
Modified: trunk/examples/producer-consumer.amf
===================================================================
--- trunk/examples/producer-consumer.amf 2010-03-09 05:10:18 UTC (rev 13)
+++ trunk/examples/producer-consumer.amf 2010-03-10 19:54:16 UTC (rev 14)
@@ -14,7 +14,8 @@
#recvnak2: [WaitMutex, mutexNAKcons] -> [WaitMutex, setcons]
#recvok2: [WaitMutex, mutexOKcons] -> [GetBuffer, getcons]
getnak2: [GetBuffer, bufferNAKcons] -> [GetBuffer, getcons]
-getok2: [GetBuffer, bufferOKcons] -> [GetBuffer, getcons]
+getok2: [GetBuffer, bufferOKcons] -> [HasCosumed, in]
+in: [HasConsumed, in] -> [GetBuffer, getcons]
#recvreplay: [ClearMutex, mutexCLEARcons] -> [GetBuffer, getcons]
}
@@ -54,6 +55,7 @@
topology {
(producer, item, self)
+ (consumer, in, self)
(producer, bufferOKprod, peer)
(producer, bufferNAKprod, peer)
# (producer, mutexOKprod, peer)
Modified: trunk/find-k.scm
===================================================================
--- trunk/find-k.scm 2010-03-09 05:10:18 UTC (rev 13)
+++ trunk/find-k.scm 2010-03-10 19:54:16 UTC (rev 14)
@@ -215,9 +215,10 @@
[name (list-ref names id)]
[mask (remove name names)])
(let-values ([(tt oneE-builder) (build-oneEmodel-builder prot)])
- (let ([dummy0 (if dump-1E (model2dot (oneE-builder name start-aut)
+ (let ([dummy0 (if dump-1E (model2dot (oneE-builder name start-aut (map (lambda (x) (item-index x names)) npp))
(string-append output-directory "/" (symbol->string name) "-1e.dot") #:show-buf #f) (void))])
(let-values ([(soln data) (search prot k name dfs start-aut
+ #:npp npp
#:ring ring
#:dump dump
#:star star
@@ -258,6 +259,7 @@
(find-solution-rec id names (modulo (add1 cur_ch) size) best-trace))
(let* ([new-k (rule 'apply k)])
(let-values ([(soln data) (search prot new-k (list-ref names id) dfs start-aut
+ #:npp npp
#:ring ring
#:star star
#:start start-depth
Modified: trunk/model-builder.scm
===================================================================
--- trunk/model-builder.scm 2010-03-09 05:10:18 UTC (rev 13)
+++ trunk/model-builder.scm 2010-03-10 19:54:16 UTC (rev 14)
@@ -131,7 +131,7 @@
(let ([tt (create-lookup-table (protocol-ba prot) #t)])
(values
tt
- (lambda (proc-type initial-aut [verbose #f])
+ (lambda (proc-type initial-aut id-mask [verbose #f])
(let* ([all-aut (protocol-ba prot)]
; set the global eps-id from the lookup table
[dmy (set! eps-id (msg->msg-id eps tt))]
@@ -148,8 +148,8 @@
[dummy2 (if verbose (display-ln "Building oneEmodel...") (void))]
[md (build-model initial-state tt)]
[model (hash->model md tt oneE-flag initial-state)]
- ;; now filter out the taus and all other transition types
- [stripped (strip-taus-short model (proc->proc-id proc-type tt) tt)]
+ ;; now filter out the taus and object transition types
+ [stripped (strip-taus model id-mask tt)]
;; remove all duplicate paths
[cleaned-model (reduce-model stripped)]
;; remove lonely nodes (without transitions to or from)
@@ -189,7 +189,7 @@
(let* ([model (remove-tau-linking raw-model lt)])
model))
-(define (strip-taus raw-model proc-id lt)
+(define (strip-taus raw-model id-mask lt)
(let* ([model (remove-tau-linking raw-model lt)]
[new-model (make-vector (vector-length model))]
; lookups to compacted model (without "extra" start states)
@@ -208,7 +208,7 @@
(build-list (vector-length new-model) values))
; for each state reachable via non-tau links, add the map
- (add-elements-rec 0 proc-id model new-model mapper)
+ (add-elements-rec 0 id-mask model new-model mapper)
;; return the compacted new model
(compact-model new-model mapper))))
@@ -241,9 +241,9 @@
-(define (add-elements-rec index proc-id model new-model mapper)
+(define (add-elements-rec index id-mask model new-model mapper)
(if (hash-has-key? mapper index) (void)
- (let* ([trans (remove-duplicates (collect-endpoints index proc-id model))]
+ (let* ([trans (remove-duplicates (collect-endpoints index id-mask model))]
[new-entry (vector-ref new-model index)]
[size (hash-count mapper)])
(begin
@@ -251,25 +251,25 @@
(vector-set! new-model index new-entry)
(hash-set! mapper index size)
(for-each
- (lambda (x) (add-elements-rec (vector-ref x 3) proc-id model new-model mapper))
+ (lambda (x) (add-elements-rec (vector-ref x 3) id-mask model new-model mapper))
trans)))))
-(define (collect-endpoints state-index proc-id model)
+(define (collect-endpoints state-index id-mask model)
(let ([ends (make-vector 1 (list))]
[visit-list (make-hash)])
(begin
- (collect-endpoints-rec state-index proc-id model ends visit-list)
+ (collect-endpoints-rec state-index id-mask model ends visit-list)
(vector-ref ends 0))))
-(define (collect-endpoints-rec state-index proc-id model ends visited-list)
+(define (collect-endpoints-rec state-index id-mask model ends visited-list)
(if (hash-has-key? visited-list state-index)
; if we've been here before, die
(void)
;; count the transitions
- (let* ([pid-tran (filter (lambda (y) (= proc-id (state-id->proc-id (vector-ref y 2))))
+ (let* ([non-pid-tran (filter (lambda (y) (member (state-id->proc-id (vector-ref y 2)) id-mask))
(vector-ref (vector-ref model state-index) 1))]
- [non-pid-tran (filter (lambda (y) (not (= proc-id (state-id->proc-id (vector-ref y 2)))))
+ [pid-tran (filter (lambda (y) (not (member y non-pid-tran)))
(vector-ref (vector-ref model state-index) 1))])
(begin
; mark this index
@@ -280,13 +280,13 @@
(vector-set! ends 0 (append pid-tran (vector-ref ends 0))))
; if everything is a tau transition, don't add these transitions, just their children
((null? pid-tran)
- (for-each (lambda (z) (collect-endpoints-rec z proc-id model ends visited-list))
+ (for-each (lambda (z) (collect-endpoints-rec z id-mask model ends visited-list))
(map (lambda (a) (vector-ref a 3)) non-pid-tran)))
; otherwise, add these transitions and their children
(#t
(begin
(vector-set! ends 0 (append pid-tran (vector-ref ends 0)))
- (for-each (lambda (z) (collect-endpoints-rec z proc-id model ends visited-list))
+ (for-each (lambda (z) (collect-endpoints-rec z id-mask model ends visited-list))
(map (lambda (a) (vector-ref a 3)) non-pid-tran)))))))))
;;
Modified: trunk/search.scm
===================================================================
--- trunk/search.scm 2010-03-09 05:10:18 UTC (rev 13)
+++ trunk/search.scm 2010-03-10 19:54:16 UTC (rev 14)
@@ -100,6 +100,12 @@
; print optimizations debugging output
(define opt-dbg 0)
+; ids of non-parameterized process names as integers
+(define npp-ids (list))
+
+; ids of parameterized process names as integers
+(define pp-ids (list))
+
;; start state
(define start-state (void))
;;;;;;;;;;;;;;;;;;;;
@@ -116,6 +122,7 @@
; start - integer-depth | #f
; stop - integer-depth | #f
(lambda (prot topo pt dfs oneE-start-aut
+ #:npp [npp (list)]
#:dump [dump #f]
#:ring [r #f]
#:star [s (list)]
@@ -123,7 +130,15 @@
#:stop [stop-d #f])
(let-values ([(stepper ss lookup-table topo-hash) (init-stepper prot topo)])
(begin
+
+ ; save the ids of all parameterized system types
+ (set! npp-ids (map (lambda (x) (item-index x (protocol-process-names prot))) npp))
+ (set! pp-ids (filter (lambda (x) (not (member x npp-ids))) (build-list (length (protocol-process-names prot)) values)))
+ ; debug
+ (display-ln "npp-ids: " npp-ids)
+ (display-ln "pp-ids: " pp-ids)
+
; TODO: generalize these reductions (and maybe figure them out from the topology)
(cond
((and r (not (null? s)))
@@ -186,7 +201,7 @@
(set! other-mask-ids (map (lambda (x) (proc->proc-id x lt)) other-mask))
(let-values ([(fresh-tt builder) (build-oneEmodel-builder prot)])
- (set! oneE (model-mdl (builder proc-type oneE-start-aut))))
+ (set! oneE (model-mdl (builder proc-type oneE-start-aut npp-ids))))
; debugging messages
(if (>= debug 2) (display-ln "checking " (topology->string topo) " for simulation of "
@@ -378,11 +393,11 @@
(#t
; otherwise, expand all possible branches
; first collect all states reachable via tau transitions
- (let* ([starts (list state)];(explode state (list proc-type-id))]
+ (let* ([starts (explode state pp-ids)]
; then collect all the proc-type transitions possible from the start set
[possibles
;(list-of-lists->list (map (lambda (x) (expand x other-mask-ids #t)) starts))]
- (list-of-lists->list (map (lambda (x) (expand x (list) #t)) starts))]
+ (list-of-lists->list (map (lambda (x) (expand x npp-ids #t)) starts))]
; finally sort the transitions according to the needed 1e transitions
[check-list (condense possibles index)])
@@ -584,7 +599,7 @@
(if (equal? start-state end-state) (void)
(let* ([end-db (make-hash)]
[dmy (hash-set! end-db (state->representative end-state) #t)]
- [possibles (remove-duplicates (expand start-state (list proc-type-id) #t))]
+ [possibles (remove-duplicates (expand start-state pp-ids #t))]
; since there *is* a path to the end-state, this ormap always gives a non #f result
;
; if it *does* return false, there is an error in our search algorithm
@@ -607,7 +622,7 @@
#t)
;; add all generated todos to done-db and filter out todos that were previously there
(let* ([possibles ;(filter (lambda (x) (if (hash-has-key? done-db x) #f #t))
- (expand end-state (list proc-type-id) #t)]
+ (expand end-state pp-ids #t)]
[dbg0 (if (>= debug 4) (display-ln "possibles for connect-taus-rec: " possibles) (void))])
(if (null? possibles) #f
(let ([res (ormap (lambda (x) (connect-taus-rec x final-db db)) possibles)])
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
