Menu
▾
▴
[Golok-commit] SF.net SVN: golok:[12] trunk
|
From: <sr...@us...> - 2010-03-05 05:41:04
|
Revision: 12
http://golok.svn.sourceforge.net/golok/?rev=12&view=rev
Author: sralmai
Date: 2010-03-05 05:40:56 +0000 (Fri, 05 Mar 2010)
Log Message:
-----------
[IMPLEMENTATION CHANGE]: 1e is constructed for each initiating process only from its epsilon transition, but all non-initiating are constructed from every single epsilon transition. Also, lr-dpp starting position is fixed (to 2,2 instead of 3,3).
Modified Paths:
--------------
trunk/examples/lr-dpp.topo
trunk/find-k.scm
trunk/model-builder.scm
trunk/search.scm
Added Paths:
-----------
trunk/examples/lr-dpp-22.topo
Added: trunk/examples/lr-dpp-22.topo
===================================================================
--- trunk/examples/lr-dpp-22.topo (rev 0)
+++ trunk/examples/lr-dpp-22.topo 2010-03-05 05:40:56 UTC (rev 12)
@@ -0,0 +1,35 @@
+#
+# lr-dpp.topo
+#
+# describes the initial system instance
+# for left right dining philosophers
+# protocol
+#
+
+# corresponding automata file
+model: lr-dpp.amf
+
+# simple process counts
+counts:
+
+left-diner 2
+right-diner 2
+
+# explicit links between processes
+links:
+
+# across this link, right-diner 1 is the
+# left peer (lpeer) and left-diner 0 is
+# the right peer (rpeer)
+#
+# so the topology rule
+# (left-diner, left-taken, lpeer)
+# means that left-diner 0 can
+# consume a "left-taken" message
+# from right-diner 1
+right-diner 1 -> left-diner 0
+
+left-diner 0 -> right-diner 0
+right-diner 0 -> left-diner 1
+
+left-diner 1 -> right-diner 1
Modified: trunk/examples/lr-dpp.topo
===================================================================
--- trunk/examples/lr-dpp.topo 2010-03-02 05:32:14 UTC (rev 11)
+++ trunk/examples/lr-dpp.topo 2010-03-05 05:40:56 UTC (rev 12)
@@ -1 +1 @@
-link lr-dpp-33.topo
\ No newline at end of file
+link lr-dpp-22.topo
\ No newline at end of file
Modified: trunk/find-k.scm
===================================================================
--- trunk/find-k.scm 2010-03-02 05:32:14 UTC (rev 11)
+++ trunk/find-k.scm 2010-03-05 05:40:56 UTC (rev 12)
@@ -151,36 +151,40 @@
(init-internals filename)
- (for-each
- (lambda (x)
- (let* ([processes (protocol-process-names prot)]
- [proc-type (list-ref processes x)]
- [proc-mask (remove proc-type processes)])
- (if dump-sys
- (model2dot (find-solution x)
- (string-append output-directory "/" (symbol->string proc-type) "-sys.dot") proc-mask)
- (find-solution x))))
-
-
- ; if only checking a single process type, find its index number and return a singleton list
- (if process-type
+ (let*
+ ([eps-auts (filter (lambda (z) (equal? eps (automaton-in-msg z))) (protocol-ba prot))]
+ [starts (if process-type
(let* ([names (protocol-process-names prot)]
[index (item-index process-type names)])
- (cond
- ((< index 0) (raise-user-error "ERROR: process not found: ~s" process-type))
- ((not (ormap (lambda (z) (eq? eps (automaton-in-msg z)))
- (filter (lambda (p) (equal? process-type (automaton-proc-type p))) (protocol-ba prot)))) (raise-user-error "ERROR: process must have an epsilon transition: ~s does not" process-type))
- (#t
+ (if (< index 0) (raise-user-error "Invalid process index ~s" process-type)
(begin
(display-ln "INFO: only checking " process-type " for simulation\n")
- (list index)))))
- ; otherwise, check all process indices with
-
- (let ([names (protocol-process-names prot)])
- (filter (lambda (pn)
- (ormap (lambda (z) (eq? eps (automaton-in-msg z)))
- (filter (lambda (a) (equal? (list-ref names pn) (automaton-proc-type a))) (protocol-ba prot))))
- (build-list (length names) values)))))
+ (list index))))
+ ; otherwise, check all process indices
+ (build-list (length (protocol-process-names prot)) values))])
+
+ (for-each
+ (lambda (start-aut)
+ (for-each
+ (lambda (x)
+ (let* ([processes (protocol-process-names prot)]
+ [proc-type (list-ref processes x)]
+ [proc-mask (remove proc-type processes)])
+ (cond
+ ; if this is an epsilon initiated process and not starting from its start, skip
+ ((and (member (list-ref processes x) (map automaton-proc-type eps-auts)) (not (equal? (automaton-proc-type start-aut) (list-ref processes x))))
+ (void))
+ (dump-sys
+ (model2dot (find-solution x start-aut)
+ (string-append output-directory "/" (symbol->string proc-type) "-from-"
+ (symbol->string (automaton-proc-type start-aut)) "-sys.dot") proc-mask))
+ (#t
+ (find-solution x start-aut)))))
+
+ ; if only checking a single process type, find its index number and return a singleton list
+ starts))
+ eps-auts))
+
(dump-solution))))
(define dump-solution
@@ -196,14 +200,15 @@
;; TODO: clean up find-solution and find-solution-rec
(define find-solution
- (lambda (id)
+ (lambda (id start-aut)
(let* ([names (protocol-process-names prot)]
[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)
- (string-append output-directory "/" (symbol->string name) "-1E.dot") #:show-buf #f) (void))])
- (let-values ([(soln data) (search prot k name dfs
+ (let ([dummy0 (if dump-1E (model2dot (oneE-builder name start-aut)
+ (string-append output-directory "/" (symbol->string name) "-from-"
+ (symbol->string (automaton-proc-type start-aut)) "-1e.dot") #:show-buf #f) (void))])
+ (let-values ([(soln data) (search prot k name dfs start-aut
#:ring ring
#:dump dump
#:star star
@@ -212,7 +217,7 @@
(if soln
; if soln == #t, then data is a model containing the simulating subset of the system
data
- (find-solution-rec id names 0 data))))))))
+ (find-solution-rec id start-aut names 0 data))))))))
;; if we try all addition rules and none work, which rule should be applied before looping over them again
@@ -231,7 +236,7 @@
; cur_ch: index of the rule to apply
; best-trace: integer measure of how close model has come to simulating 1e
(define find-solution-rec
- (lambda (id names cur_ch best-trace)
+ (lambda (id start-aut names cur_ch best-trace)
(let* ([rules (protocol-addition-rules prot)]
[rule (list-ref (protocol-addition-rules prot) cur_ch)]
[size (length rules)]
@@ -243,7 +248,7 @@
(if (>= debug 4) (display-ln "-------\n" "rule " rule " cannot be applied... skipping") (void))
(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
+ (let-values ([(soln data) (search prot new-k (list-ref names id) dfs start-aut
#:ring ring
#:star star
#:start start-depth
@@ -259,7 +264,7 @@
(begin
(set! k new-k)
(set! made-a-change #t)
- (find-solution-rec id names (modulo (+ 1 cur_ch) size) data)))
+ (find-solution-rec id start-aut names (modulo (+ 1 cur_ch) size) data)))
; is the the last rule before trying them all again?
((= 0 (modulo (+ 1 cur_ch) size))
@@ -268,17 +273,17 @@
; clear the flag and continue
(begin
(set! made-a-change #f)
- (find-solution-rec id names (modulo (+ 1 cur_ch) size) best-trace))
+ (find-solution-rec id start-aut names (modulo (+ 1 cur_ch) size) best-trace))
; otherwise apply the next rule
(begin
(set! made-a-change #f)
(set! k ((list-ref (protocol-addition-rules prot) next-id-to-inc) 'apply k))
(set! next-id-to-inc (modulo (+ 1 cur_ch) size))
- (find-solution-rec id names (modulo (+ 1 cur_ch) size) best-trace))))
+ (find-solution-rec id start-aut names (modulo (+ 1 cur_ch) size) best-trace))))
; otherwise just continue to the next rule
- (#t (find-solution-rec id names (modulo (+ 1 cur_ch) size) best-trace)))))))))
+ (#t (find-solution-rec id start-aut names (modulo (+ 1 cur_ch) size) best-trace)))))))))
; depreciated
Modified: trunk/model-builder.scm
===================================================================
--- trunk/model-builder.scm 2010-03-02 05:32:14 UTC (rev 11)
+++ trunk/model-builder.scm 2010-03-05 05:40:56 UTC (rev 12)
@@ -131,28 +131,53 @@
(let ([tt (create-lookup-table (protocol-ba prot) #t)])
(values
tt
- (lambda (proc-type [verbose #f])
+ (lambda (proc-type initial-aut [verbose #f])
(let* ([all-aut (protocol-ba prot)]
; set the global eps-id from the lookup table
- [dmyyy (set! eps-id (msg->msg-id eps tt))]
- [initial-aut
- (let* ([record (filter (lambda (x) (and
- (equal? (car x) proc-type)
- (= (cadr x) 0))) (protocol-start-conf prot))])
- (if (not (null? record)) (caddar record) (car (filter (lambda (z) (equal? proc-type (automaton-proc-type z))) all-aut))))]
+ [dmy (set! eps-id (msg->msg-id eps tt))]
+ ; [initial-aut
+ ; (let* ([record (filter (lambda (x) (and
+ ; (equal? (car x) proc-type)
+ ; (= (cadr x) 0))) (protocol-start-conf prot))])
+ ; (if (not (null? record)) (caddar record) (car (filter (lambda (z) (equal? proc-type (automaton-proc-type z))) all-aut))))]
[state-id (state->state-id (vector (automaton-proc-type initial-aut) (automaton-name initial-aut) #f) tt)]
- [initial-state (list (state->process state-id))]
- ; [initial-state (if (eq? (automaton-in-msg initial-aut) eps)
- ; (collect-all-eps initial-aut all-aut tt)
- ; (list (state->process state-id)))]
+ [initial-state (list (state->process state-id))]
+
+ ; [initial-state (if (eq? (automaton-in-msg initial-aut) eps)
+ ; (collect-all-eps initial-aut all-aut tt)
[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 model (proc->proc-id proc-type tt) tt)]
- [cleaned-model (reduce-model stripped)])
- (make-model cleaned-model tt)))))))
+ ;; remove all duplicate paths
+ [cleaned-model (reduce-model stripped)]
+ ;; remove lonely nodes (without transitions to or from)
+ [finished (compactify cleaned-model)])
+ (make-model finished tt)))))))
+
+;; simple front-end to compact-model
+(define (compactify model)
+ (let ([mapper (make-hash)])
+ (begin
+ ; mark all reachable elements
+ (mark-elements-rec model 0 mapper)
+ (compact-model model mapper))))
+
+
+
+(define (mark-elements-rec model index mapper)
+ (let ([size (hash-count mapper)])
+ (if (hash-has-key? mapper index)
+ (void)
+ (begin
+ (hash-set! mapper index size)
+ ;; add all children
+ (for-each (lambda (x) (mark-elements-rec model x mapper))
+ (map (lambda (z) (vector-ref z 3)) (vector-ref (vector-ref model index) 1)))))))
+
+
;;
;; strip-taus
;;
Modified: trunk/search.scm
===================================================================
--- trunk/search.scm 2010-03-02 05:32:14 UTC (rev 11)
+++ trunk/search.scm 2010-03-05 05:40:56 UTC (rev 12)
@@ -115,7 +115,8 @@
; star - (list-of process-types of which system states are equivalent when swapped around)
; start - integer-depth | #f
; stop - integer-depth | #f
- (lambda (prot topo pt dfs #:dump [dump #f]
+ (lambda (prot topo pt dfs oneE-start-aut
+ #:dump [dump #f]
#:ring [r #f]
#:star [s (list)]
#:start [start-d #f]
@@ -185,7 +186,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))))
+ (set! oneE (model-mdl (builder proc-type oneE-start-aut))))
; debugging messages
(if (>= debug 2) (display-ln "checking " (topology->string topo) " for simulation of "
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
