Menu
▾
▴
[Golok-commit] SF.net SVN: golok:[10] trunk
|
From: <sr...@us...> - 2010-03-01 01:26:33
|
Revision: 10
http://golok.svn.sourceforge.net/golok/?rev=10&view=rev
Author: sralmai
Date: 2010-03-01 01:26:24 +0000 (Mon, 01 Mar 2010)
Log Message:
-----------
[IMPLEMENTATION CHANGE]: Now builds a 1e model for each process type from each epsilon transition. Tested with lr-dpp, dme, dme-mult, and SpinLock. Golok finds a cut-off of 3-3 for lr-dpp in 75 seconds on my machine. (Note: the states in the 1e model visualization show the automaton (not necessarily of the same type as the starting automaton) which consumes the message produced in the previous transition.)
Modified Paths:
--------------
trunk/find-k.scm
trunk/model-builder.scm
trunk/search.scm
Modified: trunk/find-k.scm
===================================================================
--- trunk/find-k.scm 2010-03-01 00:44:47 UTC (rev 9)
+++ trunk/find-k.scm 2010-03-01 01:26:24 UTC (rev 10)
@@ -151,15 +151,18 @@
(init-internals filename)
+ (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)])
(if dump-sys
- (model2dot (find-solution x)
- (string-append output-directory "/" (symbol->string proc-type) "-sys.dot") proc-mask)
- (find-solution x))))
+ (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)
+ (find-solution x start-aut))))
; if only checking a single process type, find its index number and return a singleton list
@@ -171,7 +174,11 @@
(display-ln "INFO: only checking " process-type " for simulation\n")
(list index))))
; otherwise, check all process indices
- (build-list (length (protocol-process-names prot)) values)))
+ (build-list (length (protocol-process-names prot)) values))))
+
+ ;; collect all automata which take an epsilon in message
+ (filter (lambda (z) (equal? eps (automaton-in-msg z))) (protocol-ba prot)))
+
(dump-solution))))
(define dump-solution
@@ -187,14 +194,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
@@ -203,7 +211,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
@@ -222,7 +230,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)]
@@ -234,7 +242,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
@@ -250,7 +258,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))
@@ -259,17 +267,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-01 00:44:47 UTC (rev 9)
+++ trunk/model-builder.scm 2010-03-01 01:26:24 UTC (rev 10)
@@ -131,27 +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 (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-01 00:44:47 UTC (rev 9)
+++ trunk/search.scm 2010-03-01 01:26:24 UTC (rev 10)
@@ -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.
|
